conservation_is_protected
plain-language theorem explainer
The theorem shows that observables constant on the zero J-cost sector remain stable under any correction protocol. Thermodynamic modelers in Recognition Science cite it when confirming fault tolerance for conserved quantities. The proof performs case analysis on whether Jcost vanishes at a state, applying the ground-fixed property of the protocol or non-negativity of Jcost.
Claim. Let $X : Ω → ℝ$ satisfy $X(ω) > 0$ for all $ω$, and let $O : Ω → ℝ$ be constant on pairs of states with zero J-cost. For any correction protocol $C$ on $X$, the observable $O$ is protected by $C$.
background
The module develops the error-correction viewpoint of RS thermodynamics. Physical laws remain stable because ledger dynamics implements fault tolerance. Recognition defects are deviations from the J=0 ground state; defect energy is the J-cost; the error syndrome is the detectable signature of a defect; correction dynamics return the system to equilibrium. The 8-tick cycle supplies the error-correction period and the φ-ladder supplies code distance. Upstream, Jcost_nonneg states that J(x) ≥ 0 for x > 0 by the AM-GM inequality, rewritten as (x-1)^2/(2x) ≥ 0. CorrectionProtocol is the structure whose fields are a correction map, cost-decreasing, and ground_fixed: Jcost(X ω) = 0 implies correct ω = ω.
proof idea
The proof introduces an arbitrary state ω and splits on whether Jcost(X ω) = 0. In the zero case the ground_fixed field of C yields correct ω = ω. In the complementary case Jcost_nonneg applied to the positivity hypothesis on X gives 0 ≤ Jcost(X ω), hence strict positivity by the case assumption. The conservation hypothesis on O is unused.
why it matters
The result places conservation laws inside the protected-observable class of the error-correction framework. It supports the claim that ledger dynamics supplies fault tolerance for physical laws and connects to the eight-tick cycle together with the φ-ladder code distance. It closes one step toward showing that conserved quantities are stable under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.