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

BellFalsifier

show as:
view Lean formalization →

BellFalsifier records candidate experimental outcomes that would falsify quantum Bell violations under the Recognition Science shared-ledger model of entanglement. Quantum foundations researchers would cite the structure when tabulating the current status of local-hidden-variable and signaling hypotheses. The declaration is a bare record type with two string fields, instantiated directly by the downstream experimentalStatus list.

claimA Bell falsifier is a record consisting of a string naming a potential violation (local hidden variables, superluminal signaling, or Tsirelson-bound breach) together with a string reporting its experimental status.

background

Recognition Science treats entanglement as two particles sharing a single ledger entry created at pair production. Measurement on one particle reads the shared entry and correlates the outcomes without permitting faster-than-light signaling, thereby violating the CHSH bound |S| ≤ 2 that any local hidden-variable theory must obey. Quantum mechanics reaches the Tsirelson limit 2√2, and the module QF-005 derives this nonlocality from the ledger factorization already established in upstream ledger and phi-forcing results.

proof idea

The declaration is a structure definition that introduces the two-field record type; no tactics or lemmas are applied.

why it matters in Recognition Science

The structure supplies the data type used by experimentalStatus to list the three currently ruled-out falsifiers. It therefore closes the QF-005 ledger account of Bell violation and anchors the claim that Recognition Science reproduces quantum nonlocality from shared entries while respecting the eight-tick octave and the absence of superluminal signaling.

scope and limits

formal statement (Lean)

 223structure BellFalsifier where
 224  /-- Type of claimed violation. -/
 225  claim : String
 226  /-- Status. -/
 227  status : String
 228
 229/-- No falsification has occurred; all experiments confirm quantum prediction. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (18)

Lean names referenced from this declaration's body.