IsEquilibrium
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not assert existence of an equilibrium for every initial configuration.
- Does not give an explicit formula for the feasible set or the minimizer.
- Does not address stability under small perturbations of entries.
- Does not extend the definition to continuous-time limits or stochastic updates.
formal statement (Lean)
507def IsEquilibrium {N : ℕ} (c : Configuration N) : Prop :=
proof body
Definition body.
508 IsVariationalSuccessor c c
509
510/-- **Theorem (Equilibrium Characterization)**:
511 A configuration is at equilibrium iff it minimizes total defect
512 over its feasible set — iff it is the unique minimizer.
513
514 For log-charge = 0, this is the unity configuration (all entries = 1).
515 For general log-charge σ, this is the uniform configuration
516 (all entries = exp(σ/N)). -/