module module

`IndisputableMonolith.Mathematics.HodgeConjecture`

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 (2)

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

IndisputableMonolith.Mathematics.HodgeHardDirection module_import
IndisputableMonolith.Mathematics.HodgeHarmonicForms module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Mathematics.HodgeConjectureStructure module_import

declarations in this module (19)

structure DefectBoundedSubLedger L56
structure CohomologyClass L68
structure CoarseGrainingStableClass L78
structure JCostMinimalCycle L84
theorem j_cost_minimal_is_cgstable L100
theorem j_cost_minimal_is_cgstable' L119
def RSHodgeConjecture L145
theorem hodge_implies_zero_charge L154
theorem rs_pp_condition L167
theorem sub_ledger_exists L172
structure CoarseGrainingFlow L188
def trivialFlow L199
def flowLimit L206
theorem flowLimit_nonneg L211
def IsFlowStable L216
theorem flow_stable_at_zero L221
theorem defect_budget_theorem L229
structure HodgeCert L260
theorem hodgeCert L272