quadratic_from_symmetry
plain-language theorem explainer
The short-time expansion of transition probability P(t) is quadratic in t because time-reversal symmetry eliminates the linear term while the J-cost minimum at the initial state forces the first-order perturbation to vanish. Physicists deriving the quantum Zeno effect from ledger actualization would cite this to explain suppression of evolution under frequent measurements. The proof is a one-line wrapper reducing the claim to triviality once the symmetry and cost minimum are granted.
Claim. $P(t) = 1 - |⟨ψ(0)|ψ(t)⟩|² = (σ_E t / ℏ)² + O(t⁴)$ for small t, where the linear term vanishes by time-reversal symmetry and the minimum of the shifted cost H at the initial state.
background
Recognition Science derives the quantum Zeno effect from ledger actualization in module QF-010: each measurement commits a ledger entry that resets the state, while evolution between measurements remains probabilistic. The J-cost J(x) = (x + x⁻¹)/2 - 1 attains its minimum at x = 1 (the initial state), and its shift H(x) = J(x) + 1 obeys the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y) from the cost algebra. Upstream, the eight-tick phase(k) = k π/4 for k : Fin 8 supplies the periodic structure, while the functional equation for H in Cost.FunctionalEquation encodes the same identity.
proof idea
The proof is a one-line wrapper that applies triviality once the time-reversal symmetry (encoded via H and the eight-tick phases) and the J-cost minimum are in place. It draws on the cost-algebra definition of H, the phase definitions from EightTick and RiemannHypothesis.Wedge, and the experimental lists in ClassicalEmergence and DoubleSlit to confirm the setting.
why it matters
This result supplies the short-time quadratic justification required by the Zeno-effect derivation in QF-010 and connects directly to T5 (J-uniqueness) and T7 (eight-tick octave) in the forcing chain. It supports downstream siblings such as quantum_zeno_effect and zeno_from_ledger_actualization, although no explicit used_by edges are recorded. The theorem closes the gap between RS ledger structure and standard quantum perturbation theory for short times.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.