pith. machine review for the scientific record. sign in
structure definition def or abbrev high

NonlocalityFalsifier

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 238structure NonlocalityFalsifier where
 239  ftl_signaling_observed : Prop
 240  bell_inequality_satisfied : Prop
 241  tsirelson_bound_exceeded : Prop
 242  falsified : ftl_signaling_observed ∨ bell_inequality_satisfied ∨ tsirelson_bound_exceeded → False
 243
 244end NonlocalityNoSignaling
 245end Quantum
 246end IndisputableMonolith