IndisputableMonolith.Gravity.SevenGaps.Gap2TailAutFiberParityBlocker

declarations in this module (23)

• def AutFiberBucket L49
• theorem classMu_eq_one_div_shellAutCard L56
• theorem shellAutCard_eq_of_classMu_eq L76
• def TailAutFiberEven L97
• def TailAutFiberParityBlocker L104
• abbrev TickLow L109
• abbrev TickHigh L112
• lemma val_add_four_low L115
• lemma val_add_four_high L122
• def lowEquivHigh L130
• def splitLowHigh L153
• theorem even_card_of_tick_add_four L171
• def bucketTau L186
• def shiftBucketEquiv L190
• theorem tailAutFiberEven_of_tailAntipodalShift L205
• theorem no_tailAntipodalShift_of_parityBlocker L218
• def BareR5ResidualShape L232
• structure BareR5DecoyCertificate L244
• def bareR5DecoyCertificate L251
• theorem bareR5DecoyCertificate_banked L257
• structure Gap2TailAutFiberParityBlockerStatus L263
• def gap2TailAutFiberParityBlockerStatus L272
• theorem gap2TailAutFiberParityBlockerStatus_flags L282