No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
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
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
-
coherenceTimeCert
in IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
phi_ratio
in IndisputableMonolith.Chemistry.Quasicrystal
decl_use
-
phi8_val
in IndisputableMonolith.Cosmology.BaryonAsymmetryFromPhiLadder
decl_use
-
coherenceTimeAtRung
in IndisputableMonolith.Physics.QuantumCoherenceTimeFromJCost
decl_use