IndisputableMonolith.Foundation.CoherenceExponentUniqueness

declarations in this module (16)

• def k_fib L37
• def k_int L40
• theorem agreement_at_3 L43
• theorem both_equal_5_at_3 L46
• theorem disagreement_at_1 L49
• theorem disagreement_at_2 L52
• theorem disagreement_at_4 L55
• theorem exponent_unique_at_D3 L58
• theorem k5_forced_at_D3 L63
• def coherenceExponent L67
• theorem coherenceExponent_eq_5 L68
• def einsteinKappaExponent L71
• def einsteinKappaPeriod L72
• theorem kappa_eq_8phi5 L73
• structure CoherenceExponentCert L75
• def coherenceExponentCert L84