equilibrium_iff_minimizer
plain-language theorem explainer
A configuration reaches equilibrium precisely when it achieves the global minimum of total defect among all configurations that conserve the same total log-charge. Workers on Recognition Science ledger dynamics cite this to justify the variational update rule as selecting equilibria. The proof is a direct biconditional via the definition of equilibrium as self-successor together with reflexivity of the feasible set.
Claim. A configuration $c$ is an equilibrium if and only if, for every configuration $c'$ that preserves the total log-charge of $c$, the total defect of $c$ is at most the total defect of $c'$. Total defect is the sum of individual $J$-costs over the entries, and the feasible set consists of all positive configurations with the same total log-charge.
background
The module formalizes the ledger update rule as the global argmin of total defect over the feasible set. A Configuration is a structure of $N$ positive real entries. Total defect sums the individual $J$-costs, where $J(x) = (x + x^{-1})/2 - 1$ from LawOfExistence. Feasible $c$ is the set of all configurations $c'$ with the same total log-charge as $c$. IsEquilibrium $c$ holds when $c$ is its own variational successor, i.e., the minimizer of total defect inside Feasible $c$. The module states: the ledger evolves by constrained global $J$-cost minimization, with conservation of total log-ratio following from $J$-symmetry.
proof idea
The term proof applies constructor to split the biconditional. Forward: the equilibrium assumption directly supplies the minimizer property. Reverse: the given minimizer property is paired with the reflexivity fact that the current configuration lies in its own feasible set.
why it matters
This equivalence justifies the global minimization principle that defines the ledger's equation of motion. It rests on prior convexity and uniqueness results from Determinism and LawOfExistence, and on the conservation law from TimeEmergence. In the framework it supports the T5 $J$-uniqueness and the eight-tick octave by ensuring the update lands on the unique fixed point of the phi-ladder. No downstream uses are recorded, so the result closes the local definition of equilibrium.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.