diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau.lean new file mode 100644 index 0000000000..2f9a7f27df --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +## Saturation de la borne de Tsirelson : le témoin de Pauli et le critère de Landau + +Ce module est la quatrième tranche du pilote quantique de l'Epic #13106. Les +trois premières ont borné la frontière classique déterministe (`Conway.CHSH`), +son enveloppe randomisée (`Conway.CHSHRandomized`), puis importé la borne +quantique `2√2` de Mathlib avec sa carte d'hypothèses (`Conway.CHSHQuantum`). +`Conway.CHSHQuantum` laissait quatre points déclarés **non établis** ; cette +tranche en lève trois par une même construction explicite : + +1. **Saturation** — l'opérateur CHSH du témoin vaut *exactement* `2√2 • 1`, + égalité et non majorant : la constante de Tsirelson est atteinte ; +2. **Construction matricielle** — quatre observables explicites sur ℝ^(2×2), + combinaisons des matrices de Pauli σz et σx ; +3. **Forme spectrale bilatérale** — `chsh_landau_diagonal` : l'opérateur est + diagonal, `2√2` sur la diagonale — chaque vecteur de base est vecteur + propre, l'égalité tient des deux côtés. (La « norme d'opérateur » du + statut de `CHSHQuantum` est livrée ici en forme spectrale explicite : en + Mathlib v4.32.1 les normes matricielles sont des non-instances scoped + (`Matrix.Norms.Operator`), et l'égalité exacte `S = 2√2 • 1` en porte la + substance — la majoration est atteinte, pas seulement vraie.) + +### Le modèle réduit, et ce qu'il ne prétend pas être + +Les observables vivent dans `Matrix (Fin 2) (Fin 2) ℝ` : c'est le **modèle +réduit** à un qubit, où le produit `Aᵢ * Bⱼ` est le produit matriciel des +représentants réduits. Dans le modèle tensoriel non réduit (opérateurs +`A ⊗ 1` et `1 ⊗ B` sur ℝ⁴), la commutation croisée `Aᵢ Bⱼ = Bⱼ Aᵢ` est une +hypothèse structurelle du `IsCHSHTuple` de Mathlib ; dans le modèle réduit elle +est **fausse** — `[σz, σz + σx] = [σz, σx] ≠ 0` — et ce module ne la revendique +pas. Ce qu'il établit est plus modeste et exact : la valeur de l'opérateur CHSH +du témoin, c'est-à-dire la constante que la borne abstraite majore, est +*réalisée* par une construction concrète. L'interprétation probabiliste +complète (états, mesures, espérances sur le modèle tensoriel) reste déclarée +ouverte, comme dans `Conway.CHSHQuantum`. + +### Landau : ce qui est retenu, ce qui reste ouvert + +Landau (1988) caractérise la valeur quantique maximale du score CHSH d'une +matrice de corrélation `C` par les valeurs propres de sa partie symétrique. +Ce module ne formalise pas le théorème général (une preuve SDP complète) ; il +vérifie le critère **sur le témoin** : la matrice de corrélation réduite + +- est symétrique, +- a un carré égal à l'identité, donc des valeurs propres ±1, + +et le score du témoin vaut `2√2` — la valeur que la caractérisation de Landau +prédit pour ce spectre. La direction « suffisant » est ainsi documentée par +témoin explicite ; la caractérisation générale (nécessaire et suffisant) reste +ouverte et déclarée. + +### Statut des énoncés (grille de digestion #13106) + +| Énoncé | Statut | +|---|---| +| Opérateur CHSH du témoin `= 2√2 • 1` (égalité exacte) | **prouvé ici** | +| Involutivité des quatre observables (`M² = 1`) | **prouvé ici** | +| Auto-adjointude (symétrie des matrices réelles) | **prouvé ici** | +| Forme spectrale : `S` diagonal, `2√2` sur la diagonale (bilatéral) | **prouvé ici** | +| Matrice de corrélation symétrique, de carré `1` (spectre ±1) | **prouvé ici** | +| Caractérisation générale de Landau (théorème, les deux sens) | **non établi** — vérifié sur témoin seulement | +| Interprétation probabiliste complète (états, mesures, ℝ⁴ tensoriel) | **non établi** — déclaré ouvert | +| Commutation croisée dans le modèle réduit | **fausse** et non revendiquée (voir ci-dessus) | + +### Grille de digestion (10 points) + +1. **Énoncés et niveau de garantie** : égalités matricielles exactes sur ℝ, + sans analyse fonctionnelle ; la constante `2√2` est celle de + `Conway.CHSHQuantum.tsirelson_bound`. +2. **Provenance** : L. J. Landau, « On the violation of Bell inequalities in + quantum theory », Physics Letters A 120 (1988), 54-56 ; construction de + saturation standard (Tsirelson 1980 ; formulation pédagogique Nielsen & + Chuang §2.4-2.5). Priorité de la caractérisation : Landau 1988 ; de la + borne : Tsirelson 1980. +3. **Nouveauté** : la série CHSH disposait de la borne (importée) et du gap + strict `2 < 2√2` ; le témoin d'égalité est nouveau dans le dépôt. +4. **Dépendances** : Mathlib v4.32.1 (`Matrix`, `Real.sqrt`, notation + `!![...]` via `Mathlib.LinearAlgebra.Matrix.Notation`), + réutilise `Conway.CHSHQuantum.chshOperator` sans le redéfinir ; aucun + `sorry`, aucun axiome au-delà des standards. +5. **Trivial condensé / nouveau développé** : les carrés de σz, σx sont des + calculs d'entrées ; le cœur est l'anticommutateur `σzσx + σxσz = 0`, duquel + découlent l'involutivité des `Bⱼ` et l'égalité centrale — les preuves sont + entry-level (ext + fin_cases) : la non-commutativité des matrices interdit + `ring`, chaque identité est donc distribuée puis close sur l'atome + `(√2)² = 2`. +6. **Friction** : le modèle réduit ne porte pas la commutation croisée + (hypothèse du tuple abstrait) — c'est la limite déclarée, détaillée + ci-dessus ; la manipulation de `√2` passe par l'atome `hsq : (√2)² = 2` + et `linear_combination`, jamais par une approximation numérique. +7. **Chemin de découverte** : (1) réduire le tenseur au qubit simple ; + (2) vérifier l'anticommutation ; (3) dériver `S = (4/√2) • 1` par + distributivité, puis `4/√2 = 2√2` ; (4) n'ensuite calculer les corrélations. + La reconstruction finale suit le même ordre, les lemmes intermédiaires + portant chacun une étape. +8. **Limites** : les trois lignes « non établi / faux » de la table de statut. +9. **Raccord au corpus** : quatrième module de la série CHSH de `conway_lean` + (avec `CHSH`, `CHSHRandomized`, `CHSHQuantum`) ; renvois côté notebooks : + `Lean-13b-CHSH-Tsirelson-Native` (exécution native de la série sous kernel + `lean4-wsl` — une tranche future peut y exécuter les énoncés du présent + module), `Lean-13-Kochen-Specker`, `Lean-16f-Conway-Free-Will-Theorem`. +10. **Transmission** : chaque lemme porte une docstring qui sépare ce que la + sortie du calcul montre de ce qu'il suggère ; la table de statut est le + résumé falsifiable. + +### Sources + +- L. J. Landau, « On the violation of Bell inequalities in quantum theory », + Physics Letters A 120 (1988), 54-56. +- B. S. Cirel'son (Tsirelson), « Quantum generalizations of Bell's + inequality », Letters in Mathematical Physics 4 (1980), 93-100. +- M. Nielsen, I. Chuang, *Quantum Computation and Quantum Information*, + Cambridge University Press (2000), §2.4-2.5. +-/ + +import Conway.CHSHQuantum +import Mathlib.Data.Matrix.Basic +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.LinearCombination + +namespace Conway +namespace CHSHLandau + +/-! ### Les briques de Pauli sur ℝ^(2×2) -/ + +/-- Matrice de Pauli `σz = diag(1, -1)`, représentant de l'observable +« spin selon z » : auto-adjointe, involutive, diagonale. -/ +def sigmaZ : Matrix (Fin 2) (Fin 2) ℝ := !![1, 0; 0, -1] + +/-- Matrice de Pauli `σx`, représentant de l'observable « spin selon x » : +auto-adjointe, involutive, antidiagonale. -/ +def sigmaX : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; 1, 0] + +/-- L'atome de calcul du module : `√2` est traité comme une quantité formelle +via son carré. Aucune preuve ci-dessous n'utilise d'approximation numérique. -/ +theorem sqrt_two_sq : (√2 : ℝ) ^ 2 = 2 := Real.sq_sqrt (by norm_num) + +theorem sigmaZ_sq : sigmaZ * sigmaZ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaZ, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +theorem sigmaX_sq : sigmaX * sigmaX = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaX, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +/-- Anticommutateur des deux Pauli : `σzσx + σxσz = 0`. + +C'est le cœur algébrique du module — de lui découlent l'involutivité des +observables `B` (leur carré mélange `σzσx` et `σxσz`) et l'égalité centrale +(les termes croisés de l'opérateur CHSH se compensent deux à deux). -/ +theorem sigmaZ_anticomm_sigmaX : sigmaZ * sigmaX + sigmaX * sigmaZ = 0 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaZ, sigmaX, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +theorem sigmaZ_symm : Matrix.transpose sigmaZ = sigmaZ := by + ext i j + fin_cases i <;> fin_cases j <;> simp [sigmaZ] + +theorem sigmaX_symm : Matrix.transpose sigmaX = sigmaX := by + ext i j + fin_cases i <;> fin_cases j <;> simp [sigmaX] + +/-! ### Les quatre observables du témoin -/ + +/-- Observable d'Alice `A₀ = σz`. -/ +def A₀ : Matrix (Fin 2) (Fin 2) ℝ := sigmaZ + +/-- Observable d'Alice `A₁ = σx`. -/ +def A₁ : Matrix (Fin 2) (Fin 2) ℝ := sigmaX + +/-- Observable de Bob `B₀ = (σz + σx)/√2`. -/ +noncomputable def B₀ : Matrix (Fin 2) (Fin 2) ℝ := (√2 : ℝ)⁻¹ • (sigmaZ + sigmaX) + +/-- Observable de Bob `B₁ = (σz - σx)/√2`. -/ +noncomputable def B₁ : Matrix (Fin 2) (Fin 2) ℝ := (√2 : ℝ)⁻¹ • (sigmaZ - sigmaX) + +theorem A₀_sq : A₀ * A₀ = 1 := sigmaZ_sq + +theorem A₁_sq : A₁ * A₁ = 1 := sigmaX_sq + +/-- Involutivité de `B₀` : le carré de `(σz + σx)/√2` vaut l'identité parce +que les termes croisés s'annulent par anticommutation et que +`(1/√2)² · (1 + 1) = 1`. Chaque entrée est close sur l'atome `sqrt_two_sq`. -/ +theorem B₀_sq : B₀ * B₀ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [B₀, Matrix.smul_apply, Matrix.mul_apply, Matrix.add_apply, + Fin.sum_univ_two, sigmaZ, sigmaX, Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +/-- Involutivité de `B₁`, par le même schéma que `B₀_sq` : les termes croisés +changent de signe mais s'annulent pareil. -/ +theorem B₁_sq : B₁ * B₁ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [B₁, Matrix.smul_apply, Matrix.mul_apply, Matrix.sub_apply, + Matrix.add_apply, Fin.sum_univ_two, sigmaZ, sigmaX, + Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +theorem B₀_symm : Matrix.transpose B₀ = B₀ := by + rw [B₀] + simp only [Matrix.transpose_add, Matrix.transpose_smul, sigmaZ_symm, sigmaX_symm] + +theorem B₁_symm : Matrix.transpose B₁ = B₁ := by + rw [B₁] + simp only [Matrix.transpose_sub, Matrix.transpose_smul, sigmaZ_symm, sigmaX_symm] + +/-! ### L'égalité centrale : l'opérateur CHSH du témoin vaut exactement `2√2` -/ + +/-- **Saturation de la borne de Tsirelson** (direction suffisance du critère +de Landau, par témoin explicite) : l'opérateur CHSH du quadruple +`(σz, σx, (σz+σx)/√2, (σz-σx)/√2)` vaut *exactement* `2√2 • 1` — chaque +vecteur est vecteur propre avec la valeur propre `2√2`, et la constante que +`Conway.CHSHQuantum.tsirelson_bound` majore est atteinte. + +La lecture algébrique : par distributivité, `S = (1/√2) • (σz(σz+σx) + +σz(σz-σx) + σx(σz+σx) - σx(σz-σx))` ; les huit produits se réordonnent en +`2·σz² + 2·σx²` plus quatre termes croisés `σzσx + σxσz` qui s'annulent deux à +deux par `sigmaZ_anticomm_sigmaX` ; il reste `(4/√2) • 1`, et `4/√2 = 2√2` +par `sqrt_two_sq`. La preuve exécute ce programme entrée par entrée. -/ +theorem chsh_landau : + CHSHQuantum.chshOperator A₀ A₁ B₀ B₁ = (2 * √2 : ℝ) • + (1 : Matrix (Fin 2) (Fin 2) ℝ) := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [CHSHQuantum.chshOperator, A₀, A₁, B₀, B₁, Matrix.smul_apply, + Matrix.mul_apply, Matrix.add_apply, Matrix.sub_apply, Fin.sum_univ_two, + sigmaZ, sigmaX, Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +/-- **Forme spectrale bilatérale** : l'opérateur CHSH du témoin est diagonal, +avec `2√2` sur la diagonale et `0` ailleurs — chaque vecteur de base est +vecteur propre pour la valeur propre `2√2`. C'est la jambe « bilatérale » +qui manquait à la série : `Conway.CHSHQuantum.tsirelson_bound` donne +`≤ 2√2` en général, et l'égalité centrale `chsh_landau`, précisée ici +entrée par entrée, montre que la borne est *atteinte* — la majoration est +une égalité, des deux côtés. -/ +theorem chsh_landau_diagonal (i j : Fin 2) : + CHSHQuantum.chshOperator A₀ A₁ B₀ B₁ i j = if i = j then 2 * √2 else 0 := by + rw [chsh_landau] + fin_cases i <;> fin_cases j <;> + simp [Matrix.smul_apply, Matrix.one_apply] + +/-! ### Matrice de corrélation et critère de Landau (vérifié sur le témoin) -/ + +/-- Matrice de corrélation réduite du témoin : l'entrée `(i, j)` est la +corrélation des observables `Aᵢ` et `Bⱼ` du quadruple, toutes égales à +`1/√2` au signe près (l'entrée `(1,1)` porte le signe `-` du terme +`- A₁ * B₁` de l'opérateur CHSH). -/ +noncomputable def corrMatrix : Matrix (Fin 2) (Fin 2) ℝ := + !![(√2 : ℝ)⁻¹, (√2 : ℝ)⁻¹; (√2 : ℝ)⁻¹, -(√2 : ℝ)⁻¹] + +/-- La matrice de corrélation du témoin est symétrique — la première moitié +de l'hypothèse du critère de Landau (1988). -/ +theorem corrMatrix_symm : Matrix.transpose corrMatrix = corrMatrix := by + ext i j + fin_cases i <;> fin_cases j <;> simp [corrMatrix] + +/-- Le carré de la matrice de corrélation vaut l'identité : son spectre est +exactement `{-1, 1}` — la seconde moitié du critère de Landau, vérifiée sur +le témoin. La caractérisation générale (les deux sens, pour toute matrice de +corrélation) reste déclarée ouverte. -/ +theorem corrMatrix_sq : corrMatrix * corrMatrix = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [corrMatrix, Matrix.mul_apply, Fin.sum_univ_two, + Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +end CHSHLandau +end Conway diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau_en.lean new file mode 100644 index 0000000000..5b9b83bbc2 --- /dev/null +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/CHSHLandau_en.lean @@ -0,0 +1,283 @@ +/- +Copyright (c) 2026 CoursIA. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +## Saturation of the Tsirelson bound: the Pauli witness and Landau's criterion + +This module is the fourth tranche of the quantum pilot of Epic #13106. The +first three bounded the deterministic classical frontier (`Conway.CHSH`), +its randomized envelope (`Conway.CHSHRandomized`), then imported Mathlib's +quantum bound `2√2` together with its hypothesis map (`Conway.CHSHQuantum`). +`Conway.CHSHQuantum` left four points declared **not established**; this +tranche lifts three of them through a single explicit construction: + +1. **Saturation** — the witness's CHSH operator equals *exactly* `2√2 • 1`, + an equality rather than a bound: Tsirelson's constant is attained; +2. **Matrix construction** — four explicit observables on ℝ^(2×2), + combinations of the Pauli matrices σz and σx; +3. **Two-sided spectral form** — `chsh_landau_diagonal`: the operator is + diagonal with `2√2` on the diagonal — every basis vector is an + eigenvector, the equality holds on both sides. (The "operator norm" of + `CHSHQuantum`'s status table is delivered here as an explicit spectral + form: in Mathlib v4.32.1 matrix norms are scoped non-instances + (`Matrix.Norms.Operator`), and the exact equality `S = 2√2 • 1` carries + the substance — the bound is attained, not merely true.) + +### The reduced model, and what it does not claim to be + +The observables live in `Matrix (Fin 2) (Fin 2) ℝ`: this is the **reduced** +single-qubit model, where the product `Aᵢ * Bⱼ` is the matrix product of the +reduced representatives. In the unreduced tensor model (operators `A ⊗ 1` and +`1 ⊗ B` on ℝ⁴), cross-commutation `Aᵢ Bⱼ = Bⱼ Aᵢ` is a structural hypothesis +of Mathlib's `IsCHSHTuple`; in the reduced model it is **false** — +`[σz, σz + σx] = [σz, σx] ≠ 0` — and this module does not claim it. What it +establishes is more modest and exact: the value of the witness's CHSH +operator, i.e. the constant that the abstract bound majorizes, is *realized* +by a concrete construction. The full probabilistic interpretation (states, +measurements, expectations on the tensor model) remains declared open, as in +`Conway.CHSHQuantum`. + +### Landau: what is retained, what remains open + +Landau (1988) characterizes the maximal quantum CHSH value of a correlation +matrix `C` through the eigenvalues of its symmetric part. This module does +not formalize the general theorem (a complete SDP proof); it checks the +criterion **on the witness**: the reduced correlation matrix + +- is symmetric, +- squares to the identity, hence has eigenvalues ±1, + +and the witness's score is `2√2` — the value Landau's characterization +predicts for that spectrum. The "sufficient" direction is thus documented by +an explicit witness; the general characterization (necessary and sufficient) +remains open and declared. + +### Statement status (digestion grid #13106) + +| Statement | Status | +|---|---| +| Witness's CHSH operator `= 2√2 • 1` (exact equality) | **proved here** | +| Involutivity of the four observables (`M² = 1`) | **proved here** | +| Self-adjointness (symmetry of the real matrices) | **proved here** | +| Spectral form: `S` diagonal, `2√2` on the diagonal (two-sided) | **proved here** | +| Symmetric correlation matrix squaring to `1` (spectrum ±1) | **proved here** | +| Landau's general characterization (theorem, both directions) | **not established** — witness check only | +| Full probabilistic interpretation (states, measurements, tensor ℝ⁴) | **not established** — declared open | +| Cross-commutation in the reduced model | **false** and not claimed (see above) | + +### Digestion grid (10 points) + +1. **Statements and guarantee level**: exact matrix equalities over ℝ, no + functional analysis; the constant `2√2` is the one of + `Conway.CHSHQuantum.tsirelson_bound`. +2. **Provenance**: L. J. Landau, "On the violation of Bell inequalities in + quantum theory", Physics Letters A 120 (1988), 54-56; standard saturation + construction (Tsirelson 1980; pedagogical account Nielsen & Chuang + §2.4-2.5). Priority of the characterization: Landau 1988; of the bound: + Tsirelson 1980. +3. **Novelty**: the CHSH series had the bound (imported) and the strict gap + `2 < 2√2`; the equality witness is new to the repository. +4. **Dependencies**: Mathlib v4.32.1 (`Matrix`, `Real.sqrt`, `!![...]` + notation via `Mathlib.LinearAlgebra.Matrix.Notation`), + reuses `Conway.CHSHQuantum.chshOperator` without redefining it; no + `sorry`, no axioms beyond the standard ones. +5. **Trivial condensed / new developed**: the squares of σz, σx are + entry-level computations; the heart is the anticommutator + `σzσx + σxσz = 0`, from which follow the involutivity of the `Bⱼ` and the + central equality — the proofs are entry-level (ext + fin_cases): matrix + non-commutativity forbids `ring`, so each identity is distributed then + closed on the atom `(√2)² = 2`. +6. **Friction**: the reduced model does not carry cross-commutation (a + hypothesis of the abstract tuple) — that is the declared limit, detailed + above; handling `√2` goes through the atom `hsq : (√2)² = 2` and + `linear_combination`, never through a numerical approximation. +7. **Discovery path**: (1) reduce the tensor to the single qubit; + (2) check anticommutation; (3) derive `S = (4/√2) • 1` by distributivity, + then `4/√2 = 2√2`; (4) only then compute the correlations. The final + reconstruction follows the same order, each intermediate lemma carrying + one step. +8. **Limits**: the three "not established / false" rows of the status table. +9. **Corpus connection**: fourth module of the CHSH series of `conway_lean` + (with `CHSH`, `CHSHRandomized`, `CHSHQuantum`); notebook pointers: + `Lean-13b-CHSH-Tsirelson-Native` (native execution of the series under + the `lean4-wsl` kernel — a future tranche may execute this module's + statements there), `Lean-13-Kochen-Specker`, + `Lean-16f-Conway-Free-Will-Theorem`. +10. **Transmission**: each lemma carries a docstring separating what the + computation's output shows from what it suggests; the status table is + the falsifiable summary. + +### Sources + +- L. J. Landau, "On the violation of Bell inequalities in quantum theory", + Physics Letters A 120 (1988), 54-56. +- B. S. Cirel'son (Tsirelson), "Quantum generalizations of Bell's + inequality", Letters in Mathematical Physics 4 (1980), 93-100. +- M. Nielsen, I. Chuang, *Quantum Computation and Quantum Information*, + Cambridge University Press (2000), §2.4-2.5. +-/ + +import Conway.CHSHQuantum_en +import Mathlib.Data.Matrix.Basic +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.LinearCombination + +namespace Conway_en +namespace CHSHLandau_en + +/-! ### The Pauli building blocks on ℝ^(2×2) -/ + +/-- Pauli matrix `σz = diag(1, -1)`, representative of the "spin along z" +observable: self-adjoint, involutive, diagonal. -/ +def sigmaZ : Matrix (Fin 2) (Fin 2) ℝ := !![1, 0; 0, -1] + +/-- Pauli matrix `σx`, representative of the "spin along x" observable: +self-adjoint, involutive, antidiagonal. -/ +def sigmaX : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1; 1, 0] + +/-- The computation atom of the module: `√2` is handled as a formal quantity +through its square. No proof below uses a numerical approximation. -/ +theorem sqrt_two_sq : (√2 : ℝ) ^ 2 = 2 := Real.sq_sqrt (by norm_num) + +theorem sigmaZ_sq : sigmaZ * sigmaZ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaZ, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +theorem sigmaX_sq : sigmaX * sigmaX = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaX, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +/-- Anticommutator of the two Paulis: `σzσx + σxσz = 0`. + +This is the algebraic heart of the module — from it follow the involutivity +of the `B` observables (their square mixes `σzσx` and `σxσz`) and the central +equality (the cross terms of the CHSH operator cancel pairwise). -/ +theorem sigmaZ_anticomm_sigmaX : sigmaZ * sigmaX + sigmaX * sigmaZ = 0 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [sigmaZ, sigmaX, Matrix.mul_apply, Fin.sum_univ_two] <;> norm_num + +theorem sigmaZ_symm : Matrix.transpose sigmaZ = sigmaZ := by + ext i j + fin_cases i <;> fin_cases j <;> simp [sigmaZ] + +theorem sigmaX_symm : Matrix.transpose sigmaX = sigmaX := by + ext i j + fin_cases i <;> fin_cases j <;> simp [sigmaX] + +/-! ### The four observables of the witness -/ + +/-- Alice's observable `A₀ = σz`. -/ +def A₀ : Matrix (Fin 2) (Fin 2) ℝ := sigmaZ + +/-- Alice's observable `A₁ = σx`. -/ +def A₁ : Matrix (Fin 2) (Fin 2) ℝ := sigmaX + +/-- Bob's observable `B₀ = (σz + σx)/√2`. -/ +noncomputable def B₀ : Matrix (Fin 2) (Fin 2) ℝ := (√2 : ℝ)⁻¹ • (sigmaZ + sigmaX) + +/-- Bob's observable `B₁ = (σz - σx)/√2`. -/ +noncomputable def B₁ : Matrix (Fin 2) (Fin 2) ℝ := (√2 : ℝ)⁻¹ • (sigmaZ - sigmaX) + +theorem A₀_sq : A₀ * A₀ = 1 := sigmaZ_sq + +theorem A₁_sq : A₁ * A₁ = 1 := sigmaX_sq + +/-- Involutivity of `B₀`: the square of `(σz + σx)/√2` is the identity +because the cross terms cancel by anticommutation and +`(1/√2)² · (1 + 1) = 1`. Each entry is closed on the atom `sqrt_two_sq`. -/ +theorem B₀_sq : B₀ * B₀ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [B₀, Matrix.smul_apply, Matrix.mul_apply, Matrix.add_apply, + Fin.sum_univ_two, sigmaZ, sigmaX, Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +/-- Involutivity of `B₁`, by the same scheme as `B₀_sq`: the cross terms +change sign but cancel just the same. -/ +theorem B₁_sq : B₁ * B₁ = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [B₁, Matrix.smul_apply, Matrix.mul_apply, Matrix.sub_apply, + Matrix.add_apply, Fin.sum_univ_two, sigmaZ, sigmaX, + Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +theorem B₀_symm : Matrix.transpose B₀ = B₀ := by + rw [B₀] + simp only [Matrix.transpose_add, Matrix.transpose_smul, sigmaZ_symm, sigmaX_symm] + +theorem B₁_symm : Matrix.transpose B₁ = B₁ := by + rw [B₁] + simp only [Matrix.transpose_sub, Matrix.transpose_smul, sigmaZ_symm, sigmaX_symm] + +/-! ### The central equality: the witness's CHSH operator is exactly `2√2` -/ + +/-- **Saturation of the Tsirelson bound** (sufficient direction of Landau's +criterion, by explicit witness): the CHSH operator of the quadruple +`(σz, σx, (σz+σx)/√2, (σz-σx)/√2)` equals *exactly* `2√2 • 1` — every +vector is an eigenvector with eigenvalue `2√2`, and the constant that +`Conway.CHSHQuantum.tsirelson_bound` majorizes is attained. + +The algebraic reading: by distributivity, `S = (1/√2) • (σz(σz+σx) + +σz(σz-σx) + σx(σz+σx) - σx(σz-σx))`; the eight products reorder into +`2·σz² + 2·σx²` plus four cross terms `σzσx + σxσz` that cancel pairwise by +`sigmaZ_anticomm_sigmaX`; what remains is `(4/√2) • 1`, and `4/√2 = 2√2` +by `sqrt_two_sq`. The proof carries out this program entry by entry. -/ +theorem chsh_landau : + CHSHQuantum_en.chshOperator A₀ A₁ B₀ B₁ = (2 * √2 : ℝ) • + (1 : Matrix (Fin 2) (Fin 2) ℝ) := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [CHSHQuantum_en.chshOperator, A₀, A₁, B₀, B₁, Matrix.smul_apply, + Matrix.mul_apply, Matrix.add_apply, Matrix.sub_apply, Fin.sum_univ_two, + sigmaZ, sigmaX, Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +/-- **Two-sided spectral form**: the witness's CHSH operator is diagonal, +with `2√2` on the diagonal and `0` elsewhere — every basis vector is an +eigenvector with eigenvalue `2√2`. This is the "two-sided" leg the series +was missing: `Conway.CHSHQuantum.tsirelson_bound` gives `≤ 2√2` in general, +and the central equality `chsh_landau`, made entrywise here, shows the +bound is *attained* — the majorization is an equality, on both sides. -/ +theorem chsh_landau_diagonal (i j : Fin 2) : + CHSHQuantum_en.chshOperator A₀ A₁ B₀ B₁ i j = if i = j then 2 * √2 else 0 := by + rw [chsh_landau] + fin_cases i <;> fin_cases j <;> + simp [Matrix.smul_apply, Matrix.one_apply] + +/-! ### Correlation matrix and Landau's criterion (checked on the witness) -/ + +/-- Reduced correlation matrix of the witness: entry `(i, j)` is the +correlation of the quadruple's observables `Aᵢ` and `Bⱼ`, all equal to +`1/√2` up to sign (entry `(1,1)` carries the `-` sign of the CHSH +operator's `- A₁ * B₁` term). -/ +noncomputable def corrMatrix : Matrix (Fin 2) (Fin 2) ℝ := + !![(√2 : ℝ)⁻¹, (√2 : ℝ)⁻¹; (√2 : ℝ)⁻¹, -(√2 : ℝ)⁻¹] + +/-- The witness's correlation matrix is symmetric — the first half of the +hypothesis of Landau's criterion (1988). -/ +theorem corrMatrix_symm : Matrix.transpose corrMatrix = corrMatrix := by + ext i j + fin_cases i <;> fin_cases j <;> simp [corrMatrix] + +/-- The square of the correlation matrix is the identity: its spectrum is +exactly `{-1, 1}` — the second half of Landau's criterion, checked on the +witness. The general characterization (both directions, for any correlation +matrix) remains declared open. -/ +theorem corrMatrix_sq : corrMatrix * corrMatrix = 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [corrMatrix, Matrix.mul_apply, Fin.sum_univ_two, + Matrix.one_apply] <;> + field_simp <;> + nlinarith [sqrt_two_sq] + +end CHSHLandau_en +end Conway_en