IsEquilibrium
plain-language theorem explainer
Equilibrium configurations are those fixed under the variational successor map of the ledger. Researchers deriving the ledger's discrete-time evolution would cite this definition when proving that fixed points coincide with global defect minimizers. The definition is a direct abbreviation that equates equilibrium to self-successorship in the feasible set.
Claim. A configuration $c$ of $N$ positive real ledger entries is an equilibrium if it is a variational successor of itself, i.e., $c$ minimizes total defect over the feasible set reachable from $c$.
background
The VariationalDynamics module supplies the update rule for the Recognition Science ledger: each step replaces the current state by the global argmin of total defect over configurations feasible from it. The feasible set respects conservation of total log-charge, which is invariant because $J(x)=J(1/x)$. Configuration $N$ is the structure of $N$ positive real entries introduced in InitialCondition; defect is the sum of individual $J$-costs with $J$ the function from LawOfExistence that attains its unique minimum at unity.
proof idea
The declaration is a definition. It sets IsEquilibrium $c$ to hold precisely when IsVariationalSuccessor $c$ $c$.
why it matters
This definition is invoked directly by the equilibrium characterization theorem, which proves equivalence to being the unique minimizer of total defect, and by the variational dynamics certificate that establishes existence of successors together with non-increasing defect. It realizes the constrained global $J$-cost minimization that supplies the ledger's equation of motion and completes the F-008 development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.