variational_dynamics_certificate
plain-language theorem explainer
The variational_dynamics_certificate states that for any positive integer N and any configuration c of N ledger entries, a variational successor always exists, total defect is non-increasing along every such successor, the unity configuration is an equilibrium, and total defect remains nonnegative for all configurations. Researchers formalizing the Recognition Science ledger update rule would cite this as the precise statement of the constrained global minimization dynamics. The proof is a direct term construction that packages four upstream le
Claim. For positive integer $N$ and configuration $c$ of $N$ positive real entries, there exists a next configuration minimizing total defect among all feasible successors of $c$, every such minimizer satisfies total defect at most that of $c$, the uniform configuration with all entries 1 is an equilibrium, and total defect is nonnegative for every configuration.
background
A Configuration N is a structure with N positive real entries representing ledger states. Total defect sums the individual J-costs, where J(x) = (x + x^{-1})/2 - 1 from LawOfExistence. IsVariationalSuccessor c next holds precisely when next lies in the feasible set (log-charge conserving) and achieves the global minimum total defect over that set. IsEquilibrium c means c is its own variational successor. The module sets the ledger evolution to state(t+1) = argmin TotalDefect(s) subject to feasibility from state(t), with the conservation law preserving sum log(x_i). Upstream, total_defect_nonneg shows nonnegativity by summing nonnegative J terms, and unity_config supplies the zero-defect reference state.
proof idea
The proof is a term-mode 4-tuple. The first entry applies variational_step_exists hN c to obtain existence. The second is a lambda applying variational_step_reduces_defect c next h to obtain defect reduction. The third applies unity_is_equilibrium hN. The fourth applies total_defect_nonneg c' to obtain the lower bound.
why it matters
This is the central certificate for F-008 Variational Dynamics, supplying the explicit equation of motion for the Recognition Science ledger as global J-cost minimization under log-charge conservation. It closes the gap left by LawOfExistence (convexity), InitialCondition (unity reference), and TimeEmergence (non-increase), turning the cost landscape into deterministic dynamics. The module documentation notes that this update is non-local because the minimizer depends on the entire configuration through the shared constraint. It directly supports the determinism and equilibrium properties listed in the F-008 description.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.