Empirical/CSD: Mach–Zehnder single-photon interference (CSD Born-as-volume)

Category: 3-Local (CSD-ontic layer; genuine volume derivation).

The Mach–Zehnder interferometer — a single photon split by a beam splitter, given a relative phase φ in one arm, recombined by a second beam splitter, then detected — is the most iconic interference experiment, and was the one conspicuous phenomenon missing from the empirical tree (roadmap B4). This module supplies it as a CSD Born-as-volume derivation.

A single photon in two modes IS a qubit, and the MZ circuit is the qubit phase circuit H · D(φ) · H · |0⟩ (beam splitter = H, arm phase = D(φ) = diag(1, e^{iφ})). The corpus already has this state as Metrology.ramseyVec φ — and ramseyVec_eq_circuit machine-checks that the closed form genuinely equals the interferometer circuit output. So the MZ fringe legitimately reuses the qubit interference machinery (ramsey_fringe_volume): the detector-0 probability is the Fubini–Study volume cos²(φ/2), Born = FS volume derived one layer down (Duistermaat–Heckman), carving- free and Gleason-free.

What is genuinely new here (beyond the Ramsey fringe)

The interferometric visibility V = (P_max − P_min)/(P_max + P_min) = 1 for a pure single photon — the canonical full-coherence result. mz_bright/mz_dark give the constructive (P(0) = 1) and destructive (P(π) = 0) fringes, mzProb_{nonneg,le_one} show these are the genuine extrema of cos²(φ/2) ∈ [0,1], and mz_visibility_one concludes V = 1.

Honest scope

The fringe value reuses the Ramsey qubit derivation (same physics: a two-mode single photon is a qubit). The new content is the visibility. As with the whole volume series, the moment-region ↔ physical-detector-outcome labelling is the interpretive LF4-todo §14 boundary; the number cos²(φ/2) and the visibility 1 are derived.

References: Empirical/Metrology/Ramsey.lean (ramseyVec, ramseyVec_eq_circuit, ramseyFringe, ramsey_fringe_volume, ramsey_fringe_max/min), SigmaLayer/Interference.lean (HasBornInterference), specs/qm-empirical-tests.md (B4).

noncomputable def CSD.Empirical.CSDBridge.MachZehnder.mzOutput (φ : ℝ) : EuclideanSpace ℂ (Fin 2)

The Mach–Zehnder output state. The two-beam-splitter-plus-phase circuit H · D(φ) · H · |0⟩, which the corpus proves (machine-checked, ramseyVec_eq_circuit) equals ramseyVec φ.

Equations

• CSD.Empirical.CSDBridge.MachZehnder.mzOutput φ = CSD.Empirical.Metrology.ramseyVec φ

noncomputable def CSD.Empirical.CSDBridge.MachZehnder.mzProb (φ : ℝ) : ℝ

The Mach–Zehnder detector-0 probability as a function of the arm phase φ: the Fubini–Study volume cos²(φ/2) (= ramseyFringe φ).

Equations

• CSD.Empirical.CSDBridge.MachZehnder.mzProb φ = CSD.Empirical.Metrology.ramseyFringe φ

theorem CSD.Empirical.CSDBridge.MachZehnder.mzProb_eq (φ : ℝ) : mzProb φ = Real.cos (φ / 2) ^ 2

theorem CSD.Empirical.CSDBridge.MachZehnder.mzProb_nonneg (φ : ℝ) : 0 ≤ mzProb φ

The MZ probability is a genuine probability in [0, 1] — lower bound.

theorem CSD.Empirical.CSDBridge.MachZehnder.mzProb_le_one (φ : ℝ) : mzProb φ ≤ 1

The MZ probability is a genuine probability in [0, 1] — upper bound.

theorem CSD.Empirical.CSDBridge.MachZehnder.mz_bright : mzProb 0 = 1

Bright fringe (constructive interference): at zero relative phase the photon exits detector 0 with certainty, P(0) = 1.

theorem CSD.Empirical.CSDBridge.MachZehnder.mz_dark : mzProb Real.pi = 0

Dark fringe (destructive interference): at phase π detector 0 never fires, P(π) = 0.

noncomputable def CSD.Empirical.CSDBridge.MachZehnder.mzVisibility : ℝ

Interferometric visibility V = (P_max − P_min)/(P_max + P_min), with the extrema attained at the bright (φ = 0) and dark (φ = π) fringes (mzProb_{nonneg,le_one} confirm these bound cos²(φ/2)).

Equations

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

theorem CSD.Empirical.CSDBridge.MachZehnder.mz_visibility_one : mzVisibility = 1

Mach–Zehnder visibility = 1 for a pure single photon. The canonical full-coherence result: the fringe swings between P = 1 (bright) and P = 0 (dark), so V = (1 − 0)/(1 + 0) = 1. This is the iconic interference signature, here derived from the Born-as-volume fringe cos²(φ/2) (mz_bright, mz_dark).

theorem CSD.Empirical.CSDBridge.MachZehnder.mz_fringe_volume (φ : ℝ) (p₀ : LF4.CPN 2) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 2) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (Metrology.ramseyVec φ) ⋯) 0}).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, Filter.Tendsto (fun (M : ℕ) => (∑ i ∈ Finset.range M, (X i ⁻¹' {p : LF4.CPN 2 | LF4.momentMap p 0 ≤ LF4.momentMap (Projectivization.mk ℂ (Metrology.ramseyVec φ) ⋯) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (Metrology.ramseyFringe φ))

The MZ fringe as a genuine Fubini–Study volume. i.i.d. FS-typicality trials scoring the moment-sublevel region cut by the MZ output ray have empirical frequency converging a.s. to cos²(φ/2) — Born = FS volume, carving-free and Gleason-free (reused from the qubit interference derivation Metrology.ramsey_fringe_volume; the MZ output IS ramseyVec φ).