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 epistemic typicality measure of a global basin on the fibred ontic Σ = ℂℙ³ × T²: 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.

⚠️ Since the CR-4 migration the headlines no longer need that — they route through the unconditional fibred engine, which has no hpos at all. hardyVolVec_hpos is kept anyway, and kept deliberately: it certifies that the Hardy instance was never a boundary case, so the move to the fibred arena is not quietly dodging one. It has no consumer, and that is the point.

What is and is not claimed

Derived (carving-free, Gleason-free, unconditional). The four Born weights are the genuine typicality measures of the global basins on the fibred Σ = ℂℙ³ × T², and i.i.d. trials over that law 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).

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 the base-side born_frequency_convergence_N applies with no boundary carve-out.

⚠️ Deliberately consumer-free since the CR-4 migration. The headlines now use the fibred engine, which carries no genericity hypothesis, so nothing needs this. It is retained as the record that the Hardy instance is an interior point — evidence that the fibred route was not chosen to avoid a boundary case here.

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 epistemic typicality measure on the fibred ontic Σ = ℂℙ³ × T² (via born_value_zero + QM/Hardy.lean's hardyMax_value).

theorem CSD.Empirical.CSDBridge.HardyVolume.hardy_max_born_frequency_volume {Ω : Type u_1} [MeasurableSpace Ω] {Pr : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure Pr] (X : ℕ → Ω → LF4.KSigma 4) (hX : ∀ (n : ℕ), Measurable (X n)) (hlaw : ∀ (n : ℕ), MeasureTheory.Measure.map (X n) Pr = RecordLayer.epistemicMeasure (Projectivization.mk ℂ hardyVolVec hardyVolVec_ne_zero)) (hindep : ∀ (i : Fin 4), Pairwise (Function.onFun (fun (f g : Ω → ℝ) => ProbabilityTheory.IndepFun f g Pr) fun (n : ℕ) => (X n ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 4) i).indicator fun (x : Ω) => 1)) : ∀ᵐ (ω : Ω) ∂Pr, ∀ (i : Fin 4), Filter.Tendsto (fun (m : ℕ) => (∑ k ∈ Finset.range m, (X k ⁻¹' RecordLayer.globalBasin (RecordLayer.momentContext 4) 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 epistemic typicality measure on the fibred ontic Σ = ℂℙ³ × T², the empirical frequencies of the four global basins 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.