All missions

Motivation

Chapter 4's framework (formalized in this series' 04-framework mission) solves the online covering-packing pair only in the restricted setting a(i,j) ∈ {0,1}, b(j) = 1 — every constraint is an unweighted "cover me with at least one of these" condition. Chapter 14 delivers the promise made at the very start of the survey (p. 115: "we show how to extend the ideas we present here to handle general (non-negative) values of a(i,j) and b(j)"): fully general non-negative coefficients, normalized so every constraint reads ∑_i a(i,j)x(i) ≥ 1. This mission formalizes both halves of that generalization — the packing scheme (Theorem 14.1, with a matching lower bound, Lemma 14.2, showing an extra additive term is unavoidable) and the covering scheme (Theorem 14.3, the goal).

Setting

Fix a finite set I of primal (covering) variables with positive costs c(i), and a finite set J of dual (packing) variables/covering constraints, with a(i,j) ≥ 0 for every pair (Fig. 14.1). The packing scheme (Section 14.1) is parameterized by a target competitive ratio B > 0: on each new dual variable y(j) and its coefficients a(i,j), the algorithm increases y(j) continuously and each x(i) by an explicit exponential increment function until the new primal constraint is satisfied, achieving B-competitiveness for the packing objective at the cost of an additive O(log(a_i(max)/a_i(min))) term (beyond the multiplicative O(log n)) in how much each dual constraint can be violated — qualitatively different from Chapter 4's purely multiplicative O(log d) bound, and Lemma 14.2 proves this additive term cannot be removed. The covering scheme (Section 14.2) instead works in phases: each phase assumes a doubling lower bound α(r) on OPT and "forgets" its primal/dual variables once the primal cost exceeds α(r), restarting with α(r+1) = 2α(r) — a structurally different mechanism from Chapter 4's direct algorithms, needed because with general coefficients a single monotone run can no longer be analyzed via one potential function alone.

Formalization targets

Theorem 14.3 (the goal, p. 253): for any B > 0, the phase-based covering scheme (each constraint normalized to ∑_i a(i,j)x(i) ≥ 1/B) is competitive with an explicit ratio 8 log(2n)/B, taken directly from the proof's own final displayed chain, 2α(r) ≤ 4α(r-1) ≤ (8 log(2n)/B) Y(r-1) ≤ (8 log(2n)/B) OPT (p. 253-254) — the theorem's own statement only gives O(log n/B), so this explicit constant is this mission's own instantiation from the proof, not an independent derivation and not a transcription of a displayed theorem-level formula (flagged, per this series' explicit-constants rule).

Two milestones, in attack order:

• Theorem 14.1 (p. 249): the packing scheme is B-competitive, and violates each dual constraint by at most the book's own exact displayed bound c(i)·2log(1 + n·a_i(max)/a_i(min))/B (Claim (3) — the exact constant the proof establishes, not the theorem headline's O(·) simplification).
• Lemma 14.2 (p. 251): a matching lower bound, on the book's own explicit single-constraint instance, showing the additive log(a(max)/a(min)) term of Theorem 14.1 is necessary.

Significance

This chapter is the survey's demonstration that the primal-dual framework's core technique survives its most natural generalization, at the price of an explicit extra term the chapter also proves is unavoidable — a tight characterization, not merely an upper bound. Every other online covering/packing chapter in this survey (set cover, routing, ad-auctions, bounded allocation) is technically a special case of this chapter's general model; Chapter 4's restricted framework is the pedagogical entry point, and this chapter is where the general theory actually lives. No formal development of the general packing-covering problem was found on the platform as of 2026-09-20; this mission is the first.

Difficulty

Two distinct obstacles, mirroring this chapter's own two schemes. First, Theorem 14.1's proof (p. 249-251) establishes its per-round primal/dual derivative inequality via a direct calculus argument (differentiating the explicit increment function) — formalized here as a hypothesis (hX_le_BY) standing for that calculation, not reproduced, since the goal is a faithful statement of the resulting competitive ratio, and the increment function's own exponential form is transcribed in the theorem's docstring but the differentiation itself is out of scope. Second, Theorem 14.3's phase-based mechanism is genuinely stateful across an unbounded number of phases (each phase resets its own primal/dual variables while the LP's actual variables retain the running maximum) — modeling this process explicitly is comparable in complexity to Chapter 13's level-based algorithm, and this mission makes the same scope choice: the mechanism's output (the resulting cost/profit relationship, hX_le_ratio) is taken as a hypothesis standing for the book's own Claims (1) and (3) combined, rather than constructed phase-by-phase.

Formalization scope

GeneralInstance I J bundles Fig. 14.1's fully general LP data (a(i,j) ≥ 0, c(i) > 0) — restated locally (not importing 04-framework's CoveringInstance) per this series' rule against cross-draft imports, even though this chapter is the direct generalization of that one. aMax/aMin are the per-variable (not per-instance) maximum and minimum-non-zero coefficients Theorem 14.1 needs. harmonicNum is restated locally (duplicated from 13-bounded-allocation's own definition, for the same no-cross-draft-import reason). Both goal-adjacent theorems use this series' weak-duality "competitive against any feasible comparison solution" pattern (04-framework, reused as a convention, not re-derived): Theorem 14.1 against any feasible packing comparison (matching that it concerns the packing side), Theorem 14.3 against any feasible covering comparison (matching the covering side). Welcome contributions: completing the three sorrys (Theorem 14.1's calculus argument, Theorem 14.3's phase-based mechanism constructed explicitly, and Lemma 14.2's direct summation argument, which is the most tractable of the three to actually prove), and formalizing the sanity check that both schemes reduce to Chapter 4's Algorithm 1/2/3 when a(i,j) ∈ {0,1}, b(j) = 1 (checked by hand in SELF_REVIEW.md, not as a Lean lemma).

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

Network routing is one of the paradigmatic applications of the online primal-dual method: requests for bandwidth between a source and target arrive one at a time, and the algorithm must commit bandwidth to paths without knowing future requests. Chapter 4 already gave a simple (3, O(log n))-competitive routing algorithm as an illustration of the general framework. This chapter asks for something qualitatively stronger: a uni-criteria (1, O(log n))-competitive algorithm — one that routes the full optimal bandwidth (no loss on the throughput side at all), paying only in a bounded edge-capacity violation. The chapter shows this exact-throughput guarantee is achievable, and is moreover the key building block for several other routing objectives (fair routing, max-min fairness) built on top of it in Section 9.2 — a (1, O(log n))-competitive algorithm composes into those richer objectives in a way a merely constant-factor-lossy algorithm does not.

Setting

Fix a graph $G=(V,E)$, $|V|=n$, $|E|=m$, with integer edge capacities $u: E \to \mathbb{N}$. Routing requests $r_i$ arrive online, each demanding one unit of bandwidth between a source and target; in the splittable model (this chapter's comparison class), a request's bandwidth may be divided across multiple paths. A $(c_1,c_2)$-competitive algorithm routes at least $1/c_1$ of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most $c_2$. The chapter's generic algorithm (Section 9.1) maintains, for each of $O(\log n)$ copies $G_0,\dots,G_k$ of the graph (copy $j$ keeping only edges of capacity at least $m^j$, each capped at $\min(u(e), m^{j+2})$), a primal-dual pair matching Chapter 4's own routing LP (Fig. 9.1, identical to Fig. 4.2): a request is routed on the shortest path (by the copy's current primal edge-lengths $x(e,j)$) if that length is below $1$, multiplicatively updating $x(e,j)$ on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.

Formalization targets

Theorem 9.2 (goal, p. 204): the algorithm is (1, O(log n))-competitive with respect to all splittable routing solutions — exact throughput (ratio 1), edge load at most O(log n).

Lemma 9.1 (milestone, p. 202-204): a single copy $G_j$'s own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least $M$ (the maximum splittable bandwidth achievable in $G_j$, out of the requests introduced to it) and incurs load $O(\log n)$ on every edge of $G_j$.

Significance

This is the survey's demonstration that the online primal-dual method, in its most basic form (a single accumulating dual sum driving a multiplicative primal update, exactly Chapter 4's framework), scales to a genuinely harder bicriterion objective once composed across a carefully constructed family of graph copies — the copies are what let the algorithm avoid ever needing to reason about which of the exponentially many $s_i$-$t_i$ paths to consider, reducing routing to a sequence of independent shortest-path computations. The chapter's own Section 9.2 builds a coordinate-wise-competitive fair-routing algorithm directly on top of Theorem 9.2 (not formalized here), and its Notes section places $(1, O(\log n))$-competitiveness as "a crucial non-trivial step" the chapter needed before those richer objectives became tractable at all. No prior formalization of online routing, splittable or otherwise, was found on the platform as of 2026-09-20 (search below).

Difficulty

This is the most algorithmically intricate chapter in this series: the algorithm processes each request against every one of $O(\log n)$ graph copies, each copy running its own instance of the Chapter-4-style primal-dual update, and Theorem 9.2's own proof composes Lemma 9.1's per-copy guarantee via a combinatorial backward induction (partitioning the offline-optimal solution's paths into groups by bottleneck capacity, and showing group by group that the algorithm's cumulative routed bandwidth across the top levels dominates the cumulative optimal bandwidth in those groups) together with a separate geometric argument bounding how many copies any single edge can meaningfully appear in. Fully modeling the copy construction, the request-routing process, and both composition arguments from first principles was judged to exceed this mission's time budget without sacrificing the faithfulness of what does get stated (per CAPTAIN_BRIEF.md rule 6). Instead: Lemma 9.1 is formalized via the two facts its own proof isolates as doing the real work — a weak-duality contradiction bound (stepB ≥ M − uMin) and the step-(1c) fallback's own greedy-fill rule for part (i); the multiplicative-update invariant x(e,j) ≤ 2 for part (ii), whose consequence — the exact constant 2 + 6·log₂n — is re-derived from scratch in this mission (the displayed equation this derivation depends on was garbled by the PDF's text extraction; it was confirmed against the actual typeset page image before drafting, see SELF_REVIEW.md). Theorem 9.2 then composes Lemma 9.1 across copies via two explicit, clearly-labeled hypotheses standing for the book's own backward-induction accounting and edge-multiplicity argument, respectively — genuine mathematical content this mission does not re-derive, named honestly as hypotheses rather than silently assumed away or approximated by a weaker statement.

Formalization scope

No shared data structure was introduced: every quantity in both theorems (bandwidths, capacities, loads) is a plain real-number hypothesis-level parameter, since neither theorem's own content needs a reusable instance record (unlike the packing/covering CoveringInstance of 04-framework, this chapter's per-copy quantities are consumed once each, not threaded through a family of algorithms). per_copy_guarantee (Lemma 9.1) takes the weak-duality bound, the step-(1c) fill rule, and the x(e,j)≤2 invariant as hypotheses and derives both parts of the lemma's conclusion by real algebra (a sign case-split for part (i); Real.logb/rpow manipulation for part (ii)). routing_competitive (Theorem 9.2) takes Lemma 9.1's guarantee (universally quantified over the copy index J, a general Fintype) plus the two composition hypotheses described above, and derives the bicriterion conclusion by summation, transitivity, and scaling. This correctly rules out the trivializing formalization in which the composition hypotheses are strengthened to directly assert the theorem's own conclusion (each is a strictly weaker, independently-motivated fact — the backward-induction accounting identity and the geometric edge-multiplicity bound — checked in MODERATION_NOTES.md against this exact failure mode). Reals throughout; Real.logb 2 for log₂. Welcome contributions: completing the two sorrys (Lemma 9.1's part (i) is short algebra; part (ii) needs Real.rpow/Real.logb lemmas; Theorem 9.2's is transitivity/summation once its hypotheses are in hand), and — the natural follow-on — formalizing the copy construction and the backward-induction/edge-multiplicity arguments hquota/hload_aggregation currently stand in for, which would upgrade them from hypotheses to theorems in their own right; Section 9.2's coordinate-wise-competitive fair-routing algorithm (Theorem 9.3) and the matching lower bound (Lemma 9.5) are further natural follow-ons.

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

The metrical task system (MTS) problem is one of the earliest and most general online models: a server occupies a state in a metric space, requests arrive with per-state service costs, and the server may change state (paying the metric's transition cost) before serving each request. On a general metric, competitive algorithms are hard to design directly. Chapter 6 shows that on a weighted star metric — the simplest genuinely non-uniform metric, a hub with leaves at varying distances — the online primal-dual framework of Chapter 4 becomes applicable, but only after a change of rules: the chapter defines a new MTS model, in which the server may change state only at the boundary of a "phase" (an interval during which its accumulated service cost reaches the state's own transition charge), and shows this new model is cost-equivalent, up to a constant factor, to the standard model. This equivalence is what licenses recasting the (new-model) problem as a covering linear program with the online primal-dual framework directly applicable — the chapter's actual algorithmic payoff (an unnumbered $O(\log N)$-competitive result, Section 6.2) rests entirely on it.

Setting

Fix a set of leaves $V$ (the book's finite $\{1,\dots,N\}$) of a weighted star, each leaf $i$ at distance $d'(i) \ge 0$ from the center. The chapter immediately collapses the full star metric to a single per-state transition charge $d(i) := 2d'(i)$, since on a star every transition $i \to j$ costs at most $d'(i) + d'(j)$, and charging the doubled source leaf's distance alone (never charging for arriving) upper-bounds every transition cost independent of destination. A standard-model solution is a finite sequence of runs, each specifying a state $s_i$ occupied and the service cost $w_i \ge 0$ accumulated while in that state, ending with a transition (cost $d(s_i)$) to the next run's state; its total cost is $\sum_i (w_i + d(s_i))$. A new-model solution is a finite sequence of phases, each specifying a state visited; a phase's cost is exactly $d(\text{state})$ regardless of how much service actually occurred during it (a state change is only permitted once a phase's accumulated service reaches the phase's own $d$-value), so the new model's total cost is $\sum_i d(s_i)$.

Formalization targets

Lemma 6.1 (goal, p. 144): any standard-model solution's runs $(s, w)$ transform into a new-model solution whose cost is at most $2 \cdot \sum_i (w_i + d(s_i))$; in particular $OPT_n(\bar\sigma) \le 2 \cdot OPT_o(\bar\sigma)$.

Lemma 6.2 (milestone, p. 145): any new-model solution's phases $(s, w)$, with each phase's actual service $w_i \le d(s_i)$, are simultaneously a legal standard-model solution (the same trajectory, recosted) whose standard-model cost is at most $2 \cdot \sum_i d(s_i)$.

Together (stated in the book but not separately numbered, hence not a formalization target here): a $c$-competitive algorithm in the new model implies a $4c$-competitive algorithm in the standard model.

Significance

This is a model-equivalence result, a distinct and recurring pattern in online algorithm design from the competitive-ratio bounds formalized elsewhere in this series: rather than analyzing an algorithm directly, the chapter first shows that solving an easier, more restricted version of the problem (state changes only at phase boundaries) loses only a constant factor, and only then designs an algorithm for the restricted version. The technique generalizes (the chapter's own Notes section places it in the context of Borodin et al.'s original MTS bounds, and of later work on hierarchically well-separated trees for general metrics), but this chapter gives its cleanest, self-contained instance: two short, tight (factor-2 each direction) transformations between two formally distinct online cost models. No prior formalization of metrical task systems on a weighted star, or of this new/standard model equivalence, was found on the platform as of 2026-09-20 (search below); the platform's existing KServer.* campaign formalizes a different online problem (uniform-metric $k$-server) with a different metric structure and is not adjacent substrate for this chapter's weighted-star MTS model.

Difficulty

The central obstacle is representing "a solution" at a level of abstraction faithful to the book's own proof without committing to a full continuous-time process model (states as functions of a real time variable, phases as recursively-defined stopping times, requests as an explicit arriving sequence) that neither lemma's own proof actually needs. Both proofs work entirely at the granularity of a solution's runs (standard model) or phases (new model) — finite sequences of (state, cost) data — never referencing continuous time except to justify that this decomposition exists. This mission formalizes both lemmas at exactly that granularity: a run/phase sequence indexed by Fin k, with costStandard/costNewPhases the book's own displayed cost formulas. Lemma 6.1's proof genuinely constructs a new object (the delayed-transition solution $S'$) and only bounds its cost, never gives $S'$ a closed form — formalized here as an existential over a per-segment cost witness w', bounded above and below exactly as the proof's own argument does (with the lower bound d(s i) ≤ w' i serving as the guard against the vacuous witness w' = 0, since without it the existential is trivially satisfiable and asserts nothing). Lemma 6.2's proof, by contrast, reuses the same trajectory in both models with no construction at all, formalized directly as a cost comparison between costStandard and costNewPhases applied to the identical (s, w) data.

Formalization scope

WeightedStar V bundles centerDist : V → ℝ (the book's $d'$) with non-negativity; WeightedStar.d is the collapsed charge $d(i) = 2d'(i)$. costStandard/costNewPhases are literal transcriptions of the two models' displayed cost formulas over a Fin k-indexed run/phase sequence. standard_to_new (Lemma 6.1) is the existential described above; new_to_standard (Lemma 6.2) is the direct cost comparison. Reals throughout; V is left a general Type* (not assumed Fintype) since neither lemma's own statement needs the chapter's finiteness assumption $|V|=N$ — that assumption only matters for the unnumbered $O(\log N)$-competitive claim of Section 6.2, out of scope per BRIEF.md's explicit instruction (no numbered theorem to formalize it against). This correctly rules out the trivializing formalization in which "new-model solution" is left as an unconstrained free variable satisfying only the conclusion's own inequality, or in which the star structure is dropped entirely in favor of an arbitrary metric (the chapter's own reduction to a per-state charge $d(i)$, rather than a full metric $d: V\times V\to\mathbb R$, is precisely what the star's structure licenses, and is preserved here via WeightedStar.d rather than a bare hypothesis-level function). Welcome contributions: completing the two sorrys (Lemma 6.1's needs an explicit construction of $S'$ and its per-segment cost bound; Lemma 6.2's is a short termwise algebraic argument), and formalizing the Section 6.2 covering-LP algorithm and its $O(\log N)$-competitive claim as a follow-on mission once it can be stated against a numbered result.

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
• Bansal et al., reference [14] of this chapter's own bibliography (not independently verified by this mission), cited by the book as the source of the weighted-star MTS results this chapter presents ("The results in this chapter are based on the work of Bansal et al. [14]," p. 147).
• Borodin, Linial, Saks, reference [29] of this chapter's own bibliography (not independently verified by this mission), cited as the paper that originally formulated the standard MTS model and its tight $2N-1$ deterministic bound (p. 147).

Why neighborly families matter

A neighborly family of convex polytopes is a collection in which every two distinct members meet in the largest dimension possible without having a full-dimensional overlap: their intersection has codimension one. The question is extremal. For a fixed ambient dimension, how large can such a family be when its members must also satisfy a geometric restriction? Chapter 7 of Branko Grünbaum's Convex Polytopes records Joseph Zaks's answer for central symmetry: in every dimension at least three, no finite upper bound exists. The result belongs to discrete geometry because it combines pairwise intersection constraints, dimension, and symmetry across an entire finite family rather than studying the face structure of one polytope.

The theorem is cited by Grünbaum in §7.5 as the resolution of a problem posed in §7.4. The original result is Zaks's 1986 paper, “Arbitrarily large neighborly families of symmetric convex polytopes”. This mission formalizes the centrally symmetric conclusion quoted in the textbook, without adding the stronger congruence variants discussed elsewhere.

Geometric setting

Fix an integer $d\ge 3$ and work in the real coordinate space $\mathbb{R}^d$. In Lean this space is represented by Fin d → ℝ. A $d$-polytope is a nonempty finite convex hull whose affine span is the entire ambient space. Full affine span is essential: it rules out treating a lower-dimensional polytope embedded in $\mathbb{R}^d$ as a $d$-polytope.

A polytope $P$ is centrally symmetric when there is a center $c\in\mathbb{R}^d$ such that reflection through $c$ leaves $P$ invariant. The center is chosen separately for each member of the family; the theorem does not require one common center. In coordinates the reflection is $x\mapsto 2c-x$, represented in Lean by AffineEquiv.pointReflection ℝ c.

A finite family $S$ of $d$-polytopes is neighborly in the sense of Grünbaum §7.4 when, for every distinct $P,Q\in S$, the intersection $P\cap Q$ has affine dimension $d-1$. This use of “neighborly” concerns pairwise intersections among several convex sets. It is different from the familiar notion of a neighborly polytope, where small subsets of the vertices of a single polytope span faces.

Formalization target

For every $d\ge 3$ and every natural-number threshold $N$, the target asserts the existence of a finite set $S$ such that

$$|S|\ge N,$$

every $P\in S$ is a centrally symmetric $d$-polytope, and every distinct pair $P,Q\in S$ satisfies

$$P\cap Q\ne\varnothing, \qquad \dim\!\bigl(\operatorname{aff}(P\cap Q)\bigr)=d-1.$$

Quantifying over every threshold $N$ is the precise finite formulation of “arbitrarily large.” It does not claim that one infinite family has all these properties. The witness family may depend on both $d$ and $N$.

Significance

The result shows that central symmetry does not impose a finite ceiling on neighborly-family size once $d\ge 3$. The conclusion is therefore a structural existence statement, not merely a construction of a single large example. It also separates two issues that can otherwise be conflated: each member has an internal symmetry, while neighborliness is a relation between distinct members.

The mathematics is known, but the Lean item in this mission is statement-only and remains to be proved. A complete formalization would connect finite convex-hull geometry, affine dimension, affine reflections, and pairwise intersections in one reusable development. The full-dimensional polytope predicate is shared across the textbook series and is packaged as an expression-essential definition rather than hidden inside the theorem.

Difficulty

The quantified size threshold prevents a finite catalogue or a fixed example from resolving the target. The pairwise condition also couples every new member to all earlier members: verifying central symmetry for each polytope alone gives no control over the dimensions of its intersections with the rest of the family. The explicit nonemptiness condition matters because affine dimension is represented with a natural-valued finrank; without it, conventions for the empty affine span could obscure the intended codimension-one requirement.

Formalization scope

The family is a Finset, so its members are distinct and its cardinality is the ordinary finite cardinality. Every member satisfies Grunbaum2003.IsDPolytope, which requires a nonempty finite generating set, equality with its convex hull, and full affine span. Central symmetry is expressed by invariance under a point reflection with an individually quantified center. For distinct members, the intersection must be nonempty and the rank of the direction of its affine span, plus one, must equal $d$.

No common center, congruence, translate-only model, face-to-face condition, or infinite-family claim is included. The case $d=3$ is included, while dimensions below three are excluded exactly as in the source. The case $N=0$ is harmless because the same theorem is quantified over every positive threshold as well. The scope contains the one reviewed Zaks theorem and its single expression-essential polytope definition; it does not introduce unrelated chapter theorems or a proof strategy.

Selected references

• Joseph Zaks, Arbitrarily large neighborly families of symmetric convex polytopes, Geometriae Dedicata 20 (1986), 175–179. DOI: 10.1007/BF00164398
• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003. DOI: 10.1007/978-1-4613-0019-9

Why subpolytopes matter

A convex polytope can be studied metrically, through coordinates and lengths, or combinatorially, through the inclusion order of its faces. Grünbaum's Convex Polytopes develops the second viewpoint systematically: two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. Chapter 7 studies neighborly polytopes, which have as many low-dimensional faces as their vertex sets permit. These objects are central test cases because very strong local face incidence coexists with a large variety of realizations and combinatorial types.

The capstone of this mission is the rigidity statement attributed in §7.5 to Shemer: in even dimension, the combinatorial type of a neighborly polytope determines the combinatorial type of every subpolytope spanned by a subset of its vertices. Here “rigid” is exclusively combinatorial. It does not assert preservation of lengths, angles, coordinates, or projective realization. The source statement appears in Branko Grünbaum, Convex Polytopes, second edition, §7.5, printed p. 129b / PDF p. 161 (Springer edition).

Polytopes, faces, and neighborliness

The Lean development represents the ambient real space of dimension $d$ as Fin d → ℝ. A predicate IsDPolytope P says that $P$ is the convex hull of a finite nonempty vertex set and has full affine span. Faces are modeled by Mathlib's exposed-face predicate. The type PolytopeFace P contains all exposed faces ordered by inclusion, including the empty face and $P$ itself; an order isomorphism of these types is the formal representation of combinatorial equivalence.

For a positive integer $k$, a polytope is $k$-neighborly when every $k$-element set of vertices spans a proper face and is exactly the vertex set of that face. The definition IsKNeighborly k P states this directly for finite sets of exposed singleton vertices. Grünbaum defines an even-dimensional polytope of dimension $2r$ to be neighborly when it is $r$-neighborly. The theorem therefore assumes $r \ge 1$ and uses IsKNeighborly r for both parent polytopes.

Formalization target

Let $P$ and $Q$ be full-dimensional neighborly polytopes in $\mathbb{R}^{2r}$. Their vertices are enumerated injectively by maps $V,W : \operatorname{Fin}(m) \to \mathbb{R}^{2r}$. A permutation $\theta$ records the prescribed correspondence between the two vertex sets, and an order isomorphism $\Phi$ between the full face posets witnesses that this correspondence comes from a combinatorial equivalence of the parent polytopes.

For every index set $I \subseteq \operatorname{Fin}(m)$, the target produces an order isomorphism

$$\mathcal F\bigl(\operatorname{conv}(V(I))\bigr) \simeq \mathcal F\bigl(\operatorname{conv}(W(\theta(I)))\bigr),$$

and requires it to carry each selected singleton vertex $V(i)$ to $W(\theta(i))$. The quantifier over $I$ is unrestricted. Empty, singleton, lower-dimensional, and full vertex subsets are all included. No selected subpolytope is required to be full-dimensional or neighborly.

What the theorem determines

Knowing only how many neighborly combinatorial types exist would not reconstruct any particular vertex-induced subpolytope. The rigidity theorem is stronger: once the complete face-poset type of the parent and its vertex correspondence are fixed, the complete face-poset type of every labelled vertex subpolytope is fixed as well. This is why the formal conclusion keeps the label-preservation clause rather than stating only the existence of an abstract order isomorphism.

The result is known mathematics, while the Lean declaration supplied here is statement-only and retains sorry as its proof placeholder. The formalization contribution is therefore a precise target and its expression-essential vocabulary, not a claim that Shemer's proof has already been machine checked. A completed proof must establish exactly this uniform reconstruction theorem without adding metric hypotheses or restricting the allowed subsets.

Where the difficulty lies

The parent face-poset isomorphism directly identifies the faces already present in $P$ and $Q$, but a subpolytope can have faces that are not faces of its parent. Consequently, restricting $\Phi$ to selected vertices does not automatically yield the required subpolytope face-poset isomorphism. The theorem must control how all new faces created by taking a vertex subset depend on the original neighborly combinatorics. That gap is the substantive content of rigidity and prevents the conclusion from being a routine restriction of the given parent isomorphism.

Formalization scope

The scope is deliberately narrow. IsDPolytope, IsKNeighborly, and PolytopeFace are the only local definitions required to express the theorem. Vertices are exposed singletons, combinatorial types are full face-poset order types, and convex hulls remain in the original ambient space even when a selected subset is lower-dimensional. The theorem assumes positive even dimension through $2r$ with $r \ge 1$. It imposes no metric congruence, no choice of realization normal form, and no cardinality lower bound on the selected subset.

Useful contributions include a proof of the stated target and reusable lemmas connecting neighborliness, vertex subsets, and exposed-face posets. A reformulation that covers only nonempty or full-dimensional subsets, forgets the prescribed vertex labels, or replaces face-poset equivalence by equality of face counts would not satisfy this mission.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Graduate Texts in Mathematics 221, Springer, 2003, especially §§2.4, 3.1–3.2, 7.1–7.2, and 7.5. DOI

Motivation

A polytope can be represented not only by vertices or supporting inequalities, but also as a section of a simplex in a higher-dimensional space. Perles's prescribed-point theorem strengthens this representation: the cutting flat can be required to pass through an interior point selected in advance. This is Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition, §5.1, printed p. 74. The result isolates how a bound on the number of facets controls the dimension of a universal simplex while retaining freedom to prescribe a point in the section.

Setting

Fix natural numbers $d$ and $k$. A $d$-polytope $P\subseteq\mathbb R^d$ is represented here as a nonempty convex hull of finitely many points whose affine span is all of $\mathbb R^d$. A face is the complete maximizing locus of a supporting linear functional, and a facet is a nonempty face of affine dimension $d-1$. The quantity used in the target counts geometric faces, not the number of inequalities in a chosen description.

A $k$-simplex is the convex hull of $k+1$ affinely independent points $v_0,\ldots,v_k$ in $\mathbb R^k$. Write this simplex as $T$. Affine independence makes $T$ full-dimensional, so $\operatorname{int} T$ is its ordinary ambient interior. No regularity, coordinate normalization, or metric condition is imposed on $T$. A $d$-flat is a translate of a $d$-dimensional linear subspace. Its section of $T$ is the whole intersection $T\cap L$.

Two subsets are affinely equivalent when an affine bijection between their affine spans maps one set exactly onto the other. Distances and angles need not be preserved. In the formal statement this equivalence is witnessed by an injective affine map $A:\mathbb R^d\to\mathbb R^k$ whose range is $L$ and whose image of $P$ equals $T\cap L$.

Formalization target

The single target is the prescribed-point section theorem:

$$\begin{aligned} &P\subseteq\mathbb R^d\text{ is a }d\text{-polytope with at most }k+1\text{ facets},\\ &T\subseteq\mathbb R^k\text{ is a }k\text{-simplex},\quad p\in\operatorname{int}T\\ &\qquad\Longrightarrow\quad \exists\text{ a }d\text{-flat }L\subseteq\mathbb R^k:\ p\in L \text{ and }T\cap L\cong_{\mathrm{aff}}P. \end{aligned}$$

Grünbaum writes the number of allowed facets as $f$ and uses an $(f-1)$-simplex in $\mathbb R^{f-1}$. The Lean statement sets $f=k+1$. Every input, including the simplex and its interior point, is universally quantified before $L$ and $A$ are chosen. Thus the witnesses may depend on all the input data, but neither the simplex nor the prescribed point may be chosen to suit $P$.

Significance

The theorem gives a controlled simplex-section representation for every polytope with a bounded number of facets. Its prescribed-point clause is stronger than merely asserting that some section somewhere is affinely equivalent to $P$: it permits the ambient simplex and any one of its interior points to be fixed first. The equality $A(P)=T\cap L$ also covers the entire section, excluding a weaker containment statement.

This is a known theorem, not an open conjecture. The package supplies a source-reviewed, compiling Lean statement with a proof placeholder. A complete contribution would replace that placeholder by a machine-checked proof while preserving the facet bound, the arbitrary-simplex quantifier, the prescribed point, the flat dimension, and the exact affine-equivalence conclusion.

Difficulty

A flat chosen only to pass through $p$ may cut out the wrong affine shape, while a flat producing the correct shape need not contain the prescribed point. The theorem requires both conditions simultaneously for every allowed simplex and every interior point. Restricting to a regular simplex, moving the chosen point, or proving only an unrestricted section representation would lose essential quantifiers from the source statement.

The facet allowance also refers to geometric facets rather than a particular inequality presentation. A formal proof must therefore connect the combinatorial boundary data of $P$ with the geometry of the simplex section without replacing the source hypothesis by a representation-dependent count.

Formalization scope

Lean represents $\mathbb R^d$ by Fin d → ℝ. Grunbaum2003.IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. Grunbaum2003.faceCount P r is the finite cardinality of nonempty exposed faces whose affine-span direction has dimension $r$. For $d>0$, the hypothesis uses faceCount P (d - 1). For $d=0$, the formal statement makes the facet allowance automatic; this avoids natural-number underflow while retaining the zero-dimensional source case.

The simplex is convexHull ℝ (Set.range v) under AffineIndependent ℝ v, and interior is ambient interior. The witness L is an affine subspace containing $p$ with direction dimension $d$. The affine map is injective, has range exactly $L$, and maps all of $P$ onto the full intersection. These conventions rule out degenerate simplices, lower-dimensional input polytopes, containment-only conclusions, and vacuous facet counts.

The two definition files are expression-essential and shared with other missions in this textbook series. No proof-only theorem is packaged, and there is no separate reviewed source lemma to list as a milestone.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 5.1.10, printed p. 74; section convention printed p. 71. DOI.

Motivation

The face structure of a cube is unusually regular: its vertices, edges, and higher dimensional faces are indexed by choices of fixed and free coordinates. A natural realization question asks how much of this structure can survive in a polytope of lower dimension. In §4.9 of Convex Polytopes, Grünbaum reports the Joswig–Ziegler construction of neighborly cubical polytopes. The source result says that a cubical $d$-polytope can retain a prescribed low dimensional skeleton of an $n$-cube even when $n>d$. It concerns the entire pattern of faces and containments within that skeleton, rather than a count of vertices or edges alone. The theorem appears on printed page 69b (PDF page 95) of the supplied 2003 edition.

Setting

Fix natural numbers $n>d\geq2$. A $d$-polytope here is a nonempty finite convex hull $P\subseteq\mathbb R^d$ with full affine span. A face is an exposed subset of $P$; the empty face and $P$ itself are included in the face poset. Its order is set inclusion. For a nonempty face, dimension is the dimension of its affine span. The standard $n$-cube is $[0,1]^n$ in $\mathbb R^n$, described coordinatewise by $0\leq x_i\leq1$.

A cubical $d$-polytope is such a full dimensional polytope whose every facet, meaning every nonempty exposed face of dimension $d-1$, has a full face poset order isomorphic to the face poset of a standard $(d-1)$-cube. This is combinatorial cubicality: a facet need not be congruent or affinely equal to a metric cube. It also does not say that the vertices of $P$ have binary coordinates.

The $k$-skeleton face poset consists of the empty face together with all exposed faces of affine dimension at most $k$, with their inherited inclusion order. The source speaks of a skeleton “of” an $n$-cube: the intended correspondence preserves and reflects face containment across the two ambient dimensions. An order isomorphism of the two skeleton face posets is the Lean expression of that combinatorial equivalence.

Formalization target

The single target is the unnumbered Joswig–Ziegler existence theorem as reported by Grünbaum. For every $n>d\geq2$, with $k=\lfloor d/2\rfloor-1$, it asks for a cubical $d$-polytope $P$ such that

$$\operatorname{Skel}_k(P)\cong\operatorname{Skel}_k([0,1]^n).$$

The witness $P$ may depend on both $n$ and $d$. The strict inequality $n>d$ and lower bound $d\geq2$ are source conditions. They have not been expanded or narrowed for this package. For $d=2$ and $d=3$, the cutoff is zero, so the skeleton includes the empty face and vertices. At larger dimensions the claim includes all faces through the stated cutoff and their order relations.

In Lean the theorem is Grunbaum2003.neighborly_cubical_realization. Its conclusion supplies a set in Fin d → ℝ, proves the cubical-polytope predicate of that set, and supplies a nonempty type of order isomorphisms between the two skeleton face posets. The declaration is a compiled statement with a sorry body. No machine-checked proof of the existence theorem is claimed here.

Significance

This theorem separates dimension of realization from the low dimensional combinatorics being realized. In particular, an $n$-cube skeleton can occur inside a lower dimensional cubical polytope, subject to the precise cutoff above. The conclusion is a structural face-poset match, not a numerical face-vector equality. A complete formal proof would establish an existence statement about genuine full dimensional convex polytopes and an order equivalence of their truncated face systems.

The reusable formal objects in this package are the full dimensional polytope predicate, the face subtype, the skeleton subtype, the standard cube, and the cubical-polytope predicate. They express the geometry and combinatorics independently of the particular neighborly realization theorem. The goal is kept as one mission because the source states one dimension-parametric existence result; the definitions are only its expression dependencies.

Difficulty

A lower dimensional realization cannot retain every face of a higher dimensional cube. The theorem therefore specifies exactly which dimensions of faces can be preserved. Merely matching the number of vertices would leave edges, higher faces, and incidence unconstrained. Likewise, requiring all facets to look like cubes says nothing by itself about whether a large cube's skeleton appears. A proof must produce a genuine cubical witness and the ordered skeleton correspondence simultaneously, for every allowed pair of dimensions.

Formalization scope

The Lean coordinate spaces are real functions on Fin d and Fin n. Natural division d / 2 is floor division, and the assumption $d\geq2$ makes natural subtraction by one agree with the source's integer cutoff. The full dimensional condition rules out an empty or lower dimensional witness. IsExposed supplies faces, including the improper empty and whole faces; the skeleton predicate treats the empty face explicitly because its conventional dimension is $-1$, outside natural-number dimensions. The nonempty face dimension is the finrank of the affine direction.

The face-poset order is inherited from set inclusion. Cubicality is checked on each qualifying facet by an order isomorphism with the full face poset of the reference cube. The target's order isomorphism similarly covers the whole selected skeleton rather than only vertices. Contributions toward a proof may introduce construction and comparison lemmas, but none is asserted as an additional theorem item in this reviewed package.

Selected references

• Branko Grünbaum, Convex Polytopes, 2nd ed., Springer, 2003, §4.9, unnumbered Joswig–Ziegler existence theorem, printed p. 69b / PDF p. 95 of the supplied source.pdf.
• Michael Joswig and Günter M. Ziegler, “Neighborly cubical polytopes,” 2000, arXiv:math/9812033. This is corroboration for the construction; the mission retains Grünbaum's stated parameter range.

Motivation

A polytope may be described by its vertices or by its facets. These descriptions can differ sharply in size even when every vertex has only binary coordinates. Grünbaum's account of 0/1-polytopes in §4.9 records a result of Bárány and Pór: the maximal number of facets grows superexponentially with dimension. The result is an existence statement about the geometry of binary coordinate sets. The source describes random polytopes as witnesses, without specifying a probability distribution as part of the theorem.

Setting

Fix a dimension $d$. A $d$-polytope here is a nonempty convex hull of finitely many points in $\mathbb R^d$ with full affine span. A 0/1-polytope is the convex hull of a subset of $\{0,1\}^d$. Both properties are required of the witness. A facet is a nonempty exposed face of affine dimension $d-1$. The count $f_{d-1}(P)$ uses the book's convention that the empty face has dimension $-1$ and is excluded from natural-indexed face counts. This representation follows Grünbaum §§2.4 and 3.1 for faces and full-dimensional polytopes, and §4.9 for the binary coordinate family.

Formalization target

The single source obligation is the unnumbered Bárány–Pór assertion quoted by Grünbaum in §4.9, printed p. 69a (PDF p. 94). In mathematical notation, the statement is

$$\exists c>1\;\exists D\geq 2\;\forall d\geq D\;\exists P\subseteq\mathbb R^d:\quad P\text{ is a full-dimensional 0/1-polytope}\quad\text{and}\quad c^{d\log d}<f_{d-1}(P).$$

The constant $c$ and threshold $D$ are chosen before $d$; the witness $P$ may depend on $d$. The logarithm in Lean is natural logarithm. Changing a fixed logarithm base rescales the existential constant. The result is asymptotic: it does not assert the inequality in every small dimension. The threshold $D\geq2$ also keeps the natural-number expression $d-1$ in the facet dimension away from underflow.

The goal item Grunbaum2003.barany_por_binary_facet_growth carries this entire obligation. Its body is sorry, so the package presents a compiled statement, not a machine-checked proof. There are no separate source lemmas in this mission and no milestones to assert beyond the goal.

Significance

The theorem shows that binary vertex coordinates do not impose a merely exponential ceiling on the number of facets. It gives a family of full-dimensional binary polytopes whose facet counts eventually exceed an expression of the form $c^{d\log d}$ for one fixed $c>1$. A formal proof would establish that family in the chosen polytope and face-count representation. The present statement makes the quantifier order, full-dimensionality, binary-coordinate restriction, and strict facet inequality explicit for such a proof.

Difficulty

The existence of many binary vertices alone does not certify many facets: one must establish distinct supporting faces of codimension one. The source attributes the strong lower bound to a random construction. A proof must connect that construction to the geometric facet count while keeping one constant valid for every sufficiently large dimension. The mission statement leaves the construction method to the proof, as the quoted book assertion supplies no probability-space parameters or probability bound.

Formalization scope

Lean represents a point of $\mathbb R^d$ by Fin d → ℝ and a polytope by a set of such points. IsDPolytope requires a finite nonempty convex-hull presentation and full affine span. IsZeroOnePolytope requires a convex-hull presentation whose generators have every coordinate equal to zero or one. faceCount P k uses the finite cardinality of nonempty exposed faces of affine dimension $k$; for the full-dimensional witness, faceCount P (d - 1) is the facet count. No face-finiteness, simplicity, or probabilistic assumption is added to the theorem.

The package uses these three expression-essential definitions and the Mathlib real-power and logarithm notation. IsDPolytope and faceCount match the definitions already staged for other missions in this textbook series. A proof may reuse geometric lemmas or supply a new formal version of the Bárány–Pór construction, provided it proves the stated inequality for the original full-dimensional binary family.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §§2.4, 3.1, 4.9, printed pp. 17, 31, 69a (supplied source.pdf, PDF pp. 35, 51, 94).
• Imre Bárány and Attila Pór, “On 0–1 Polytopes with Many Facets,” Advances in Mathematics 161 (2001), 209–228, Theorem 1.1, p. 210. https://www.renyi.hu/~barany/cikkek/86.pdf

Motivation

The cosmological constant $\Lambda$ entered physics in 1917, when Einstein added a term $\Lambda g_{\mu\nu}$ to his field equations in order to allow a spatially homogeneous universe that neither expands nor contracts (Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, 1917). The resulting Einstein static universe is the unique balance in which the attraction of pressureless matter, the repulsion carried by $\Lambda$, and a positive spatial curvature cancel exactly. Two facts about that balance shaped the next century of cosmology:

1. it is possible only for one specific relation between $\Lambda$, the matter density and the curvature, so the static model is fine-tuned by construction;
2. it is unstable: an arbitrarily small increase of the scale factor grows, and an arbitrarily small decrease collapses.

After Hubble's 1929 observations Einstein dropped the term; it returned in 1998, when the supernova measurements of the Supernova Cosmology Project and the High-$z$ Supernova Search Team required $\Lambda>0$. Interpreting $\Lambda$ as a vacuum energy density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ with equation of state $w=-1$ then produced the cosmological constant problem: the measured value, about $10^{-52}\,\mathrm{m}^{-2}$, is roughly $10^{-122}$ in Planck units, tens of orders of magnitude below the scale that effective quantum field theory suggests (Wikipedia, Cosmological constant problem).

This mission formalizes the classical ordinary-differential-equation content of that story: the static solution, its uniqueness, its instability, the vacuum-energy reading of $\Lambda$, the density-parameter bookkeeping, and the numerical size of the discrepancy.

Setting

A homogeneous isotropic universe is described by a positive scale factor $a:I\to\mathbb{R}$ on a set of times $I\subseteq\mathbb{R}$. Matter is pressureless dust, whose density dilutes with volume,

$$\rho(a)=\rho_0\left(\frac{a_0}{a}\right)^{3},$$

where $\rho_0>0$ and $a_0>0$ are reference values. Units are geometrized, $c=1$, so $\Lambda$ has dimension (length)$^{-2}$; $G>0$ is Newton's constant and $k\in\mathbb{R}$ the curvature constant.

The dynamics are the two Friedmann equations. The first Friedmann equation is the constraint

$$\dot a(t)^2=\frac{8\pi G}{3}\,\rho\big(a(t)\big)\,a(t)^2-k+\frac{\Lambda}{3}a(t)^2 ,\qquad t\in I,$$

and the acceleration equation for dust is

$$\ddot a(t)=F\big(a(t)\big),\qquad F(x):=-\frac{4\pi G}{3}\,\rho(x)\,x+\frac{\Lambda}{3}x=-\frac{4\pi G}{3}\frac{\rho_0a_0^3}{x^{2}}+\frac{\Lambda}{3}x .$$

The Hubble parameter is $H=\dot a/a$, the critical density is $\rho_c=3H^2/(8\pi G)$, and the density parameters are

$$\Omega_m=\frac{\rho}{\rho_c},\qquad \Omega_\Lambda=\frac{\Lambda}{3H^2},\qquad \Omega_k=-\frac{k}{a^2H^2}.$$

Formalization targets

Goal — the static universe exists for exactly one balance, and it is unstable

For $G,\rho_0,a_0,a_E>0$, the constant function $a\equiv a_E$ satisfies both Friedmann equations if and only if

$$\Lambda=4\pi G\,\rho(a_E)\qquad\text{and}\qquad k=\Lambda a_E^{2},$$

in which case $\Lambda>0$, $F(a_E)=0$, $F'(a_E)=\Lambda>0$, and the equilibrium is unstable in the following exact sense: every solution of $\ddot a=F(a)$ on $[0,\infty)$ with $a(0)>a_E$ and $\dot a(0)\ge 0$ is strictly increasing and satisfies $a(t)\to\infty$; and every positive solution on $[0,T]$ with $a(0)<a_E$ and $\dot a(0)\le 0$ is strictly decreasing.

Supporting targets

$\Lambda$ is exactly a perfect fluid of constant density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ and pressure $p_{\text{vac}}=-\rho_{\text{vac}}$; the density parameters satisfy $\Omega_m+\Omega_k+\Omega_\Lambda=1$; the acceleration equation is a consequence of the first Friedmann equation along a solution with $\dot a\ne0$; and the observed $\Lambda$ is smaller than $10^{-120}$ in Planck units.

Significance

The static solution is the historical origin of $\Lambda$, and its instability is the reason the static model was never a viable cosmology even before the expansion was observed: the balance point is a local maximum of the effective potential, not a minimum, so the equilibrium cannot be maintained. The same function $F$ and the same linearization $\ddot\delta=\Lambda\,\delta$ govern the late-time behaviour of the standard $\Lambda$CDM model, where the growing mode becomes the de Sitter expansion $e^{\sqrt{\Lambda/3}\,t}$.

What the mission produces on top of the textbook statements: a machine-checked ODE treatment of a dust-plus-$\Lambda$ cosmology that does not stop at the linearized equation. The classical physics argument computes $F'(a_E)=\Lambda$ and calls the equilibrium unstable; the formal statements here ask for the nonlinear conclusion — monotone escape to infinity on one side and strict collapse on the other — which is what "unstable" has to mean for the exact equations. Mathlib contains neither the Friedmann equations nor a general instability criterion for second-order autonomous scalar ODEs, so both have to be built here.

Difficulty

The linearized step is routine calculus. The nonlinear instability is not: from $\ddot a=F(a)$ with $F(a_E)=0$ and $F$ strictly increasing on $(0,\infty)$, one must run a bootstrapping argument in which the sign of $\ddot a$ controls $\dot a$, which in turn controls whether $a$ stays in the region where the sign of $\ddot a$ was known. The obvious approach — solve the ODE explicitly — is not available: the dust-plus-$\Lambda$ equation with the static value of $k$ has no elementary closed-form solution through the static point, and the first Friedmann equation, which is the conserved energy of the second, degenerates exactly at $a=a_E$, where $\dot a=0$. Divergence $a(t)\to\infty$ additionally requires ruling out that $\dot a$ stalls, i.e. a quantitative lower bound on $\dot a$ once the solution has left a neighbourhood of $a_E$.

Formalization scope

Everything is stated for real-valued functions $a:\mathbb{R}\to\mathbb{R}$ of a real time variable; derivatives are the usual derivative of a real function, and each equation is asserted pointwise on an explicit set of times ($\mathbb{R}$, $[0,\infty)$, $[0,T]$, or a general open set), never globally by fiat. Dust density, the Friedmann equations, the acceleration function $F$, the Hubble parameter, the critical density and the three density parameters are all fixed in one definition file shared by every statement, so all items commit to the same conventions: $c=1$, curvature entering as $-k$ in the equation for $\dot a^2$, and $\rho_0,a_0$ as fixed reference constants rather than the value of the density at a particular time.

Two trivializing readings are ruled out explicitly. First, the contracting-side statement is posed on a bounded interval $[0,T]$ with positivity of $a$ assumed there, because a collapsing solution reaches $a=0$ in finite time; posing it on $[0,\infty)$ would make its hypotheses unsatisfiable and the statement vacuous. Second, the escape statement asks for $a(t)\to\infty$, not merely $\dot a\ge0$, so it cannot be satisfied by a solution that converges to a finite limit.

Useful contributions beyond the listed items: a reusable instability criterion for $\ddot x=F(x)$ at a zero of $F$ with $F'>0$, and the corresponding stability criterion, both of which are independent of cosmology.

Selected references

• Wikipedia, Cosmological constant. https://en.wikipedia.org/wiki/Cosmological_constant
• Wikipedia, Cosmological constant problem. https://en.wikipedia.org/wiki/Cosmological_constant_problem
• A. Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 1917.
• S. Weinberg, The cosmological constant problem, Reviews of Modern Physics 61 (1989) 1. https://doi.org/10.1103/RevModPhys.61.1
• J. Martin, Everything you always wanted to know about the cosmological constant problem (but were afraid to ask), Comptes Rendus Physique 13 (2012) 566. https://doi.org/10.1016/j.crhy.2012.04.008

Motivation

Quantum electrodynamics (QED) is the relativistic quantum field theory of electrodynamics: it describes how light and charged matter interact, and it is the most precisely tested theory in physics, reproducing quantities such as the anomalous magnetic moment of the electron and the Lamb shift of hydrogen to many digits. Its modern covariant formulation was developed by Tomonaga, Schwinger and Feynman, with Dyson showing the equivalence of the operator and diagrammatic approaches.

Every one of those computations starts from a single classical object: the QED action, a functional of a Dirac spinor field and an electromagnetic four-potential on Minkowski space. Perturbation theory, Feynman rules, renormalization and the S-matrix are all built on top of the classical Lagrangian and the structural facts about it — the Clifford algebra of the Dirac matrices, the $U(1)$ gauge symmetry, the conserved Noether current, and the Euler–Lagrange field equations. This mission formalizes exactly that classical layer, in the notation of the "Mathematical formulation" section of the Wikipedia article on quantum electrodynamics.

Nothing quantized is attempted here: no Fock space, no Dyson series, no renormalization. Those require a separate infrastructure and, in the interacting case, are not covered by any complete rigorous construction in four spacetime dimensions. What is formalizable today, and what this mission asks for, is the classical field theory that the quantum theory quantizes.

Setting

Spacetime is $\mathbb{R}^4$ with coordinates $x = (x^0, x^1, x^2, x^3)$ and the Minkowski metric $\eta$ of signature $(+,-,-,-)$: $\eta_{00} = 1$, $\eta_{11} = \eta_{22} = \eta_{33} = -1$, and $\eta_{\mu\nu} = 0$ for $\mu \ne \nu$. Since $\eta$ is its own inverse, the same array serves as the contravariant metric $\eta^{\mu\nu}$ used to raise indices. The symbol $\partial_\mu$ denotes the partial derivative in the $\mu$-th coordinate direction, and $\Box = \eta^{\mu\nu}\partial_\mu\partial_\nu$ is the wave operator.

The Dirac matrices are four complex $4\times4$ matrices $\gamma^0,\dots,\gamma^3$ subject to the Clifford relation

$$\gamma^\mu\gamma^\nu + \gamma^\nu\gamma^\mu = 2\eta^{\mu\nu} I_4$$

together with the hermiticity relation $(\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0$, which makes $\gamma^0$ hermitian and $\gamma^1,\gamma^2,\gamma^3$ anti-hermitian. The standard Dirac basis is one concrete solution of these relations.

A spinor field is a map $\psi : \mathbb{R}^4 \to \mathbb{C}^4$; its Dirac adjoint is $\bar\psi = \psi^\dagger\gamma^0$, and for a $4\times4$ matrix $M$ the pairing $\bar\psi M \chi$ is the complex number $\sum_{i,j}\overline{\psi_i}\,(\gamma^0 M)_{ij}\,\chi_j$. A gauge field is a map $A : \mathbb{R}^4 \to \mathbb{R}^4$ whose value $A_\mu(x)$ is the covariant component of the electromagnetic four-potential. From it one forms the field tensor (the curvature of the gauge connection)

$$F_{\mu\nu} = \partial_\mu A_\nu - \partial_\nu A_\mu, \qquad F^{\mu\nu} = \eta^{\mu\alpha}\eta^{\nu\beta}F_{\alpha\beta},$$

and, for a coupling constant $e$, the gauge covariant derivative $D_\mu\psi = \partial_\mu\psi + ieA_\mu\psi$. The Dirac current is $J^\mu = \bar\psi\gamma^\mu\psi$.

With $m$ the mass of the spinor field, the QED Lagrangian density is

$$\mathcal{L} = \bar\psi\,(i\gamma^\mu D_\mu - m)\,\psi - \tfrac{1}{4}F_{\mu\nu}F^{\mu\nu}.$$

Its Euler–Lagrange equations are the Dirac equation $(i\gamma^\mu D_\mu - m)\psi = 0$ and the Maxwell equation $\partial_\mu F^{\mu\nu} = e J^\nu$. The Lorenz gauge condition is $\eta^{\mu\nu}\partial_\mu A_\nu = 0$.

Formalization targets

Goal

For a coupled solution $(\psi, A)$ of the QED field equations in the Lorenz gauge, the four-potential obeys an inhomogeneous wave equation whose source is a conserved current:

$$\Box A^\nu = e\,J^\nu \qquad\text{and}\qquad \partial_\nu J^\nu = 0 .$$

This is the "QED version of the classical Maxwell equations in the Lorenz gauge" of the source, together with the conservation law that makes the source of that wave equation consistent. It fixes no gauge beyond Lorenz, no representation of the Dirac matrices, and no sign or normalization beyond those of the stated Lagrangian.

Supporting targets

$$\gamma^\mu\gamma^\nu+\gamma^\nu\gamma^\mu = 2\eta^{\mu\nu}I_4,\qquad (\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0 \quad\text{for the Dirac basis;}$$ $$\partial_\lambda F_{\mu\nu} + \partial_\mu F_{\nu\lambda} + \partial_\nu F_{\lambda\mu} = 0;$$ $$F_{\mu\nu}[A + d\chi] = F_{\mu\nu}[A],\qquad D_\mu\big(e^{-ie\chi}\psi\big)\big[A + d\chi\big] = e^{-ie\chi} D_\mu\psi[A],\qquad \mathcal{L}\big[e^{-ie\chi}\psi, A + d\chi\big] = \mathcal{L}[\psi, A];$$ $$\bar\psi\gamma^\mu\psi \in \mathbb{R},\qquad \partial_\mu(\bar\psi\gamma^\mu\psi) = 0 \ \text{ for solutions of the Dirac equation},\qquad \Box A^\nu = eJ^\nu \ \text{ in Lorenz gauge.}$$

Significance

The classical layer is what every later construction quantizes. The Clifford relation is what makes the Dirac operator a square root of the wave operator; the $U(1)$ invariance of $\mathcal{L}$ is what forces the coupling to be through $D_\mu$ and what makes the current conserved by Noether's theorem; conservation of $J^\mu$ is the consistency condition without which $\partial_\mu F^{\mu\nu} = eJ^\nu$ has no solutions at all, since the left side is annihilated by $\partial_\nu$ identically. The Lorenz-gauge wave equation is the form in which the photon propagator is read off.

Formalizing it adds a reusable, machine-checked Minkowski-space field-theory layer: a metric with index raising, coordinate partial derivatives on $\mathbb{R}^4$ with a wave operator, an abstract Dirac representation together with a concrete basis satisfying it, the field tensor, the covariant derivative, the Dirac current and the QED Lagrangian. Mathlib has Clifford algebras and Fréchet calculus, but not this concrete apparatus. None of the statements in this mission is currently known to have a machine-checked proof; all are standard textbook results with well-understood proofs, so the work is formalization rather than discovery.

Difficulty

The arguments are elementary on paper and awkward in Lean for three separate reasons.

First, all index manipulation is explicit: raising an index is a sum over $\mathrm{Fin}\ 4$, and every "obvious" rearrangement of $\sum_{\mu\alpha\beta}\eta^{\mu\alpha}\eta^{\nu\beta}\partial_\mu\partial_\alpha A_\beta$ has to be done by hand with Finset.sum lemmas.

Second, differentiation is Fréchet differentiation in disguise: $\partial_\mu f$ is the derivative of $f$ evaluated at a basis vector, so the product rule, the sum rule and the symmetry of second derivatives each require the corresponding differentiability side conditions. The naive move of treating $\partial_\mu$ as a formal symbol that commutes with everything fails: without a $C^2$ hypothesis, $\partial_\mu\partial_\nu \ne \partial_\nu\partial_\mu$, and without differentiability the derivative takes the junk value $0$, so an identity that "obviously" holds termwise may hold only under the stated smoothness assumption.

Third, the current conservation law is not a pure computation: it needs the Dirac equation, the hermiticity relation $(\gamma^\mu)^\dagger = \gamma^0\gamma^\mu\gamma^0$, and the reality of $m$, $e$ and $A_\mu$, in the precise combination that cancels the terms containing $A_\mu$ between $\partial_\mu\bar\psi$ and $\partial_\mu\psi$. Any attempt to prove it from smoothness alone, without the equation of motion, cannot work — the current of an arbitrary smooth spinor field is not conserved.

Formalization scope

Spacetime is Fin 4 → ℝ, a gauge field is Spacetime → Fin 4 → ℝ with lower index, a spinor field is Spacetime → Fin 4 → ℂ, and the Dirac matrices are Fin 4 → Matrix (Fin 4) (Fin 4) ℂ. Sums over indices are Finset.sum over Fin 4. Partial derivatives are fderiv ℝ f x (Pi.single μ 1), which is $0$ when $f$ is not differentiable at $x$; smoothness hypotheses are stated as ContDiff ℝ 1 or ContDiff ℝ 2 exactly where they are used. Complex conjugation is starRingEnd ℂ, matrix adjoint is Matrix.conjTranspose, and the coupling constant $e$, the mass $m$ and the gauge parameter $\chi$ are real, with no positivity or nonvanishing assumption on $e$ or $m$.

Conventions fixed once and shared by every statement: signature $(+,-,-,-)$; $D_\mu = \partial_\mu + ieA_\mu$; $F_{\mu\nu} = \partial_\mu A_\nu - \partial_\nu A_\mu$; $J^\mu = \bar\psi\gamma^\mu\psi$ taken as a real number via its real part, with the reality of the underlying complex pairing stated as a separate target; the Maxwell equation carries the coupling on the right-hand side as $\partial_\mu F^{\mu\nu} = eJ^\nu$; and the Dirac equation is $\sum_\mu i\gamma^\mu D_\mu\psi = m\psi$.

The statements are not vacuous: $\psi = 0$, $A = 0$ satisfies all field equations, plane-wave solutions of the free Dirac equation satisfy the Dirac hypothesis with $A = 0$, and the concrete Dirac basis witnesses the abstract representation hypothesis, so no hypothesis in the mission is unsatisfiable. The goal is not trivially true: it asserts a pointwise identity between second derivatives of $A$ and a quadratic expression in $\psi$, not an implication between definitionally equal objects.

A complete development needs Mathlib's fderiv calculus (product rule, symmetry of the second derivative via IsSymmSndFDerivAt), Finset.sum manipulation, Matrix arithmetic over ℂ, and Complex.exp. The Minkowski-space layer — metric, partial derivatives, wave operator, field tensor, Dirac representation — is reusable for any later mission on classical field theory or on the quantized theory. Contributions of further structural results in this notation (energy–momentum tensor, plane-wave solutions, the free-field propagator) are welcome as follow-up problems.

Selected references

• Wikipedia, Quantum electrodynamics, section "Mathematical formulation". https://en.wikipedia.org/wiki/Quantum_electrodynamics
• C. Itzykson and J.-B. Zuber, Quantum Field Theory, McGraw-Hill, 1980.
• M. E. Peskin and D. V. Schroeder, An Introduction to Quantum Field Theory, Addison-Wesley, 1995.
• R. P. Feynman, QED: The Strange Theory of Light and Matter, Princeton University Press, 1985.

Motivation

The ΛCDM model — "Lambda cold dark matter" — is the standard cosmological model: a spatially homogeneous and isotropic universe governed by general relativity, whose energy content is dominated today by cold dark matter and by a cosmological constant $\Lambda$ acting as dark energy. It is the framework in which the cosmic microwave background, the large-scale distribution of galaxies, the primordial light-element abundances, and the observed accelerating expansion are fitted simultaneously with a handful of parameters.

Inside this model, almost everything quantitative requires numerical integration of the Friedmann equations. There is one striking exception: for a spatially flat universe containing only pressureless matter and a positive cosmological constant, and with radiation neglected, the expansion history has a closed form in elementary functions. That closed form is where the textbook statements "the universe is about $13.8$ billion years old" and "the expansion switched from decelerating to accelerating at redshift $z \approx 0.6$" actually come from. This mission formalizes that closed form and the two consequences just named.

Setting

Write $a(t)$ for the dimensionless scale factor of a homogeneous isotropic universe, normalized so that $a = 1$ at the present epoch, and $H(t) = \dot a(t)/a(t)$ for the Hubble parameter; $H_0 > 0$ denotes its present-day value. The energy content is described by present-day density parameters $\Omega_i$, the ratios of each species' density to the critical density $\rho_c = 3H_0^2/(8\pi G)$. This mission works with the minimal, radiation-free, spatially flat case: a matter parameter $\Omega_m > 0$ and a dark-energy parameter $\Omega_\Lambda > 0$ with

$$\Omega_m + \Omega_\Lambda = 1 .$$

Matter dilutes as $a^{-3}$ and the cosmological constant does not dilute at all, so the first Friedmann equation for this content reads

$$\left(\frac{\dot a}{a}\right)^{2} \;=\; H_0^{2}\left(\frac{\Omega_m}{a^{3}} + \Omega_\Lambda\right).$$

The candidate closed-form solution, with the big bang placed at $t = 0$, is

$$a(t) \;=\; \left(\frac{\Omega_m}{\Omega_\Lambda}\right)^{1/3}\, \sinh^{2/3}\!\left(\tfrac{3}{2}\sqrt{\Omega_\Lambda}\,H_0\,t\right), \qquad t > 0,$$

and the time at which it reaches $a = 1$ — the predicted age of the universe — is

$$t_0 \;=\; \frac{2}{3H_0\sqrt{\Omega_\Lambda}}\;\operatorname{arsinh}\sqrt{\frac{\Omega_\Lambda}{\Omega_m}}.$$

All quantities are real; $\sinh^{2/3}$ is the real power $x \mapsto x^{2/3}$ applied to $\sinh$, which is positive for $t > 0$.

Target

The goal theorem asserts that the displayed $a(t)$ is a positive solution of the flat matter-plus-$\Lambda$ Friedmann equation on $t > 0$, normalized by $a(t_0) = 1$ at the age $t_0 > 0$ given above:

$$0 < a(t), \qquad \left(\frac{\dot a(t)}{a(t)}\right)^{2} = H_0^{2}\left(\frac{\Omega_m}{a(t)^{3}} + \Omega_\Lambda\right) \quad (t > 0), \qquad 0 < t_0, \qquad a(t_0) = 1 .$$

The milestones build to this and then go beyond it, in increasing strength: the derivative $\dot a = a H_0\sqrt{\Omega_\Lambda}\coth\theta$ with $\theta = \tfrac32\sqrt{\Omega_\Lambda}H_0 t$; the Friedmann equation itself; the normalization $a(t_0) = 1$; the equivalent logarithmic age formula

$$t_0 = \frac{2}{3H_0\sqrt{\Omega_\Lambda}}\,\log\frac{1+\sqrt{\Omega_\Lambda}}{\sqrt{\Omega_m}};$$

the deceleration-to-acceleration transition, $\ddot a(t) = 0$ exactly when $a(t)^3 = \Omega_m/(2\Omega_\Lambda)$, together with the sign criterion $\ddot a(t) > 0 \iff \Omega_m < 2\Omega_\Lambda a(t)^3$; the qualitative picture that $a$ is strictly increasing on $(0,\infty)$ and tends to $0$ as $t \downarrow 0$; and finally the statement that the closed form, together with the density $\rho = \rho_c(\Omega_m a^{-3} + \Omega_\Lambda)$ and the pressure $p = -\rho_c\Omega_\Lambda$, satisfies both Friedmann equations, i.e. assembles into an FRW universe in the sense of the platform's existing FRWUniverse definition.

Significance

The result. The closed form turns cosmological parameter statements into arithmetic. With $\Omega_m \approx 0.315$, $\Omega_\Lambda \approx 0.685$ and $H_0 \approx 67.4\ \mathrm{km\,s^{-1}Mpc^{-1}}$ it yields the standard age of roughly $13.8$ billion years, and the transition condition $a^3 = \Omega_m/(2\Omega_\Lambda)$ gives $1+z = (2\Omega_\Lambda/\Omega_m)^{1/3} \approx 1.6$, i.e. $z \approx 0.6$. Both numbers are quoted constantly; here they are consequences of a theorem rather than of a numerical integration. The transition result is also the precise sense in which a positive $\Lambda$ is what makes the late-time expansion accelerate.

Formalizing it. The mathematics is classical and the derivation is standard in cosmology texts; nothing here is an open question. What the mission produces is a machine-checked account: a reusable parameter bundle for the flat ΛCDM model, a verified closed-form solution of a nonlinear ODE, verified transcendental identities for the age, and a bridge to the platform's existing FRW-cosmology development, so that later work on distances, horizons, or the radiation-inclusive model can build on published statements instead of restating them.

Difficulty

The obstruction is not conceptual but analytic. The scale factor is a real power $x^{2/3}$ of $\sinh$, so it is not differentiable by the polynomial-power rules: every derivative step goes through the real rpow API, needs positivity of $\sinh\theta$ on $t > 0$, and produces exponents that must be recombined by hand ($a^3$ collapses to $(\Omega_m/\Omega_\Lambda)\sinh^2\theta$ only after such a step). The Friedmann identity itself then rests on $\coth^2 = 1 + \operatorname{csch}^2$, which must be applied where $\sinh\theta \neq 0$. The age milestones require the explicit value of $\operatorname{arsinh}$ as a logarithm together with the flatness relation $\Omega_m = 1 - \Omega_\Lambda$. The second-derivative milestones require differentiating the first-derivative formula again and tracking the sign of $\sinh^2\theta - \tfrac13\cosh^2\theta$; the naive route of computing deriv (deriv ·) symbolically without first establishing a HasDerivAt statement on a neighbourhood is the main trap.

Formalization scope

Parameters are bundled in a structure carrying $H_0 > 0$, $\Omega_m > 0$, $\Omega_\Lambda > 0$ and $\Omega_m + \Omega_\Lambda = 1$; radiation and curvature are absent by construction, and dark energy is a true cosmological constant ($w = -1$), not a general equation of state. Time is a real variable with the big bang at $t = 0$, and every statement about the solution is restricted to $t > 0$, where $\sinh\theta > 0$; outside that range the real power of a non-positive base is a junk value and nothing is claimed. Powers $x^{1/3}$, $x^{2/3}$ are real powers, while $a^3$ is a natural-number power. Derivatives are Mathlib's deriv/HasDerivAt; the Friedmann equation is stated in the source's ratio form $(\dot a/a)^2 = H_0^2(\Omega_m a^{-3} + \Omega_\Lambda)$ rather than a cleared-denominator variant, and $a(t) > 0$ is part of the goal, so the statement cannot be satisfied by a degenerate $a \equiv 0$. The hypotheses $\Omega_m, \Omega_\Lambda > 0$ with $\Omega_m + \Omega_\Lambda = 1$ are jointly satisfiable, so no statement is vacuous.

The final milestone reuses the published FRWUniverse structure (an FRW universe with Newton's constant $G$, curvature $K$, time domain $I$, scale factor and its two derivatives, density, its derivative, and pressure, subject to both Friedmann equations pointwise) rather than introducing a competing model; contributions that connect these statements to distance–redshift relations, or that relax flatness or restore radiation, are welcome.

Selected references

• Wikipedia, Lambda-CDM model, https://en.wikipedia.org/wiki/Lambda-CDM_model — section "Cosmic expansion history" (the Friedmann equation in density parameters, the closed-form solution, the age, and the acceleration transition).
• Planck Collaboration, Planck 2018 results. VI. Cosmological parameters, Astronomy & Astrophysics 641 (2020) A6, https://doi.org/10.1051/0004-6361/201833910.

Motivation

Convex hulls are often defined using arbitrary finite convex combinations. In finite dimensional geometry, Carathéodory's theorem gives a uniform bound on how many points are needed to represent any one point of the hull. This is the finite representation result stated in Branko Grünbaum's Convex Polytopes, second edition (2003), §2.3, Theorem 2.3.5, printed page 15 (PDF page 33). It matters when one wants a description whose number of witnesses depends on the ambient dimension rather than on the size of the generating set. The mission concerns that exact textbook statement for an arbitrary subset of real coordinate space.

Setting

Fix a natural number $d$. The ambient space $\mathbb R^d$ is represented in Lean as Fin d → ℝ: a point assigns a real coordinate to each of the $d$ indices. Let $A$ be any set of such points. Its convex hull, written $\operatorname{conv}(A)$ in the book and convexHull ℝ A in Lean, is the smallest convex set containing $A$. A convex combination is a finite weighted sum of points of $A$ whose real weights are nonnegative and total one. No finiteness, closedness, boundedness, convexity, or nonemptiness assumption is imposed on $A$.

The witnesses in the target are indexed by Fin (d + 1), which has exactly $d+1$ elements, corresponding to the book's indices $0,\ldots,d$. Repeated points and zero weights are permitted. They allow a representation that uses fewer than $d+1$ distinct points to be written with the same fixed index type.

Formalization targets

Theorem 2.3.5: Carathéodory's finite convex representation

For every $x\in\operatorname{conv}(A)$, find points $x_0,\ldots,x_d\in A$ and real numbers $\alpha_0,\ldots,\alpha_d\geq 0$ such that

$$\sum_{i=0}^{d}\alpha_i=1, \qquad x=\sum_{i=0}^{d}\alpha_i x_i.$$

The Lean goal is Grunbaum2003.caratheodory_convex_representation. It quantifies over every natural dimension, every set $A$ in that real coordinate space, and every point $x$ of its convex hull. The existential witnesses and all four required clauses are part of one theorem. This is the sole goal and sole source obligation in the frozen mission grouping; there is no separate supporting milestone to attest.

Significance

The result turns membership in a convex hull into a representation with a dimension controlled number of generators. The bound is independent of the cardinality of $A$, which may even be infinite. In the textbook's chapter, this is the finite representation model from which other discussions of convex sets can proceed. It does not itself claim a separation theorem, a compactness statement about closures, or a representation of unbounded closed convex sets using recession directions; those are distinct statements with different hypotheses and conclusions.

A formal proof of this statement would establish the textbook result in Lean for the exact source quantifiers and index bound. The present proposal contains a statement with sorry, not a proof. The original statement compiled in the local Lean workspace and passed source aware moderation; successful compilation verifies that its expression is well formed but does not settle the theorem. The open work in this mission is to replace the placeholder with a machine checked proof of the stated result.

Difficulty

The definition of convexHull ℝ A establishes membership by finite convex combinations, but such a combination can have arbitrarily many terms. The target asks for a bound of $d+1$ terms, uniformly for every point and every generating set. Merely unfolding convex hull membership therefore does not deliver the claimed index bound. The witness must also keep membership in $A$, nonnegative coefficients, normalization, and the exact vector equality simultaneously. These constraints explain why a general finite combination cannot simply be relabelled as a Fin (d + 1) family.

Formalization scope

The representation uses real scalars and the coordinate space Fin d → ℝ. The Lean statement uses convexHull ℝ A for the hull, Fin (d + 1) for both point and weight families, and a finite sum for normalization and the represented point. d = 0 is included. When $A$ is empty, the hypothesis $x\in\operatorname{conv}(A)$ has no instance; no artificial nonemptiness premise is added. There is no extra affine independence or strict positivity condition on the witnesses.

The only expression dependencies are Mathlib's convex hull, real numbers, finite indexing, finite sums, and scalar multiplication. The proposal does not introduce a duplicate convex hull definition or a book specific representation predicate. A complete proof may use Mathlib's existing convexity library, but the theorem statement and its source obligations remain fixed. Contributions that prove the exact quantified statement are within scope; variants with a restricted $A$, a changed ambient space, or fewer clauses would answer a different question.

Selected references

• Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §2.3, Theorem 2.3.5, printed p. 15, PDF p. 33. Publisher record. Source copy: source.pdf in the book record; SHA-256 070befaa8c47f043ef9da1df0705910480eb692f044d1843c9f048f3e61fecac.

Motivation

A system of natural units fixes the size of the base units not by reference to an artefact or a historical convention, but by declaring that certain universal constants have numerical value $1$. The oldest and most widely used such system is the one Max Planck proposed in 1899, at the end of Über irreversible Strahlungsvorgänge, built from the speed of light $c$, the gravitational constant $G$, the quantum of action (today $\hbar$) and the Boltzmann constant $k_B$. Planck's claim for these units was that they are "independent of special bodies or substances" and therefore retain their meaning "for all times and for all civilizations, including extraterrestrial and non-human ones".

The claim that gives the system its force is a uniqueness claim: there is one and only one choice of base length, mass, time and temperature for which all four constants read $1$. Textbooks and reference works state the resulting expressions $l_P=\sqrt{\hbar G/c^3}$, $m_P=\sqrt{\hbar c/G}$, $t_P=\sqrt{\hbar G/c^5}$, $T_P=\sqrt{\hbar c^5/G}/k_B$ as the Planck units, but the accompanying argument is usually a dimensional-analysis sketch rather than a proof that the defining system of equations has exactly one positive solution. This mission formalizes the statement and its standard consequences.

Setting

Fix four positive real numbers $c$, $G$, $\hbar$, $k_B$ — the numerical values of the four constants in some reference system of units (SI, say).

A unit system is a quadruple $u=(L,M,T,\Theta)$ of positive reals: the size of the chosen unit of length, mass, time and temperature, measured in the reference system. Changing to $u$ divides every quantity by the appropriate product of $L,M,T,\Theta$. Concretely, a speed is divided by $L/T$, a quantity of dimension $L^3M^{-1}T^{-2}$ (the dimension of $G$) by $L^3/(MT^2)$, an action by $ML^2/T$, and a heat capacity by $ML^2/(T^2\Theta)$.

Say that $u$ normalizes $c,G,\hbar,k_B$ when each of the four constants has numerical value $1$ in $u$, i.e. when

$$\frac{L}{T}=c,\qquad \frac{L^3}{MT^2}=G,\qquad \frac{ML^2}{T}=\hbar,\qquad \frac{ML^2}{T^2\Theta}=k_B .$$

The Planck system is the quadruple

$$\Big(\sqrt{\tfrac{\hbar G}{c^3}},\ \sqrt{\tfrac{\hbar c}{G}},\ \sqrt{\tfrac{\hbar G}{c^5}},\ \tfrac{1}{k_B}\sqrt{\tfrac{\hbar c^5}{G}}\Big).$$

Formalization targets

Goal

$$\exists!\,(L,M,T,\Theta)\in(0,\infty)^4:\quad \frac{L}{T}=c,\ \ \frac{L^3}{MT^2}=G,\ \ \frac{ML^2}{T}=\hbar,\ \ \frac{ML^2}{T^2\Theta}=k_B,$$

together with the identification of that unique solution as the Planck system above. The statement is asserted for arbitrary positive $c,G,\hbar,k_B$, so it does not depend on the SI values of the constants, and it fixes nothing beyond positivity.

Supporting targets

The milestones record the standard relations among the Planck units: $l_P=c\,t_P$; the reduced Compton wavelength $\hbar/(m_Pc)$ of the Planck mass equals $l_P$; the Schwarzschild radius $2Gm_P/c^2$ of the Planck mass equals $2l_P$; the coherent derived units of Table 2 of the source (energy, momentum, force, density, acceleration, frequency) have the stated closed forms; Newton's law of gravitation takes the constant-free form $F'=m_1'm_2'/r'^2$ when every quantity is replaced by its ratio to the corresponding Planck unit; and normalizing $4\pi G$ in place of $G$ yields the rationalized Planck units.

Significance

The uniqueness statement is what licenses the everyday practice of "setting $c=G=\hbar=k_B=1$": it says that the convention determines the units completely, so that a dimensionless equation written in Planck units can be translated back into a dimensional one in exactly one way. It also makes precise the sense in which the Planck scale is defined rather than measured: the quantities $10^{-35}\,\mathrm{m}$, $10^{-43}\,\mathrm{s}$, $10^{-8}\,\mathrm{kg}$ are consequences of the SI values of four constants and of nothing else.

What formalization adds here is not a new theorem — the algebra is elementary and the result is classical — but a machine-checked statement of a claim that is normally left implicit, together with a reusable Lean model of "system of base units" and "constant normalized to $1$" in which variant conventions can be stated and compared. The rationalized-units milestone is included precisely to exercise that generality: it is the same theorem applied to $4\pi G$ instead of $G$, and it shows that the formalization does not secretly hard-code the Planck convention.

Difficulty

The obvious argument — "count dimensions, invert a $4\times4$ exponent matrix" — proves uniqueness of the exponents in a monomial ansatz $L=c^aG^b\hbar^d$, not uniqueness of the solution among all positive quadruples, which is what the claim asserts. The formal statement therefore has to be proved directly from the four equations: eliminate $M$ and $\Theta$, reduce to $L^5=G\hbar T^3$ with $T=L/c$, and cancel a positive factor $L^3$. The remaining friction is Lean-side rather than mathematical: the four defining equations are stated with division, so every step carries a non-vanishing side condition, and the closed forms are square roots, so equalities are proved by comparing squares of non-negative reals rather than by ring alone.

Formalization scope

The development is over ℝ. A unit system is a structure with four real fields, positivity is a separate predicate rather than a subtype, and "normalizes" is the conjunction of the four displayed equations as written with division — for a positive unit system this is equivalent to the product form, but the division form is what the statements use. All four constants are universally quantified positive reals; no SI numerals appear anywhere in the development, and the milestones about the derived units state closed forms (e.g. force $=c^4/G$, density $=c^5/(\hbar G^2)$) rather than decimal approximations.

Two trivialization risks are ruled out explicitly. The hypotheses are satisfiable — the Planck system itself is exhibited as a positive solution in the first milestone — so the uniqueness statement is not vacuous. And the goal is not merely "the Planck system normalizes the constants": it also asserts that every positive normalizing system equals it.

Infrastructure needed beyond Mathlib is minimal: Real.sqrt and its interaction with squaring and positivity. The unit-system model is reusable for other natural-unit conventions (Stoney units, reduced Planck units with $8\pi G=1$, Hartree atomic units), and contributions extending it in that direction are welcome.

Selected references

• Max Planck, Über irreversible Strahlungsvorgänge, Sitzungsberichte der Königlich Preußischen Akademie der Wissenschaften zu Berlin 5 (1899), 440–480; the base units appear on pp. 478–480. biodiversitylibrary.org
• K. A. Tomilin, Natural Systems of Units: To the Centenary Anniversary of the Planck System, Proceedings of the XXII Workshop on High Energy Physics and Field Theory (1999), 287–296. inspirehep.net
• C. W. Misner, K. S. Thorne, J. A. Wheeler, Gravitation, W. H. Freeman (1973), p. 1215.
• Planck units, Wikipedia (the source text this mission formalizes). en.wikipedia.org/wiki/Planck_units
• 2022 CODATA values for the Planck length, mass, time and temperature, NIST. physics.nist.gov