Documentation

CsdLean4.Empirical.CSD.LeggettGargVolume

Empirical/CSD: the Leggett–Garg two-time survival probability as a Kähler typicality volume #

Category: 3-Local (CSD-ontic layer).

The CSD twin of [Empirical/QM/LeggettGarg.lean]. The Leggett–Garg two-time correlation ⟨Q(0)Q(Δ)⟩ = cos(2Δ) is built (with intermediate collapse) from the qubit survival probability P(0→0) = cos²Δ = |⟨0, e^{-iΔσ_x}|0⟩⟩|². Here that Born weight is realised as a Fubini–Study typicality volume on the ontic Σ = ℂℙ¹: for the precessed state |Δ⟩ = cos Δ|0⟩ − i sin Δ|1⟩,

μ_FS { [φ] : Φ₀([φ]) ≤ Φ₀([|Δ⟩]) } = cos²Δ,

with volume = Born computed via the Duistermaat–Heckman theorem fs_moment_pushforward_uniform (carving-free, busch_effect_gleason-free). So the LG transition statistics are ontic typicality volumes, not a Born postulate.

References #

Empirical/QM/LeggettGarg.lean (lgCorr_eq); LF4/MomentUniform.lean (fs_born_volume_ratio_qubit_uncond); Empirical/CSD/MalusVolume.lean (the same volume-frequency pattern for the Malus law).

source
noncomputable def CSD.Empirical.CSDBridge.LeggettGargVolume.lgState (Δ : ℝ) :
EuclideanSpace ℂ (Fin 2)

The precessed qubit state |Δ⟩ = e^{-iΔσ_x}|0⟩ = cos Δ|0⟩ − i sin Δ|1⟩.

Equations
Instances For
    source
    @[simp]
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_zero (Δ : ℝ) :
    (lgState Δ).ofLp 0 = ↑(Real.cos Δ)
    source
    @[simp]
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_one (Δ : ℝ) :
    (lgState Δ).ofLp 1 = -(Complex.I * ↑(Real.sin Δ))
    source
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_normsq (Δ : ℝ) :
    ∑ i : Fin 2, ‖(lgState Δ).ofLp i‖ ^ 2 = 1
    source
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_ne (Δ : ℝ) :
    lgState Δ ≠ 0
    source
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_norm (Δ : ℝ) :
    ‖lgState Δ‖ = 1
    source
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lgState_born0 (Δ : ℝ) :
    ‖inner ℂ (EuclideanSpace.single 0 1) (lgState Δ)‖ ^ 2 = Real.cos Δ ^ 2
    source
    theorem CSD.Empirical.CSDBridge.LeggettGargVolume.lg_survival_as_volume (Δ : ℝ) (p₀ : LF4.CPN 2) :
    (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (lgState Δ) ⋯) 0} = ENNReal.ofReal (Real.cos Δ ^ 2)

    The Leggett–Garg survival probability cos²Δ is a Fubini–Study typicality volume. The P(0→0) = cos²Δ transition weight of the two-time correlation equals the FS volume of the moment-sublevel region cut by the precessed state [|Δ⟩] on the ontic ℂℙ¹ — Born as Kähler volume, via Duistermaat–Heckman.