GroundStateCompatibleTorsion
plain-language theorem explainer
A torsion schedule is ground-state compatible when the first generation, realized as a one-channel φ-power ratio configuration, is a neutral equilibrium of the variational dynamics: it is its own successor and carries zero log-charge. Mass and generation authors cite this predicate to pin the ground exponent at zero. It is a two-conjunct Prop definition, not a proved statement.
Claim. A map $\tau$ from generations to integers is ground-state compatible when the one-channel $\varphi$-power configuration built from $\tau$ on the first generation is an equilibrium of the variational dynamics and has vanishing total log-charge: $\mathrm{IsEquilibrium}(c_{\tau_1})$ and $\sum_i \log(c_{\tau_1,i}) = 0$.
background
The module derives the charged-generation torsion schedule ${0,11,17}$ from $D=3$ cube combinatorics (passive edges and faces), and certifies agreement with every other torsion representation in the codebase. The remaining premise is the structural coupling rule that assigns ground / passive-edge / face+edge modes to the three generations; uniqueness under that rule is proved, but the rule itself is not yet forced by the Recognition Composition Law alone.
A configuration is at equilibrium when it is its own variational successor (equivalently, the unique minimizer of total defect on its feasible set). The log-charge of a configuration is the sum of logarithms of its positive entries: the conserved ledger charge under tick evolution. Neutral sector means that charge is zero.
Here the first-generation torsion integer is realized as a one-channel $\varphi$-power ratio configuration via the local bridge map phiRatioConfig. Ground-state compatibility asks that this configuration sit at a neutral equilibrium.
proof idea
Definitional abbreviation only: the predicate is the conjunction of IsEquilibrium on the $\varphi$-ratio configuration of $\tau$ at the first generation, and equality of that configuration's log_charge to zero. No tactics, no lemmas discharged at this site.
why it matters
This predicate is the hypothesis of groundStateCompatible_forces_ground_zero, which proves that any ground-state-compatible torsion schedule must send the first generation to exponent $0$. That forces the geometric ground rung $\tau_1 = 0$ ("no geometric coupling") required by the cube-derived schedule ${0,11,17}$ and by agreement with Anchor and RecogSpec torsion tables.
In the broader mass ladder, the ground exponent zero is the baseline against which second- and third-generation torsion ($E_{\mathrm{passive}}=11$, $W_{\mathrm{endo}}=17$) lift masses on the $\varphi$-ladder. The definition therefore sits at the interface between variational neutrality (Foundation.VariationalDynamics) and the generation-torsion bridge that replaces hardcoded numerals by an explicit structural premise. It does not yet close the open coupling-from-RCL gap flagged in the module header; it only packages the neutral-equilibrium condition used to force $\tau_1=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.