module module moderate

`IndisputableMonolith.Quantum.BellInequality`

BellInequality module defines the objects needed to state and bound quantum correlations in Recognition Science. It includes types for angles, outcomes, and the singlet Bell pair along with correlation and CHSH functions. Physicists studying quantum foundations reference these when deriving Tsirelson bounds. The module contains only definitions and no proof bodies.

claimDefines measurement direction as angle $θ$, outcome as $±1$, Bell pair as singlet state, quantum correlation as expectation $C(θ_1,θ_2)$, CHSH combination $S$, classical bound $2$, and Tsirelson bound $2√2$.

background

The module sits in the quantum domain and imports the RS time quantum $τ_0 = 1$ tick from Constants. Key definitions include MeasurementAngle for simplified directions, Outcome for binary results, BellPair for entangled states, singlet for the antisymmetric two-qubit state, and quantumCorrelation for expectation values. These establish the setting for classical versus quantum correlation bounds.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the quantum measurement primitives that enable analysis of Bell inequalities within the Recognition Science framework. It draws on the fundamental constants from the upstream Constants module to set RS-native units. The definitions support potential extensions to the phi-ladder and eight-tick structures in quantum contexts.

scope and limits

Does not derive Tsirelson bound from RS forcing chain.
Does not model detector efficiencies or noise.
Does not connect to mass formulas or D=3.
Does not address multi-particle generalizations.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (26)

abbrev MeasurementAngle L44
inductive Outcome L47
structure BellPair L60
def singlet L69
def quantumCorrelation L76
theorem quantum_correlation_bounded L80
theorem perfect_anticorrelation L87
def chshCombination L96
theorem classical_chsh_bound L102
def tsirelsonBound L109
theorem tsirelson_bound_value L111
def optimalAngles L117
def optimalCHSH L121
lemma cos_three_pi_div_four L126
theorem optimal_chsh_value L138
theorem quantum_violation L163
theorem bell_from_shared_ledger L178
theorem no_signaling L184
def aspectExperiment L192
def loopholeFreeExperiment L195
theorem nobel_prize_2022 L198
def bellPairEntropy L203
theorem max_entanglement_entropy L206
theorem entanglement_monogamy L212
structure BellFalsifier L223
def experimentalStatus L230