module module moderate

`IndisputableMonolith.Quantum.BellInequality`

The Quantum.BellInequality module supplies the basic objects and functions needed to state Bell inequalities and their quantum bounds inside the Recognition Science framework. A physicist examining how RS derives correlation limits or comparing classical versus Tsirelson bounds would cite these definitions. It is a definition module containing no proofs.

claimDefines MeasurementAngle as a real angle $\theta$, Outcome as $\pm 1$, BellPair and singlet state, the correlation function $C(\theta_1,\theta_2)$, CHSH combination, classical bound 2, and Tsirelson bound $2\sqrt{2}$.

background

The module sits in the quantum domain and imports the RS time quantum $\tau_0=1$ tick from Constants. It introduces MeasurementAngle (a direction reduced to an angle), Outcome, BellPair, the singlet state, quantumCorrelation, the CHSH combination, classical_chsh_bound, tsirelsonBound, and optimalAngles. These objects prepare the standard quantum-information setting for later comparison with RS-native correlation laws such as the Recognition Composition Law.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module establishes the notational base for Bell-inequality results inside Recognition Science and supplies the objects that any parent theorem deriving the Tsirelson bound from the J-function or forcing chain would require. No downstream uses are recorded yet.

scope and limits

Does not derive any bound from the J-uniqueness or RCL.
Does not link angles to the phi-ladder or eight-tick octave.
Does not contain mass formulas or alpha-band constraints.
Does not address experimental predictions or measurement protocols.

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