module module

`IndisputableMonolith.Gravity.SevenGaps.ZqShellBalanceBlocker`

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

def ShellAmplitudeVanishes L52
theorem one_shell_block L58
theorem oscillatoryTail_implies_shellAmplitudeVanishes L67
def EventuallyAgrees L81
theorem exactShellAmplitude_congr L86
theorem oscillatoryTail_of_eventuallyAgrees L95
theorem oscillatoryTail_congr_eventually L116
def EventuallyZeroPhase L128
theorem eventuallyZeroPhase_not_oscillatoryTail L134
def SupportedBelow L145
theorem merely L150
theorem supportedBelow_not_oscillatoryTail L151
def ShellConstant L164
theorem exactShellAmplitude_shellConstant L170
theorem norm_exactShellAmplitude_shellConstant L182
theorem one_lt_shellMass_of_two_le L191
theorem shellConstant_not_shellAmplitudeVanishes L207
theorem shellConstant_not_oscillatoryTail L222
theorem p24_shell_balance_blocker_certificate L236