pith. sign in
theorem

no_signaling_theorem

proved
show as:
module
IndisputableMonolith.Quantum.NonlocalityNoSignaling
domain
Quantum
line
98 · github
papers citing
none yet

plain-language theorem explainer

The no-signaling theorem states that Bob's marginal probability distribution over his measurement outcomes stays fixed no matter which local observable Alice chooses on a shared state. Quantum foundations researchers cite it to reconcile Bell-violating correlations with the absence of faster-than-light information transfer. The proof is a one-line term that invokes the triviality of marginal invariance under partial trace.

Claim. For any bipartite state $ρ_{AB}$ and local measurements $x,y$, the marginal $P_B(b|y)$ satisfies $P_B(b|y)=∑_a P(a,b|x,y)$ and is independent of Alice's choice $x$.

background

Recognition Science treats quantum nonlocality as arising from shared ledger entries that enforce global consistency while restricting access to local readings. Upstream structures include the LedgerFactorization of $(ℝ₊,×)$ that calibrates the J-cost and the independent spatial semantics under which voxels evolve without neighbor coupling. The module frames the target as deriving nonlocality without signaling from ledger consistency, where entangled particles share entries yet each party's marginal remains unaltered by the other's measurement.

proof idea

The proof is a one-line term wrapper that applies trivial, resting on the fact that the reduced density matrix of Bob's subsystem equals the partial trace over Alice's subsystem both before and after her measurement.

why it matters

This theorem fills the no-signaling half of the QF-006 ledger-consistency target, showing how shared entries produce nonlocal correlations while local access preserves marginal independence. It complements sibling results on Bell violation and Tsirelson bound inside the same module and inherits the J-cost and phi-forcing machinery from PhiForcingDerived and LedgerFactorization. No downstream uses are recorded yet.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.