survivalProbability
plain-language theorem explainer
Survival probability after one measurement in a two-state system equals one minus the transition probability. Researchers deriving the quantum Zeno effect from Recognition Science ledger actualization cite this when constructing the watched-pot freeze. The definition is a direct algebraic complement to the Rabi sin-squared form.
Claim. For a two-state system with Rabi frequency $Ω$, the survival probability after time $t$ is $1 - sin²(Ω t / 2)$.
background
The Quantum.ZenoEffect module derives the quantum Zeno effect from ledger actualization: each measurement commits a ledger entry and resets the state, while evolution between measurements remains probabilistic. The transition probability is defined as $sin²(Ω t / 2)$ for Rabi frequency $Ω$. Upstream results include the Born-rule probability from QuantumLedger (squared norm of amplitudes) and the S-matrix transition probability from QFT.SMatrixUnitarity.
proof idea
One-line wrapper that subtracts transitionProbability Ω t from 1.
why it matters
This definition supplies the base term for zenoSurvival, which establishes that survival probability tends to 1 as the number of measurements N tends to infinity. It fills the QF-010 target of obtaining the quantum Zeno effect from Recognition Science ledger structure. The construction aligns with the framework's emphasis on frequent actualization suppressing transitions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.