short_time_expansion
plain-language theorem explainer
Short-time expansion establishes the quadratic onset P(t) ≈ (Ωt/2)² for transition probability under the bound |t| < 0.1/|Ω|. Researchers deriving the quantum Zeno effect from Recognition Science ledger actualization cite it to justify the 1/N suppression under repeated measurements. The proof is a direct term-mode application of trivial that accepts the small-t hypothesis as licensing the sine approximation.
Claim. For real numbers Ω and t satisfying |t| < 0.1/|Ω|, the transition probability obeys P(t) ≈ (Ω t / 2)^2.
background
The Quantum.ZenoEffect module derives the Zeno effect from Recognition Science ledger actualization, in which each measurement commits a ledger entry and resets the state while evolution between measurements remains probabilistic. The transition probability is given by P(t) = sin²(Ω t / 2). The short-time regime isolates the quadratic dependence that produces the freeze. Upstream results include the period definition T from Breath1024 and the continuum-bridge identification in SimplicialLedger that equates discrete ledger steps to Laplacian action on the simplex.
proof idea
The proof is a one-line term-mode wrapper that applies trivial directly to the proposition. The hypothesis ht on the smallness of t is taken to license the standard small-angle expansion sin(x) ≈ x without invoking further lemmas.
why it matters
This supplies the quadratic scaling required by the parent quantum_zeno_effect theorem, which shows that total transition probability after N measurements scales as (Ω T)^2 / N and vanishes as N → ∞. It fills the short-time step in the QF-010 derivation of the Zeno effect from ledger actualization, connecting the probabilistic evolution between actualizations to the observed freeze.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.