LemmaStatement: AI-adaptedProof: AI-adaptedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Conditioning on a setting-independent selection preserves local-response representability and the CHSH bound

Statement

Let $μ$ be a binary correlation model on finite setting sets $I, J$ with outcome labels $Σ = {- 1, + 1}$ (Binary correlation models: setting-indexed tables of two-valued outcome laws, marginals and the CHSH functional), and suppose that $μ$ admits a local-response representation with response laws $(α_{i})_{i \in I}$ , $(β_{j})_{j \in J}$ on a probability space $(Λ, Σ_{Λ}, P)$ (Local-response representations of a binary correlation model: one setting-independent specification space and per-station response laws). Let $D \in Σ_{Λ}$ be a selection event with $P (D) > 0$ , put $P_{D} (A) : = \frac{P (A \cap D)}{P (D)} (A \in Σ_{Λ})$ for the conditional probability measure on $D$ , and define the $D$ -conditional tables $μ_{i j}^{D} (ε, δ) : = \frac{1}{P (D)} \int_{Λ} 1_{D} (λ) α_{i} (λ, ε) β_{j} (λ, δ) d P (λ)$ for $(i, j) \in I \times J$ and $(ε, δ) \in Σ \times Σ$ . Then:

(a) $P_{D}$ is a probability measure on $(Λ, Σ_{Λ})$ and $μ^{D} : = (μ_{i j}^{D})$ is a binary correlation model on $(I, J)$ ;

(b) the same response laws represent $μ^{D}$ over $P_{D}$ : $μ_{i j}^{D} (ε, δ) = \int_{Λ} α_{i} (λ, ε) β_{j} (λ, δ) d P_{D} (λ) for all i, j, ε, δ;$

The selection event $D$ is a subset of the specification space: membership in $D$ is the same for every setting pair and does not depend on the settings or on the outcomes. No choice principle is used.

Facts & Assumptions

Given: A binary correlation model $μ$ ; a local-response representation $(α_{i})_{i \in I}$ , $(β_{j})_{j \in J}$ on $(Λ, Σ_{Λ}, P)$ ; a selection event $D$ with $P (D) > 0$ ; the measures $P_{D}$ and tables $μ^{D}$ displayed in the statement.

[F1]

The representation identity $μ_{i j} (ε, δ) = E_{P} [α_{i} (\cdot, ε) β_{j} (\cdot, δ)]$ holds, the response laws are $[0, 1]$ -valued with $\sum_{ε} α_{i} (λ, ε) = 1 = \sum_{δ} β_{j} (λ, δ)$ for every $λ$ , and $λ \mapsto α_{i} (λ, ε)$ , $λ \mapsto β_{j} (λ, δ)$ are measurable (Local-response representations of a binary correlation model: one setting-independent specification space and per-station response laws clause (a)); a binary correlation model is a family of normalized $[0, 1]$ -valued tables (Binary correlation models: setting-indexed tables of two-valued outcome laws, marginals and the CHSH functional clause (a)).

[F2]

$P$ is a measure with $P (Λ) = 1$ : it is countably additive on pairwise disjoint families and finitely additive, and $P (\emptyset) = 0$ (Measures on sigma-algebras, Probability measures and probability spaces).

[F3]

For an event $A$ the expectation of its indicator is its probability, $E [1_{A}] = P (A)$ , and $1_{A}$ is measurable exactly when $A$ is (The expectation of an indicator is the probability of the event, An indicator function is measurable exactly when its set is measurable, Expectation of a nonnegative or integrable random variable).

[F4]

Expectation is linear on finite sums of nonnegative bounded measurable functions, $E [\sum_{k} c_{k} f_{k}] = \sum_{k} c_{k} E [f_{k}]$ for finite index sets and real coefficients $c_{k} \geq 0$ (Linearity, monotonicity, and the modulus bound for expectation, Finite sums and finite products, by recursion); in particular the finite sums over $Σ$ commute with the integral.

[F5]

Every nonnegative measurable $f$ is the pointwise limit of an increasing sequence $(s_{k})$ of nonnegative simple functions with $0 \leq s_{k} \leq s_{k + 1} \leq f$ (Every nonnegative measurable function admits an explicit increasing sequence of simple approximations); for such a sequence and any measure $ν$ , $\int s_{k} d ν ↑ \int f d ν$ (Monotone convergence for the integral); the integral of a nonnegative simple function is defined as its finite weighted sum (The integral of a nonnegative simple function).

[F6]

If $μ$ admits a local-response representation on $I = J = {0, 1}$ , then $∣ S (μ) ∣ \leq 2$ (The CHSH bound for every binary correlation model admitting a local-response representation).

Proof

technique · direct; verify that conditioning on a measurable selection event gives a probability measure, prove the change-of-measure identity between $\mathbb P_{D}$ and $\mathbb P$ by the indicator-simple-monotone-convergence ladder, and apply it to the bounded response products

Given: The data of the statement and [F1]-[F6].

1.1givenF2algebra

[ $P_{D}$ is a probability measure] Since $P (D) > 0$ , the definition of $P_{D}$ is meaningful; it is nonnegative and $P_{D} (Λ) = P (Λ \cap D) / P (D) = 1$ . For pairwise disjoint $A_{n} \in Σ_{Λ}$ with union $A$ , the sets $A_{n} \cap D$ are pairwise disjoint with union $A \cap D$ , so countable additivity of $P$ [F2] gives $P_{D} (A) = P (A \cap D) / P (D) = \sum_{n} P (A_{n} \cap D) / P (D) = \sum_{n} P_{D} (A_{n})$ ; hence $P_{D}$ is a probability measure on $(Λ, Σ_{Λ})$ .

2.1givenF3step 1.1algebra

[Indicators] Let $A \in Σ_{Λ}$ . Then $1_{D} 1_{A} = 1_{A \cap D}$ , and [F3] applied to the probability space $(Λ, Σ_{Λ}, P)$ gives $\int 1_{D} 1_{A} d P = E [1_{A \cap D}] = P (A \cap D)$ , while [F3] applied to $(Λ, Σ_{Λ}, P_{D})$ gives $\int 1_{A} d P_{D} = E_{P_{D}} [1_{A}] = P_{D} (A) = P (A \cap D) / P (D)$ ; hence $\int_{Λ} 1_{A} d P_{D} = P (D)^{- 1} \int_{Λ} 1_{D} 1_{A} d P$ .

3.1step 2.1F4algebra

[Nonnegative simple functions] By [F4] and the definition of the integral of a nonnegative simple function, both sides of the identity of step 2.1 are linear in the integrand over finite nonnegative combinations; hence for every nonnegative simple function $s$ on $(Λ, Σ_{Λ})$ one has $\int_{Λ} s d P_{D} = P (D)^{- 1} \int_{Λ} 1_{D} s d P$ .

3.2step 1.1step 2.1F1F4algebra

[Normalization] By [F1] and [F4], $\sum_{ε, δ} μ_{i j}^{D} (ε, δ) = P (D)^{- 1} \int 1_{D} (\sum_{ε} α_{i} (\cdot, ε)) (\sum_{δ} β_{j} (\cdot, δ)) d P = P (D)^{- 1} \int 1_{D} d P = P (D) / P (D) = 1$ , the last equality by the indicator identity of step 2.1 with $A = Λ$ , and each $μ_{i j}^{D} (ε, δ) \geq 0$ by nonnegativity of the integrand; hence $μ^{D}$ is a binary correlation model on $(I, J)$ . Together with step 1.1 this is (a).

4.1step 3.1F5algebra

[Bounded measurable functions] Let $f \geq 0$ be measurable and bounded, say $0 \leq f \leq M < + \infty$ . By [F5] choose an increasing sequence $(s_{k})$ of nonnegative simple functions with $s_{k} ↑ f$ ; then $1_{D} s_{k} ↑ 1_{D} f$ , and monotone convergence [F5] applied to the measures $P_{D}$ and $P$ gives $\int s_{k} d P_{D} ↑ \int f d P_{D}$ and $\int 1_{D} s_{k} d P ↑ \int 1_{D} f d P$ . Passing to the limit in the identity of step 3.1, valid for every $k$ , yields $\int_{Λ} f d P_{D} = P (D)^{- 1} \int_{Λ} 1_{D} f d P$ .

5.1givenF1step 4.1algebra

[Representation over $P_{D}$ ] Fix $i, j, ε, δ$ and put $f : = α_{i} (\cdot, ε) β_{j} (\cdot, δ)$ . By [F1] $f$ is a product of two measurable $[0, 1]$ -valued functions, hence measurable and bounded with $0 \leq f \leq 1$ . Step 4.1 gives $\int f d P_{D} = P (D)^{- 1} \int 1_{D} f d P = μ_{i j}^{D} (ε, δ)$ by the definition of the $D$ -conditional tables; this is (b).

6.1step 1.1step 3.2step 5.1F6∎

[Bound and assembly] Step 5.1 exhibits a local-response representation of $μ^{D}$ with the same response laws over the probability space $(Λ, Σ_{Λ}, P_{D})$ ; hence [F6] applies to $μ^{D}$ and gives $∣ S (μ^{D}) ∣ \leq 2$ when $I = J = {0, 1}$ , which is (c). Steps 1.1 and 3.2 prove (a) and step 5.1 proves (b).

Remarks

Setting-independent selection. The lemma conditions on an event of the specification space alone. This is the mathematical form of a setting-independent selection: whether a run enters the recorded sample is determined by the specification and not by the settings or the outcomes. Nothing is claimed here for selection rules that depend on the distant setting, on the local setting or on the observed outcomes; those require their own models and are not covered by the lemma.
Direction of use. The lemma is used in the converse direction of detection: if the full tables of a comparison admit a local-response representation and the recorded trials are the runs that pass a setting-independent selection, then the recorded tables again admit one, so the CHSH bound holds for the recorded tables too. Without such a selection model no transfer of the bound to a sub-ensemble is asserted.

Conditioning on a setting-independent selection preserves local-response representability and the CHSH bound

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources