Outcome
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.