experimentalStatus
plain-language theorem explainer
The declaration enumerates current experimental outcomes for three potential falsifiers of Bell inequality violations within Recognition Science. Quantum foundations researchers would cite it when mapping shared ledger entries to observed nonlocality without local realism. It is assembled as a direct list literal of BellFalsifier records confirming alignment with quantum predictions.
Claim. The experimental status is the list of BellFalsifier records: (``Local hidden variables'', ``Ruled out at $>100σ$''); (``FTL signaling'', ``Never observed''); (``Tsirelson violation'', ``Never observed'').
background
BellFalsifier is the structure pairing a claim string with a status string; its doc-comment states that Bell violation would be falsified by experiments showing |S| ≤ 2, discovery of local hidden variables, superluminal signaling, or Tsirelson bound violation. The module sets the local theoretical setting as QF-005, deriving Bell inequality violation from Recognition Science ledger structure where entanglement corresponds to shared ledger entries that produce non-local correlations without faster-than-light signaling. The upstream BellFalsifier definition supplies the record type used to record that no such falsification has occurred.
proof idea
The definition is a direct list literal that constructs three BellFalsifier records from string pairs; no lemmas or tactics are applied beyond the structure constructor.
why it matters
This definition closes the experimental side of the BellInequality module whose target is to derive Bell violation from shared ledger entries. It records that experiments align with the quantum prediction |S| ≤ 2√2 (Tsirelson bound) and with the eight-tick octave and phi-ladder structure of Recognition Science. No downstream theorems depend on it yet; it serves as a standing reference for the claim that local hidden variables remain ruled out.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.