Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A convex set contains the segment joining any two of its points. For a bounded closed convex set in finite-dimensional real space, extreme points describe the set through convex combinations. An extreme point cannot lie strictly between two distinct points of the set. Allowing unbounded sets introduces a second ingredient: directions in which one can move indefinitely while remaining in the set.
This mission concerns that second ingredient and its interaction with extreme points. A closed convex set is line-free if it contains no entire straight line. It may nevertheless contain rays and be unbounded. Its characteristic cone consists of directions v for which x + t v stays in the set whenever x belongs to the set and t is nonnegative. For a nonempty closed convex set, checking one basepoint gives the same cone as checking every basepoint. Thus the cone records the directions of recession without singling out an origin inside the set.
The goal is Grünbaum’s Theorem 2.5.6:
for every line-free, closed convex set K in real d-dimensional space. The plus sign denotes Minkowski addition: all sums of one point from each set. The equation says that every point of K is a recession vector plus a finite convex combination of extreme points. Conversely, each such sum belongs to K. There is no topological closure around the convex hull in this equation.
A ray illustrates the two ingredients. Its endpoint is its only extreme point, while its characteristic cone supplies every nonnegative displacement along the ray. A singleton has only itself as an extreme point and has zero characteristic cone. A whole straight line shows why the line-free hypothesis matters: it has no extreme points and cannot be recovered from their convex hull by this formula.
The ambient dimension is arbitrary and finite; the set need not be full-dimensional or polyhedral. The characteristic cone is defined using all basepoints, so its value on the empty set is the whole ambient space. Since the empty set has no extreme points, its convex hull and the displayed Minkowski sum are empty, and the equation remains valid. This convention extends the formula without asserting that the book defines a characteristic cone at an absent basepoint.
The source is Branko Grünbaum, Convex Polytopes, second edition (2003), §2.5, Theorem 6, printed page 25 (PDF page 43). The characteristic cone and line-free condition appear on printed page 24 (PDF page 42); extreme points are defined in §2.4 on printed page 17 (PDF page 35). These definitions supply the vocabulary for the single representation goal.
A quantum computer manipulates superpositions of many degrees of freedom, and every gate it applies is imperfect. Before 1996 it was widely argued that this fragility is fatal: the accuracy demanded of each elementary operation appeared to grow with the length of the computation, so that arbitrarily long computations would require arbitrarily perfect hardware. The discovery of quantum error-correcting codes, of fault tolerant syndrome extraction, and of transversally encoded operations changed that picture, but the first fault tolerant schemes still required the error per operation to shrink as the computation grew.
Knill, Laflamme and Zurek, Resilient Quantum Computation: Error Models and Thresholds (arXiv:quant-ph/9702058), together with the independent work of Kitaev and of Aharonov and Ben-Or, removed that requirement: they exhibited a fixed threshold value such that any physical error rate below it permits arbitrarily accurate encoded computation, at an overhead that is only polylogarithmic in the length of the computation. Their paper is also the one that pushes past independent stochastic noise: its thresholds are proved for quasi-independent error models, which accommodate coherent over-rotation and weak residual couplings between neighbouring qubits.
This mission formalizes the quantitative engine of that paper: the concatenation recursion, the error-model bounds it is applied to, the threshold it produces, and the resulting overhead.
Fix a physical implementation in which each gate, state preparation and idle memory step carries an error location. A noisy network with error locations indexed by a finite set is described through an error expansion; each summand fails at a set of locations, and the model constrains how probable simultaneous failures are.
Write for the underlying probability measure and for the event that location has failed. Two models from Section I.B of the paper are used here.
The fault tolerant construction of Section I turns physical qubits into encoded qubits: each encoded gate is a transversal operation preceded by fault tolerant recovery networks built from the -qubit Steane code. The analysis of Section II declares an encoded gate failed according to an explicit combinatorial rule, and shows that a failure requires two failures among a set of minimal pairs of physical error locations. Consequently one level of encoding maps a failure parameter to .
Iterating this reduction is concatenation. Define the level- failure parameter by
written in the Lean development. Let bound the number of qubits and time steps at the level below that are consumed by one encoded gate, so that one computational gate at level costs physical resources.
For , , , and every gate count and target failure probability with , there exists a level with
The first clause is resilience: a computation of encoded gates can be made to fail with probability below any prescribed . The second is the cost: the overhead per computational gate is polylogarithmic in , with exponent . The threshold itself is the hypothesis ; no numerical value is hard-coded, so the statement survives any improvement of the paper's count and of the resulting bounds and .
The milestone list covers the closed form of the concatenation recursion and its threshold form ; convergence below threshold; the failure bounds and for a network under the two error models; the criterion under which ; and the overhead estimate .
The threshold theorem is the reason large-scale quantum computation is regarded as a physically meaningful goal rather than an idealization: it converts an engineering requirement that scales with the problem size into a fixed, size-independent accuracy target, and it fixes the currency — threshold value and overhead exponent — in which every later architecture is compared. The quasi-independent models matter separately: they show the conclusion does not depend on noise being stochastic, which is what rules out the objection that coherent over-rotations invalidate the stochastic analysis.
The paper's own argument is a physics-style derivation: a circuit-level construction, a combinatorial count of failure-inducing pairs of error locations, and a recursion. This mission formalizes the recursion, the probabilistic bounds and the resulting threshold and overhead statements. It does not formalize the circuit-level content — the -qubit code, the cat-state syndrome extraction networks, transversality, or the count itself; these enter the formal statements as the parameters and . No machine-checked proof of the full threshold theorem, in the sense of a verified fault tolerant circuit construction, is known to the author of this proposal; formalizing the quantitative layer is a prerequisite for one.
The obvious route to "errors vanish under concatenation" is to iterate the bound and observe the doubly exponential decay. That step is the easy half, and the milestone list makes it explicit. What the naive argument silently assumes is exactly what Section II must establish: that the level- failure events again obey a quasi-independent bound, with simultaneous encoded failures bounded by rather than merely each single failure bounded by . This is why the paper's failure declaration is defined backwards in time and demands disjoint pairs of contributing locations. A formalization that bounds only single-gate failure probabilities cannot close the induction.
The second difficulty is bookkeeping at the edges: the recursion is stated for a failure parameter that is a probability in one model and an operator strength in the other, and the overhead bound involves a real exponent and a ceiling, whose interaction with the degenerate cases and has to be handled rather than assumed away.
All parameters are real numbers: , and the gate count is a natural number cast to . levelError is defined by recursion on the level and is total, so it is meaningful for every real ; the threshold hypothesis appears explicitly as where it is needed.
The two error models are predicates on a measure on a measurable space, a Finset of error locations, and a family of failure events, with values in ENNReal; they quantify over all subsets of the location set, matching the paper's "at a given many error locations". The network failure bounds are stated for , the probability that some location fails.
The goal is not vacuous: the hypotheses , , , are simultaneously satisfiable (for instance , , , , ), and the conclusion asserts a strict inequality together with a quantitative overhead bound, so it cannot be discharged by a degenerate reading. Degenerate inputs are inside the statement rather than excluded: , and the case , are covered by the and must be handled.
A complete development needs only Mathlib's real analysis (Real.log, Real.logb, Real.rpow, Nat.ceil) and the measure-theoretic union bound; nothing quantum is required by the formal statements. Contributions strengthening the milestone list towards the circuit level — a formal model of error locations in a network, of the induced next-level error model, or of stabilizer-code recovery — are welcome as further targets.
Quantum computations are performed on physical devices whose elementary operations are never exact: every gate, every idle qubit, every time step is subject to decoherence, damping and systematic inaccuracy. Without protection these errors accumulate and destroy the computation. In 1997 Dorit Aharonov and Michael Ben-Or proved that this can be overcome: as long as the error rate — the probability, per location per time step, that a fault occurs — is below a fixed positive threshold, an arbitrary quantum circuit can be simulated reliably with only polylogarithmic overhead (arXiv:quant-ph/9906129). This threshold theorem is the reason large-scale quantum computing is regarded as physically possible in principle, and the number it produces is the target every hardware programme is measured against.
The engine of the proof is not quantum mechanical but combinatorial. A circuit is encoded, then the encoded circuit is encoded again, times over. The locations of the resulting circuit are organised into a tree of nested rectangles, and the computation survives precisely when the set of faulty locations is sparse in a recursive sense. The mission formalizes that engine: the recursive sparseness calculus of §7.4–7.6 and §8.2 of the paper, which converts a constant error rate below the threshold into a doubly exponentially small failure probability.
Fix two natural numbers: , the number of locations in a rectangle, and , the number of faulty sub-rectangles a rectangle tolerates (in the paper , where is the number of errors the code corrects and is the spread of a fault). A -rectangle is a single location of the circuit, and an -rectangle consists of many -rectangles. A fault pattern of an -rectangle records, for each of its locations, whether a fault occurred there.
Following Definition 18 of the paper, a fault pattern is -sparse by recursion on : at level it is sparse when the location carries no fault; at level it is sparse when at most of the constituent -rectangles carry a pattern that is not -sparse. Under independent probabilistic noise of rate each location is faulty with probability , independently; write for the probability that the pattern of an -rectangle is -sparse, and for the probability that it is not.
Two thresholds appear. The threshold condition for probabilistic noise (Definition 19) is
and the threshold condition for general noise (Definition 21) is
The corresponding thresholds are and : every positive below them satisfies the respective condition.
The goal is the quantitative core of Theorem 10. Below the threshold there are constants such that for every circuit size and every accuracy some recursion depth satisfies both
The first inequality says that, over all rectangles of the simulated circuit, the probability that any of them carries a non-sparse fault pattern is below ; the second says that the overhead per simulated location, , is polylogarithmic in — the cost claimed in Theorem 10.
The milestones build up to it: the two threshold conditions hold below the respective thresholds, the exponent gap of equation 7.5 exists, the base case , the union-bound recursion , Lemma 10 itself (), and the analogous recursion 8.8–8.10 governing the bad part in the general-noise analysis.
Lemma 10 is where a constant error rate becomes a vanishing one. Each level of concatenation only has to improve reliability slightly, because the improvement compounds doubly exponentially in the number of levels; this is exactly why constant-rate noise can be tolerated while Shor's earlier scheme needed a polylogarithmically small rate. The same recursion, with in place of and an extra factor of , controls the trace norm of the bad part of the fault-path expansion in the general-noise model (§8.2), which is how the result is extended from probabilistic errors to decoherence, damping and systematic inaccuracy.
Formalizing this part of the paper yields a reusable, model-independent statement: nothing in the milestones mentions density matrices, so the sparseness calculus can later be plugged into a formal model of noisy quantum circuits, or reused for classical concatenated fault tolerance. What this mission does not do is formalize the circuit-level statement of Theorem 10 — that requires a full Lean model of quantum circuits with mixed states, fault-tolerant procedures, and the code constructions of §3–§6, and is deliberately out of scope here.
The obvious approach — bound the failure probability by a union bound over all fault sets of size and iterate — is exactly right, but the iteration is where the work is. The recursion only produces the doubly exponential decay once the threshold condition is converted into the strict exponent gap of equation 7.5, and the induction has to keep alive to reuse that gap at every level. In the general-noise recursion there is a second trap: the factor exceeds , so the recursion is not contracting termwise, and one needs to bound it by .
On the probabilistic side, the statements are about a genuine product distribution on an exponentially large sample space, not a recursively defined real number: the union-bound step must be carried out over the actual set of fault patterns, where independence across the sub-rectangles is what makes the product bound valid.
Fault patterns are a type defined by recursion on the level: is the booleans and is the functions from the sub-rectangles to ; every level is a finite type with decidable equality. Sparseness is a decidable predicate following Definition 18 verbatim. The noise distribution is given by the weight of a pattern, the product over all locations of (faulty) or (clean), and the sparseness probability is the sum of these weights over the sparse patterns — an honest finite product measure, so no hypothesis is built into the definitions and each statement carries the range hypotheses it needs.
Two conventions are worth flagging. First, the thresholds are formalized as and ; the paper prints the exponent as in equations 7.4 and 8.6, which is inconsistent with its own threshold conditions 7.3 and 8.5, and is the exponent for which the paper's claim "any satisfies the threshold condition" is true. Second, Lemma 10 is stated with rather than the paper's strict , because at the two sides are equal.
Nothing here is vacuous: all hypotheses are satisfiable — for instance , , satisfies every hypothesis of the goal — and the goal quantifies over all circuit sizes and all accuracies, so it cannot be discharged by a degenerate choice. A complete development needs only real analysis, finite sums and binomial counting from Mathlib. Contributions that generalise the branching factor to a per-rectangle bound , or that connect the calculus to a formal model of noisy circuits, are welcome.
A Padé approximant is the "best" approximation of a function near a point by a rational function of prescribed numerator and denominator degrees. The idea goes back to Georg Frobenius (1881), who studied relations among the convergents of a power series, and was developed systematically by Henri Padé in his 1892 thesis. Unlike a truncated Taylor polynomial, a rational approximant can reproduce poles, and it often converges where the Taylor series does not; this is why Padé approximants are standard tools in numerical computation, in the resummation of divergent perturbation series in physics, and — through the "ad hoc methods inspired by Padé theory" — in Diophantine approximation and transcendence proofs.
The theory rests on one structural fact, stated in the source as a single sentence: when it exists, the Padé approximant is unique as a formal power series for the given and . That sentence hides the two theorems this mission asks for — that a suitable pair of polynomials always exists, and that any two such pairs define the same rational function.
Fix a field and a formal power series
Given integers and , one looks for a rational function
whose Maclaurin expansion agrees with that of through order , i.e.
This is denoted .
Written this way the condition is nonlinear in the unknowns and presupposes . The classical device, due to Frobenius, is to linearize: instead of asking that vanish to order , one asks that
A pair satisfying these three conditions is what this mission calls a Padé pair of type for ; it is the predicate every statement below is phrased with. The linearized problem is a homogeneous linear system, so it is always solvable, whereas the original ratio problem is not: the linearized solution may have , in which case no normalized of the displayed shape exists (the " entry of the Padé table is defect"). The two formulations coincide exactly when .
The goal theorem is the conjunction of existence and uniqueness for the linearized problem, over an arbitrary field , for all :
Statement (U) is the precise content of "the Padé approximant is unique": the two pairs need not be equal — they may differ by a common polynomial factor — but they determine the same element of , and hence the same formal power series wherever the quotient is defined.
The milestones are: existence (E); uniqueness (U); the equivalence between the linearized condition and agreement of Maclaurin expansions when ; the Bézout form used by the extended-Euclidean computation of the approximant; the normalization of the denominator to constant term ; and the two worked examples given in the source, namely for and for .
The result itself. Existence and uniqueness are what make the Padé table — the doubly indexed array — a well-defined object, and therefore what make every identity among its entries (the block structure of the table, the Frobenius identities, Wynn's -algorithm and the cross rules) meaningful. Every computational route to the approximant, including the extended-Euclidean route recorded in the source, computes the approximant only because of (U).
Formalizing it. Mathlib has formal power series, polynomials, truncation, and the inverse of a power series with invertible constant term, but no Padé theory: there is no predicate for the condition and no existence or uniqueness statement. This mission adds the linearized predicate and the two structural theorems, which is the minimum foundation on which the Padé table, the block theorem, and convergence results such as Nuttall–Pommerenke could later be built. The results are classical and have textbook proofs; the contribution here is the machine-checked development, not new mathematics.
Neither theorem is deep, but both have a specific step where the obvious approach fails.
For existence, the naive route — solve for , then read off — requires knowing that the homogeneous system for the coefficients of given by the equations "coefficients of of vanish" has a nonzero solution. That is a rank argument about a rectangular Toeplitz-like matrix, and the work in Lean is in packaging it as a linear-algebra statement rather than in the mathematics.
For uniqueness, the one-line argument is to divide: from and conclude . This is invalid, because need not be invertible modulo (its constant term may vanish) and is not a domain. The correct argument compares , whose left side is divisible by while its right side has degree at most ; the difficulty is the degree bookkeeping, not the algebra.
A solver should also note that (U) is not the claim , which is false — rescaling, or a common factor, gives distinct pairs.
The development is over an arbitrary field F (the definition itself only needs a commutative ring), with f : PowerSeries F, and P Q : Polynomial F. Conventions fixed in Lean, and worth reading before starting:
Polynomial.degree ≤ (m : WithBot ℕ), so the zero polynomial satisfies every bound; in particular is allowed and is excluded by an explicit hypothesis.PowerSeries F through the canonical coercion.PowerSeries.exp ℚ and supplied as an explicit series .Contributions of further Padé material — the Padé table, defect entries, the block structure, or the -algorithm — are welcome as follow-up missions built on this predicate.
A two-stage stochastic linear program chooses a first-stage decision before uncertain coefficients are known and then uses recourse variables to repair the decision after the data are observed. The resulting expected recourse cost is central to existence, stability, and numerical methods: if it can be infinite, an apparently feasible model may still have no meaningful expected objective; if it is differentiable with a continuous gradient, deterministic smooth optimization methods become available on the feasible first-stage domain. Chapter III of Peter Kall's Stochastic Linear Programming develops these properties for fixed recourse. This mission packages two complete results from that development: Theorem 12 on continuous differentiability and Theorem 15 on the exact finiteness criterion under complete recourse.
Theorem 12 is the goal. Theorem 15 is retained as a separate source theorem from the same expected-recourse setting, not as a lemma asserted to prove Theorem 12. Keeping both statements makes the distinction between the general feasible-domain regime and the stronger complete-recourse regime explicit.
Fix a deterministic matrix (W\in\mathbb R^{m\times p}). A random data point is a triple (d=(A,b,q)), where (A\in\mathbb R^{m\times n}), (b\in\mathbb R^m), and (q\in\mathbb R^p), with arbitrary joint probability law μ. For a first-stage vector (x\in\mathbb R^n), the pointwise recourse value is the extended-real linear-program value
The extended-real convention records an infeasible recourse problem as (+\infty) and an unbounded-below problem as (-\infty). The recourse domain is
Thus (K) requires almost-sure feasibility but does not assume complete recourse and does not exclude a value of (-\infty). The signed extended expectation follows Kall's equation III.(8): it is the integral of the positive part minus the integral of the negative part. A separate real-valued expected-recourse adapter integrates (Q(x,d).\mathrm{toReal}); the target uses that adapter only after explicitly concluding almost-sure finiteness and integrability, so totalization at infinities does not hide a divergent cost.
The shared moment condition is exactly the disjunction from Theorem 10 and Corollary 11: all coordinates of (A,b,q) are square integrable; or (q) is almost surely constant while (A,b) are integrable; or (A,b) are almost surely constant while (q) is integrable; or all three random coefficient ranges are bounded. No independence or finite-support hypothesis is imposed.
Finally, (W) has complete recourse when every right-hand side (z\in\mathbb R^m) admits a nonnegative (y) satisfying (Wy=z). This is stronger than membership of one decision in (K), but it does not by itself prevent an unbounded-below recourse cost.
Assume one of the four moment alternatives, assume the signed expected recourse is strictly above (-\infty) at every (x\in K), and assume the joint law μ is absolutely continuous with respect to Lebesgue measure on the full finite-dimensional coefficient space. Then the pointwise recourse value is finite almost everywhere and its real projection is integrable for each (x\in K). Moreover, there is a continuous field of linear functionals (g(x)) such that
including boundary points of (K). In Lean this is stated by ContinuousOn g K together with HasFDerivWithinAt for the expected-recourse function at every point of (K). It is not weakened to differentiability only on the interior, and it does not add complete recourse.
Under complete recourse and one of the same four moment alternatives, for an arbitrary fixed (x\in\mathbb R^n),
The left side means that the signed extended expectation equals a real number, not merely that a totalized real integral returns a value. The right side requires feasibility of the dual inequalities almost surely; it does not require attainment or optimality. This full equivalence is the mission's supporting milestone.
Theorem 12 supplies a smooth expected objective on the entire source feasible domain under an absolutely continuous data law. That conclusion is stronger than convexity or local Lipschitz continuity: it provides a continuously varying derivative while retaining boundary points and the random dependence of all coefficient blocks. The explicit finiteness and integrability clauses make clear when the real expected objective faithfully represents the extended-real model.
Theorem 15 separates two different well-posedness questions. Complete recourse guarantees primal feasibility for every residual, while almost-sure feasibility of the dual inequalities is exactly what prevents the expected value from escaping the real line under the stated moment conditions. Omitting either direction would lose the source's characterization.
Both results are established in the 1976 book; the staged Lean theorem declarations contain proof placeholders. Completing them would give machine-checked versions of the source statements using reusable definitions for equality-constrained nonnegative linear-program values, pointwise recourse, expected recourse, complete recourse, the signed expectation, and the four moment regimes.
For differentiability, a pointwise optimal solution or dual vector need not vary continuously when the active basis changes. Absolute continuity removes coefficient configurations lying on relevant exceptional hyperplanes only after a measure-theoretic argument, and the conclusion must hold relative to a possibly closed feasible domain rather than only on an open set. One must also prove finiteness and integrability before using the real-valued expectation; simply differentiating the totalized toReal expression would not establish the source theorem.
For finiteness, complete recourse handles feasibility but not unbounded negative cost. The dual system is random through (q), and the equivalence concerns almost-sure existence of a dual-feasible vector together with a signed extended expectation. Assuming dual feasibility or integrability of the recourse value at the outset would make one direction circular.
All coefficient spaces use finite Fin indices and real scalars. The law is an arbitrary probability measure on the joint product (A,b,q). The density premise for Theorem 12 is ambient absolute continuity with respect to the product Lebesgue volume; it is not a density on an unspecified lower-dimensional support. Consequently, some constant-coordinate moment branches may be incompatible with that density premise, matching the reviewed ambient interpretation rather than silently changing the measure space.
The feasible domain uses (Q(x,d)<+\infty) almost surely and includes its boundary. The signed expectation preserves positive and negative infinities. Theorem 12 assumes it is above (-\infty) on (K) and concludes the conditions needed for the separate real integral. Theorem 15 adds complete recourse but no density, independence, finite support, pre-assumed dual feasibility, or pre-assumed value integrability. Its decision (x) remains arbitrary.
The mission reuses the platform definitions of LPValue, PointwiseRecourse, ExpectedRecourse, and CompleteRecourse. The book-local Kall1976 namespace contains only the expression-essential data type, feasible domain, signed expectation, moment disjunction, and the two reviewed theorem statements. Contributions may add analytical, measure-theoretic, or linear-programming lemmas needed for proofs, but may not replace the signed expectation by a totalized real value, restrict Theorem 12 to the interior, or weaken Theorem 15 to one implication.
A convex polytope has both a geometric realization and a finite combinatorial structure: its faces, ordered by inclusion. Reconstruction asks how much of that structure must be known before the rest is forced. Chapter 12 of Branko Grünbaum's Convex Polytopes distinguishes several forms of unambiguity and then proves reconstruction results for general polytopes and for important special classes. The central input is not a coordinate description. It is a lower-dimensional part of the face lattice, such as the graph or a higher skeleton.
This mission groups five established results that address the same recovery problem under different hypotheses. The main theorem reconstructs every d-polytope, for d ≥ 3, from a supplied equivalence of its (d−2)-skeleton. The supporting targets sharpen the amount of data needed for simple polytopes, simplicial polytopes, and zonotopes, and record a polynomial-time version whose output is the vertex–facet incidence relation. Each theorem retains its own quantified polytopes, equivalence, and reconstruction witness. Grouping them does not require a single witness to serve all five regimes.
A d-polytope is represented as the convex hull of a nonempty finite subset of Fin d → ℝ, with affine span equal to the whole ambient space. A face is an exposed face in Mathlib's sense. This convention includes the empty face and the polytope itself. PolytopeFace P is the resulting face poset ordered by set inclusion.
For a natural number k, the k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face whose affine dimension is at most k. An equivalence of skeletons is an order equivalence, so it preserves and reflects every inclusion relation among the retained faces. Strong unambiguity is represented by demanding an extension of every supplied skeleton equivalence, rather than merely asserting that some full face-lattice equivalence exists. The extension equation requires agreement on every skeleton face.
The graph of a polytope is modeled through its vertices and one-dimensional faces. PolytopeVertex P consists of points whose singleton is exposed. Two distinct vertices are adjacent in polytopeGraph P when they lie in a common one-dimensional exposed face. A source polytope is simple when every vertex has exactly d graph neighbors. A simplicial polytope is one whose facets are simplices. A zonotope is a finite vector sum of closed line segments; full dimension is imposed separately by the d-polytope hypothesis.
(d−2)-skeletonFor d ≥ 3, d-polytopes P and Q, and every supplied order equivalence
the main target produces an order equivalence of the complete face posets whose restriction is exactly φ. This is the explicit face-lattice reformulation of Theorem 12.3.1. It asserts strong and weak d-unambiguity, but it does not add dimensional unambiguity.
The Blind–Mani target uses only the 1-skeleton when the source is simple. The target polytope is arbitrary in the same dimension; its simplicity is not assumed separately. The Björner–Edelman–Ziegler target likewise uses the 1-skeleton when the source is a full-dimensional zonotope, without requiring the target to be a zonotope.
Perles's target has a different domain. The source is a simplicial d-polytope, the target is an arbitrary e-polytope, and the input compares their floor(d/2)-skeletons. Its conclusion includes both e=d and extension of the supplied skeleton equivalence. Thus this clause, unlike the other reconstruction clauses, explicitly includes dimensional unambiguity.
The algorithmic target states that one binary function works uniformly for every d ≥ 3, every vertex count, and every valid labelled d-polytope input. The input contains the complete duplicate-free table of nonempty faces in dimensions at most d−2; the output contains exactly the facets, as labelled vertex sets. Dimension, vertex count, and row count are self-delimiting headers, followed by dense incidence rows. Correctness is required on valid encodings, while the binary function itself is total. ContainmentPolyTime uses Mathlib's Turing-machine polynomial-time predicate together with finite stack alphabets.
The general theorem says that codimension-two face data already fixes every missing facet and incidence relation. The special-class results show that much smaller data can suffice: only the graph for simple polytopes and zonotopes, and the half-dimensional skeleton for simplicial polytopes. Perles's result also recovers ambient dimension. The algorithmic theorem separates mere uniqueness from effective recovery by requiring one polynomial-time procedure and a concrete vertex–facet output.
Formalizing these results creates reusable interfaces for face-poset reconstruction, graph-based simplicity, zonotopes, and finite incidence encodings. It also records distinctions that informal summaries can blur: extension of every supplied equivalence versus existence of an unrelated isomorphism; combinatorial reconstruction versus dimension recovery; and uniqueness versus polynomial-time computability. The statements are established mathematics, but their Lean theorem bodies remain open and use sorry; this mission makes no proof-completion claim.
Counting faces or matching their dimensions does not reconstruct the face lattice. The conclusion must preserve every inclusion relation and agree with the specific equivalence supplied on the visible skeleton. An arbitrary isomorphism of complete face lattices would be too weak if it failed to extend that map.
For simple polytopes and zonotopes, graph isomorphism alone does not expose higher-dimensional faces directly; the target still asks for all incidences. In the simplicial case, reconstructing the lattice without proving e=d would omit the dimensional-unambiguity clause. For the effective result, a mathematical reconstruction argument is insufficient unless it yields one uniform polynomial-time binary function. Conversely, an efficient procedure on an incomplete or coordinate-dependent input would not meet the stated incidence model.
All geometric ambient spaces are finite-dimensional real coordinate spaces. Full-dimensional polytopes are nonempty finite convex hulls. Exposed faces include both improper faces. Skeletons retain the empty face separately, avoiding a natural-number encoding of its source dimension −1. Natural subtraction in d−2 is protected by the explicit 3 ≤ d hypothesis wherever that threshold is used.
The graph definition removes loops and symmetrizes adjacency. Simplicity is the exact neighbor-cardinality condition at every vertex. The zonotope definition allows arbitrary segment endpoints and degenerate summands, but the separate full-dimensionality hypothesis rules out a lower-dimensional source. Only the simplicial theorem compares different ambient dimensions and concludes their equality.
The algorithm receives no real coordinates. Its vertex map is injective and has range exactly the exposed singleton faces. The input and output row predicates are biconditionals, so they prohibit missing faces and extraneous rows; Nodup prohibits repetitions. The empty face is implicit, and the output row order is unrestricted. Contributions must not weaken extension to unrelated existence, assume the target belongs to the source's special class, omit Perles's dimension equality, replace complete incidence tables by partial data, or allow the polynomial bound to depend on the individual instance.
An exclusion system models particles moving among sites under the rule that each site is either vacant or occupied. A move exchanges the occupation variables at two sites, so particle number is conserved. On a countably infinite site set, however, the formal sum of all possible exchanges need not automatically determine a well-defined Markov evolution. Individual rates can be continuous and bounded while infinitely many potential exchanges remain active. Chapter 8, Section 3 of Stewart N. Ethier and Thomas G. Kurtz, Markov Processes: Characterization and Convergence, gives conditions under which this formal operator closes to the generator of a conservative Feller semigroup Ethier--Kurtz, Theorem 3.6.
This mission states that theorem with its complete weighted two-site domain and its finite-coordinate core. It does not replace the countable system by a finite Markov chain, collapse the ordered-pair generator sum, or substitute the neighboring spin-flip theorem. Spin flips change particle number one coordinate at a time; exclusion moves exchange two coordinates and conserve it.
Let S be a countable type of sites. A configuration is a function η : S → Bool, where false and true relabel vacancy and occupation. The product topology is induced by the discrete topology on Bool. The Lean space C(S → Bool, ℝ) consists of continuous real-valued observables on this compact configuration space and carries the uniform norm.
For sites i and j, exclusionExchange i j η swaps η i and η j and leaves every other coordinate unchanged. When i = j, the exchange is the identity. For an observable f, its two-site exchange variation is
The theorem assigns a continuous nonnegative rate c i j to every ordered pair and a nonnegative real dominating weight γ i j. Both families are symmetric, the diagonal rates vanish, and c i j η ≤ γ i j. The rows of γ are summable with one uniform upper bound, which is the Lean form of equation (3.27).
Rate dependence on the configuration is controlled through a different operation. spinFlip k η toggles the single coordinate k, and spinVariation (c i j) k measures the resulting uniform change in the rate. Equation (3.28) requires these single-site influences to be summable and bounded by K * γ i j, with one constant K for all pairs. The influence condition therefore deliberately uses single-site flips even though the dynamics itself uses two-site exchanges.
The pre-generator graph implements equation (3.29). Its domain is exactly the continuous observables satisfying
where the sum is over ordered pairs and has no factor of one half. For (f,g) in the graph, the continuous output satisfies
The goal is Theorem 3.6 in full. Every observable in the weighted domain has a continuous image in the graph. The graph closure in the product uniform-norm topology is single-valued and equals the derivative graph of a strongly continuous contraction semigroup. The semigroup preserves nonnegative functions and the constant function one, expressing the conservative Feller conclusion.
The last clause retains the source's cylinder core. Restrict the initial graph to observables determined by finitely many coordinates: there is a finite set F such that configurations agreeing on F receive the same value. The closure of that restricted graph equals the entire closed generator graph. Generation, the full weighted domain, and the core remain one target because they are conclusions of the same source theorem.
The theorem turns an infinite formal exchange sum into a closed Markov generator on continuous observables. The conclusion is stronger than pointwise convergence of the series: it identifies the whole generator domain through a derivative biconditional, provides positivity and conservativity, and establishes a finite-coordinate class from which the closed graph can be recovered.
The result is proved in the textbook. The formalization target is its precise Lean statement, including symmetry, zero diagonal, domination, the uniform row bound, the single-site influence bound, the weighted ordered-pair domain, graph closure, Feller generation, and cylinder core. Reusable infrastructure consists of the book-wide contraction-semigroup predicate and the already shared single-site flip and variation definitions; the exchange, exchange variation, and weighted graph are specific to this model.
A naive finite-state jump-process argument does not apply. Countability and a uniform row bound do not turn the full ordered-pair collection into a finite set of moves. Pointwise notation for the exchange series also does not by itself prove that the result is continuous, that the graph closure is single-valued, or that finite-coordinate observables form a core. The weighted two-site domain and the configuration-influence condition are therefore essential parts of the theorem rather than optional regularity assumptions.
The spin-flip and exclusion models cannot be interchanged. A coordinate flip creates or removes occupation and is measured by a one-site domain. An exclusion move conserves occupation by swapping two coordinates and requires the γ-weighted two-site variation domain. Only the rate-influence hypothesis uses the shared one-site variation.
The Lean statement allows empty, finite, and countably infinite S, matching the source's countability assumption without adding nonemptiness. Bool is an exact two-state encoding of {0,1}. Real suprema define both one-site and two-site uniform variations over the nonempty compact configuration space. Explicit Summable hypotheses prevent divergent real tsum expressions from being silently totalized.
The graph records a continuous output equal to the actual pointwise ordered-pair series. Its first conclusion ensures that this representation does not shrink the stated weighted domain. Closure is taken in C(S → Bool, ℝ) × C(S → Bool, ℝ). The semigroup is real-time indexed, while its laws and bounds are imposed for nonnegative times. No finite-site restriction, finite-total-rate replacement, factor of one half, exchange-based substitute for the influence bound, or weakened core statement is admitted.
A convex polytope carries more than its underlying topological ball. Its faces form a finite complex whose incidence relations record the polytope's combinatorial structure. Chapter 11 of Branko Grünbaum's Convex Polytopes asks how this structure can be represented by subdivisions and by embeddings into Euclidean spaces of smaller dimension. The first target places every polytope boundary over the simplest boundary complex in the same dimension, that of a simplex. The second determines exactly how much ambient dimension is needed to realize any prescribed skeleton, both topologically and as a genuine polytopal complex.
These are established mathematical results, not open conjectures. The mission poses their reviewed Lean statements as formal proof tasks. It groups Theorems 11.1.1 and 11.1.9 because both use the boundary-complex, carrier, refinement, skeleton, and incidence-equivalence model introduced at the start of §11.1. They remain separate statements with separate quantified objects; no common homeomorphism, realization, or witness is imposed between them.
A d-polytope is represented in Lean as the convex hull of a nonempty finite subset of Fin d → ℝ whose affine span is the whole ambient space. A face uses Mathlib's exposed-face convention. For polytopes this includes the proper exposed faces as well as the empty and full improper faces.
The boundary complex boundaryFaces P consists of every exposed face of P except P itself. Thus the empty face is retained. Its carrier is the union of those cells. The statement BoundaryRefines P Q supplies one homeomorphism between the two complete boundary carriers. For each boundary face of Q, its inverse image must be exactly the union of a finite subfamily of boundary faces of P, and that subfamily must be closed under taking faces. Exact inverse-image equality is essential: containment alone would not express the source's refinement relation.
The k-skeleton face poset SkeletonFace P k contains the empty face and every nonempty exposed face of affine dimension at most k, ordered by inclusion. Its topological carrier skeletonCarrier P k is the union of these cells. A finite polytopal complex in real m-space is a finite family of polytopal cells, explicitly permitting the empty cell, closed under taking faces, with each pairwise intersection a face of both participating cells. Combinatorial equivalence is represented by an order isomorphism of the complete cell posets, rather than merely by a homeomorphism of their carriers.
For every natural dimension d, every full-dimensional d-polytope P, and every affinely independent family of d+1 vertices in real d-space, the first target states
The chosen vertices describe an arbitrary d-simplex. The result does not assume that P is simplicial. The same homeomorphism controls all target-face inverse images, and the zero-dimensional case retains its empty boundary carrier.
For 1 ≤ k ≤ d and every d-polytope P, the second target identifies two attained minima. The first ranges over dimensions m for which the carrier of the k-skeleton is homeomorphic to some subset of real m-space. The second ranges over dimensions m for which a finite polytopal complex in real m-space has a cell poset order-isomorphic to the complete k-skeleton face poset. Both minima equal
This compact formula preserves the four cases stated in Theorem 11.1.4: d=k, d=k+1, k+2≤d≤2k+2, and d≥2k+2. The latter two formulas agree at their shared endpoint. Applying the arbitrary-polytope statement to simplices retains the source comparison with a(d,k) and b(d,k).
The refinement theorem gives a uniform relationship between the boundary complex of an arbitrary polytope and the simplex boundary. It preserves both topology and the subdivision data carried by faces. The embedding theorem then gives the exact ambient dimension required by every k-skeleton, while showing that allowing an arbitrary topological embedding does not improve on the best dimension obtainable from a combinatorially equivalent polytopal complex.
Formalizing these targets provides reusable infrastructure for boundary carriers, face-closed refinements, skeleton carriers, and finite polytopal complexes. The definitions distinguish topological equivalence from incidence equivalence and record attainment as well as lower bounds through IsLeast. The theorem bodies remain open: the proposal does not claim that either classical result already has a Lean proof.
For the refinement target, a homeomorphism of boundary carriers alone is insufficient. One must also prove, simultaneously for every target cell, that its inverse image is exactly a finite union of source cells closed under faces. The obvious topological equivalence of polytope boundaries therefore does not establish the required combinatorial refinement.
For the embedding target, constructing one realization in the displayed dimension proves only attainment. It does not rule out all realizations in smaller dimensions. Conversely, a lower-bound argument does not construct the topological subset or polytopal complex required by IsLeast. Both notions of realization must meet at the same explicit value without replacing the full cell-poset equivalence by a weaker topological condition.
All ambient spaces are finite-dimensional real coordinate spaces. Polytopes are nonempty finite convex hulls, and the goal polytopes are full-dimensional. Exposed faces include the empty face and the whole polytope; the boundary removes only the whole polytope. Skeleton dimension is the real dimension of an affine-span direction, with the empty face admitted separately. The topological minimum ranges over arbitrary subsets with the subspace topology, while the combinatorial minimum ranges only over finite polytopal complexes satisfying face closure and the common-face intersection condition.
IsLeast asserts both membership of the displayed value and that it is a lower bound for every attainable dimension. The condition 1 ≤ k ≤ d excludes the source's untreated k=0 case. Natural subtraction occurs only in the branch d>k+1, so the formula does not gain a truncated-subtraction shortcut. Contributions must not drop attainment, restrict the arbitrary polytope, replace exact inverse-image equality by containment, omit empty faces, weaken order isomorphism to a carrier homeomorphism, or require the two source theorems to share a witness.
A convex polytope has finitely many faces in each dimension, and their numbers form its f-vector. Determining which integer vectors occur is a basic realization problem in discrete geometry: necessary identities such as Euler's relation do not by themselves decide whether a proposed vector comes from a polytope. For simplicial polytopes, whose facets are simplices, the g-theorem gives a complete answer. In the matrix formulation recorded in Chapter 10 of Branko Grünbaum's Convex Polytopes, realizable extended f-vectors are exactly the products of M-sequences with an explicit binomial matrix.
This is a known theorem, not an open conjecture. The mission asks for a machine-checked proof of the reviewed Lean statement while preserving the theorem's full biconditional. It is not merely a collection of upper or lower bounds on individual coordinates: one side asserts geometric realizability of the whole vector, and the other gives a simultaneous arithmetic characterization.
A d-polytope is represented as a nonempty finite convex hull in the real coordinate space Fin d → ℝ whose affine span is the whole space. A nonempty exposed face has dimension equal to the real dimension of the direction space of its affine span. The function faceCount P j counts the nonempty exposed j-dimensional faces of P.
A simplicial d-polytope is a d-polytope for which every facet is the convex hull of d affinely independent points. The extended f-vector is indexed by Fin (d+1): its coordinate f 0 is fixed to one for the empty face, while f j.succ is the integer embedding of faceCount P j for each j : Fin d.
An M-sequence in the formalization is a natural-valued function g used only from index zero through m. It begins with g 0 = 1. Each positive entry through m is either zero, with empty boundary, or is represented by a strictly increasing binomial expansion whose upper boundary is at most the preceding entry. This is the finite Macaulay condition used on printed pages 198a–198b.
The integer-valued matrix gTheoremMatrix d j k is Björner's matrix . Its entries are
with rows and columns . Subtraction is performed in the integers, not truncated natural-number arithmetic.
For every natural dimension d and every integer vector f : Fin (d+1) → ℤ, the main item states the equivalence
The left side includes both f 0 = 1 and a single simplicial polytope realizing every remaining coordinate. The right side uses one M-sequence and checks the matrix equation at every column. Its sum ranges over exactly Finset.range (d / 2 + 1), so the row indices are zero through the floor of half the dimension. Values of g outside that finite range are irrelevant on both sides of the arithmetic condition.
The theorem converts a geometric existence question into an exact finite arithmetic criterion. It characterizes the entire vector at once, retaining the correlations between face numbers that coordinatewise extremal theorems cannot express. The biconditional also has two substantive directions: every simplicial polytope produces an M-sequence, and every permitted M-sequence is realized by a simplicial polytope.
Formalizing this statement supplies reusable interfaces for full-dimensional polytopes, exposed-face counts, simpliciality, finite M-sequences, and the g-theorem matrix. The theorem body remains open in the proposal. The established mathematical result is being posed as a Lean proof task rather than claimed as already machine-checked.
Neither direction follows from Euler or Dehn–Sommerville linear identities alone. Those equations describe an affine subspace but do not impose the nonlinear integrality and growth conditions encoded by an M-sequence. Conversely, verifying the Macaulay inequalities for a candidate sequence does not directly construct a polytope realizing all coordinates. Proving separate inequalities for each face number would also be insufficient, because the target requires one polytope and one sequence to witness simultaneous equality of the complete vectors.
All ambient geometry is finite-dimensional and real. Faces use Mathlib's exposed-face convention, and faceCount excludes the empty face before assigning a natural dimension; the leading coordinate f 0 = 1 restores the empty face in the extended vector. The polytope witness is full-dimensional in Fin d → ℝ. The matrix and the target vector are integer-valued, while the M-sequence itself is natural-valued.
The mission retains all dimensions, including the low-dimensional boundary cases. Natural subtractions inside binomial indices use Lean's truncated subtraction exactly as in the reviewed source adapter, while subtraction between the two binomial coefficients occurs in ℤ. The M-sequence witness is constrained only over the finite range used by the matrix product; no unintended condition is imposed on its unused tail.
The definitions of IsDPolytope and faceCount are reused from exact private platform declarations. The simplicial predicate is reused byte-for-byte from the preceding staged package, and the M-sequence and matrix declarations preserve their reviewed local definitions with only platform-compatible module imports. Contributions should prove the iff without weakening it to one direction, replacing realizability with coordinatewise inequalities, restricting the dimension, changing the index ranges, or allowing different witnesses for different coordinates.
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).
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.
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:
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).log(a(max)/a(min)) term of Theorem 14.1 is necessary.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.
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.
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).
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.
Fix a graph , , , with integer edge capacities . Routing requests 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 -competitive algorithm routes at least of the maximum possible bandwidth while guaranteeing every edge's load (bandwidth allocated divided by capacity) is at most . The chapter's generic algorithm (Section 9.1) maintains, for each of copies of the graph (copy keeping only edges of capacity at least , each capped at ), 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 ) if that length is below , multiplicatively updating on the path's edges; otherwise, subject to a capacity-limited fallback rule, on an arbitrary feasible path.
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 's own guarantee, which Theorem 9.2's proof composes across all copies: the algorithm accepts at least (the maximum splittable bandwidth achievable in , out of the requests introduced to it) and incurs load on every edge of .
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 - 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 -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).
This is the most algorithmically intricate chapter in this series: the algorithm processes each
request against every one of 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.
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.
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 -competitive result, Section 6.2) rests entirely on it.
Fix a set of leaves (the book's finite ) of a weighted star, each leaf at distance from the center. The chapter immediately collapses the full star metric to a single per-state transition charge , since on a star every transition costs at most , 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 occupied and the service cost accumulated while in that state, ending with a transition (cost ) to the next run's state; its total cost is . A new-model solution is a finite sequence of phases, each specifying a state visited; a phase's cost is exactly 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 -value), so the new model's total cost is .
Lemma 6.1 (goal, p. 144): any standard-model solution's runs transform into a new-model solution whose cost is at most ; in particular .
Lemma 6.2 (milestone, p. 145): any new-model solution's phases , with each phase's actual service , are simultaneously a legal standard-model solution (the same trajectory, recosted) whose standard-model cost is at most .
Together (stated in the book but not separately numbered, hence not a formalization target here): a -competitive algorithm in the new model implies a -competitive algorithm in the standard model.
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 -server) with a different metric structure and is not adjacent
substrate for this chapter's weighted-star MTS model.
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
) and only bounds its cost, never gives 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.
WeightedStar V bundles centerDist : V → ℝ (the book's ) with non-negativity;
WeightedStar.d is the collapsed charge . 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
— that assumption only matters for the unnumbered -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 , rather than a full metric
, 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 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 -competitive claim as a follow-on mission
once it can be stated against a numbered result.
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.
Fix an integer and work in the real coordinate space . In Lean this space is represented by Fin d → ℝ. A -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 as a -polytope.
A polytope is centrally symmetric when there is a center such that reflection through leaves 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 , represented in Lean by AffineEquiv.pointReflection ℝ c.
A finite family of -polytopes is neighborly in the sense of Grünbaum §7.4 when, for every distinct , the intersection has affine dimension . 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.
For every and every natural-number threshold , the target asserts the existence of a finite set such that
every is a centrally symmetric -polytope, and every distinct pair satisfies
Quantifying over every threshold 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 and .
The result shows that central symmetry does not impose a finite ceiling on neighborly-family size once . 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.
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.
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 .
No common center, congruence, translate-only model, face-to-face condition, or infinite-family claim is included. The case is included, while dimensions below three are excluded exactly as in the source. The case 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.
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).
The Lean development represents the ambient real space of dimension as Fin d → ℝ. A predicate IsDPolytope P says that 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 itself; an order isomorphism of these types is the formal representation of combinatorial equivalence.
For a positive integer , a polytope is -neighborly when every -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 to be neighborly when it is -neighborly. The theorem therefore assumes and uses IsKNeighborly r for both parent polytopes.
Let and be full-dimensional neighborly polytopes in . Their vertices are enumerated injectively by maps . A permutation records the prescribed correspondence between the two vertex sets, and an order isomorphism between the full face posets witnesses that this correspondence comes from a combinatorial equivalence of the parent polytopes.
For every index set , the target produces an order isomorphism
and requires it to carry each selected singleton vertex to . The quantifier over is unrestricted. Empty, singleton, lower-dimensional, and full vertex subsets are all included. No selected subpolytope is required to be full-dimensional or neighborly.
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.
The parent face-poset isomorphism directly identifies the faces already present in and , but a subpolytope can have faces that are not faces of its parent. Consequently, restricting 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.
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 with . 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.
A basic classification question in polytope theory asks what combinatorial types can occur when the dimension and number of vertices are fixed. The question is not merely whether there are finitely many types. Effective enumeration asks for a uniform algorithm which produces the complete list, with no omissions and no repeated combinatorial type. This converts a structural finiteness assertion into a finite procedure that can in principle support tabulation, comparison, and exhaustive study of small polytopes.
Grünbaum formulates this enumeration problem in §5.5 of Convex Polytopes and states its solvability as Theorem 5.5.2, printed p. 91 (PDF p. 117 of the supplied source). The surrounding discussion represents a combinatorial type by a finite scheme recording which subsets of labelled vertices form proper faces. The source then selects one representative for every realizable type. This mission follows that statement and encoding, as recorded in the supplied edition of the book (Springer DOI).
Fix natural numbers and . A -polytope is a nonempty finite convex hull in real coordinate space whose affine span is the whole space. Its faces are exposed faces. Following Grünbaum's convention, this includes the empty face and the polytope itself as improper faces. The natural-valued function counts nonempty exposed faces whose affine direction has dimension ; in particular, is the number of vertices.
A finite scheme is encoded as a list of lists of natural numbers. Each inner list represents a finite subset of vertex labels; its order and repeated entries have no mathematical meaning. The predicate SchemeRealizes k S P supplies an injective labelling whose range is exactly the set of exposed singleton vertices of . For every finite subset of natural numbers, membership of in the scheme is equivalent to the existence of a nonempty proper exposed face whose labelled vertices are exactly . Quantifying over every finite natural-number subset prevents an out-of-range label from silently denoting a face.
Two polytopes have the same combinatorial type when their complete face posets are order-isomorphic. The Lean subtype PolytopeFace P contains every exposed face of , including the two improper faces, and inherits the inclusion order. Thus Nonempty (PolytopeFace P ≃o PolytopeFace Q) is the formal equivalence relation used in the target.
The target is Grünbaum's Theorem 5.5.2 (book record and DOI). In Lean it states that there is a single function
which is computable and has the required behavior for every and . Its finite output satisfies three clauses. First, every output scheme is realized by some -polytope. Second, every -polytope with vertices realizes an output scheme. Third, if realizations of two output positions have order-isomorphic complete face posets, then those positions are equal. The three clauses jointly express soundness, completeness, and selection of a single representative per combinatorial type.
The theorem is Grunbaum2003.combinatorial_types_effectively_enumerable. Its body is an intentional sorry: this package supplies the reviewed, compiling statement and does not claim a machine-checked proof.
The conclusion gives more than abstract finiteness. It asserts one terminating procedure, uniform in both parameters, whose finite result represents all and only the desired types. Soundness prevents junk schemes; completeness prevents a legitimate polytope type from being missed; uniqueness prevents the output from counting the same type twice under different label lists. The theorem thereby isolates the precise data that an implementation or a formal proof must justify.
A formal proof would connect geometric realizability, finite incidence data, and computability in one development. The reusable infrastructure includes a full-dimensional finite-hull predicate, exposed-face counting, the complete exposed-face poset, and a labelled finite-scheme realization predicate. These definitions can also support formal statements about realization tests and enumerations under additional restrictions, without changing this mission's source obligation.
Finite syntactic generation alone is insufficient: most arbitrary families of vertex subsets need not be face systems of convex polytopes. Conversely, merely knowing that only finitely many combinatorial types exist does not provide an effective method for recognizing realizable schemes. The target must establish a total algorithm while simultaneously proving that every accepted scheme is geometrically realizable, every eligible polytope is represented, and no two selected entries encode order-isomorphic face posets.
Vertex relabelling is another source of redundancy. Two different nested lists can describe the same incidence structure, and two different geometric realizations can have the same face lattice. The uniqueness clause therefore compares realized complete face posets rather than list equality. A procedure that only enumerates labelled presentations, or one that decides equivalence without selecting representatives, would not prove the stated theorem.
The Lean function returns nested finite lists, so finiteness of each output and of each scheme is built into the type. Mathlib's Computable₂ supplies total computability on the paired natural inputs. The quantifier order chooses one before , , and any polytope, preserving uniformity. No rational-coordinate, simplicial, or fixed-combinatorics hypothesis is introduced.
IsDPolytope requires a nonempty finite convex hull with full affine span. faceCount P 0 = k imposes the prescribed vertex count. SchemeRealizes requires exactly the exposed singleton vertices and exactly the nonempty proper exposed faces under an injective finite labelling. PolytopeFace retains the empty and full improper faces for the final order-isomorphism comparison. These choices prevent the statement from becoming vacuous through an unconstrained incidence code or a predicate that assumes realizability.
Natural-number boundary cases remain explicit. If no -polytope with vertices exists, an empty output is permitted. In dimension zero, the unique point has one vertex and no nonempty proper face, so the empty scheme represents it. This coding extension does not remove any positive-dimensional case. The expression dependencies are exactly the four definitions listed above; proof-only lemmas and unrelated theorems from the book are not included as mission items.
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.
Fix natural numbers and . A -polytope is represented here as a nonempty convex hull of finitely many points whose affine span is all of . A face is the complete maximizing locus of a supporting linear functional, and a facet is a nonempty face of affine dimension . The quantity used in the target counts geometric faces, not the number of inequalities in a chosen description.
A -simplex is the convex hull of affinely independent points in . Write this simplex as . Affine independence makes full-dimensional, so is its ordinary ambient interior. No regularity, coordinate normalization, or metric condition is imposed on . A -flat is a translate of a -dimensional linear subspace. Its section of is the whole intersection .
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 whose range is and whose image of equals .
The single target is the prescribed-point section theorem:
Grünbaum writes the number of allowed facets as and uses an -simplex in . The Lean statement sets . Every input, including the simplex and its interior point, is universally quantified before and 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 .
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 : it permits the ambient simplex and any one of its interior points to be fixed first. The equality 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.
A flat chosen only to pass through 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 with the geometry of the simplex section without replacing the source hypothesis by a representation-dependent count.
Lean represents 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 . For , the hypothesis uses faceCount P (d - 1). For , 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 with direction dimension . The affine map is injective, has range exactly , and maps all of 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.
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 -polytope can retain a prescribed low dimensional skeleton of an -cube even when . 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.
Fix natural numbers . A -polytope here is a nonempty finite convex hull with full affine span. A face is an exposed subset of ; the empty face and 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 -cube is in , described coordinatewise by .
A cubical -polytope is such a full dimensional polytope whose every facet, meaning every nonempty exposed face of dimension , has a full face poset order isomorphic to the face poset of a standard -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 have binary coordinates.
The -skeleton face poset consists of the empty face together with all exposed faces of affine dimension at most , with their inherited inclusion order. The source speaks of a skeleton “of” an -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.
The single target is the unnumbered Joswig–Ziegler existence theorem as reported by Grünbaum. For every , with , it asks for a cubical -polytope such that
The witness may depend on both and . The strict inequality and lower bound are source conditions. They have not been expanded or narrowed for this package. For and , 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.
This theorem separates dimension of realization from the low dimensional combinatorics being realized. In particular, an -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.
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.
The Lean coordinate spaces are real functions on Fin d and Fin n. Natural division d / 2 is floor division, and the assumption 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 , 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.
source.pdf.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.
Fix a dimension . A -polytope here is a nonempty convex hull of finitely many points in with full affine span. A 0/1-polytope is the convex hull of a subset of . Both properties are required of the witness. A facet is a nonempty exposed face of affine dimension . The count uses the book's convention that the empty face has dimension 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.
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
The constant and threshold are chosen before ; the witness may depend on . 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 also keeps the natural-number expression 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.
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 for one fixed . 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.
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.
Lean represents a point of 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 ; 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.
source.pdf, PDF pp. 35, 51, 94).A polytope can be given by a list of vertices, a list of inequalities, or much less explicit access. The last case arises when geometric information is available through queries to a physical or computational object but a full description is unavailable. Grünbaum's account of a result by Gritzmann, Klee, and Westwater asks how much of a polytope can be recovered when each query shoots a ray from a known interior point and reports where it meets the boundary. The target is the complete face lattice, including incidence among faces of every dimension, and the cost is the number of oracle calls. The result appears in Convex Polytopes, §3.6, printed pp. 52b–52c (PDF pp. 74–75 of the supplied source).
Fix a positive integer . A -polytope is a nonempty finite convex hull in real coordinate space whose affine span is the whole space. The origin is known to lie in the interior of . A ray query supplies a nonzero direction ; the oracle returns the intersection of the positive ray with the boundary of . The theorem requires this boundary-point property for every nonzero direction. It does not give the reconstruction program the vertices, inequalities, face counts, or coordinates of .
A face is represented by an exposed subset of , ordered by inclusion. The resulting face lattice includes the empty and whole faces. For , counts nonempty faces of affine dimension ; hence is the vertex count and is the facet count. The empty face has dimension in the book's convention and is excluded from these natural-indexed counts. These conventions follow Grünbaum §§2.4 and 3.1 (printed pp. 17 and 31; PDF pp. 35 and 51).
The single source obligation is the unnumbered Gritzmann–Klee–Westwater theorem of Grünbaum §3.6. For each , one finite exact-real ray-query program works for every eligible and every correct ray oracle for . It halts with an encoding of the entire face lattice after at most
queries. The square on the facet count, both coefficients, and the continuation of “queries” across the page break are part of the printed statement. The program is selected before the unknown polytope and its oracle. The finite running time and output may depend on the instance. No common output, fixed runtime bound, or bit-complexity bound is asserted.
The Lean declaration is Grunbaum2003.ray_oracle_face_lattice_reconstruction. It asserts existence of the program, universal correctness, finite termination in a halt instruction, the displayed query inequality, and a concrete encoding of the whole face lattice. Its body is sorry: this package is a compiled statement and does not claim a machine-checked proof.
The conclusion recovers all face incidences from boundary samples on rays from one interior point. It is stronger than recovering only a vertex or facet list because the output explicitly determines the ordering of all faces. The bound measures the information requested from the oracle; the source does not constrain the number of internal arithmetic steps. A formal proof would connect the geometric reconstruction argument to a precise query machine and establish that its output matrix has exactly the claimed faces and inclusions.
Ray answers are geometric points, while the desired output is a global combinatorial structure. Sampling one direction per visible feature gives no direct certificate that all faces and incidences have been found. In particular, a proposed reconstruction must use only the permitted oracle answers and still know when its finite description is complete. The theorem also needs a uniform program for every polytope in a fixed dimension, with the instance dependent query count above. The present statement makes these quantifier and resource requirements explicit.
The machine has a finite instruction list for rational constants, exact real arithmetic, sign branches, tape movement, oracle queries, and halt. Its tape begins at zero. A query reads a nonzero direction from the tape and writes back the oracle's boundary answer; only this instruction increments the query counter. A zero direction, invalid label, or division by zero fails instead of creating a successful execution. Thus an unrestricted oracle value at zero cannot certify the theorem. Arithmetic and sign tests are exact real operations, matching the source's query model rather than imposing a bit model.
The output is a self-delimiting Boolean inclusion matrix indexed by a finite type. A bijection connects its indices to all exposed faces of , and each matrix entry is one precisely when the associated faces are ordered by inclusion. This rules out an output consisting merely of face counts, vertices, or facets. IsDPolytope, faceCount, PolytopeFace, the ray-oracle predicate, machine syntax and execution, and the output predicate are the expression dependencies of the goal. The exposed-face subtype and full-dimensional polytope predicate are shared unchanged with this book's other staged missions. Contributions needed for a proof may include geometric face finiteness and reconstruction lemmas, but those are not added as unreviewed mission items here.
source.pdf, PDF pp. 74–75).The cosmological constant entered physics in 1917, when Einstein added a term 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 , and a positive spatial curvature cancel exactly. Two facts about that balance shaped the next century of cosmology:
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- Supernova Search Team required . Interpreting as a vacuum energy density with equation of state then produced the cosmological constant problem: the measured value, about , is roughly 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 , the density-parameter bookkeeping, and the numerical size of the discrepancy.
A homogeneous isotropic universe is described by a positive scale factor on a set of times . Matter is pressureless dust, whose density dilutes with volume,
where and are reference values. Units are geometrized, , so has dimension (length); is Newton's constant and the curvature constant.
The dynamics are the two Friedmann equations. The first Friedmann equation is the constraint
and the acceleration equation for dust is
The Hubble parameter is , the critical density is , and the density parameters are
For , the constant function satisfies both Friedmann equations if and only if
in which case , , , and the equilibrium is unstable in the following exact sense: every solution of on with and is strictly increasing and satisfies ; and every positive solution on with and is strictly decreasing.
is exactly a perfect fluid of constant density and pressure ; the density parameters satisfy ; the acceleration equation is a consequence of the first Friedmann equation along a solution with ; and the observed is smaller than in Planck units.
The static solution is the historical origin of , 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 and the same linearization govern the late-time behaviour of the standard CDM model, where the growing mode becomes the de Sitter expansion .
What the mission produces on top of the textbook statements: a machine-checked ODE treatment of a dust-plus- cosmology that does not stop at the linearized equation. The classical physics argument computes 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.
The linearized step is routine calculus. The nonlinear instability is not: from with and strictly increasing on , one must run a bootstrapping argument in which the sign of controls , which in turn controls whether stays in the region where the sign of was known. The obvious approach — solve the ODE explicitly — is not available: the dust-plus- equation with the static value of 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 , where . Divergence additionally requires ruling out that stalls, i.e. a quantitative lower bound on once the solution has left a neighbourhood of .
Everything is stated for real-valued functions 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 (, , , or a general open set), never globally by fiat. Dust density, the Friedmann equations, the acceleration function , 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: , curvature entering as in the equation for , and 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 with positivity of assumed there, because a collapsing solution reaches in finite time; posing it on would make its hypotheses unsatisfiable and the statement vacuous. Second, the escape statement asks for , not merely , 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 at a zero of with , and the corresponding stability criterion, both of which are independent of cosmology.
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 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.
Spacetime is with coordinates and the Minkowski metric of signature : , , and for . Since is its own inverse, the same array serves as the contravariant metric used to raise indices. The symbol denotes the partial derivative in the -th coordinate direction, and is the wave operator.
The Dirac matrices are four complex matrices subject to the Clifford relation
together with the hermiticity relation , which makes hermitian and anti-hermitian. The standard Dirac basis is one concrete solution of these relations.
A spinor field is a map ; its Dirac adjoint is , and for a matrix the pairing is the complex number . A gauge field is a map whose value is the covariant component of the electromagnetic four-potential. From it one forms the field tensor (the curvature of the gauge connection)
and, for a coupling constant , the gauge covariant derivative . The Dirac current is .
With the mass of the spinor field, the QED Lagrangian density is
Its Euler–Lagrange equations are the Dirac equation and the Maxwell equation . The Lorenz gauge condition is .
For a coupled solution of the QED field equations in the Lorenz gauge, the four-potential obeys an inhomogeneous wave equation whose source is a conserved current:
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.
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 invariance of is what forces the coupling to be through and what makes the current conserved by Noether's theorem; conservation of is the consistency condition without which has no solutions at all, since the left side is annihilated by 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 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.
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 , and every "obvious" rearrangement of has to be done by hand with Finset.sum lemmas.
Second, differentiation is Fréchet differentiation in disguise: is the derivative of 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 as a formal symbol that commutes with everything fails: without a hypothesis, , and without differentiability the derivative takes the junk value , 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 , and the reality of , and , in the precise combination that cancels the terms containing between and . 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.
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 when is not differentiable at ; 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 , the mass and the gauge parameter are real, with no positivity or nonvanishing assumption on or .
Conventions fixed once and shared by every statement: signature ; ; ; 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 ; and the Dirac equation is .
The statements are not vacuous: , satisfies all field equations, plane-wave solutions of the free Dirac equation satisfy the Dirac hypothesis with , 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 and a quadratic expression in , 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.
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 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 billion years old" and "the expansion switched from decelerating to accelerating at redshift " actually come from. This mission formalizes that closed form and the two consequences just named.
Write for the dimensionless scale factor of a homogeneous isotropic universe, normalized so that at the present epoch, and for the Hubble parameter; denotes its present-day value. The energy content is described by present-day density parameters , the ratios of each species' density to the critical density . This mission works with the minimal, radiation-free, spatially flat case: a matter parameter and a dark-energy parameter with
Matter dilutes as and the cosmological constant does not dilute at all, so the first Friedmann equation for this content reads
The candidate closed-form solution, with the big bang placed at , is
and the time at which it reaches — the predicted age of the universe — is
All quantities are real; is the real power applied to , which is positive for .
The goal theorem asserts that the displayed is a positive solution of the flat matter-plus- Friedmann equation on , normalized by at the age given above:
The milestones build to this and then go beyond it, in increasing strength: the derivative with ; the Friedmann equation itself; the normalization ; the equivalent logarithmic age formula
the deceleration-to-acceleration transition, exactly when , together with the sign criterion ; the qualitative picture that is strictly increasing on and tends to as ; and finally the statement that the closed form, together with the density and the pressure , satisfies both Friedmann equations, i.e. assembles into an FRW universe in the sense of the platform's existing FRWUniverse definition.
The result. The closed form turns cosmological parameter statements into arithmetic. With , and it yields the standard age of roughly billion years, and the transition condition gives , i.e. . 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 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.
The obstruction is not conceptual but analytic. The scale factor is a real power of , so it is not differentiable by the polynomial-power rules: every derivative step goes through the real rpow API, needs positivity of on , and produces exponents that must be recombined by hand ( collapses to only after such a step). The Friedmann identity itself then rests on , which must be applied where . The age milestones require the explicit value of as a logarithm together with the flatness relation . The second-derivative milestones require differentiating the first-derivative formula again and tracking the sign of ; the naive route of computing deriv (deriv ·) symbolically without first establishing a HasDerivAt statement on a neighbourhood is the main trap.
Parameters are bundled in a structure carrying , , and ; radiation and curvature are absent by construction, and dark energy is a true cosmological constant (), not a general equation of state. Time is a real variable with the big bang at , and every statement about the solution is restricted to , where ; outside that range the real power of a non-positive base is a junk value and nothing is claimed. Powers , are real powers, while is a natural-number power. Derivatives are Mathlib's deriv/HasDerivAt; the Friedmann equation is stated in the source's ratio form rather than a cleared-denominator variant, and is part of the goal, so the statement cannot be satisfied by a degenerate . The hypotheses with are jointly satisfiable, so no statement is vacuous.
The final milestone reuses the published FRWUniverse structure (an FRW universe with Newton's constant , curvature , time domain , 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.
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.
Fix a natural number . The ambient space is represented in Lean as Fin d → ℝ: a point assigns a real coordinate to each of the indices. Let be any set of such points. Its convex hull, written in the book and convexHull ℝ A in Lean, is the smallest convex set containing . A convex combination is a finite weighted sum of points of whose real weights are nonnegative and total one. No finiteness, closedness, boundedness, convexity, or nonemptiness assumption is imposed on .
The witnesses in the target are indexed by Fin (d + 1), which has exactly elements, corresponding to the book's indices . Repeated points and zero weights are permitted. They allow a representation that uses fewer than distinct points to be written with the same fixed index type.
For every , find points and real numbers such that
The Lean goal is Grunbaum2003.caratheodory_convex_representation. It quantifies over every natural dimension, every set in that real coordinate space, and every point 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.
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 , 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.
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 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 , 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.
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 is empty, the hypothesis 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 changed ambient space, or fewer clauses would answer a different question.
source.pdf in the book record; SHA-256 070befaa8c47f043ef9da1df0705910480eb692f044d1843c9f048f3e61fecac.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 . 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 , the gravitational constant , the quantum of action (today ) and the Boltzmann constant . 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 . Textbooks and reference works state the resulting expressions , , , 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.
Fix four positive real numbers , , , — the numerical values of the four constants in some reference system of units (SI, say).
A unit system is a quadruple of positive reals: the size of the chosen unit of length, mass, time and temperature, measured in the reference system. Changing to divides every quantity by the appropriate product of . Concretely, a speed is divided by , a quantity of dimension (the dimension of ) by , an action by , and a heat capacity by .
Say that normalizes when each of the four constants has numerical value in , i.e. when
The Planck system is the quadruple
together with the identification of that unique solution as the Planck system above. The statement is asserted for arbitrary positive , so it does not depend on the SI values of the constants, and it fixes nothing beyond positivity.
The milestones record the standard relations among the Planck units: ; the reduced Compton wavelength of the Planck mass equals ; the Schwarzschild radius of the Planck mass equals ; 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 when every quantity is replaced by its ratio to the corresponding Planck unit; and normalizing in place of yields the rationalized Planck units.
The uniqueness statement is what licenses the everyday practice of "setting ": 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 , , 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 " 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 instead of , and it shows that the formalization does not secretly hard-code the Planck convention.
The obvious argument — "count dimensions, invert a exponent matrix" — proves uniqueness of
the exponents in a monomial ansatz , 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 and , reduce to with
, and cancel a positive factor . 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.
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 , density ) 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 , Hartree atomic units), and contributions extending it in that
direction are welcome.
A coupling constant is the number that fixes the strength of an interaction: it is the coefficient that multiplies the interaction term of a Lagrangian relative to its kinetic term, and in a perturbative treatment it is the parameter the expansion is organised in. The central structural fact about such a coupling in a quantum field theory is that it is not constant: once quantum corrections are resummed, the coupling depends on the energy scale at which the theory is probed. This scale dependence — the running of the coupling — is what distinguishes quantum electrodynamics, whose coupling grows with energy until perturbation theory breaks down (the Landau pole), from quantum chromodynamics, whose coupling decreases logarithmically at high energy (asymptotic freedom, Gross–Politzer–Wilczek, Nobel Prize in Physics 2004).
This mission formalizes the elementary mathematics behind those statements: the one-loop renormalization-group equation, its exact solution, and the two qualitatively different behaviours it produces depending on the sign of the one-loop coefficient. The source is the Wikipedia article Coupling constant (sections Beta functions, QED and the Landau pole, QCD and asymptotic freedom), which states these facts in prose and in the single displayed formula for the running QCD coupling.
Write for a single real coupling and for the logarithm of the energy scale. The beta function is defined by
and at one loop is a cubic monomial,
with a scheme- and theory-dependent real coefficient . Saying that runs at one loop on a set of scales means that is differentiable at every with .
For QCD the article records the one-loop form of the strong coupling directly in terms of the process energy and the QCD scale :
The goal theorem is the dichotomy governed by the sign of , for an initial condition at the reference scale :
i.e. : the coupling dies off logarithmically in the energy.
the flow cannot be continued up to the finite scale , which is the Landau pole of the one-loop approximation.
Both follow from the exact one-loop solution, which is itself a milestone:
The dichotomy above is the mathematical content of the two headline claims made about running couplings: that a positive one-loop coefficient drives the coupling to infinity at a finite energy, and that a negative one makes it vanish logarithmically at high energy. The milestones also isolate the statement that a vanishing beta function means the coupling does not run at all (scale invariance), and record the elementary analytic properties of the explicit QCD formula : it is strictly decreasing above , tends to as , and satisfies the one-loop flow equation .
Nothing here is open mathematics: these are exercises in the theory of a separable scalar ODE. What the mission produces is a machine-checked, reusable Lean development of the one-loop renormalization-group flow — a small piece of formalized physics infrastructure that later missions on renormalization or dimensional transmutation can import.
The only real subtlety is that the exact solution is obtained by differentiating , which requires knowing in advance that the solution never vanishes. Positivity is not assumed: it is a separate milestone, and must be derived from the initial condition together with the flow equation (if reached at a first time , the identity on forces to have a strictly positive limit). The Landau-pole statement is a non-existence claim and has no analytic content beyond this, but it does depend on the positivity step.
Scales are parametrised logarithmically: the independent variable is , the coupling is a function , and the flow hypothesis is imposed pointwise as a two-sided derivative at each point of the given set (at an endpoint of a closed interval this is slightly stronger than a one-sided derivative, which only strengthens the hypotheses of the positive results and weakens the non-existence claim — the Landau pole statement is therefore the conservative reading). No uniqueness or existence theory for ODEs is assumed; the statements quantify over arbitrary functions satisfying the flow equation. The QCD formula is taken with real arguments and no constraint tying or to a particular number of flavours; the numerical values quoted in the source (, MeV) are measurements and are deliberately not formalized.
Degenerate cases are visible in the statements rather than hidden: appears as its own milestone (constant coupling), and the value of for , where the logarithm is non-positive or zero, is never asserted.