IndisputableMonolith.Gravity.SevenGaps.Gap2AntipodalBalanceBridge

declarations in this module (21)

• def EventuallyTickFiberAntipodalMassBalanced L46
• theorem eventuallyTickFiberMassBalanced_implies_antipodal L52
• lemma exp_two_pi_I_mul_nat L61
• lemma exp_eighth_period L80
• theorem tickRoot_add_four L112
• lemma antipodal_pair_term_eq_zero L131
• lemma sum_fin8_antipodal_cancel L138
• theorem exactShellAmplitude_eq_zero_of_antipodalBalanced_at L155
• theorem sum_amp_eq_zero_of_amps_zero L164
• theorem eventuallyAntipodalBalanced_implies_oscillatoryTail L173
• structure TailAntipodalShift L195
• theorem tickFiberMass_add_four_of_tailAntipodalShift L207
• theorem eventuallyTickFiberAntipodalMassBalanced_of_tailAntipodalShift L233
• theorem oscillatoryTail_of_tailAntipodalShift L240
• def equivIterate4 L248
• lemma tick_shift_four L251
• lemma mu_shift_four L273
• theorem nonempty_tailAntipodalShift_of_tailFiberShift L283
• structure Gap2AntipodalBalanceBridgeStatus L297
• def gap2AntipodalBalanceBridgeStatus L307
• theorem gap2AntipodalBalanceBridgeStatus_flags L317