pith. machine review for the scientific record. sign in
theorem proved term proof

flow_stable_at_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 221theorem flow_stable_at_zero (L : DefectBoundedSubLedger) (cgf : CoarseGrainingFlow L)
 222    (cls : CoarseGrainingStableClass L) (hstable : IsFlowStable L cgf cls)
 223    (hlimit : flowLimit cgf = 0) : cls.z_charge = 0 := by

proof body

Term-mode proof.

 224  have hle : cls.z_charge ≤ 0 := hlimit ▸ hstable
 225  exact le_antisymm hle cls.symmetric
 226
 227/-- **Defect Budget Theorem**: A class that is stable under ALL coarse-graining flows
 228    (including those with limit 0) must have z_charge = 0. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (17)

Lean names referenced from this declaration's body.