transitionProbability
Transition probability for a two-state system is defined as the square of the sine of half the Rabi frequency times time. Physicists modeling quantum measurement effects from ledger actualization cite this when building the Zeno freeze from repeated actualizations. The definition is a direct one-line encoding of the standard Rabi formula with no additional hypotheses.
claim$P(t) = [sin(Ω t / 2)]^2$, where Ω is the Rabi frequency and t is elapsed time.
background
Module Quantum.ZenoEffect derives the quantum Zeno effect from Recognition Science ledger actualization: each measurement commits a ledger entry, frequent actualizations reset the state, and evolution between measurements remains probabilistic. The supplied definition supplies the base transition probability for a driven two-level system. Upstream probability definitions from QuantumLedger (Born-rule norm squared), SMatrixUnitarity (|S_ij|^2), and BoltzmannDistribution supply the shared probabilistic interpretation used here.
proof idea
One-line definition that directly sets the value to the squared sine of half the product of Rabi frequency and time.
why it matters in Recognition Science
This definition is the base probability fed by survivalProbability, transition_at_zero, and transition_bounded inside the same module. It fills the QF-010 target of deriving the Zeno effect from ledger actualization, connecting standard Rabi dynamics to the Recognition Science forcing chain through probabilistic actualization. It leaves open how RS-native constants (phi-ladder, phi^-5 for hbar) fix the value of Ω.
scope and limits
- Does not derive the N to infinity Zeno suppression limit.
- Does not relate Ω to Recognition Science constants such as phi.
- Does not extend the formula to systems with more than two levels.
Lean usage
noncomputable def survivalProbability (Ω t : ℝ) : ℝ := 1 - transitionProbability Ω tformal statement (Lean)
49noncomputable def transitionProbability (Ω t : ℝ) : ℝ :=
proof body
Definition body.
50 (Real.sin (Ω * t / 2))^2
51
52/-- **THEOREM**: Transition probability starts at 0. -/