exponent_unique_at_D3

formal source

  55theorem disagreement_at_4 : k_fib 4 ≠ k_int 4 := by decide
  56
  57/-- D = 3 is the unique dimension in {1,2,3,4} where both routes agree. -/
  58theorem exponent_unique_at_D3 :
  59    ∀ D ∈ ({1, 2, 3, 4} : Finset ℕ), k_fib D = k_int D ↔ D = 3 := by
  60  decide
  61
  62/-- Corollary: k = 5 is uniquely forced at D = 3. -/
  63theorem k5_forced_at_D3 : k_fib 3 = 5 ∧ k_int 3 = 5 ∧ k_fib 3 = k_int 3 := by
  64  decide
  65
  66/-- From k=5: ℏ = φ^(-5) in RS units. -/
  67def coherenceExponent : ℕ := 5
  68theorem coherenceExponent_eq_5 : coherenceExponent = 5 := rfl
  69
  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