zero_charge_equilibrium_is_unity
plain-language theorem explainer
In any positive dimension N, an equilibrium configuration whose conserved log-charge vanishes must have every entry equal to 1 (the unity configuration). Ground-state and stability arguments in the variational ledger cite this uniqueness. The proof reduces via the uniform-minimizer characterization of equilibria, then specializes the uniform sector to charge zero.
Claim. Let $N > 0$ and let $c$ be an $N$-entry configuration of positive real ratios. If $c$ is an equilibrium of the variational ledger update and its conserved log-charge vanishes, then every entry of $c$ equals $1$: $c$ coincides with the unity configuration.
background
The module extracts a B4-style dynamic statement from the variational ledger update: equilibria coincide with variational minimizers; in a zero-charge sector the unique equilibrium is the unity configuration; stability of a one-channel ratio then forces $r = 1$.
A Configuration N is an $N$-tuple of positive real ledger ratios. The unity configuration sets every entry to $1$ and has zero total $J$-defect. The conserved scalar log_charge labels the charge sector; IsEquilibrium means the configuration is a fixed point of the variational step.
Upstream, any equilibrium equals the uniform minimizer of its own charge sector: $c.entries = (\mathrm{uniform_config}, hN, (\log_charge, c)).entries$. The uniform configuration at charge $0$ is definitionally the unity configuration.
proof idea
Three-step calc chain. First apply equilibrium_entries_eq_uniform: equilibrium entries equal those of the uniform configuration at the same log-charge. Rewrite the charge hypothesis to replace that charge by $0$. Finish by funext and simp on the definitions of uniform_config and unity_config, which agree entrywise when the uniform value is $0$ in log-charge (i.e., ratio $1$).
why it matters
This is the middle bullet of the module's B4-style claim: zero-charge equilibria are uniquely the unity state. The sole downstream consumer is stable_zero_charge_ratio_eq_one, which packages a single positive ratio $r$ as a one-channel configuration and concludes $r = 1$ from equilibrium plus vanishing log-charge. That forces neutral stable observables onto the identity rung of the $\varphi$-ladder, consistent with the ground-state picture in which the zero-defect configuration is the unique variational rest point. It does not itself invoke T5–T8, but it supplies the dynamical uniqueness step those forcing results rely on when specializing to neutral sectors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.