LF3 Singlet / Kernel: pointer-sector kernel, correlation, marginals #
Category: 3-Local (LF3 algebraic core: P_st, cAmp, cst_squared_eq, correlation, marginals, no-signalling).
Paper §6 / §7.
The algebraic core: ‖c_{st}(a,b)‖² = (1 − st · a·b) / 4 (spec §9.8 calls
this "the algebraic core of LF3"). Together with the strong-readout pointer
probability P_{st}, the singlet correlation −a·b, the marginal identities
= 1/2, and the operational no-signalling consequences, these supply the
content of LF3_main_theorem.
cAmp is defined in closed form via Real.sqrt ((1 − st a·b)/4). This
sidesteps the explicit construction of joint spin eigenstates |s_a, t_b⟩
(which require either a parametric spectral decomposition or a unit
eigenvector of jointSpinProj); the squared-amplitude content ‖cAmp‖² = (1 − st a·b)/4 is preserved exactly. A future v2 may swap the closed-form
definition for cAmp := inner ℂ jointSpinEig singlet once the eigenstate
construction is added; downstream theorems consume only ‖cAmp‖², so the
swap is transparent.
The pointer-sector probability P_{st}(a, b) = (1 − st · a·b) / 4
(paper §6.9, spec §9.8).
Equations
- CSD.LF3.P_st a b s t = (1 - s.val * t.val * CSD.LF3.dotR a b) / 4
Instances For
For unit vectors, |a · b| ≤ 1. Cauchy–Schwarz: identify dotR with the
real inner product on EuclideanSpace ℝ (Fin 3) (the equality is rfl
up to the ofLp and star_trivial reductions), then apply
abs_real_inner_le_norm with the unit-norm hypotheses.
The pointer-sector probability is non-negative (needed to take Real.sqrt).
Singlet amplitude (closed form) #
The singlet amplitude c_{st}(a, b), defined in closed form as the real
square root of P_{st}(a, b). This is one canonical representative of
the bra-ket form ⟨s_a, t_b | ψ⁻⟩; only ‖cAmp‖² is consumed downstream
(in sectorVolume_strong_readout and the LF1↔LF2↔LF3 chain).
Equations
- CSD.LF3.cAmp a b s t = ↑√(CSD.LF3.P_st a b s t)
Instances For
The algebraic core of LF3 (paper §6.9, spec §9.8):
‖c_{st}(a,b)‖² = (1 − st · a·b) / 4.
Born-form equivalence (paper §6.11) #
The closed-form cAmp = √P_st is a real-valued representative of the
physical complex amplitude ⟨s_a, t_b | ψ⁻⟩. The Born-form fidelity claim is
that this representative agrees with the genuine bra-ket inner product
⟨v, ψ⁻⟩ on its squared norm, whenever v : EuclideanSpace ℂ (Fin 2 × Fin 2) is an actual joint spin eigenstate |s_a, t_b⟩. The equivalence is
expressed as a hypothesis on ‖inner ℂ v singlet‖² = P_st a b s t; in a v2
with a constructed jointSpinEig, this hypothesis discharges from the
rank-1 projector identity jointSpinProj = |v⟩⟨v|.
Closed-form / bra-ket equivalence. If v : EuclideanSpace ℂ (Fin 2 × Fin 2) is a vector whose bra-ket inner product with the singlet has
squared norm equal to P_{st}(a, b), then ‖cAmp s t (a, b)‖² = ‖⟨v, ψ⁻⟩‖². The hypothesis h_inner is the inner-product-norm equality that
a rank-1 projector identity jointSpinProj = |v⟩⟨v| would entail (via a
spectral argument); the theorem here consumes that conclusion directly.
A v2 construction of jointSpinEig from the spectral decomposition of
jointSpinProj would discharge h_inner automatically.
Correlation and marginals (paper §6.10 / §7.3) #
Singlet A-side marginal at the strong-readout limit: ∑_t P_{st} = 1/2. Two-term sum, 1/2 for each sign.
Singlet B-side marginal at the strong-readout limit.
No-signalling corollaries (paper §7.10) #
No-signalling, strong-readout, A side. Alice's marginal is independent of Bob's setting.
No-signalling, strong-readout, B side. Bob's marginal is independent of Alice's setting.
Bridge to the abstract layer (paper §6.11) #
The strong-readout sector volume at the singlet equals the singlet kernel
P_{st}(a, b). Composes sectorVolume_strong_readout (operator-level
sector volume on a StrongReadoutCompat-equipped projector algebra and
measurement unitary) with cst_squared_eq (the closed-form algebraic
core for the singlet amplitude).