theorem
proved
term proof
conservation_is_protected
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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