singlet
plain-language theorem explainer
The singlet definition constructs a BellPair for a given natural number identifier by setting the shared ledger entry to trivial and labeling the correlation type as singlet, modeling the state |ψ⟩ = (|01⟩ - |10⟩)/√2. Physicists deriving Bell violations from Recognition Science ledger structures cite it when instantiating entangled pairs for correlation calculations. It is realized by a direct constructor application with no further computation.
Claim. For each natural number identifier $n$, singlet$(n)$ yields the Bell pair $(n, True, ``singlet'')$, which represents the maximally entangled two-qubit state $|ψ⟩ = (|01⟩ - |10⟩)/√2$.
background
In this module a BellPair is the structure with fields id : ℕ, sharedEntry : True (abstract shared ledger), and correlationType : String. The module documentation frames entanglement as two particles created together sharing a ledger entry, so that a measurement on one reads the common data without allowing signaling. The local theoretical setting is QF-005, which derives Bell inequality violation from Recognition Science ledger structure rather than local hidden variables. Upstream dependencies supply only identity morphisms from CostAlgebra and ArithmeticOf together with the BellPair structure itself.
proof idea
The definition is a one-line wrapper that applies the BellPair constructor to the supplied identifier, the trivial proof for the sharedEntry field, and the string literal ``singlet''.
why it matters
This supplies the concrete singlet instance used by downstream declarations including IsoSpinMultiplet, confinement_from_ledger, and SharedLedgerEntry. It fills the concrete state needed for the module's derivation of quantum correlations from shared ledgers, connecting directly to the Recognition Science account of nonlocality via ledger entries and the Tsirelson bound. No open scaffolding is closed here; the definition simply populates the singlet case for later correlation theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.