feat(canonical): 🌻 CANONICAL COQ HOME — 38 bundles / 297 Qed / single source of truth

[gHashTag]

🏠 CANONICAL COQ HOME — Single Source of Truth

Anchor: phi^2 + phi^-2 = 3 · TRINITY · v3.0 MEASURED HARDWARE · 🌻

After the 2026-04-30 Coq theorem census (trios#373) discovered that the Trinity stack's actual Coq corpus is 438 theorems / 376 Qed across 65 canonical files in 3 repos — not the previously claimed 47 Qed — this PR establishes t27/proofs/canonical/ as the SINGLE SOURCE OF TRUTH for all Trinity Coq proofs.

What lands in this PR

proofs/canonical/
├── _Index.v              ← master Require Import (38 bundles)
├── _CoqProject           ← Coq build (logical paths Trinity.Canonical.{Sacred,Kernel,Igla})
├── _Manifest.json        ← bundle → source-mirror manifest with SHA-1 content hashes
├── Makefile              ← `make all` invokes coqc; `make verify-counts` grep audit
├── README.md             ← full census + quickstart + provenance
├── sacred/   (17 files)  ← phi-mathematics + Standard Model bounds
├── kernel/    (9 files)  ← phi/Trit/E8 building blocks
├── igla/     (12 files)  ← INV-1..INV-9 runtime invariants
└── refutation/           ← R5-honest falsification index (lemmas inline in IGLA)

Canonical audit (deduped, this PR)

Metric	Count
Bundles canonicalized	38
Theorem-like declarations	333
Qed (proven)	297
Admitted (R5-honest budget)	41
Abort (WIP, no silent merges)	11
Files added	39 (.v) + 4 metadata + 1 CI workflow

Source-of-truth dedup picks max(Qed) − 0.5·Admitted − 0.3·Abort per logical bundle across mirrors in gHashTag/{trinity-clara, t27, trios}. Each canonical file carries a header with SPDX, INV-#, PhD chapter slot, content SHA-1, and source-mirror reference (provenance preserved verbatim).

IGLA invariants (runtime contract, INV-1..INV-9)

Bundle	INV	Qed	Title
INV1_BpbMonotoneBackward.v	INV-1	9	BPB Monotone Backward Pass
INV1b_LrPhiOptimality.v	INV-1b	5	lr_phi optimality
INV2_IglaAshaBound.v	INV-2	13	ASHA Champion Survival (threshold 3.5)
INV3_Gf16Precision.v	INV-3	9	GF16 Safe Domain
INV4_NcaEntropyBand.v	INV-4	12	NCA Entropy Band 1.5..2.8 (81 = 3⁴)
INV5_LucasClosureGf16.v	INV-5	10	Lucas Closure (φ^{2n}+φ^{-2n} ∈ ℤ)
INV6_HybridQkGain.v	INV-6	2+5A	Hybrid QK Gain φ²
INV7_IglaFoundCriterion.v	INV-7	11	Victory Criterion (≥3 distinct, BPB<1.5, step≥4000)
INV7b_RainbowBridgeConsistency.v	INV-7b	15+2A	Rainbow Bridge Consistency
INV8_WorkerPoolComposite.v	INV-8	10	Worker Pool Composite
INV9_EmaDecayValid.v	INV-9	8	EMA Decay Valid
IglaCatalog.v	catalog	5	Composite IGLA predicate

Sacred core (17 bundles, phi-math + SM bounds)

CorePhi.v (12 Qed, anchor trinity_identity), AlphaPhi.v (12), ExactIdentities.v (11+11A), DerivationLevels.v (21), Catalog42.v (13), FormulaEval.v (17), ConsistencyChecks.v (7+7A), Unitarity.v (5+2A, CKM+PMNS), BoundsGauge.v (9), BoundsLeptonMasses.v (8A), BoundsMasses.v (11), BoundsMixing.v (9), BoundsQuarkMasses.v (4+4A), GammaPhi3.v (1), L5Identity.v (2), StrongCP.v (1), DLBounds.v (1).

Kernel (9 bundles)

Phi.v (16), PhiAttractor.v (4+5Abort), PhiFloat.v (6), PhiDistance.v (1), FlowerE8Embedding.v (5+6Abort), Trit.v (1), Semantics.v (1), GenIdempotency.v (1), TernarySufficiency.v (2).

CI verification

.github/workflows/coq-canonical.yml:

• audit-counts job — fast grep-only audit (no compile), gates Qed ≥ 280 and Admitted ≤ 50
• coq-compile job — coq-community/docker-coq-action@v1 with Coq 8.18 + OCaml 4.14-flambda, runs make against _CoqProject to verify all 38 bundles compile

R5-honest disclosure

• 41 Admitted. lemmas with explicit close-with comments (Coq.Interval for sqrt5 irrationality, Welch t-test bounds, real induction over phi^(2n))
• 11 Abort. markers preserve work-in-progress (kernel PhiAttractor.v / FlowerE8Embedding.v)
• 28 refutation_* / *_falsification_* lemmas — every INV paired with explicit refutation example (refutation_jepa_proxy, refutation_pre_warmup, inv2_falsification_is_contradiction, gf16_falsification_witness, etc.)
• AI-as-author forbidden everywhere — only "AI-assisted code generation" in Acknowledgments

Companion PRs (follow-up)

• gHashTag/trinity-clara: stub proofs/igla/*.v → Require Export Trinity.Canonical.Igla.<INV>
• gHashTag/trios: stub docs/phd/theorems/**/*.v → Require Export Trinity.Canonical.<cat>.<file>
• gHashTag/trios: stub trinity-clara/proofs/igla/*.v → Require Export Trinity.Canonical.Igla.<INV>

These will land after this PR merges, so the imports resolve.

Provenance

• Census artefact: trios#373 comment
• PhD App.E (Pre-reg PDF): trios#416
• PhD Ch.10 (Coq L1 Pareto): trios#400
• PhD Ch.31 (Golden Seal): trios#95
• GOLDEN SUNFLOWERS Master Book: trios#380

Acknowledgments

AI-assisted code generation; human first-author and review.

phi^2 + phi^-2 = 3 · TRINITY · 297 Qed canonical · t27 = HOME · 🌻

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.