module module

`IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttack`

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

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

IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase module_import
IndisputableMonolith.Gravity.SevenGaps.Gap2SignatureBlockerAttackAudit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker module_import
IndisputableMonolith.Gravity.SevenGaps.RegulatorRemovalNoGo module_import

declarations in this module (22)

def signatureFiber L55
def signatureMass L59
def burnsideMass L63
theorem burnsideMass_eq_pow L67
def sigEmbed L75
theorem signatureFiber_eq_map L83
theorem signatureMass_eq_burnside L98
theorem shellMass_eq_sum_signatureMass L107
def sigmaTick L118
theorem sigmaTick_is_ShellSigTick L122
theorem ShellSigTick_iff_sigmaTick L126
theorem exactShellAmplitude_signature_fiberwise L140
theorem cubeSig_components L182
theorem burnsideMass_two_two_two L186
theorem signatureMass_cube_two L193
theorem signatureMass_cube L200
theorem burnsideMass_cube_eq_pow L206
def SignatureMassCancellationStatement L228
theorem signatureFin8OscillatoryTailBlocker_iff_signatureMassCancellation L232
structure Gap2SignatureBlockerAttackStatus L245
def gap2SignatureBlockerAttackStatus L255
theorem gap2SignatureBlockerAttackStatus_flags L265