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

experimentalStatus

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 230def experimentalStatus : List BellFalsifier := [

proof body

Definition body.

 231  ⟨"Local hidden variables", "Ruled out at >100σ"⟩,
 232  ⟨"FTL signaling", "Never observed"⟩,
 233  ⟨"Tsirelson violation", "Never observed"⟩
 234]
 235
 236end BellInequality
 237end Quantum
 238end IndisputableMonolith

depends on (1)

Lean names referenced from this declaration's body.