SharedLedgerEntry
plain-language theorem explainer
SharedLedgerEntry encodes a global ledger record for entangled particles as a pair of complex values fixed to be negatives of each other. Quantum foundations researchers cite it when showing that Bell correlations arise from pre-existing ledger data rather than instantaneous messages. The declaration is a direct structure definition that imposes the anti-correlation condition as a field.
Claim. A structure consisting of two complex numbers $v_A$ and $v_B$ together with the equality $v_A = -v_B$, representing the shared ledger entry whose values are fixed at entanglement and read locally by each party.
background
The module QF-006 derives nonlocality without signaling from ledger consistency. Entangled particles share a single ledger entry rather than exchanging messages; Alice and Bob each perform a local read of the same (or anti-correlated) record. The ledger itself is introduced via LedgerFactorization.of as a factorization of the positive reals under multiplication with calibrated J-cost, and PhiForcingDerived.of supplies the underlying J-cost structure. PrimitiveDistinction.from supplies the seven-axiom starting point that reduces to four structural conditions plus definitional facts.
proof idea
The declaration is a structure definition. It directly assembles the two complex fields and the anti-correlation equality as a single constructor; no lemmas or tactics are applied.
why it matters
The structure supplies the concrete object needed for the ledger-consistency argument in QF-006. It lets the module state that reading is local while the correlation is global, thereby separating nonlocality from signaling. The construction sits downstream of LedgerFactorization and PhiForcingDerived and is used by sibling declarations such as no_signaling_theorem and ledger_explains_nonlocality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.