  28
  29noncomputable def coherenceTimeAtRung (k : ℕ) : ℝ := phi ^ k
  30
  31theorem coherenceTimeRatio (k : ℕ) :
  32    coherenceTimeAtRung (k + 1) / coherenceTimeAtRung k = phi := by
  33  unfold coherenceTimeAtRung
  34  have hpos := pow_pos phi_pos k
  35  rw [pow_succ, div_eq_iff hpos.ne']
  36  ring
  37
  38/-- φ^8 = 21φ + 13 (Fibonacci identity). -/
  39theorem phi8_fibonacci : phi ^ 8 = 21 * phi + 13 := by
  40  have h2 := phi_sq_eq
  41  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  42  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  43  nlinarith [sq_nonneg (phi ^ 4)]
  44
  45/-- φ^8 > 46 (proved separately). -/
  46theorem phi8_gt_46 : phi ^ 8 > 46 := by
  47  rw [phi8_fibonacci]; linarith [phi_gt_onePointSixOne]
  48
  49/-- φ^12 > 300 (bounding coherence). -/
  50theorem phi12_gt_300 : phi ^ 12 > 300 := by
  51  have h8 := phi8_fibonacci
  52  have h4 : phi ^ 4 = 3 * phi + 2 := by
  53    have h2 := phi_sq_eq
  54    have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  55    nlinarith
  56  have h12 : phi ^ 12 = (phi ^ 8) * (phi ^ 4) := by ring
  57  nlinarith [phi_gt_onePointSixOne]
  58
  59structure CoherenceTimeCert where
  60  phi_ratio : ∀ k, coherenceTimeAtRung (k + 1) / coherenceTimeAtRung k = phi
  61  phi8_val : phi ^ 8 = 21 * phi + 13

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.