full_defect_monotone
plain-language theorem explainer
Total defect (ledger entropy) is non-increasing along any variational trajectory of the full N-entry configuration. Thermodynamic arguments in RS cite this as the second-law statement for the complete system before observer coarse-graining. The proof is a one-line re-export of the variational-dynamics monotone-defect theorem.
Claim. For every $N\in\mathbb{N}$, every trajectory $t\mapsto c_t$ of $N$-entry ledger configurations that obeys the variational successor rule at each tick, and every tick $t$, the total defect satisfies $\sum_i J((c_{t+1})_i)\le\sum_i J((c_t)_i)$.
background
In the RS ledger, each entry $x>0$ carries a defect equal to the J-cost $J(x)=(x+x^{-1})/2-1$. The total defect of an $N$-entry configuration is the sum of these costs; InitialCondition identifies entropy with that sum, so zero defect is the unique minimum-entropy (unity) state.
A trajectory is a tick-indexed sequence of configurations. It is variational when each successive pair satisfies the variational update rule from VariationalDynamics: each step is a defect-reducing successor under the conserved log-charge constraint.
This module (F-011) builds temperature and the canonical ensemble from that structure. The full-ledger monotone statement is the unrestricted second-law input before an observer with resolution $K<N$ treats the unseen entries as a heat bath.
proof idea
One-line wrapper: the claim is definitionally the same as trajectory_defect_monotone from VariationalDynamics, which itself applies variational_step_reduces_defect at each tick via the IsVariationalTrajectory hypothesis. No extra algebra is done here.
why it matters
F-011 needs a clean second-law fact for the complete ledger before introducing observer-relative entropy and temperature $T=\partial E/\partial S$. Entropy is total defect and energy is log-charge; monotone total defect along variational dynamics is the ledger form of irreversible relaxation toward unity.
The parent result is the variational-dynamics theorem that each variational step reduces defect. This declaration re-exports that fact into the thermodynamics namespace so temperature, equilibrium entropy, and the canonical-ensemble construction can cite a local name. No downstream consumers are wired yet in the graph; the intended landing is the observer/heat-bath development in this same module.
Framework landmarks: J-uniqueness (T5) fixes the cost whose sum is entropy; variational minimization supplies the dynamics. The statement does not yet force the eight-tick octave or $D=3$; it is pure ledger thermodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.