EPRPair
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.
claimAn 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 in Recognition Science
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.
scope and limits
- Does not derive the explicit form of the entangled state from the J-cost or ledger axioms.
- Does not compute expectation values or CHSH bounds.
- Does not model measurement outcomes or state collapse.
- Does not prove the no-signaling property; that is left to downstream theorems.
formal statement (Lean)
38structure EPRPair where
39 /-- State: |Φ⁺⟩ = (|00⟩ + |11⟩)/√2 -/
40 entangled : Bool := true
proof body
Definition body.
41 /-- Location of particle A -/
42 location_A : ℝ × ℝ × ℝ
43 /-- Location of particle B (far away) -/
44 location_B : ℝ × ℝ × ℝ
45 /-- Separation distance -/
46 separation : ℝ
47
48/-- A measurement on one particle of the pair. -/