Empirical/CSD: the quantum Zeno effect (Build 15d)

Category: 3-Local (CSD-ontic volume layer; the freezing-under-frequent-measurement entry of the open-system tranche, after einselection (15a), QEC-decoherence (15b), and weak measurement (15c)).

A watched system does not evolve. Frequent projective measurements onto the initial state freeze the dynamics: the survival probability tends to one as the number of measurements grows. This file derives the mechanism and the limit, then states the honest CSD reading.

Part A: the Zeno mechanism (quadratic short-time decay, DERIVED)

For a Hermitian H and unit ψ the survival amplitude is a(s) = ⟨ψ, exp(-isH) ψ⟩ and the survival probability P(s) = ‖a(s)‖². The Zeno mechanism is the quadratic short-time behaviour: the initial decay slope vanishes (P'(0) = 0) and the leading correction is -(ΔH)²s² for the variance (ΔH)² = ⟨ψ,H²ψ⟩ − ⟨ψ,Hψ⟩².

Concrete qubit witness. This file realises the mechanism on the witness H = σx, ψ = |0⟩, where the evolution is the closed-form qubit rotation exp(-isσx) = cos s · I − i sin s · σx (zenoU; the standard matrix-exponential identity for the involution σx²=I, taken as the closed form, not re-derived from Matrix.exp). Everything downstream is then derived:

• the survival amplitude a(s) = ⟨0, zenoU s · 0⟩ = cos s (survAmp_eq), so P(s) = cos² s (survProb_eq) -- the genuine matrix computation, not asserted;
• the variance (ΔH)² = ⟨0,σx²·0⟩ − ⟨0,σx·0⟩² = 1 − 0 = 1 (varH_eq), computed from the matrices (meanH_eq, meanHsq_eq);
• the quadratic bound P(s) ≥ 1 − (ΔH)²·s² (zeno_survival_quadratic), derived from cos²s = 1 − sin²s ≥ 1 − s² (Real.sin_sq_le_sq); the coefficient is exactly the variance, not a free parameter -- this is the physics, not a hypothesis;
• the zero initial slope P'(0) = 0 (zeno_survival_slope_zero), via HasDerivAt on s ↦ cos² s. This zero slope is why frequent measurement freezes evolution.

Part B: the Zeno limit (freezing, DERIVED)

n equally-spaced projective re-measurements onto |0⟩ over a fixed total time t give survival P_n = P(t/n)^n (zenoSurvival). Then:

• zeno_survival_lower_bound: P_n ≥ 1 − (ΔH)²t²/n, derived from the Part-A quadratic bound plus Bernoulli's inequality (1−x)^n ≥ 1 − nx (one_add_mul_le_pow);
• zeno_freezing (headline): Tendsto (fun n => P_n) atTop (nhds 1) -- frequent measurement freezes the state -- by squeezing 1 − (ΔH)²t²/n ≤ P_n ≤ 1 between two sequences tending to one (tendsto_of_tendsto_of_tendsto_of_le_of_le). The full squeeze is proved, not just the lower bound.

Non-vacuity. (ΔH)² = 1 > 0 (zeno_variance_pos): |0⟩ is not a σx-eigenstate, so absent measurement the state genuinely evolves -- at s = π/2 the survival is 0 (zeno_no_measurement_decays, the state has fully precessed away). The freezing is a real effect of the repeated measurement, not a fixed-point triviality. (For an eigenstate (ΔH)²=0 the result is trivial; the genuine Zeno case is (ΔH)²>0.)

Part C: the CSD reading and its D1 gating

The honest CSD reading: each projective measurement re-carves the Σ-volume onto the initial sector |0⟩; frequent re-carving freezes the ontic-volume evolution, and the survival probability P_n → 1 is the ontic volume staying concentrated on the initial sector. The single-step survival P(s) = ‖⟨0, zenoU s·0⟩‖² is the rank-1 Born weight of the |0⟩ outcome, which the moment-map / Duistermaat-Heckman cluster (fs_born_volume_ratio_N, imported one layer down, Gleason-free) reads as a Fubini-Study volume ratio on the ontic Σ; this file does not re-prove that and does not fake a new volume theorem.

The dynamical realisation -- the measurement-interspersed Σ-flow Φ whose iteration freezes the ontic trajectory, the Zeno limit as a property of the de-isolation flow -- is D1-gated to LF6 (Φ = id in every concrete SectorData). What is delivered here is the operational / survival-probability freezing; the ontic-flow realisation is not claimed.

All exports are foundational-triple-only (no busch_effect_gleason): concrete Matrix algebra over EuclideanSpace ℂ (Fin 2), real trigonometric inequalities, and the Bernoulli / squeeze limit.

The witness observable and the closed-form qubit rotation

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.σx : Matrix (Fin 2) (Fin 2) ℂ

The measurement observable σx = !![0,1;1,0] (the unit Pauli-X axis). The preparation |0⟩ (WeakMeasurement.e0) is not an eigenstate of σx, so it genuinely evolves.

Equations

• CSD.Empirical.CSDBridge.QuantumZeno.σx = !![0, 1; 1, 0]

theorem CSD.Empirical.CSDBridge.QuantumZeno.σx_mul_self : σx * σx = 1

σx² = I (the Pauli involution).

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.zenoU (s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The closed-form qubit rotation zenoU s = cos s · I − i sin s · σx, i.e. exp(-isσx) (the standard matrix-exponential identity for the involution σx²=I, with θ = -is; taken as the closed form, not re-derived from Matrix.exp). It is the deterministic, unitary evolution generated by σx for a time s.

Equations

• CSD.Empirical.CSDBridge.QuantumZeno.zenoU s = !![↑(Real.cos s), -(Complex.I * ↑(Real.sin s)); -(Complex.I * ↑(Real.sin s)), ↑(Real.cos s)]

theorem CSD.Empirical.CSDBridge.QuantumZeno.zenoU_closed_form (s : ℝ) : zenoU s = ↑(Real.cos s) • 1 - (Complex.I * ↑(Real.sin s)) • σx

zenoU s = cos s · I − i sin s · σx (the closed-form linkage to exp(-isσx)).

The ⟨0, M·0⟩ sandwich on the qubit

theorem CSD.Empirical.CSDBridge.QuantumZeno.toEuclideanLin_ofLp (M : Matrix (Fin 2) (Fin 2) ℂ) (v : EuclideanSpace ℂ (Fin 2)) (i : Fin 2) : ((Matrix.toEuclideanLin M) v).ofLp i = M.mulVec v.ofLp i

theorem CSD.Empirical.CSDBridge.QuantumZeno.mulVec_e0 (M : Matrix (Fin 2) (Fin 2) ℂ) (i : Fin 2) : M.mulVec WeakMeasurement.e0.ofLp i = M i 0

theorem CSD.Empirical.CSDBridge.QuantumZeno.inner_e0_M (M : Matrix (Fin 2) (Fin 2) ℂ) : inner ℂ WeakMeasurement.e0 ((Matrix.toEuclideanLin M) WeakMeasurement.e0) = M 0 0

The diagonal sandwich ⟨0, M·0⟩ = M₀₀ on the |0⟩ preparation.

Part A: survival amplitude, probability, and the variance

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.survAmp (s : ℝ) : ℂ

The survival amplitude a(s) = ⟨0, exp(-isσx)·0⟩ on the |0⟩ preparation.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.survProb (s : ℝ) : ℝ

The survival probability P(s) = ‖a(s)‖².

Equations

• CSD.Empirical.CSDBridge.QuantumZeno.survProb s = ‖CSD.Empirical.CSDBridge.QuantumZeno.survAmp s‖ ^ 2

theorem CSD.Empirical.CSDBridge.QuantumZeno.survAmp_eq (s : ℝ) : survAmp s = ↑(Real.cos s)

(Part A) The survival amplitude is cos s -- derived from the matrix zenoU s, not asserted.

theorem CSD.Empirical.CSDBridge.QuantumZeno.survProb_eq (s : ℝ) : survProb s = Real.cos s ^ 2

(Part A) The survival probability is cos² s.

theorem CSD.Empirical.CSDBridge.QuantumZeno.survProb_nonneg (s : ℝ) : 0 ≤ survProb s

theorem CSD.Empirical.CSDBridge.QuantumZeno.survProb_le_one (s : ℝ) : survProb s ≤ 1

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.meanH : ℝ

The mean ⟨H⟩ = ⟨0, σx·0⟩.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.meanHsq : ℝ

The second moment ⟨H²⟩ = ⟨0, σx²·0⟩.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.varH : ℝ

The variance (ΔH)² = ⟨H²⟩ − ⟨H⟩².

Equations

• CSD.Empirical.CSDBridge.QuantumZeno.varH = CSD.Empirical.CSDBridge.QuantumZeno.meanHsq - CSD.Empirical.CSDBridge.QuantumZeno.meanH ^ 2

theorem CSD.Empirical.CSDBridge.QuantumZeno.meanH_eq : meanH = 0

⟨H⟩ = 0: |0⟩ is centred on the σx axis (computed from the matrix).

theorem CSD.Empirical.CSDBridge.QuantumZeno.meanHsq_eq : meanHsq = 1

⟨H²⟩ = 1: from σx² = I and ‖|0⟩‖ = 1.

theorem CSD.Empirical.CSDBridge.QuantumZeno.varH_eq : varH = 1

(Part A) The variance (ΔH)² = 1 -- computed from the matrices, not assumed. This is the coefficient in the quadratic bound below.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_variance_pos : 0 < varH

(Part A, non-vacuity) (ΔH)² > 0: |0⟩ is not a σx-eigenstate, so the state genuinely evolves absent measurement.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_survival_quadratic (s : ℝ) : 1 - varH * s ^ 2 ≤ survProb s

(Part A core) The Zeno mechanism: quadratic short-time bound P(s) ≥ 1 − (ΔH)²·s². Derived from cos²s = 1 − sin²s ≥ 1 − s² with the coefficient equal to the computed variance. The quadratic (not linear) leading behaviour is the freezing mechanism.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_survival_slope_zero : HasDerivAt survProb 0 0

(Part A) Zero initial decay slope P'(0) = 0. The survival probability has a vanishing first derivative at s = 0; this is the precise sense in which a watched system does not begin to evolve. Proved via HasDerivAt on s ↦ cos² s.

Part B: the Zeno limit (freezing under frequent measurement)

theorem CSD.Empirical.CSDBridge.QuantumZeno.pow_lower {P u : ℝ} (n : ℕ) (hP : 0 ≤ P) (hPu : 1 - u ≤ P) (_hu : 0 ≤ u) : 1 - ↑n * u ≤ P ^ n

Bernoulli + monotonicity helper: if 0 ≤ P, 1 − u ≤ P, 0 ≤ u, then 1 − n·u ≤ P^n.

noncomputable def CSD.Empirical.CSDBridge.QuantumZeno.zenoSurvival (t : ℝ) (n : ℕ) : ℝ

n equally-spaced projective re-measurements onto |0⟩ over total time t: the survival probability P_n = P(t/n)^n.

Equations

• CSD.Empirical.CSDBridge.QuantumZeno.zenoSurvival t n = CSD.Empirical.CSDBridge.QuantumZeno.survProb (t / ↑n) ^ n

theorem CSD.Empirical.CSDBridge.QuantumZeno.zenoSurvival_le_one (t : ℝ) (n : ℕ) : zenoSurvival t n ≤ 1

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_survival_lower_bound (t : ℝ) (n : ℕ) : 1 - varH * t ^ 2 / ↑n ≤ zenoSurvival t n

(Part B) The Zeno lower bound P_n ≥ 1 − (ΔH)²t²/n. Derived from the Part-A quadratic bound plus Bernoulli's inequality.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_freezing (t : ℝ) : Filter.Tendsto (fun (n : ℕ) => zenoSurvival t n) Filter.atTop (nhds 1)

(Part B headline) The Zeno freezing theorem. Under n → ∞ equally-spaced projective re-measurements over a fixed total time t, the survival probability tends to one: a watched system does not evolve. Proved by squeezing 1 − (ΔH)²t²/n ≤ P_n ≤ 1.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_no_measurement_decays : survProb (Real.pi / 2) = 0

(Part B, non-vacuity) Without measurement the state decays. At the single time s = π/2 the survival probability is 0: |0⟩ precesses entirely off the σx axis. So the freezing zeno_freezing is a genuine effect of the repeated measurement, contrasting the free evolution that would carry the state away.

theorem CSD.Empirical.CSDBridge.QuantumZeno.zeno_nonvacuous : 0 < varH ∧ survProb (Real.pi / 2) = 0

(Non-vacuity bundle) The genuine Zeno regime: positive variance (the state would evolve) together with full free decay at s = π/2 (it does evolve, maximally), against which the freezing limit is non-trivial.