fix(phd): remove '84 theorems' and 'anchor paper' overclaims (R5-honest)#744
Merged
Conversation
Phase 3 of L-DOI-HONEST sweep (after PR #739 + #740). After Zenodo metadata rehab (NASA report ZENODO-REHAB-2026-05-12-T22:45), canonical records 19227877 / 19227879 are R5-honest software description stubs. PhD monograph still carried legacy 'Trinity anchor paper' / '84 theorems' phrasings that contradict the audited reality. Fixes: - docs/phd/appendix/G-data-availability.tex: AVL-1 and AVL-3 descriptions now say 'software description stub'; AVL-1 links to gHashTag/t27/coq with audited counts (48 statements, 35 Proven, 0 Admitted on 2026-05-12) - docs/phd/bibliography.bib: two @misc entries for DOI 19227877 rewritten to drop 'paper' / '84 theorems' wording; note fields explicitly state 'software description stub, not a peer-reviewed paper' and link Coq witness with audited counts - docs/phd/frontmatter/list-of-theorems.tex: TODO-3 no longer hard-codes '≥84 theorems' target; uses audit-driven count instead - docs/phd/reproducibility.md: 'Trinity paper anchor' row renamed; added explicit Coq witness row with audit counts - docs/phd/theorems/igla/README.md: references row points to audited counts in gHashTag/t27/coq Anchor: phi^2 + phi^-2 = 3 (algebraic identity). DOI 10.5281/zenodo.19227877 is a software description stub of Trinity B007. No theorem counts are claimed in title / abstract metadata anymore (see ZENODO-REHAB report).
…ited counts PASS-2 of L-DOI-HONEST after the 2026-05-12 community-attach audit found 8 more files in trios that contained R5 violations the Phase-3 PR #744 did not cover, plus the Phase-3 counts themselves (48 statements / 35 Proven) turned out to be a SUBSET (only docs/phd/theorems/Kernel/* + /Theorems/*), not the full gHashTag/t27 Coq corpus. Source of truth on 2026-05-12 — gHashTag/t27 (clone, audit cmd: `find ./coq ./proofs -name '*.v' -print0 | xargs -0 grep -hcE '...'`): 28 .v files (10 under coq/, 18 under proofs/) 218 statements (122 Theorem + 96 Lemma) 162 Qed | 32 Admitted | 11 Abort NO proofs/canonical/ directory NO _Manifest.json Earlier framings retired in this commit: - "84 Coq theorems" (4 files) - "84 + 5 = 89 (F_11 Fibonacci prime)" (1 file) - "376 Theorems for the IGLA Invariants" / "312 Qed, 64 Admitted" (1 file) - "Trinity Anchor record (TRI-27 series)" (1 file) - "TRI-27 anchor DOI" (1 file) - "297 Qed canonical + SHA-1 manifest across 65 .v files" (1 file) - Phase-3 understated 48/35/0 counts (5 files) Fixes: - artifact/CLAIMS.md: "Trinity Anchor record (TRI-27 series)" -> "software description stub for Trinity B007 (NOT a peer-reviewed paper)" + audited Coq counts - docs/golden-sunflowers/app-b-golden-ledger-297-qed-canonical-sha-1.md: prepended [SUPERSEDED — 2026-05-12 R5-honest sweep] banner; document retained for provenance but explicitly marked unverified (the proofs/canonical/ directory and _Manifest.json it describes do not exist) - docs/phd/appendix/G-data-availability.tex: update audit row from 48/35/0 to 218/162/32/11 + 28 files - docs/phd/bibliography.bib: zenodo_trinity + coq_companion_zenodo notes now say "software description stub, NOT a peer-reviewed paper" and quote the audited 218/162/32 counts; the second entry retires the "376 Theorems" title in favour of "Audited Trinity Invariants (IGLA)" - docs/phd/frontmatter/list-of-theorems.tex: TODO comment now uses 218 statements / 162 Qed instead of 48/35 - docs/phd/reproducibility.md: row count updated to 218/162/32/11 - docs/phd/theorems/igla/README.md: same - docs/research/coq-invariants-strategy.md: TL;DR diagram + invariants section quote audited counts (218 t27-side, 340 trios-PhD-side) - tools/acm_ae_check/src/lib.rs: ZENODO_DOI const doc explicitly identifies the deposit as "Trinity B007 software description stub (NOT a paper)"; TRI-27 anchor phrasing dropped - trinity-clara/proofs/README.md: F_11=89 cosmetic framing retired; "Connection to Existing 84 Theorems" section now points to the audited Trinity Coq corpus with a footnote explaining the supersession Anchor: phi^2 + phi^-2 = 3 (algebraic identity, falsifiable independently of any DOI). Audited Coq witness: https://github.com/gHashTag/t27/tree/main/coq + https://github.com/gHashTag/t27/tree/main/proofs (28 .v files, 218 statements, 162 Qed, 32 Admitted, 11 Abort, audit 2026-05-12) Co-authored-by: Trinity Queen Hive <queen-hive@trinity.local>
Owner
Author
|
🌀 PASS-2 push — this PR now contains an additional commit closing R5 violations the original Phase-3 sweep missed. What's new in PASS-2:
📜 Full NASA mission report: ZENODO-REPO-AUDIT-PASS-2-2026-05-12-T23:50 φ² + φ⁻² = 3 · R5-HONEST · TRINITY |
…7 -> 19020270/75/80/82) + bump zenodo-registry verified date to 2026-05-12
PASS-3 anomalies fixed in trios (17 files):
- docs/golden-sunflowers/{app-a, app-f, ch-6, ch-8, ch-14, ch-21, ch-30}.md: 35+ D-series DOI replacements
- docs/phd/chapters/{ch_06, ch_08, ch_14, ch_21, ch_30, fa_06, fa_08, fa_14, fa_30}.tex: same
- docs/infrastructure/zenodo-registry.md: §4 D-series table canonical DOIs + Retired note + §7 D-series-mid-March row + footer updated; §1 rule 5 anchor reworded as software description stub
All references now point to canonical 2026-05-12 D-series records.
R5 verification: 0 hallucinated/superseded DOI references remain in trios.
Anchor: phi^2 + phi^-2 = 3
Issue: #264
Owner
Author
🔥 PASS-3 update — three new anomaly classes purgedThis PR was expanded with PASS-3 fixes discovered after PASS-2 was declared complete. R5 honesty gate triggered a third iterative deep sweep. Three new anomaly classes found and fixed:
See full NASA PASS-3 report: trios#264 — NASA PASS-3 RVR-003 comment R5 verification (post-PASS-3): 0 hallucinated / 0 superseded / 0 self-DOI errors remain across all three repos. Anchor: |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
🔴 R5-HONEST · Phase 3 of L-DOI-HONEST sweep
Companion to PR #739 (trios), PR #137 (trainer), and ZENODO-REHAB report.
Context
Phase 2 (Zenodo metadata rehab, 2026-05-12) made all canonical Trinity Zenodo records R5-honest: "software description stub, not a peer-reviewed paper", linked to gHashTag/t27/coq witness (48 statements, 35 Proven, 0 Admitted).
Phase 3 (this PR) fixes the matching repo-side overclaims that survived the previous sweep — found via deep-grep across gHashTag/{trios,trinity,trinity-fpga,trios-trainer-igla} (279 files touched 10.5281/zenodo.*, 7 carried R5 violations).
Witness
fix/zenodo-repo-honest-deepsweep.grep -rE '^\s*(Theorem|Lemma|Qed|Admitted)\s+' coq --include='*.v'in gHashTag/t27.Anchor
phi^2 + phi^-2 = 3(algebraic identity, not an empirical claim).