variational_step_exists
plain-language theorem explainer
For any N > 0 and ledger configuration c of N positive reals, a next configuration exists that lies in the feasible set from c and minimizes total defect among all such configurations. Researchers formalizing the Recognition Science ledger dynamics cite this to guarantee that the update rule is well-defined at every finite step. The proof constructs the minimizer explicitly as the uniform configuration that equalizes the conserved log-charge and verifies it meets the defect lower bound via direct calculation.
Claim. For every natural number $N > 0$ and every configuration $c$ of $N$ positive real entries, there exists a configuration $next$ such that $next$ belongs to the feasible set generated by $c$ and $next$ minimizes the total defect among all configurations in that set.
background
A Configuration of size N is a structure holding N positive real entries together with a proof that each entry is positive. The log-charge of c is the sum of log(entries_i), which the conservation law requires to be invariant under one-tick updates. Total defect is the sum of individual defects, where defect(x) equals J(x) = (x + x^{-1})/2 - 1 from the Law of Existence module. The feasible set from c consists of all configurations reachable in one tick while preserving this log-charge sum. The module VariationalDynamics supplies the update rule state(t+1) = argmin {TotalDefect(s) : s feasible from state(t)}, building directly on the non-negativity of defect and the strict convexity of J established upstream.
proof idea
The term-mode proof defines μ := log_charge c / N and instantiates next as constant_config μ. It applies constant_config_log_charge together with mul_div_cancel₀ to confirm that log_charge next equals log_charge c. Minimality follows by rewriting with constant_config_total_defect, invoking the upstream lemma total_defect_lower_bound on an arbitrary feasible c', and substituting the equality of log-charges to obtain the required inequality.
why it matters
This supplies the existence clause of the variational_dynamics_certificate theorem, which encodes the full equation of motion for the Recognition Science ledger. It completes the F-008 specification by showing that a total-defect minimizer is always available inside the feasible set. The result rests on the conservation law and the defect lower bound; once paired with the separate uniqueness theorem it yields deterministic evolution. It leaves open the large-N continuum limit that would recover classical field equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.