Documentation

CsdLean4.Empirical.CSD.ElitzurVaidmanVolume

Empirical/CSD: the Elitzur–Vaidman split probability as a Kähler typicality volume #

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

The CSD twin of [Empirical/QM/ElitzurVaidman.lean]. In the bomb tester, after the first beam splitter the photon is in H|0⟩ = (|0⟩+|1⟩)/√2, and the 1/2 weights (survive, and the conditioned dark-port) are the Born weights |⟨e, H|0⟩⟩|² = 1/2. Here that 1/2 is realised as a Fubini–Study typicality volume on the ontic Σ = ℂℙ¹: for the beam-splitter state |+⟩ = (|0⟩+|1⟩)/√2,

μ_FS { [φ] : Φ₀([φ]) ≤ Φ₀([|+⟩]) } = 1/2,

with volume = Born computed via Duistermaat–Heckman (carving-free, busch_effect_gleason-free). So the interaction-free-measurement branch weights are ontic typicality volumes.

References #

Empirical/QM/ElitzurVaidman.lean (bomb_safe_prob); LF4/MomentUniform.lean (fs_born_volume_ratio_qubit_uncond); Empirical/CSD/MachZehnderVolume.lean (the interferometer as a Kähler volume).

source
noncomputable def CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState :
EuclideanSpace ℂ (Fin 2)

The beam-splitter state |+⟩ = (|0⟩ + |1⟩)/√2.

Equations
Instances For
    source
    @[simp]
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_zero :
    bsState.ofLp 0 = (↑√2)⁻¹
    source
    @[simp]
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_one :
    bsState.ofLp 1 = (↑√2)⁻¹
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.norm_inv_sqrt2_sq :
    ‖(↑√2)⁻¹‖ ^ 2 = 1 / 2
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_normsq :
    ∑ i : Fin 2, ‖bsState.ofLp i‖ ^ 2 = 1
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_ne :
    bsState ≠ 0
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_norm :
    ‖bsState‖ = 1
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.bsState_born0 :
    ‖inner ℂ (EuclideanSpace.single 0 1) bsState‖ ^ 2 = 1 / 2
    source
    theorem CSD.Empirical.CSDBridge.ElitzurVaidmanVolume.ev_split_as_volume (p₀ : LF4.CPN 2) :
    (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ bsState bsState_ne) 0} = ENNReal.ofReal (1 / 2)

    The Elitzur–Vaidman 1/2 split probability is a Fubini–Study typicality volume. The beam splitter's Born weight 1/2 (the survival / conditioned-dark-port weight) equals the FS volume of the moment-sublevel region cut by [|+⟩] on the ontic ℂℙ¹ — Born as Kähler volume, via Duistermaat–Heckman.