module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerCohomology`

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.Gravity.SevenGaps.Gap2IncidenceParity module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerCohomologyHostileProbe module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2LetterCostDichotomy module_import

declarations in this module (53)

def NaturalPotential L82
def historyOfPotential L90
def IsLedgerCoboundary L96
def IsCountLinear L101
def dnV L105
def dnE L106
def dnT L107
theorem dnV_kindRates L109
theorem dnE_kindRates L110
theorem dnT_kindRates L111
theorem dnV_countLinear L113
theorem dnE_countLinear L114
theorem dnT_countLinear L115
theorem dnV_equivariant L117
theorem dnE_equivariant L118
theorem dnT_equivariant L119
theorem historyCost_dnV L122
theorem historyCost_dnE L126
theorem historyCost_dnT L130
def IncidenceLocal L140
def incidenceLocalCost L149
theorem incidenceLocalCost_is L156
theorem historyCost_incidenceLocal L163
theorem kindRateCost_incidenceLocal L206
theorem incidenceCost_incidenceLocal L211
theorem incidenceLocalCost_equivariant L216
theorem incidenceLocal_history_countLinear_of_nV_le_one L232
theorem properFeature_invisible_at_nV_le_one L241
theorem incidenceCost_not_coboundary L250
theorem incidenceCost_history_not_a_function_of_counts L259
theorem incidenceCost_not_countLinear L268
theorem incidence_is_genuine_H1_class L281
theorem a17_escape_history_at_dust L301
theorem a17_escape_not_coboundary L305
theorem a17_escape_is_count_combination L312
theorem a17_escape_census_history L326
theorem count_span_rank_three L336
theorem count_differentials_independent L350
def measuredH1Dim L361
def measuredCountSpanDim L367
theorem measured_H1_cap1 L373
theorem measured_H1_cap2 L374
theorem measured_H1_cap3 L375
theorem measured_count_cap1 L376
theorem measured_count_cap2 L377
theorem measured_count_cap3 L378
theorem measured_H1_exceeds_count_at_cap2 L380
theorem measured_H1_exceeds_count_at_cap3 L383
theorem measured_H1_equals_count_at_cap1 L386
theorem centeredIncidence_is_coboundary L391
structure LedgerCohomologyVerdict L402
def ledgerCohomologyVerdict L422
theorem index_flag_unmoved L435