Equilibrium
plain-language theorem explainer
Packages five recognition-equilibrium properties for a level field on a coupling graph: sigma conservation under pair resolution, exact variance drop by half the squared gap, nonincreasing variance, nonnegative total J-cost, and zero cost exactly at edgewise consensus. Cosmology and baryogenesis modules treat this as the descent package for Phase-7 forward dynamics. Pure structure definition; no proof body.
Claim. For a level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$ and a finite set $E$ of coupled pairs, recognition equilibrium asserts: resolving any distinct pair $(i,j)$ by sending both endpoints to their mean preserves the level sum; the level variance drops by exactly $(x_i-x_j)^2/2$ and never increases; the total recognition cost on $E$ is nonnegative; and that cost vanishes if and only if $x$ is constant on every edge of $E$.
background
Phase-7 forward dynamics evolves a recognition-level field $x$ on a coupling graph by posting, each tick, one forced recognition event: resolve a coupled pair $(i,j)$ by sending both endpoints to their arithmetic mean. That move is the sigma-neutral, $J$-minimal update (no free rate parameter). The module discharges the numerical checks from the cosmogenesis forward-dynamics script as theorems.
levelSum is the conserved sigma quantity $\sum_k x_k$. pairResolve replaces $x_i$ and $x_j$ by $(x_i+x_j)/2$ and leaves all other sites fixed. variance is the spread about the mean level, used as the Lyapunov function of the descent. Upstream, variance_nonincreasing is the immediate corollary of the exact drop law: after rewrite by the pair-resolve identity, nonnegativity of a square finishes the inequality. Total cost aggregates the nonnegative $J$-cost over edges; its vanishing locus is edgewise consensus.
The structure does not invent new dynamics: it bundles the conservation, Lyapunov, and ground-state facts already proved componentwise in the same module.
proof idea
No proof body: this is a structure ... : Prop definition. Each field is a named hypothesis-shaped clause whose mathematical content is already established by sibling theorems (pairResolve_levelSum, the exact variance identity, variance_nonincreasing, total-cost nonnegativity and the zero-cost-iff-consensus characterization). Instantiating the structure later is a matter of supplying those five proofs, not re-deriving them inside the structure itself.
why it matters
This is the Lean packaging of the central convergence claim of recognition equilibrium: forced pair resolution is a strict Lyapunov descent of level variance to the unique zero-cost ground state, which is exactly consensus on the coupling graph. Module doc ties it to Phase-7 cosmogenesis and notes that total edge demand is deliberately not claimed monotone; variance is the Lyapunov quantity.
Downstream, baryogenesis staging and J-cost baryogenesis treat equilibrium as the matter-antimatter balance locus ($J=0$), and use the package when arguing that a nonzero relic at sphaleron equilibrium forces a $B-L$ source, that gated wall slopes are generation-sensitive, and that hypercharge and lepton-Yukawa constraints are independent of earlier rows. Stellar assembly configurations also sit on the same equilibrium interface. In the broader RS chain this is the cosmological landing of the $J$-cost ground state (T5 uniqueness of $J$), not a new forcing step T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.