equilibrium_attractive
plain-language theorem explainer
Variational trajectories of the Recognition Science ledger have non-increasing total defect bounded below by zero, so the defect sequence converges. Researchers formalizing ledger stability and deterministic evolution would cite this result. The proof is a direct term pairing of the monotonicity lemma with pointwise non-negativity of defect.
Claim. Let $N$ be a natural number and let traj be a sequence of $N$-entry configurations such that each successive pair satisfies the variational successor condition. Then for every time $t$ the total defect of traj$(t+1)$ is at most the total defect of traj$(t)$, and the total defect of traj$(t)$ is nonnegative.
background
In this module a Trajectory is a function from natural numbers to configurations of fixed size $N$. IsVariationalTrajectory requires that each step obeys the constrained global J-cost minimization update rule derived from the ledger's conservation of total log-charge. The total_defect of a configuration is the sum of individual defects, where each defect is given by the J-cost $J(x) = ½(x + x^{-1}) - 1$ from the LawOfExistence module. Upstream, total_defect_nonneg proves non-negativity by summing the non-negativity of each term, and trajectory_defect_monotone establishes monotonicity along any variational step.
proof idea
The proof is a term-mode construction that applies the upstream lemma trajectory_defect_monotone directly to the given trajectory and hypothesis, then pairs the result with the pointwise application of total_defect_nonneg.
why it matters
This theorem shows that every variational trajectory produces a monotone decreasing defect sequence bounded below by zero and therefore convergent, confirming the attractiveness of equilibrium under the ledger's update rule. It fills the gap between the existence of the variational dynamics (from LawOfExistence and InitialCondition) and the deterministic evolution theorem, placing the result inside the Recognition Science forcing chain that drives configurations toward the zero-defect state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.