variational_step_reduces_defect
plain-language theorem explainer
If next is a variational successor of configuration c, then the total defect of next is at most the total defect of c. Ledger-evolution researchers cite this to obtain monotonicity of defect along discrete trajectories. The proof is a one-line application of the minimality clause inside the successor definition to the current state itself.
Claim. Let $c$ and $next$ be configurations of $N$ ledger entries. If $next$ belongs to the feasible set generated by $c$ and minimizes total defect over that set, then the total defect of $next$ is at most the total defect of $c$.
background
A Configuration of $N$ entries is a tuple of positive reals whose total defect is the sum of individual $J$-costs, where $J(x) = (x + x^{-1})/2 - 1$. The module VariationalDynamics supplies the update rule that was missing from LawOfExistence, InitialCondition, TimeEmergence and Determinism: the next state is defined to be the global minimizer of total defect inside the feasible set that preserves log-charge. IsVariationalSuccessor encodes exactly this constrained minimization: next lies in Feasible c and satisfies the universal inequality total_defect next ≤ total_defect c' for every feasible c'.
proof idea
One-line wrapper that applies the second conjunct of the IsVariationalSuccessor hypothesis to the current configuration c, using the sibling lemma self_feasible c to witness that c itself belongs to the feasible set.
why it matters
This theorem is the key monotonicity step inside the F-008 certificate for variational dynamics. It is invoked directly by trajectory_defect_monotone to obtain non-increasing defect along any variational trajectory, by variational_dynamics_certificate to confirm the reduction property, and by variational_implies_recognition_step to embed the dynamics inside the earlier TimeEmergence framework. The result closes the gap between the abstract recognition step postulated in TimeEmergence and an explicit, globally consistent update rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.