recognitionEquilibrium
plain-language theorem explainer
For any finite level field and any coupling graph, forced pair-resolution satisfies the full recognition-equilibrium package: sigma conservation, exact variance drop as a Lyapunov law, nonnegative total J-cost, and zero cost iff edgewise consensus. Cosmologists and RS auditors cite this as the closed-system convergence certificate for Phase-7 forward dynamics. The proof is pure structure assembly wiring five already-proved component lemmas into the Equilibrium record.
Claim. For every $n\in\mathbb{N}$, every level field $x:\{0,\ldots,n-1\}\to\mathbb{R}$, and every finite coupling set $E$, pair-resolution on $x$ satisfies: resolving any distinct pair $(i,j)$ preserves the total level sum; level variance drops by exactly $(x_i-x_j)^2/2$ and never increases; total recognition cost over $E$ is nonnegative; and that cost vanishes if and only if $x$ is constant on every edge of $E$.
background
The module discharges the central convergence facts of the Phase-7 forward dynamics. A recognition level field $x$ lives on $n$ regions; each tick resolves one coupled pair $(i,j)$ by sending both endpoints to their mean (the unique sigma-preserving, $J$-minimal move). Region ratios are forced as $\phi^{x_i-x_j}$.
The structure packages five properties: sigma conservation under pair resolution; exact variance decrement $(x_i-x_j)^2/2$ (so variance is a strict Lyapunov function until consensus); the non-increase corollary; nonnegativity of total edge cost built from the recognition $J$-cost; and the characterization that zero total cost is exactly graph consensus.
Upstream lemmas already prove each field: pair resolution leaves the level sum unchanged; variance drops by the exact law-given amount; total cost is nonnegative and vanishes iff every coupled pair is equal. $J$-cost is reused from RefineTrigger; $\phi$ from Constants.
proof idea
Term-mode structure construction. Each field of the equilibrium package is filled by the matching named lemma:
- sigma conservation from the level-sum invariance of pair resolution;
- exact variance drop from the pair-resolve variance identity;
- variance non-increase from its immediate corollary;
- cost nonnegativity from the total-cost nonnegativity theorem;
- ground-state characterization from the total-cost zero-iff-consensus theorem.
No new algebra is performed; the declaration only assembles prior results so they hold for arbitrary $x$ and arbitrary edge sets.
why it matters
This is the closed-system convergence certificate for Recognition equilibrium in Phase-7 cosmogenesis. The module states that closed descent relaxes any connected world to consensus (variance is a strict Lyapunov function), so a forced open input is needed to keep structure alive; conjugate births at the horizon supply that input while preserving sigma.
It closes the §1–§4 descent chain (pair resolve, variance Lyapunov, total-cost ground state) and underwrites later birth-conservation arguments that keep sigma $=0$ through driven expansion. In the broader RS framework this is the dynamical content of recognition-cost minimization toward the $J$-ground state, complementary to T5 $J$-uniqueness and the eight-tick octave (T7) cadence that posts the cosmogenesis ledger.
No Lean dependents yet; the theorem is the module's public packaging result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.