CorrectionProtocol
plain-language theorem explainer
CorrectionProtocol equips a state function X with a map that never raises J-cost and fixes all zero-cost states. RS thermodynamics researchers cite it to formalize fault tolerance and protected observables. It is introduced as a bare structure whose two fields directly encode the reduction and invariance conditions.
Claim. A correction protocol for $X : Ω → ℝ$ is a map correct : Ω → Ω such that $J(X(correct(ω))) ≤ J(X(ω))$ for every state ω and correct(ω) = ω whenever $J(X(ω)) = 0$, where $J$ is the J-cost function.
background
J-cost quantifies deviation from the ground state J = 0; upstream ObserverForcing.cost defines it as the cost of any recognition event while MultiplicativeRecognizerL4.cost derives it from comparator ratios. The module frames RS thermodynamics as error correction on the ledger, treating defects as stabilizer violations and the 8-tick cycle as the correction period. MODULE_DOC states that physical laws remain stable because ledger dynamics implements fault tolerance, with the φ-ladder supplying code distance.
proof idea
The declaration is a structure definition. Its two fields directly assert cost non-increase and ground-state fixed-point behavior; no lemmas or tactics are invoked.
why it matters
CorrectionProtocol supplies the basic object for the error-correction viewpoint. It is instantiated in is_complete_correction, is_fault_tolerant, and is_protected_observable; the last feeds conservation_is_protected, which asserts that conserved quantities remain stable under correction. The module doc-comment links the structure to the eight-tick octave (T7) and the φ-ladder code distance, closing the scaffolding between recognition defects and thermodynamic stability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.