module module moderate

`IndisputableMonolith.Quantum.ZenoEffect`

The Quantum.ZenoEffect module defines transition and survival probabilities for two-state systems under Recognition Science time quanta. It establishes the Zeno effect via P(t) = sin²(Ωt/2) and related scaling lemmas. Quantum measurement researchers cite it to link RS constants to suppression of transitions. The module is a collection of definitions and short lemmas with no complex proofs.

claimTransition probability $P(t) = \sin^2(\Omega t / 2)$ for Rabi frequency $\Omega$, with survival probability $1 - P(t)$ and short-time Zeno scaling derived from the RS time quantum $\tau_0$.

background

The module sits in the quantum domain and imports the RS time quantum $\tau_0 = 1$ tick from Constants. It introduces transitionProbability for two-state systems as the sin-squared Rabi formula and defines survivalProbability together with zenoSurvival. The setting uses the fundamental time quantum to constrain Rabi dynamics without additional hypotheses.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the Zeno-effect formalization that supports quantum measurement derivations in the Recognition framework. It connects the time quantum to transition suppression and feeds the overall forcing chain from T5 J-uniqueness onward.

scope and limits

Does not address multi-state or continuous spectra.
Does not incorporate gravity or the RS mass ladder.
Does not prove the full anti-Zeno crossover dynamics.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (19)

def transitionProbability L49
theorem transition_at_zero L53
theorem transition_bounded L58
def survivalProbability L67
def zenoSurvival L71
theorem quantum_zeno_effect L76
theorem short_time_expansion L82
theorem zeno_scaling L88
theorem anti_zeno_effect L96
def zenoAntiZenoCrossover L103
theorem zeno_from_ledger_actualization L116
theorem quadratic_from_symmetry L127
def experimentalHistory L139
def typicalFidelity L148
def applications L157
structure ZenoProtection L165
def philosophicalNote L180
structure ZenoFalsifier L191
def experimentalStatus L198