groundStateCompatible_forces_ground_zero
plain-language theorem explainer
Variational stability of first-generation torsion, realized as a neutral one-channel φ-power ratio, forces that ground exponent to vanish. Anyone pinning the charged-generation schedule {0, 11, 17} from cube geometry cites this to lock the ground rung at zero. The proof feeds the compatibility data into the neutral-sector unity theorem for stable ratios, then uses uniqueness of the integer n with φ^n = 1.
Claim. Let $\tau$ assign an integer torsion to each fermion generation. If the first-generation value is ground-state compatible—i.e., the one-channel configuration with ratio $\varphi^{\tau(\mathrm{first})}$ is a variational equilibrium and has vanishing log-charge—then $\tau(\mathrm{first})=0$.
background
The Generation Torsion Bridge derives charged-generation torsion from $D=3$ cube combinatorics alone: ground generation has no geometric coupling ($\tau=0$), the second couples to passive edges ($E_{\mathrm{passive}}=11$), and the third adds faces ($W_{\mathrm{endo}}=17$). The module certifies agreement with every other torsion representation and uniqueness under an explicit structural predicate, while recording that the coupling rule itself remains a premise until derived from the Recognition Composition Law.
Ground-state compatibility packages two conditions on the first generation: the $\varphi$-power ratio configuration is an equilibrium of the variational dynamics, and its log-charge is zero (neutral sector). Upstream, stable one-channel ratios in the neutral sector are forced to unity: any $r>0$ that is an equilibrium configuration with vanishing log-charge satisfies $r=1$.
Here $\varphi$ is the self-similar fixed point forced by J-uniqueness (T5–T6). Integer powers of $\varphi$ equal 1 only at exponent zero, which converts ratio-unity into a vanishing ground exponent.
proof idea
Destructure the compatibility hypothesis into an equilibrium witness and a zero log-charge witness. Instantiate the upstream neutral-sector theorem stable_zero_charge_ratio_eq_one at the positive real $\varphi^{\tau(\mathrm{first})}$ (positivity from $\varphi>0$), obtaining $\varphi^{\tau(\mathrm{first})}=1$. Apply the characterization that $\varphi^n=1$ for $n\in\mathbb{Z}$ if and only if $n=0$, and conclude $\tau(\mathrm{first})=0$. Term-mode proof: one unpacking step, one upstream application, one iff elimination.
why it matters
This pins the ground rung of the torsion schedule at zero, matching the geometric assignment "Gen 1: no coupling" in the cube derivation chain that produces ${0,11,17}$. The module's remaining premise is that cube-admissible torsion encodes a structural coupling rule not yet forced by the cost functional alone; this lemma discharges the variational half of the ground-state clause of that premise.
No downstream consumers are wired yet (used_by is empty), so the result is presently a leaf. It is the natural interface between ground-state dynamics and the mass/generation ladder (yardstick $\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Framework landmarks in play: $\varphi$ as the T6 fixed point, and the $D=3$ cube arithmetic that forces the higher torsions once the ground is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.