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.
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?
The virial theorem relates the long-time average of the total kinetic energy of a bound system of particles to the average of the virial of the forces acting on them. It gives the average kinetic energy of systems too complicated to solve exactly, such as stars, planetary systems, galaxies and galaxy clusters. Fritz Zwicky used it to infer the existence of unseen matter, and it enters the derivation of the Chandrasekhar limit for white dwarfs. It does not depend on the notion of temperature and holds for systems that are not in thermal equilibrium.
Timeline (as recounted in the source article):
point particles move in . Particle has a constant mass , position , velocity and momentum ; the net force on it is . The kinetic energy is , the moment of inertia is , and
The time average over a duration is .
When forces come from pair potentials depending only on the distance , the force of on is , , and the total potential energy is . Power-law potentials are ; gravity is .
For a motion with , (continuous forces) that is bounded (positions and velocities bounded for ),
The theorem turns boundedness of a motion into a quantitative relation between averaged energies, without solving the equations of motion; with it gives for self-gravitating systems, the relation used for mass estimates of galaxy clusters. The result is classical and proved in the literature. This mission formalizes the standard derivation: the calculus identities for and , the pair-force algebra under Newton's third law, the gradient computation for distance potentials, and the averaging argument.
The mathematics is elementary; the work lies in the formal infrastructure: product rules for inner products of vector-valued trajectories, the gradient of in , re-indexing a double sum over ordered pairs into a sum over , and the fundamental theorem of calculus for with the required integrability. A tempting oversimplification is to assume that and converge individually; bounded motion does not guarantee this, so the targets are stated as limits of the combined expression.
Space is EuclideanSpace ℝ (Fin 3) and particles are indexed by Fin N. Trajectories are functions ; the equations of motion are hypotheses HasDerivAt (r k) (v k t) t and HasDerivAt (fun s => m k • v k s) (F k t) t. Masses are constant real numbers. Time averages are (interval integral). Pair forces are defined with Mathlib's gradient, with . Power-law coefficients may depend on the pair (symmetric), which contains the article's single constant . Real powers are Real.rpow; collision-freeness is assumed wherever pair distances enter. Boundedness is imposed only for . The hypotheses are satisfiable (for instance by a uniform circular two-body motion), so no target holds vacuously.
The Standard Model of particle physics does not explain the values of its dimensionless constants, nor does it require them to be constant in time. The proton-to-electron mass ratio is one such constant: it compares the scale of the strong interaction (which sets most of the proton mass) with the electroweak scale (which sets the electron mass). A measured change of over cosmic time would signal physics beyond the Standard Model, while a tight null result constrains models with additional scalar fields.
The standard test compares the frequencies of molecular transitions observed in distant galaxies with laboratory values. Different transitions respond differently to a change of , so a relative shift between them cannot be confused with the overall cosmological redshift.
Timeline. Optical studies of molecular hydrogen at redshifts reached (Malec et al. 2010; van Weerdenburg et al. 2011). Ammonia inversion lines, about 100 times more sensitive, moved the field to radio astronomy and gave constraints at the level toward the lensing galaxy of PKS 1830−211 at (Henkel et al. 2009; Kanekar 2011). Jansen et al. (2011) and Levshakov, Kozlov & Reimers (2011) pointed out that methanol transitions have sensitivity coefficients ranging from about to . Ellingsen et al. (2012) gave a first methanol limit from two lines. Bagdonaite et al. (Science, 2013) observed four methanol lines in PKS 1830−211 with the Effelsberg 100-m telescope and derived the limit at a look-back time of about 7 billion years.
A transition with frequency has sensitivity coefficient defined by
or, in infinitesimal form, . Pure rotational transitions have frequency inversely proportional to the reduced mass, hence to , so . Mixed torsion–rotation transitions of methanol have strongly enhanced coefficients (Table 1 of the paper: and ).
Each observed line is assigned a position , a velocity (km/s) on a common scale centred on redshift . If in the absorbing galaxy differs from the laboratory value by , the positions satisfy
up to a velocity offset common to all lines, where is the speed of light. Plotting against and fitting a straight line therefore gives .
The fit is a weighted least-squares fit with weights , where is the 1σ uncertainty of the -th position. With , , , , and , the slope, intercept and slope standard error are , and . The reduced chi-squared is .
The data (Table 1) are four lines: – (, ), – (, ), – (, ) and – (, ). Because A- and E-symmetry methanol behave as separate species that may be spatially segregated, the fiducial fit uses only the three E lines.
With the E-line estimate , its statistical error and the adopted systematic error ,
i.e. to the printed precision.
The result. The authors report the limit as statistically more constraining than previous radio-domain tests of a drifting . Because it uses a single molecular species, it is much less exposed to the main systematic of multi-species comparisons, namely that different molecules sit in different gas at slightly different velocities. The milestones record the internal evidence behind the choice of the fiducial fit: the poor four-line and the A–E velocity separation.
Formalizing it. The physical inputs (sensitivity coefficients, measured positions, the systematic budget) are taken as data. What the mission checks by machine is the chain from those data to the printed numbers: the definition of the sensitivity coefficient and its value for rotational lines, the correctness of the line-fit estimator, and the arithmetic of every reported fit, separation and error combination.
The numerical milestones are exact statements about explicit rational data, but they involve nested sums, quotients and square roots, so a certified proof requires careful interval bounds rather than floating-point evaluation. The paper's numbers are rounded from unrounded measurements: recomputing from the rounded Table 1 entries gives, for example, instead of , and instead of for the four-line fit. Tolerances therefore had to be chosen so that every statement is both faithful to the printed value and true for the tabulated data. The general recovery milestone requires showing that the normal equations are nondegenerate whenever the are not all equal.
Fin n. Velocities are in km/s and km/s.deriv.Reusable pieces: the weighted least-squares definitions and the exact-recovery lemma apply to any straight-line fit with known uncertainties.
In the paper that introduced the AdS/CFT correspondence (hep-th/9711200), Maldacena takes a stack of branes in string or M-theory, sends the string or Planck length to zero while holding the energies of the worldvolume theory fixed, and follows the supergravity solution of the branes through the same limit. The field theory on the branes decouples from the bulk, and the supergravity metric converges, after an overall rescaling, to a product of an anti-de Sitter space and a round sphere. The conjectured duality is between the worldvolume conformal field theory and string/M-theory on that product.
Section 2 of the paper treats D3-branes, whose limit is ; that case, together with the Appendix on Poincaré coordinates for anti-de Sitter space, is the subject of the separate mission Maldacena 1999: the near-horizon geometry of D3-branes is AdS5 × S5. This mission covers the next three cases in the paper:
In each case the paper states the ratio of the sphere radius to the anti-de Sitter "radius", and how both depend on the number of branes.
Anti-de Sitter space. For and , of radius is the hyperboloid
in flat (Appendix, eq. (A.1)). The Poincaré coordinates , with and , are given by , and (eq. (A.2)). In these coordinates the induced metric is
where . In Lean these objects are AdS, poincareEmbedding, ambientForm and minkowskiForm, taken from the published definition file Maldacena1999_Defs; the induced metric of a tangent vector is ambientForm applied to the Fréchet derivative of poincareEmbedding.
Brane metrics. Each brane solution has the form , with the Minkowski metric along the branes and the round metric of the unit -sphere:
The decoupling limits hold fixed (M5), (M2), and , and (D1–D5), while or . The Lean definitions m5Metric, m2Metric and d1d5Metric evaluate these metrics on a tangent vector , where is tangent at a point of the unit sphere and .
With written in terms of by the chain rule, the rescaled metrics converge to
for M5-branes; to
for M2-branes; and to
for the D1–D5 system.
The goal asserts that each limit equals the metric of (induced metric (A.3) plus a round sphere), with radii, in units of or :
These three limits are the geometric input for the paper's conjectures that the six-dimensional theory is dual to M-theory on , the M2-brane theory to M-theory on , and the two-dimensional theory of the D1–D5 system to IIB string theory on . The radii set the regime in which supergravity can be trusted (large , or large ). They also fix which anti-de Sitter isometry group appears (, , ); the paper matches it with the bosonic conformal group of the brane theory.
The paper derives these limits in a few lines each. To our knowledge they have not been formalized. The mission produces machine-checked statements and proofs of the three limits and of their identification with anti-de Sitter geometry, reusing the published Poincaré-coordinate results of the D3-brane mission.
The computation is elementary but full of exponents. Each case needs a change of radial variable, a fractional power of a harmonic function whose constant term is dropped in the limit, and a comparison of the coefficient of with the Poincaré form, which in the M5 and M2 cases requires a constant rescaling of . In Lean, the limits are one-sided limits of expressions built from real powers Real.rpow, and the goal requires a Fréchet-derivative computation on (available from the published theorem Maldacena1999.induced_metric_poincare).
All metrics are evaluated pointwise on tangent vectors; no manifold structure is used. The round sphere is the unit sphere in Euclidean and a tangent vector at is a with . The limits are taken along (resp. ) with , , , , and the tangent vector fixed. For the D1–D5 system only the six-dimensional metric (4.2) is formalized: the compact factor , whose volume is constant in the limit, is not modelled. In the goal the anti-de Sitter coordinate is the paper's up to a constant factor ( for M5, for M2, for D1–D5), so that the limit metric has exactly the form (A.3). All physical parameters are strictly positive. Fluxes, supersymmetry and the duality conjectures themselves are out of scope.
In 1997 Maldacena observed that the low-energy limit of a stack of coincident D3-branes in type IIB string theory can be described in two ways: as four-dimensional super-Yang–Mills theory living on the branes, and as supergravity (ultimately string theory) on the near-horizon geometry of the branes. The paper computes that this near-horizon geometry is five-dimensional anti-de Sitter space times a five-sphere, , with both factors of the same radius , in string units, and conjectures that the two descriptions are dual. This AdS/CFT correspondence became one of the most cited results in theoretical physics (Maldacena 1999; see also Gubser–Klebanov–Polyakov 1998, Witten 1998).
The duality itself is a physical conjecture with no complete mathematical formulation. What the paper does contain is a small body of exact geometric computations on which the conjecture rests: the decoupling limit of the D3-brane metric, the description of AdS as a hyperboloid with its symmetry, the Poincaré coordinates in which the limiting metric is written, and the ordinary differential equation expressing broken conformal invariance of a probe brane. This mission formalizes exactly those computations.
Fix . The ambient space has coordinates and flat metric . Anti-de Sitter space of radius is the hyperboloid (eq. (A.1))
Linear maps preserving form the group , which contains the conformal group of -dimensional Minkowski space.
The Poincaré coordinates (eq. (A.2)) are and for ; on the hyperboloid, , where . Written in reverse, this is a map .
The D3-brane metric (eq. (2.2)) for string coupling , branes and string scale is
where are the worldvolume coordinates and is the round metric of the unit five-sphere. The decoupling limit (eq. (2.1)) sends keeping fixed.
For , , with , and every tangent vector with tangent to ,
which is eq. (2.3): the metric of in Poincaré coordinates plus the round metric of of the same radius.
The goal is the precise sense in which "the near-horizon geometry of D3-branes is with ": the radius formula is what later links the 't Hooft coupling of the gauge theory to the curvature of the string background, and the Poincaré-patch form (A.3) is the coordinate system in which essentially all subsequent AdS/CFT computations are carried out. Milestones 1–4 give a reusable, self-contained account of anti-de Sitter space as a quadric in with its Poincaré chart, useful to any development of Lorentzian geometry. Milestone 6 is the step by which the paper argues that the probe D3-brane action (2.6) is fixed by conformal symmetry.
All of these statements are standard computations in the physics literature; none is open. The value of the mission is a machine-checked version of the geometric content of the paper, stated with the paper's own conventions, not a new result. The duality conjecture itself is outside the scope of the mission.
The computations are elementary but bookkeeping-heavy. The induced-metric identity (A.3) requires differentiating a map from to with arbitrary, so sums over the index sets must be split into the timelike, spacelike and light-cone components; a computation for one fixed does not suffice. The bijection statement needs an explicit inverse and the observation that the hyperboloid equation determines from and . The limit statements require controlling square roots of expressions that blow up like . The ODE characterisation requires a uniqueness argument on an interval, not only verification that the stated function is a solution.
Coordinates of are indexed by with index for , index for and index for ; worldvolume coordinates are indexed by with index timelike. Metrics are represented by the quadratic forms they induce on tangent vectors; the induced metric is expressed through the Fréchet derivative of . The round metric of is the Euclidean norm squared of a tangent vector of the unit sphere in . Square roots and divisions are Lean's total functions; all statements restrict to , , , , , where no junk values arise. The symmetry milestone is stated for the full group , which contains the named in the paper.
No new infrastructure beyond Mathlib's calculus, real analysis and matrix libraries is needed. Contributions of general lemmas about quadrics in pseudo-Euclidean spaces are welcome.
Projective measurement is usually taught together with state update: an observable is measured, a value is obtained, and the conditional state is assigned. These are two different questions. The first is the prediction of the outgoing ensemble from the incoming ensemble and the measured observable alone, before the outcome is known; the second is the incorporation of the outcome once it is known. The technical brief by G. Carcassi for the Assumptions of Physics collaboration (AoP technical briefs) isolates the first question and treats the measurement as a black-box process that only relates incoming and outgoing ensembles, without committing to a mechanism.
Within this view the standard prediction, the nonselective (Lüders) post-measurement ensemble, admits several characterizations that come from different traditions: the algebraic pinching map, the long-time limit of a dephasing Lindblad equation (open quantum systems, see Lindblad 1976), and a closest-point principle, either in Hilbert–Schmidt distance or in quantum relative entropy (Umegaki 1962). The brief's Theorem 1 states that these characterizations select the same process.
Fix a finite index set ; the Hilbert space is and operators are complex matrices. A density matrix is a positive semidefinite matrix with . An observable is a Hermitian matrix with spectral decomposition
where ranges over the distinct eigenvalues of and is the orthogonal projection onto the -eigenspace.
The spectral equilibration process is an unknown map on density matrices. The brief's four conditions on it are:
For every Hermitian and every map ,
The milestones follow the steps of the brief's proof: the block decomposition (eq. 2); the blockwise solution (eqs. 4–5); convergence (eqs. 9–10) and EQ-LIND EQ-MEAS; the equivalence ; preserves density matrices; the Pythagorean identity (eq. 11) and EQ-HS EQ-MEAS; the relative-entropy chain rule (eq. 12); (eq. 13); non-negativity and definiteness of ; and EQ-KL EQ-MEAS.
The result says that "projective measurement" can be specified without reference to wave-function collapse: any of the three dynamical or variational descriptions pins down the same input–output map. Downstream, this justifies treating repeatable measurements as equilibration processes whose outputs are fixed points, and treating the outcome-update step as classical conditioning on a mixture.
The mathematics in finite dimension is classical; this mission asks for a machine-checked proof of the equivalence in Lean 4 with Mathlib. A complete development produces reusable pieces: spectral projections and the pinching map for Hermitian matrices, explicit solutions and asymptotics of a dephasing Lindblad semigroup, and an extended-real relative entropy with Klein's inequality.
The Hilbert–Schmidt part is linear algebra once block-diagonality is in place. The Lindblad part requires uniqueness of solutions of a linear matrix ODE on the closed half-line, to transfer the explicit blockwise formula to an arbitrary solution. The relative-entropy part is the most delicate: it needs the interaction between the functional-calculus logarithm and block structure ( is block diagonal when commutes with ), the support conventions that make take the value , and Klein's inequality with its equality case for matrices, which the development must supply if the library does not already provide it.
Real.log (so , i.e. the logarithm on the support); takes values in the extended reals and equals unless .Contributions of general-purpose lemmas (Klein's inequality, uniqueness for linear ODEs on half-lines, properties of pinching) are welcome as separate theorems.
In 1948 R. P. Feynman published a third formulation of non-relativistic quantum mechanics, alongside Schrödinger's differential equation and Heisenberg's matrix algebra (Feynman 1948). The probability amplitude for a particle to follow a path is postulated to be , with the classical action, and the amplitude to arrive at is the sum of these contributions over all paths from the past. This is the path integral, now a standard tool across quantum field theory, statistical mechanics and probability.
The formulation is claimed to be mathematically equivalent to ordinary quantum mechanics. The key step of that claim is Section 6 of the paper, "The wave equation": the wave function defined by the path integral satisfies Schrödinger's equation. This mission formalizes that step for a particle in one dimension, as the paper does.
Timeline:
Fix , a mass and a potential . For a time step the short-time action between positions (time ) and (time ) is (Eq. 22)
and the normalizing factor is (Eq. 28, principal branch). The one-step path-integral evolution (Eqs. 18, 23) takes a wave function to
Iterating and letting is the path integral (15) of Section 5. The Hamiltonian is . The paper also uses the Gaussian moments of Eq. (26), which are oscillatory; footnote 13 defines them by replacing with and letting :
For every Schwartz function and every ,
that is, for the path-integral evolution, which is Schrödinger's equation (30). This is the content of Feynman's statement that (18), valid to first order in , yields (30).
The goal is the step that connects the path-integral postulates to the ordinary formulation: without it the formulation of Sections 3–5 is not known to reproduce any quantum mechanics. The Fresnel integrals of (26) and the short-time kernel appear throughout semiclassical analysis and in every derivation of path integrals from the Schrödinger equation.
The physics result is classical and its rigorous versions are known (via the Trotter product formula or oscillatory-integral estimates). The work here is the formalization: Mathlib has the complex Gaussian integral and Schwartz functions, but not Fresnel integrals, the free Schrödinger kernel, or the short-time asymptotics of oscillatory integrals. None of the targets is currently formalized on the platform.
Feynman's derivation expands in a Taylor series under the integral and integrates term by term against . Those integrals are not absolutely convergent, and the higher moments do not even exist as improper Riemann integrals, so the term-by-term step is not justified as written. A proof has to control the Taylor remainder against an oscillatory kernel whose width is of order , uniformly as , with a prefactor that blows up like . The naive dominated-convergence argument does not apply, because the kernel has modulus everywhere and does not concentrate in absolute value.
𝓢(ℝ, ℂ), which formalizes the paper's "relatively smooth" that "falls off sufficiently for large ". For such the integral defining is absolutely convergent, so the Lebesgue (Bochner) integral is used.Useful infrastructure: Fresnel integrals, Fourier representation of the free Schrödinger kernel on Schwartz space, and differentiation of oscillatory integrals with a parameter. All are reusable beyond this mission.
A coincident pair of a D-brane and an anti-D-brane in type II string theory carries an open-string tachyon, a mode of negative mass squared. In Sen, hep-th/9805019 it was conjectured that at the minimum of the tachyon potential the negative potential energy exactly cancels the sum of the tensions of the brane and the anti-brane, so that the system decays to a configuration of zero energy density, i.e. the supersymmetric vacuum. The paper formalized here, A. Sen, Tachyon condensation on the brane antibrane system, JHEP 08 (1998) 012, gives a short argument for this, and the author says explicitly that it is not a rigorous mathematical proof. The argument follows Gava–Narain–Sarmadi, hep-th/9704006 and belongs to the programme of tachyon condensation. Later work, starting with open string field theory computations, tested the same conjecture numerically.
Work in string units (). Wrap a D2-brane and an anti-D2-brane on a torus with radii and area . Each brane carries one unit of magnetic flux, , with signs chosen so that each carries unit of D0-brane charge. T-duality on both circles gives a dual torus with radii and coupling . On the dual torus the system is described by a gauge theory: a gauge field is a pair of complex-matrix-valued functions of , with field strength . The gauge transform by a matrix-valued is . The background configuration is
subject to twisted boundary conditions with transition functions and . A D-brane with coupling has tension .
With the mass at the classical minimum (two D2-branes with zero field strength on the dual torus, re-expressed through ), for each fixed :
The vanishing of the energy at the tachyon minimum is the basis for identifying stable non-BPS D-branes as tachyonic solitons on brane–antibrane pairs, as discussed at the end of the paper, and it was a starting point for later work on tachyon condensation. The paper's argument is heuristic. This mission makes explicit which steps are mathematics (the gauge-theoretic facts (4)–(8), the gauge covariance used on p. 3, and the algebra (9)–(11) and its limit) and machine-checks them. The physical inputs (the BPS argument that the mass (9) persists as parameters vary, and the identification of the minimum-energy configuration) are recorded as modelling assumptions in the definitions, not proved.
The algebraic milestones (9)–(11) and the limits are elementary. The substantive formal work is in the gauge-theory milestones: computing derivatives of the matrix exponential in (5), the smooth homotopy with flat ends required by (8) (existence rests on the simple connectivity of , but the statement asks for an explicit smooth -valued map with prescribed boundary values and vanishing normal derivative), and the covariance computation of the field strength under a non-unitary, merely invertible .
Coordinates are ; the paper's index is Fin 2 (, ). Matrices are Matrix (Fin 2) (Fin 2) ℂ; partial derivatives are taken entrywise; the inverse is the Mathlib matrix inverse; the exponential is NormedSpace.exp. Radii and couplings are real, with positivity assumed wherever the paper's quantities are physical. The goal cannot be trivialized by division by zero, because it is a statement about the limit of large positive radii. All definitions live in a single definition file under the namespace SenTachyon.
In the 1993 essay Dimensional Reduction in Quantum Gravity (arXiv:gr-qc/9310026), G. 't Hooft argued that, once gravitational collapse is taken into account, the number of quantum states available to a region of space grows with the area of its boundary rather than with its volume. The essay is the origin of what is now called the holographic principle (developed further by Susskind, arXiv:hep-th/9409089). Besides the physical counting argument, the essay contains a small, fully precise mathematical model: a cellular automaton on the cubic lattice whose data on a one-dimensional line determine the data everywhere. This mission formalizes the quantitative estimates and the automaton statements of the essay.
Entropy estimates (eqs. (4)–(11)). In natural units, a region bounded by a sphere of radius has volume and area . A thermal gas of particle species at temperature has energy and entropy with positive constants . It stays outside its own Schwarzschild radius if . A black hole of mass has entropy (eq. (1), additive constant dropped).
Plaquette automaton (eqs. (12)–(19)). Data live on lattice sites. An elementary plaquette has lowest corner and is spanned by two of the unit vectors ; its corners in cyclic order are . On every plaquette a relation is imposed such that any three entries determine the fourth uniquely. The relations may differ from plaquette to plaquette. On the unit cube with corners , , , , , , , , the six face relations are (12a–f). The staircase (eq. (14)) is the sequence
A family of face relations is consistent (eq. (16)) if every choice of extends to data on the cube satisfying all six relations; equivalently, the three values of produced by (12b), (12d), (12f) agree. Linear relations (eq. (17)) have the form , with every invertible mod .
For any family of plaquette relations with the three-determine-the-fourth property, two solutions on that agree on the staircase agree everywhere:
The goal is the essay's concrete mathematical example of dimensional reduction: in a -dimensional lattice model, a one-dimensional set of data carries all the information. Milestone 5 shows that the reduction is sharp in the linear case: no data beyond the staircase are needed, and none of the staircase data are constrained. Milestones 1–2 are the scaling estimates behind the area law . The physical argument around them (black-hole thermodynamics, the Schwarzschild criterion) is taken as modelling input, not formalized. The results are stated in the essay but, as far as is known, have not been machine-checked.
The local step (one cube, Milestone 3) is elementary. The goal needs a global propagation argument. The staircase is a thin zig-zag line, and each application of a plaquette relation fixes only one new site. So the proof has to show that repeated local determination starting from the line eventually reaches every site of , in both directions along the line and in both transverse directions. Layer-by-layer propagation in does not apply directly, because the staircase is not a full layer.
Sites are ℤ × ℤ × ℤ. Data take values in ZMod p for an arbitrary natural number ; the uniqueness statements hold for every . The three-determine-the-fourth property is stated with unique existence () for each slot, which matches "uniquely determined" in the essay. Relations may depend on the plaquette, so no translation invariance is assumed. Consistency (16) is encoded as extendability of the four free values on the unit cube. In Milestones 1–2 the region is a round sphere of radius , so and are expressions in , and the constants are existentially quantified before all physical variables. Contributions welcome: proofs of each milestone, and further faithful statements from the triangular-lattice model (eqs. (20a–f)).
Neutrinos produced by weak interactions are created in flavour eigenstates (, , ), while they propagate as mass eigenstates. When the two bases differ, the flavour content of a neutrino beam oscillates with distance. In ordinary matter this picture is modified: electron neutrinos scatter coherently forward on electrons via the charged current, which adds an extra potential energy to the component only (Wolfenstein 1978). Mikheyev and Smirnov observed that this potential can resonantly enhance the mixing, so that an almost complete flavour conversion is possible even for a tiny vacuum mixing angle — the MSW effect. It is the accepted explanation of the energy dependence of the solar deficit and is relevant for neutrinos crossing the Earth and for supernova neutrinos.
This mission formalizes the constant-density result of Section 8.2 of E. Kh. Akhmedov's lecture notes Neutrino physics (hep-ph/0001264): the two-flavour transition probability in matter of constant density, eq. (95), together with the statements that lead to it and follow from it, eqs. (91)–(98).
Fix the vacuum parameters: the mass-squared difference , the neutrino energy , and the vacuum mixing angle . The matter is described by the Fermi constant and the electron number density , through the charged-current potential (eq. (87))
Write . After discarding all terms proportional to the identity (common phases), the vector of flavour amplitudes evolves by the Schrödinger equation with the real symmetric MSW Hamiltonian (eq. (91))
The derived quantities are the energy gap in matter (eq. (94)), the oscillation length in matter (eq. (96)) and the oscillation amplitude in matter (eq. (97)):
The vacuum oscillation length is (eq. (61)). Distance and time are identified (, units with ).
If solves for all with (a pure is produced at ), then for every
Eq. (95) shows that at constant density the flavour transition has exactly the vacuum form with replaced by ; together with the resonance condition (98) it underlies quantitative discussions of matter effects, from the solar neutrino problem to long-baseline experiments crossing the Earth. The milestones separate the linear-algebra content (diagonalizing a real symmetric matrix) from the analytic content (solving a linear constant-coefficient ODE and the uniqueness of its solution).
The result is textbook material and is proved in the source. This mission adds a machine-checked derivation from the Schrödinger equation itself — including uniqueness of the solution of the initial-value problem, which the source leaves implicit — and reusable Lean definitions for later missions on the adiabatic (variable-density) regime of Section 8.3.
The algebra of eqs. (93)–(97) is elementary. The substantive step for a formal proof is the passage from "the Hamiltonian is diagonalized by a rotation" to "every solution of the ODE with the given initial datum has the stated component": this needs a uniqueness theorem for linear ODEs on (or an equivalent argument). Degenerate parameter values (, ) must be handled, since the Lean statements do not exclude them.
All parameters are real numbers; the state is a function (index , ) assumed differentiable everywhere with derivative , where is the real matrix above viewed as a complex matrix. The probability is the squared modulus . is assumed throughout; the sign of , the value of and the density are unrestricted. Lean's division convention () applies to and when ; in that degenerate case is a multiple of the identity and both sides of the goal are .
A statement that assumed the closed-form solution, or assumed the probability formula as a hypothesis, would be trivial; the goal instead quantifies over every solution of the initial-value problem. Proofs of any milestone, and reusable lemmas on uniqueness for linear constant-coefficient ODEs, are welcome.
Leptogenesis is a class of scenarios in which the baryon asymmetry of the Universe is produced from a lepton asymmetry generated in the out-of-equilibrium decays of heavy singlet neutrinos , which also give the light neutrinos their small masses through the type I seesaw (Fukugita–Yanagida 1986). The review of Davidson, Nardi and Nir (Phys. Rep. 466 (2008) 105) collects the standard results of the field. One of its central quantitative facts is an upper bound on the CP asymmetry in the decays of the lightest singlet , in terms of and the light-neutrino masses. This bound is the origin of the familiar lower bound GeV for thermal leptogenesis with hierarchical singlets (Eq. (5.12) of the review).
Timeline. Casas and Ibarra introduced the orthogonal-matrix parametrization of the seesaw in 2001 (hep-ph/0103065). Davidson and Ibarra derived the bound on the total asymmetry in 2002 (hep-ph/0202239); Hamaguchi, Murayama and Yanagida gave a related bound (hep-ph/0109030). Once flavour effects were recognised (around 2006), attention moved to the flavoured asymmetries , whose bound (Eq. (5.10) of the review) is the goal of this mission.
There are three lepton flavours and three singlets with Majorana masses . We work in the mass basis of the charged leptons and of the . The Yukawa matrix is an arbitrary complex matrix, and is the Higgs vev. The light-neutrino mass matrix (Eq. (2.5)) is
a complex symmetric matrix. It is diagonalized as with unitary and , (Eq. (2.6)). The largest and smallest light masses are and . The Casas–Ibarra matrix is (Eq. (2.11)).
At tree level decays into and with partial rate and total rate (Eq. (4.5)). So the branching fractions satisfy . For hierarchical singlets the flavoured CP asymmetry is (Eq. (5.9))
Eq. (5.10) is the input to the lower bounds on and on the reheat temperature for hierarchical thermal leptogenesis (Eq. (5.12), Sec. 9.4.3), and it shows that flavoured asymmetries are not suppressed for degenerate light neutrinos, unlike the total one (Eq. (5.17)). These are established results. The work here is to formalize them: to state the seesaw quantities precisely and machine-check the linear-algebra steps (Takagi factorization, complex orthogonality, operator-norm bounds) that the physics literature takes for granted. To the captain's knowledge none of these statements has a machine-checked proof.
The goal reduces to an operator-norm estimate for the complex symmetric matrix . That estimate needs the diagonalization , which is a Takagi (Autonne–Takagi) factorization, not a unitary eigen-decomposition: is symmetric, not Hermitian. The obvious move, applying the spectral theorem to , fails because is in general not normal. The milestone-1 existence statement therefore needs its own argument, for example through the Hermitian matrix . The total-asymmetry bound (milestone 4) needs a finer argument than the triangle inequality to produce the difference rather than .
Fin 3); the singlet "" is index .⨆ i, masses i and ⨅ i, masses i over the three diagonal entries. No ordering of the is imposed.IsLightMassDiagonalization m U masses (unitary , , ). It is always satisfiable by milestone 1, so it is not vacuous.In the note Reformulating String Theory with the 1/N Expansion (arXiv:hep-th/9405069), C. B. Thorn argues that stability and causality, which are manifest in quantum field theory but obscure in string theory, would become evident if strings were composite objects built from point-like constituents ("string bits"). The proposal combines the light-cone parametrization of the string with 't Hooft's expansion (G. 't Hooft, Nucl. Phys. B72 (1974) 461): bits are created by the entries of an matrix field , closed strings by the singlet traces , and plays the role of the string coupling.
A load-bearing step of the proposal is that a long closed chain of bits behaves like a continuous string: in the continuum limit with fixed, the finite-energy excitations must be string excitations. Thorn justifies this with the remark (p. 5) that "the low energy excitations of an particle discretized string are the two-body level spacing". This mission formalizes that remark for the harmonic Hamiltonian written in the paper, together with the cyclic symmetry that ties the matrix traces to closed strings.
A discretized light-cone string with bits is described by transverse positions with cyclic identification and Hamiltonian (p. 4)
The potential term is the quadratic form of the cyclic Laplacian , (indices mod ), and the equations of motion are . A normal-mode frequency is an with an eigenvalue of ; write for the set of them. With these are the excitation-level spacings of the chain.
The singlet creation operators are ; since the commute with each other, cyclic invariance of the trace gives the cyclic symmetry of the string wave function.
For all and ,
The goal is the quantitative content of the paper's continuum-limit argument in the harmonic case: the gap of an -bit chain closes like relative to the two-body scale, so at fixed the low-lying spectrum approaches the equally spaced string spectrum. The same spectral facts about the cyclic Laplacian (the spectrum of the cycle graph) are used in lattice field theory and spectral graph theory, so the milestones are reusable outside this mission. The results are classical; the work here is their machine-checked formalization in a form tied to the string-bit Hamiltonian.
The trace and quadratic-form statements are finite algebra. The substance lies in the spectrum: exhibiting real eigenvectors for every needs trigonometric sum identities, and the completeness statement needs an argument that no other eigenvalues exist, which must handle the degenerate pairs . Identifying the least positive value then requires the symmetry and monotonicity of on .
String/M theory appears to admit a very large number of four-dimensional vacua, and M. R. Douglas's 2003 paper The statistics of string/M theory vacua proposes to study them statistically: instead of constructing vacua one at a time, one places a measure on a space of effective theories and computes expected numbers and distributions of vacua. Two concrete mathematical ingredients of that programme are the subject of this mission.
The first is the Bousso–Polchinski counting of flux vacua (Section 3.6 of the paper, following Bousso–Polchinski 2000). Quantized fluxes form an integer vector , and the flux energy is a positive quadratic form in . The number of flux choices with energy below controls whether a small cosmological constant can be realised; the paper evaluates the number distribution (3.13) by replacing the lattice sum with an integral, obtaining a density proportional to .
The second is the Gaussian ensemble of superpotentials (Section 4 and 4.1): a random polynomial superpotential whose coefficients are independent complex Gaussians, with an explicit normalising constant and an explicit count of coefficients.
Fix an integer (the number of independent flux quanta, in the paper) and a constant (in the paper ). For a flux vector the flux potential is
and the flux vacua count below level is
This is the cumulative distribution function of the measure of eq. (3.13). The unit ball in has volume , and the unit sphere has area .
For the superpotential ensemble, a polynomial in variables of degree at most has one coefficient per monomial with ; the paper states there are of them. The coefficients are given the weight , , which the paper says is unit normalised.
This is the precise, integrated form of the approximation in (3.13): integrating from to gives exactly .
The goal makes rigorous the step "replace the sum with an integral" that underlies the Bousso–Polchinski estimate of how many flux vacua lie below a given energy, with the exact constant appearing in (3.13). Milestones 4 and 5 certify the combinatorial and analytic constants of the Gaussian ensemble (4.6) on which the paper's densities (4.7)–(4.10) are built. None of these results is new mathematics: the goal is the -dimensional analogue of the Gauss circle problem at leading order, and the milestones are classical. What the mission adds is a machine-checked version of the precise constants used in the paper.
The goal requires comparing a lattice-point count with a volume. The naive bound, counting unit cubes centred at lattice points, must be controlled uniformly: cubes meeting the boundary of the ball contribute an error of order with , and one has to show that this is . The volume formula for Euclidean balls expressed through the Gamma function, and its transport to the product space with the sum-of-squares form, is further required infrastructure.
Fin J → ℤ; the count uses Set.ncard, whose value on an infinite set would be — milestone 1 rules out that degenerate reading.Fin J → ℝ (not EuclideanSpace), with the quadratic form written out explicitly.DouglasVacua.fluxPotential, DouglasVacua.fluxVacuaCount.Gambini and Pullin (IJMPD 23 (2014) 1442023) study quantum fields living on the discrete quantum spacetimes of spherically symmetric loop quantum gravity. Discreteness makes the field equations lattice-like and hence breaks Lorentz invariance. Collins, Perez, Sudarsky, Urrutia and Vucetich (PRL 93 (2004) 191301) argued that in interacting theories such Planck-scale violations feed, through renormalized loop diagrams, into large low-energy violations: a difference of second derivatives of the self-energy that should vanish by Lorentz invariance stays bounded away from zero. Gambini and Pullin argue that two exponential weights — a Gaussian fuzziness factor from the spread of the ADM mass, and a Lorentz-invariant nonlocal interaction factor of the type found in string field theory — make this quantity arbitrarily small.
Because the full self-energy calculation is lengthy, the paper's Appendix A replaces it by a two-dimensional model integral in which rotations play the role of Lorentz transformations and a parameter plays the role of lattice spacing. This mission formalizes the precise mathematical claims made about that model.
For real parameters define the denominator base and the model integrand
The paper's integral (A.1) is . For one has , which is rotation invariant.
(A.1) is only a formal expression: is not Lebesgue integrable on (for it decays like ; for it grows like along the -axis). The mission therefore uses the disk-truncated integral
which regularizes (A.1) in a rotation-invariant way.
The weighted model integral (A.2) is, for weights ,
The first factor models the fuzziness (it acts on one direction only), and the second models the nonlocal interaction (rotation invariant here, Lorentz invariant in the physical case).
"With suitable choices of and one can make the integral as small as desired":
In the paper this model is the only precisely stated mathematical content backing the claim that the two exponential weights restore approximate Lorentz invariance. Formalizing it pins down exactly which statements hold (and in what sense the formal integral (A.1) "vanishes" or "does not vanish"), separating the rigorous content of the toy model from the physical argument it illustrates. The results are elementary real analysis; no machine-checked proofs of them are known to exist.
The main difficulty is that the unweighted integral (A.1) diverges, so both "vanishes" and "does not vanish" need a regularization. The weighted statements need integrability and dominated-convergence estimates on and a change of variables (swapping and ) for the symmetry claims. The divergence to in milestone 2 needs separate upper and lower estimates for the positive and negative parts of on growing disks.
All objects are real-valued functions on with Lebesgue (product) measure. is a Bochner integral over the whole plane; where the integrand is not integrable, the Lean integral is by convention, which is why milestone 3 is included and all weighted statements assume . The disk is the closed Euclidean disk , not a sup-norm ball. The parameter is restricted to (or ) wherever it matters, so that . The sentence in the paper "more precisely one needs and both larger than " is heuristic; only its sufficiency direction along is formalized (milestone 5). No necessity claim is formalized, because a large alone already makes small.
Kernel methods, multidimensional scaling and low-distortion embeddings all work best on data whose distance comes from a Hilbert space. A distance on a set is Hilbertian when can be mapped into a Hilbert space so that becomes the norm distance; for such a , the kernel is positive definite for and (Berg, Christensen and Ressel, 1984), and the classical Euclidean toolbox applies. Optimal transport distances are popular for comparing probability measures, so it is natural to ask whether they are Hilbertian. In dimension one the answer is yes for : the map sending a measure to its quantile function is an isometry into , and between univariate Gaussians is the Euclidean distance between (mean, standard deviation). Peyré and Cuturi, Computational Optimal Transport (FnT ML 2019), §8.3, show that this does not extend to the plane: for and the -Wasserstein distance on is not Hilbertian (Proposition 8.2, p. 507).
The tool is a classical characterization. Schoenberg (1938) proved that a distance is Hilbertian exactly when its square is conditionally negative definite; Berg, Christensen and Ressel (1984, Prop. 3.2) give the modern form. The easy direction turns non-embeddability into a finite check, and the book's proof of Proposition 8.2 performs that check numerically on 35 measures supported on the four corners of the unit square (Figure 8.6, p. 508). Stronger, quantitative statements are known: planar does not even embed into with bounded distortion (Naor and Schechtman, 2007), and Andoni, Naor and Neiman (2018) study which powers of Wasserstein distances embed.
Let be a set. A function is negative definite (Definition 8.3, p. 501, in the conditional form used in §8.3) if it is symmetric and, for every , every and every with ,
A function is Hilbertian (Definition 8.4, p. 506) if there are a real Hilbert space and a map with for all .
On with the Euclidean norm , let be the Borel probability measures with . A coupling of and is a measure on whose two marginals are and , and the -Wasserstein distance (2.18) is
finite on . For points and a histogram (nonnegative, summing to one) the discrete measure is ; for two histograms , is the set of nonnegative matrices with row sums and column sums , and (2.11).
The configuration of the book's proof consists of the corners , , , of the unit square, the 35 histograms of with entries in , and the centering matrix .
For and ,
A Hilbertian distance gives positive definite Gaussian and Laplace kernels, Euclidean multidimensional scaling and Johnson–Lindenstrauss dimension reduction for free. Proposition 8.2 says none of these can be obtained for or on , , by an isometric embedding; this is why the literature turned to approximate embeddings, sliced distances and entropic surrogates (pp. 507–508). The negative-definiteness test of milestone 1 is a reusable certificate for non-embeddability of any finite metric.
The result is known, and the book's proof is a floating-point eigenvalue computation. The formal content of this mission is a machine-checked proof with an exact certificate: rational or algebraic Wasserstein distances between explicit discrete measures and an explicit zero-sum vector. As far as this mission is aware, no formal proof of the statement exists in Mathlib or on the platform. Schoenberg's converse is cited by the book and is not part of the mission.
The abstract part is short: expanding and using gives milestone 1. The obstacle is the certificate. The book observes that has a positive top eigenvalue (about for and for ), but a proof needs exact transport costs between the chosen measures, each the value of a small linear program whose optimality has to be established (for instance by a dual certificate), together with a vector for which the quadratic form is provably positive. For the costs involve , the diagonal of the square. A second, separate difficulty is connecting the measure-theoretic to the discrete program (milestone 4) and transporting a counterexample from into (milestone 3), both of which require working with couplings as measures on a product space.
EuclideanSpace ℝ (Fin d); is the published definition WassersteinDRO.Duality.wassersteinDistance (an -valued infimum over all measures with the two marginals, raised to ), converted to a real number. The distance is considered on , the set where it is finite; outside it the real conversion is a junk . The book names no domain; since the counterexample consists of finitely supported measures, the finite computation gives non-Hilbertianity on and on every smaller set containing those measures.Fin n). Histograms are real vectors; the reduction milestone is stated for every .CompOT.NotHilbertian, duplicating chunk II of the series.Contributions welcome: the forward direction of Schoenberg's characterization, the discrete-measure bridge (reusable wherever discrete optimal transport meets measure-theoretic couplings), the isometric-embedding invariance of , and exact certificates for the grid computation.
Best subset selection with a ridge term, the -regularized least squares problem
is a standard model for sparse linear regression. It can be solved to certified optimality by branch-and-bound (BnB) over a mixed integer formulation, and the speed of BnB depends on how tight the lower bounds of its node relaxations are. Two mixed integer formulations are in common use: the Big-M formulation, which links each coefficient to a binary indicator through a box (Bertsimas, King and Mazumder, 2016), and the perspective formulation, which replaces by an auxiliary variable constrained by a rotated second-order cone (Frangioni and Gentile, 2006; Günlük and Linderoth, 2010). Which formulation gives the stronger continuous relaxation decides which one a solver should be built on.
Hazimeh, Mazumder and Saab (2021) compare the relaxations in Section 2. Their Proposition 2 compares the interval relaxation of the Big-M formulation with that of the perspective formulation without a box, , studied by Dong, Chen and Linderoth (2015). This mission formalizes that comparison.
Fix a design matrix , a response , parameters and a bound . Write and for for every .
The Big-M formulation (2) is
Its interval relaxation replaces by ; its optimal value is . Eliminating gives the equivalent form (37),
The reverse Huber penalty is for and for , and . The interval relaxation of has the value (6),
Let be the set of minimizers of , and, as in (9),
The comparison runs through the scalar function and through .
The mission also contains the scalar inequality (39) as a supporting statement (not a milestone): for and , .
Proposition 2 says that neither relaxation dominates the other. For a tight Big-M bound the Big-M relaxation yields the larger lower bound; for a loose one, provided some optimal solution of lies in the box, the perspective relaxation does. Equivalently, with the other data fixed, a small favours the Big-M relaxation and a large favours (p. 8). Together with Proposition 1 of the same paper, which shows that the box-constrained perspective relaxation beats both when , this motivates the paper's choice of as the formulation on which its BnB solver is built.
The proposition is proved in the paper (Appendix A, pp. 29–30). No machine-checked proof of it, of the reformulation (37), or of any property of the reverse Huber penalty exists on the platform. The mission produces a formal statement of both inequalities with every hypothesis explicit, and the definitions of the two relaxation values in a form that later missions on perspective relaxations can reuse.
The scalar inequalities (39) and Lemma 1 are elementary but split into cases at the kink of the reverse Huber penalty, , and at the sign of . The passage from coordinatewise inequalities to optimal values is where care is needed. is defined over pairs , and its identification with a minimum of over a compact box requires eliminating and showing attainment. For (11) a pointwise comparison of and on the box only bounds by the box-restricted value , not by , which is an infimum over all of ; the hypothesis is what closes this gap, and dropping it gives a statement the paper does not prove.
All declarations live in the namespace L0BnB.BigMvsPR. Vectors are Fin p → ℝ, is a Matrix (Fin n) (Fin p) ℝ, and is X *ᵥ β. Every norm is an explicit sum: , and is . The reverse Huber penalty is an if on .
Optimal values are real infima (sInf): over the feasible pairs of the interval relaxation, over all of , over the box. For each set of values is nonempty () and bounded below by , so no infimum takes Lean's junk value. is defined as the displayed minimum (6); its identification with the interval relaxation of is a result of Dong, Chen and Linderoth that the paper cites and does not prove, and it is not part of this mission. is the set of minimizers of , as the paper uses it in the proof of (11).
All theorems assume . The paper remarks that Proposition 2 applies for any ; is excluded because and divide by . The goal is stated for optimal values, not for the objective functions at a single point: a pointwise comparison of and is a milestone, not the proposition. Milestone (37) is stated with IsLeast, so it asserts attainment as well as the value.
The paper states no bounds in this result, so no constants are instantiated. Contributions welcome: proofs of the scalar lemmas, of (37) (which needs compactness of the box and continuity of ), and of the goal.
Scattered subspaces are a central object of finite geometry. An -subspace of an -dimensional vector space over defines an -linear set of the projective space , and when is scattered this linear set has the largest possible number of points for its rank. Maximum scattered subspaces give rise to maximum rank distance (MRD) codes, to translation caps, and to two-intersection sets and the associated two-weight codes and strongly regular graphs (Polverino 2010; Sheekey–Van de Voorde 2020).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590v2, Combinatorica 41, 2021) generalised the notion to -scattered subspaces, which meet every -dimensional -subspace in dimension at most , and proved that such a subspace has dimension at most unless it defines a subgeometry. This mission concerns the extremal case: subspaces attaining , and the way they meet hyperplanes.
Timeline.
Let be finite fields, , and let be an -dimensional vector space over , viewed also as an -dimensional vector space over . A hyperplane of is an -dimensional -subspace.
Fix an integer with . An -subspace of is -scattered if and every -dimensional -subspace satisfies . It is maximum -scattered if no -scattered subspace of has larger -dimension.
Put and suppose . For an -subspace of dimension , let be the number of hyperplanes with . The proof works with the Gaussian binomial coefficients , the -Pochhammer symbols , the elementary symmetric values of , and the sums
If is a maximum -scattered -subspace of of dimension , then for every hyperplane of
The result. Theorem 2.7 says that a maximum -scattered subspace of dimension has only possible intersection dimensions with hyperplanes. Its linear set therefore meets hyperplanes in few sizes, which links these subspaces to sets of few intersection numbers and to codes with few weights. Inside the paper, the upper bound is the input to §3: it shows that the Delsarte dual of a maximum -scattered subspace of dimension is maximum -scattered (Theorem 3.3). That theorem in turn gives maximum -scattered subspaces when does not divide .
Formalizing it. The theorem is proved in the paper, but no machine-checked version exists. Beyond the geometry, the mission produces a library of finite -series facts: Gaussian binomials as rational functions of , the -binomial theorem in both forms, Carlitz's inversion formula, and the elementary symmetric evaluation . Some of these are proved on the platform in a different Mathlib environment, but they are not available in this one. Counting statements about subspaces over finite fields (hyperplanes through a subspace, ordered independent tuples) are also needed and are reusable.
The lower bound is a dimension count. The upper bound is not: the obvious approach bounds from the scattered property alone, but the -scattered condition controls intersections with -dimensional subspaces, and hyperplanes have dimension , which is far larger. No pointwise argument is known; the paper determines the distribution only through its first moments, given by a double count, and then shows that a specific nonnegative combination of the vanishes. The moment identities hold only for (Lemma 5.7 needs each independent vectors of to stay independent over ), and closing the argument requires exact evaluation of a triple -series with signed Gaussian binomials and quadratic exponents.
F, a finite field K with [Algebra F K], and a finite-dimensional K-module with a compatible F-module structure (IsScalarTower F K V). We take finrank K V, finrank F K and Fintype.card F.IsHScattered.Proofs of any milestone, of standard counting facts for subspaces of finite vector spaces, and of the -series lemmas are welcome.
A constraint satisfaction problem (CSP) asks whether variables ranging over a finite domain can be assigned values so that every constraint from a fixed finite list of relations is satisfied. A central organizing principle of the algebraic theory of CSPs is that the complexity of is governed by its polymorphisms, the functions that preserve every relation of when applied coordinate-wise. For this principle to be usable, one needs to know which sets of functions arise as polymorphism sets. For ordinary relations this goes back to the Galois theory of clones and relations. Pippenger (Galois theory for minors of finite functions, Discrete Mathematics, 2002) characterized the families of functions that are the polymorphism sets of pairs of relations, allowing infinitely many pairs.
Promise constraint satisfaction problems (PCSPs) relax CSPs: every constraint comes as a pair , and the task is to distinguish instances satisfiable with the strong relations from those unsatisfiable even with the weak relations . Approximate graph colouring and -SAT are PCSPs. Brakensiek and Guruswami (arXiv:1704.01937v2, SIAM J. Comput. 2021) develop an algebraic theory of PCSPs based on polymorphisms. In §6.2 they prove a finite version of Pippenger's characterization: the families of the form for a finite family of promise relations are exactly the families satisfying three explicit conditions. This mission formalizes that theorem and its CSP analogue (§6.3).
Fix a finite set . A family of functions over consists, for every arity , of a set of functions .
A promise relation of arity is a pair of subsets of with . A finite family of promise relations is indexed by a finite set of relation symbols, each with its own arity . A function is a polymorphism of if for every and all , applying coordinate by coordinate gives a tuple in :
is the family of all polymorphisms of .
For and a map , the projection (or minor) is
A family is projection-closed if whenever has arity and . It is finitizable if there is a finitized arity such that for every arity and every ,
Finally is the identity, a function of arity .
The finite family is existential together with its signature and arities; nothing about its shape is fixed in the statement.
A CSP is a finite family with for every pair. With a clone (for of arity and of arity , the function of arity is in ):
Theorem 6.5 identifies the polymorphism families of finite promise templates intrinsically, without reference to relations. Together with the Galois correspondence of §6.1 (if then is definable from , so reduces to ), it justifies studying PCSPs entirely through families of functions closed under minors, the viewpoint later systematized by the theory of minions (Barto, Bulín, Krokhin, Opršal, arXiv:1811.00970). Lemma 6.8 recovers, in the same language, the description of polymorphism clones of finite CSP templates as the finitely related clones.
The results are proved in the paper; to our knowledge none of them has a machine-checked proof. The mission produces a Lean formalization of both directions, built on the published definitions of relational structures and polymorphisms already used by other PCSP missions on the platform, and reusable definitions of projections (minors), projection-closed and finitizable families, and clones.
The arguments are elementary, and the difficulty lies in uniformity and finiteness. For Claim 6.6, a single arity must detect every failure of the polymorphism condition for functions of every arity , so has to be bounded independently of ; an argument that handles each arity separately does not give finitizability. For Lemma 6.7, a finite family of promise relations has to be produced from alone. The general Galois connection between functions and relations produces infinitely many relations (one for each arity and each witness of non-membership), and the content of the lemma is that the three conditions allow a finite family instead. In both directions the encoding matters: functions of arity must be compared with tuples of a relation, and coordinates, projections and the identity must be matched exactly, with no degenerate arity left over.
A family of functions is FunFamily D := (L : ℕ) → Set ((Fin L → D) → D), with a finite type with decidable equality. Coordinates are 0-based (Fin L), and is fun y => f (y ∘ π) with π : Fin L → Fin R. A finite family of promise relations is a finite type τ of symbols with arities ar : τ → ℕ and two structures 𝔸 𝔹 : RelStruct τ ar D with 𝔸.rel R ⊆ 𝔹.rel R; polymorphisms are the published IsPolymorphism (definition PCSPBLPAff_Symmetric_Setting), and a CSP uses one structure on both sides.
All function arities are positive. The paper's "" is read as positive integers: "" is compared at every arity , projection-closure and finitizability quantify over , and the finitized arity is at least . Including arity would make the necessity direction false as stated (with every empty the paper's finitized arity is ).
The clone condition of Lemma 6.8 is the paper's displayed one (p. 30): act on disjoint blocks of inputs, and the composed function has arity .
A trivializing formalization is ruled out by the statement's shape: the finite family, its signature and its arities are all existentially quantified (fixing a single relation would turn the necessity direction into a special case), is part of every family (without it fails), and finitizability is an equivalence for every function, members and non-members alike.
The development needs only finite types and functions; no complexity theory is involved. Proofs of the milestones, and reusable lemmas about projections (composition of projections, projections along injective maps), are welcome.
Discrete optimal transport between two histograms is a linear program. Its feasible set, the transportation polytope, has been studied since Hitchcock (1941) and Kantorovich, and the structure of its vertices underlies the classical algorithms for the problem: the north-west corner rule produces a vertex, and the network simplex moves from vertex to vertex. A linear program with a nonempty bounded feasible set attains its minimum at a vertex, so knowing what vertices look like tells us what optimal transport plans can be assumed to look like.
This mission is the fourth of a series formalizing G. Peyré and M. Cuturi, Computational Optimal Transport (Foundations and Trends in Machine Learning, 2019). It covers §3.4.1 of the book, Tree Structure of the Support of All Vertices of U(a, b) (pp. 405–407), whose single numbered result, Proposition 3.4, states that the support of a vertex is a forest. The book credits the result to Brualdi, Combinatorial Matrix Classes (2006, Theorem 8.1.2).
Fix integers and histograms , . The transportation polytope is
the set of nonnegative matrices whose row sums are and whose column sums are . Histograms are nonnegative and sum to one; is the set of couplings between them. The cost of a plan for a cost matrix is .
A point of a set is an extremal point (vertex) of if, whenever and , necessarily .
Take source nodes and target nodes . The complete bipartite graph between them has the edges . For a matrix , the support is the set of edges with , and the support graph is . A transport plan is a flow on the complete bipartite graph, with leaving node and entering node ; records the edges the flow actually uses.
If is an extremal point of , then
For , and any cost , some minimizer of over is an extremal point of .
Proposition 3.4 is the sparsity statement of discrete optimal transport: a vertex of moves mass along at most source–target pairs, out of possible. With the companion, some optimal plan is that sparse. This is what makes the network simplex method a combinatorial algorithm on spanning trees of the bipartite graph (§3.5 of the book), and it is the reason the north-west corner rule (§3.4.2) can produce a feasible vertex with a tree support. The same fact, specialized to and uniform histograms, is one step on the way from Kantorovich's relaxation back to Monge's assignment problem.
The result is classical and proved; it has not, to our knowledge, been formalized. Mathlib has the transportation polytope only implicitly (no dedicated definition), and it has the edge count of trees (SimpleGraph.IsTree.card_edgeFinset) but not the corresponding bound for forests. The mission produces a machine-checked link between the convex geometry of and the combinatorics of its support graph, reusable by later missions of the series on the network simplex and on the assignment problem.
The convex-geometric half is elementary; the work is in the passage between a cycle of a graph and a matrix. The cycle is an object of Mathlib's graph library (a closed walk with distinct vertices in a graph on ), while the perturbation is a matrix indexed by . An informal picture of a cycle as a list of edges hides what the matrix statement needs: each source and each target must be visited at most once, and Mathlib's cycles are walks whose distinctness conditions have to be carried to the matrix level.
The edge bound for forests is not packaged in Mathlib either: it counts the edges of a tree, a connected acyclic graph, while the support graph of a vertex is in general disconnected, and the empty graph must be handled.
All objects live in the namespace CompOT.Vertices. Indices are Fin n and Fin m (0-based; the book's ). Matrices are Matrix (Fin n) (Fin m) ℝ, and is the set of matrices with nonnegative entries, row sums and column sums . Extremality is the book's midpoint definition, relative to the set: the points in range over only. This rules out the trivializing reading in which range over all matrices (no point would then be extremal and the goal would be vacuous); conversely, the sanity file shows a non-extremal coupling, so extremality is not automatic either.
The support graph is a SimpleGraph (Fin n ⊕ Fin m) with Sum.inl i adjacent to Sum.inr j exactly when and no other adjacencies. The book calls the edges directed, but the cycles of its proof alternate between sources and targets, so "no cycles" is Mathlib's SimpleGraph.IsAcyclic of this undirected graph. The number of nonzero entries is the cardinality of .
The goal, feasibility milestone and companion carry , , the book's standing notation for histograms (p. 360). These hypotheses make the index sets nonempty, so natural-number subtraction in the bound agrees with the book's integer expression.
Useful infrastructure, reusable beyond this mission: the forest edge bound for finite simple graphs, and the correspondence between cycles of a bipartite graph and signed matrices with zero line sums. Contributions of either as standalone lemmas are welcome.
The convex feasibility problem asks for a point in the intersection of closed convex sets. It underlies signal and image reconstruction, phase retrieval relaxations, and the constraint handling inside larger optimization methods. The workhorse algorithms are projection methods: the method of alternating projections (MAP), going back to von Neumann for subspaces, and the Douglas–Rachford and Peaceman–Rachford splitting schemes, which can be applied to the indicator, distance or squared-distance functions of the sets.
Without a regularity condition on how the sets meet, projection methods can converge arbitrarily slowly. Bounded linear regularity, an error bound saying that a point close to every set is close to their intersection, is the standard condition under which linear rates are obtained (Bauschke and Borwein, SIAM Review, 1996, doi:10.1137/S0036144593251710). Section 5 of D. Davis and W. Yin, Faster convergence rates of relaxed Peaceman–Rachford and ADMM under regularity assumptions (arXiv:1407.5210v3, Math. Oper. Res. 42(3), 2017) applies relaxed Peaceman–Rachford splitting (PRS) to the squared distance functions of two sets and proves that, under bounded linear regularity, the distance of the iterates to the intersection contracts by an explicit factor at every step, with step sizes and relaxation parameters allowed to vary between iterations. MAP is the special case of step size and relaxation .
Let be a real Hilbert space and closed convex sets with . For the distance function is , and is the metric projection, the nearest point of . The problem is modelled with
For the proximal map is the minimiser of , and the reflection is . With two step sizes, , and .
Given , step sizes and relaxation parameters , iteration (5.1) is
The pair is boundedly linearly regular (Definition 5.1) if for every there is such that
where is the open ball. The rate function is
Suppose is boundedly linearly regular, is generated by (5.1), every lies in , and on . Then for all
and if , the iterates converge to a point with
The milestones follow the paper's own argument: Proposition 5.1 Parts 2 and 3 (the gradient of and the closed form ); Proposition 5.2, the fundamental inequality specialised to squared distances; Propositions C.1 and C.2 (the fixed-point set of is , and the iterates are Fejér monotone for ); and the displays (5.5)–(5.7), (5.8), (5.10) and (5.11) of the proof of Theorem 5.1, ending with the one-step contraction at a single point.
With and , iteration (5.1) is MAP, , and under the assumptions of Theorem 5.1 it contracts the distance to by from the second iterate on, converging linearly to a point of the intersection.
Theorem 5.1 gives an explicit, iteration-wise linear rate for relaxed PRS on the two-set feasibility problem with step sizes and relaxation parameters that may change from step to step. Its specialisation, Corollary 5.1, recovers linear convergence of MAP under bounded linear regularity with rate , better than the derived in earlier work on cyclic projections. Remark 5.1 of the paper notes that Douglas–Rachford on indicator functions is a limiting case of the scheme as the step sizes grow, though the rate degenerates in that limit.
The results are proved in the paper; the proof of the convergence statement cites Bauschke–Combettes, Convex Analysis and Monotone Operator Theory in Hilbert Spaces, Theorem 5.12 (Fejér monotone sequences whose distance to a closed convex set decays converge strongly). No machine-checked proof of these statements was found on Prove2Me (search of 2026-10-07). A formalization produces a checked chain from the closed form of the prox of through the fundamental inequality to the linear rate, and with it reusable facts about squared distance functions, metric projections onto closed convex sets in Hilbert space, and Fejér monotone sequences.
The obvious argument would contract the distance to directly, but one PRS step measures only at and at the reflected point , never . Transferring the second distance back to costs a factor with , and only after that does the regularity inequality turn into . The fundamental inequality (5.2) itself rests on the prox-gradient calculus of the earlier sections, specialised to functions whose gradients are Lipschitz. Passing from a contracting distance to convergence of the iterates to one point needs Fejér monotonicity and a completeness argument; a contracting distance alone does not give a limit.
Everything lives in a real Hilbert space (InnerProductSpace ℝ H with CompleteSpace H); is Mathlib's Metric.infDist. The squared distance is viewed as an extended-real function so that the published proximal predicate ThreeOpSplitting.ConvexRates.IsProx applies, and prox maps are arbitrary maps satisfying it (unique here). Metric projections are maps satisfying the published RandomGradFree.Nonsmooth.IsMetricProjection. Step sizes and prox maps are indexed by the iteration. The hypotheses of the goal are: closed and convex with nonempty intersection; bounded linear regularity of the pair; ; ; iterates in an open ball on which the regularity inequality holds with . The range is Algorithm 1's standing assumption, used in the proof but not restated in (5.1). The condition is stated as a uniform bound on all rate factors. The product in (5.4) runs over ; the page prints the upper index , which claims an extra factor that the proof does not give. In the proof's (5.9)–(5.10) the page swaps and relative to (5.2); the milestone states the pairing that (5.2) produces. Corollary 5.1's improved rate is stated for , since it uses .
A trivializing formalization is ruled out: the goal mentions none of the proof's intermediate quantities, takes the prox maps as genuine minimisers of the squared-distance objective rather than chosen points, and measures distances to a nonempty intersection, so the junk value of infDist on the empty set never arises.
A complete development needs the closed form of , differentiability of , the fundamental inequality of the paper's §1 specialised to these functions, and the convergence theorem for Fejér monotone sequences. The last three are reusable well beyond this mission. Proofs of any milestone, and of Mathlib-level lemmas on metric projections, are welcome.
An assignment problem pairs each of sources with exactly one of destinations while minimizing a specified cost. A permutation records those pairings. The number of permutations grows as , so a direct search quickly becomes impractical. In discrete optimal transport, the same data can be placed in a linear optimization problem over nonnegative matrices: a matrix entry records how much mass moves from one source to one destination. That formulation permits a source's mass to be split, which gives it many more feasible solutions than the assignment problem. The question for this mission is whether the added flexibility can improve the optimum when every source and destination carries the same mass. The setting and answer are given in Peyré and Cuturi, Computational Optimal Transport, §2.2–2.3.
This capstone is the first in a series based on the textbook. It links a finite combinatorial optimization problem to the matrix model used throughout later chapters. The general transport model is needed again when marginals are unequal, when cost matrices come from distances, and when entropy is added to the objective. The uniform matching case isolates a useful boundary: relaxing an assignment to allow fractional flows expands the feasible set, yet it does not change the best objective value.
Fix an integer and a real cost matrix . The entry is the cost of sending a unit of mass from source to destination . No sign or metric assumption is imposed on . A permutation assigns source to destination , with every destination used once. The assignment objective of equation (2.2) is
The factor matters: it treats each source as having mass , so the assignment and transport objectives use the same total mass.
A histogram is a vector of masses. The uniform histogram has at each of the indices. A coupling of histograms and is a nonnegative matrix with row sums and column sums . The set of such matrices is
Its linear cost is , and denotes the minimum cost over , as in equations (2.10)–(2.11). For a permutation , the scaled permutation matrix has entry in column of row and zero elsewhere. Consequently is a coupling of with itself, and its transport cost equals . A general member of may distribute a row's mass across several columns.
Because every scaled permutation matrix is feasible for the transport problem, the unrestricted minimum cannot exceed the assignment minimum:
This is the weaker claim in the milestone list. The symmetry of couplings under transposition and the identity supply reusable statements about the model. The list also states the book's scaled form of Birkhoff's extreme point characterization.
The goal is the stronger statement: there is an assignment that also minimizes over the full coupling polytope,
This is Proposition 2.1, pp. 372–373. It quantifies over every real cost matrix of the given size. The equality of optimal values follows from the stated common optimizer; the proposition does not claim that every optimal transport plan is a permutation matrix.
The result gives an exact linear relaxation for uniform assignment. One can optimize over a convex set of matrices without paying an optimal value penalty for allowing fractional mass. The conclusion has a precise limit: it guarantees at least one integral, scaled permutation optimizer, while other optimal couplings can coexist when the cost matrix has ties. When source and destination weights are unequal, the assignment formulation may not even be feasible; the broader coupling model then carries information that a permutation cannot represent.
For formalization, the result fixes a finite transport interface that later missions can compare with their own conventions: nonnegative matrix entries, prescribed row and column sums, and a cost that is linear in the matrix. Mathlib already contains Birkhoff's theorem for doubly stochastic matrices with row sums equal to . This mission's formal target uses the probability normalization , so the scaling is part of the mathematical statement. The textbook result is known; the goal here is a machine checked Lean proof of this precise version and its cited supporting claims. The listed Lean declarations are currently open statements with sorry placeholders.
The evident inequality points in the easy direction: enlarging a feasible set can only reduce a minimum. It gives no reason why a minimizer over the larger set should happen to be a permutation matrix. A generic feasible coupling can split mass between several destinations, and even a unique assignment need not be the only point under consideration in the relaxed problem. The central issue is the geometry of the uniform coupling polytope and its relation to permutation matrices. Its normalization differs from the usual doubly stochastic convention, so a proof using a standard library theorem must retain the factor at every point where a matrix or objective is converted.
The Lean index types are Fin n and Fin m; they have and elements but are numbered from zero. Histograms are real valued functions on those types, and couplings are real matrices constrained to be nonnegative with exact finite row and column sums. The pairing is a finite double sum. The goal assumes so that the displayed is meaningful and the assignment problem has an index to assign. There is no additional positivity requirement on . The minimum values are represented by real infima only in statements where the uniform coupling polytope and permutation set are nonempty and their finite dimensional objectives are bounded below.
An optimal coupling in the goal is compared with all matrices in , including fractional ones. Restricting that comparison to permutation matrices would erase the proposition's content. The definitions of coupling feasibility, scaled permutation matrices, and the assignment cost are reusable beyond this chapter. Contributions that establish the scaling relation to Mathlib's doubly stochastic matrices, the extreme point characterization in this normalization, or the goal from these components fit the mission. The optional strict inclusion claim on p. 372 is excluded from the milestones because its printed formulation fails at ; it would require a separate statement. The page also prints row and column sums of as despite defining entries ; the Lean statement uses .
A manufacturer that sells through an independent retailer may also open its own direct channel, an online store or a factory outlet. This is called supply chain encroachment. The operations literature has asked whether encroachment helps or hurts the two firms. The usual approach compares the double-marginalization cost of a pure retail channel with the competition the direct channel creates. With quality exogenous and uniform across channels, Arya, Mittendorf and Sappington (2007) showed that encroachment can lead to a win–win outcome when the manufacturer's direct selling cost is large, because it pushes the wholesale price down.
Ha, Long and Nasiry (Quality in Supply Chain Encroachment, MSOM 18(2), 2016; authors' manuscript SSRN 3970373) make product quality a decision of the manufacturer. Their main model lets her commit to the qualities of both channels before the retailer orders. In that model quality differentiation is not always optimal: for some parameters she sells the same quality in both channels (their Proposition 4).
Commitment is a modelling assumption. When design lead times are short, the manufacturer can redesign the direct-channel product after seeing the retailer's order, so she cannot credibly announce its quality in advance. Section 6.3 of the paper studies this fast-design case. Its only analytical result is Proposition 7: without commitment, quality differentiation across channels is always optimal. This mission formalizes that proposition and the three steps of its proof.
Consumers. A consumer has quality sensitivity , uniform on , and obtains surplus from one unit of quality at price . The manufacturer sells units of quality directly and the retailer sells units of quality . Each consumer buys at most one unit, and the market-clearing prices depend on which product has the higher quality:
At both channels clear at .
Costs. One unit of quality costs the manufacturer , with . She pays a selling cost for each unit sold directly; the retailer's selling cost is .
Profits. For a wholesale price ,
Timing without commitment.
The game has perfect information and is solved by backward induction. A strategy profile has three parts: a stage-1 choice , a retailer rule , and a stage-3 rule . The profile is a subgame perfect equilibrium (SPE) when, at every history on or off the path, the mover's action is feasible and no feasible alternative gives the mover more. The manufacturer encroaches when on the equilibrium path.
For every , and every SPE whose equilibrium path has and ,
Write with .
The case gives in the same way, and the two agree at . 2. Derivatives (31)–(32). The -derivatives of and , their values at , and the equivalence
Milestone 3 is stronger than the goal: it holds at every stage-3 history, not only on the equilibrium path.
The result. Proposition 7 shows that the structure of the optimal product line depends on the timing of design decisions. With commitment, the manufacturer sometimes keeps a single quality. A lower-quality direct product would draw a larger retail order but forgo market segmentation, and with some parameter values she accepts that trade. Without commitment, the direct-channel quality can no longer influence the retailer's order. She then always differentiates, so whenever both channels sell, consumers face a two-product line. The paper's numerical work (Figure 6) compares the two regimes. The analytical statement that differentiation is universal without commitment is this proposition.
Formalizing it. The proposition has a short, informal proof in the e-Companion. That proof argues through first-order conditions, "given that is optimal". It uses the strict signs printed in (31) and (32), although optimality gives only weak inequalities. Its contradiction relies on the retailer's order being positive, which the statement leaves implicit. A machine-checked proof pins down exactly which hypotheses the result needs. It also contributes reusable facts about Cournot-type stage games with vertically differentiated products. No part of this paper has been formalized before.
The stage-3 problem is a joint choice of quality and quantity , and the demand system changes form at , so the manufacturer's profit is not differentiable in there. The value function after optimizing is a piecewise expression: to the right of , to the left, and the linear profit wherever the optimal is zero. An argument that is not optimal has to work with one-sided derivatives of this function at a kink. It must also check that the optimal quantity stays positive on both sides near .
An obvious shortcut is to argue that differentiation is optimal because segmentation always pays. That argument fails at . There the manufacturer is a one-product monopolist, and is optimal whenever happens to equal her monopoly quality. The positive retail order is therefore essential.
All definitions live in the namespace QualityEncroach.NoCommit. They are real-valued throughout, and the formalization fixes the following conventions:
A trivializing formalization is ruled out: the stage-3 rule maps to , so is chosen after the order. Putting at stage 1 would give the committed game, where the proposition is false. The goal is conditional on an SPE existing, which the paper does not prove. A verification file checks the price formulas on hand instances in both branches. At , , , and , it checks that the basic parameter conditions hold and a uniform stage-3 choice is strictly beaten by . The numerical check does not establish the existence of an optimal stage-3 choice or an SPE.
A complete development needs elementary real analysis only: maximization of concave quadratics, one-variable derivatives, and one-sided optimality conditions at a kink. Proofs of any milestone, and proofs of the goal from milestone 3, are welcome.
Best subset selection with ridge shrinkage asks for a coefficient vector that fits a response through a design matrix while using few nonzero coefficients:
This -regularized least squares problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (BnB). The speed of BnB is governed by the strength of the continuous relaxation solved at every node: a larger relaxation value prunes more nodes. Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) build the solver L0BnB on a perspective formulation and compare its relaxation with two standard alternatives. Their Proposition 1 quantifies that comparison, and their experiments (Section 4.2.1 of the paper) report speed-ups of more than 90× from using the perspective formulation with a tight bound instead of the bound-free formulation.
The mission formalizes Proposition 1 together with the three steps of its proof in the paper's Appendix A.
Fix , , regularization parameters and a bound on ; write .
The Big-M formulation introduces indicators and minimizes subject to , . Its interval relaxation lets ; its optimal value is .
The reverse Huber penalty is for and for . Put
and let if and if . The paper's Theorem 1 shows that the interval relaxation of the perspective formulation is equivalent to
and denotes the optimal value of (5). Without a bound, the relaxation value of is
Finally , and denotes an optimal solution of (5).
For ,
The goal is the conjunction of milestones 2 and 4.
In the regime both added terms are nonnegative: because , and because whenever . So the perspective relaxation is at least as strong as both the Big-M relaxation and , strictly so as soon as one coordinate of lies strictly inside in absolute value (for (7)) or (for (8)). The bounds are explicit in the relaxation's own solution, so they can be evaluated at a BnB node. This is the theoretical justification for the paper's design choice of building its solver on with a valid, tight ; the regime , where (5) is (6) with the additional box constraint , is complementary.
Proposition 1 is proved in the paper; it has no machine-checked proof. The mission produces one, together with reusable Lean definitions of the three relaxation values and of the reverse Huber penalty that other statements about perspective relaxations of sparse regression can be stated against.
The arithmetic of the coordinate-wise penalties is short. The substance is in comparing optimal values that are defined as infima over different feasible sets. The obvious argument "" requires that the Big-M relaxation, which is posed over pairs , have value at most ; that is the content of (37), a statement about a different feasible set in more variables. Likewise (8) needs , i.e. that the infimum in (6) is a genuine lower bound of a set bounded below, and both inequalities use the regime , in which . Dropping the regime hypothesis makes (8) false in general: for one has and , and the right side can exceed .
All objects live in the namespace L0BnB.Strength. Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M as hypotheses; is Fin p. Norms are explicit sums: is ∑ i, v i ^ 2, is ∑ i, |β i|, and is ∀ i, |β i| ≤ M. The regime is written M < Real.sqrt (lam0 / lam2).
Optimal values are sInf of the image of the feasible set in ℝ. Each set is nonempty (, ) and bounded below by under the positivity hypotheses, so sInf is the true infimum and never a junk value. is defined over pairs with , not through ; (37) is a theorem. is (6) as printed: the paper attributes to its reference [21] the identification of (6) with the interval relaxation of in variables, and that identification is not part of the mission. is the value of (5), which is the paper's definition; Theorem 1 (the equivalence of (5) with the relaxation) belongs to a sibling mission.
The optimal solution is a binder with the hypotheses and for every in the box. A formalization in which is an arbitrary feasible point, or in which or is defined through a chosen minimizer, would change the statement and is ruled out. The paper uses no in this result, so no constant is instantiated.
Needed infrastructure is light: continuity of and compactness of the box for the attainment in (37), and csInf lemmas on ℝ. Contributions of proofs of any milestone, and of the attainment of the infimum in (5), are welcome.
Online retailers, search engines and streaming services show products on a sequence of pages, and most consumers look at only the first few. Which products are seen therefore depends on where they are placed. Gallego, Li, Truong and Wang (Operations Research, 2020) call the problem of placing products on pages to maximize expected revenue product framing. They show that it is NP-hard even with two pages and the multinomial logit model, and they give simple algorithms with constant-factor guarantees.
This mission concerns their second guarantee. In their basic model every consumer chooses with the same choice model, whatever the number of pages she views. In practice the number of pages viewed is itself informative: consumers who browse many pages may be keener buyers. Section 6 of the paper lets the choice model depend on the number of pages viewed and proposes the TRUNC algorithm for this setting. The guarantee is that TRUNC earns at least one third of the optimal expected revenue.
There are products with revenues and virtual pages, each holding at most products; write . A framing places each product on at most one page, with at most products per page. A consumer views a random number of pages, with law , tail and failure rate . Her consideration set is the set of products on pages .
A consumer who views pages is of type and buys product from consideration set with probability , where , for , and . The revenue of for type and the best capacitated revenue are
A framing earns , where is the set of products on pages . Its maximum over all framings is . The assumptions are:
TRUNC(), for , picks an optimal assortment for and places it, in any arrangement, on pages , leaving the remaining pages blank. TRUNC takes the best of these framings; its revenue is .
The analysis passes through the bound-revealing program (10): minimize over nondecreasing with nonincreasing and over tails with , subject to .
Under Assumptions B1–B4, for every choice of optimal assortments and every arrangement on the pages,
In the order the proof uses them:
The theorem shows that framing under type-dependent choice admits a constant-factor approximation using only calls to an assortment oracle, although the framing problem itself is NP-hard. The constant does not depend on the number of products, pages or page capacity. The bound-revealing program (10) is a self-contained extremal problem about log-concave tails and is reusable wherever a revenue curve with decreasing average returns meets an IFR horizon. The numerical value of (10) decreases with ( at , about at ), so the constant is approached only as the number of pages grows.
The result is proved in the paper. No part of it has a machine-checked proof: the platform has no item on product framing, discrete failure rates or program (10). A complete development would give a machine-checked proof of the approximation ratio. It would also give a checked treatment of the perturbation arguments of Appendix A.4, which the paper presents briefly.
Two steps are elementary: the upper bound (a consumer of type never sees more than products) and the lower bound (every consumer of type sees all of ).
The difficulty lies in the extremal problem (10). It is not convex: the IFR constraint is a log-concavity condition, and the objective is a maximum of products . A direct bound such as gives a constant that decays with . The uniform constant comes from showing that the extremal tail is geometric beyond the maximizing page and that the extremal is pinned down on both sides of it. The paper reaches this structure through optimality conditions, so a formal proof must also establish that (10) attains its minimum, or must avoid that step.
Products are Fin n. Pages are the natural numbers , as in the paper, with and . A framing is f : Fin n → ℕ: product is on page f i when , and f i = 0 means it is not displayed. The law and the functions of (10) are functions on of which only the values on are used, and .
and are maxima over finite nonempty families, and is a Finset.sup' over . TRUNC is a predicate on its outputs, not a function, and the goal is quantified over every family of runs. Assumption B3 is used with , as everywhere in the paper. IFR is required only where the failure rate is defined (), so laws whose support ends before page are allowed. Nonnegative revenues are assumed; the lower bound of milestone 2 needs them.
No trivializing reading. The goal is not stated for one particular filling heuristic, or for some run only, and is the revenue of the framings themselves, not the lower bound .
Page numbers refer to the authors' accepted manuscript of the Operations Research article, which differ from the journal typesetting. The development needs only Mathlib (finite sums and maxima over Finset). Program (10) and Lemma 8 are independent of the framing model. Contributions are welcome at every milestone: Lemma 8 and the bound for (10) are the most self-contained.
Best subset selection with ridge shrinkage asks for a sparse linear model: given a design matrix and responses , minimize
where counts nonzero coefficients. The problem is NP-hard, and exact methods solve it as a mixed integer program by branch-and-bound (Bertsimas, King, Mazumder 2016). The speed of branch-and-bound is governed by two things: how tight the continuous relaxation at each node is, and how cheaply that relaxation can be solved.
Hazimeh, Mazumder and Saab (arXiv:2004.06152v2; Mathematical Programming 2022) build a branch-and-bound solver whose node relaxations are solved by first-order methods rather than by a conic interior-point solver. Their starting point is the perspective formulation, a standard device for strengthening relaxations of mixed integer programs with indicator variables (Frangioni, Gentile 2006; Günlük, Linderoth 2010). Theorem 1 of the paper shows that the interval relaxation of this formulation is a box-constrained least squares problem with a separable penalty in alone. This mission formalizes Theorem 1.
Timeline. Owen (2007) introduced the reverse Huber penalty as a hybrid of lasso and ridge. Dong, Chen, Linderoth (2015) showed that the interval relaxation of the perspective formulation without a Big-M bound reduces to least squares with a reverse Huber penalty. Hazimeh, Mazumder and Saab (2020–2021) added the Big-M constraint and obtained Theorem 1, with a second regime in which the penalty becomes .
Fix , , , and , and write . The perspective formulation is problem (3) of the paper:
Here indicates whether may be nonzero, stands in for through the rotated second-order cone constraint , and bounds . The interval relaxation replaces with .
The reverse Huber penalty (4) is for and for . Put
and let if and if . The reduced relaxation (5) is
with optimal value . For one coordinate , is the minimum of over , , , .
The interval relaxation of (3) is equivalent to (5):
and both problems attain the common optimal value .
The result. Theorem 1 removes the auxiliary variables and all conic constraints from the node relaxation. What remains is a composite problem, a smooth least squares loss plus a separable, convex penalty under a box constraint, to which coordinate descent and proximal methods apply directly. The paper's solver, its active-set strategy, and the dual bounds of its Section 3 are all built on (5). The theorem also exposes a regime change: when , the ridge term of the perspective formulation disappears from the relaxation and the penalty is pure . Propositions 1 and 2 of the paper, which compare the strengths of the perspective, Big-M and relaxations, use this reduced form.
Formalizing it. The result is proved in the paper (Appendix A) by a coordinatewise argument. To our knowledge it has no machine-checked proof. Formalizing it gives a verified bridge from the conic mixed integer formulation to the penalized form that later results of the paper use, and a checked case analysis at the regime boundary , where the two formulas must agree with the stated tie-breaking.
The obvious approach, "minimize over and coordinate by coordinate", is correct in outline, but each step hides a boundary case. The rotated cone constraint degenerates at or , where is undefined, and the paper's convention for must be handled. The one-variable problem (36) is a minimum of a pointwise maximum of two functions of , one convex and decreasing then increasing, the other increasing. Its minimizer lies either in the interior of the region where the first term dominates or on the crossover , depending on the regime. The paper's proof describes the cases loosely: it optimizes the Case I term without imposing the side condition that Case I attains the maximum. A complete argument must prove the lower bound over all feasible , not just evaluate at a candidate. Finally, the minimum over must be shown to split into a sum of coordinate minima, each attained.
Data are X : Matrix (Fin n) (Fin p) ℝ, y : Fin n → ℝ, and reals lam0 lam2 M with 0 < lam0, 0 < lam2, 0 < M; the paper's is Fin p. The squared norm is the explicit sum , and is for all . The cone constraint is kept in product form . In and (36), Lean's coincides with the paper's convention for . Every "min" is stated with IsLeast (membership plus lower bound), so attainment is part of each statement. is defined as a real infimum over the box, and Theorem 1 asserts that this infimum is attained by both problems. No normalization of or is assumed; the paper's unit-norm assumption starts in Section 3. The paper writes no in these results, so there are no constants to instantiate.
A goal stating only one inequality (that is achieved by some , or that it bounds the relaxation from below), or a goal over , would not be Theorem 1. The IsLeast form rules out both. The goal uses with both regimes.
A complete development needs: a two-variable convexity argument for on ; a lemma that the infimum of a separable objective over a product of feasible sets is the sum of the coordinate infima; and continuity of with compactness of the box to obtain an optimal . The coordinate lemmas and the definition of the reverse Huber penalty are reusable in the companion missions on relaxation strength and Lagrangian duality. Contributions to any milestone, or an alternative proof of the goal, are welcome.
Thompson sampling (TS) selects each action by sampling a parameter from the current posterior and playing the action that is optimal for the sample. It is a stationary randomized strategy: the distribution of the action is a fixed function of the posterior, the same in every period, and the action is drawn at random from it. Its Bayesian regret bounds, surveyed in §8.1 of the tutorial by Russo, Van Roy, Kazerouni, Osband and Wen (Found. Trends Mach. Learn. 11(1), 2018), grow sublinearly in the horizon .
A natural question is whether the randomization is essential. A strategy that maps the posterior to an action deterministically, for example "play the action with the highest posterior mean", is equally stationary and conceptually simpler. §8.1.3 of the tutorial answers the question with Example 8.1 (A Known Standard), taken from Russo and Van Roy, Learning to optimize via information-directed sampling (Operations Research 66(1), 2018): in a two-action problem with a known baseline action, every stationary deterministic strategy suffers linearly growing expected regret under some prior. The example is the standard justification for why posterior sampling, and not a deterministic function of the posterior, is the right stationary rule.
There are two actions and a binary unknown parameter with prior
In each period the agent selects an action and observes a binary reward . Rewards are conditionally independent across periods given and the actions:
The mean reward of action is its success probability, and the optimal action is action if and action if , so or .
The history lists the actions and rewards of the first periods. The posterior is given by Bayes' rule (4.2) of the tutorial, applied period by period:
with the prior on the empty history.
A stationary deterministic strategy is one function from posterior probabilities to actions, used in every period: . The expected cumulative regret (Bayesian regret, p. 71) of running from the prior for periods is
the expectation taken over and the rewards. The Lean development names these objects succProb (), optMean (), post (), Strategy (), lawGiven (the probability of a history given ) and expRegret.
This is the sentence "for any deterministic stationary strategy, there exists a prior probability such that expected cumulative regret grows linearly with time" (p. 79). The prior is chosen after the strategy. No constant is fixed; only the linear shape is asserted.
The example separates two properties that regret analyses often conflate: being a function of the posterior alone (stationarity) and achieving sublinear Bayesian regret. It shows that a stationary strategy with sublinear regret on all priors must randomize, which is the structural reason TS samples rather than maximizes. It also explains why deterministic algorithms with good regret, such as upper confidence bound methods, are necessarily nonstationary: their confidence radii depend on the period and on counts, not only on the posterior.
The tutorial gives the argument in one paragraph. A formal version makes precise what is left implicit there: that the posterior is the actual conditional probability computed from the history, that "uninformative" means the posterior is invariant under action , and that under action the posterior never leaves . The result is a closed-form regret identity in each case, not only an asymptotic statement. As far as is known, neither the example nor its source in Russo and Van Roy (2018) has been machine-checked.
The mathematics is elementary; the work lies in the bookkeeping of a history-dependent strategy. The strategy's action in period depends on the whole history through , so the law of is a product of indicator factors, each evaluating at a posterior computed from a prefix of the same history. A direct computation of the regret must show that every history of positive probability follows a single action path, and that is a statement about the posterior along every prefix, not only at the first period. A first attempt that defines the posterior by a recursion in which "the posterior stays at " is built in proves nothing about the example; the posterior must be Bayes' rule applied to the history.
0 : Fin 2, action is 1 : Fin 2; is true; a reward of is true. Lean period s : Fin T is the paper's period .Fin t → Fin 2 × Bool; every probability and expectation is a finite sum, so no measure theory is needed.post is the closed form of iterated Bayes' rule (4.2). The probabilities with which the strategy picks its actions are or and do not depend on ; on histories of positive probability they cancel, so post is the true conditional probability there. For its denominator is positive, so Lean's convention is never used.ℝ → Fin 2; its values outside are never used. The same function acts in every period, which is what "stationary" means.The tutorial's argument for the example is on p. 79; the tutorial attributes the example to Russo and Van Roy (2018).