coherence_exponent_eq_5

formal source

  75def coherence_exponent : ℕ := octave - D
  76
  77/-- The coherence exponent equals 5 -/
  78theorem coherence_exponent_eq_5 : coherence_exponent = 5 := by
  79  unfold coherence_exponent octave D
  80  norm_num
  81
  82/-- The coherence exponent equals F₅ -/
  83theorem coherence_exponent_is_fib_5 : coherence_exponent = fib 5 := by
  84  rw [coherence_exponent_eq_5, fib_5_eq]
  85
  86/-- The coherence exponent arises from the Fibonacci identity -/
  87theorem coherence_exponent_from_fibonacci :
  88    coherence_exponent = fib 6 - fib 4 := by
  89  rw [coherence_exponent_is_fib_5, fibonacci_deficit]
  90
  91/-! ## Uniqueness of D = 3 -/
  92
  93/-- Check if n is a Fibonacci number (for small n, by enumeration) -/
  94def is_fibonacci (n : ℕ) : Bool :=
  95  n ∈ [1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987, 1597]
  96
  97/-- D = 1 satisfies the Fibonacci constraint but is degenerate -/
  98theorem D_1_fibonacci_constraint : is_fibonacci 1 ∧ is_fibonacci (2^1) := by
  99  constructor <;> native_decide
 100
 101/-- D = 2 does NOT satisfy: 2^2 = 4 is not Fibonacci -/
 102theorem D_2_fails : ¬ is_fibonacci (2^2) := by native_decide
 103
 104/-- D = 3 satisfies the Fibonacci constraint -/
 105theorem D_3_fibonacci_constraint : is_fibonacci 3 ∧ is_fibonacci (2^3) := by
 106  constructor <;> native_decide
 107
 108/-- D = 5 does NOT satisfy: 2^5 = 32 is not Fibonacci -/