module module

`IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.PathSumMeasure module_import
IndisputableMonolith.Gravity.SevenGaps.SimplicialClass module_import

declarations in this module (75)

def complexity L79
theorem relabel_nV_eq L84
theorem relabel_nE_eq L91
theorem relabel_nT_eq L98
theorem complexity_congr L106
structure ExactComplex L118
structure ExactRelabel L126
def refl L140
def symm L148
def trans L163
theorem trans_vEquiv L174
theorem trans_eEquiv L177
theorem trans_tEquiv L180
theorem symm_vEquiv L183
theorem symm_eEquiv L185
theorem symm_tEquiv L187
def toEquivTriple L192
theorem toEquivTriple_injective L198
theorem ext L209
def GlobalEquivalent L222
def exactSetoid L227
def exactCodeEquiv L237
instance instFintypeExactComplex L246
theorem exactComplex_card_eq L251
theorem exactComplex_card_le L260
abbrev ShellSig L291
abbrev sigV L296
abbrev sigE L298
abbrev sigT L300
theorem shellSig_card_le L303
abbrev ExactPathClass L319
instance instFiniteExactQuotient L322
instance instFintypeExactPathClass L327
def exactComplexity L334
theorem shell_index_unique L342
def toExact L351
theorem toExact_relax L359
theorem toExact_complexity L363
theorem exactPathClass_card_le L374
def isolatedVertices L409
def isolatedSig L414
def isolatedClass L421
instance instNonemptyExactPathClass L424
theorem exactPathClass_unbounded_support L430
abbrev ExactAut L438
instance instFiniteExactAut L445
theorem exactAutCard_pos L451
def exactMu L457
theorem exactMu_pos L461
theorem exactMu_le_one L468
theorem exactMu_congr L502
def classMuOn L509
def classMu L514
theorem classMu_pos L518
theorem classMu_le_one L523
def liftedPhase L531
def zRSUVShell L545
theorem norm_zRSUVShell_le L553
theorem norm_zRSUVShell_le_entropy L578
theorem log_le_linear L596
theorem exists_gaussian_domination L608
theorem pow_eq_exp_log L663
theorem summable_zRSUVShell L674
def Z_RS_uv L718
theorem zRSUVCutoff_tendsto L724
def zeroPhase L734
def shellMass L737
theorem shellMass_pos L742
theorem zRSUVShell_zeroPhase_eq L747
theorem zRSUVShell_zeroPhase_re_pos L759
theorem Z_RS_uv_zeroPhase_re_pos L768
def HasZRSRegulatorRemoval L796
structure ExactShellGaugeUVStatus L811
def exactShellGaugeUVStatus L831
theorem exactShellGaugeUVStatus_grounded L843