module module

`IndisputableMonolith.Gravity.SevenGaps.CapShellBridge`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker module_import

declarations in this module (28)

abbrev ShellsUpTo L43
def boundedShellIndex L52
def boundedShellSig L56
def boundedToShell L65
def exactToBounded L71
def exactRelabelToBounded L84
def exactClassToCap L95
def shellToCap L104
theorem boundedToShell_congr L110
def capToShell L140
theorem shellToCap_boundedToShell L144
theorem boundedToShell_exactToBounded L165
theorem capToShell_shellToCap L181
theorem shellToCap_capToShell L189
def capShellEquiv L197
def autEquivToExact L207
theorem autCard_toExact L225
theorem mu_eq_exactMu_toExact L230
def shellAutCard L236
theorem shellAutCard_capToShell L240
theorem classMu_capToShell L263
def phaseModelAtCap L288
theorem classPhase_phaseModelAtCap L295
def capPhaseFamily L305
theorem sum_fin_eq_sum_range L312
theorem sum_shellsUpTo_eq_exactComplexityCutoff L329
theorem phasedZq_eq_exactComplexityCutoff L343
theorem capShellCompatibility L372