module module

`IndisputableMonolith.Mathematics.HodgeHarmonicForms`

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

used by (1)

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

IndisputableMonolith.Mathematics.HodgeHardDirection module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Mathematics.HodgeConjecture module_import

declarations in this module (13)

structure JCostGradient L44
def IsJCostCritical L53
theorem all_ledgers_are_jcost_critical L58
def IsGloballyMinimal L64
theorem globally_minimal_gives_cycle L68
theorem harmonic_form_theorem_zero_charge L91
theorem harmonic_form_theorem_minimal_ledger L105
structure HodgeDecomposition L121
theorem hodge_decomposition_exists L132
theorem hard_direction_via_defect_budget L153
theorem hard_direction_for_zero_limit_ledger L163
structure HarmonicFormsCert L175
theorem harmonicFormsCert L189