pith. machine review for the scientific record. sign in
def

philosophicalNote

definition
show as:
view math explainer →
module
IndisputableMonolith.Quantum.ZenoEffect
domain
Quantum
line
180 · github
papers citing
none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Quantum.ZenoEffect on GitHub at line 180.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 177
 178    But note: the pot does eventually boil in the real world!
 179    Real measurements take time and are not infinitely frequent. -/
 180def philosophicalNote : String :=
 181  "Real measurements take time, so perfect Zeno freeze is impossible. " ++
 182  "But significant suppression is achievable and useful."
 183
 184/-! ## Falsification Criteria -/
 185
 186/-- The Zeno effect derivation would be falsified by:
 187    1. Frequent measurement not suppressing decay
 188    2. Linear (not quadratic) short-time behavior
 189    3. Infinite measurement rate not leading to freeze
 190    4. Anti-Zeno effect in expected Zeno regime -/
 191structure ZenoFalsifier where
 192  /-- Type of potential falsification. -/
 193  falsifier : String
 194  /-- Status. -/
 195  status : String
 196
 197/-- All predictions verified. -/
 198def experimentalStatus : List ZenoFalsifier := [
 199  ⟨"Zeno suppression", "Verified in ions, atoms, photons"⟩,
 200  ⟨"Quadratic short-time", "Confirmed"⟩,
 201  ⟨"Anti-Zeno effect", "Also observed as predicted"⟩
 202]
 203
 204end ZenoEffect
 205end Quantum
 206end IndisputableMonolith