Kernel-checked entanglement package on the bipartite matrix algebra
(2×2 ⊗ 2×2, native product index — three statements at arbitrary
finite local dimensions), in Lean 4 + Mathlib. Ten compared theorems,
namespace EntangledBorn.
The composite-algebra package:
separable_chsh_le— every separable state (Werner's notion, spelled inline as a finite convex combination of Kronecker products of one-party states) has normalized CHSH expectation at most 2 for the real-Pauli tuple, proved through the Bloch-disk constraint with no spectral theory;entanglement_exists— an entanglement witness: a state, positive semidefinite with unit trace, that is not separable, with Born CHSH expectation exactly 2√2, the Tsirelson value (the Bell state, exhibited explicitly in the Solution);effect_of_involution— spectral projections without spectral theory: (1+W)/2 is an effect for every Hermitian involution W, in any finite dimension;born_correlation_forced— the two-party correlation law forced, not postulated: for any state representing a generalized probability measure on effects (Busch's vocabulary; no continuity assumed), the correlation at any pair of binary-observable settings is an explicit difference of the measure's values at two effects;entangled_born_correlations— the assembly: one state that is not separable, is the unique state reproducing its own effect statistics (Born-rule uniqueness on the composite algebra), attains 2√2, and carries the correlation table XX = ZZ = 1, XZ = ZX = 0.
The general bounds and the Horodecki-line quantitative layer (added 2026-08-31):
separable_chsh_le_general— the separable bound at arbitrary finite local dimensions: every separable state has CHSH expectation at most 2 at every four Hermitian-involution settings, two per party;state_chsh_le_general— the state-level Tsirelson bound at the same generality: any bipartite state obeys 2√2 at every such settings;werner_chsh_max— the Werner family W_p = p·|Φ⁺⟩⟨Φ⁺| + ((1−p)/4)·1, spelled inline from the explicit Bell projector: CHSH expectation at most 2√2·p at any Hermitian-involution settings with traceless party-1 observables, for p ≥ 0 — the Werner line of the Horodecki–Horodecki–Horodecki 1995 criterion;werner_violation_iff— the violation threshold: for p ≥ 0, W_p violates CHSH (value > 2) at some such settings iff p > 1/√2;werner_separable_third— the separability endpoint (Werner 1989): W_p is separable for 0 ≤ p ≤ 1/3, by an explicit 7-term convex decomposition into product states.
No physical claim is part of the compared statements: they assert
properties of explicit matrices over the complex numbers, nothing
stronger. All hypotheses are inline; the compared statements use only
Mathlib vocabulary (Matrix.PosSemidef, Matrix.IsHermitian,
Matrix.trace, the Kronecker product, Real.sqrt,
Matrix.vecMulVec) with no custom definitions. Axioms on every
compared theorem: propext, Classical.choice, Quot.sound,
audited in-build.
Prior art is disclosed in formalization.yaml at full strength — in
particular the closest prior formalization, the Isabelle/HOL AFP entry
TsirelsonBound (2023), which proves the separable CHSH bound and the state-level Tsirelson
bound 2√2 at general local dimensions and settings (the latter in the
wider commuting-tuple form), and Bell-state attainment without stating
the non-separability corollary; the general bounds
here (separable_chsh_le_general, state_chsh_le_general) now match
that generality in Lean, with the remaining asymmetry (its
absolute-value form of the separable bound vs the one-sided form
here) disclosed in the yaml. The Werner trio is the quantitative
content of Horodecki–Horodecki–Horodecki 1995 and Werner 1989, with
no formal counterpart found in any prover by the sweeps (AFP,
physlib, Lean-QuantumInfo, CoqQ, Mathlib, arXiv), re-run on the
submission date; each claim is dated accordingly.
Challenge.lean states the ten results with placeholder proofs;
Solution.lean proves them all by transfer from the PdtEntangled,
PdtBornComposite and PdtWerner developments (PdtBusch supplies
the frame-function layer; PdtTsirelson enters the build through
PdtEntangled's bridge theorem); comparator.json is the machine comparison
surface; formalization.yaml carries sources, classification, and
disclosure.
Build:
lake exe cache get
lake build
(pinned toolchain and Mathlib; a green build is the kernel verification).
This repository is the complete, self-contained proof development for
this entry — nothing is imported from any parent project. It belongs
to the larger kernel-verified project
stalex444/pdt-lean
(pinned reference revision
d66ffbe,
where the PdtTsirelson and PdtBusch modules also live; Zenodo
concept DOI
10.5281/zenodo.21210683).