IndisputableMonolith.Gravity.SevenGaps.Gap2EnrichedCarrierPhase

declarations in this module (37)

• abbrev LabeledTick L54
• def GlobalEquivalentInvariant L57
• def descendedTick L62
• theorem descendedTick_mk L69
• def enrichedPhase L77
• def selfLoopCount L85
• theorem selfLoopCount_congr L90
• theorem selfLoopCount_ge_invariant L131
• def selfLoopTick L138
• theorem selfLoopTick_invariant L142
• def selfLoopClassTick L149
• def selfLoopPhase L152
• def twoLoopsComplex L158
• def twoBridgesComplex L163
• theorem selfLoopCount_twoLoops L167
• theorem selfLoopCount_twoBridges L181
• theorem not_ge_twoLoops_twoBridges L195
• def doubleEdgeSig L203
• def twoLoopsClass L208
• def twoBridgesClass L211
• theorem selfLoopClassTick_twoLoops L214
• theorem selfLoopClassTick_twoBridges L219
• theorem selfLoopClassTick_not_ShellSigTick L226
• theorem oscillatoryTail_of_enriched_eventual_balance L242
• theorem oscillatoryTail_of_enriched_identically_zero L252
• def TypedResidual_enriched_carrier_oscillatoryTail L274
• def TypedResidual_continuum_substrate_oscillatoryTail L280
• theorem bare_r5_of_enriched_carrier_oscillatoryTail L285
• theorem typedResidual_continuum_substrate_oscillatoryTail_of_enriched L292
• theorem typedResidual_continuum_substrate_oscillatoryTail_of_enriched_eventual_balance L298
• structure EnrichedCarrierPhaseSubstrate L306
• def selfLoopEnrichedSubstrate L311
• theorem enrichedCarrierPhaseSubstrate_nonempty L316
• theorem signatureBlocker_iff_no_shellSig_oscillatoryTail L320
• structure Gap2EnrichedCarrierPhaseStatus L328
• def gap2EnrichedCarrierPhaseStatus L338
• theorem gap2EnrichedCarrierPhaseStatus_flags L348