LF4 Hardy LF3-chain lift (Phase A — state and ray) #
Category: 3-Local (LF4 §14 chain lift on the Hardy state).
Constructs the Hardy state |ψ⟩ = (1/√12)(|00⟩ + |01⟩ + |10⟩ − 3|11⟩) as
a unit vector in EuclideanSpace ℂ (Fin 4), and its projective ray
hardyRay ∈ ℂℙ³. This is Phase A of the four-phase Hardy LF3-chain
lift (see plan).
The Hardy state is the canonical non-maximally-entangled 2-qubit state
that exhibits the four Hardy probability constraints P(A=1,B=1) = 1/12 > 0,
P(A=1,B'=−1) = P(A'=−1,B=1) = P(A'=1,B'=1) = 0 under the QM choice of
Pauli axes A=B=Z, A'=B'=X (Hardy 1992). The unnormalised version
hardyVec : Fin 2 × Fin 2 → ℂ and the four amplitude theorems
(hardyAmp_AB, hardyAmp_A_B'minus, hardyAmp_A'minus_B,
hardyAmp_A'_B') live in Empirical/QM/Hardy.lean.
This phase delivers only the state/ray geometry; Phases B–D add the fibre measure, outcome regions, and the four frequency-convergence capstones.
Source #
- Hardy 1992 Phys. Rev. Lett. 68, 2981 (the canonical Hardy state).
- The unnormalised
hardyVecis defined inEmpirical/QM/Hardy.leanas|00⟩ + |01⟩ + |10⟩ − 3|11⟩; this module reindexes it fromFin 2 × Fin 2 → ℂtoEuclideanSpace ℂ (Fin 4)(via the existingkReindexisometry fromSingletKahler.lean) and normalises.
The unnormalised Hardy state in EuclideanSpace ℂ (Fin 2 × Fin 2) #
The Hardy state |00⟩ + |01⟩ + |10⟩ − 3|11⟩ as an unnormalised vector
in EuclideanSpace ℂ (Fin 2 × Fin 2).
Equations
- CSD.LF4.hardyVecE = EuclideanSpace.single (0, 0) 1 + EuclideanSpace.single (0, 1) 1 + EuclideanSpace.single (1, 0) 1 + EuclideanSpace.single (1, 1) (-3)
Instances For
The normalised Hardy state in EuclideanSpace ℂ (Fin 4) #
The Hardy state (1/√12) · (|00⟩ + |01⟩ + |10⟩ − 3|11⟩), re-indexed
into EuclideanSpace ℂ (Fin 4) via kReindex. Unit norm.
Equations
Instances For
The projective ray of the Hardy state, [hardyPsi] ∈ ℂℙ³.
Instances For
Phase B: fibre measure, outcome regions, carving identities #
Hardy posited fibre law #
hardyMuPsi := δ_{[hardyPsi]} ⊗ vol_{T²} — the Hardy preparation on the
non-trivial-fibre compact-Kähler instance. Pushes through π = pr₁ to
δ_{hardyRay}, parallel to kMuPsi for the singlet.
The Hardy posited fibre law on Σ = ℂℙ³ × T².
Equations
Instances For
Generic torus-fibre outcome region #
A torus-fibre arc outcome region of measure v for v ∈ [0, 1].
Generalises sgRegion and the singlet kRegion pattern to a single
helper, used by all four Hardy outcome regions below.
Generic torus-fibre outcome region of measure v.
Equations
Instances For
Carving identity. μψ(hardyFibreRegion v) = ENNReal.ofReal v for
v ∈ [0, 1]. Same shape as sgMuPsi_sgRegion and kMuPsi_kRegion.
The four Hardy Born values #
The QM-predicted joint probabilities for the four Hardy-constraint
contexts on the Hardy state. Computed from the QM-side hardyAmp_*
theorems after squaring and dividing by the joint norm products
(amplitudes ∈ ℤ; norms² = 12, 24, 24, 24 for ‖ψ‖²·‖a‖²·‖b‖²).
P(A=+1, B=+1) on the Hardy state: 1/12 (positive coincidence).
Equations
- CSD.LF4.hardyBorn_AB = 1 / 12
Instances For
P(A=+1, B'=−1) on the Hardy state: 0.
Equations
Instances For
P(A'=−1, B=+1) on the Hardy state: 0.
Equations
Instances For
P(A'=+1, B'=+1) on the Hardy state: 0 (the load-bearing zero
that drives no_lhv_hardy).
Equations
Instances For
The four Hardy outcome regions #
Outcome region for (A=+1, B=+1): a fibre arc of measure 1/12.
Instances For
Outcome region for (A=+1, B'=−1): measure 0 (the QM-forbidden
outcome).
Instances For
Outcome region for (A'=−1, B=+1): measure 0.
Instances For
Outcome region for (A'=+1, B'=+1): measure 0.
Instances For
The four carving identities #
μψ(R_{AB}) = 1/12.
μψ(R_{A,B'−}) = 0.
μψ(R_{A'−,B}) = 0.
μψ(R_{A',B'}) = 0.
Phase C: Hardy LF3-chain frequency-convergence capstones #
For i.i.d. trials with law hardyMuPsi (the Hardy preparation on the
non-trivial-fibre compact-Kähler instance), the empirical frequency of
each Hardy outcome region converges almost surely to the QM-predicted
Born value. Four corollaries — one per Hardy constraint — composed from
a single parametric helper hardy_freq_convergence.
Parallel to sg_frequency_convergence (single-qubit case) and
ofKählerPreparation_singlet_frequency_convergence (singlet case).
Foundational triple only.
Parametric Hardy frequency-convergence helper. For any
v ∈ [0, 1], i.i.d. trials with law hardyMuPsi have empirical
frequency of hardyFibreRegion v converging a.s. to v.
Hardy chain capstone 1: empirical frequency of (A=+1, B=+1)
converges to 1/12 (the positive Hardy coincidence).
Hardy chain capstone 2: empirical frequency of (A=+1, B'=−1)
converges to 0 (QM-forbidden outcome).
Hardy chain capstone 3: empirical frequency of (A'=−1, B=+1)
converges to 0.
Hardy chain capstone 4: empirical frequency of (A'=+1, B'=+1)
converges to 0 (the load-bearing QM-forbidden outcome that drives
no_lhv_hardy).
Phase E: QM ↔ LF4 amplitude loop — Hilbert Born identities #
Closes the loop between the posited Hardy Born values (1/12, 0, 0, 0) and
the Hilbert quantities ‖⟨hardyPsi, |a ⊗ b⟩‖² for the four Hardy joint
outcomes. Each Hardy Born value is shown to equal a Hilbert inner-product
squared, by direct entry computation through hardyVecE_ofLp_* and
LinearIsometryEquiv.inner_map_map (the kReindex transport).
The four joint outcome vectors are the QM Empirical/QM/Hardy.lean
zPlus, xPlus, xMinus (single-qubit eigenstates of Z and X) tensored
and normalised:
| Outcome | Joint state (unnormalised) | Normalisation |
|---|---|---|
(A=+1, B=+1) | |00⟩ | 1 (already unit) |
(A=+1, B'=−1) | |0⟩ ⊗ (−|0⟩ + |1⟩) | 1/√2 |
(A'=−1, B=+1) | (−|0⟩ + |1⟩) ⊗ |0⟩ | 1/√2 |
(A'=+1, B'=+1) | (|0⟩ + |1⟩) ⊗ (|0⟩ + |1⟩) | 1/2 |
These are re-indexed via kReindex from EuclideanSpace ℂ (Fin 2 × Fin 2)
to EuclideanSpace ℂ (Fin 4), matching hardyPsi.
The four Born identities use the explicit hardyVecE entries
(1, 1, 1, −3); the algebra agrees with the QM-side hardyAmp_*
theorems (= 1, 0, 0, 0 for the unnormalised amplitudes; after
normalisation ‖inner‖² = 1/12, 0, 0, 0 matching hardyBorn_*).
Four Hardy joint outcome vectors #
Joint outcome |0⟩ ⊗ (1/√2)(−|0⟩ + |1⟩) = (1/√2)(−|00⟩ + |01⟩).
Equations
- CSD.LF4.hardyOutcome_AB'minus = (↑√2)⁻¹ • CSD.LF4.kReindex (-EuclideanSpace.single (0, 0) 1 + EuclideanSpace.single (0, 1) 1)
Instances For
Joint outcome (1/√2)(−|0⟩ + |1⟩) ⊗ |0⟩ = (1/√2)(−|00⟩ + |10⟩).
Equations
Instances For
Joint outcome (1/√2)(|0⟩+|1⟩) ⊗ (1/√2)(|0⟩+|1⟩) = (1/2)(|00⟩+|01⟩+|10⟩+|11⟩)`.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Four Hilbert Born identities #
Each ‖⟨hardyPsi, hardyOutcome_*⟩‖² = hardyBorn_* by direct computation.
The inner product on EuclideanSpace ℂ (Fin 4) reduces (via kReindex
isometry transport) to an inner product on EuclideanSpace ℂ (Fin 2 × Fin 2),
which is a sum of hardyVecE's explicit entries against the joint
outcome's EuclideanSpace.single components.
Helper: inner ℂ hardyVecE (single i 1) = star (hardyVecE.ofLp i),
giving the four explicit values via the entry lemmas.
Helper: star ((√12 : ℂ)⁻¹) = (√12 : ℂ)⁻¹ (real number is self-conjugate).
Hardy Hilbert Born identity 1: ‖⟨hardyPsi, |00⟩⟩‖² = 1/12 (the
positive coincidence).
Hardy Hilbert Born identity 2: ‖⟨hardyPsi, |0⟩⊗(−|0⟩+|1⟩)/√2⟩‖² = 0.
Hardy Hilbert Born identity 3: ‖⟨hardyPsi, (−|0⟩+|1⟩)/√2 ⊗ |0⟩⟩‖² = 0.
Hardy Hilbert Born identity 4 (load-bearing): ‖⟨hardyPsi, |++⟩⟩‖² = 0.
Uses all four hardyVecE entries (1, 1, 1, −3); sum 1 + 1 + 1 − 3 = 0.
Full §14 observable correspondence for the four Hardy outcomes #
Composing the Hilbert Born identities (Phase E above) with the carving identities (Phase B), each Hardy Born value equals both the Hilbert inner-product squared and the ontic measure of the carved outcome region. The §14 correspondence for Hardy at the projector level.
Hardy §14 observable correspondence (A=+1, B=+1).
Hardy §14 observable correspondence (A=+1, B'=−1).
Hardy §14 observable correspondence (A'=−1, B=+1).
Hardy §14 observable correspondence (A'=+1, B'=+1). The load-bearing zero.