theorem
proved
phi8_fibonacci
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost on GitHub at line 39.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
62 phi8_amp : phi ^ 8 > 46
63 phi12_amp : phi ^ 12 > 300
64
65noncomputable def coherenceTimeCert : CoherenceTimeCert where
66 phi_ratio := coherenceTimeRatio
67 phi8_val := phi8_fibonacci
68 phi8_amp := phi8_gt_46
69 phi12_amp := phi12_gt_300