IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure

declarations in this module (56)

• structure BoundedComplex L81
• def emptyComplex L92
• abbrev CodeType L115
• def toCode L120
• def ofCode L125
• def codeEquiv L137
• instance instFintypeBoundedComplex L146
• theorem boundedComplex_card_pos L150
• structure Relabel L157
• def refl L171
• def symm L179
• def trans L193
• theorem refl_vEquiv L203
• theorem symm_vEquiv L205
• theorem symm_eEquiv L207
• theorem symm_tEquiv L209
• theorem trans_vEquiv L212
• theorem trans_eEquiv L215
• theorem trans_tEquiv L218
• def toEquivTriple L223
• theorem toEquivTriple_injective L229
• theorem ext L240
• def Equivalent L251
• def relabelSetoid L257
• abbrev TriangulationClass L266
• theorem triangulationClass_finite L270
• theorem classCount_le_labeledCount L276
• theorem labeledCount_eq_card L282
• abbrev Aut L290
• instance instFiniteAut L297
• theorem autCard_pos L301
• def mu L307
• theorem mu_pos L311
• theorem mu_le_one L318
• theorem mu_congr L348
• def Z L362
• theorem Z_norm_le_muSum L367
• theorem Z_norm_le_card L381
• theorem Z_relabel_invariant L400
• theorem summand_class_constant L415
• def unitaryWeight L427
• theorem unitaryWeight_norm L432
• theorem zRS_scoped_wellDefined L444
• def provedFamily L464
• theorem provedFamily_growthBase_derived L473
• theorem proved_count_le_structural_bound L479
• structure GapStatus L493
• def pathSumMeasureStatus L504
• theorem status_count_finite L514
• theorem status_quotient_finite L515
• theorem status_measure_defined L516
• theorem status_measure_positive L517
• theorem status_modulus_bound L518
• theorem status_relabel_invariance L519
• theorem status_continuum_open L521
• theorem status_substrate_measure_open L523