IndisputableMonolith.Gravity.SevenGaps.ZqContinuumBlocker

declarations in this module (26)

• abbrev CapPhaseFamily L50
• def phasedZqSequence L53
• def HasPhasedZqComplexityLimit L58
• def PhasedZqCauchyCriterion L62
• theorem hasPhasedZqComplexityLimit_iff_cauchy L70
• def exactShellAmplitude L88
• def Zcap L98
• def OscillatoryTail L104
• theorem Zcap_telescoping L111
• theorem cauchySeq_Zcap_iff_oscillatoryTail L120
• def exactComplexityCutoff L147
• def HasExactComplexityCutoffLimit L153
• def ExactShellTailCancellation L160
• theorem exactComplexityCutoff_sub L167
• theorem hasExactComplexityCutoffLimit_iff_tailCancellation L178
• theorem exactShellAmplitude_zeroPhase L209
• theorem zeroPhase_epsilon_one_failure L222
• theorem zeroPhase_not_exactShellTailCancellation L253
• theorem zeroPhase_not_oscillatoryTail L287
• theorem zeroPhase_Zcap_not_cauchy L296
• theorem not_hasExactComplexityCutoffLimit_zeroPhase L302
• theorem zeroPhase_fails_both_removal_routes L310
• structure CapShellCompatibility L323
• theorem hasPhasedZqLimit_iff_exactShellTail_of_compatibility L332
• def zeroCapPhaseFamily L343
• theorem zeroPhase_compatibility_and_limit_impossible L351