def
definition
philosophicalNote
show as:
view math explainer →
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
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