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?
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.
Linear sets are point sets of a finite projective space defined by a subspace over a subfield. They appear throughout finite geometry, for instance in the study of semifields and, through the correspondence studied by Sheekey and Van de Voorde (arXiv:1806.05929), maximum rank distance (MRD) codes; see Polverino's survey (doi:10.1016/j.disc.2009.04.007). In these applications one needs to decide when two linear sets are the same up to a collineation, which can be difficult (Csajbók–Zanella, arXiv:1501.03441; Csajbók–Marino–Polverino, arXiv:1607.06962). The natural candidate answer, "when their defining subspaces are in the same orbit of the semilinear group", is only a sufficient condition: on the projective line there are maximum scattered subspaces in different -orbits defining equivalent linear sets (the two papers just cited).
Csajbók, Marino, Polverino and Zullo (arXiv:1906.10590, Combinatorica 41 (2021)) introduced -scattered subspaces, a generalisation of scattered subspaces, and showed in their §4 that for the sufficient condition is also necessary. This mission formalizes that result, Theorem 4.5.
Let be finite fields and let be an -dimensional vector space over ; it is also a vector space over . The projective space has as points the one-dimensional -subspaces , .
For an -subspace of , the -linear set of is
of rank .
For , the subspace is -scattered (Definition 1.1) if and every -dimensional -subspace of satisfies . The linear set of an -scattered is called -scattered (Definition 4.1); for it is scattered with respect to lines.
The group consists of the bijective additive maps of that are semilinear: for some field automorphism of . Each induces a collineation of , , and these collineations form . Two linear sets are -equivalent if for some ; two subspaces are -equivalent if for some .
For and -scattered -subspaces , of ,
The result. Theorem 4.5 says that, for , an -scattered linear set remembers its defining subspace up to a scalar and up to the semilinear group. The equivalence problem for such linear sets, a geometric question about point sets, becomes the equivalence problem for subspaces, which is algebraic and can be attacked with linearized polynomials. Through the correspondence of Sheekey and Van de Voorde between maximum -scattered subspaces and MRD codes, the paper derives from it (Theorem 4.10, not part of this mission) that two -linear MRD codes with minimum distance , , and left idealiser isomorphic to are equivalent if and only if their associated linear sets in are -equivalent. Lemma 4.4 and Proposition 4.3 are of independent use: they say that the rank and, up to scalars, the subspace of any linear set scattered with respect to lines are invariants of the point set.
The formalization. The theorem is proved in the paper; no part of it, nor any statement about linear sets over a field extension, is machine-checked in Mathlib. The mission produces a formal model of linear sets, of the semilinear group and of its induced collineations that later finite-geometry missions can reuse, together with formal proofs of the four milestones. Proposition 4.2 is quoted from [5] without proof in the paper, so formalizing it means formalizing Bonoli and Polverino's argument.
The "if" direction is a direct computation, . The obvious approach to the converse, reconstructing from point by point, fails because a point of determines only up to a scalar of , and these scalars can a priori differ from point to point. Without the condition they really do differ: for the theorem is false. The step that needs is the rigidity of the intersections of with two-dimensional -subspaces, which is where the quoted result on linear sets of size on a projective line enters. Proposition 4.2 itself is a counting statement about point weights on and is not available in any library.
F, K with [Algebra F K]; is Fintype.card F. is a finite-dimensional K-module with a compatible F-module structure ([IsScalarTower F K V]), and is Module.finrank K V.IsHScattered F K h U includes the range and the spanning condition , as in Definition 1.1. With this forces .K-submodule K ∙ u; linearSet F K U is a Set (Submodule K V) and is its Set.ncard.f : V ≃+ V for which some σ : K ≃+* K gives f (a • v) = σ a • f v. The collineation sends a subspace to Submodule.span K (f '' P). The image is the set f '' U, and is (λ • ·) '' W with .Welcome contributions: the general theory of linear sets (point weights, with equality iff is scattered), the fact that a semilinear map of maps -subspaces to -subspaces, and the counting argument behind Proposition 4.2. These are reusable for every linear-set mission.
A constraint satisfaction problem (CSP) asks whether variables can be assigned values so that every constraint, drawn from a fixed finite set of relations, holds. The algebraic approach to CSPs explains their complexity through polymorphisms, the operations that preserve all constraint relations; this programme culminated in the CSP dichotomy theorem of Bulatov and Zhuk (2017). A promise CSP (PCSP) pairs each relation with a weaker relation : given an instance that is promised to be satisfiable with the -constraints, one must distinguish it from instances that are not even satisfiable with the -constraints. Approximate graph colouring (is a 3-colourable graph 100-colourable?) and -SAT are PCSPs, and their complexity is not captured by the classical theory.
Brakensiek and Guruswami (arXiv:1704.01937) developed the polymorphism theory of PCSPs and classified the Boolean, symmetric, folded case.
Timeline.
Fix the Boolean domain . A promise relation of arity is a pair with , and a family is a finite set of promise relations, possibly of different arities. A function is a polymorphism of if, whenever , applying coordinate-wise gives a tuple in ; is the set of functions that are polymorphisms of every member of .
A relation is symmetric if it is closed under permuting coordinates. Every symmetric relation has the form , where is the Hamming weight. A function is folded if , and idempotent if and ; a family is folded (idempotent) if all its polymorphisms are. For odd the paper singles out three function families:
and their negations . Finally, is -fixing if some set of at most coordinates satisfies whenever vanishes on .
Let be a finite, folded, symmetric family. If there are odd with
then
No value of is fixed: the goal asserts only that one bound works for all arities.
The milestones follow the paper's proof:
Theorem 4.13 is the structural half of the paper's main dichotomy (Theorem 2.16): a folded symmetric Boolean PCSP is polynomial-time solvable if it has one of the six families as polymorphisms for every odd arity, and NP-hard otherwise. Hardness follows by feeding the -fixing structure into a Label Cover reduction (Theorem 5.3). Bounded "fixing" or junta-like structure of all polymorphisms is the standard route from algebra to NP-hardness for PCSPs. This theorem is the cleanest Boolean instance of it, and it underlies later classifications of symmetric Boolean PCSPs.
The result has been proved and published since 2018. To our knowledge none of it has been formalized. A formalization supplies a checked Boolean polymorphism toolkit (Hamming-weight relations, folding, idempotence, relaxations), checked closure computations under alternating-threshold and majority operations, and a uniform-constant Frobenius-type lemma. All of these can be reused by other Boolean PCSP missions.
The obvious argument fixes a polymorphism and bounds its relevant coordinates directly from a constraint that , or violates. This gives a bound that depends on the arity , and an -dependent bound is trivial ( always works). The work is in making the constant uniform. The proof has to replace by a single canonical promise relation that does not depend on , classify exactly which symmetric relations exclude and , and use an additive-combinatorics lemma whose constants depend only on that relation's arity. Its bounded version must hold with the same constants. The non-idempotent polymorphisms need a separate reduction through the negated family .
The domain is Bool (false ). A family is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar Bool from the published definition PCSPBLPAff_Symmetric_Setting, with [Fintype τ] (finitely many relations) and 𝔸.rel R ⊆ 𝔹.rel R (promise). IsPolymorphism 𝔸 𝔹 f from that file is Definition 2.4. Coordinates are Fin L, so the 1-based sign of becomes . Anti-functions negate the output. Family properties (folded, idempotent, non-degenerate) quantify over polymorphisms of every arity . A folded or idempotent family has no nullary polymorphisms, so admitting changes nothing. The constants , , and are quantified before the arity and the function (respectively before ). A statement that lets the constant depend on or is trivially true and is not the goal.
Out of scope are the complexity conclusions: "PCSP() is NP-hard" (Theorems 2.16 and 5.3) and item 2 of Lemma 2.13 (transfer of tractability). The cited inputs for those conclusions are also out of scope: the PCP theorem with parallel repetition (Proposition 5.2) and Schaefer's theorem. No complexity predicate appears in any statement.
A complete development needs the following, with Mathlib's Nat.frobeniusNumber as a starting point for Lemma 4.9:
Contributions are welcome at any milestone, including separate proofs of the closure computations and of Lemma 4.9.
Brands are routinely held responsible for the labour and environmental practices of their suppliers. A brand that is linked in public to a non-compliant supplier loses consumer willingness to pay, and firms answer this risk by auditing their suppliers. Supply networks are not trees, however: one supplier often serves several competing brands. Chen, Qi and Dawande (SSRN 2889889, Manufacturing & Service Operations Management, 2020) ask how the position of a supplier in such a network, and in particular its centrality (the number of buyers it serves), affects which suppliers get audited when buyers decide on their own, and when they audit jointly.
This mission formalizes the paper's answer for unilateral auditing by competing buyers (Sec. 4.2, Proposition 2). A companion mission treats joint auditing (Proposition 3).
Two buyers source from three suppliers: an independent supplier for each buyer , and a common supplier that serves both. Each supplier complies with social-responsibility standards with probability . In stage 1, buyer chooses an auditing effort on and on , and audits at most one of them: . Auditing a supplier with effort costs , with a fixed cost and ; effort means no audit and costs nothing.
A non-compliant supplier that passes the audits is discovered in public with probability . Hence causes damage to with probability , and causes damage to both buyers with probability , independently. A buyer with at least one exposed supplier suffers the MWTP damage : his demand intercept drops from to . Each exposed supplier is then paid per unit instead of , so a buyer with exposed suppliers has unit cost .
In stage 2 the buyers compete in quantities with inverse demands , (Dixit 1979; Singh and Vives 1984). Its equilibrium profit for is , in closed form (Lemma 1). Buyer 's ex ante expected profit is the expectation of over the eight damage outcomes, minus his audit costs; is symmetric. Three conditions on (p. 8) make all stage-2 quantities positive.
An equilibrium is a profile , , in which each buyer's strategy is a best response to the other's, with the tie-breaking rule of p. 10: a buyer who is indifferent between auditing and not auditing does not audit. Two explicit efforts, (eq. (1)) and (eq. (2)), are rational functions of the parameters; is a buyer's optimal effort on his independent supplier when the rival audits nobody, and is the symmetric solution when both audit their independent suppliers.
Assume and . There exist such that for every , writing , , , ,
In every equilibrium the common supplier receives zero effort.
Lemma 1 (stage-2 equilibrium), the OA.2 expected-profit display, the best-response function (OA-9) with and as its values, the dominance inequality (OA-11), Lemmas OA5 and OA6 (the two kinds of auditing equilibria and their threshold ranges), the monotonicity facts (OA-14)–(OA-15), Lemma OA7 (the order of the thresholds) and Lemma OA8 (no equilibrium audits ). The thresholds of the milestones are the explicit ones the proof defines in (OA-10), (OA-12), (OA-13).
The result separates network position from competition. Without downstream competition (, Proposition 1) there is a Pareto-dominant equilibrium in which one buyer audits the common supplier. With competition, Proposition 2 shows that the common supplier, the most central and therefore the most consequential source of risk, is never audited: auditing it would also protect the rival, who free-rides. This inefficiency is what motivates the paper's analysis of joint auditing (Proposition 3) and of social welfare (Proposition 4).
The result is proved in the paper, partly by omission: the e-companion leaves the proof of Lemma OA8 and the case to the reader. No machine-checked version exists. A formal proof would give a complete case analysis of a two-stage game with a discontinuous fixed cost, a constrained strategy set and a tie-breaking rule, and would check the paper's closed forms, several of which are printed with small slips.
The first-order conditions alone do not determine the equilibria. The fixed cost makes each buyer's payoff discontinuous at zero effort, so every candidate must be compared with no audit, and the best response is a choice among three regimes (audit , audit , audit nobody). Uniqueness claims therefore require excluding every profile in the constrained strategy set, including those where a buyer audits the common supplier, for which the paper gives no proof. The threshold comparisons rest on monotonicity in the rival's effort, and the expected profit is multilinear in the four efforts (plus the quadratic audit costs), with coefficients that are differences of squared Cournot quantities whose signs depend on the p. 8 conditions.
All objects live in the namespace SupplierAudit.Competition. The source is the authors' accepted manuscript on SSRN (2889889); main-text printed pages equal PDF pages, and e-companion page ec is PDF page .
Params carries and the standing assumptions , , , , , and the three conditions of p. 8. The theorems add (competition, Sec. 4.2). is a separate real argument and the goal quantifies over .CournotDuopoly). The model's stage-2 profit is the closed form for all ; Lemma 1 states that it is the game's unique equilibrium.A formalization in which equilibrium is plain Nash, efforts range over all of , a buyer may audit both suppliers, or "interior" is a hypothesis on the equilibrium efforts themselves would state a different (and in places false or vacuous) theorem; these are ruled out by the definitions above. Proofs of any milestone are welcome, as is reusable infrastructure for linear Cournot duopolies and for finite expectations over independent Bernoulli events.
Best-subset selection with ridge shrinkage, , is a mixed-integer program that statisticians want to solve to certified optimality at the scale of modern data ( up to features). Hazimeh, Mazumder and Saab (arXiv:2004.06152, Mathematical Programming 2022) built a branch-and-bound solver, L0BnB, whose node relaxations are solved in the primal space by active-set coordinate descent instead of by an interior-point method. Branch-and-bound prunes a node only with a valid dual bound, a certified lower bound on the node's relaxation value. A primal method returns an approximate minimizer, not such a bound, so the solver must turn an inexact primal point into a dual feasible point and needs to know how much is lost in doing so. This mission formalizes the paper's answer, its main theorem (Theorem 3).
Data are with columns , , and parameters . The reverse Huber penalty is for and for . The penalty equals if and otherwise. The reduced relaxation (5) is
Throughout, the columns of and have unit norm (the standing assumption of Section 3 of the paper).
Algorithm 2 (active-set coordinate descent) returns a point in the box such that the set
is empty: no coordinate outside the support wants to move. Write , , and let be an optimal solution of (5) with . The primal gap is .
The two duals of (5) (Theorem 2 of the paper) are, with ,
the latter under . The dual variables built from are , and . The dual points built from are , with a maximizer of (25) and a maximizer of under the constraints (27).
If , with when and when ,
If ,
The paper states these as (29) and (30); the goal states the expressions its proof establishes.
In the order the proof uses them: the closed-form coordinate updates (14) and (15); Proposition 3, ; the bound ; Lemma 2, which bounds coordinate by coordinate and makes it vanish off the support; inequality (53); the closed form (28) of ; the optimality conditions (58); the bound (57) on the support; and inequality (56).
The result. In both regimes the loss of the dual bound is controlled by the primal gap times the sparsity of the iterate, with constants depending only on and ; the number of features does not enter. Since L0BnB seeks solutions with , the cheap dual bound obtained from an inexact primal solution is nearly as good as the exact one, which is what allows pruning without an interior-point solve at every node. The paper notes that with plain coordinate descent in place of Algorithm 2 the same argument gives in place of .
Formalizing it. The result is proved in the paper; it has no machine-checked proof. The mission produces a checked version of the main theorem with explicit constants, a formal model of what "output of an active-set method" means for the analysis, and reusable closed forms for the boxed soft-thresholding updates of an - or reverse-Huber-penalized box-constrained least squares problem.
The bound is not a consequence of weak duality alone: weak duality says only that each dual value is below the primal optimum, and says nothing about how far the constructed dual point is from the dual optimum. The obvious estimate, a Lipschitz bound on or summed over all coordinates, gives a loss proportional to . Getting instead requires showing that the dual contribution of every coordinate outside vanishes exactly, which uses the emptiness of through Proposition 3 and the closed forms (14)–(15) of one-dimensional nonsmooth box-constrained problems. On the support, the loss must be bounded using the structure of and at coordinates where hits the box, which is where and (58) enter.
Indices are Fin p; norms are explicit sums; is Real.sign with ; is max a 0. The unit norms of the columns of and of are hypotheses, never built into the definitions, and each theorem assumes only the ones it uses. is any point of the box minimizing over the box. The output of Algorithm 2 is modelled by its two properties used in the paper: and ("" encoded as " is not a minimizer"); the iterations are not formalized. and are arbitrary maximizers satisfying (25) and (27). The dual variables (23)–(24) are defined by their formulas; their optimality (Theorem 2, a separate mission) is neither assumed nor needed, and the goal is an inequality between explicit numbers.
Instantiations of . (29) is stated as (55): becomes with decided by . (30) is stated as (59): becomes . The proof's final rearrangement of (29), which counts instead of , is not used.
A formalization that takes , or , that drops the hypothesis , or that replaces the constants by an existential "" would be trivial or a different statement; the goal quantifies over every optimal , every box-feasible with and every maximizer , , with the explicit constants above.
Needed infrastructure: one-dimensional convex minimization on an interval with piecewise penalties, Cauchy–Schwarz for finite sums, and first-order optimality conditions for box-constrained composite problems. Proofs of any milestone are welcome independently.
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.
Second order dynamical systems with vanishing damping are continuous-time models of accelerated first-order methods. The system is the continuous limit of Nesterov's accelerated gradient method (Su, Boyd, Candès 2016), and its trajectories converge weakly to a minimizer of a convex when (Attouch, Chbani, Peypouquet, Redont 2018). Two modifications of this system have been studied separately. A Hessian-driven damping term damps oscillations and keeps the fast rates (Attouch, Peypouquet, Redont 2016). A Tikhonov regularization term with selects one minimizer, the one of minimum norm, and can turn weak convergence into strong convergence (Attouch, Chbani, Riahi 2018).
Boţ, Csetnek and László (arXiv:1911.12845v2, Math. Program. 2021) study the system with both terms. Their results split into two regimes according to how fast decays. This mission covers the slow-decay regime of §4.1, where and the trajectory approaches the minimum-norm minimizer in a weighted average sense.
Timeline. 2016: Su, Boyd and Candès derive the continuous model of Nesterov's method. 2016: Attouch, Peypouquet and Redont add Hessian-driven damping (, ) and prove fast rates and weak convergence. 2018: Attouch, Chbani and Riahi add Tikhonov regularization without Hessian damping and prove, among other results, strong ergodic convergence to the minimum-norm minimizer when . 2020: Boţ, Csetnek and László combine both terms and extend that ergodic result (their Theorem 4.2).
Let be a real Hilbert space, , , , and . The data satisfy the paper's General assumption:
A global -solution of system (5) is a twice continuously differentiable with
The set is nonempty, closed and convex, so it has a unique element of minimum norm, the minimum-norm minimizer . For the Tikhonov approximation curve is
the unique minimizer of a strongly convex function. Finally, measures the distance of the trajectory to , with derivative .
If and , then every global -solution satisfies
No rate and no constant is asserted, so the goal does not depend on any particular choice of .
The result shows that slow Tikhonov regularization still selects the minimum-norm minimizer when Hessian damping is added: the weighted time average of tends to zero and the trajectory comes arbitrarily close to infinitely often. The hypothesis is only , well below the threshold that the paper needs for its fast rates, and no growth condition on beyond the divergence of is imposed. It complements Theorem 4.4 of the same paper (a separate mission), which reaches full strong convergence under fast decay, , plus further conditions.
On the formal side, the theorem and its milestones are proved in the paper and in the cited literature, but none of them has a machine-checked proof. The work splits into an energy estimate for a nonautonomous second order ODE in a Hilbert space (Lemma 4.1), two facts about the Tikhonov curve that underlie the whole theory of Tikhonov regularization of convex problems (milestones 2 and 3), an integrated differential inequality (46), and a l'Hospital-type averaging step. The Tikhonov-curve facts are reusable for any formal treatment of viscosity selection and minimum-norm solutions.
The obvious attempt, a Lyapunov function that decreases along the trajectory and controls , fails because is not a stationary point of the perturbed system: in general. The distance to therefore need not decrease, and pointwise convergence is not available under the slow-decay hypothesis alone. The comparison point has to move along the Tikhonov curve , whose convergence to comes without a rate. The available bound controls only a weighted integral of corrected by , so the passage from (46) to the goal needs both and the divergence of the weight. In the formal setting the Tikhonov-curve limit is itself a nontrivial weak-compactness argument in a Hilbert space, which the paper does not spell out.
InnerProductSpace ℝ H, CompleteSpace H). is gradient g, and is the Fréchet derivative of gradient g at applied to . "Twice Fréchet differentiable" means and are differentiable; Lipschitz continuity on bounded sets is stated on every closed ball around the origin.Filter.liminf, whose value on an unbounded function is a default. is boundedness from above of the image of , and membership is integrability on .A multi-armed bandit learner repeatedly chooses one of several actions, observes only the loss of the chosen action, and tries to perform nearly as well as a single fixed action selected in hindsight. Two common loss models make different demands on the learner. In a stochastic model, each arm has a stable mean loss and the learner can gradually distinguish the best arm. In an adversarial model, losses may change with time and even respond to previous choices. A useful bandit algorithm should handle both without first being told which model generated the losses.
Zimmert and Seldin's Tsallis-INF paper analyzes one algorithm in both regimes. Its Theorem 1 gives a square-root guarantee against arbitrary adversarial losses and a logarithmic guarantee when the regret satisfies a self-bounding constraint. The latter condition includes the usual stochastic case with a unique best arm and also permits some adversarial deviations. This mission formalizes the reduced-variance (RV) estimator part of that theorem and six supporting statements from its analysis.
There are arms and rounds . At round , the environment supplies a loss for each arm . The learner draws an arm from a probability vector and observes only . The environment can base its current losses on the actions from earlier rounds. It may also randomize: a seed records its internal random choices, while its response to a history remains adaptive. The learner's random actions are then drawn successively from its history-dependent weight vectors. Expectations below average over both sources of randomness.
The pseudo-regret at horizon compares the learner's expected total loss with the lowest expected total loss of a fixed arm:
For the algorithm studied here, is the vector of estimated losses accumulated before round . The symmetric half-Tsallis regularizer is
The vector maximizes over the probability simplex. With the RV loss estimator, arm has baseline and estimate . This is an estimator based on the one observed loss, even though its update is a vector.
The self-bounding condition chooses gaps with exactly one zero, at , and a constant , as defined in Section 2. It requires
The gaps measure how costly it is to place weight on each non-best arm. In a stochastic bandit with a unique best arm, the usual expected-loss gaps give this relation with Zimmert and Seldin, §2 and §4.1.
The first target is an upper bound for every bounded, randomized adaptive adversary and every :
The paper prints in Theorem 1's display. Its proof yields , the coefficient formalized here; the difference is recorded in the moderation notes. The theorem's other displayed bounds retain their printed constants.
For , set and
Under the self-bounding condition, the same algorithm must satisfy
When , it must also satisfy . The goal states both clauses together with the adversarial guarantee. Its six milestones give a pathwise stability bound from Lemma 19, two per-round stability bounds from Lemma 11, two accumulated penalty bounds from Lemma 12, and a finite tail-sum estimate from Lemma 15.
The adversarial clause limits the cost of learning even when no arm has a persistent advantage. The self-bounding clause gives gap-sensitive logarithmic growth when the learner receives enough information to identify a unique best arm, while allowing the additive deviation . The two guarantees apply to the same weight rule and the same RV estimator Zimmert and Seldin, Theorem 1.
The paper proves its RV claims in prose and equations. A complete Lean proof would make the algorithm's randomized adaptive loss model, its path law, the estimator and the exact constants explicit in machine-checked form. The local theorem statements and definitions in this proposal compile with placeholder theorem proofs; the mission's mathematical results are therefore targets for formalization, not results already machine checked here. The setting definitions may also support formal analyses of other bandit algorithms with adaptive randomized losses.
The learner sees only one loss at each round, so the weight vector depends on estimates whose individual coordinates can be much larger than the observed losses. Bounding the change in the regularized potential by a simple worst-case estimate loses the dependence on the arm weights that the gap-sensitive result needs. The RV estimator reduces this difficulty but can take negative values, which changes the stability calculation. The self-bounding guarantee also compares the theorem's zero-gap arm with a best arm chosen in expectation at horizon ; for these need not coincide. That comparator issue is documented for audit.
The arms are Fin K, with the paper's first arm represented by Lean index zero. Histories are functions on natural-number rounds; entry zero is unused. A referenced published adversarial protocol supplies bounded losses and dependence on past actions. A probability measure on adversary seeds and a finite sum over action paths define the run law. The algorithm is an argmax predicate whose estimates are computed from its own weights and the observed loss. The real-valued simplex supremum defines ; makes that simplex nonempty, and its compactness bounds the objective. The goal requires measurable seeded losses, a probability measure, , in the self-bounding regime, and where is used. The penalty milestones take conditionally unbiased estimators that depend only on actions through their own round, are measurable, and have finite expected absolute size, as required for a sequential run and genuine expectations. Positive, non-increasing learning rates are explicit.
The argmax is taken over every simplex weight vector, and the run law includes every action path with its product probability. These choices rule out an arbitrary weight rule or a zero-valued integral masquerading as the algorithm. The development needs reusable facts about the simplex, measurability and integrability of the finite-path law, positivity of Tsallis-INF weights, and bounds on the real potential. Contributions that establish those facts or close the six milestone theorems fit this mission.
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.
A constraint satisfaction problem (CSP) asks for an assignment of values from a finite domain to variables so that every constraint, a tuple of variables required to lie in a fixed relation, is satisfied. The algebraic theory of CSPs rests on a Galois correspondence: the complexity of is determined by the set of its polymorphisms, because holds exactly when every relation of is definable from by a primitive positive formula (Geiger 1968; Bodnarčuk, Kalužnin, Kotov and Romov 1969), and such definitions translate into reductions (Jeavons 1998). This correspondence underlies the CSP dichotomy theorem.
Promise CSPs (PCSPs) relax a CSP by a promise: every constraint comes as a pair with , and the task is to tell instances satisfiable with the -relations from instances not even satisfiable with the -relations. Approximate graph colouring and -SAT are examples. Brakensiek and Guruswami (arXiv:1704.01937v2, §6.1) showed that the Galois correspondence survives this generalisation, with pp-definitions replaced by positive primitive promise definitions (ppp-definitions). This is the starting point of the algebraic approach to PCSPs later systematised by Barto, Bulín, Krokhin and Opršal (arXiv:1811.00970). Pippenger (2002) had earlier proved a variant of the correspondence for pairs of relations, not in this complexity-theoretic form.
Fix a finite domain . A relation of arity is a set , and a promise relation is a pair of relations of arity with . A family is indexed by a set of symbols with arities . In Lean it is a pair of relational structures 𝔸 𝔹 : RelStruct τ ar D, with = 𝔸.rel R, = 𝔹.rel R and (IsPromiseFamily).
A function is a polymorphism of if for every and all the tuple obtained by applying coordinate-wise, , lies in . is the set of polymorphisms of all arities .
A -PCSP is a finite list of clauses, each a symbol applied to a tuple of variables, with repetition allowed. It is read twice: as , with each clause asking its tuple to lie in , and as , with in place of . Let .
Definition (ppp-definability). A promise relation is ppp-definable from a finite family if there are and a -PCSP on variables such that
A family is ppp-definable from if each of its promise relations is.
For a finite family and a family over the same finite domain,
The printed Theorem 6.1 concludes a polynomial-time reduction from to . Its proof opens by reducing to the displayed statement, and the reduction follows from it by substituting gadgets.
The result. Theorem 6.1 shows that the complexity of depends only on : two finite families with the same polymorphisms have polynomial-time equivalent PCSPs. Hardness can then be read off from the absence of structured polymorphisms, and tractability from their presence. The paper's Boolean symmetric dichotomy (its Theorem 2.16) is organised in exactly this way, and the theorem justifies studying families of polymorphisms instead of families of relations. Section 6.2 of the paper, which characterises the sets of functions of the form , is its companion.
Formalizing it. The result and its proof are published, and no machine-checked version is known to exist. This mission produces a reusable definition of ppp-definability for promise families over arbitrary finite domains, built on the published relational-structure vocabulary PCSPBLPAff_Symmetric_Setting. It also produces the closure properties (weakening, transitivity) any later work on gadget reductions between PCSPs will need, and the encoding of the polymorphism relation as a gadget. The complexity-theoretic conclusion, a polynomial-time reduction, is not part of the mission.
The printed proofs are short, but each hides a construction. Transitivity requires substituting a gadget for every clause of an intermediate PCSP: the auxiliary variables of all gadgets are renamed apart, and EQUAL clauses are carried through unchanged. Proposition 6.3 requires one clause for every symbol and every -tuple of elements of , indexed by the finite set of such tuples and laid out on the coordinates of . The goal must handle (so , nullary functions, and with one point), where Proposition 6.3 as printed () does not apply. A tempting shortcut is to read the hypothesis only for arities . With that reading the theorem is false: for and , both unary, every function of positive arity is a polymorphism of both families, yet constant assignments satisfy every , so is not ppp-definable.
𝔸 𝔹 : RelStruct τ ar D with [Fintype τ] and IsPromiseFamily 𝔸 𝔹. is a promise family over any signature τ', possibly infinite; the conclusion is stated relation by relation.IsPolymorphism from the published setting file. PolSubset quantifies over every arity L : ℕ, including . This convention makes the goal true, and no hypothesis is added.Instance over the signature τ ⊕ Unit, whose new symbol has arity 2 and is EQUAL in both readings. The same clause list is read in withEqual 𝔸 (as ) and in withEqual 𝔹 (as ). PPPDefinable requires Ψ.n = k + ℓ. The first variables are Fin.castAdd ℓ, and is Fin.append x y. The two clauses of the definition keep the paper's quantifiers: existence of an extension on the side, and every satisfying assignment on the side. A formalization with two independent instances, or with both readings in , would trivialise the notion and is excluded.Fintype.card (Fin L → D) through any bijection e. The statements hold for every such ordering.PolyTime predicate or placeholder is introduced.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.
Approximating an unknown probability measure by the empirical measure of an i.i.d. sample is the basic operation of statistics, Monte Carlo integration, quantization and particle approximations of nonlinear PDEs. The natural way to compare with on is an optimal-transport cost, because it metrizes weak convergence together with convergence of moments. For many applications the mean of this cost is not enough: one needs to know how unlikely a large deviation is, for a fixed sample size .
The main consumer in operations research is data-driven distributionally robust optimization. Mohajerin Esfahani and Kuhn (Math. Program. 171, 2018) build Wasserstein balls around whose radius is calibrated so that the true distribution lies inside with probability ; their finite-sample guarantee (their inequality (7), quoted from this paper for ) is exactly a concentration inequality of the kind proved here. On Prove2Me that inequality appears as the hypothesis Concentration7 of WassDDRO.Consistency.Setting; Theorem 2 of this mission is the statement that discharges it.
Timeline. Bolley, Guillin and Villani (PTRF 137, 2007) proved concentration inequalities for on non-compact spaces, under assumptions that often included functional inequalities for , and for rather large deviations. Boissard (Electron. J. Probab. 16, 2011) gave bounds in for empirical and occupation measures. Boissard and Le Gouic (arXiv:1105.5263) and Dereich, Scheutzow and Schottstedt (Ann. IHP 49, 2013) studied the mean speed of convergence; the latter introduced the multiscale bound used here and obtained sharp moment estimates for a limited range of parameters. Fournier and Guillin (arXiv:1312.2128, 2013; PTRF 162, 2015) gave moment bounds for all and under a -th moment (their Theorem 1, mission I of this series) and the concentration inequalities of their Theorem 2, the subject of this mission, under integrability conditions only.
Fix and give the Euclidean norm . Let be a Borel probability measure on and i.i.d. with law . For the transport cost between probability measures is
where is the set of couplings, measures on with marginals and (no root is taken). The moment conditions use
The proof works with a multiscale distance . For let be the partition of into dyadic cubes of side . For measures on ,
For measures on one cuts space into the shells , , rescales each to (the measure ), and sums the compact distances with weights . Lemma 5 bounds by . The splitting separates the fluctuation of the shell masses, , from the fluctuation inside the shells, . A Poisson measure with intensity (a Poisson() number of i.i.d. points) and enter the compact case.
Assume or , and one of (1) with ; (2) with ; (3) with . Then for all , ,
with , or according as , , , and under (1), under (2), under (3). The constants depend only on , the parameters of the condition, the value of the moment and .
In attack order: Lemma 5 (the coupling bound ); Lemma 9 (Poisson moment generating function and tails); Proposition 8 (concentration for in the Poissonized compact case); Lemma 11 ( for ); Proposition 10 (the compact case of Theorem 2, ); Lemma 12 (binomial deviations); Lemma 13 (the tail of ); display (6) ().
The result. Theorem 2 gives, for every dimension and every in its range, a deviation inequality whose small- part has the same dimension-dependent exponent as the mean rate of Theorem 1, and whose large- part is governed only by the tail of . Under exponential moments the tail is again exponential; under a polynomial moment it is polynomial, which is the correct order. It is the input for finite-sample confidence radii in Wasserstein DRO, for non-asymptotic guarantees in quantization and for propagation-of-chaos estimates.
Formalizing it. The theorem is proved (2013, published 2015) and widely cited; no machine-checked proof of it, or of any rate for the empirical measure in transport cost, exists in Mathlib or on Prove2Me. The work is formalizing the known proof: Poisson and binomial concentration (Lemmas 9, 12), the local Poisson bound (Lemma 11), Poissonization and depoissonization (Propositions 8, 10), and the shell decomposition (Lemma 13, display (6)). Lemmas 9, 11 and 12 are general probability facts useful well beyond this paper.
The obvious route is a bounded-differences (McDiarmid) inequality for . On it is not available: moving a single sample point changes the cost by an amount that is unbounded, and the measures allowed here have only exponential or polynomial moments. Even on a compact set it bounds the deviation from the mean rather than from , so it gives nothing below the mean rate, and it does not see the dimension-dependent exponent of . The bound must hold at all scales of the dyadic decomposition simultaneously, while the cell counts of a multinomial sample are dependent, and in the non-compact case the masses of far-away shells, which are rare events, must be controlled with a tail that degrades exactly as the moment condition allows.
is EuclideanSpace ℝ (Fin d) with ; the Euclidean norm matters, since involves the diameter of . The sample is under the product measure , and is the published WassersteinDRO.Duality.empiricalDistribution; couplings are the published WassersteinLinOpt.Ball.couplings. Costs, moments, , , and expectations are valued in (lower Lebesgue integrals and -valued series), so no bound can hold through a junk value of a divergent integral. Probabilities are the product measure applied to the event. is represented by its law, a Poisson() mixture of i.i.d. samples, as on p. 13. Poisson and binomial laws are Mathlib's poissonMeasure and binomial.
Constants: in each of the three parts, the condition's parameters, the moment value (resp. ) and are fixed before , and come after. A formalization with fixed before the constants would be trivial (the constants could absorb ), and one stating the goal as the sum of the bounds for and would assume the proof; the goal mentions neither , , nor .
Departures from the print, each disclosed in the statements: the page writes for ; Theorem 2 opens with "" but prints only for , , , so it is posed for or ; Proposition 8's "" is relaxed to that range (its proof does not use , and Theorem 2 needs it for every ) (Proposition 10 is posed, as printed, for every ); Lemma 12 assumes and a positive success probability, without which (a) and (b) are false. "Supported in " is -null complement of .
The definitions of , , Notation 4 and Lemma 5 duplicate those of mission I of the series and are to be merged later. Contributions on Poisson and binomial concentration, and on transport costs between discrete measures, are reusable and 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.