IsVariationalSuccessor
plain-language theorem explainer
The variational successor of a configuration c is the feasible next state c' that achieves the global minimum total defect among all configurations reachable from c in one tick. Ledger dynamics work cites this as the precise equation of motion that turns the J-cost landscape into explicit time evolution. The definition is a direct conjunction of membership in the feasible set and the universal inequality on total_defect.
Claim. Let $c$ and $c'$ be configurations of $N$ positive real entries. Then $c'$ is a variational successor of $c$ if $c'$ belongs to the feasible set from $c$ and the total defect of $c'$ is less than or equal to the total defect of every other member of that feasible set.
background
The VariationalDynamics module supplies the missing update rule for the Recognition Science ledger after LawOfExistence, InitialCondition, TimeEmergence and Determinism have been established. A Configuration is the structure whose entries are positive reals; total_defect sums the individual defect values J(x) = (x + x^{-1})/2 - 1 over those entries. The feasible set from a current configuration collects those next configurations that preserve the total log-charge, i.e., the sum of log(entries_i) is invariant under the step.
proof idea
The definition is a direct encoding of the argmin condition: membership in Feasible current together with the inequality total_defect next ≤ total_defect c' for every other feasible c'. No tactics or lemmas are invoked; the body is the literal statement of the variational principle.
why it matters
This definition is invoked by every subsequent result on conservation and trajectories inside the module. It is used to define IsEquilibrium as a fixed point of the successor map and IsVariationalTrajectory as a sequence in which each consecutive pair satisfies the relation. Downstream theorems such as conservation_is_unconditional and the NoetherCharge and TopologicalCharge structures rely on it to obtain invariance of charges without extra symmetry hypotheses. It realizes the update principle stated in the module documentation and supplies the deterministic evolution rule required by the J-cost convexity and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.