structure
definition
CoherenceTimeCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost on GitHub at line 59.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
70
71end IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost