IsEquilibrium
plain-language theorem explainer
A configuration of N ledger entries is at equilibrium when it is a fixed point of the variational successor map. Ledger dynamics work cites this fixed-point condition to identify stationary states under global defect minimization. The definition is a one-line wrapper equating equilibrium to self-succession.
Claim. A configuration $c$ of $N$ positive real ledger entries is at equilibrium if $c$ is a variational successor of itself.
background
Module F-008 supplies the ledger update rule as state(t+1) equals the argmin of total defect over the feasible set reachable in one tick, with total log-charge conserved. Configuration is the structure whose entries are positive reals (Fin N to R with positivity). Defect of an entry x equals the J-cost J(x) = (x + x^{-1})/2 - 1, zero only at x=1. Upstream LawOfExistence establishes the unique minimum of J at unity; InitialCondition supplies the zero-defect starting state; TimeEmergence shows defect is non-increasing.
proof idea
One-line wrapper that applies IsVariationalSuccessor c c.
why it matters
This definition supplies the fixed-point notion used by equilibrium_iff_minimizer to equate equilibrium with global minimization of total defect over the feasible set. It anchors the variational_dynamics_certificate for F-008, which states the equation of motion as the constrained argmin. The construction connects directly to the J-minimum at unity from LawOfExistence and the conservation law that fixes the uniform configuration for nonzero log-charge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.