module module

`IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.ExactShellGaugeUV module_import

declarations in this module (29)

abbrev RelabelTriple L83
theorem relabelTriple_card L88
def act L102
def actRelabel L108
theorem exactComplex_ext L123
theorem sigma_relabel_ext L136
def relabelSigmaEquiv L166
instance instFiniteExactRelabel L178
def torsorEquiv L187
def orbitCard L209
theorem sum_card_relabel L213
theorem sum_card_relabel_eq_orbit L226
theorem orbitCard_mul_autCard L255
instance instFintypeExactQuotient L265
class is L270
theorem classMuOn_out L271
theorem fiber_card L283
theorem sum_orbitCard L296
theorem sum_classMuOn_eq_card_div_factorials L314
def cubeSig L345
theorem cube_sum_le_shellMass L353
theorem shellMass_lower L387
theorem shellMass_unbounded L430
theorem single_shell_re_lower_bound L450
theorem not_hasZRSRegulatorRemoval_zeroPhase L474
def OscillatoryRemovalOpen L509
structure RegulatorRemovalNoGoStatus L518
def regulatorRemovalNoGoStatus L531
theorem regulatorRemovalNoGoStatus_grounded L540