module module

`IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugePreflight`

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.MeasureSubstrateBlocker module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import

declarations in this module (34)

theorem equivalent_refl L96
theorem equivalent_symm L100
theorem equivalent_trans L105
instance instFiniteRelabel L112
def gaugeOrbitCard L122
def relabelingCount L126
def pairCount L133
theorem gaugeOrbitCard_pos L137
def torsorEquiv L147
theorem relabelingCount_eq_autCard L168
theorem pairCount_eq_orbitCard_mul_autCard L177
theorem pairCount_pos L188
theorem gaugeOrbitCard_congr L195
theorem autCard_congr L203
theorem pairCount_congr L210
theorem gaugeMassRep_congr L218
def orbitCardClass L226
theorem orbitCardClass_mk L229
def pairCountClass L233
theorem pairCountClass_mk L236
theorem pairCountClass_pos L239
def gaugeOrbitMass L247
theorem gaugeOrbitMass_eq_mu L254
theorem gaugeOrbitMass_mul_pairCount L268
theorem gaugeCountingMass_unique L281
instance instFintypeTriangulationClass L294
theorem labeledZ_eq_orbitWeighted_classSum L303
structure GaugePreflightStatus L352
def gaugePreflightStatus L361
theorem status_gauge_torsor L367
theorem status_measure_derived L369
theorem status_uniqueness L371
theorem status_counting_principle_open L375
theorem gaugePreflight_grounded L381