Outcome
Outcome encodes the two possible results of a spin measurement in a Bell experiment as the constructors plus and minus. Researchers formalizing quantum nonlocality from shared ledger entries in Recognition Science would cite this when building correlation functions. The definition is a direct inductive type with a pattern-matching conversion to real numbers.
claimAn outcome is an element of the two-element set with members $+$ and $-$, where $+$ maps to the numerical value $+1$ and $-$ maps to $-1$.
background
The module QF-005 derives Bell inequality violation from Recognition Science ledger structure, treating entanglement as shared entries that produce non-local correlations without signaling. Outcome supplies the elementary measurement results needed to define Bell pairs and correlation functions. Upstream results include the Monty Hall Outcome (pairs from Fin 3 × Fin 3 for probability counting) and the active-edge count A from IntegrationGap and Masses.Anchor, which fix the phi-power balance at D = 3.
proof idea
The declaration is an inductive definition introducing constructors plus and minus, with deriving clauses for DecidableEq and Repr. The companion toReal function is a one-line pattern match sending plus to 1 and minus to -1.
why it matters in Recognition Science
This supplies the measurement alphabet for the quantumCorrelation and chshCombination constructions that reach the Tsirelson bound. It supports the paper proposition on quantum nonlocality from ledger structure and connects to the forcing chain landmarks T5 (J-uniqueness), T7 (eight-tick octave), and T8 (D = 3). Downstream uses appear in Monty Hall outcome counting, showing reuse of the plus/minus pattern across decision and quantum modules.
scope and limits
- Does not specify measurement angles or settings.
- Does not compute correlation values or bounds.
- Does not encode the shared-ledger mechanism.
- Does not prove the CHSH or Tsirelson inequalities.
formal statement (Lean)
47inductive Outcome where
48 | plus : Outcome
49 | minus : Outcome
50deriving DecidableEq, Repr
51
52/-- Convert outcome to numerical value. -/
53def Outcome.toReal : Outcome → ℝ
54 | Outcome.plus => 1
55 | Outcome.minus => -1
56
57/-! ## Entangled State -/
58
59/-- A Bell pair (maximally entangled two-qubit state). -/