docs(clara): honest PhD/Coq provenance, fix proof-count contradictions

[gHashTag]

Summary

Add docs/TRINITY_PHD_PROVENANCE.md as the canonical, auditable provenance appendix for this DARPA CLARA PA-25-07-02 submission, and rewire the application/submission documents to cite audited proof counts and PhD/Trinity provenance instead of the stale v1.1 "84 Coq theorems" headline.

• Proof counts (now consistent across all documents):
  • IGLA bundle in this repo (proofs/igla/): 47 Qed, 4 Admitted (with declared close_with: paths), 1 honest Qed-placeholder bound to a runtime guard, 1 Axiom, 10 falsification witnesses across 8 .v files. Source: proofs/igla/_metadata.json.
  • Upstream gHashTag/t27 Coq base (audit cutoff 2026-05-12): 28 .v files, 218 stated Theorem/Lemma, 162 Qed / 32 Admitted / 2 Abort.
  • README now carries an explicit "honest scoping" note: this repo is a submission slice, not the full upstream proof base, and the IGLA bundle is not fully proven — it is honestly partial.
• PhD / upstream provenance added: gHashTag/trios:docs/phd/ (chapters Ch. 22 / 24 / 28 / 34 and App. B/F/G/H/I/M/N as pointers — canonical paths live in trios), gHashTag/trios:crates/trios-phd/ (Rust audit harness), assertions/igla_assertions.json (runtime invariant contract / L-R14), and review threads trios#372 / trios#264.
• Zenodo DOIs added (framework 10.5281/zenodo.19227879, φ/VSA 10.5281/zenodo.19227877, FPGA 10.5281/zenodo.18947017) — marked as software/provenance handles, not a proof source.
• Team consistency: added Dmitrii Vasilev ORCID 0009-0008-4294-6159 to bios in README, EXECUTIVE-SUMMARY, and CLARA-COST-PROPOSAL. Flagged missing affiliation/ORCID for Dr. Stergios Pellis as an explicit pre-submission TODO without inventing data. Re-keyed the cost proposal's anonymous "PI feat(canonical): 🌻 Stub 7 mirror files → Trinity Canonical Coq Home (companion to t27#569) #1 / PI fix(coq): L-CLARA-FREEZE — close 2 Admitted (Strategy A) — trios#562 #2" rows to the named PI + Co-Is used elsewhere in the package.
• Contradictions fixed:
  • Red Team 100% (50/50) vs 96% (48/50): proposal §4.7 now aligns on the canonical 50/50 source from evidence/CLARA-RED-TEAM.md, with a one-sentence note explaining the retired figure.
  • Bibliography entry L-COQ-SWEEP-CLARA-4: close 4 Admitted in trinity-clara proofs/igla/ #3 in submission/EXECUTIVE-SUMMARY.md had a milestone-table row glued into it — restored to a clean Stakhov/Aranson citation and pointed milestone-table readers to proposal/CLARA-PROPOSAL-TECHNICAL.md §7.
  • Stale "84 Coq theorems" headline removed from README, EXECUTIVE-SUMMARY, CLARA-SUBMISSION-PACKAGE, SUBMISSION_REPORT, SUBMISSION-FINAL-REPORT, submission/README, CLARA-PROPOSAL-TECHNICAL, ARCHITECTURE, FAQ, CLARA-LITERATURE-REVIEW, CLARA-SOA-COMPARISON, CLARA-IMPROVEMENTS-SUMMARY. Surviving mentions are explicit historical-context notes ("v1.1 cited 84 …").

No changes to proofs/, assertions/, test_vectors/, code, or performance/energy claims. This PR is provenance/honesty plumbing, not a science change.

Files changed

• Added: docs/TRINITY_PHD_PROVENANCE.md
• Modified: README.md, submission/EXECUTIVE-SUMMARY.md, submission/CLARA-SUBMISSION-PACKAGE.md, submission/README.md, submission/SUBMISSION-FINAL-REPORT.md, submission/SUBMISSION_REPORT.md, proposal/CLARA-PROPOSAL-TECHNICAL.md, proposal/CLARA-COST-PROPOSAL.md, evidence/CLARA-IMPROVEMENTS-SUMMARY.md, evidence/CLARA-LITERATURE-REVIEW.md, evidence/CLARA-SOA-COMPARISON.md, docs/ARCHITECTURE.md, docs/FAQ.md

Test plan

• Verified IGLA proof counts directly from proofs/igla/*.v and proofs/igla/_metadata.json (47 Qed / 4 Admitted / 1 placeholder / 1 axiom / 10 witnesses for the canonical six-INV bundle; documented separately for the additional CorePhi.v / hybrid_qk_gain.v files in the provenance appendix).
• grep sweep confirms every surviving "84 Coq theorems" mention is now in an explicit historical-context note (v1.1 snapshot retired).
• grep sweep confirms no remaining anonymous "PI feat(canonical): 🌻 Stub 7 mirror files → Trinity Canonical Coq Home (companion to t27#569) #1 / PI fix(coq): L-CLARA-FREEZE — close 2 Admitted (Strategy A) — trios#562 #2" rows.
• Red Team numbers consistent: 100% (50/50) across README, EXECUTIVE-SUMMARY, submission, evidence/CLARA-RED-TEAM, proposal §4.7.
• Co-I ORCID present in README, EXECUTIVE-SUMMARY, CLARA-COST-PROPOSAL, and provenance appendix.
• No markdownlint or test harness is checked into this repo, so no automated lint was run. Manual review of new links and counts only.

Remaining honest risks

• Dr. Pellis affiliation/ORCID is still missing. Flagged in three places with <!-- TODO --> comments; must be filled in before final submission seal.
• CorePhi.v / hybrid_qk_gain.v are post-_metadata.json additions and currently carry additional Admitted obligations beyond the 4 budgeted in the canonical IGLA bundle. The provenance appendix discloses them honestly but does not count them as closed — that work continues upstream.
• PhD chapter numbers (Ch. 22 / 24 / 28 / 34 / App. B/F/G/H/I/M/N) are pointers into gHashTag/trios:docs/phd/. If the published thesis renumbers, the appendix language already says "canonical paths are whatever is checked in to trios:docs/phd/" — but reviewers chasing a specific chapter should consult trios directly.
• The phrase "84 Coq theorems" still appears in a few git log / historical-change-note contexts inside the proposal; we did not rewrite git history. Anyone running historical diffs may still encounter the figure.

🤖 Generated with Claude Code