def definition def or abbrev

`IsFlowStable`

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

formal statement (Lean)

 216def IsFlowStable (L : DefectBoundedSubLedger) (cgf : CoarseGrainingFlow L)
 217    (cls : CoarseGrainingStableClass L) : Prop :=

Definition body.

 218  cls.z_charge ≤ flowLimit cgf
 219
 220/-- If a class is flow-stable and the flow converges to 0, the class has z_charge = 0. -/

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

defect_budget_theorem in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
flow_stable_at_zero in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
hodge_hard_direction_case_A in IndisputableMonolith.Mathematics.HodgeHardDirection decl_use
hard_direction_for_zero_limit_ledger in IndisputableMonolith.Mathematics.HodgeHarmonicForms decl_use
hard_direction_via_defect_budget in IndisputableMonolith.Mathematics.HodgeHarmonicForms decl_use
HarmonicFormsCert in IndisputableMonolith.Mathematics.HodgeHarmonicForms decl_use

Lean names referenced from this declaration's body.

has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
CoarseGrainingFlow in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
CoarseGrainingStableClass in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
DefectBoundedSubLedger in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
flowLimit in IndisputableMonolith.Mathematics.HodgeConjecture decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
L in IndisputableMonolith.Recognition decl_use
L in IndisputableMonolith.Recognition.Cycle3 decl_use