Binary universal block code with logarithmic regret

Open

QAlgorithms.Papers.Independent.Intakethird100.P80.universal_code51

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Fix a finite nonlocality scenario and a normalized setting law $\sigma$ . Let $\mathcal P_\sigma$ be its full family of potential-outcome local trial laws. There exist actual binary prefix block codes $C_n$ on the entire finite trial-word alphabet, a constant $K>0$ , and an integer $N\ge2$ , such that every $n\ge N$ and every word $z^n$ satisfy

|C_n(z^n)|\le\inf_{\pi\in\Pi}\left[-\log_2\prod_{i=1}^n P_{\sigma;\pi}(z_i)\right]+K\log_2 n.

An impossible word has infinite ideal length. The codes also exist for the smaller block lengths; the bound is asymptotic. Both constants are chosen before the block length and the sample word. This is the source's local-family specialization, not a claim for an arbitrary composite statistical class.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P80

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P80

open scoped BigOperators ENNReal Topology Classical

open MeasureTheory Filter

section ProbabilityCoding

/-- PDF p.27, (51), specialized to the local family of pp.29–31: actual binary initialTrials codes
for the FULL alphabet, uniform in n and in the data. Impossible likelihoods have length infinity.
A threshold n>=2 expresses O(log n); both constants precede all n and sample words. -/
theorem universal_code51 (S : BellExperiment) (s : Sigma S) :
    ∃ (C : (n : ℕ) → (Fin n → BellTrial S) → List Bool) (K : ℝ) (N : ℕ),
      0 < K ∧ 2 ≤ N ∧ (∀ n, IsPrefixCode (C n)) ∧
      ∀ n, N ≤ n → ∀ z : Fin n → BellTrial S,
        ENNReal.ofReal ((C n z).length : ℝ) ≤
          (⨅ p : PiLocal S, idealLength (trialJointLaw (localTable p.1) s.1) z) +
          ENNReal.ofReal (K * Real.logb 2 n) := by sorry

end ProbabilityCoding

end QAlgorithms.Papers.Independent.Intakethird100.P80

end

Source

The statistical strength of nonlocality proofs, arXiv:quant-ph/0307125v2, PDF p. 27, Appendix IV-A.3: universal code with logarithmic regret

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every experiment $S$ consisting of a positive finite number of parties, positive finite numbers of settings for each party, and positive finite numbers of outcomes at each party and setting, and for every nonnegative distribution $s$ of total mass $1$ on its joint settings, the following objects exist: a family $C_n$ assigning a finite Boolean word to every length- $n$ trial sample, a real constant $K>0$ , and a natural number $N\ge2$ . Here a trial consists of a joint setting $a$ and an outcome tuple $x$ permitted at $a$ . For every $n\in\mathbb N$ , the map $C_n$ is prefix-free in the precise sense that $C_n(z)$ being a prefix of $C_n(t)$ implies $z=t$ . To state the length bound, let $V$ be the finite set of assignments $v$ prescribing an outcome at every setting of every party, let $\mathcal P(V)$ be its simplex of nonnegative distributions of total mass $1$ , and define

P_p(a,x)=\sum_{\substack{v\in V\\v|_a=x}}p(v),\qquad L_p(z)=\prod_{i=0}^{n-1}s(a_i)P_p(a_i,x_i) \quad\text{for }z_i=(a_i,x_i).

Put $I_p(z)=+\infty$ when $L_p(z)=0$ , and otherwise put $I_p(z)=\max\{0,-\log_2L_p(z)\}$ , embedded in $[0,+\infty]$ . For every natural number $n\ge N$ and every length- $n$ trial sample $z$ , the asserted bound is

|C_n(z)| \le \inf_{p\in\mathcal P(V)} I_p(z) +\max\{0,K\log_2 n\},

with both finite terms interpreted as extended nonnegative real numbers. The prefix condition also applies at $n=0$ , whose sample space has one element, while the length bound applies only for $n\ge N$ . Settings of probability zero are allowed; if every $L_p(z)$ vanishes, the right-hand side of the bound is $+\infty$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph