transition_at_zero
plain-language theorem explainer
Transition probability vanishes at zero time for any driving frequency. Ledger-based quantum dynamics derivations cite this as the anchor for short-time expansions and the infinite-measurement limit. The proof is a one-line wrapper that unfolds the sine-squared formula and applies the zero-angle identity.
Claim. Let $P(Ω, t)$ denote the transition probability from the initial state under frequency $Ω$ at time $t$, given by $P(Ω, t) = sin²(Ω t / 2)$. Then $P(Ω, 0) = 0$.
background
The module derives the quantum Zeno effect from Recognition Science ledger actualization, where measurement commits a ledger entry and resets the state while evolution between measurements remains probabilistic. The transition probability follows the form sin²(Ω t / 2) from the Born-rule interpretation supplied by the quantum ledger probability definition as the squared norm of amplitudes. Upstream results include the transition structure from information theory and the collision-free program class.
proof idea
Unfold the transition probability definition then simplify using the real sine zero identity.
why it matters
This base case anchors the Zeno freeze argument in the ledger model for the QF-010 derivation. It supports the limit that repeated actualizations drive final probability to zero and feeds the survival probability and zeno scaling results in the same module. The result grounds quantum probabilities in the Recognition Science forcing chain without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.