EPRPair
plain-language theorem explainer
The EPRPair structure supplies the basic data type for an entangled pair in the Recognition Science ledger model. Quantum foundations researchers would cite it when formalizing how shared ledger entries generate nonlocal correlations while preserving local accessibility. The declaration is a plain structure definition that bundles an entanglement flag with three-dimensional locations and separation distance.
Claim. An EPR pair consists of two particles located at positions $r_A, r_B$ in three-dimensional Euclidean space, separated by distance $d = |r_A - r_B|$, with the entanglement flag set true to indicate the shared ledger entry corresponding to the state $|Φ^+⟩ = (|00⟩ + |11⟩)/√2$.
background
The module QF-006 frames nonlocality without signaling as a consequence of ledger consistency: entangled particles share ledger entries while any local reading leaves the distant party's view unchanged. This setting draws on upstream ledger factorization structures that calibrate the J-cost on the positive reals and phi-forcing derivations that fix the discrete tiers underlying physical quantities. The structure therefore inherits the three-dimensional spatial embedding and the global consistency requirement already established in the foundation modules.
proof idea
The declaration is a structure definition that introduces four fields: a Boolean entanglement flag defaulting to true, two location triples in ℝ³, and a separation scalar. No lemmas or tactics are invoked; the body simply declares the carrier type for later use in correlation and no-signaling statements.
why it matters
EPRPair anchors the ledger-based account of Bell correlations inside the Recognition framework. It directly supports the module target of deriving nonlocality from shared ledger entries while blocking signaling, and it supplies the object type for sibling results such as no_signaling_theorem and bell_violation. The construction aligns with the forcing-chain requirement of D = 3 spatial dimensions and the global consistency enforced by the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.