`harmonicFormsCert`

proved

show as: view math explainer →

module: IndisputableMonolith.Mathematics.HodgeHarmonicForms
domain: Mathematics
line: 189 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Mathematics.HodgeHarmonicForms on GitHub at line 189.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 186    (∀ cgf : CoarseGrainingFlow L, IsFlowStable L cgf cls) →
 187    ∃ cyc : JCostMinimalCycle L, cyc.cycle_class.z_charge = cls.z_charge
 188
 189theorem harmonicFormsCert : HarmonicFormsCert where
 190  critical_defined := trivial
 191  zero_charge_case := fun L cls h => harmonic_form_theorem_zero_charge L cls h
 192  decomposition_exists := fun L h cls => hodge_decomposition_exists L h cls
 193  hard_direction_budget := fun L cls h => hard_direction_via_defect_budget L cls h
 194
 195end HodgeHarmonicForms
 196end Mathematics
 197end IndisputableMonolith

papers checked against this theorem

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