All missions

Recognizing a convex set from its projections

A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.

The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.

Sets, convex hulls, and affine projections

Fix an integer $d\geq3$. Real coordinate space $\mathbb R^d$ consists of vectors with $d$ real coordinates. A set $K\subseteq\mathbb R^d$ is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires $K$ to fill the ambient space.

The convex hull of a set $V$, written $\operatorname{conv}(V)$, is the smallest convex set containing $V$. A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map $f:\mathbb R^d\to\mathbb R^j$ has a $j$-dimensional target and reaches every point of that target. When $j<d$, such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.

The recognition target

For every bounded convex set $K\subseteq\mathbb R^d$, the goal is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\quad 2\leq j<d,\quad \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\quad f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.

This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.

What the criterion establishes

The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.

The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.

Why the converse requires more than one image

Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.

Mathematical conventions

Real $d$-space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on $K$.

The hypothesis $d\geq3$ makes explicit the admissible ambient dimension needed for $2\leq j<d$. In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.

Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.

Selected references

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.

Motivation

A fusion reactor only makes sense if the plasma gives back more energy than it loses. In 1955 J. D. Lawson turned that sentence into an inequality: for a hot, thermalized fuel, the product of the particle density $n$ and the energy confinement time $\tau_E$ must exceed a temperature-dependent threshold before the fusion products alone can keep the plasma hot. The criterion was published in 1957 (Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proc. Phys. Soc. B 70 (1957) 6–10) and has been the standard figure of merit for magnetic and inertial confinement ever since: machines are compared by their $n\tau_E$ and by the triple product $nT\tau_E$.

Timeline, as far as this mission's material traces it:

• 1955 — Lawson derives the criterion in a classified AERE report, balancing the volumetric fusion rate against bremsstrahlung radiation losses and ignoring conduction losses.
• 1957 — the report is declassified and published.
• 2004 — the textbook derivation in the form used here, together with the reactivity fit $\langle\sigma v\rangle \approx 1.1\cdot 10^{-24}\,T^2\ \mathrm{m^3/s}$ valid near $T = 14$ keV (J. Wesson, Tokamaks, 3rd ed., Oxford, 2004).
• 2022 — an inertial-confinement experiment at the National Ignition Facility is reported to exceed the Lawson criterion for ignition (Abu-Shawareb et al., Phys. Rev. Lett. 129, 075001).

Setting

Consider a steady-state, fully ionized plasma of deuterium and tritium. All quantities are real numbers and strictly positive, and the temperature $T$ is measured in energy units (electronvolts), so Boltzmann's constant does not appear: the article's $k_\mathrm{B}T$ is our $T$.

• $n$ — the particle (electron) density. Under the standing assumptions of the derivation — all species at the same temperature, no ions other than fuel ions (no impurities, no helium ash), and deuterium and tritium in the optimal 50-50 mixture — the ion density equals the electron density and $n_\mathrm{d} = n_\mathrm{t} = n/2$.
• $W = 3nT$ — the energy density of electrons and ions together, by the ideal gas law.
• $\langle\sigma v\rangle$ — the fusion cross section times relative velocity, averaged over the Maxwellian velocity distribution at temperature $T$.
• $f = n_\mathrm{d} n_\mathrm{t}\langle\sigma v\rangle$ — the volume rate of fusion reactions (reactions per volume per time), which for the 50-50 mixture equals $\tfrac14 n^2\langle\sigma v\rangle$.
• $E_\mathrm{ch}$ — the energy carried by the charged fusion products, the only part that can heat the plasma; $E_\mathrm{ch} = 3.5$ MeV for D-T, the neutron's 14.1 MeV being lost.
• $P_\mathrm{loss}$ — the power loss density, and $\tau_E = W/P_\mathrm{loss}$ — the energy confinement time.

The plasma is self-heating when fusion heating exceeds the losses:

$$f\,E_\mathrm{ch} \;\ge\; P_\mathrm{loss}.$$

Target

The goal theorem is the Lawson criterion itself — equation (1) of the source — obtained by substituting the model quantities into the self-heating condition:

$$n\,\tau_E \;\ge\; L \;\equiv\; \frac{12\,T}{E_\mathrm{ch}\,\langle\sigma v\rangle}.$$

The milestones are the surrounding statements of the same derivation, in the order a reader meets them:

$$f = \tfrac14 n^2\langle\sigma v\rangle,\qquad P_\mathrm{loss} = \frac{3nT}{\tau_E},\qquad \tfrac14 n^2\langle\sigma v\rangle E_\mathrm{ch} \ge \frac{3nT}{\tau_E},$$

the triple-product form and its numerical D-T value,

$$nT\tau_E \;\ge\; \frac{12}{E_\mathrm{ch}}\frac{T^2}{\langle\sigma v\rangle},\qquad nT\tau_E \;\ge\; 3\cdot 10^{21}\ \mathrm{keV\,s\,m^{-3}}\quad (E_\mathrm{ch} = 3500\ \mathrm{keV},\ \langle\sigma v\rangle = 1.1\cdot10^{-24}T^2),$$

the inertial-confinement form obtained from $\tau_E \approx R\sqrt{m_i/T}$,

$$n R \;\ge\; \frac{12\,T^{3/2}}{E_\mathrm{ch}\langle\sigma v\rangle\sqrt{m_i}},$$

and the empirical tokamak scaling: if $\tau_E = c\,n^{1/3}/P^{2/3}$ and $P = a\,n^2T^2$, then $nT\tau_E = c\,a^{-2/3}T^{-1/3}$, independent of the density.

Significance

The result itself. The criterion is what makes different confinement concepts comparable at all: it converts "does this machine work?" into a single number that can be measured and plotted, and its triple-product form is the quantity reported by tokamaks and by inertial-confinement shots alike. The last milestone explains why the triple product, rather than $n\tau_E$, is the quantity of record for tokamaks: under the empirical energy-confinement scaling it does not depend on the density and depends on temperature only as $T^{-1/3}$.

Formalizing it. Nothing here is an open problem: every statement is a known consequence of the stated model, and the mathematical content is algebra and monotonicity over the positive reals. What the mission produces is a machine-checked, reusable encoding of the energy-balance model of a D-T plasma, with every degenerate case (zero density, zero confinement time, vanishing reactivity) explicitly excluded, and with the chain from the model assumptions to each published form of the criterion verified end to end. The value is in the faithfulness of the model layer, not in the difficulty of the deductions.

Difficulty

The deductive content is elementary; the difficulty is representational. Three places where a careless encoding silently changes the theorem:

• Division. $\tau_E = W/P_\mathrm{loss}$ and $12T/(E_\mathrm{ch}\langle\sigma v\rangle)$ are total functions in Lean and return $0$ on zero denominators. Without strict positivity of $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$ and $P_\mathrm{loss}$, several of these statements become false or empty rather than merely degenerate.
• Direction of the inequality. The self-heating hypothesis and the conclusion point the same way only because one multiplies by the positive quantity $\tau_E/(n\,E_\mathrm{ch}\langle\sigma v\rangle)$; the factor $12 = 4\cdot 3$ comes from the $\tfrac14$ of the 50-50 mixture and the $3$ of $W = 3nT$, and either one dropped leaves a statement that still compiles.
• Fractional powers. The inertial-confinement and tokamak milestones involve $T^{3/2}$, $n^{1/3}$, $P^{2/3}$; these are Real.rpow, whose rules require positive bases, which is why the positivity hypotheses appear again there.

Formalization scope

The model is a Lean structure LawsonCriterion.DTPlasma bundling $n$, $T$, $\langle\sigma v\rangle$, $E_\mathrm{ch}$, $\tau_E$, $P_\mathrm{loss}$, all of type ℝ, with a strict-positivity field for each and one defining equation, tauE = energyDensity n T / Ploss where energyDensity n T = 3 * n * T. The 50-50 reaction rate is DTPlasma.rate, the heating rate is DTPlasma.fusionHeating = rate * Ech, and DTPlasma.SelfHeating is the proposition fusionHeating ≥ Ploss. Conventions this commits to:

• temperature in energy units, so T is $k_\mathrm{B}T$; the numerical milestone additionally fixes keV for T and Ech, m³/s for sigmav, and so keV·s·m⁻³ for the triple product;
• only the 50-50 D-T mixture and the charged-product energy enter; bremsstrahlung, conduction and impurities are not modelled separately — they are whatever Ploss is;
• Real.rpow for the fractional exponents, Real.sqrt for the thermal speed.

The statements are not vacuous: the definition file also publishes a witness, LawsonCriterion.unitDTPlasma, so the structure is inhabited and every hypothesis set here is satisfiable. Conversely, no statement is trivially true — each is an inequality between quantities that genuinely vary with the plasma parameters.

Contributions welcome beyond the listed milestones: a version that separates radiation from conduction losses, the D-D and D-³He variants, and the statement that $T \mapsto T/\langle\sigma v\rangle$ attains a minimum for a realistic reactivity model — the step where the source passes from the inequality to its "absolute lower limit", which this mission does not formalize.

Selected references

• J. D. Lawson, Some Criteria for a Power Producing Thermonuclear Reactor, Proceedings of the Physical Society, Section B 70 (1957) 6–10. doi:10.1088/0370-1301/70/1/303
• J. Wesson, Tokamaks, Oxford Engineering Science Series 48, 3rd ed., Clarendon Press, 2004.
• H. Abu-Shawareb et al., Lawson Criterion for Ignition Exceeded in an Inertial Fusion Experiment, Physical Review Letters 129, 075001 (2022). doi:10.1103/PhysRevLett.129.075001
• Lawson criterion, Wikipedia, revision 1367242125 — the source text this mission formalizes. link

Motivation

Hubble's law — officially the Hubble–Lemaître law — is the observation that galaxies recede from us at a speed proportional to their distance, $v = H_0 D$. It is the first observational basis for the expansion of the universe and one of the standard pieces of evidence cited for the Big Bang model. Georges Lemaître derived the proportionality from relativistic cosmology in 1927; Edwin Hubble published the observational relation in 1929, building on Vesto Slipher's redshifts and Henrietta Swan Leavitt's Cepheid distance scale. Alexander Friedmann had already shown in 1922 that the Einstein field equations admit expanding solutions, with an expansion rate governed by what is now called the scale factor.

Behind the astronomy sits a piece of elementary mathematics that is rarely written out in full: in a spatially homogeneous expansion, the linear velocity–distance relation is forced, it holds with the same constant for every observer, and the Hubble "constant" is in fact a function of time whose evolution is fixed by a single dimensionless parameter. This mission formalizes that kinematic core: the statements are about the scale factor and its derivatives, and involve no Einstein equations.

Setting

A scale factor is a function $a : \mathbb{R} \to \mathbb{R}$ of cosmic time $t$. A comoving point is labelled by a fixed coordinate $\mathbf{x} \in \mathbb{R}^3$ (with the Euclidean norm), and its proper position at time $t$ is

$$\mathbf{X}_{\mathbf{x}}(t) \;=\; a(t)\,\mathbf{x}.$$

The proper distance between the comoving points $\mathbf{x}$ and $\mathbf{y}$ is

$$D_{\mathbf{x},\mathbf{y}}(t) \;=\; \lVert a(t)\mathbf{x} - a(t)\mathbf{y}\rVert .$$

The Hubble parameter and the dimensionless deceleration parameter are

$$H(t) \;=\; \frac{\dot a(t)}{a(t)},\qquad q(t) \;=\; -\,\frac{\ddot a(t)\,a(t)}{\dot a(t)^{2}} .$$

$H_0$ denotes the present-day value of $H$; the name "Hubble constant" refers to the fact that $H$ is constant in space at a fixed time, not in time.

Target

The goal theorem is the idealized Hubble law, stated in the source as a theorem of Euclidean geometry: any two points moving away from the origin, each along a straight line and with speed proportional to its distance from the origin, move away from each other with a speed proportional to their distance apart. Formally, for $H \ge 0$, a time $t$ and curves $p, q : \mathbb{R} \to \mathbb{R}^3$ with

$$p'(t) = H\,p(t), \qquad q'(t) = H\,q(t),$$

the separation satisfies

$$\frac{d}{ds}\Big|_{s=t}\big(p(s) - q(s)\big) \;=\; H\,\big(p(t) - q(t)\big), \qquad \big\lVert H\,(p(t)-q(t))\big\rVert \;=\; H\,\lVert p(t)-q(t)\rVert .$$

The relative velocity is parallel to the separation vector and its magnitude is $H$ times the separation, with the same $H$ for every pair — so no comoving observer occupies a distinguished centre of the expansion.

The milestones supply the cosmological content that surrounds this geometric fact:

1. proper distances scale as $D(t) = \big(a(t)/a(t_0)\big) D(t_0)$;
2. a comoving point has velocity $H(t)$ times its proper position vector;
3. Hubble's law itself, $\dot D(t) = H(t)\,D(t)$;
4. the evolution law $\dot H = -(1+q)H^{2}$;
5. the zero-deceleration case: if $q \equiv 0$ then $H(t) = 1/t$, with $t$ the time since the Big Bang, so the Hubble time $1/H$ is exactly the age;
6. a constant Hubble parameter forces exponential growth $a(t) = a(t_0)e^{H_0(t-t_0)}$;
7. the small-redshift limit: with $1 + z = a(t_0)/a(t_\mathrm{e})$, the ratio $z/(t_0 - t_\mathrm{e})$ tends to $H(t_0)$ as $t_\mathrm{e} \to t_0$, which is the $z \approx H_0 D/c$ form of the law used observationally.

Significance

The result itself is elementary but load-bearing: it is what licenses reading a linear redshift–distance diagram as evidence for uniform expansion rather than for a privileged position in space, and items 4–6 are the statements through which cosmological observations (the sign of $q$, the approach of $q$ to $-1$ in $\Lambda$CDM) are turned into claims about the past and future behaviour of $H$ and $a$.

Formalizing it produces a small, reusable Lean layer for expansion kinematics: the scale factor, the Hubble and deceleration parameters, proper position and proper distance, with the differentiation lemmas that connect them. The platform already carries Friedmann-equation missions that fix the dynamics of $a$; this mission is the kinematic complement, and its Hubble parameter is the same function $\dot a/a$ that those developments use. Nothing here is an open research problem: every statement is a known textbook fact, and the work is the formalization.

Difficulty

The mathematical content is a few lines of calculus, so the difficulty is entirely in the encoding. Three places are easy to get wrong. First, proper distance is defined through a norm, so the identity $\lVert a(t)v\rVert = a(t)\lVert v\rVert$ needs positivity of $a$, and differentiating it needs positivity on a neighbourhood, not just at the point. Second, $q$ is defined by a quotient with $\dot a^{2}$ in the denominator: in Lean division by zero returns zero, so a statement about $q$ that forgets $\dot a(t) \ne 0$ silently changes meaning. Third, milestone 5 propagates a hypothesis stated on $(0,\infty)$ down to the endpoint $t=0$, where the Big Bang condition $a(0)=0$ lives; the continuity argument at the endpoint is the only step with any technical content.

Formalization scope

Time is $\mathbb{R}$ and space is EuclideanSpace ℝ (Fin 3); derivatives are Mathlib's deriv / HasDerivAt, so "velocity" is always a derivative at a point rather than a difference quotient. Smoothness is assumed exactly where it is used: differentiability at a single time for the first-order statements, ContDiff ℝ 2 for the statements involving $\ddot a$. Positivity of the scale factor is stated explicitly wherever it is needed, as is $\dot a(t) \ne 0$ in the statements mentioning $q$.

Degenerate readings are excluded: the goal's hypotheses are satisfiable (any pair of comoving points in an expanding universe satisfies them, as milestone 2 shows), and the milestones are non-vacuous for concrete scale factors such as $a(t) = t$ and $a(t) = e^{H_0 t}$. The goal theorem's second clause is a norm identity that is true for every $H \ge 0$; it carries the "speed proportional to distance" half of the source's statement, while the first clause carries the "moving away from each other along the separation" half.

The definition layer is a single self-contained file (scale factor derived quantities, proper position, proper distance); it is reusable by any mission about expansion kinematics. Contributions of the milestone proofs, and of variants such as the redshift relation $1+z = a(t_0)/a(t_\mathrm{e})$ derived from null geodesics rather than assumed, are welcome.

Selected references

• Wikipedia, "Hubble's law" (Hubble–Lemaître law), https://en.wikipedia.org/wiki/Hubble%27s_law — the source text for this mission, in particular the sections "Recessional velocity", "Time-dependence of Hubble parameter", "Idealized Hubble's law" and "Ultimate fate and age of the universe".
• E. Hubble, "A relation between distance and radial velocity among extra-galactic nebulae", PNAS 15 (1929) 168–173, https://doi.org/10.1073/pnas.15.3.168.
• G. Lemaître, "Un univers homogène de masse constante et de rayon croissant rendant compte de la vitesse radiale des nébuleuses extra-galactiques", Annales de la Société Scientifique de Bruxelles A47 (1927) 49–59.
• A. Friedmann, "Über die Krümmung des Raumes", Zeitschrift für Physik 10 (1922) 377–386, https://doi.org/10.1007/BF01332580.

Motivation

Chapters 3-4 of Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) answer "can the network stay stable?" — the backpressure algorithm's throughput optimality (Theorem 4.5) says yes, for any arrival rate inside the capacity region. But networks are usually operated with plenty of unused capacity precisely so that they can also serve a second goal: maximizing some concave utility (throughput, fairness, revenue) of the rates actually delivered. Answering "how close to utility-optimal can a stable policy get, and at what congestion cost?" needs a single theorem that treats stability and utility optimization in one drift analysis. Theorem 5.4, adapted from Neely, Modiano & Li [108], Georgiadis, Neely & Tassiulas [115] and Neely [116], is that theorem, and it is the technique — "Lyapunov optimization" or "drift-plus-penalty" — behind a large fraction of the cross-layer control literature that followed this book.

Setting

A network of $N$ queues has backlog vector $U(t)=(U_1(t),\dots,U_N(t))$, and a $K$-dimensional control process $R(t)=(R_1(t),\dots,R_K(t))$ influencing the system's dynamics (e.g. admitted data rates). For any nonnegative function $L$ of the backlog vector, the one-step Lyapunov drift is $\Delta(U(t)):=\mathbb E\{L(U(t{+}1))-L(U(t))\mid U(t)\}$, the expected one-slot change in $L$ conditioned on the current backlog. Given any scalar-valued concave utility function $g$ of a $K$-dimensional rate vector and an arbitrary target value $g^*$, the goal is to stabilize $U(t)$ while making the time-average utility of $R(t)$ close to $g^*$. The time-average rate vector is $r(t):=\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{R(\tau)\}$ (5.18), and the achieved long-run utility is $\bar g:=\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{g(R(\tau))\}$.

Formalization targets

Milestone — Lemma 5.3 (Lyapunov Drift)

$$\Delta(U(t))\le\mathbb E\{y(t)\mid U(t)\}-\mathbb E\{x(t)\mid U(t)\}\ \forall t \ \Longrightarrow\ \limsup(\text{avg }x)\le\limsup(\text{avg }y),\ \liminf(\text{avg }x) \le\liminf(\text{avg }y).$$

The most abstract drift lemma in the whole book: $x(t),y(t)$ are arbitrary scalar processes, not necessarily linear or even a function of $U(t)$.

Goal — Theorem 5.4 (Lyapunov Optimization)

$$\Delta(U(t))-V\,\mathbb E\{g(R(t))\mid U(t)\}\le B-\varepsilon\sum_{i=1}^N U_i(t)-Vg^*\ \forall t$$ $$\Longrightarrow\quad \limsup_{t\to\infty}\tfrac1t\sum_\tau\sum_i\mathbb E\{U_i(\tau)\}\le\frac{B+V(\bar g-g^*)}\varepsilon, \qquad \liminf_{t\to\infty}g(r(t))\ge g^*-\frac BV.$$

This is the weakest, most general level — a drift-minus-utility condition, checked against an arbitrary target $g^*$, with no reference to any specific control policy.

Significance

Theorem 5.4 is the abstract engine that every concrete utility-maximizing algorithm in the rest of the chapter (the CLC1 joint flow-control/routing/scheduling algorithm of Theorem 5.1, and its robustness variant under approximate scheduling, Corollary 5.2) instantiates by exhibiting a control rule whose per-slot decision satisfies (5.19) for some $V,\varepsilon,B$ — the drift condition does the work of turning a per-slot optimization rule into a global performance guarantee. Its $[O(1/V),O(V)]$ tradeoff (utility gap shrinks like $1/V$, congestion grows like $V$) is the quantitative signature of every "Lyapunov optimization"/"drift-plus-penalty" algorithm in the cross-layer control literature that followed this book, making Theorem 5.4 the single result a reader needs to understand that entire family of algorithms at once, independent of which specific control problem it is applied to.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov optimization, drift-plus-penalty, utility fairness, concave utility — no hits at all, not even an adjacent object). This mission is the first formalization of the book's utility-optimization engine.

Difficulty

The central subtlety, flagged explicitly by the book's own notation, is that (5.20) and (5.21) compare two different kinds of quantity that are easy to conflate: $\bar g$ is a limsup of an expectation of utility, $\mathbb E\{g(R(\tau))\}$, while $g(r(t))$ in (5.21) is the utility evaluated at the time-averaged expected rate. Jensen's inequality (using $g$'s concavity) is exactly what would relate $g(\mathbb E\{R(t)\})$ to $\mathbb E\{g(R(t))\}$ — and it is not proved or needed by this theorem's own statement, only by later results that connect the two more tightly. A formalization that silently merges these into one "utility" quantity would be proving something the book does not claim. The second trap is the target $g^*$: it is a free parameter of the hypothesis, not the true optimal utility — the theorem's strength is exactly that it says nothing special about how $g^*$ was chosen, so a formalization must not add a hidden side condition forcing $g^*$ to equal a genuine optimum.

Formalization scope

∆(U(t)) is restated locally in this chunk's own sub-namespace (drafts cannot import chunk 04-backpressure's copy), via Mathlib's condExp on the σ-algebra generated by the current backlog vector, exactly as in Chapter 4. Explicit Measurable/Integrable guards on U, R, g∘R and every drift term prevent condExp/∫ from silently defaulting to 0 (a trivializing formalization this mission rules out: without these guards, a non-integrable process would satisfy the hypotheses vacuously and "prove" a stability/utility conclusion for a process that is not actually controlled). r(t) and \bar g are written inline as their defining Cesàro averages rather than as separate named definitions, since each is used exactly once. Out of scope for this mission: Theorem 5.1 (the CLC1 algorithm's concrete instantiation), Corollary 5.2 (the robustness-to-suboptimal-scheduling variant), and Lemma 5.5 (continuity of near-optimal solutions, which needs the capacity region Λ as a hypothesis object). All three need substantially more setup (a named algorithm, or the capacity-region machinery of Chapter 3) than this session's time budget allowed without approximating either — left for a future mission rather than approximated.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, Modiano & Li, "Fairness and optimal stochastic control for heterogeneous networks", IEEE/ACM Transactions on Networking, 16(2), 2008. https://doi.org/10.1109/TNET.2007.900405
• Neely, "Energy optimal control for time-varying wireless networks", IEEE Transactions on Information Theory, 52(7), 2006. https://doi.org/10.1109/TIT.2006.876219

Motivation

Every stability result in Georgiadis, Neely & Tassiulas's survey Resource Allocation and Cross-Layer Control in Wireless Networks (Foundations and Trends in Networking, 2006) — the throughput optimality of the dynamic backpressure algorithm (Theorem 4.5), the utility-optimal Lyapunov drift bound of Chapter 5, the energy-constrained control algorithm of Chapter 6 — is proved the same way: exhibit a drift condition on a quadratic Lyapunov function of the queue backlog vector, then invoke one fixed abstract lemma to conclude stability and an explicit congestion bound. That fixed lemma, Lyapunov drift stability (Lemma 4.1, adapted from Kingman [67], Loynes [87] and Neely, Modiano & Li [110]), is the engine this mission formalizes — the single result the rest of the book's algorithm-specific theorems are instances of.

Setting

A network of $L$ queues has backlog vector process $U(t)=(U_1(t),\dots,U_L(t))$ on slots $t=0,1,2,\dots$, on a common probability space $(\Omega,P)$. The quadratic Lyapunov function is $L(U(t)):=\sum_{i=1}^L U_i(t)^2$. A single queue's backlog sequence $U:\mathbb N\to\mathbb R$ (read as $\mathbb E\{U(t)\}$) is strongly stable if $\limsup_{t\to\infty}\frac1t\sum_{\tau=0}^{t-1}\mathbb E\{U(\tau)\}<\infty$; a network is strongly stable if every one of its $L$ queues is. The conditional drift of $L$ given the current backlog vector, $\mathbb E\{L(U(t+1))-L(U(t))\mid U(t)\}$, measures how the aggregate squared backlog is expected to change over one slot, conditioned on where the network currently is — formalized via Mathlib's conditional expectation on the $\sigma$-algebra generated by $U(t)$.

Formalization targets

Goal — Lemma 4.1 (Lyapunov Stability)

$$\text{if } \exists\, B>0,\varepsilon>0,\ \forall t,\ \mathbb E\{L(U(t{+}1))-L(U(t))\mid U(t)\} \le B-\varepsilon\sum_{i=1}^L U_i(t),$$ $$\text{then the network is strongly stable and } \limsup_{t\to\infty}\tfrac1t\sum_{\tau=0}^{t-1}\sum_{i=1}^L\mathbb E\{U_i(\tau)\}\le B/\varepsilon.$$

This is the weakest, most general level: a bounded-outside-a-compact-region drift condition implies both a qualitative stability conclusion and a quantitative congestion bound, with no mention of any particular algorithm, arrival distribution, or network topology.

Milestones

• Lemma 4.3 (elementary inequality): $V\le\max[U-\mu,0]+A \Rightarrow V^2\le U^2+\mu^2+A^2-2U(\mu-A)$ for nonnegative reals — the per-slot squared-backlog bound the standard proof of Lemma 4.1 instantiates on the queueing recursion.
• Lemma 4.2 (T-slot Lyapunov drift): the same conclusion as the goal, with the drift measured over a block of $T$ slots rather than one — needed whenever a single slot's expected drift can be positive, and the tool the book itself uses (§4.4.1) to re-derive Chapter 3's single-queue admissibility-based stability condition (Lemma 3.6) as a worked demonstration of the method.

Significance

Lyapunov drift stability is the one lemma every later result in this book's method reduces to: Chapter 4's own Theorem 4.5 (backpressure throughput optimality) applies it directly to the dynamic backpressure algorithm's per-slot optimality property; the book explicitly notes ("This drift inequality is in the exact form for application of the Lyapunov drift lemma... proving the result", p. 57) that once a drift bound of this shape is established, the stability conclusion is free. The T-slot version (Lemma 4.2) extends the reach of the method to settings — Markov-modulated channels, non-i.i.d. arrivals — where no single slot need have negative drift.

Formalizing it. No result in this mission has a machine-checked proof anywhere; nothing adjacent exists on the platform (searched for Lyapunov drift, max-weight, differential backlog, backpressure — the one Lyapunov-drift hit, a Foster-Lyapunov hitting-time bound for a finite-state MDP with an absorbing target state, is a different mathematical object from a vector queue backlog with no absorbing state, and is not reused). This mission is the first formalization of the book's stability engine.

Difficulty

The obvious first idea is to bound $\mathbb E\{U_i(t)\}$ directly via the one-step queueing recursion and telescope. This fails for the same reason it fails in Chapter 3: expectation does not commute with $\max(\cdot,0)$. Lemma 4.1's actual content is a genuine Foster–Lyapunov drift argument on the aggregate quadratic quantity $L(U(t))$, not a per-queue linear one — the quadratic form is what turns a one-sided drift condition into a bound on $\sum_i U_i(t)$ itself (via the elementary inequality of Lemma 4.3, which converts the linear queueing recursion into a quadratic one that the drift condition directly controls). A second trap is conditioning: the drift bound is conditioned on the current backlog vector $U(t)$, not on the full history — a weaker, memoryless form of conditioning that is exactly what makes the lemma apply uniformly to i.i.d., Markov-modulated, and adversarial channel processes alike, provided the algorithm itself is memoryless in the state.

Formalization scope

The Lyapunov-drift hypothesis conditions on the σ-algebra generated by the current backlog vector, MeasurableSpace.comap (U t) inferInstance, via Mathlib's condExp; explicit Measurable/ Integrable guards on U t and on the drift term prevent condExp/∫ from silently defaulting to 0 for a non-measurable or non-integrable process (a trivializing formalization this mission rules out: without those guards, an arbitrary non-integrable backlog process would satisfy the drift hypothesis vacuously and "prove" the theorem for a process that manifestly is not stable). The limsup ≤ B/ε conclusion is stated as ∀ t, (Cesàro average at t) ≤ B/ε rather than via Mathlib's Filter.limsup, matching the standard telescoping proof (which bounds the average for every t, not merely eventually) and avoiding Filter.limsup's junk value on an unbounded sequence in the non-complete lattice ℝ. Out of scope for this mission: the algorithm-specific Theorem 4.5 (dynamic backpressure throughput optimality) and Lemma 4.4 (the single-queue corollary via admissible processes) — the former needs the book's named algorithm plus Chapter 3's capacity region restated as a local hypothesis and the explicit constant B of Eq. (4.12); the latter needs this chunk's own restatement of Chapter 3's admissibility structures. Both are left for a future mission with a larger time budget rather than approximated.

Selected references

• Georgiadis, Neely & Tassiulas, Resource Allocation and Cross-Layer Control in Wireless Networks, Foundations and Trends in Networking, Vol. 1, No. 1 (2006), pp. 1-144. https://doi.org/10.1561/1300000001
• Neely, Modiano & Li, "Fairness and optimal stochastic control for heterogeneous networks", IEEE/ACM Transactions on Networking, 16(2), 2008. https://doi.org/10.1109/TNET.2007.900405
• Loynes, "The stability of a queue with non-independent inter-arrival and service times", Mathematical Proceedings of the Cambridge Philosophical Society, 58(3), 1962. https://doi.org/10.1017/S0305004100036781

Motivation

Search-engine ad-auctions sell items (ad slots) to buyers who arrive with per-item bids and a fixed daily budget, online: each item must be allocated the moment it appears, with no ability to revisit past allocations, and no buyer may ever be charged more than its budget. Buchbinder and Naor's survey [1] models this as a generalization of online bipartite matching and derives an allocation algorithm through the same online primal-dual recipe formalized elsewhere in this series (Chapter 4's framework), applied to a genuinely different LP shape — a maximization (revenue) problem whose "packing" role and "covering" role are the reverse of Chapters 4, 5 and 7 — and to a different constraint structure (budget caps on a per-buyer accumulated sum, not a per-constraint 0/1 covering requirement). This mission covers Section 10.1, "The Basic Algorithm": the single-slot allocation algorithm and its $(1-1/c)(1-R_{\max})$-competitive analysis (Theorem 10.1). Sections 10.2-10.3 (multiple ad-slots via strong duality; stochastic per-buyer spending guarantees) are out of scope — see Formalization scope.

Setting

Fix a finite set $I$ of buyers, each with budget $B_i > 0$, and a finite set $M$ of items; buyer $i$ bids $b_{ij} \ge 0$ for item $j$, revealed one item at a time in the order enumerated by $M$. Let $R_{\max} := \max_{i,j} b_{ij}/B_i$, carried as an explicit positive parameter. The Allocation algorithm (p. 212), upon each item $j$'s arrival, allocates it to the buyer $i$ maximizing $b_{ij}(1-x_i)$ (where $x_i \in [0,1]$ is buyer $i$'s current primal value); if $x_i \ge 1$ already, nothing happens (the buyer is "full"). Otherwise it charges buyer $i$ the minimum of $b_{ij}$ and its remaining budget, sets the dual allocation variable $y_{ij} \leftarrow 1$, sets $z_j \leftarrow b_{ij}(1-x_i)$, and updates $x_i \leftarrow x_i(1+b_{ij}/B_i) + b_{ij}/((c-1)B_i)$ for a constant $c$ fixed by the analysis. The revenue actually collected from buyer $i$ is $\min\!\big(\sum_j b_{ij}y_{ij},\,B_i\big)$ — the buyer is never charged more than its budget. Unlike Chapters 4/7, this LP's dual (the ad-auctions revenue objective, Fig. 10.1) is the maximization problem being solved online; the "primal" covering LP ($x_i$, $z_j$ variables) exists only as a duality certificate.

Formalization targets

Theorem 10.1 (the goal, p. 212), given the milestone's dual near-feasibility bound and the fact that each buyer's total accrued bids exceed its budget by at most a factor of $R_{\max}$ (Claim (3)'s consequence):

$$\forall\, (x'', z'')\text{ feasible for Fig. 10.1's covering LP},\ \ \textstyle\sum_i \mathrm{actualCharge}(i) \ \ge\ (1-\tfrac1c)(1-R_{\max}) \Big(\textstyle\sum_i B_i x''_i + \sum_j z''_j\Big),$$

with $c = (1+R_{\max})^{1/R_{\max}}$ taken verbatim from the theorem's own statement — the exact formula, not an $O(\cdot)$ instantiation. Inequality (10.1) (p. 213), the milestone, is the book's own induction-proved lower bound on a buyer's primal value in terms of its accrued bids: $x_i \ge \frac{1}{c-1}\big(c^{(\sum_j b_{ij}y_{ij})/B_i} - 1\big)$.

Significance

Theorem 10.1 is the entry point to a short but influential sub-line of the online primal-dual method — Section 10.2 extends it to multiple ad-slots via strong duality for maximum-weight matching (rather than the weak duality this framework otherwise relies on throughout), and Section 10.3 incorporates stochastic per-buyer spending guarantees, both reusing this section's constant $c=(1+R_{\max})^{1/R_{\max}}$ and its limit $c\to e$ as $R_{\max}\to0$ (recovering the classic $(1-1/e)$-competitive ratio for the unweighted, unbudgeted case). It is also the first mission in this series to apply the online primal-dual method to a genuine revenue-maximization problem rather than a covering/packing pair with matching roles. No formal development of ad-auctions, budgeted online matching, or this constant was found on the platform as of 2026-09-20 (searches below); this mission is the first.

Difficulty

As with 04-framework's Algorithm 3 and 07-generalized-caching's Fractional Caching algorithm, the central obstacle is characterizing an online process by its own final output. Unlike those two chapters, however, step (3)'s update increment varies per allocation (bd, the specific bid of the item just won), so no closed-form solution of the recurrence exists in general; buyerX is instead defined as an explicit List.foldl realizing the exact per-step update, over the (temporally ordered) list of bids a buyer actually won — a faithful, if less immediately readable, transcription of "the algorithm's output as a function of its own trajectory," in the same spirit as this series' other closed-form definitions. A second difficulty specific to this chapter: the book's derivation of inequality (10.1) is itself an induction on iterations (not a single algebraic step, unlike Eq. (7.2) in 07-generalized-caching), and the theorem's final bound further combines it with a separate "at most one undercharged iteration" argument (Claim (3)'s conclusion, p. 214-215) turning the raw accrued-bid bound into one about the actually collected (budget-capped) revenue — both are stated here as explicit hypotheses (the milestone, and h_at_most_one_undercharge) rather than derived, since the goal is a faithful statement, not a proof; both sorrys are documented, not silently discharged.

Formalization scope

AdAuctionsInstance I M bundles b : I → M → ℝ, B : I → ℝ (hB_pos), and Rmax : ℝ with hRmax_pos : 0 < Rmax and hRmax_bound : ∀ i j, b i j ≤ Rmax * B i — the last two as explicit hypotheses, never derived via Finset.sup, matching 04-framework's d and 07-generalized-caching's k. cParam inst := (1+Rmax)^(1/Rmax) uses Real.rpow (ℝ^ℝ). buyerX inst i bids folds step (3)'s update over a list of won bids; revenue/actualCharge realize $\sum_j b_{ij}y_{ij}$ and its budget-capped charge. Reals throughout. Explicitly out of scope: Section 10.2's multiple-slot generalization (Theorem 10.2), which requires strong duality for maximum-weight bipartite matching as an explicit premise (the book: "our analysis... crucially relies on strong duality") — a substantially different LP structure (an integral matching LP, not this section's per-buyer budget LP) that this mission's AdAuctionsInstance does not model, and whose applicability of PrimalDualOnline.LP.strong_duality_adapter (this book's own Theorem 2.2) was not verified in the time available. Section 10.3's stochastic guarantee (Theorem 10.3) is likewise out of scope, and its own BRIEF.md-flagged ambiguity (whether its scalar g is $\min_i g_i$ or another aggregate of the per-buyer vector $g_i$) was not resolved. Both are natural follow-on missions, not attempted here. Welcome contributions: completing the two sorrys, and the Section 10.2-10.3 follow-on mission(s).

Selected references

• N. Buchbinder, J. Naor. The Design of Competitive Online Algorithms via a Primal-Dual Approach. Foundations and Trends in Theoretical Computer Science, 3(2-3):93-263, 2009. https://doi.org/10.1561/0400000024

Motivation

A convex set can be studied through its images in lower-dimensional spaces. Each image retains part of the geometry while discarding information along the directions that are collapsed. Finite convex hulls behave well under affine maps: the image of a convex hull of finitely many points is again the convex hull of finitely many points. The converse is subtler. It asks whether sufficiently comprehensive lower-dimensional image data forces the original bounded convex set itself to have a finite description by points.

This mission formalizes the projection-recognition criterion attributed to Klee in Branko Grünbaum's Convex Polytopes, second edition, §5.1, Theorem 5.1.8, printed page 74 (PDF page 100 of the supplied source). The criterion concerns every projection into one suitable intermediate dimension, not a chosen coordinate view. It therefore characterizes a global property of the original set by an entire family of dimension-reducing images.

Setting

Fix a natural number $d\geq 3$. Real coordinate space $\mathbb R^d$ is represented in Lean by functions from Fin d to the real numbers. A subset $K\subseteq\mathbb R^d$ is convex when it contains every line segment joining two of its points, and it is bounded when all of its points lie within some finite metric ball. Neither condition requires $K$ to be nonempty, closed, or full-dimensional.

For a set $V$, its convex hull $\operatorname{conv}(V)$ is the smallest convex set containing $V$. In the convention used by Grünbaum in §3.1, printed page 31 (PDF page 51), a polytope is equivalently the convex hull of a finite set. The generating set need not be a minimal vertex set, and the formal statement permits the finite set to be empty or contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map

$$f:\mathbb R^d\longrightarrow\mathbb R^j$$

has image dimension exactly $j$. When $j<d$, it is singular. Grünbaum defines a projection at the opening of §5.1, printed page 71 (PDF page 97), as an image under a singular affine map. Using a surjective affine map to coordinate $j$-space represents a projection to a $j$-dimensional affine space followed by an affine choice of coordinates. Whether a set is a finite convex hull is unchanged by that coordinate identification.

Formalization target

For every bounded convex set $K\subseteq\mathbb R^d$, the target is the equivalence

$$K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\;2\leq j<d,\; \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\; f(K)\text{ is a polytope}.$$

The dimension $j$ may depend on $K$, but it is selected before the universal quantifier over affine maps. Every surjective affine map with that target dimension is tested. For each map, the finite set whose convex hull is $f(K)$ may be different; no common projected generator set and no uniform bound on its size is asserted. This is one theorem with both directions, so there are no separate milestone statements in the package.

Significance

The forward implication records the stability of finite convex hulls under affine images. The recognition implication is the substantive part: under boundedness and convexity, polytopality of every projection in one eligible intermediate dimension forces $K$ itself to be a polytope. The conclusion concerns $K$ rather than merely its closure and does not add a hidden closedness assumption.

The theorem is established mathematics in the cited textbook. The present artifact is a compiled formal statement, not a completed machine-checked proof: its theorem body is by sorry. Completing it would connect Mathlib's finite convex-hull and affine-map infrastructure to the classical projection-recognition argument while preserving the source's quantifier order and lower-dimensional boundary cases.

Difficulty

Each projected set may have its own unrelated finite generating set. Those separate witnesses do not directly assemble into a finite generating set in the original ambient space, because every projection has discarded a kernel direction. Checking one convenient projection is inadequate: that image can conceal structure occurring precisely in the collapsed directions. The challenge is therefore to use the universal family of projections at the selected dimension without replacing it by a fixed axis projection or adding compactness, full dimensionality, or nonempty interior.

Formalization scope

The Lean declaration is Grunbaum2003.polytope_iff_polytope_projections, in the book-wide namespace Grunbaum2003. It takes Bornology.IsBounded K and Convex ℝ K as the exact domain hypotheses. Polytopality is written directly as existence of a finite set with convex hull equal to the set; no stronger book-local full-dimensional polytope predicate is used. Projections are all surjective real affine maps from Fin d → ℝ to Fin j → ℝ.

The explicit premise $3\leq d$ records the admissible ambient range required by $2\leq j<d$. In dimension three, the only possible target dimension is two. No displayed existential claim is made for dimensions zero, one, or two, where no such $j$ exists. Within every admissible dimension, empty sets, singletons, and other lower-dimensional bounded convex sets remain in scope. Surjectivity prevents a map from having rank below $j$, and the strict inequality $j<d$ ensures dimension loss. There are no expression-essential book-local definitions or supporting theorems; the only dependencies are Mathlib modules for convex hulls, boundedness, finite-dimensional coordinate spaces, and affine maps.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, §3.1 and §5.1, especially Theorem 5.1.8 on printed page 74. Springer book record and DOI.

Motivation

Perturbative quantum field theory computes correlation functions of a field by expanding around a Gaussian (free) theory. Every term of that expansion is a Feynman diagram, and the rule that turns a diagram into a number is Wick's theorem: the expectation of a product of Gaussian field modes is the sum, over all ways of pairing the modes up, of the product of the two-point functions of the pairs. The same identity is known in probability and statistics as the Isserlis theorem (L. Isserlis, 1918) and is the standard tool for computing moments of Gaussian vectors; in random-matrix theory the counting of pairings it produces is the origin of the Catalan-number asymptotics of Wigner's semicircle law.

The uploaded source is the Wikipedia article Feynman diagram, which states Wick's theorem for the free scalar field and then, in the section Higher Gaussian moments — completing Wick's theorem, verifies the one-variable case by direct Gaussian integration. This mission formalizes that content: the combinatorics of pairings, the one-dimensional Gaussian moment formulas, and the multivariate identity itself.

Setting

Fix $d, n \in \mathbb{N}$ and work on $\mathbb{R}^d$ with coordinates $x_1,\dots,x_d$. Let $\mu$ be a centered Gaussian measure on $\mathbb{R}^d$: a Gaussian probability measure all of whose coordinate means vanish, $\int x_i \, d\mu(x) = 0$ for every $i$. Its covariance (in the physics reading, the propagator) is

$$G_{ij} \;=\; \int x_i x_j \, d\mu(x).$$

A pairing of the labels $\{0,1,\dots,2n-1\}$ is a partition of these $2n$ labels into $n$ unordered pairs; equivalently, a permutation $\sigma$ of the labels with $\sigma\circ\sigma = \mathrm{id}$ and $\sigma(i)\neq i$ for all $i$ (a fixed-point-free involution). The set of pairings is written $P_n$. For a weight $W_{ab}$ indexed by labels, the Wick sum is

$$\mathrm{Wick}(W) \;=\; \sum_{\sigma \in P_n} \ \prod_{\substack{i \,:\, i < \sigma(i)}} W_{i\,\sigma(i)},$$

the inner product ranging over the $n$ pairs of $\sigma$, each counted once through its smaller element.

In the article's field-theory notation the labels are momenta $k_1,\dots,k_{2n}$, the coordinates are the field modes $\phi(k_j)$, and the two-point function carries the momentum-conserving delta function, $\langle \phi(k)\phi(k')\rangle = \delta(k-k')/k^2$. This mission works with the finite-dimensional Gaussian vector rather than the field, so the delta functions are absorbed into the covariance matrix $G$.

Formalization targets

Goal — Wick's theorem (Isserlis' theorem)

For a centered Gaussian measure $\mu$ on $\mathbb{R}^d$ and any labels $k_1,\dots,k_{2n} \in \{1,\dots,d\}$,

$$\int \prod_{j=1}^{2n} x_{k_j} \, d\mu(x) \;=\; \sum_{\sigma\in P_n} \ \prod_{i < \sigma(i)} \left( \int x_{k_i} x_{k_{\sigma(i)}} \, d\mu(x) \right).$$

No hypothesis is imposed on the covariance: it may be singular and the labels $k_j$ may repeat, which is exactly the situation the article's "completing Wick's theorem" section addresses.

Supporting targets (milestones)

1. $\int_{\mathbb{R}} e^{-a x^{2}/2}\,dx = \sqrt{2\pi/a}$ for $a>0$.
2. $\int_{\mathbb{R}} x^{2n} e^{-a x^{2}/2}\,dx = \dfrac{(2n-1)!!}{a^{n}}\sqrt{2\pi/a}$ for $a>0$.
3. $\int x^{2n}\,d\mathcal{N}(0,v) = (2n-1)!!\, v^{n}$ for a real Gaussian law of variance $v \ge 0$.
4. $\#P_n = (2n-1)!!$.
5. Correlation functions of odd order vanish: $\int \prod_{j=1}^{2n+1} x_{k_j}\,d\mu = 0$.
6. The four-point function: $\langle x_{k_1}x_{k_2}x_{k_3}x_{k_4}\rangle$ equals the sum of the three products $G_{k_1k_2}G_{k_3k_4} + G_{k_1k_3}G_{k_2k_4} + G_{k_1k_4}G_{k_2k_3}$.

Targets 1–3 are the article's displayed Gaussian integrals, target 4 is its pairing count, targets 5–6 are the two explicit consequences it records for the field correlators.

Significance

Wick's theorem is the computational content of every Feynman-diagram expansion: once it is available, a perturbative term is a finite sum over diagrams, and the symmetry factors of diagrams are bookkeeping on the pairing set $P_n$. On the probabilistic side it gives all moments of a Gaussian vector in closed form, which is the entry point to Gaussian chaos expansions, Wiener–Itô integrals, and moment methods for random matrices.

Mathlib (revision 0df444a) has real Gaussian measures gaussianReal, the general class IsGaussian of Gaussian measures on a topological vector space, the Gaussian integral $\int e^{-bx^2} = \sqrt{\pi/b}$, and the double factorial Nat.doubleFactorial, but no higher-moment formula for Gaussian measures and no Isserlis/Wick statement. The mission therefore produces new library-level content, not a re-derivation of existing formal results; the result itself has been classical since 1918 (Isserlis) and 1950 (Wick).

Difficulty

The obvious route — expand the characteristic function $\exp(-\tfrac12 t^{\mathsf T} G t)$ and differentiate $2n$ times at $t=0$ — requires differentiating under an integral sign $2n$ times and identifying the resulting combinatorial sum with a sum over pairings; both steps are where the formal work lies. Integrability is not automatic from the statement and has to be established (Gaussian measures have moments of all orders, but the product $\prod_j x_{k_j}$ must be shown integrable before any manipulation). The naive attempt to reduce to the independent case by diagonalizing $G$ meets a second difficulty: the change of variables must be tracked through the pairing sum, and $G$ may be singular, so no invertible whitening transform exists in general. The one-variable case (milestone 3) is not a special case to be waved through either: it is the statement the article singles out, because a naive "each mode pairs with a distinct partner" argument fails when all labels coincide.

Formalization scope

The ambient space is EuclideanSpace ℝ (Fin d); measures are Mathlib Measures and Gaussianity is the Mathlib class IsGaussian, which is defined by every continuous linear functional pushing forward to a real Gaussian law. Centering is stated as an explicit hypothesis on the coordinate means, so the measure is not assumed standard and the covariance is unconstrained (in particular degenerate covariances, and repeated labels $k_i = k_j$, are included). Integrals are Bochner integrals, which return $0$ for non-integrable functions; the statements are nonetheless non-vacuous because Gaussian measures integrate all polynomials.

Pairings are formalized as fixed-point-free involutions of Fin (2 * n) and the pair product ranges over $\{i : i < \sigma(i)\}$, so each pair contributes once. The case $n = 0$ is included: the empty product is $1$, the unique pairing of the empty label set is the identity, and both sides of the goal equal $1$. The double factorial is Mathlib's Nat.doubleFactorial, evaluated at 2 * n - 1 in truncated natural subtraction, so the $n = 0$ value is $0!! = 1$.

Contributions welcome: the Gaussian moment lemmas (milestones 1–3) as standalone Mathlib-style results, the pairing count (milestone 4) as pure combinatorics independent of the analysis, and any reduction of the goal to the independent-coordinate case.

Selected references

• L. Isserlis, On a formula for the product-moment coefficient of any order of a normal frequency distribution in any number of variables, Biometrika 12 (1918), 134–139. DOI: 10.1093/biomet/12.1-2.134
• G. C. Wick, The evaluation of the collision matrix, Physical Review 80 (1950), 268–272. DOI: 10.1103/PhysRev.80.268
• Feynman diagram, Wikipedia. https://en.wikipedia.org/wiki/Feynman_diagram

Motivation

Since the 2019 revision of the SI, seven constants of nature have fixed, exact numerical values: the caesium hyperfine frequency $\Delta\nu_{\mathrm{Cs}}$, the speed of light $c$, the Planck constant $h$, the elementary charge $e$, the Boltzmann constant $k$, the Avogadro constant $N_A$ and the luminous efficacy $K_{\mathrm{cd}}$. Every other constant is either measured, and then carries an uncertainty, or is a closed-form expression in the seven, and is then known exactly. The CODATA 2022 adjustment (Mohr, Newell, Taylor and Tiesinga, Rev. Mod. Phys. 97, 025002, 2025) is the authoritative statement of which constants fall on which side of that line, and of the statistical procedure that produces the recommended values of the measured ones.

The exactly known side of the line is pure mathematics: the tabulated value of the Stefan-Boltzmann constant, of the radiation constants, of the molar gas constant and of the Faraday constant are theorems about $\pi$, an integral, and rational arithmetic - not measurements. The measured side rests on one statistical object, the weighted linear least-squares fit of $N=133$ input data to $M=79$ adjusted constants, together with the diagnostics ($\chi^2$, the Birge ratio, normalized residuals, expansion factors) the task group uses to decide that the fit is acceptable. This mission formalizes both.

Setting

Write $h$, $c$, $k$, $e$, $N_A$ for the numerical values of the defining constants in coherent SI units, and $\hbar = h/2\pi$. The spectral radiance of a blackbody at thermodynamic temperature $T$, per unit frequency, is Planck's function

$$B_\nu(T,\nu) \;=\; \frac{2h\nu^3}{c^2}\,\frac{1}{e^{h\nu/kT}-1},$$

and per unit wavelength

$$B_\lambda(T,\lambda) \;=\; \frac{2hc^2}{\lambda^5}\,\frac{1}{e^{hc/(\lambda k T)}-1}.$$

The derived constants named in Tables XXXII and XXXIII of the paper are $\sigma = (\pi^2/60)k^4/\hbar^3c^2$ (Stefan-Boltzmann), $c_1 = 2\pi hc^2$ and $c_2 = hc/k$ (radiation constants), $R = N_Ak$ (molar gas), $F = N_Ae$ (Faraday), $K_J = 2e/h$ (Josephson) and $R_K = h/e^2$ (von Klitzing).

For the adjustment, let $A \in \mathbb{R}^{N\times M}$ be the design matrix of the linearized observational equations, $z \in \mathbb{R}^N$ the input data and $W \in \mathbb{R}^{N\times N}$ the weight matrix - the inverse of the covariance matrix of the data, symmetric and positive definite. The fit minimizes

$$\chi^2(x) \;=\; (z - Ax)^{\mathsf T} W (z - Ax), \qquad x \in \mathbb{R}^M,$$

with $\nu = N - M$ degrees of freedom, Birge ratio $R_B = (\chi^2/\nu)^{1/2}$ and normalized residuals $r_i = (X_i - \langle X_i\rangle)/u(X_i)$.

Formalization targets

Goal

$$\int_0^{\infty} \pi\,B_\nu(T,\nu)\,\mathrm{d}\nu \;=\; \sigma T^4 \qquad (T>0), \qquad \sigma = \frac{\pi^2}{60}\frac{k^4}{\hbar^3c^2}.$$

The goal fixes no digits: it asserts that the constant appearing in the tabulated closed form is exactly the one produced by integrating Planck's law over the spectrum and over a Lambertian hemisphere. The numerical enclosure of $\sigma$ is a separate, weaker milestone, so that the goal survives any change of tabulated digits.

Supporting targets

$$\int_0^\infty \frac{x^3}{e^x-1}\,\mathrm{d}x = \frac{\pi^4}{15}, \qquad \sigma = \frac{2\pi^5k^4}{15h^3c^2}, \qquad R = N_Ak, \qquad F = N_Ae,$$

together with the numerical enclosures of $\sigma$, of Wien's displacement constants $b = c_2/x_5$ and $b' = x_3k/h$ (where $x_5$, $x_3$ solve $x = 5(1-e^{-x})$ and $x = 3(1-e^{-x})$), and the identity $K_J^2R_K = 4/h$.

On the statistical side:

$$\chi^2(x) \;=\; \chi^2(\hat x) + (x-\hat x)^{\mathsf T}A^{\mathsf T}WA\,(x-\hat x) \quad\text{whenever}\quad A^{\mathsf T}WA\,\hat x = A^{\mathsf T}Wz,$$

the equivalence of minimality with the normal equations, the closed form $\hat x = (A^{\mathsf T}WA)^{-1}A^{\mathsf T}Wz$ when $A^{\mathsf T}WA$ is invertible, and the behaviour of $\chi^2$, $R_B$ and $r_i$ under an expansion factor $f$ applied to the uncertainties.

Significance

The exact-constant statements are what makes the tabulated values checkable rather than authoritative: a reader who accepts the SI definitions can, in principle, re-derive $R = 8.314\,462\,618\,153\,24\ \mathrm{J\,mol^{-1}K^{-1}}$ and $F = 96\,485.332\,123\,310\,0184\ \mathrm{C\,mol^{-1}}$ by arithmetic, and $\sigma = 5.670\,374\,419\ldots\times10^{-8}\ \mathrm{W\,m^{-2}K^{-4}}$ from Planck's law and $\zeta(4)$. Formalizing them turns "in principle" into a machine-checked derivation from the seven fixed numbers.

The least-squares statements make precise what the adjustment is, independently of the 133 data of this particular round: that the recommended values are the unique minimizer of a quadratic form, that the normal equations characterize it, and that multiplying a group of uncertainties by an expansion factor $f$ - the device used in 2022 with $f = 1.7$, $2.5$ and $3.9$ - rescales $\chi^2$ by $f^{-2}$, the Birge ratio by $f^{-1}$ and the residuals by $f^{-1}$, without moving the fitted values. None of these statements is new mathematics; none of them, as far as the catalog shows, is currently available as a machine-checked statement about the CODATA quantities.

Difficulty

Two hard points. First, $\int_0^\infty x^3/(e^x-1)\,\mathrm{d}x = \pi^4/15$: the obvious route expands $1/(e^x-1)$ as a geometric series and integrates term by term, which needs a dominated convergence or monotone convergence argument plus the value $\zeta(4)=\pi^4/90$; interchanging the sum and the integral is the step that must be justified, not assumed. The goal then needs this together with a change of variables $x = h\nu/kT$ on $(0,\infty)$ and an integrability argument for the original integrand.

Second, the numerical enclosures. $5.670\,374\,419\times10^{-8} < \sigma$ requires certified rational bounds on $\pi^5$; the Wien constants require certified bounds on a transcendental root, obtained from interval evaluation of $e^{-x}$ at rational points plus monotonicity of $x - n(1-e^{-x})$. Floating-point evaluation proves nothing here.

The least-squares milestones are routine linear algebra, with one subtlety: the decomposition identity needs symmetry of $W$, and the characterization of minimizers needs positive definiteness, so both hypotheses are carried explicitly.

Formalization scope

All physical quantities are plain real numbers: each constant is the numerical value of the quantity in the coherent SI unit named in its docstring, and the code carries no units. The defining constants are given by the exact decimal literals of Table XXXII, so they are exact rationals; $\hbar$ is defined as $h/2\pi$ and is therefore irrational.

Planck's function is a total function of two real arguments. Outside the physical regime it returns junk rather than failing - at $T = 0$ the exponent is $0$, the denominator $e^0 - 1 = 0$, and Lean's division returns $0$ - so every statement about it carries $0 < T$ and a positivity hypothesis on the spectral variable. The goal's integral is the Bochner integral over $(0,\infty)$ with respect to Lebesgue measure; it is not trivially true by non-integrability, since the integrand is integrable for $T>0$.

The adjustment is formalized over $\mathrm{Fin}\,N$ and $\mathrm{Fin}\,M$ with an arbitrary design matrix $A$ and an arbitrary weight matrix $W$, hypotheses on $W$ (Hermitian, positive definite) stated where they are used rather than baked into the definition; $\nu = N-M$ is an integer, not a truncated natural number.

Contributions welcome: the $\zeta(4)$ integral and the interval-arithmetic enclosures are reusable well beyond this mission, as are the least-squares statements.

Selected references

• P. J. Mohr, D. B. Newell, B. N. Taylor, E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, Rev. Mod. Phys. 97, 025002 (2025). https://doi.org/10.1103/RevModPhys.97.025002
• Bureau International des Poids et Mesures, The International System of Units (SI), 9th edition (2019). https://www.bipm.org/en/publications/si-brochure

Motivation

Linear systems are the inner loop of scientific computing: discretized differential equations, least-squares fitting, network flow balances and equilibrium models all end in $Ax = b$. Direct elimination solves the system exactly in $O(n^3)$ operations, but for the large sparse systems produced by discretization the cost and the round-off growth make iterative methods preferable: start from an arbitrary vector and apply a cheap update until the residual is small. The question such a method raises is when the iteration converges, and to that the chapter gives a clean sufficient answer: diagonal dominance.

This mission is the third in a series formalizing the lecture notes Métodos Numéricos by Sergio Roberto de Freitas (UFMS, 2000). It covers the iterative part of Chapter 5, Solução de Sistemas Lineares.

Setting

Let $A = (a_{ij})$ be a real $n \\times n$ matrix and $b \\in \\mathbb{R}^n$. Assume $a_{ii} \\neq 0$ for all $i$.

The Jacobi method computes every coordinate of the new iterate from the old one:

$$x_i^{(k+1)} = \\frac{1}{a_{ii}}\\left(b_i - \\sum_{j \\neq i} a_{ij} x_j^{(k)}\\right).$$

The Gauss-Seidel method updates the coordinates in order $i = 1, \\dots, n$ and uses the values already updated in the same sweep:

$$x_i^{(k+1)} = \\frac{1}{a_{ii}}\\left(b_i - \\sum_{j < i} a_{ij}x_j^{(k+1)} - \\sum_{j > i} a_{ij}x_j^{(k)}\\right).$$

Both are instances of an affine iteration $x^{(k+1)} = Bx^{(k)} + d$ associated with an equivalent rewriting $Ax = b \\iff x = Bx + d$.

The matrix $A$ is diagonally dominant when each diagonal entry dominates its row:

$$|a_{ii}| > \\sum_{j \\neq i} |a_{ij}| \\qquad (i = 1, \\dots, n).$$

Target

The goal theorem is Proposição 5.10.1: if $A$ is diagonally dominant and x^\\star solves Ax^\\star = b, then the Gauss-Seidel iterates converge to x^\\star from any starting vector.

The milestones are the general facts the source uses to get there: that the limit of a convergent affine iteration is a fixed point of it and hence a solution of the system (Proposição 5.5.1), that a contraction condition $\\lVert Bv \\rVert \\le c\\lVert v \\rVert$ with $c < 1$ forces convergence to the solution (Proposição 5.5.3), and that the Jacobi sweep has exactly the solutions of $Ax = b$ as its fixed points (Proposição 5.5.2).

Significance

Diagonal dominance is the hypothesis a practitioner can check by inspection, and it is satisfied by the matrices that come from standard finite-difference stencils, from strictly diagonally dominant collocation systems and from many equilibrium models. The theorem says that for those systems Gauss-Seidel needs no spectral analysis and no preconditioner to be safe: convergence holds from any starting vector. The supporting milestones isolate the two halves of the argument — a fixed-point identification and a contraction estimate — in a form reusable for other splittings (Jacobi, SOR, block variants).

Mathlib has Banach's fixed point theorem and the theory of matrix norms, but not the Gauss-Seidel sweep, the notion of diagonal dominance as used here, or the convergence statement, which is what this mission adds.

Difficulty

Gauss-Seidel is not a plain affine map applied coordinatewise: within one sweep the coordinates are updated sequentially, so the new value of coordinate $i$ depends on the new values of coordinates $j < i$. Formalizing the sweep therefore requires a recursion over the coordinate index before the recursion over the iteration counter, and the contraction estimate has to be propagated along that inner recursion. The classical proof compares \\max_i |x_i^{(k+1)} - x_i^\\star| with \\max_i |x_i^{(k)} - x_i^\\star| and needs, for each $i$, a bound that already uses the improved bounds for $j < i$; getting that induction right is the substance of the mission.

Formalization scope

Vectors are functions from a finite index type with $n$ elements to $\\mathbb{R}$, and convergence is convergence in that finite product space (equivalently, coordinatewise). The Gauss-Seidel sweep is defined through an auxiliary partial sweep: after $k$ inner steps the first $k$ coordinates carry their new values and the remaining ones their old values, and the full sweep is the partial sweep after $n$ steps. The Jacobi sweep is defined directly. Diagonal dominance is the strict inequality above, with the sum taken over the row with the diagonal index removed; for $n = 0$ every statement is vacuous, and the goal theorem is then trivially true because the space has a single point. Division by the diagonal entry is total division, so the definitions make sense even when $a_{ii} = 0$; diagonal dominance rules that out, because the right-hand side of the dominance inequality is nonnegative. The goal theorem assumes a solution x^\\star is given rather than asserting its existence, and it asserts convergence for every starting vector, generalizing the source's choice $x^{(0)} = 0$. The contraction milestone states the consistency of the norms as the hypothesis $\\lVert Bv \\rVert \\le c \\lVert v \\rVert$ in the supremum norm rather than fixing a particular matrix norm.

Selected references

• S. R. Freitas, Métodos Numéricos, Departamento de Computação e Estatística, Universidade Federal de Mato Grosso do Sul, 2000. Chapter 5, Solução de Sistemas Lineares, pp. 85–118. (Course notes supplied with this mission.)