stable_zero_charge_ratio_eq_one
plain-language theorem explainer
In the neutral (zero log-charge) sector, any one-channel positive ratio that is a variational equilibrium must equal 1. Mass and generation-bridge arguments cite this to pin the ground rung. The proof reduces to the zero-charge equilibrium uniqueness lemma and reads off the single configuration entry.
Claim. Let $r > 0$. Package $r$ as the unique entry of a one-channel configuration. If that configuration is a variational equilibrium and has total log-charge zero, then $r = 1$.
background
The module extracts a B4-style dynamic claim from the variational ledger update: equilibria coincide with defect minimizers; in a zero-charge sector the unique equilibrium is the unity configuration; hence a stable one-channel ratio is forced to $r = 1$.
A configuration is a finite tuple of positive reals. The log-charge is the sum of entry logarithms, the conserved ledger charge. Equilibrium means the configuration is its own variational successor (equivalently, it uniquely minimizes total defect on its feasible set). The unity configuration has every entry equal to 1 and zero total defect.
The one-channel ratio packaging puts a single positive $r$ into a length-1 configuration. Upstream, zero-charge equilibrium uniqueness already says any equilibrium with vanishing log-charge has the same entries as the unity configuration.
proof idea
Apply the zero-charge equilibrium uniqueness theorem at $N = 1$ to the ratio configuration, using the given equilibrium and zero log-charge hypotheses. That yields equality of entry functions with the unity configuration on one channel. Evaluate both sides at the unique index $0$; simplifying the definitions of the ratio packaging and the unity configuration gives $r = 1$.
why it matters
This is the one-channel specialization that turns neutral-sector uniqueness into a concrete ratio constraint. Downstream, the generation-torsion bridge uses it: variational stability in the neutral sector forces the ground exponent to zero, via the identity that a compatible torsion has $\phi^{\tau_{\mathrm{first}}} = 1$ and hence $\tau_{\mathrm{first}} = 0$. In the broader forcing picture it supports the ground-state rung of the mass ladder (yardstick times $\phi$ powers), locking the neutral ground before generation structure is attached. It closes the module's third bullet: stable one-channel ratios in the neutral sector are forced to unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.