transition_bounded
plain-language theorem explainer
Transition probability P(Ω, t) = sin²(Ω t / 2) satisfies P ≤ 1 for all real Ω and t. Researchers working on measurement-induced state freezing in the Recognition Science ledger model cite this to keep probabilities normalized. The proof is a one-line term wrapper that unfolds the definition and invokes the standard bound sin²(x) ≤ 1.
Claim. For all real numbers $Ω$ and $t$, the transition probability $P(Ω, t) := sin²(Ω t / 2)$ obeys $P(Ω, t) ≤ 1$.
background
The module QF-010 derives the quantum Zeno effect from ledger actualization in Recognition Science. Measurement commits a ledger entry, resetting the state; between measurements the system evolves with transition probability sin²(Ω t / 2). The upstream probability definition from QuantumLedger returns the squared norm of amplitudes (Born rule), while the SMatrixUnitarity version returns |S_ij|², both ensuring non-negative values that must sum to at most 1.
proof idea
The term proof unfolds transitionProbability to expose sin²(Ω t / 2), then directly applies the Mathlib lemma Real.sin_sq_le_one to the scaled argument Ω t / 2.
why it matters
This bound is a prerequisite for the survival probability and full Zeno effect statements in the same module. It closes the unitarity step required by ledger actualization before the N → ∞ limit can be taken. In the Recognition framework it supports the probabilistic evolution between actualizations while preserving the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.