IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseTailBlocker

declarations in this module (22)

• theorem shellSig_zero_eq L54
• theorem exactComplex_zero_eq L60
• theorem exactPathClass_zero_eq L68
• theorem exactPathClass_zero_subsingleton L80
• theorem finset_univ_exactPathClass_zero L83
• theorem tickFiberMass_shell_zero L91
• theorem exactPathClass_zero_subsingleton_or_the_precise_finite_head_fact L103
• lemma fin8_add_one_ne L116
• theorem no_tickFiberMassBalanced L126
• theorem exactShellAmplitude_eq_zero_of_massBalanced_at L145
• theorem sum_amp_eq_zero_of_amps_zero L161
• theorem tickFiberMassBalanced_implies_exactShellTailCancellation L171
• theorem tickFiberMassBalanced_implies_oscillatoryTail L186
• theorem exactShellTailCancellation_of_identically_zero_amplitudes L201
• def EventuallyTickFiberMassBalanced L217
• theorem eventuallyTickFiberMassBalanced_implies_oscillatoryTail L225
• theorem eventuallyTickFiberMassBalanced_implies_exactShellTailCancellation L242
• def ShellSigTick L263
• def SignatureFin8OscillatoryTailBlocker L276
• structure Gap2TickPhaseTailBlockerStatus L282
• def gap2TickPhaseTailBlockerStatus L289
• theorem gap2TickPhaseTailBlockerStatus_flags L296