is_protected_observable

formal source

 141
 142/-- Physical laws are "protected" observables that are stable under error correction.
 143    An observable O is protected if it commutes with the correction protocol. -/
 144def is_protected_observable {X : Ω → ℝ} (O : Ω → ℝ) (C : CorrectionProtocol X) : Prop :=
 145  ∀ ω, O (C.correct ω) = O ω ∨ Jcost (X ω) > 0
 146
 147/-- **Theorem**: Conservation laws are protected observables.
 148    Quantities that are conserved in the J=0 sector remain stable. -/
 149theorem conservation_is_protected {X : Ω → ℝ} (O : Ω → ℝ) (C : CorrectionProtocol X)
 150    (hX_pos : ∀ ω, 0 < X ω)
 151    (h_conserved : ∀ ω₁ ω₂, Jcost (X ω₁) = 0 → Jcost (X ω₂) = 0 → O ω₁ = O ω₂) :
 152    is_protected_observable O C := by
 153  intro ω
 154  by_cases h : Jcost (X ω) = 0
 155  · left
 156    have h_correct := C.ground_fixed ω h
 157    rw [h_correct]
 158  · right
 159    have hnonneg : 0 ≤ Jcost (X ω) := Jcost_nonneg (hX_pos ω)
 160    exact lt_of_le_of_ne hnonneg (Ne.symm h)
 161
 162end Thermodynamics
 163end IndisputableMonolith