15 Arithmetic and Quantum-Information Miscellanea (from ONON5213.tex)
Three small, self-contained results mined from the master manuscript ONON5213.tex in the 2026-08-19 session, none previously formalized. Each is genuinely tied to real Mathlib infrastructure (riemannZeta, its Euler product, or elementary trigonometry) — none is restated bare-numeral arithmetic. Session note: this pass also triaged large parts of ONON5213.tex that were not formalized, either because the underlying claim was already covered by an existing file (the bulk of the "Complete Arithmetic Table" and Standard-Model chapters — see DecodingReality.lean, WeylCasimir.lean, PerfectNumbersE8.lean, KappaShadow3.lean, ThreeGenerations.lean, etc.) or because the claim itself does not survive scrutiny (the "Path A" / "Bridge" Riemann-Hypothesis section’s Gram-matrix argument rests on a ratio \(\Lambda (1-s)/\Lambda (s)\) that the functional equation makes identically \(1\) for every \(s\), not a quantity that varies with \(\mathrm{Re}(s)\) as the argument requires) — the latter is recorded privately in Supabase research_notes, per this project’s standing rule against cataloguing manuscript errors in the public tree.
For every \(n \geq 1\), the Dirichlet eta function \(\eta (s) = (1-2^{1-s})\zeta (s)\) satisfies \(\eta (2n)/\zeta (2n) = 1 - 2^{1-2n}\), unconditionally (requires \(\zeta (2n) \neq 0\), from riemannZeta_ne_zero_of_one_le_re). The concrete instance \(\eta (4)/\zeta (4) = 7/8\) (eta_four_div_zeta_four’) and the explicit value \(\eta (4) = 7\pi ^4/720\) (eta_four_eq, via riemannZeta_four) are also proved.
Honest boundary: the physical identification of this ratio with a fermion/boson thermal-capacity ratio in \(3{+}1\) dimensions is not formalized — only the arithmetic value.
The partial products \(\prod _{p {\lt} n}(1-p^{-2})\) over primes converge to \(6/\pi ^2 = 1/\zeta (2)\), obtained by inverting Mathlib’s convergent Euler product \(\prod _{p{\lt}n}(1-p^{-2})^{-1} \to \zeta (2)\) (riemannZeta_eulerProduct) term-by-term and evaluating via riemannZeta_two.
Honest boundary: the physical identification \(\alpha /\pi ^2 = (\alpha /6)\prod _p(1-p^{-2})\) with the fine-structure constant is not formalized — only the underlying arithmetic identity both rest on.
At the angle configuration \(\theta _{ab}=0,\ \theta _{ab'}=\pi /2, \theta _{a'b}=\theta _{a'b'}=\pi /4\), the CHSH combination \(S = E(a,b)-E(a,b')+E(a',b)+E(a',b')\) with \(E(\theta )=-\cos \theta \) evaluates exactly to \(-1-\sqrt2\) (chshValue_eq), so \(|S| = 1+\sqrt2 {\gt} 2\), exceeding the classical bound, while respecting Tsirelson’s bound \(|S|\le 2\sqrt2\) (chshValue_within_tsirelson_bound). Separately, ckw_forces_zero_concurrence formalizes the elementary consequence of the CKW monogamy inequality: given \(1+x^2 \le y^2 \le 1\), necessarily \(x=0\).
Honest boundary: this is standard textbook CHSH/CKW material, not GPP-specific; the source’s stronger claim that Haar measure on \(\mathrm{Gr}(2,4)\) forces exactly the Tsirelson bound is not formalized, nor is the general quantum correlation-function formalism — only the source’s own explicit numerical evaluation.