module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume`

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

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

IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LabeledWeightBridge module_import
IndisputableMonolith.Gravity.SevenGaps.GaugeCountingInevitableReasons module_import
IndisputableMonolith.Gravity.SevenGaps.InsertionAsymmetryInevitableReasons module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.MeasureSubstrateBlocker module_import

declarations in this module (62)

theorem size_v L138
theorem size_e L142
theorem size_t L146
abbrev SectorGroup L154
def push L159
def pushRel L170
theorem equivalent_push L178
abbrev PairSpace L189
def pairSpaceEquiv L193
theorem finCongr_self L201
def toSector L207
def ofSector L213
theorem toSector_ofSector L216
theorem target_eq_push L225
theorem ofSector_toSector L264
def sectorEquiv L286
theorem card_sectorGroup L295
theorem pairCount_eq_factorials L304
theorem pairCount_congr_sizes L312
theorem orbitCard_mul_autCard L319
def labelDensity L337
theorem labelDensity_eq_mu L343
class weight L351
theorem gaugeCounting_iff_labelIndifference L357
theorem gaugeVolume_is_size_data L376
def classMass L393
theorem equivalent_out L397
theorem fiber_card L402
theorem classMass_of_invariant L417
def gibbsWeight L441
theorem gibbsWeight_invariant L445
theorem gaugeVolume_pos L451
theorem gibbs_induces_measure L460
theorem invariant_weight_gives_measure_iff L479
theorem measure_is_uniform_count_over_gauge_volume L513
theorem sector_ratio_is_orbit_ratio L539
theorem uniformLabeled_eq_mu_times_gaugeVolume L575
def fugacityWeight L607
theorem fugacityWeight_invariant L615
theorem gibbsWeight_eq_fugacity_one L622
theorem classMass_fugacity_mk L627
theorem mu_pos L638
theorem gaugeCounting_iff_fugacity_one L649
theorem fugacity_absorbs_into_action L669
structure GluingLaw L710
theorem gluingLaw_forces_inverse_factorial L719
theorem gibbsWeight_factorizes L739
theorem gluingLaw_gives_gibbsWeight L752
theorem gluingLaw_gives_gaugeCounting L763
theorem inverseFactorial_gluingLaw L775
structure GaugeVolumeStatus L799
def gaugeVolumeStatus L828
theorem status_group_order L839
theorem status_size_only L840
theorem status_label_density L841
theorem status_premise_named L842
theorem status_indifference_undershoots L844
theorem status_absorbable L846
theorem status_gluing L847
theorem status_gibbs_unique L848
theorem status_cost_route_open L850
theorem gaugeVolume_grounded L853