NonlocalityFalsifier
plain-language theorem explainer
The structure encodes the three experimental outcomes that would refute the ledger-consistency account of quantum nonlocality. A foundations researcher would cite it to mark the boundary between the Recognition Science derivation and possible Bell-test or signaling results. It is introduced as a direct structure definition that packages the propositions and requires their disjunction to be contradictory.
Claim. Let $P$ be the proposition that faster-than-light signaling has been observed, $Q$ the proposition that a Bell inequality holds, and $R$ the proposition that quantum correlations exceed the Tsirelson bound. The structure consists of fields for $P$, $Q$, $R$, and the implication $(P ∨ Q ∨ R) → ⊥$.
background
The module addresses QF-006: deriving nonlocality without signaling from ledger consistency. Quantum mechanics appears contradictory because Bell inequality violations establish nonlocal correlations while no-signaling theorems forbid faster-than-light information transfer. Recognition Science resolves this by positing that entangled particles share ledger entries (accounting for nonlocality) while local reads leave the distant entry unchanged (enforcing no signaling). The ledger therefore maintains global consistency without communication. No upstream lemmas are referenced; the structure stands as the explicit falsification interface for the module's target claim.
proof idea
The declaration is a structure definition that directly assembles the three propositions and the required contradiction. No tactics or lemmas are applied; the body is the field list itself.
why it matters
It supplies the concrete falsification criteria for the QF-006 target stated in the module doc. The structure closes the loop on the ledger-consistency explanation by naming the observations (FTL signaling, Bell satisfaction, Tsirelson violation) that would defeat the account. It sits at the interface between the Recognition framework's quantum ledger model and experimental tests, without yet feeding any downstream theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.