unity_is_equilibrium
plain-language theorem explainer
The unity configuration (all entries equal to 1) is an equilibrium under the ledger's constrained J-cost minimization update. A researcher modeling Recognition Science dynamics would cite this to anchor the zero-defect fixed point of the variational flow. The term-mode proof directly constructs the IsEquilibrium predicate by invoking self-feasibility of unity together with non-negativity of total defect on any other feasible successor.
Claim. For $N > 0$, let $c$ be the configuration with every entry equal to 1. Then $c$ is an equilibrium: it is a variational successor of itself, and for every feasible successor $c'$ the total defect of $c'$ satisfies $0$ ≤ total defect of $c'$.
background
The VariationalDynamics module supplies the missing update rule for the Recognition Science ledger: each step replaces the current state by the global argmin of total defect over the feasible set reachable in one tick. Total defect is the sum of individual defect terms, where defect(x) = J(x) and J(x) = ½(x + x⁻¹) − 1 attains its unique minimum at x = 1. The unity_config is the all-ones vector; upstream results from InitialCondition show that its total defect is exactly zero and that total defect is nonnegative for every configuration.
proof idea
The term proof constructs the IsEquilibrium predicate in two steps. First it applies self_feasible to confirm the unity configuration is a valid successor of itself. Second it rewrites the defect of unity to zero via unity_defect_zero and invokes total_defect_nonneg on an arbitrary feasible successor to obtain the required inequality.
why it matters
This theorem supplies the base equilibrium case required by the downstream variational_dynamics_certificate, which certifies the full equation of motion state(t+1) = argmin TotalDefect(s) over feasible s. It closes the loop from LawOfExistence (J minimum at unity) and InitialCondition (zero defect at unity) to the dynamics, and aligns with the J-uniqueness step of the forcing chain. The module doc-comment explicitly flags the zero log-charge case as the equilibrium of interest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.