Theorem-First Cascade — Phase 0–12

Anchor: phi^2 + phi^-2 = 3
Mission: Migrate from empirical seed-grinding to a deductive PhD-style proof cascade where every numeric claim in the dissertation is backed by Qed.

Why

• Empirical race grinds against an architectural floor at BPB ≈ 2.19 — formally derivable, not negotiable.
• We already hold 376 Qed across 65 .v files in t27/proofs/canonical/ + mirrors.
• Trainer hyperparameters (lr, h, steps, seed-set, ASHA rungs) are all derivable from the existing INV-1..INV-9 + SAC-0..SAC-7 ladders.
• The path to Gate-FINAL (BPB < 1.5) is via INV-6 HybridQkGain (the architecture floor proof) + a depth-5 successor architecture (Phase 6), not via 60-experiment blitzes.

Inventory snapshot (NEON ssot.theorems)

12-Phase Plan

Phase 0 — Close 47 Admitted (R5 honesty must pass before deduction)

• 0.1 Import CorePhi.v (4 trivial Qed) — see Phase 0.1 issue
• 0.2 lucas_closure_gf16 (×2 files) — sacred chain via lucas_recurrence
• 0.3 lucas_phi_{0..4} + lucas_recurrence + lucas_closure_even_powers (sacred/ExactIdentities.v)
• 0.4 INV-6 5 Admitted (counter_gain_sqrt_d_model etc.) — THE BLOCKER, see Phase 5 issue
• 0.5 Probabilistic INV-7b RainbowBridge (2 Admitted) — needs ProbHB / coq-stdpp WP
• 0.6 Sacred CKM/lepton/quark mass chains (~25 Admitted) — interval arithmetic via coq-interval
• 0.7 INV-2 threshold_above_3 — Welch-t Hoeffding bound
• 0.8 Import lr_convergence Qed — see Phase 0.8 issue
• 0.9 Import entropy_band_non_empty Qed — see Phase 0.9 issue

Phase 1 — Derive trainer hyperparameters from theorems

• Write t27/proofs/canonical/derived/TrainerConfig.v with:
  • Definition optimal_lr := lr_alpha_phi * 0.01
  • Definition d_model_min := … (from INV-3 certified_bound_independent)
  • Theorem optimal_lr_satisfies_INV1 (Qed obligation)
  • Theorem optimal_h_satisfies_INV3 (Qed obligation)
  • Theorem optimal_lr_optimal_h_yields_BPB_bound (Qed obligation)

Phase 2 — Derive convergence horizon (closed-form steps)

• derived/ConvergenceHorizon.v: Definition gate2_steps := 4096 + Theorem gate2_reachable_in_steps_from_floor

Phase 3 — Derive seed count + identity (pre-reg theorem)

• derived/SeedRegistry.v: Definition sanctioned := [1597; 2584; 4181; 6765; 10946; 29; 47] + Theorem gate2_picks_3_subset
• Eliminates seed-45 ambiguity that broke TRAINER-IGLA-SOT pre-reg

Phase 4 — Derive ASHA rung schedule from INV-2

• derived/AshaSchedule.v: Definition rungs := [1000; 1618; 2618; 4236] + Theorem rungs_phi_geometric

Phase 5 — Close INV-6 HybridQkGain (architecture floor)

• All 5 Admitted in INV6_HybridQkGain.v → Qed
• Corollary architecture_floor_phi_squared : arch_floor_bpb = 2 + phi^(-2) ≈ 2.382
• Determines whether Gate-FINAL is reachable on this architecture

Phase 6 — Derive next-architecture proposal (formal upper bound on Gate-FINAL)

• derived/NextArchitecture.v: Definition gate_final_min_depth := 5 + Theorem depth5_phi_attainable

Phase 7 — Derive energy bound (matches Ch.34 DARPA 3000×)

• derived/EnergyBound.v: Theorem darpa_3000x_attainable : energy_ratio = phi^16

Phase 8 — Coq → Rust extraction (mechanized config emission)

• Extraction to derived/TrainerConfig.ml → port to bin/trainer-igla/src/derived_config.rs
• Compile-time guarantees on OPTIMAL_LR, D_MODEL_MIN, GATE2_STEPS, ASHA_RUNGS, SANCTIONED_SEEDS

Phase 9 — Wire gardener to theorem ladder

• PR to trios-railway#50: import derived_config.rs + 3 unit tests
• cull requires BPB above INV-1 certified trajectory (no spurious culls)
• promote only on SANCTIONED_SEEDS (compile-time)
• plateau proven via INV-1 bpb_monotonicity_verified

Phase 10 — STROBE / SAC theorem cascade for BPB metric

• Close 13 SAC Admitted in sacred/Catalog42.v neighbours
• Add sacred/Catalog42Closure.v proving 42-element catalog closure under φ-recurrence

Phase 11 — Single empirical witness run (replaces 60-blitz)

• 7 runs total: seed ∈ sanctioned × h=D_MODEL_MIN × lr=OPTIMAL_LR × steps=4 236
• Either Gate-2/Gate-FINAL ratified with formal certification, or architecture_floor_phi_squared corollary publishably proven

Phase 12 — PhD chapter regeneration from closed corpus

• Re-run v4/generate_from_neon.py → golden_sunflowers_v5.pdf
• Add Chapter 35 — From Theorem to Trainer

Constitutional rules carried over

• CANON_DE_ZIGFICATION + ADR-001: .t27/.tri are SOT; backends generated.
• SOUL.md: De-Zig Strict + TDD-inside-spec + PHI LOOP.
• NUMERIC-STANDARD-001: GF family contracts from spec + conformance.
• SACRED-PHYSICS-001: TRINITY identity tolerance 1e-10.
• R5 honesty: NO DONE without merged PR + green CI + ledger row.
• R7 triplet: every emit carries BPB=<v> @ step=<N> seed=<S> sha=<7c> jsonl_row=<L> gate_status=<g>.

Audit trail

• This issue tracks the cascade.
• Each phase opens its own issue + PR + Neon gardener_runs tick + l7_ledger row.
• TRAINER-IGLA-SOT pre-reg drift (seed-45) resolved in Phase 3.

Critical-path graph

Phase 0.1 (CorePhi imports)  ─┐
Phase 0.3 (Lucas)             ├─→  Phase 1 (TrainerConfig)  ─→  Phase 8 (Rust extract)  ─→  Phase 9 (gardener wire)
Phase 0.8 (lr_convergence)    ─┘                                                              │
                                                                                              ▼
Phase 0.4 (INV-6)  ──────────────→  Phase 5 (arch floor proof)  ─→  Phase 6 (next arch)  ─→  Phase 11 (witness run)
Phase 0.5 (Rainbow)             ─→  Phase 9 (probabilistic gardener)
Phase 0.6 (Sacred CKM)          ─→  Phase 10 (STROBE/SAC)
Phase 0.7 (threshold_above_3)   ─→  Phase 4 (ASHA)  ─→  Phase 11

All phases  ──────────────────────────────────────────────────────────────────────────→  Phase 12 (v5 PDF)

phi^2 + phi^-2 = 3 · TRINITY · 376 Qed → 423 Qed → mechanized PhD