Empirical/Metrology A3: the Heisenberg limit (1/N scaling) via the GHZ probe

Category: 3-Local (QM-validity metrology layer; reuses the A2 Quantum-Fisher- Information machinery, no CSD ontology beyond the A1/A2 lineage).

This is item A3 of specs/metrology-plan.md: the Heisenberg-limit comparison. N qubits used as one entangled GHZ probe carry N times the metrological information of N qubits used as N independent (separable) Ramsey probes, both accumulating the same phase φ.

The GHZ probe (this file's Lean content)

The phase-accumulated GHZ state on a genuine N-qubit carrier EuclideanSpace ℂ (Fin (2^N)) is ψ_N(φ) = (1/√2)(|0…0⟩ + e^{iNφ}|1…1⟩), with |0…0⟩ the all-zeros index 0 and |1…1⟩ the all-ones index 2^N − 1. All N qubits flip together, so the collective phase is Nφ; only two components are nonzero (ghzPhaseVec). It is genuinely normalized (ghzPhaseVec_norm, for N ≥ 1; the A2 fsMetric/qfi definitions are faithful only for unit ψ). Its genuine derivative (only the all-ones component varies) is certified by ghzPhaseVec_hasDerivAt via the chain rule on φ ↦ exp((N·φ:ℂ)·I) assembled through the ℝ-linear CLM ghzSingleRL (mirroring A2's singleRL/ramseyVec_hasDerivAt; it is proved, not asserted). Then:

• ‖dψ_N‖² = N²/2, ⟪ψ_N, dψ_N⟫ = i·N/2, so ‖⟪ψ_N,dψ_N⟫‖² = N²/4;
• g = N²/2 − N²/4 = N²/4, hence F_Q^GHZ = 4·(N²/4) = N² (ghz_qfi) — the Heisenberg quadratic enhancement. The N² comes from the phase being Nφ, not from the carrier dimension.

SQL (separable) probe and the Heisenberg advantage

N independent Ramsey probes each have F_Q = 1 (A2's ramsey_qfi). The (classical / quantum) Fisher information is additive over independent probes, so F_Q^SQL = N·1 = N (sqlQFI; the additivity is the standard fact, with A2's per-probe ramsey_qfi = 1 the input — see the sqlQFI docstring). Therefore F_Q^GHZ / F_Q^SQL = N²/N = N (heisenberg_advantage: N² = N·N; ghz_qfi_div_sql): the N-fold metrological enhancement. Operationally, the quantum Cramér-Rao bound Var(φ̂) ≥ 1/(n·F_Q) over n shots gives precision scaling 1/N² (Heisenberg, standard deviation 1/N) for the GHZ probe versus 1/N (SQL, standard deviation 1/√N) for the separable probes.

What is and is not modelled

ghzPhaseVec is the N-qubit GHZ-phase family and ghzDeriv its derivative vector; ghz_qfi is the geometric Quantum Fisher Information of that family (the A2 trajectory pullback of the Fubini-Study metric). The dynamical N-body interaction that prepares the GHZ state, and the physical phase-imprinting Hamiltonian, are not modelled (as in A2: this is the QFI of the state family, single parameter φ). F_Q^GHZ = N² is the Heisenberg limit and F_Q^SQL = N the standard quantum limit. This reuses A2's fsMetric/qfi/singleRL idiom verbatim, so the A2 metric infrastructure genuinely generalizes from the qubit to the N-qubit entangled probe. QM-validity layer; the CSD content is the A1/A2 metrology lineage.

The GHZ carrier indices: all-zeros 0 and all-ones 2^N − 1

def CSD.Empirical.Metrology.ghzZero (N : ℕ) : Fin (2 ^ N)

The all-zeros computational-basis index |0…0⟩ of the N-qubit carrier EuclideanSpace ℂ (Fin (2^N)), i.e. 0 : Fin (2^N).

Equations

• CSD.Empirical.Metrology.ghzZero N = ⟨0, ⋯⟩

def CSD.Empirical.Metrology.ghzOne (N : ℕ) : Fin (2 ^ N)

The all-ones computational-basis index |1…1⟩ of the N-qubit carrier, i.e. the top index 2^N − 1 : Fin (2^N) (the binary all-ones bitstring).

Equations

• CSD.Empirical.Metrology.ghzOne N = ⟨2 ^ N - 1, ⋯⟩

theorem CSD.Empirical.Metrology.ghzZero_ne_ghzOne {N : ℕ} (hN : 1 ≤ N) : ghzZero N ≠ ghzOne N

The all-zeros and all-ones indices are distinct for a genuine N-qubit system (N ≥ 1), since then 2^N ≥ 2.

The phase-accumulated GHZ state and its derivative vector

noncomputable def CSD.Empirical.Metrology.ghzPhaseVec (N : ℕ) (φ : ℝ) : EuclideanSpace ℂ (Fin (2 ^ N))

The phase-accumulated GHZ state ψ_N(φ) = (1/√2)(|0…0⟩ + e^{iNφ}|1…1⟩) on the genuine N-qubit carrier EuclideanSpace ℂ (Fin (2^N)). Only the all-zeros (ghzZero) and all-ones (ghzOne) components are nonzero; the collective phase Nφ reflects all N qubits flipping together.

Equations

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

noncomputable def CSD.Empirical.Metrology.ghzDeriv (N : ℕ) (φ : ℝ) : EuclideanSpace ℂ (Fin (2 ^ N))

The GHZ derivative vector dψ_N(φ) = (i·N·e^{iNφ}/√2)·|1…1⟩: only the all-ones component varies with φ. Certified to be the genuine derivative of ghzPhaseVec in ghzPhaseVec_hasDerivAt.

Equations

• CSD.Empirical.Metrology.ghzDeriv N φ = EuclideanSpace.single (CSD.Empirical.Metrology.ghzOne N) (↑(1 / √2) * (Complex.exp (↑N * ↑φ * Complex.I) * (↑N * Complex.I)))

Normalisation

theorem CSD.Empirical.Metrology.norm_exp_phase_N (N : ℕ) (φ : ℝ) : ‖Complex.exp (↑N * ↑φ * Complex.I)‖ = 1

‖e^{iNφ}‖ = 1.

theorem CSD.Empirical.Metrology.ghzPhaseVec_norm (N : ℕ) (hN : 1 ≤ N) (φ : ℝ) : ‖ghzPhaseVec N φ‖ = 1

‖ghzPhaseVec N φ‖ = 1 for N ≥ 1: the two nonzero components each have squared modulus 1/2. Load-bearing: the A2 fsMetric/qfi definitions are faithful only for a normalized state.

The genuine derivative

noncomputable def CSD.Empirical.Metrology.ghzSingleRL {N : ℕ} (i : Fin (2 ^ N)) : ℂ →L[ℝ] EuclideanSpace ℂ (Fin (2 ^ N))

EuclideanSpace.single i, packaged as an ℝ-linear continuous map. Built ℝ-linear from the start so composing the ℝ-valued HasDerivAt of a scalar trajectory with it needs no restrictScalars (which triggers the ℝ-ℂ-EuclideanSpace module diamond). The Fin (2^N)-indexed analogue of A2's singleRL.

Equations

• CSD.Empirical.Metrology.ghzSingleRL i = LinearMap.toContinuousLinearMap { toFun := EuclideanSpace.single i, map_add' := ⋯, map_smul' := ⋯ }

theorem CSD.Empirical.Metrology.hasDerivAt_ghzSingle {N : ℕ} (i : Fin (2 ^ N)) {a : ℝ → ℂ} {a' : ℂ} {φ : ℝ} (h : HasDerivAt a a' φ) : HasDerivAt (fun (φ : ℝ) => EuclideanSpace.single i (a φ)) (EuclideanSpace.single i a') φ

Componentwise lift: a scalar HasDerivAt a a' φ lifts to a vector HasDerivAt of the single-supported vector, via ghzSingleRL. The Fin (2^N) analogue of A2's hasDerivAt_single.

theorem CSD.Empirical.Metrology.ghzPhaseVec_hasDerivAt (N : ℕ) (φ : ℝ) : HasDerivAt (ghzPhaseVec N) (ghzDeriv N φ) φ

ghzDeriv is the genuine derivative of ghzPhaseVec. The all-zeros component is constant; the all-ones component φ ↦ e^{iNφ}/√2 has derivative i·N·e^{iNφ}/√2, proved via the chain rule HasDerivAt.cexp on φ ↦ exp((N·φ:ℂ)·I) and assembled through ghzSingleRL. This earns the "derivative" label; it is not asserted. Mirrors A2's ramseyVec_hasDerivAt.

The headline Heisenberg QFI: F_Q^GHZ = N²

theorem CSD.Empirical.Metrology.ghzDeriv_normSq (N : ℕ) (φ : ℝ) : ‖ghzDeriv N φ‖ ^ 2 = ↑N ^ 2 / 2

‖dψ_N‖² = N²/2 for the GHZ derivative vector.

theorem CSD.Empirical.Metrology.ghz_inner (N : ℕ) (hN : 1 ≤ N) (φ : ℝ) : inner ℂ (ghzPhaseVec N φ) (ghzDeriv N φ) = ↑N * Complex.I / 2

⟪ψ_N, dψ_N⟫ = i·N/2 for the GHZ state and its derivative. The cross term collapses via e^{iNφ}·conj(e^{iNφ}) = 1.

theorem CSD.Empirical.Metrology.ghz_qfi (N : ℕ) (hN : 1 ≤ N) (φ : ℝ) : qfi (ghzPhaseVec N φ) (ghzDeriv N φ) = ↑N ^ 2

The GHZ Quantum Fisher Information F_Q^GHZ = N² (the Heisenberg limit). With ‖dψ‖² = N²/2 and ‖⟪ψ,dψ⟫‖² = N²/4: g = N²/4, so F_Q = 4·(N²/4) = N². The N² is the quadratic enhancement carried by the collective phase Nφ.

The SQL (separable) probe and the Heisenberg advantage

def CSD.Empirical.Metrology.sqlQFI (N : ℕ) : ℝ

The standard-quantum-limit QFI F_Q^SQL = N. N independent Ramsey probes, each with per-probe F_Q = 1 (A2's ramsey_qfi); the (classical/quantum) Fisher information is additive over independent probes, so F_Q^SQL = N·1 = N. (Additivity is the standard fact for independent probes; the per-probe input is A2's ramsey_qfi = 1. We record the value N rather than re-deriving general tensor-product QFI additivity.)

Equations

• CSD.Empirical.Metrology.sqlQFI N = ↑N * 1

@[simp]

theorem CSD.Empirical.Metrology.sqlQFI_eq (N : ℕ) : sqlQFI N = ↑N

F_Q^SQL = N.

theorem CSD.Empirical.Metrology.heisenberg_advantage (N : ℕ) (hN : 1 ≤ N) (φ : ℝ) : qfi (ghzPhaseVec N φ) (ghzDeriv N φ) = ↑N * sqlQFI N

The Heisenberg advantage: F_Q^GHZ = N · F_Q^SQL (i.e. N² = N·N), the N-fold metrological enhancement. The entangled GHZ probe carries N times the per-shot information of the N separable probes.

theorem CSD.Empirical.Metrology.ghz_qfi_div_sql (N : ℕ) (hN : 1 ≤ N) (φ : ℝ) : qfi (ghzPhaseVec N φ) (ghzDeriv N φ) / sqlQFI N = ↑N

The Heisenberg enhancement ratio F_Q^GHZ / F_Q^SQL = N (for N ≥ 1). Operationally: precision Var(φ̂) ≥ 1/(n·F_Q) scales as 1/N² (Heisenberg) for the GHZ probe versus 1/N (SQL) for the separable probes.