IsVariationalTrajectory
plain-language theorem explainer
A sequence of ledger configurations is variational when every consecutive pair obeys the successor update rule derived from global J-cost minimization. Researchers formalizing deterministic ledger evolution cite this definition to anchor charge conservation and defect monotonicity theorems. The definition is a direct universal quantification over ticks requiring the IsVariationalSuccessor predicate on each step.
Claim. Let $traj : ℕ → Configuration_N$ be a sequence of configurations. Then $traj$ is a variational trajectory if for every tick $t$, the pair $(traj(t), traj(t+1))$ satisfies the variational successor condition.
background
The Variational Dynamics module supplies the missing update rule for the Recognition Science ledger: each state evolves by constrained global minimization of total defect subject to the feasibility set and log-ratio conservation. A Trajectory is the type $ℕ → Configuration N$ of infinite sequences of N-entry configurations. Upstream modules establish the J-cost functional with unique minimum at unity (LawOfExistence), non-increasing defect along any admissible step (TimeEmergence), and uniqueness of minimizers from strict convexity (Determinism). The module doc states the update explicitly as state(t+1) = argmin_{s ∈ Feasible(state(t))} TotalDefect(s), with simultaneous non-local update across all entries.
proof idea
This is a one-line definition that directly wraps the universal quantification ∀ t, IsVariationalSuccessor (traj t) (traj (t + 1)). No tactics or lemmas are applied; the body is the predicate itself.
why it matters
This definition completes the equation-of-motion layer (F-008) for the ledger, enabling all downstream conservation and stability results. It is invoked as hypothesis in topological_charge_trajectory_conserved, total_charge_always_zero, trajectory_defect_monotone, and equilibrium_attractive. The parent theorems establish that topological charge is invariant along any such trajectory and that total defect decreases monotonically to equilibrium, directly supporting the eight-tick octave structure and D = 3 charge quantization in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.