zenoSurvival
plain-language theorem explainer
zenoSurvival defines the total survival probability after N measurements spaced over time T as the single-interval survival probability raised to the Nth power. A physicist modeling the watched-pot effect or measurement-induced state freezing would cite this expression when analyzing suppression of transitions. The definition is a direct composition of the single-step survival function applied to the rescaled interval T/N.
Claim. Let $S(t)$ denote the probability of remaining in the initial state after a single interval of length $t$ under transition frequency $Ω$. The survival probability after $N$ equally spaced measurements over total time $T$ is then $[S(T/N)]^N$.
background
The module QF-010 derives the quantum Zeno effect from Recognition Science ledger actualization, in which each measurement commits a ledger entry that resets the system while evolution between measurements remains probabilistic. The upstream survivalProbability definition states that single-interval survival equals one minus the transition probability. The Breath1024.T abbreviation supplies fundamental periods while Gap45.SyncMinimization.T defines the nth triangular number; neither enters the present expression directly. The local setting treats frequent actualization as the mechanism that keeps the system pinned to its measured state.
proof idea
This is a one-line definition that applies the sibling survivalProbability function to the rescaled interval T/N and raises the result to the power N. No additional lemmas or tactics are required beyond the direct composition.
why it matters
The definition supplies the finite-N expression taken to the limit in the downstream quantum_zeno_effect theorem, which asserts survival approaches 1 as N tends to infinity. It realizes the QF-010 target of obtaining the Zeno freeze from ledger actualization within the Recognition Science framework. The construction encodes how repeated measurements suppress transitions, consistent with the forcing chain and the underlying discreteness that yields quantum behavior.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.