BellPair
plain-language theorem explainer
BellPair encodes a maximally entangled two-qubit state through a shared ledger entry in the Recognition Science model. Quantum foundations researchers would cite it when formalizing nonlocality from ledger structure rather than hidden variables. The declaration is a direct structure definition with three fields and no proof obligations.
Claim. A Bell pair is a structure with an identifier $n$ in the natural numbers, a shared ledger entry represented by the trivial proposition, and a correlation type given by a string.
background
The module QF-005 derives Bell inequality violation from Recognition Science ledger structure. Entanglement corresponds to two particles sharing a single ledger entry, which produces non-local correlations without signaling. BellPair supplies the data type for such pairs, with fields for identifier, shared entry, and correlation type. Upstream identities from CostAlgebra and ArithmeticOf supply the underlying algebraic morphisms used in the ledger model.
proof idea
The declaration is a structure definition with an empty proof body. It directly introduces the three fields and the type BellPair without invoking any lemmas or tactics.
why it matters
BellPair supplies the type used by the singlet constructor to instantiate specific entangled states. It fills the QF-005 target of explaining quantum nonlocality from shared ledger entries, enabling later derivation of the CHSH combination and the Tsirelson bound. The definition anchors the transition from classical local realism to the quantum correlation function in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.