def definition def or abbrev

`experimentalHistory`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 139def experimentalHistory : List String := [

proof body

Definition body.

 140  "1977: Misra and Sudarshan name the effect",
 141  "1989: Itano et al. observe in trapped ions (NIST)",
 142  "2001: BEC observation",
 143  "2006: Photon tunneling suppression"
 144]
 145
 146/-- The effect has been observed with high fidelity.
 147    State preservation >99% with ~1000 measurements per decay time. -/

depends on (5)

Lean names referenced from this declaration's body.

State in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
State in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
measurements in IndisputableMonolith.StandardModel.WeinbergAngle decl_use