SilverSight/docs/reviews/CONJECTURE_UPGRADE_ROADMAP.md

Conjecture Upgrade Roadmap

How to turn each sorry into a theorem

Four conjectures in UnifiedCovariant.lean are currently tagged sorry. Each has a precise upgrade path from informal conjecture to formal theorem.

Reorganized 2026-07-02 (covariant semi-symmetry test). §§2–4 were ordered by "blocked on Mathlib." They are re-subordinated to a new §0 active milestone: a direct curvature computation that names the covariant semi-symmetry hypothesis on the classical rung (symmetric / semisymmetric / pseudosymmetric) using an explicit metric + connection — no ℂℙⁿ, jet bundles, or Berger classification required. Resolve §0 first; §§2–4 are then corollaries or get re-scoped by its result.

---

0. ACTIVE MILESTONE — Covariant Semi-Symmetry Discriminator

Goal. Place the geometric object on the classical ladder — symmetric (∇R = 0, Cartan) / semisymmetric (R·R = 0, Szabó) / pseudosymmetric (R·R = f·Q(g,R), Deszcz) — by finite tensor computation on a written-down metric + connection. Unlike §§2–4 this needs no missing Mathlib infrastructure; it is computable now (by hand / CAS / the 12-language rig, then Lean once the tensors are pinned).

Load-bearing correction this milestone must resolve. The static Fisher–Rao metric on Δ₇, g_ij = δ_ij / p_i, is positive-definite (all p_i > 0) — signature (7,0), Riemannian. Under p ↦ 2√p it is isometric to an orthant of the round sphere S⁷: constant curvature, hence fully symmetric (∇R = 0), holonomy SO(7). This contradicts §4's claimed signature (1,6) / SO⁰(1,6): the bare Fisher metric is at the top of the ladder, not "semi," and (1,6) cannot come from it.

Where "semi" and (1,6) actually come from — the Kelvin/Rossby upgrade. rossbyDriftFromChirality (BraidStateN.lean) supplies a signed, directional β-term (left = +1, right = −1, scarred = ±½, achiral = 0), explicitly "analogous to the planetary vorticity gradient β." Kelvin/Rossby waves solve a hyperbolic operator whose signature in 7D is (1, n−1) = (1, 6): the one time-like direction is the drift/propagation direction the chirality selects; the six space-like directions are the simplex. So SO⁰(1,6) is a property of the drift-perturbed wave operator, not the static metric — and the directional (chiral) drift is precisely what breaks ∇R = 0, pushing the object off "symmetric" onto the "semi" rung. The Kelvin/Rossby directionality upgrade is therefore not supporting evidence; it is the load-bearing mechanism of the hypothesis.

Test sequence.

• 0a — Baseline (decisive, essentially done). Static φ-scaled Fisher–Rao on Δ₇ is positive-definite (7,0) and symmetric (∇R = 0), holonomy SO(7). Establishes that any "semi" / (1,6) structure must be drift-induced. 🟢
• 0b — Drift-perturbed connection. Define the connection modified by rossbyDriftFromChirality (preferred direction / torsion / Randers– Finsler directional term). Show its signature is (1,6) — deriving SO⁰(1,6) from the wave operator, replacing §4's static-metric justification. 🟡
• 0c — Ladder placement. Compute ∇R and R·R of the drift-perturbed structure. ∇R = 0 → symmetric; R·R = 0 with ∇R ≠ 0 → semisymmetric (Szabó) = the hypothesis; R·R = f·Q(g,R) → pseudosymmetric (Deszcz). 🟡
• 0d — Physics↔geometry edge. Verify the ∇R obstruction direction equals the Rossby β / drift direction (chiral → Rossby/dispersive; achiral → Kelvin/eigensolid-trapped). A match is a verified edge from the formalism to named geophysical directionality (Rossby westward, Kelvin unidirectional from Coriolis) → populates ene.relations with provenance = the computation. 🟡

Outcome. The hypothesis is either named (a rung + a proof) or refuted (∇R = 0 even after drift → symmetric all along). Both are verified edges, not mirages.

---

1. Eigensolid Convergence

File location: UnifiedCovariant.lean:146 Status: ✅ RESOLVED (2026-06-26, Sidon-orthogonality bypass). Location: formal/SilverSight/PIST/UnifiedCovariant.lean — Layer 2. Resolution: Replaced spectral operator norm with computable L∞ row-sum bound.

What was done

1. crossingMatrix (Matrix (Fin 8) (Fin 8) ℚ) defined with explicit Sidon entries: diagonal σ = 39/256, paired off-diagonal τ = 1/7.

2. maxRowSum — L∞ row-sum norm, computed by dec_trivial over Fin 8.

3. crossing_matrix_norm_bound proved: maxRowSum crossingMatrix ≤ 1775/1792.

4. braid_operator_contractive — for any state vector s ∈ ℚ^8, |(C·s)_i| ≤ r · ‖s‖_∞ where r = 1775/1792.

5. EigensolidConvergenceHypothesis (deprecated) removed.

6. Build: lake build SilverSight — 3307 jobs, 0 errors.

Key insight (Sidon-orthogonality bypass)

The Sidon uniqueness property (I₄) guarantees at most 2 non-zero entries per row of C. Each row sum is then a concrete rational — evaluating all 8 rows and comparing to 1775/1792 is a finite computation (dec_trivial), not a spectral analysis. No NormedSpace topology, no eigenvalues, no continuous analysis.

Documentation

• Formula doc: docs/reviews/SIDON_ORTHOGONALITY_BYPASS_FORMULA.md
• Breakglass log: BREAKGLASS_LOG.md (entry 2)

---

2. Golden ℂℙ⁷ is Kähler

File location: UnifiedCovariant.lean:217 Current status: def goldenCP7 : Type := sorry Blocking issue: ℂℙ⁷ as a complex manifold is not in Mathlib.

Upgrade to theorem

Standard fact. The complex projective space \mathbb{CP}^n with the Fubini–Study metric g_{FS} and the standard complex structure J_0 (satisfying J_0^2 = -I) is a Kähler manifold. Scaling the metric by any positive constant preserves the Kähler condition.

Theorem statement:

Let \mathbb{CP}^7 be complex projective space with the standard complex structure J_0 and the (\phi)-scaled Fubini–Study metric g = \phi \cdot g_{FS}. Then (\mathbb{CP}^7, J_0, g) is a Kähler manifold with Kähler form \omega = \phi \cdot \omega_{FS}.

Formal statement in Lean:

theorem goldenCP7_is_Kaehler : KaehlerManifold goldenCP7 := ...

where KaehlerManifold is defined by the triple (M, J, \omega) with J^2 = -I, d\omega = 0, and \omega(JX, JY) = \omega(X, Y).

The role of \phi. The golden ratio scales the metric but does not appear in the complex structure. The cohomology class of the Kähler form is [\omega] = \phi \cdot [\omega_{FS}] \in H^{1,1}(\mathbb{CP}^7). The conjecture from the unified model is that this particular scaling factor \phi is forced by the spectral gap \sigma - \tau, i.e.,

[ \phi = \frac{[\omega]}{[\omega_{FS}]} ]

relates the geometric structure to the discrete Layer-1 invariants.

Prerequisites:

• Formal definition of \mathbb{CP}^n as a complex manifold (does not exist in Mathlib as of 2026-06)
• Definition of the Fubini–Study metric and Kähler form
• Proof that d\omega_{FS} = 0 (standard)

Upgrade difficulty: 🔴 Hard — blocked by missing Mathlib infrastructure.

---

3. Cartan Connection on J^1(\Delta_7)

File location: UnifiedCovariant.lean:224 Current status: theorem Cartan_connection_on_J1_exists : admits_Cartan_connection openSimplex7 := by sorry Blocking issue: No formal model of jet bundles or Cartan connections in Mathlib.

Workaround (built 2026-06-26, docs/reviews/CARTAN_CONNECTION_FORMULA.md): reduce the jet-bundle Cartan connection to a finite Chevalley–Eilenberg Maurer–Cartan check — the 2-cochain μ from the Sidon crossing matrix satisfies d_CE μ + ½[μ,μ]_NR = 0 because Sidon support-disjointness makes the deformation operad forest-structured (μ_i ∘ₖ μ_j = 0 across disjoint supports), so no jet-bundle formalization is needed. Gates A (arithmetic) and B (structural review) passed; Gate C (build) is NOT done — needs the Nijenhuis–Richardson bracket defined in Lean (~30 lines) + the 1015-equation system discharged by dec_trivial. ⚠️ That doc asserts signature (1,6) / SO⁰(1,6) but justifies it from the Fisher–Rao metric — which is positive-definite (7,0). The (1,6) must come from the Kelvin/Rossby drift (§0), not the static metric; §0 resolves this before §3's holonomy containment can stand.

Upgrade to theorem

Definition. Let M be an (m)-dimensional manifold. The first jet bundle J^1(M) is the vector bundle whose fibre at p \in M consists of 1-jets of smooth functions:

[ J^1_p(M) = { j^1_p f \mid f \in C^\infty(M) }. ]

A Cartan connection on J^1(M) is a principal bundle connection on the (GL(m,\mathbb{R}))-bundle of 1-jets satisfying the Cartan structure equations.

Theorem statement:

Let \Delta_7 be the open 7-simplex with the Fisher–Rao metric. Then J^1(\Delta_7) admits a Cartan connection whose curvature is determined by the golden-ratio spectral gap \sigma - \tau.

Prerequisites:

• Formal definition of jet bundles (not in Mathlib)
• Formal definition of Cartan connections (not in Mathlib)
• Formal definition of the Fisher–Rao metric on \Delta_7
• Construction of the specific connection

Upgrade difficulty: 🟡 Medium via the 2026-06-26 workaround — the remaining step is Gate C (define the NR bracket + dec_trivial on the 1015-equation system). The abstract jet-bundle route stays 🔴, but it is no longer on the critical path.

---

4. Holonomy \mathrm{SO}^0(1,6)

File location: UnifiedCovariant.lean:227 Current status: theorem holonomy_is_SO_1_6 : has_SO_1_6_holonomy openSimplex7 := by sorry Blocking issue: Requires curvature computation and Berger's classification.

Upgrade to theorem

Berger's theorem. The holonomy group of a non-symmetric irreducible Riemannian manifold is one of: \mathrm{SO}(n), \mathrm{U}(n), \mathrm{SU}(n), \mathrm{Sp}(n), \mathrm{Sp}(n)\mathrm{Sp}(1), \mathrm{G}_2, or \mathrm{Spin}(7).

Theorem statement:

The holonomy group of the (\phi)-scaled Fisher–Rao metric on \Delta_7 is the identity component of the indefinite orthogonal group \mathrm{SO}^0(1,6).

Evidence. The tangent space T_p\Delta_7 \cong \mathbb{R}^7. The Fisher–Rao metric at a point p is g_{ij} = \delta_{ij}/p_i. The signature is (1,6) (one positive, six negative — the metric on the simplex is not positive-definite in the standard basis; the positive direction corresponds to the barycentric direction). The holonomy containment \mathrm{Hol}(g) \subseteq \mathrm{SO}(1,6) follows from metric compatibility. The full \mathrm{SO}^0(1,6) claim requires computing the curvature and showing the holonomy is irreducible and not a proper subgroup.

Prerequisites:

• Riemannian holonomy in Mathlib (partial — HolonomyGroup exists for Riemannian manifolds but not pseudo-Riemannian)
• Curvature computation for the Fisher–Rao metric on \Delta_7
• Berger's classification (not in Mathlib)

Upgrade difficulty: 🔴 Very hard — requires curvature computation and classification theorem.

---

Summary

Conjecture	Upgrade difficulty	Path
§0 Covariant semi-symmetry discriminator	🟡 ACTIVE	∇R / R·R on the drift-perturbed metric — no Mathlib blocker
Eigensolid convergence	✅ DONE	Sidon-orthogonality bypass (row-sum bound, dec_trivial)
Golden ℂℙ⁷ Kähler	🔴 Hard	Depends on ℂℙⁿ formalization in Mathlib
Cartan connection	🟡 workaround exists	Jet-bundle Cartan connection reduced to a finite Sidon-support MC/NR check (CARTAN_CONNECTION_FORMULA.md, 2026-06-26); needs NR bracket in Lean + Gate C
Holonomy SO⁰(1,6)	🔴 Very hard → re-scoped by §0	(1,6) is the Kelvin/Rossby wave-operator signature, not the static Fisher metric ((7,0), symmetric)

§0 is the active milestone: it names the covariant semi-symmetry hypothesis by direct computation and unblocks §4 by relocating the (1,6) signature to the drift-perturbed wave operator. §1 resolved; §§2–3 remain pending Mathlib infrastructure but are downstream of §0.