Empirical/CSD: Hardy's probability as a derived Kähler-volume frequency

Category: 3-Local (CSD-ontic layer; genuine volume derivation, not a transport tag, and not conditional on any preparation bundle).

The two-qubit (N = 4) surfacing of LF4.born_frequency_convergence_N for the Hardy state at the golden-ratio maximum, in the spirit of Empirical/CSD/BellVolume.lean and Empirical/CSD/GHZVolume.lean.

What this adds over the QM layer

Empirical/QM/Hardy.lean closes the Hardy paradox: no LHV distribution satisfies the four Hardy constraints (no_lhv_hardy), QM realises them (exists_hardy_realisation_max), and the maximal Hardy probability is the closed-form (5√5 − 11)/2 ≈ 9.017 % (hardyMax_probability_eq). That number is an inner-product Born value. This file derives the same number as a genuine Fubini–Study typicality volume on the ontic Σ = ℂℙ³: carving-free, Gleason-free, unconditional.

The interior-point property (no boundary obstruction)

Unlike the GHZ state — a stabiliser state that is sparse in its Mermin bases and therefore a boundary point of the probability simplex (GHZVolume.lean) — the golden-ratio Hardy state

|ψ_max⟩ ∝ |00⟩ + √φ |01⟩ + √φ |10⟩ − φ² |11⟩       (φ = (1+√5)/2)

has all four computational-basis amplitudes nonzero. Its Born weights

P_00 = 1/(5φ+3) = (5√5−11)/2,   P_01 = P_10 = φ/(5φ+3),   P_11 = φ⁴/(5φ+3),

are all strictly positive, so the Hardy state is an interior point of the 3-simplex and the genericity hypothesis hpos of born_frequency_convergence_N holds outright — no Φ ∈ (0,π) carve-out is needed, the full Hardy instance is covered. P_00 is exactly the Hardy probability the experiment measures.

What is and is not claimed

Derived (carving-free, Gleason-free, unconditional). The four Born weights are the genuine Fubini–Study volumes of the barycentric moment regions on ℂℙ³, and i.i.d. FS trials have frequencies converging a.s. to them. In particular the Hardy probability (5√5 − 11)/2 is a Kähler volume. No busch_effect_gleason, no carving, no preparation bundle.

Not claimed. (i) The closed-form amplitudes are the physics input (cf. LF3 cAmp, BellVolume); identifying hardyVolVec with the abstract Hardy state in the computational basis is the amplitude identity, supplied by construction — the amplitudes here are exactly those of QM/Hardy.lean's hardyMaxVec, normalised. (ii) Region → physical-outcome labelling is LF4-todo §14. The LHV impossibility itself lives in QM/Hardy.lean.

Experimental verification

• Hardy 1993: Phys. Rev. Lett. 71, 1665; Lundeen, Steinberg 2009: Phys. Rev. Lett. 102, 020404 (weak-measurement confirmation).

Helpers (file-local, mirroring GHZVolume.lean)

theorem CSD.Empirical.CSDBridge.HardyVolume.normSq_inner_single (ψ : EuclideanSpace ℂ (Fin 4)) (i : Fin 4) : ‖inner ℂ (EuclideanSpace.single i 1) ψ‖ ^ 2 = ‖ψ.ofLp i‖ ^ 2

‖⟨eᵢ, ψ⟩‖² = ‖ψᵢ‖² on ℂℙ³.

theorem CSD.Empirical.CSDBridge.HardyVolume.realNormSq (r : ℝ) : ‖↑r‖ ^ 2 = r ^ 2

‖↑r‖² = r².

The normalising constant nrm = √(5φ+3)

theorem CSD.Empirical.CSDBridge.HardyVolume.denom_pos : 0 < 5 * Hardy.HardyQMMax.phi + 3

5φ + 3 > 0 (the squared norm of the golden-ratio Hardy state).

noncomputable def CSD.Empirical.CSDBridge.HardyVolume.nrm : ℝ

The normalisation nrm = √(5φ+3) = ‖ψ_max‖.

Equations

• CSD.Empirical.CSDBridge.HardyVolume.nrm = √(5 * CSD.Empirical.Hardy.HardyQMMax.phi + 3)

theorem CSD.Empirical.CSDBridge.HardyVolume.nrm_pos : 0 < nrm

theorem CSD.Empirical.CSDBridge.HardyVolume.nrm_sq : nrm ^ 2 = 5 * Hardy.HardyQMMax.phi + 3

The normalised golden-ratio Hardy state on ℂℙ³

noncomputable def CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec : EuclideanSpace ℂ (Fin 4)

The golden-ratio Hardy state, normalised onto Fin 4 ↔ (Fin 2 × Fin 2): amplitudes (1, √φ, √φ, −φ²)/√(5φ+3). These are exactly the amplitudes of QM/Hardy.lean's hardyMaxVec, divided by ‖ψ_max‖ = √(5φ+3).

Equations

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

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_ofLp_zero : hardyVolVec.ofLp 0 = ↑(1 / nrm)

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_ofLp_one : hardyVolVec.ofLp 1 = ↑(Hardy.HardyQMMax.sqrtPhi / nrm)

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_ofLp_two : hardyVolVec.ofLp 2 = ↑(Hardy.HardyQMMax.sqrtPhi / nrm)

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_ofLp_three : hardyVolVec.ofLp 3 = ↑(-Hardy.HardyQMMax.phi ^ 2 / nrm)

The four Born weights

theorem CSD.Empirical.CSDBridge.HardyVolume.born_value_zero : ‖inner ℂ (EuclideanSpace.single 0 1) hardyVolVec‖ ^ 2 = 1 / (5 * Hardy.HardyQMMax.phi + 3)

theorem CSD.Empirical.CSDBridge.HardyVolume.born_value_one : ‖inner ℂ (EuclideanSpace.single 1 1) hardyVolVec‖ ^ 2 = Hardy.HardyQMMax.phi / (5 * Hardy.HardyQMMax.phi + 3)

theorem CSD.Empirical.CSDBridge.HardyVolume.born_value_two : ‖inner ℂ (EuclideanSpace.single 2 1) hardyVolVec‖ ^ 2 = Hardy.HardyQMMax.phi / (5 * Hardy.HardyQMMax.phi + 3)

theorem CSD.Empirical.CSDBridge.HardyVolume.born_value_three : ‖inner ℂ (EuclideanSpace.single 3 1) hardyVolVec‖ ^ 2 = (Hardy.HardyQMMax.phi ^ 2) ^ 2 / (5 * Hardy.HardyQMMax.phi + 3)

Norm, non-vanishing, genericity

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_norm : ‖hardyVolVec‖ = 1

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_ne_zero : hardyVolVec ≠ 0

theorem CSD.Empirical.CSDBridge.HardyVolume.hardyVolVec_hpos (j : Fin 4) : 0 < ‖inner ℂ (EuclideanSpace.single j 1) hardyVolVec‖ ^ 2

Genericity: all four Born weights are strictly positive (the Hardy state is an interior point of the 3-simplex), so born_frequency_convergence_N applies with no boundary carve-out.

The Hardy volume-frequency capstone

theorem CSD.Empirical.CSDBridge.HardyVolume.hardy_max_volume_probability : ‖inner ℂ (EuclideanSpace.single 0 1) hardyVolVec‖ ^ 2 = (5 * √5 - 11) / 2

Hardy's maximal probability as a derived Kähler volume. The |00⟩ computational-basis Born weight of the golden-ratio Hardy state — the quantity the Hardy experiment measures — equals the closed-form maximum (5√5 − 11)/2 ≈ 9.017 %, here obtained as a genuine Fubini–Study typicality volume on the ontic Σ = ℂℙ³ (via born_value_zero + QM/Hardy.lean's hardyMax_value).

theorem CSD.Empirical.CSDBridge.HardyVolume.hardy_max_born_frequency_volume (p₀ : LF4.CPN 4) {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.CPN 4) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = Matrix.UnitaryGroup.fubiniStudyMeasure p₀) (hindep : ∀ (i : Fin 4), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' LF4.bornRegion hardyVolVec hardyVolVec_ne_zero i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' LF4.bornRegion hardyVolVec hardyVolVec_ne_zero i).indicator (fun (x : Ω) => 1) ω) / ↑m) Filter.atTop (nhds (‖inner ℂ (EuclideanSpace.single i 1) hardyVolVec‖ ^ 2))

CSD Hardy joint frequencies as derived Kähler-volume convergence. For i.i.d. trials drawing microstates from the Fubini–Study typicality measure on the ontic Σ = ℂℙ³, the empirical frequencies of the four barycentric Born outcome regions converge, on a single almost-sure event, to the golden-ratio Hardy state's joint Born weights ‖⟨eᵢ, hardyVolVec⟩‖² — the i = 0 coordinate of which is Hardy's maximal probability (5√5 − 11)/2 (hardy_max_volume_probability).

Carving-free, Gleason-free, unconditional — no busch_effect_gleason, no carved regions, no preparation bundle. The amplitude values are the physics input; the volume = Born number step is derived.