Empirical/Metrology: Ramsey interferometry as a parameter-driven Kähler flow

Category: 3-Local (CSD-ontic metrology layer; genuine volume derivation, not a transport tag).

This is item A1 of specs/metrology-plan.md: the Ramsey sequence |0⟩ → [π/2 pulse] → [free precession, phase φ(θ)] → [π/2 pulse] → measure realised in CSD. Two pieces:

1. The phase flow (ramseyPhaseFlow). The free-precession step is the diagonal unitary diag(1, e^{iφ}) acting on the probe Σ = ℂℙ¹. It is the first metrology flow: a deterministic, Fubini–Study-measure-preserving symplectic flow on Σ driven by the external classical parameter φ(θ) = ω·t (ramseyPhaseFlow_measurePreserving), genuinely ≠ id (ramseyPhaseFlow_ne_id). It is the λ = (0,1) instance of the audited diagonal-phase observable flow LF4.obsFlow (diag(exp(i·t·λ))); we reuse that machinery rather than reinvent it.

2. The fringe (ramsey_fringe_volume). The measurement-|0⟩ probability is the standard symmetric Ramsey fringe cos²(φ/2). The Ramsey output state ramseyVec φ is machine-checked to be the genuine interferometer output H · diag(1,e^{iφ}) · H · |0⟩ (ramseyVec_eq_circuit, with the corpus Hadamard QM.Gates.qmH and the same diagonal the flow uses); it has |0⟩-amplitude (1 + e^{iφ})/2, so its Born weight is ‖(1 + e^{iφ})/2‖² = (1 + cos φ)/2 = cos²(φ/2). The fringe is therefore the Malus reading (Empirical/CSD/MalusVolume.csd_malus_law) with θ = φ the accumulated phase: the |0⟩-outcome moment-sublevel region cut by [ramseyVec φ] has Fubini–Study volume cos²(φ/2), and i.i.d. FS-typicality frequencies converge to it via LF4.qubit_born_frequency_convergence_uncond. With Born = FS volume derived one layer down (the Duistermaat–Heckman / moment-map cluster, fs_moment_pushforward_uniform), this is carving-free and Gleason-free (foundational triple only, no busch_effect_gleason).

What is and is not claimed

Derived (Lean-checked, carving-free, Gleason-free). The fringe value cos²(φ/2) is the genuine Fubini–Study volume of the moment-sublevel region cut by the Ramsey output ray, and i.i.d. FS frequencies converge to it. The phase flow is a genuine Φ ≠ id, FS-measure-preserving deterministic dynamics on the probe Σ = ℂℙ¹.

Honest scope / not claimed. This is single-qubit (single-system) Ramsey. The Born = FS volume identity is imported from the DH cluster, not re-derived here; the concrete SectorData instances still carry Φ = id (this metrology phase flow runs on the projective probe space, not threaded through SectorData). The moment-region ↔ physical-detector identification is LF4-todo §14. The Quantum Fisher Information = Fubini–Study metric (A2), the Heisenberg 1/N limit (A3), and decoherence as open symplectic drift (A4) are deferred per specs/metrology-plan.md; the fringe sensitivity dP/dφ = -(sin φ)/2 here (ramsey_fringe_hasDerivAt) is the QFI precursor, with maximal slope at φ = π/2.

Experimental verification

• Ramsey 1950: Phys. Rev. 78, 695 (the method of separated oscillatory fields). The symmetric cos²(φ/2) fringe is the canonical two-pulse Ramsey signal (standard atomic-clock / interferometry references).

The Ramsey phase flow (free precession)

def CSD.Empirical.Metrology.ramseyLam : Fin 2 → ℝ

The free-precession diagonal diag(1, e^{iφ}) is the λ = (0,1) observable eigenvalue vector: obsPhase ![0,1] φ = (exp(i·φ·0), exp(i·φ·1)) = (1, e^{iφ}).

Equations

• CSD.Empirical.Metrology.ramseyLam = ![0, 1]

noncomputable def CSD.Empirical.Metrology.ramseyPhaseFlow (φ : ℝ) : LF4.CPN 2 → LF4.CPN 2

The Ramsey phase flow Φ_φ (the free-precession step): the deterministic self-map of the probe projective ontic space Σ = ℂℙ¹ given by the action of the free-precession unitary diag(1, e^{iφ}). It is the λ = ramseyLam instance of the audited diagonal-phase observable flow LF4.obsFlow; the external parameter φ(θ) = ω·t drives the flow.

Equations

• CSD.Empirical.Metrology.ramseyPhaseFlow φ = CSD.LF4.obsFlow CSD.Empirical.Metrology.ramseyLam φ

theorem CSD.Empirical.Metrology.ramseyPhaseFlow_apply (φ : ℝ) (p : LF4.CPN 2) : ramseyPhaseFlow φ p = LF4.obsUnitary ramseyLam φ • p

theorem CSD.Empirical.Metrology.ramseyPhaseFlow_measurePreserving (φ : ℝ) (p₀ : LF4.CPN 2) : MeasureTheory.MeasurePreserving (ramseyPhaseFlow φ) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

FS-invariance of the Ramsey phase flow (the Liouville / hΦ_pres content). The first metrology flow: the parameter-φ-driven free precession preserves the Fubini–Study typicality measure on the probe Σ = ℂℙ¹, so it is a physically admissible deterministic ontic dynamics in the LF1 sense. Direct from the corpus's U(2)-invariance via the diagonal-phase observable flow.

theorem CSD.Empirical.Metrology.ramseyLam_eq_obsLamWitness : ramseyLam = LF4.obsLamWitness ⋯

ramseyLam = ![0,1] is exactly the N = 2 non-triviality eigenvalue witness obsLamWitness of ObservableFlow.lean.

theorem CSD.Empirical.Metrology.ramseyPhaseFlow_ne_id : ramseyPhaseFlow Real.pi ≠ id

The Ramsey phase flow is genuinely not the identity (at φ = π, the full diag(1,-1) inversion). The computational-basis rays are fixed (they are eigenvectors of the diagonal flow), so the witness is the superposition [|0⟩+|1⟩], whose two populated coordinates acquire the distinct phases 1 and -1. This is the genuine Φ ≠ id half of the metrology flow. Reduces to the audited LF4.obsFlow_ne_id.

The Ramsey output state and its fringe amplitude

noncomputable def CSD.Empirical.Metrology.ramseyVec (φ : ℝ) : EuclideanSpace ℂ (Fin 2)

The Ramsey output state H · diag(1, e^{iφ}) · H · |0⟩, given in closed form: (1/2)·((1 + e^{iφ})|0⟩ + (1 - e^{iφ})|1⟩). That this closed form genuinely IS the interferometer circuit output is machine-checked in ramseyVec_eq_circuit (not a hand-check). Its |0⟩-amplitude is (1 + e^{iφ})/2, giving the fringe Born weight cos²(φ/2) via ramseyVec_amp_zero_sq.

Equations

• CSD.Empirical.Metrology.ramseyVec φ = EuclideanSpace.single 0 ((1 + Complex.exp (↑φ * Complex.I)) / 2) + EuclideanSpace.single 1 ((1 - Complex.exp (↑φ * Complex.I)) / 2)

theorem CSD.Empirical.Metrology.ramseyVec_ofLp_zero (φ : ℝ) : (ramseyVec φ).ofLp 0 = (1 + Complex.exp (↑φ * Complex.I)) / 2

theorem CSD.Empirical.Metrology.ramseyVec_ofLp_one (φ : ℝ) : (ramseyVec φ).ofLp 1 = (1 - Complex.exp (↑φ * Complex.I)) / 2

theorem CSD.Empirical.Metrology.exp_phase_eq (φ : ℝ) : Complex.exp (↑φ * Complex.I) = ↑(Real.cos φ) + ↑(Real.sin φ) * Complex.I

e^{iφ} = cos φ + (sin φ)·i (real/imaginary split of the free-precession phase).

theorem CSD.Empirical.Metrology.ramseyVec_amp_zero_sq (φ : ℝ) : ‖(1 + Complex.exp (↑φ * Complex.I)) / 2‖ ^ 2 = Real.cos (φ / 2) ^ 2

The fringe Born weight (cosine branch). ‖(1 + e^{iφ})/2‖² = (1 + cos φ)/2 = cos²(φ/2) — the symmetric Ramsey fringe.

theorem CSD.Empirical.Metrology.ramseyVec_amp_one_sq (φ : ℝ) : ‖(1 - Complex.exp (↑φ * Complex.I)) / 2‖ ^ 2 = Real.sin (φ / 2) ^ 2

The complementary fringe Born weight (sine branch). ‖(1 - e^{iφ})/2‖² = (1 - cos φ)/2 = sin²(φ/2) — the |1⟩ outcome.

theorem CSD.Empirical.Metrology.ramseyVec_norm (φ : ℝ) : ‖ramseyVec φ‖ = 1

theorem CSD.Empirical.Metrology.ramseyVec_ne_zero (φ : ℝ) : ramseyVec φ ≠ 0

The Ramsey output state IS the interferometer circuit H · D(φ) · H · |0⟩

noncomputable def CSD.Empirical.Metrology.ramseyD (φ : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

The free-precession diagonal D(φ) = diag(1, e^{iφ}) — the same diagonal the flow ramseyPhaseFlow uses (see ramseyD_eq_obsUnitary).

Equations

• CSD.Empirical.Metrology.ramseyD φ = Matrix.diagonal ![1, Complex.exp (↑φ * Complex.I)]

theorem CSD.Empirical.Metrology.ramseyD_eq_obsUnitary (φ : ℝ) : ramseyD φ = ↑(LF4.obsUnitary ramseyLam φ)

D(φ) is exactly the unitary generating the Ramsey phase flow: the free-precession matrix in the circuit and the generator of ramseyPhaseFlow are the same object (obsPhase ramseyLam φ = (exp(i·φ·0), exp(i·φ·1)) = (1, e^{iφ}), up to mul_comm).

theorem CSD.Empirical.Metrology.ramseyVec_eq_circuit (φ : ℝ) : ramseyVec φ = (Matrix.toEuclideanLin QM.Gates.qmH) ((Matrix.toEuclideanLin (ramseyD φ)) ((Matrix.toEuclideanLin QM.Gates.qmH) (EuclideanSpace.single 0 1)))

The Ramsey output state is the genuine interferometer circuit output, machine checked: ramseyVec φ = H · D(φ) · H · |0⟩, with H the corpus Hadamard QM.Gates.qmH = (1/√2)!![1,1;1,-1] and D(φ) = diag(1, e^{iφ}) the free-precession phase. Both output coordinates reduce (via Fin-casing) to the already-proved ramseyVec_ofLp_* amplitudes (1 ± e^{iφ})/2. This turns the docstring's H·diag·H·|0⟩ from a hand-check into a kernel-checked identity.

The Ramsey fringe as a derived Kähler volume

noncomputable def CSD.Empirical.Metrology.ramseyFringe (φ : ℝ) : ℝ

The Ramsey fringe P(|0⟩ | φ) = cos²(φ/2) (the measurement-|0⟩ probability).

Equations

• CSD.Empirical.Metrology.ramseyFringe φ = Real.cos (φ / 2) ^ 2

theorem CSD.Empirical.Metrology.ramsey_fringe_max : ramseyFringe 0 = 1

Interferometer maximum: at zero accumulated phase the fringe is 1 (constructive).

theorem CSD.Empirical.Metrology.ramsey_fringe_min : ramseyFringe Real.pi = 0

Interferometer minimum: at φ = π the fringe is 0 (destructive).

theorem CSD.Empirical.Metrology.ramsey_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 ℂ (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 ℂ (ramseyVec φ) ⋯) 0}).indicator (fun (x : Ω) => 1) ω) / ↑M) Filter.atTop (nhds (ramseyFringe φ))

The Ramsey fringe as a derived Kähler-volume frequency. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on the probe Σ = ℂℙ¹, the empirical frequency of the moment-sublevel |0⟩-outcome region cut by the Ramsey output ray [ramseyVec φ] converges almost surely to the standard symmetric Ramsey fringe cos²(φ/2) (= ramseyFringe φ).

The limit is ‖⟨e₀, ramseyVec φ⟩‖² = ‖(1 + e^{iφ})/2‖² = cos²(φ/2), with volume = Born derived from the moment map (no carving), foundational triple only (no busch_effect_gleason). The Ramsey fringe is the Malus reading (Empirical/CSD/MalusVolume.csd_malus_law) with θ = φ the accumulated phase. The identification of the region with the physical detector outcome is LF4-todo §14.

Fringe sensitivity (the QFI precursor)

theorem CSD.Empirical.Metrology.ramsey_fringe_hasDerivAt (φ : ℝ) : HasDerivAt ramseyFringe (-Real.sin φ / 2) φ

Fringe sensitivity dP/dφ = -(sin φ)/2 (the slope of cos²(φ/2)). The maximal-sensitivity operating point is φ = π/2, where |dP/dφ| = 1/2 (ramsey_sensitivity_at_quadrature). This is the precursor to the Quantum Fisher Information = Fubini–Study metric statement (A2), deferred per specs/metrology-plan.md.

theorem CSD.Empirical.Metrology.ramsey_sensitivity_at_quadrature : -Real.sin (Real.pi / 2) / 2 = -(1 / 2)

The fringe slope is maximal in magnitude at quadrature φ = π/2: dP/dφ = -1/2.