trajectory_defect_monotone
plain-language theorem explainer
Along any trajectory obeying the variational update rule for the Recognition Science ledger, total defect is non-increasing at each tick. Researchers proving convergence of ledger states to equilibrium cite this monotonicity. The argument is a one-line term that applies the per-step defect reduction lemma to each consecutive pair using the trajectory hypothesis.
Claim. Let $N$ be a natural number. For a trajectory $traj: ℕ → Configuration(N)$ such that each consecutive pair satisfies the variational successor condition, the total defect satisfies $total_defect(traj(t+1)) ≤ total_defect(traj(t))$ for all $t ∈ ℕ$.
background
The VariationalDynamics module supplies the missing update rule for the ledger: each state evolves to the configuration of minimal total J-cost (defect) among those reachable in one tick while preserving the sum of log-ratios. Trajectory is the type of maps from ticks to configurations of fixed size N. IsVariationalTrajectory requires that every step is a variational successor, i.e., realizes the global argmin of total defect subject to the conservation law.
proof idea
The proof is a one-line term-mode wrapper. It constructs the function that, for arbitrary t, feeds the pair (traj t, traj (t+1)) and the witness (h t) directly into the lemma variational_step_reduces_defect.
why it matters
This supplies the monotonicity half of equilibrium_attractive, whose statement records that every variational trajectory has non-increasing defect bounded below by zero and therefore converges. It completes the ledger equation of motion inside the Recognition framework, connecting the constrained J-minimization update to the unique minimum of J at unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.