correlation_is_permanent
plain-language theorem explainer
On any variational trajectory, total ledger defect is nonincreasing after a fixed measurement time: every later configuration has defect at most that of the measured state. Anyone formalizing RS decoherence or the variational-to-measurement bridge cites this permanence of observer–system correlation. The proof is induction on the time lag, chaining one-step defect monotonicity at each successor.
Claim. Let $N\in\mathbb{N}$ and let $\gamma$ be a variational trajectory of $N$-entry ledger configurations. For any measurement time $t_m$ and any future time $t_f\ge t_m$, the total defect satisfies $\mathrm{total\,defect}(\gamma(t_f))\le\mathrm{total\,defect}(\gamma(t_m))$. In particular, no later variational step can restore a higher-defect uncorrelated state.
background
Module F-009 (Measurement Mechanism) supplies the missing mechanism behind the claim that quantum randomness is projection through finite resolution. Observers are subsystems of the ledger (not external agents): they see only $K$ of $N$ entries. A measurement is a variational step that couples observer and system entries; the outcome is fixed by the full configuration, while the observer's partial view underdetermines it.
Total defect (from InitialCondition) aggregates J-cost imbalance across all ledger entries. Variational trajectories are those generated by the global variational update; along them, defect is monotone nonincreasing one step at a time. The measurement event creates observer–system correlation precisely by that update.
Permanence is the multi-step reading of the same monotonicity: if the post-measurement state has defect $d$, every future state has defect $\le d$. Returning to an uncorrelated higher-defect state would violate the monotone bound. The module doc frames this as decoherence: the measurement record is permanent.
proof idea
Introduce the future time and the inequality $t_m\le t_f$. Decompose $t_f=t_m+d$ via Nat.exists_eq_add_of_le, then induct on the lag $d$.
Zero lag: both sides equal; simp closes.
Successor: rewrite $t_m+d.succ$ as $(t_m+d)+1$ with Nat.add_assoc. Apply the one-step lemma trajectory_defect_monotone (under IsVariationalTrajectory, defect at the next tick is $\le$ defect at the current tick). Chain the inductive hypothesis to push the bound back to $t_m$. The calc block is a pure telescoping inequality; no new analytic content beyond one-step monotonicity and arithmetic.
why it matters
This is the formal content of decoherence in the RS ledger picture: once a variational measurement couples observer and system, the correlation cannot be undone because defect only falls. Downstream it is wired into the Unified Forcing Chain structure Variational_To_Measurement_Bridge, whose doc lists "defect monotonicity makes that correlation permanent" among the subsystem/observer facts that turn the variational layer into a measurement mechanism. The witnessing theorem variational_to_measurement_bridge_holds packages this permanence with outcome determination, partial-view underdetermination, and J-cost weighting.
In the module it sits between outcome determination and the argument that subsystem information is insufficient to predict the outcome. Together with the later quadratic-near-equilibrium J-cost expansion (Born-rule weight $\approx$ Gaussian), it closes the measurement story without external collapse postulates. It does not itself force $\varphi$, the eight-tick octave, or $D=3$; those live earlier in the T0–T8 chain. Its job is local: lock the measurement record once the variational step has fired.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.