kappa_eq_8phi5

formal source

  70/-- Einstein coupling κ = 8φ^5 in RS units (from k=5 and 8-tick period). -/
  71def einsteinKappaExponent : ℕ := 5
  72def einsteinKappaPeriod : ℕ := 8
  73theorem kappa_eq_8phi5 : einsteinKappaExponent = 5 ∧ einsteinKappaPeriod = 8 := by decide
  74
  75structure CoherenceExponentCert where
  76  agree_at_3 : k_fib 3 = k_int 3
  77  both_five : k_fib 3 = 5 ∧ k_int 3 = 5
  78  disagree_1 : k_fib 1 ≠ k_int 1
  79  disagree_2 : k_fib 2 ≠ k_int 2
  80  disagree_4 : k_fib 4 ≠ k_int 4
  81  unique_at_3 : ∀ D ∈ ({1, 2, 3, 4} : Finset ℕ), k_fib D = k_int D ↔ D = 3
  82  k5_forced : k_fib 3 = 5 ∧ k_int 3 = 5 ∧ k_fib 3 = k_int 3
  83
  84def coherenceExponentCert : CoherenceExponentCert where
  85  agree_at_3 := agreement_at_3
  86  both_five := both_equal_5_at_3
  87  disagree_1 := disagreement_at_1
  88  disagree_2 := disagreement_at_2
  89  disagree_4 := disagreement_at_4
  90  unique_at_3 := exponent_unique_at_D3
  91  k5_forced := k5_forced_at_D3
  92
  93end IndisputableMonolith.Foundation.CoherenceExponentUniqueness