IndisputableMonolith.Gravity.SevenGaps.Gap2TickPhaseSubstrate

declarations in this module (35)

• def tickDerivedPhase L58
• def tickRoot L63
• theorem tickDerivedPhase_exp L66
• structure ExactShellTickPhaseSubstrate L83
• def tickFiber L98
• def TickEquidistributedInShell L105
• def tickFiberMass L111
• def TickFiberMassBalanced L118
• theorem tickCardEquidistribution_constantMu_implies_massBalanced L123
• lemma eighth_root_ne_one L142
• lemma eighth_root_pow_eight L167
• theorem sum_tickRoots_eq_zero L176
• theorem exactShellAmplitude_tick_fiberwise L201
• theorem exactShellAmplitude_eq_zero_of_massBalanced L232
• theorem tickEquidistribution_implies_shellAmplitudeVanishes L256
• def TypedResidual_strengthened_tick_balance L281
• def TypedResidual_shell_phase_enrichment_schema L287
• def signatureVertexTick L300
• def edgeHeavyComplex L304
• def edgeHeavySig L309
• def edgeHeavyClass L316
• theorem signatureVertexTick_edgeHeavy L319
• theorem signatureVertexTick_isolated L324
• theorem signatureVertexTickPhase_not_shellConstant L329
• theorem signatureVertexTickPhase_not_eventuallyZero L355
• def signatureVertexTickSubstrate L383
• theorem typedResidual_shell_phase_enrichment_schema_closed L388
• def complexityTick L395
• def complexityTickPhase L398
• theorem complexityTickPhase_shellConstant L403
• theorem complexityTickPhase_not_oscillatoryTail L409
• theorem complexityTickPhase_decoy_dead L414
• structure Gap2TickPhaseSubstrateStatus L421
• def gap2TickPhaseSubstrateStatus L427
• theorem gap2TickPhaseSubstrateStatus_flags L433