module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2GluingDerivation`

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

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

IndisputableMonolith.Gravity.SevenGaps.Gap2LabelErasure module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2LedgerGenerated module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2SizeBlindnessReach module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2GaugeVolume module_import

declarations in this module (181)

abbrev inlV L46
abbrev inrV L49
def dunion L52
theorem dunion_nV L71
theorem dunion_nE L74
theorem dunion_nT L77
def interleave L88
def gaugeVol L92
theorem gaugeVol_add L98
theorem gaugeVol_dunion L114
theorem pairCount_eq_gaugeVol L123
theorem interleave_pos L128
theorem gaugeVol_pos L136
def dust L154
theorem dust_nV L164
theorem dust_nE L165
theorem dust_nT L166
def autDustEquiv L171
theorem autCard_dust L188
theorem mu_dust L193
def dunionDustRelabel L199
theorem dunion_dust_equivalent L206
theorem unrestricted_gluing_multiplicativity_false L214
theorem mu_dust_union_off_by_binomial L226
theorem orbitCard_dunion_of_autMul L260
def sizeWeight L292
theorem sizeWeight_invariant L297
theorem classMass_sizeWeight L305
class mass L318
def GluesAt L319
theorem shuffle_of_gluesAt L331
instance carries L381
theorem two_mul_choose L382
theorem interleave_pt L399
theorem interleave_edge L403
theorem interleave_bqEdge L407
theorem interleave_bqTet L411
structure CarrierShuffle L418
theorem edgeWeight L444
theorem vertexRec L453
theorem dustRow L473
theorem bRec L492
theorem tetWeight L512
theorem cRec L520
theorem bouquetTetCol L545
theorem bouquetRow L566
theorem closedForm L601
theorem gibbs_of_unit_fugacities L646
def bouquet L683
theorem bouquet_nV L693
theorem bouquet_nE L694
theorem bouquet_nT L695
def cone L700
theorem cone_nV L710
theorem cone_nE L711
theorem cone_nT L712
theorem inrV_zero L715
theorem dunion_dust_edgeVerts L721
theorem dunion_dust_tetVerts L731
def dunionConeRelabel L742
theorem dunion_cone_equivalent L762
def autBouquetEquiv L769
theorem autCard_bouquet L792
theorem perm_fin_two_fixes L799
def autConeOneEquiv L809
theorem autCard_cone_one L836
theorem stab_card L844
def autConeEquiv L871
theorem autCard_cone L894
theorem autMul_dust_bouquet L911
theorem orbitCard_dust_bouquet L919
theorem autMul_dust_one_bouquet L930
theorem orbitCard_dust_one_bouquet L940
theorem perm_fix_of_fixes_others L963
theorem stab1_card L971
theorem dunion_edgeVerts_inl L996
theorem dunion_edgeVerts_inr L1002
theorem dunion_tetVerts_inl L1008
theorem dunion_tetVerts_inr L1014
def edge L1021

… and 101 more