Motivation

Most Markovian queueing models have no closed-form transient solution. The M/M/1 queue already needs modified Bessel functions (Chapter 2 of the book), and a finite-capacity or multi-class model with state-dependent rates has no closed form at all. What an analyst can always write down is the system of forward equations $p'(t)=p(t)Q$ for the state probabilities. Chapter 8 of Gross, Shortle, Thompson and Harris, Fundamentals of Queueing Theory (4th ed., Wiley 2008, DOI 10.1002/9781118625651), presents two numerical techniques that turn such models into numbers: the randomization (or uniformization) method for the transient distribution of a finite continuous-time Markov chain, and the Fourier-series method for inverting a Laplace transform, as needed for the M/G/1 waiting-time transform (5.33) and the busy-period transform (5.37).

Uniformization goes back to Jensen (1953) and is the standard transient solver in performance-evaluation and reliability tools. Its appeal is that it replaces a matrix exponential, which is numerically delicate, by powers of a stochastic matrix weighted by Poisson probabilities, with an error bound that can be fixed before the computation starts (Grassmann 1977; Gross and Miller 1984). The Fourier-series method with Euler summation is due to Abate and Whitt (Abate and Whitt 1992; Abate, Choudhury and Whitt 1999).

Setting

A continuous-time Markov chain $X(t)$ on the states $\{0,1,\dots,N\}$ is described by its infinitesimal generator $Q=(q_{ij})$: for $i\ne j$, $q_{ij}\ge0$ is the rate of jumps from $i$ to $j$, and the diagonal entry is $-q_i$ with

$$q_i=\sum_{j\ne i}q_{ij},\qquad i=0,1,\dots,N.$$

The transient state-probability vector $p(t)=(p_0(t),\dots,p_N(t))$, $p_n(t)=\Pr\{X(t)=n\}$, is the solution of the forward equations

$$p'(t)=p(t)Q\quad(t\ge0),$$

started from a given probability vector $p(0)$. Fix a constant $\Lambda>0$ with $\Lambda\ge q_i$ for every $i$ (the book takes $\Lambda=\max_i q_i$) and define the uniformized matrix

$$\tilde P=\frac{Q}{\Lambda}+I,\qquad \tilde p_{in}=\begin{cases}q_{in}/\Lambda&(i\ne n),\\1-q_i/\Lambda&(i=n).\end{cases}$$

It is the transition matrix of a discrete-time chain $Y_k$: the state of $X$ after the $k$-th event of a Poisson process of rate $\Lambda$ that has been thinned. Write $\phi^{(k)}=p(0)\tilde P^{k}$ for its distribution after $k$ steps.

For the second half of the chapter, the Laplace transform of a real function $f$ on $[0,\infty)$ is $\bar f(s)=\int_0^\infty e^{-st}f(t)\,dt$, and the Fourier-series approximant with parameter $A$ is

$$f_{A,n}(t)=\frac{e^{A/2}}{2t}\Big[\bar f\Big(\frac{A}{2t}\Big)+2\sum_{k=1}^{n}(-1)^k\,\mathrm{Re}\,\bar f\Big(\frac{A+2k\pi i}{2t}\Big)\Big],$$

with $f_A(t)=\lim_{n\to\infty}f_{A,n}(t)$.

Formalization targets

Goal: the randomization formula with its truncation bound (Eqs. (8.9)–(8.12))

The forward equations have a solution, and every solution satisfies, for all $t\ge0$,

$$p(t)=\sum_{k=0}^{\infty}p(0)\tilde P^{(k)}\,\frac{e^{-\Lambda t}(\Lambda t)^k}{k!},$$

and whenever $\sum_{k=0}^{T}e^{-\Lambda t}(\Lambda t)^k/k!>1-\epsilon$, every component of the sum truncated at $k=T$ is within $\epsilon$ of $p_n(t)$.

Milestones

1. Eq. (8.12): $\tilde P$ has the entries above and is a stochastic matrix.
2. Eqs. (8.13)–(8.14): $\phi^{(k)}=\phi^{(k-1)}\tilde P$ and each $\phi^{(k)}$ is a probability vector.
3. p.385: $\phi=\phi\tilde P\iff0=\phi Q$.
4. Eqs. (8.27)–(8.28): for bounded Lipschitz $f$, $A>0$ and $t>0$,

$$f_A(t)-f(t)=\sum_{k=1}^{\infty}e^{-kA}f\big((2k+1)t\big),\qquad |f_A(t)-f(t)|\le\frac{Ce^{-A}}{1-e^{-A}}\ \text{ if } |f(x)|\le C \text{ for } x>3t.$$

The mission also contains Eqs. (8.7)–(8.8) as a further theorem, outside the milestone list: the transition probabilities satisfy $p_{in}(t)=\sum_k\tilde p^{(k)}_{in}e^{-\Lambda t}(\Lambda t)^k/k!$, and $p_n(t)=\sum_i p_i(0)p_{in}(t)$.

Significance

The randomization formula reduces the transient analysis of any finite Markovian queue (finite-buffer, multi-server, with balking, reneging or state-dependent rates) to repeated vector–matrix products with a sparse stochastic matrix. The truncation point is chosen from a Poisson tail alone, independently of $Q$. Milestone 3 shows that the same matrix gives the stationary equations, so one iteration serves both transient and steady-state computation. The discretization identity (8.27) is what justifies the parameter choice in Algorithm 8.1: the error decays like $e^{-A}$.

All of these results are classical and proved in the literature. None of them is formalized in Lean or Mathlib as far as a search of the platform and Mathlib shows. Mathlib has the matrix exponential and Poisson summation under decay hypotheses, but no continuous-time Markov chain generators, no uniformization, and no Laplace transform. This mission would add the finite-state link between generators, stochastic matrices and matrix exponentials that later chapters of queueing and reliability theory use, and a verified error formula for a numerical inversion method in wide use.

Difficulty

The book's derivation is probabilistic: it conditions on the number of events of the Poisson($\Lambda$) process and thins them. A formal statement cannot rest on that picture, because $p(t)$ is defined analytically, by the forward equations. The goal therefore contains a uniqueness statement for a linear ODE on $[0,\infty)$ with one-sided derivative at $0$, which the book never mentions. The componentwise bound then needs $\tilde P$ to be stochastic, so that every $\phi^{(k)}_n$ lies in $[0,1]$. That is exactly where $\Lambda\ge\max_i q_i$ is used; with a smaller $\Lambda$ the matrix $\tilde P$ has negative diagonal entries and the bound fails.

For (8.27), the book gives no proof. The identity is an aliasing (Poisson-summation) formula for a periodic function assembled from the values of $f$ at all odd multiples of $t$. The convergence of the conditionally summed series (8.24) is the delicate point: continuity of $f$ at $t$, the book's only hypothesis, does not guarantee convergence of a Fourier series. Mathlib's Poisson summation theorems require decay of the Fourier transform that the damped, reflected function built from $f$ does not have.

Formalization scope

• States are Fin (N+1); a row vector is Fin (N+1) → ℝ; $pQ$ is vecMul. A generator is a real matrix with nonnegative off-diagonal entries and diagonal $-\sum_{j\ne i}q_{ij}$.
• $p(t)$ is not defined as the series. It is any function with $p(0)=p_0$ and one-sided derivative $p(t)Q$ within $[0,\infty)$ at every $t\ge0$. The goal also asserts that such a function exists, so it cannot hold vacuously, and it asserts the series identity for every solution. Defining $p(t)$ as the series (8.9) would make the goal a tautology and is ruled out.
• $\Lambda$ is any real with $\Lambda>0$ and $\Lambda\ge q_i$ for all $i$ (the book takes equality with $\max_i q_i$).
• The truncation bound is stated componentwise, as on p.384 ("an error bound on $p_n(t)$ of $\epsilon$"), for an arbitrary real $\epsilon$ and truncation point $T$.
• The series (8.8), (8.9) are stated with HasSum, so convergence is part of the claim.
• The Laplace transform is the Lebesgue integral over $(0,\infty)$ at a complex argument. $f_A(t)$ is the limit of the partial sums $f_{A,n}(t)$, and the convergence is part of milestone 4.
• Strengthened hypotheses in milestone 4: $f$ bounded and Lipschitz on $[0,\infty)$ replaces "$t$ is a continuity point of $f$", which is not sufficient for convergence.
• Corrected misprints: $e^{-\lambda t}$ in (8.9) is $e^{-\Lambda t}$; $q_{ij}/\Lambda$ in (8.12) is $q_{in}/\Lambda$; $\phi(Q/\Lambda-I)$ on p.385 is $\phi(Q/\Lambda+I)$.
• Not formalized: Theorem 8.1 (Bromwich inversion) and the real form (8.21), which the book states without hypotheses on $f$; the limit claim $\lim_k\phi^{(k)}=\lim_t p(t)$ on p.385, which fails when $\tilde P$ is periodic; the Euler-summation approximation (8.26) and the round-off discussion, which are stated with "≈".

Useful infrastructure: the matrix exponential and its derivative (Matrix, NormedSpace.exp), uniqueness for linear ODEs (Grönwall), Fourier series on the circle, and a reusable Laplace transform file. Contributions of general lemmas on generators and stochastic matrices are welcome, as they apply to every finite Markovian model in the series.

Selected references

• D. Gross, J. F. Shortle, J. M. Thompson, C. M. Harris, Fundamentals of Queueing Theory, 4th ed., Wiley, 2008, §§8.1.2–8.2. https://doi.org/10.1002/9781118625651
• A. Jensen, "Markoff chains as an aid in the study of Markoff processes", Skandinavisk Aktuarietidskrift 36 (1953) 87–91.
• W. K. Grassmann, "Transient solutions in Markovian queueing systems", Computers & Operations Research 4 (1977) 47–53.
• D. Gross, D. R. Miller, "The randomization technique as a modeling tool and solution procedure for transient Markov processes", Operations Research 32 (1984) 343–361. https://doi.org/10.1287/opre.32.2.343
• J. Abate, W. Whitt, "The Fourier-series method for inverting transforms of probability distributions", Queueing Systems 10 (1992) 5–87. https://doi.org/10.1007/BF01158520
• J. Abate, G. L. Choudhury, W. Whitt, "An introduction to numerical transform inversion and its application to probability models", in W. Grassmann (ed.), Computational Probability, Kluwer, 1999, 257–323.

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Chudnovsky's bound.

Formalization target

The campaign template with the value $19.8899945$ filled in: PiIrrationality.UpperBound (19.8899945 : ℝ), i.e. $\mu(\pi) \le 19.8899945$.

Value. The bound is quoted in the literature as $19.8899944\ldots$ (e.g. Hata 1993), a truncation. This entry rounds the last digit up to $19.8899945$ so that the goal follows from the published constant.

How the bound arises

Chudnovsky determined the exact asymptotic behaviour of the Hermite-type contour integrals $\frac{1}{2\pi i}\oint \left(\frac{n!}{z(z-1)\cdots(z-n)}\right)^k e^{wz}\,dz$ behind Mahler's approximations, which sharpens the resulting exponent.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $19.8899945$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• G. V. Chudnovsky, Hermite–Padé approximations to exponential functions and elementary estimates of the measure of irrationality of $\pi$, Lecture Notes in Math. 925, Springer (1982), 299–322.
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

Motivation

The irrationality measure $\mu(\pi)$ is the supremum of the $\mu$ for which $|\pi - p/q| < q^{-\mu}$ has infinitely many rational solutions $p/q$. Every irrational number has $\mu \ge 2$ (Dirichlet), almost every real number has $\mu = 2$, and it is conjectured that $\mu(\pi) = 2$. Known upper bounds:

• Mahler (1953): $42$, the first proof that $\pi$ is not a Liouville number.
• Mignotte (1974): $20.6$.
• Chudnovsky (1982): $19.8899944\ldots$
• Rhin–Viola (1993): $14.797074$.
• Hata (1993): $8.016045\ldots$
• Salikhov (2008): $7.606308\ldots$
• Zeilberger–Zudilin (2020): $7.103205334137\ldots$, the current record.

The campaign's first proved value is Mahler's $42$. This entry records Mignotte's bound.

Formalization target

The campaign template with the value $20.6$ filled in: PiIrrationality.UpperBound (20.6 : ℝ), i.e. $\mu(\pi) \le 20.6$.

Value. The paper's abstract states $|\pi - p/q| > q^{-20.6}$ for all $q \ge 2$, which gives $\mu(\pi) \le 20.6$ exactly as stated. The paper also proves $|\pi - p/q| > q^{-20}$ for $q \ge q_0$ (explicit), so $\mu(\pi) \le 20$ follows from the same source; this entry uses the table value $20.6$.

How the bound arises

Mignotte refined Mahler's method of explicit rational approximations to $\pi$ (Hermite's approximation formulae for the exponential and logarithm) and sharpened the estimates that turn their size and denominators into an irrationality measure.

Significance

Each step down the list replaces Mahler's approximations with a sharper family. Formalizing $20.6$ would build reusable explicit machinery: integral constructions of rational approximations to $\pi$, bounds on their common denominators via prime-number estimates, and the standard lemma turning a sequence of good approximations into an irrationality-measure bound.

Selected references

• M. Mignotte, Approximations rationnelles de $\pi$ et quelques autres nombres, Mém. Soc. Math. France 37 (1974), 121–132. https://doi.org/10.24033/msmf.139
• K. Mahler, On the approximation of $\pi$, Indag. Math. 15 (1953), 30–42.
• F. Beukers, A rational approach to $\pi$, Nieuw Arch. Wiskd. (5) 1 (2000), 372–379.
• Source table: https://teorth.github.io/optimizationproblems/constants/7a.html

This mission formalizes Y. Lodha and J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200 (doi:10.4171/GGD/347; arXiv:1308.4250v3, whose page numbers are used): the group $G_0$ generated by three explicit piecewise projective homeomorphisms of the line is nonamenable and finitely presented, the first torsion-free finitely presented counterexample to the von Neumann–Day problem.

Motivation

A discrete group is amenable when it has a finitely additive invariant probability measure on all its subsets. A group containing a nonabelian free subgroup is not amenable, and von Neumann and Day asked whether the converse holds. The counterexamples found before Monod's work are built from torsion groups by elaborate inductive constructions. Monod (2013) found nonamenable groups without free subgroups among piecewise projective homeomorphisms of the line. Lodha and Moore isolate in Monod's group $H$ a subgroup with three explicit generators and nine explicit relations.

Timeline.

• 1929: von Neumann introduces amenability for groups (Fund. Math. 13, no DOI).
• 1950: Day poses the problem in print, attributing it to von Neumann (doi:10.1090/S0002-9947-1950-0044031-5).
• 1980: Ol'shanskii's counterexample (doi:10.1070/RM1980v035n04ABEH001876); soon after, Adyan shows certain Burnside groups are counterexamples (doi:10.1070/IM1983v021n03ABEH001799).
• 2003: Ol'shanskii and Sapir, the first finitely presented counterexample (doi:10.1007/s10240-002-0006-7); Ivanov gives another in 2005 (doi:10.1007/s10711-004-2826-8). Both are torsion-by-cyclic.
• 2013: Monod's groups $H(A)$ of piecewise projective homeomorphisms, nonamenable without free subgroups (doi:10.1073/pnas.1218426110); formalized on this platform in the Monod mission.
• 2016: Lodha and Moore, a torsion-free finitely presented counterexample (doi:10.4171/GGD/347).
• 2020: Lodha, a nonamenable group of type $F_\infty$ in the same family (doi:10.1112/topo.12172).

Setting

The generators act on the real line: $a(t) = t + 1$, and $b$, $c$ are the piecewise projective maps of p. 2 (aFun, bFun, cFun). As homeomorphisms of the projective line $\mathbb R \cup \{\infty\}$ (a, b, c) they generate $G_0$ (G0), inside the group where the published Monod bundle defines $H$ (Monod.Hpp).

Lodha and Moore move to infinite binary sequences through the continued-fraction map $\Phi$ (Phi), under which $a$, $b$, $c$ become functions $x$, $x_1$, $y_{10}$ of sequences (Proposition 3.1). There $x_s$ and $y_s$ are $x$ and $y$ acting on the sequences that extend $s$. $G$ is the group generated by all $x_s$ and $y_s$, $G_0$ the group generated by the $x_s$ and the $y_s$ with $s$ not constant, and $R$ the five families of relations (1)–(5) among them. Products are taken left to right, as in the paper.

Section 5 rewrites words in the generators by explicit substitutions into standard forms and sufficiently expanded standard forms, and tracks them through strings in $0$, $1$, $y$, $y^{-1}$; these notions form the second definitions bundle.

Formalization targets

Goal: Theorem 1.1

$$\neg\,\text{IsAmenable}(G_0) \ \wedge\ G_0 \text{ is finitely presented}.$$

Milestones

• Nonamenability (§2): Lodha and Moore's definition of a $\mu$-amenable equivalence relation, with its equivalence to amenability (Connes, Feldman and Weiss, whose theorem is published as ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel) as two milestones; Theorems 2.1 (Zimmer) and 2.2 (Carrière and Ghys) as printed; the group $K = \langle t+1, 2t, -1/t\rangle$; and the identities and orbit comparison of p. 4.
• Presentations (§3): Proposition 3.1, the identification of $a$, $b$, $c$ with $x$, $x_1$, $y_{10}$, the relations (1)–(5), the presentation of $F$ they contain, Propositions 3.4 and 3.5, the reduction to a finite presentation, the three-generator presentation of $G_0$, and Theorem 3.3.
• Section 5: Lemmas 5.2, 5.3, 5.4, 5.6, 5.9, 5.10 and 5.11.

Significance

The result. $G_0$ settles the finitely presented von Neumann–Day problem with a group that is torsion-free, has explicit generators and relations, and acts by piecewise projective maps, so its elements can be described by labeled tree diagrams much as those of Thompson's group $F$. It shows that $\langle a, b, c\rangle$ shares the combinatorics of $F$ without its unresolved amenability question.

Formalizing it. Before this mission none of the paper was formalized. The Monod mission's milestones supply the setting, and the case of Carrière and Ghys that Monod uses is already proved there by an elementary argument (Monod.not_isAmenableRel_mob).

Difficulty

Nonamenability is a short reduction to Theorem 2.2, which in general is deep. Finite presentation is the bulk: one must show that every word that evaluates to the identity can be reduced to an $X$-word by the substitutions of §5, through a well-founded ordering on standard forms (Lemma 5.6) and an analysis of how $y$ acts on binary expansions (Lemmas 5.9–5.11).

Formalization scope

Lean representation and conventions.

• Sequences are List Bool (finite) and Stream' Bool (infinite). $x$ is explicit; $y$ and $y^{-1}$ are defined by the recursion of p. 5, digit by digit.
• The groups on sequences are subgroups of the opposite of the permutation group of Stream' Bool, so that products are left to right as in the paper. Statements about $a$, $b$, $c$ take products in the opposite of the homeomorphism group for the same reason.
• a, b, c are the homeomorphisms that agree with the formulas on $\mathbb R$, and toSeqGroup turns a bijection of sequences into a group element. Both fall back to the identity for a function that is not a homeomorphism or a bijection. Every generator is in fact one, so the fallback is never reached, and a trivial group would make the goal false.
• $\phi$ is a limit of finite continued fractions; its defining equations are a milestone.
• $K$ is a subgroup of $\mathrm{PSL}_2(\mathbb R)$ (Matrix.ProjectiveSpecialLinearGroup, with the quotient topology), as on p. 4; a class acts on the projective line by the Möbius map of either of its matrices, through the published Monod bundle.

What is left out, and deviations.

• §4 (labeled tree diagrams) is not formalized: the paper calls it "not essential for understanding the proof", and its claims are left to the reader. Remark 3.2 (history) is left out, as are two remarks in the introduction: Thurston's unpublished result that $\langle a, b\rangle$ is a copy of Thompson's group $F$ (on this platform as Monod's published theorem that $H_{\mathbb Q}(\mathbb Z) \cong F$) and the assertion that $t \mapsto t + 1/2$ and $b$ generate a nonamenable group.
• Lodha and Moore's definition of a $\mu$-amenable relation is read with the action of $\mathbb Z$ Borel; read literally, every equivalence relation with countable classes would be $\mu$-amenable (the note on the definitions explains; CountableOrbit.exists_perm_rel_iff_exists_zpow_eq is the underlying fact).
• In the three-generator presentation of p. 7, the fourth and ninth relations as printed in $a$, $b$, $c$ do not hold in $G_0$ (LodhaMoorePrinted.printed_relations_four_and_nine_ne); the milestone uses the translations of the relations in $x_s$, $y_s$ that they come from.
• The substitutions of p. 9 include the rule for $y_s^{-1}$ that the proof of Lemma 5.2 uses and the paragraph before Lemma 5.6 writes out (without it Lemmas 5.2 and 5.4 fail: it is the only substitution that applies to $y_s^{-1}$, LodhaMoorePrinted.eq_of_step_singleton_y_neg_one), and allow commuting $y_u^i$ and $y_v^j$ for any exponents, as the proof of Lemma 5.6 does (with commuting only for positive exponents, Lemma 5.6 fails: LodhaMoorePosCommute.not_forall_exists_derives_sufficientlyExpanded).
• Theorems 2.1 and 2.2 and the Connes–Feldman–Weiss equivalence are cited results, stated as Lodha and Moore apply them; the direction of the equivalence from their definition to the standard one is the easy one. Both directions assume the setting of Connes, Feldman and Weiss: a $\sigma$-finite measure, quasi-invariant for the relation.

What a development needs. Monod's mission supplies $H$, its lack of free subgroups, the elementary non-amenability argument for $\mathrm{SL}_2(A)$ with $A$ dense, and the passage from an amenable group to an amenable orbit relation. The theorem of Connes, Feldman and Weiss is published and proved (ConnesFeldmanWeiss.exists_nonsingular_generator_of_isAmenableRel); it gives the hard direction of the equivalence. The presentation of Thompson's group $F$ is published by the Cannon–Floyd–Parry mission on the two presentations of Thompson's group $F$. Proofs of any milestone are welcome.

Selected references

• Y. Lodha, J. T. Moore, A nonamenable finitely presented group of piecewise projective homeomorphisms, Groups Geom. Dyn. 10 (2016) 177–200. doi:10.4171/GGD/347
• N. Monod, Groups of piecewise projective homeomorphisms, Proc. Natl. Acad. Sci. USA 110 (2013) 4524–4527. doi:10.1073/pnas.1218426110
• A. Connes, J. Feldman, B. Weiss, An amenable equivalence relation is generated by a single transformation, Ergodic Theory Dynam. Systems 1 (1981) 431–450. doi:10.1017/S014338570000136X
• R. J. Zimmer, Amenable ergodic group actions and an application to Poisson boundaries of random walks, J. Funct. Anal. 27 (1978) 350–372. doi:10.1016/0022-1236(78)90013-7
• Y. Carrière, É. Ghys, Relations d'équivalence moyennables sur les groupes de Lie, C. R. Acad. Sci. Paris Sér. I Math. 300 (1985) 677–680 (no DOI).
• J. Belk, Thompson's group F, PhD thesis, Cornell University, 2004 (no DOI). arXiv:0708.3609
• J. W. Cannon, W. J. Floyd, W. R. Parry, Introductory notes on Richard Thompson's groups, L'Enseignement Math. (2) 42 (1996) 215–256. doi:10.5169/seals-87877

Motivation

This is the second mission of the series on Assumptions of Physics by G. Carcassi and C. A. Aidala (book, v3.0, 2025), formalizing Part II, Chapter 2, "Domain combination and relationships". The chapter asks when the outcome of one experiment can be inferred from another (e.g. temperature from the height of a mercury column), and shows that such inference relationships between verifiable statements correspond to causal relationships between possibilities, which are continuous maps of the natural topologies. It builds on the definitions of the first mission (Assumptions of Physics I), which must be launched first because this mission imports its definition file.

Setting

Statements are truth sets $s\subseteq\Omega$ over the possible assignments $\Omega$ of a fixed logical context; an experimental domain $\mathcal D$, its possibilities $X$, verifiable sets $U(s)$ and natural topology are as in mission I. An inference relationship from $\mathcal D_Y$ to $\mathcal D_X$ is a map $r:\mathcal D_Y\to\mathcal D_X$ with $r(s)\equiv s$; $\mathcal D_Y$ depends on $\mathcal D_X$ if one exists, and two domains are equivalent if each depends on the other. A causal relationship is a function $f:X\to Y$ between possibilities with $x\preccurlyeq f(x)$. The combined domain of a countable family of domains is generated by all their statements under finite conjunction and countable disjunction.

Formalization targets

Goal (Theorem 2.10, Experimental Relationship Theorem, with continuity made explicit)

$$\mathcal D_Y\subseteq\mathcal D_X \iff \exists\, f:X\to Y \text{ continuous with } x\preccurlyeq f(x)\ \forall x\in X.$$

Milestones

• Corollary 2.3: a sub-domain depends on the domain.
• Corollary 2.5: domain equivalence is an equivalence relation.
• Corollary 2.9: a causal relationship is unique if it exists.
• Corollary 2.11: $\mathcal D_X\equiv\mathcal D_Y$ iff there is a homeomorphism $f:X\to Y$ with $x\equiv f(x)$.
• Proposition 2.14: the possibilities of a combined domain are the non-impossible conjunctions $\bigwedge_i x_i$ of possibilities $x_i\in X_i$.

Significance

Theorem 2.10 is what justifies describing experimental relationships by functions between possibilities rather than by maps between all finite-precision statements, and Corollary 2.11 identifies equivalence of experimental domains with homeomorphisms that respect the statements. Later chapters use these to transport structure between equivalent domains. The results are proved informally in the book; no machine-checked formalization is known to the drafters.

Difficulty

The forward direction requires showing that each possibility of $\mathcal D_X$ lies inside exactly one possibility of $\mathcal D_Y$ and that preimages of verifiable sets are verifiable. The converse is subtler: Definition 2.7 does not require continuity, and the book's Corollary 2.8 ("all causal relationships are continuous") does not hold in general. For example, with $\Omega=\{0,1\}$, $\mathcal D_X=\{\emptyset,\{1\},\Omega\}$ and $\mathcal D_Y=\{\emptyset,\{0\},\Omega\}$, the identity on possibilities is a causal relationship but $\mathcal D_Y\not\subseteq\mathcal D_X$. The goal therefore includes continuity of $f$ explicitly. That is the hypothesis the book's proof of the converse actually uses.

Formalization scope

Domains are ExperimentalDomain Ω on a common type Ω; dependence is ExperimentalDomain.DependsOn (existence of an equivalence-preserving map, which here is the inclusion $\mathcal D_Y\subseteq\mathcal D_X$), causal relationships are predicates IsCausalRel on functions between the possibility types, and topological notions are Mathlib's (Continuous, ≃ₜ). The combined domain ExperimentalDomain.combined takes a family over an arbitrary countable index type. Theorem 2.12 (transport of structure) is informal in the source and is not formalized here. Propositions 2.15–2.28 are left out: the residual possibility depends on the choice of basis, and Proposition 2.18 appears to need a stronger independence hypothesis than Definition 2.17 provides. They are candidates for a later mission.

Selected references

• G. Carcassi, C. A. Aidala, Assumptions of Physics, Ver. 3.0, December 31, 2025. https://assumptionsofphysics.org/book — Part II, Chapter 2 "Domain combination and relationships", pp. 149–168.

We formalize the equivalence between Turing machines and the WordRAM model of computation. Turing machines are the standard model for studying computability, but algorithms are rarely described in terms of tape operations. WordRAM is much closer to assembly, with memory accesses, arithmetic instructions, branches, and loops. The goal is to connect this familiar way of expressing algorithms to the foundations of computability. This will also bring us closer to one day formalizing Fine Grained Complexity.

The formal target is halting equivalence through simulations in both directions, with the stated memory bounds and a family of word widths, each fixed during a run.

References:

• Stephen A. Cook and Robert A. Reckhow. Time Bounded Random Access Machines. Journal of Computer and System Sciences 7(4), 354–375, 1973.
• Torben Hagerup. Sorting and Searching on the Word RAM. STACS 1998, 366–398.

Motivation

A basic question of combinatorial geometry asks when a family of sets can be pierced (or stabbed) by few points. For intervals on the real line the answer is classical: if every two of finitely many closed intervals intersect, one point meets all of them, namely the rightmost left endpoint. This is the one-dimensional case of Helly's theorem. The situation changes as soon as the sets are allowed to have holes. Unions of two intervals can intersect pairwise without any point being common to three of them, so no single point suffices, and it is not obvious that any bound depending only on the number of holes exists.

This mission formalizes the answer given in Section 8.6 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer, 2007): pairwise intersecting unions of $d$ intervals can always be pierced by $2d^2$ points. The section uses the result to illustrate a general method of combinatorics, in which a linear programming relaxation of a covering problem is bounded through LP duality and then rounded. The same scheme, a bound on the fractional transversal number followed by a rounding step, appears across discrete geometry and combinatorial optimization.

Timeline.

• 1970: Gyárfás and Lehel prove that a bound depending only on $d$ exists; their bound is exponential in $d$ (A Helly-type problem in trees, in Combinatorial Theory and its Applications, North-Holland).
• 1992: Alon and Kleitman solve the Hadwiger–Debrunner $(p,q)$-problem with a method combining fractional transversals and LP duality (Adv. Math. 96).
• 1997: Kaiser proves the bound $d^2$ using algebraic topology (Discrete Comput. Geom. 18).
• 1998: Alon gives the short LP-duality proof of the bound $2d^2$ formalized here (Discrete Comput. Geom. 19).
• 2001: Matoušek shows that the transversal number cannot in general be below a constant multiple of $d^2/\log d$ (Discrete Comput. Geom. 26).

Setting

Fix an integer $d \ge 1$. A $d$-interval is a union of $d$ closed intervals on the real line,

$$J = [a_1,b_1] \cup \dots \cup [a_d,b_d], \qquad a_k \le b_k .$$

The numbers $a_k$ and $b_k$ are the endpoints of $J$. A finite family $\mathcal J$ of $d$-intervals is pairwise intersecting if $J_1 \cap J_2 \ne \emptyset$ for all $J_1, J_2 \in \mathcal J$. A set $X$ of real numbers is a transversal of $\mathcal J$ if every $J \in \mathcal J$ contains a point of $X$.

More generally, for a finite set $V$ and a system $\mathcal F$ of subsets of $V$: a transversal is a set $X \subseteq V$ meeting every member; the transversal number $\tau(\mathcal F)$ is the smallest size of a transversal; a matching is a subsystem of pairwise disjoint members, and the matching number $\nu(\mathcal F)$ is the largest size of a matching. The fractional transversal number $\tau^*(\mathcal F)$ is the optimal value of the linear program

$$\min \sum_{v\in V} x_v \quad \text{s.t.} \quad \sum_{v \in F} x_v \ge 1 \ (F \in \mathcal F),\ x \ge 0,$$

and the fractional matching number $\nu^*(\mathcal F)$ is the optimal value of

$$\max \sum_{F\in\mathcal F} y_F \quad \text{s.t.} \quad \sum_{F :\, v \in F} y_F \le 1 \ (v \in V),\ y \ge 0 .$$

Formalization targets

Goal: Theorem 8.6.1

$$\mathcal J \text{ finite, pairwise intersecting family of } d\text{-intervals} \;\Longrightarrow\; \exists X \subset \mathbb R,\ |X| \le 2d^2,\ X \cap J \ne \emptyset \ \ \forall J \in \mathcal J .$$

This is the book's theorem with its constant $2d^2$.

Milestones

1. Lemma 8.6.2. If $J_1,\dots,J_n$ ($n \ge 1$, repetitions allowed) are $d$-intervals with $J_i \cap J_j \ne \emptyset$ for all $i,j$, then some endpoint of some $J_i$ lies in at least $n/2d$ of the $J_j$.
2. §8.6, p. 182. For every finite set system with nonempty members,

$$\nu(\mathcal F) \le \nu^*(\mathcal F) = \tau^*(\mathcal F) \le \tau(\mathcal F).$$

3. Lemma 8.6.3. If $\mathcal J$ is a finite pairwise intersecting family of $d$-intervals and $P$ its set of endpoints, there are weights $x_p \ge 0$, $p \in P$, with $\sum_{p \in J \cap P} x_p \ge 1$ for every $J \in \mathcal J$ and $\sum_{p\in P} x_p \le 2d$.

Significance

The result. Theorem 8.6.1 shows that the piercing number of pairwise intersecting $d$-intervals is bounded by a function of $d$ alone, and that this function is polynomial. The section also states, without proof, the extension $\tau(\mathcal J) \le 2d^2\,\nu(\mathcal J)$ for arbitrary finite families of $d$-intervals. Upper bounds of this kind feed into piercing and hitting-set questions for families with bounded "complexity", and the chain $\nu \le \nu^* = \tau^* \le \tau$ is the standard frame in which such bounds are proved.

Formalizing it. The theorem, both lemmas and the duality chain are proved in the literature and in the book. None of them is on the platform. The work consists of formalizing the book's proof: a double-counting argument, LP duality for the pair of fractional programs together with the rationality of an optimal basic solution, and a rounding step. The general-set-system milestone is reusable for any transversal problem, independent of $d$-intervals.

Difficulty

The obvious generalization of the one-dimensional argument fails: for $d \ge 2$ no point need be common to all members, so there is no single extremal endpoint to choose, and a greedy piercing procedure has no control over how many points it uses. The difficulty is to obtain a bound that does not depend on the size of the family. In the book's route the counting statement of Lemma 8.6.2 holds only for equal weights, while the fractional programs produce arbitrary real weights, and the passage between the two, as well as the passage from a fractional transversal of small total weight to an actual finite set of points, are the steps that need care.

Formalization scope

A $d$-interval is stored as data: two functions left, right : Fin d → ℝ with left k ≤ right k, together with the set toSet $= \bigcup_k [a_k,b_k]$. Components are indexed $0,\dots,d-1$. Endpoints are those of the given components, so they depend on the representation, as in the book's proofs. Families are Finsets of such data; Lemma 8.6.2 uses a Fin n-indexed sequence, since the proof of Lemma 8.6.3 applies it to a sequence with repetitions. The hypotheses $d \ge 1$ (the book's definition) and, in Lemma 8.6.2, $n \ge 1$ are explicit. The quantity $n/2d$ is real division. Transversal sizes are cardinalities of a Finset ℝ bounded by $2d^2$.

For set systems, $V$ is a finite type and $\mathcal F$ a Finset (Finset V) with nonempty members; without this assumption no transversal exists and both fractional programs degenerate. The numbers $\tau^*$ and $\nu^*$ are expressed through optimal feasible solutions, not as infima or suprema, so no junk value of an empty or unbounded set is involved. $\tau$ is an sInf over $\mathbb N$ that is attained under the nonemptiness assumption, and $\nu$ is a maximum over the finite family of matchings.

A trivializing formalization is ruled out: the pairwise-intersection hypothesis is satisfiable by nonempty families, the transversal is required to meet the actual sets $J$, not a representation artifact, and the bound $2d^2$ and $2d$ are the book's constants, not weakened ones.

Needed infrastructure: finite sums over Finset ℝ, LP duality for a finite primal–dual pair in inequality form (or a direct proof of the chain), rationality of an optimal vertex, and a left-to-right sweep over a sorted finite set of reals. Contributions of a general LP duality statement for set-system relaxations are welcome and reusable.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.6. https://doi.org/10.1007/978-3-540-30717-4
• N. Alon, Piercing d-intervals, Discrete Comput. Geom. 19 (1998) 333–334.
• N. Alon, D. Kleitman, Piercing convex sets and the Hadwiger–Debrunner (p, q)-problem, Adv. Math. 96 (1992) 103–112.
• T. Kaiser, Transversals of d-intervals, Discrete Comput. Geom. 18 (1997) 195–203.
• J. Matoušek, Lower bounds on the transversal numbers of d-intervals, Discrete Comput. Geom. 26 (2001) 283–287.
• A. Gyárfás, J. Lehel, A Helly-type problem in trees, in Combinatorial Theory and its Applications (P. Erdős, A. Rényi, V. T. Sós, eds.), North-Holland, 1970, 571–584.

Motivation

A deep-space probe sends a vector $w\in\mathbb{R}^k$ encoded as $z=Qw\in\mathbb{R}^n$, and up to about 8% of the transmitted numbers may be corrupted arbitrarily. Section 8.5 of Matoušek and Gärtner's Understanding and Using Linear Programming (Springer 2007, DOI 10.1007/978-3-540-30717-4) shows that decoding reduces to finding a sparse solution of an underdetermined linear system $Ax=b$, and that under suitable conditions this sparse solution is found exactly by a single linear program. The same problem arises in signal processing (sparse representations in redundant wavelet dictionaries) and in computer tomography, and it is the core of what became known as compressed sensing.

Timeline, as recorded in the book's references:

• 1999: Chen, Donoho and Saunders introduce basis pursuit, minimizing the $\ell_1$-norm subject to $Ax=b$ (SIAM J. Sci. Comput. 20).
• 2005: Candès, Rudelson, Tao and Vershynin prove that for every $\alpha\in(0,1)$ there is $\beta(\alpha)>0$ such that a random $\lfloor\alpha n\rfloor\times n$ matrix is exact for $\lfloor\beta n\rfloor$-sparse vectors with probability exponentially close to 1 (FOCS 2005).
• 2006: Donoho, via neighborliness of centrally symmetric polytopes, obtains the constants $\alpha=0.75$, $\beta=0.08$ used in the book, and shows that no $\lfloor 0.75n\rfloor\times n$ matrix is exact for $r>0.25n$ when $n$ is large (Discrete Comput. Geom. 35).
• 2006: Linial and Novik prove further upper bounds showing that these existence results are asymptotically optimal (Discrete Comput. Geom. 36).

Setting

Let $A$ be a real $m\times n$ matrix with $m<n$ and $b\in\mathbb{R}^m$. The support of $x\in\mathbb{R}^n$ is $\operatorname{supp}(x)=\{i: x_i\ne 0\}$. For an integer $r\ge 0$, a sparse solution of $Ax=b$ is an $x$ with $Ax=b$ and $|\operatorname{supp}(x)|\le r$. The $\ell_1$-norm is $\|x\|_1=|x_1|+\dots+|x_n|$.

Basis pursuit is the optimization problem

$$\text{(BP)}\qquad\text{minimize } \|x\|_1\ \text{ subject to } x\in\mathbb{R}^n,\ Ax=b,$$

which is equivalent to the linear program

$$\text{(BP}'\text{)}\qquad\text{minimize } u_1+\dots+u_n\ \text{ subject to } Ax=b,\ -u\le x\le u,\ u\ge 0 .$$

The matrix $A$ is BP-exact for $r$ if for every $b\in\mathbb{R}^m$: whenever $Ax=b$ has a solution $\tilde x$ with at most $r$ nonzero components, $\tilde x$ is the unique optimal solution of (BP). The crosspolytope is $B^n_1=\{x:\|x\|_1\le 1\}$, the kernel of $A$ is $L=\{x: Ax=0\}$, and $L+z=\{\ell+z:\ell\in L\}$. For $z$ with $\|z\|_1=1$, the cone at $z$ is $C_z=\{t(x-z): t\ge 0,\ x\in B^n_1\}$, and $L$ is good for $z$ if $(L+z)\cap B^n_1=\{z\}$.

Formalization targets

Goal: Lemma 8.5.4 (reformulation of BP-exactness)

For $m<n$ and $r\le m$:

$$A \text{ is BP-exact for } r\iff \forall z\in\mathbb{R}^n\ \text{with}\ \|z\|_1=1,\ |\operatorname{supp}(z)|\le r:\quad (L+z)\cap B^n_1=\{z\}.$$

This is the book's geometric characterization of exact recovery, and the statement on which the known probabilistic proofs are built.

Milestones

1. Observation 8.5.1: $Ax=b$ has at most one sparse solution for every $b$ if and only if every $2r$ or fewer columns of $A$ are linearly independent.
2. The remark after it (p. 169): under $m<n$, that column condition forces $m\ge 2r$.
3. Equivalence of (BP) and (BP′) (p. 170): in every optimal solution of (BP′), $u_i=|x_i|$; and $x$ is optimal for (BP) iff $(x,|x|)$ is optimal for (BP′).
4. From the proof of Lemma 8.5.4 (p. 173): if $Az=b$, the solution set of $Ax=b$ is exactly $L+z$.
5. From "Intuition for BP-exactness" (p. 174): for $\|z\|_1=1$ and $|\operatorname{supp}(z)|\le r$, $L$ is good for $z$ iff $L\cap C_z=\{0\}$.

Further draft item: Theorem 8.5.2

With $m=\lfloor 0.75n\rfloor$, $r=\lfloor 0.08n\rfloor$ and $A$ an $m\times n$ matrix of independent $N(0,1)$ entries, there is a constant $c>0$ such that for every $n$

$$\Pr[A \text{ is BP-exact for } r]\ \ge\ 1-e^{-cm}.$$

The book states this without proof. It is included as a separate theorem, not a milestone of the goal.

Significance

Lemma 8.5.4 converts an algorithmic property, that an $\ell_1$ linear program returns a prescribed sparse vector for every right-hand side, into a purely geometric property of the kernel of $A$ relative to the low-dimensional faces of the crosspolytope. With milestone 5 it becomes the statement that $L$ avoids a finite family of cones, which is where union bounds over faces and estimates for random subspaces enter. Observation 8.5.1 separates what is information-theoretically possible (uniqueness of sparse solutions) from what is computationally achievable by linear programming; finding a sparse solution directly is NP-hard in general. Theorem 8.5.2 is the quantitative payoff: a fixed fraction of arbitrary gross errors can be corrected by solving one linear program.

All of these results are proved in the literature; Lemma 8.5.4, Observation 8.5.1 and the milestones are elementary, and Theorem 8.5.2 rests on Donoho's polytope-neighborliness analysis. The platform has a related formalization of Wainwright's restricted nullspace property (Theorem 7.8 of High-Dimensional Statistics, namespace HighDimStat.SparseLinear), which fixes a support set $S$ rather than characterizing exactness for all $r$-sparse vectors through the crosspolytope. A machine-checked proof of Theorem 8.5.2 with the constants $0.75$ and $0.08$ is, to our knowledge, not available anywhere; it would require substantial Gaussian and high-dimensional geometry infrastructure.

Difficulty

For the goal and milestones the difficulty is bookkeeping, not ideas: the scaling between a sparse solution $\tilde x$ and the boundary point $\tilde x/\|\tilde x\|_1$, the case $\tilde x=0$, and the fact that BP-exactness quantifies over all right-hand sides $b$ while the geometric side quantifies over boundary points of the crosspolytope.

Theorem 8.5.2 is of a different order. A union bound over the $\binom{n}{r}2^r$ faces of dimension $r-1$ reduces it to bounding the probability that a random $(n-m)$-dimensional subspace meets one cone $C_F$ nontrivially, and getting that probability small enough to beat the combinatorial factor with the stated numerical constants is the hard part. Rough asymptotic estimates do not give $0.08$ at $\alpha=0.75$.

Formalization scope

Vectors are functions Fin n → ℝ (the book's indices $1,\dots,n$ become $0,\dots,n-1$) and matrices are Matrix (Fin m) (Fin n) ℝ. The $\ell_1$-norm is written out as $\sum_i|x_i|$, since Mathlib's norm on Fin n → ℝ is the sup norm. The support is a Finset of indices. Optimality in (BP) and (BP′) is stated against every feasible point; no infimum is taken, so an empty or unbounded feasible set cannot create a spurious optimum. "Every $2r$ or fewer columns" ranges over finsets of distinct column indices, column $j$ being Aᵀ j. The hypotheses $m<n$ and $r\le m$ of Lemma 8.5.4 are kept as on the page, although the equivalence does not use them; $m<n$ is also the standing assumption of §8.5 needed for $m\ge 2r$.

In Theorem 8.5.2 the random matrix has the product law of independent gaussianReal 0 1 entries, the constant $c>0$ is quantified before $n$, and measurability of the BP-exact event is part of the conclusion, so the bound concerns a genuine probability rather than an outer measure.

A trivializing formalization is ruled out: BP-exactness requires uniqueness among all minimizers for every right-hand side, not just optimality of $\tilde x$, and the crosspolytope condition is an equality of sets, not an inclusion that $z$ alone would satisfy.

All definitions live in one module (MatousekLP.SparseRecovery.BasisPursuit); the $\ell_1$ and support vocabulary is reusable for later sparse-recovery missions. Contributions are welcome on every milestone, on the goal, and on the infrastructure towards Theorem 8.5.2 (Gaussian measures on matrix spaces, measurability of the BP-exact event, the face structure of the crosspolytope).

Selected references

• J. Matoušek and B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.5. https://doi.org/10.1007/978-3-540-30717-4
• S. S. Chen, D. L. Donoho and M. A. Saunders, Atomic decomposition by basis pursuit, SIAM J. Sci. Comput. 20(1), 1999, 33–61. https://doi.org/10.1137/S1064827596304010
• E. J. Candès, M. Rudelson, T. Tao and R. Vershynin, Error correction via linear programming, Proc. 46th IEEE FOCS, 2005, 295–308. https://doi.org/10.1109/SFCS.2005.5464411
• D. L. Donoho, High-dimensional centrally symmetric polytopes with neighborliness proportional to dimension, Discrete Comput. Geom. 35, 2006, 617–652. https://doi.org/10.1007/s00454-005-1220-0
• N. Linial and I. Novik, How neighborly can a centrally symmetric polytope be?, Discrete Comput. Geom. 36, 2006, 273–281. https://doi.org/10.1007/s00454-006-1235-1

Motivation

A binary error-correcting code is a set of $n$-bit words chosen so that the words stay distinguishable after a few bits have been corrupted in transmission. A code can correct any $r$ errors exactly when every two of its words differ in at least $2r+1$ positions. The more words the code has, the more information each transmitted block carries. So the central quantitative question of coding theory is how large a code of given length and minimum distance can be. Codes are used in every technology that transmits or stores data, from disks and phones to deep-space probes.

In 1973 Philippe Delsarte showed that an upper bound on this maximum size is the optimum value of an explicit linear program (Delsarte, An algebraic approach to the association schemes of coding theory, Philips Res. Repts. Suppl. 10, 1973). The bound was far stronger than the classical volume argument and remains a standard tool. This mission formalizes the self-contained proof of the bound in §8.4 of Matoušek and Gärtner's textbook (Springer 2007). That proof follows Best, Brouwer, MacWilliams, Odlyzko and Sloane (IEEE Trans. Inform. Theory 24, 1978). The mission also covers the step of Delsarte's original argument that the book isolates as a lemma.

Timeline.

• 1950: Hamming introduces single-error-correcting codes and the sphere-packing bound.
• 1973: Delsarte proves the linear programming bound using association schemes.
• 1978: Best et al. give the elementary parity proof and small improvements, among them $A(17,3) \le 6552$.
• 2005: Schrijver replaces the linear program by a semidefinite program and improves many entries of the code tables (IEEE Trans. Inform. Theory 51).

Setting

A word is $\mathbf w = (w_1,\dots,w_n) \in \{0,1\}^n$, and a code is any set $C \subseteq \{0,1\}^n$. The Hamming distance $d_H(\mathbf w,\mathbf w')$ is the number of positions $j$ with $w_j \ne w'_j$. The weight $|\mathbf w|$ is the number of ones in $\mathbf w$. The word $\mathbf w \oplus \mathbf w'$ is the entrywise sum modulo 2. For $I \subseteq \{1,\dots,n\}$, the restricted distance $d^I_H(\mathbf w,\mathbf w')$ counts only the differing positions that lie in $I$.

A code has distance $d$ if $d_H(\mathbf w,\mathbf w') \ge d$ for all distinct $\mathbf w,\mathbf w' \in C$ (Definition 8.4.1). The quantity $A(n,d)$ is the maximum of $|C|$ over all codes $C \subseteq \{0,1\}^n$ with distance $d$.

For $0 \le i,t \le n$ the Krawtchouk numbers are

$$K_t(n,i) = \sum_{j=0}^{\min(i,t)} (-1)^j \binom ij \binom{n-i}{t-j}.$$

The distance distribution of a code $C$ is

$$\tilde x_i(C) = \frac{1}{|C|}\,\bigl|\{(\mathbf w,\mathbf w')\in C^2 : d_H(\mathbf w,\mathbf w') = i\}\bigr|, \qquad i=0,\dots,n.$$

The Delsarte linear program has variables $x_0,\dots,x_n$. It maximizes $x_0+\dots+x_n$ subject to:

• $x_0 = 1$;
• $x_i = 0$ for $1 \le i \le d-1$;
• $\sum_{i=0}^n K_t(n,i)\,x_i \ge 0$ for $1 \le t \le n$;
• $x \ge 0$.

For Delsarte's original argument, $M_i$ is the $2^n\times 2^n$ matrix whose $(\mathbf v,\mathbf w)$ entry is $1$ when $d_H(\mathbf v,\mathbf w) = i$ and $0$ otherwise. The weights are $\tilde y_i = |\{(\mathbf w,\mathbf w')\in C^2 : d_H = i\}| / (2^n\binom ni)$.

Formalization targets

Goal: Theorem 8.4.3 (the Delsarte bound)

$$A(n,d) \;\le\; \max\Bigl\{\textstyle\sum_{i=0}^n x_i \;:\; x \text{ feasible for the Delsarte program}\Bigr\}\quad\text{for all } n, d.$$

The goal is stated against every upper bound $v$ of the objective on the feasible set. No particular optimum value is fixed, so the statement covers every $n$ and $d$ at once.

Milestones, in attack order

1. Lemma 8.4.5. For every $I$ and $C$, the pairs in $C^2$ with even $d^I_H$ are at least as many as the pairs with odd $d^I_H$.
2. Corollary 8.4.6. $\sum_{(\mathbf w,\mathbf w')\in C^2}(-1)^{(\mathbf w\oplus\mathbf w')^T\mathbf v}\ge 0$ for every $\mathbf v$.
3. Proposition 8.4.4. $\sum_{i=0}^n K_t(n,i)\,\tilde x_i(C) \ge 0$ for every $C$ and every $t = 1,\dots,n$.
4. §8.4, p. 160. The values $\tilde x_i(C)$ sum to $|C|$. For a nonempty code with distance $d$, the vector $\tilde x(C)$ is feasible for the program.
5. Lemma 8.4.2 (sphere-packing bound). $A(n,2r+1) \le \lfloor 2^n / \sum_{i=0}^r\binom ni\rfloor$.
6. Lemma 8.4.7. $\tilde M = \sum_{i=0}^n \tilde y_i M_i$ is positive semidefinite.

Significance

The Delsarte bound turns an extremal problem over the $2^{2^n}$ subsets of the cube into a linear program with $n+1$ variables. For $A(17,3)$ it gives $6553$, while the sphere-packing bound gives $7281$. Many entries of the standard code tables rest on this bound or its refinements. The positive semidefiniteness in Lemma 8.4.7 is the starting point of the semidefinite programming bounds of Schrijver and of later work. The same framework also underlies the linear programming bounds for spherical codes and sphere packings.

The theorem is classical and fully proved in the literature. Neither Mathlib nor this platform has a formal statement or proof of it. Mathlib has Hamming distance and binomial coefficients, but it has no $A(n,d)$, no Krawtchouk numbers and no LP bound for codes. This mission would produce the first formal statement and proof. It would also produce reusable identities on Krawtchouk sums and character sums over $\{0,1\}^n$.

Difficulty

Two of the program's constraints are immediate once $\tilde x_i$ is defined: $\tilde x_0 = 1$, and $\tilde x_i = 0$ for $i < d$. The difficulty lies in the Krawtchouk constraints. They do not follow from counting pairs at a single distance. They require a sign-weighted count over all words of weight $t$, and the sum must then be regrouped by the distance of each pair. That regrouping identifies a count of words, split by how many ones they share with a fixed word, with the Krawtchouk number. Formally this is an exchange of finite sums together with a binomial counting identity, and the index bookkeeping, including the range $j \le \min(i,t)$, has to be exact.

The obvious attempt proves the inequality one distance class at a time. It fails because the individual terms $K_t(n,i)\,\tilde x_i$ have no sign. Only the whole sum is nonnegative.

Formalization scope

• Words and codes. Words are Fin n → Bool, with bit $1$ as true. The book's positions $1,\dots,n$ become 0, …, n-1. Codes are Finsets of words, and $d_H$ is Mathlib's hammingDist.
• The maximum $A(n,d)$. $A(n,d)$ is a Finset.sup over the finite family of codes with distance $d$. This family contains the empty code, so the maximum is attained.
• Krawtchouk numbers. $K_t(n,i)$ is an integer, and its natural-number subtractions are honest for $i \le n$ and $j \le t$.
• LP variables and the $x_i = 0$ constraints. The LP variables are indexed by Fin (n+1) with no index shift. The constraints $x_i = 0$ are imposed for $1 \le i < d$, so they are vacuous for $d \le 1$.
• The empty code. Lean's convention $1/0 = 0$ gives $\tilde x(\emptyset) = 0$. Proposition 8.4.4 then holds trivially, and the feasibility milestone carries the hypothesis $C \ne \emptyset$ that the book's division presupposes.
• The sphere-packing floor. The floor in the sphere-packing bound is natural-number division by a denominator that is at least $1$.
• Positive semidefiniteness. This is Mathlib's Matrix.PosSemidef over $\mathbb R$.

No trivialization. The goal is not stated as "$A(n,d) \le \sup$" with a real supremum, which Lean would evaluate to $0$ on an empty or unbounded set. Its hypothesis ranges over upper bounds of a feasible program: $(1,0,\dots,0)$ is always feasible, so the hypothesis is never vacuous.

Contributions welcome. Useful lemmas include:

• Krawtchouk identities, for example $\sum_{t}K_t(n,i) = 2^n[i=0]$ and $K_i(n,t)\binom ni = K_t(n,i)\binom nt$;
• counting words of weight $t$ that meet a fixed support in exactly $j$ positions;
• general facts on character sums $\sum_{\mathbf w\in C}(-1)^{\mathbf w^T\mathbf v}$.

These are reusable for other LP and SDP bounds in coding theory.

Selected references

• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer Universitext, 2007, §8.4. https://doi.org/10.1007/978-3-540-30717-4
• P. Delsarte, An algebraic approach to the association schemes of coding theory, Philips Research Reports Supplements 10, 1973.
• M. R. Best, A. E. Brouwer, F. J. MacWilliams, A. M. Odlyzko, N. J. A. Sloane, Bounds for binary codes of length less than 25, IEEE Trans. Inform. Theory 24 (1978), 81–93. https://doi.org/10.1109/TIT.1978.1055827
• A. Schrijver, New code upper bounds from the Terwilliger algebra and semidefinite programming, IEEE Trans. Inform. Theory 51 (2005), 2859–2866. https://doi.org/10.1109/TIT.2005.851748