pith. sign in
module module moderate

IndisputableMonolith.Quantum.ZenoEffect

show as:
view Lean formalization →

This module defines transition and survival probabilities for two-state quantum systems in Recognition Science, with the Zeno effect following from the discrete time quantum. Physicists studying measurement-induced suppression of evolution would cite these when linking continuous Rabi dynamics to the RS tick. The module is a collection of definitions and short lemmas establishing the sine-squared form and its short-time quadratic behavior.

claimThe transition probability for a two-state system is $P(t) = \sin^2(\Omega t / 2)$, where $\Omega$ is the Rabi frequency and $t$ is measured in units of the RS time quantum $\tau_0 = 1$.

background

The module imports the RS time quantum $\tau_0 = 1$ tick from IndisputableMonolith.Constants. It introduces transitionProbability as the probability $P(t) = \sin^2(\Omega t / 2)$ for a two-state system, along with related quantities such as survivalProbability and zenoSurvival. The local setting is the quantum domain of Recognition Science, where time is discretized by the fundamental tick and continuous evolution is recovered in the appropriate limit.

proof idea

This is a definition module, no proofs. The listed siblings establish the sine-squared transition law by direct substitution, verify boundary conditions such as transition_at_zero, and derive boundedness and short-time expansions from trigonometric identities.

why it matters in Recognition Science

The module supplies the quantum transition machinery required to embed the Zeno effect inside the Recognition framework. It would feed into higher-level results on actualization and measurement that connect to the forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law, although no direct downstream theorems are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (19)