module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2KindRule`

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.Gravity.SevenGaps.Gap2LatticeKindRule module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.Analysis.RecognitionDualEntryEnrichment4D module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2PostingCostDerivation module_import

declarations in this module (24)

theorem pairCost_equivariant L103
def oneVertex L120
theorem pairCost_not_kindOnly L135
theorem pairCost_costSizeBlind L157
theorem kind_rule_fails_by_counting L171
theorem kind_rule_fails_by_incidence L178
theorem letter_cost_is_silent_on_the_state_space L196
theorem history_cost_is_silent_on_the_state_space L204
theorem countermodel_weight_classMass_ne_mu L216
def pinning_is_a_counting_normalization L227
def ChargesCountsOnly L241
theorem does L253
theorem chargesCountsOnly_perComplex_kindRates L254
theorem chargesCountsOnly_kindTotals_perComplex L271
def indexCost L291
theorem indexCost_inl L296
theorem indexCost_not_chargesCountsOnly L301
theorem chargesCountsOnly_excludes_incidence L324
theorem pairCost_chargesCountsOnly L350
theorem kindOnly_of_constant_rates L367
structure KindRuleIndex L380
def kindRuleIndex L403
theorem index_kind_rule_not_forced L413
theorem index_lattice_question_open L415