`conservation_is_protected`

proved

show as: view math explainer →

module: IndisputableMonolith.Thermodynamics.ErrorCorrection
domain: Thermodynamics
line: 149 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Thermodynamics.ErrorCorrection on GitHub at line 149.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.