Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The quantum linear systems problem asks, given a sparse Hermitian matrix with condition number and a procedure preparing a state , to prepare a state close to . Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in and but grows like in the target precision , because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to , an exponential improvement.
The reduction has two parts. A quantum part implements a linear combination of unitaries applied to , and turns any function that is -close to on the spectrum of into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.
For a real number (a condition number: the ratio of the largest to the smallest singular value), the domain is
A function is -close to on a set if for all .
The Chebyshev polynomials of the first kind are , and ; those of the second kind satisfy the same recursion with , .
For natural numbers let
the probability of more than heads in fair coin flips. The tamed inverse (74) is , and the odd Chebyshev series is
In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters and below.
With and , the truncated series
is -close to on , for every and .
Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the -th power of the rotation block in terms of and , and Proposition 9 (p. 9), the perturbation bound for normalized states.
Lemma 14 provides a polynomial of degree whose Chebyshev coefficients have total weight , approximating uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement (Lemma 16), it gives the query complexity of Theorem 4. The same polynomial approximation of reappears in later work on quantum singular value transformation and matrix inversion.
All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity , but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for . The formalization produces a checked uniform approximation of with explicit, non-asymptotic parameters.
The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all , and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which or is negative.
All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum is over Finset.range n, so the series of (55)/(88) truncated at is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.
The formalization commits to the following conventions, each disclosed in the item it affects.
A trivializing reading is ruled out: the goal fixes the page's , and constant , so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain excludes the origin, where Lean's would make closeness to meaningless.
Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on , binomial tail bounds, and uniform approximation of . Contributions of general lemmas of this kind are welcome.
Steepest descent is the oldest method for unconstrained minimization: to minimize a smooth function , it moves from the current point along the negative gradient . It is the prototype of every first-order method, and its worst-case evaluation complexity — how many iterations it may need before the gradient norm drops below a tolerance — is the reference point against which faster methods are measured.
For a function that is bounded below and has a Lipschitz continuous gradient, steepest descent with a suitable step-length rule reaches within iterations (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Whether this bound is tight on nonconvex problems remained open until Cartis, Gould and Toint (preprint 15 October 2009; SIAM J. Optim. 20(6), 2010) built explicit one-dimensional examples showing that it is essentially sharp. The same paper shows that Newton's method can be as slow, and that the bound of cubically regularized Newton methods is also tight; those results are the other missions of this series.
Timeline:
Let be twice continuously differentiable, bounded below, with a derivative that is bounded and Lipschitz continuous. The paper calls these standing assumptions AS.0. Write for the gradient.
Steepest descent with step lengths starts at and sets
The step lengths are only required to lie in a fixed interval (condition (2.6))
Such step lengths can be produced by a Goldstein–Armijo linesearch, which accepts a step when the decrease lies between and for fixed constants .
Fix and put . The mission's definitions (namespace SlowConvergence.SteepestDescent) record the paper's prescribed data: iterates xk, steps sk, values fk, gradients (gk), and the quintic pieces p with the quantities , , of (2.11)–(2.15).
For every , every and every step-length sequence with , there is satisfying AS.0 on all of on which the steepest descent run from has
No constant (Lipschitz constant, gradient bound, lower bound) is fixed in the goal; only its existence is asserted.
The result. Since is arbitrary, the example shows that the upper bound for steepest descent cannot be improved to for any under AS.0, even with a standard Goldstein–Armijo linesearch. It separates steepest descent from second-order methods with better worst-case bounds, and it is the template for the Newton and regularized-Newton examples of the same paper. A matching upper bound for gradient descent with step is formalized elsewhere on the platform (ShiOptRates.gd_exact_rate); together the two describe the complexity of the method up to the exponent .
Formalizing it. The result is proved on paper; to our knowledge no machine-checked version exists. The mission adds a statement in which the method, the function class and the iteration count are fixed precisely. It also corrects three printed slips that a formal check exposes: the iteration count is off by one, the Goldstein–Armijo interval is printed reversed, and an intermediate step of (2.17) is false while its end bounds hold.
Matching prescribed values and gradients at the iterates is easy one point at a time. The difficulty is doing it with uniform control. The interval lengths shrink like , so a naive interpolant has second derivatives growing with , and the gradient is then not globally Lipschitz. The prescribed values must also decrease at a rate whose sum stays finite, or the function is unbounded below. Both constraints pin the exponent: the construction works only because makes the iterates escape to infinity while keeps finite. A further step remains: the paper's function lives on and must be extended to all of without losing any property of AS.0.
The problem is one-dimensional: f : ℝ → ℝ, the gradient is deriv f, and the second derivative is iteratedDeriv 2. AS.0 is ContDiff ℝ 2 f, BddBelow (Set.range f), a global bound on |deriv f|, and LipschitzWith L (deriv f). Every property holds on all of ; the paper constructs on and says it extends smoothly to the negative reals, and that extension is part of the goal.
Conventions:
Real.rpow with base .Infrastructure needed: quintic Hermite interpolation on intervals, gluing piecewise polynomials into a function on along an unbounded increasing knot sequence, a extension to the negative reals, and bounds for real -series. The gluing lemma and the extension are reusable for the Newton and regularized-Newton missions of the series. Contributions of any milestone, of a construction of the glued function of (2.16), or of a direct proof of the goal are welcome.
Quasi-Newton methods replace a costly exact Hessian with an operator updated from successive changes in position and gradient. A secant update must map the observed step to the observed gradient difference . Many operators satisfy that one equation, so the choice of update needs another criterion. Gilbert and Lemaréchal's working paper studies variable-storage quasi-Newton algorithms and, in its Annex, characterizes familiar update formulas by how little they change the previous operator. The Annex treats real Hilbert spaces, rather than only matrices on Euclidean space, and allows the underlying scalar product and the weighting operator to vary. Its least-change characterization is the subject of this mission.
The source is the August 1988 IIASA Working Paper WP-88-121. A revised journal article appeared in 1989, but the theorem numbers and printed page references here belong to the working paper. The work is a formalization of a result proved in that paper; the mathematical question is not open.
Let be a complete real inner-product space. A continuous linear operator is the current Hessian approximation. A step and a gradient difference determine the quasi-Newton equation for the updated operator . Write , where is the perturbation. The source restricts to the Hilbert–Schmidt class , so its size can be measured by an orthonormal basis :
The index set need not be countable; membership in means the displayed family is summable. The value is independent of the chosen orthonormal basis. For , the paper's bracket operator is . The order of its arguments matters.
The nonsymmetric feasible set is . For a self-adjoint , the symmetric problem uses . A bijective continuous operator weights the symmetric objective . The vector records how this weight changes the update. Both the feasible set and the weighted objective matter: taking a minimum over every bounded operator would change the problem.
The goal is Proposition A.2 on printed p. 28 of the working paper. Suppose , is bijective, and . With and , define
The target asserts that belongs to and is the unique minimizer of over . Its formula depends on only through . No positivity condition on or on is part of this result.
The milestones follow the source's supporting statements in order. They establish that the Hilbert–Schmidt sum is independent of the orthonormal basis and defines a norm on its domain; that the operator norm is bounded by this norm and the Hilbert–Schmidt class is stable under multiplication by bounded operators; the bracket identity ; the two bracket composition identities; Proposition A.1, the unique nonsymmetric least-change update for ; and its instance , Broyden's update (A.5). The goal adds self-adjointness and a single two-sided weight.
The Annex then draws consequences of the goal, which are further milestones: the instance is the psb (Powell symmetric Broyden) update; Proposition A.3 states that for nonzero a self-adjoint positive operator ( for ) with exists if and only if for a bijective , if and only if ; with the weight becomes and (A.7) becomes the dfp (Davidon–Fletcher–Powell) update (A.8); and (A.9) is a product form of the dfp update from which its positivity follows when is self-adjoint positive and .
The theorem gives a precise optimization property to a rank-two symmetric secant formula. It identifies the operator selected by the weighted least-change criterion and guarantees there is no other feasible minimizer with the same value. Taking the weight to be the identity yields the psb update, and taking with yields the dfp update, so two of the classical symmetric secant formulas are least-change updates for different weights. Proposition A.1 similarly characterizes the rank-one update that becomes Broyden's formula when its right weight is the identity. These consequences explain why the familiar formulas arise from a common variational question, as the Annex states.
The paper supplies a mathematical proof. The remaining formalization work is to represent the Hilbert–Schmidt class, its norm and ideal property, the weighted objectives, and the exact minimization claims in Lean, then prove those claims. Mathlib supplies Hilbert spaces, Hilbert bases, bounded linear maps, adjoints, and the rank-one operator corresponding to the paper's bracket. The statements drafted for this mission compile, but they carry sorry and have no machine-checked proof from this mission yet. A completed development would leave reusable Hilbert–Schmidt and rank-one operator results beyond this quasi-Newton application.
The secant equation alone fixes an operator on only one vector. Even in two dimensions, a rank-one perturbation can satisfy that equation while failing to preserve self-adjointness. Requiring self-adjointness leaves many candidates, and minimizing the two-sided weighted Hilbert–Schmidt norm must distinguish exactly one of them. In infinite-dimensional spaces the norm also has a domain: some bounded operators have an infinite square sum. A formulation that silently assigns a finite default value to a nonsummable operator could turn the least-change claim into a different assertion. These are the mathematical and formal obstacles the milestone list exposes.
Lean uses an arbitrary complete real inner-product space, with no finite-dimensional or separability assumption, and an arbitrary HilbertBasis index type. Each theorem takes a basis parameter; the basis-independence milestone states why this represents the paper's basis-free norm. The reusable definitions for the bracket and the Hilbert–Schmidt square sum are separate from the paper-specific feasible sets. bracket u v abbreviates Mathlib's rankOne ℝ u v, with paired with the input. A bijective bounded operator is represented by a continuous linear equivalence ; the bounded inverse theorem makes this equivalent to the paper's bijective member of . The definition of applies the adjoint of to .
Lean's real tsum has a default value when the family is not summable, so the Hilbert–Schmidt norm is used as a norm only for operators satisfying the explicit summability predicate. Both and include that predicate. The ideal-property milestone covers the weighted operators in the two objectives. The hypothesis is exactly the proposition's condition; it entails , so no extra nonzero-denominator hypothesis is imposed. The statement spells out “unique solution” as feasibility, minimality over every feasible perturbation, and equality of every feasible minimizer with . The paper prints “problem (A.5)” in Proposition A.2, but (A.5) labels Broyden's displayed formula; its preceding paragraph defines the relevant symmetric minimization as (A.6). This mission formalizes (A.6).
In Proposition A.3 and (A.9), "positive" is the paper's strict notion for , not the non-strict positivity of Mathlib. The identity (A.9) is stated for self-adjoint and , the setting of the Annex's symmetric problem; the paper's sentence before the psb formula repeats the "(A.5)" misprint and is read as (A.6) in the same way.
The definition layer, basis independence, operator-ideal property, bracket results, both least-change propositions, and the Broyden, psb, dfp and positivity statements are welcome proof targets. The scaling results of §4.1 are outside this mission.
Modular composition asks, given univariate polynomials over a ring, for . It is the bottleneck step in the classical algorithms for factoring univariate polynomials over finite fields (Cantor–Zassenhaus, von zur Gathen–Shoup, Kaltofen–Shoup), for irreducibility testing and for computing minimal polynomials. Brent and Kung (1978) gave an algorithm using operations for degree , and for three decades no algorithm with a near-linear operation count was known in general.
Kedlaya and Umans (Dagstuhl Seminar Proceedings 08381, 2008; journal version SIAM J. Comput. 40(6), 2011, doi:10.1137/08073408X) obtained near-linear modular composition over finite fields, and with it asymptotically faster algorithms for factoring polynomials over finite fields. Their route has two halves: a reduction of modular composition to multivariate multipoint evaluation (Section 3), and new fast algorithms for the latter (Sections 4 and 6). This mission formalizes the correctness of the first half, Theorem 3.1. The paper notes that Shoup and Smolensky used essentially the same transformation in an unpublished 1992 manuscript.
Throughout, is an arbitrary commutative ring. Variables are indexed from .
MULTIVARIATE MULTIPOINT EVALUATION (Problem 2.1): given with individual degrees at most and points , output .
MODULAR COMPOSITION (Problem 2.2): given with individual degrees at most , and of degree at most with the leading coefficient of a unit, output , the unique with and .
The inverse Kronecker map (Definition 2.3) is the -linear map that sends the monomial to , where is the base- expansion. It trades individual degree for number of variables: every individual degree of is below .
The algorithm of Theorem 3.1 takes , sets and , receives points whose differences are units, and
for all , , with individual degrees , of degree with a unit, and distinct with unit differences. The right-hand side is stated through the characterization of the remainder (divisibility by and degree below ).
A supporting theorem states that the interpolation formula over a commutative ring (Figure 1) recovers every polynomial of degree from its values at nodes with unit differences.
Theorem 3.1 says that modular composition is no harder than one multivariate multipoint evaluation with variables, individual degrees below , and points, up to quasi-linear univariate work. Combined with the paper's fast multipoint evaluation algorithms this gives modular composition over in bit operations, and from there the paper's improved bounds for polynomial factorization, irreducibility testing, minimal polynomials and modular power projection (Sections 7–8). The converse reduction (Theorem 3.3) shows the two problems are essentially equivalent.
The paper's proof of correctness is a short paragraph; the operation counts are the paper's main concern. This mission makes the correctness exact: the algorithm is defined step for step, and its output is proved equal to the specification. As far as the platform's corpus shows, neither the inverse Kronecker map nor this reduction has a machine-checked statement; the running-time half is not part of this mission.
The obvious argument substitutes for and invokes the inverse Kronecker identity. Two points keep this from being immediate. First, is linear but not multiplicative, and it discards base- digits beyond position ; the identity holds only for individual degrees at most , which here requires . Second, the algorithm never sees itself, only its values at points: interpolation recovers it only if its degree is below , which is why Step 2 reduces modulo before substituting, and interpolation over a ring (not a field) needs the unit-difference hypothesis throughout. Mathlib's Lagrange interpolation is stated over fields, so the ring version must be handled directly.
CommRing R); there is no field or nontriviality assumption.Fin m; the new variables are Fin m × Fin ℓ; points are Fin N'.MvPolynomial.degreeOf; "degree at most " is natDegree ≤ N - 1.Nat.clog d₀ d and ; is not a free parameter.Ring.inverse of the node differences.MvPolynomial.eval, which is exactly the output of Problem 2.1.Step 5 is the interpolation formula applied to the computed values and nodes alone; it is not defined as the polynomial , and the goal is the six-step output, not the congruence alone, so the statement cannot be closed by unfolding definitions.
Useful infrastructure, reusable beyond this mission: base- digit manipulation of exponent vectors, Lagrange interpolation over commutative rings with unit node differences, and remainders modulo polynomials with unit leading coefficient. Proofs of any milestone, and of the supporting interpolation theorem, are welcome independently.
Many objectives in statistics and machine learning are neither smooth nor convex, yet are well behaved in a weaker sense: robust phase retrieval, blind deconvolution, robust PCA and training with piecewise-linear losses all lead to weakly convex functions, functions that become convex after adding a fixed quadratic. For such functions the plain subgradient method remains the method of choice, and the natural question is how fast it reaches approximate stationarity. Davis and Drusvyatskiy (SIAM J. Optim. 2019) gave the first such rate, measured by the gradient of the Moreau envelope, of order .
Das Gupta, Van Parys and Ryu (Math. Program. 204 (2024) 567–639) introduced BnB-PEP, a branch-and-bound method for solving nonconvex performance-estimation problems to global optimality, and used it to construct optimal and efficient first-order methods. Their one fully analytical result (§6.3) is a new potential-function analysis of the subgradient method on weakly convex functions with bounded subgradients. It produces an explicit stepsize and a rate that strictly improves on the Davis–Drusvyatskiy bound for all large enough . The certificate was found numerically; the paper then gives a classical proof that can be checked by hand. This mission formalizes that result.
Work in with the Euclidean norm. A function is -weakly convex if is convex. For such , a vector is a subgradient of at , written , when
The class consists of the -weakly convex whose subgradients all satisfy . Since exactly when , the paper sets and writes ; here the normalized bound is written (Lean: InWeakClass 1 L f, with subgradients IsWeakSubgrad 1 f x g).
For the proximal point is the unique minimizer of , and the Moreau envelope is the minimum value
(Lean: SAGA.Convex.IsProxPoint f (1/ρ̂) x y and moreauEnv ρ̂ f x). The envelope is continuously differentiable, and its gradient is a subgradient of at the prox point . With , the paper's choice, small means that is near a point that is nearly stationary for .
The method is for , where each is arbitrary. One writes , , assumes a global minimizer and the initial condition , and sets .
For the stepsize , provided ,
The bound holds for every choice of subgradients along the run.
For , , and , the potentials satisfy
In proof order: the Moreau-envelope facts of §6.3.1; the one-step inequality (32) for an arbitrary point; the telescoping display after (32); the closed form (44) of with nonnegativity; Theorem 1; the closed form (45) of its bound in ; the majorant (46) with Bernoulli's upper bound; and the minimizer of (46) with its value.
The result. Corollary 1 gives an explicit, non-asymptotic rate for the most basic method of nonsmooth nonconvex optimization, with explicit constants and an explicit stepsize. As the bound is asymptotic to , and the paper shows it is strictly below the earlier bound once . It also bounds . It shows that computer-assisted performance estimation can produce closed-form guarantees beyond the convex, interpolable function classes where PEP is usually applied.
Formalizing it. The result is proved on paper twice (pp. 622–627), but nothing about weakly convex functions, their subdifferential or the Moreau envelope in the nonconvex regime is formalized on the platform, and the convergence analysis has not been machine-checked. A complete development formalizes the potential-function proof and supplies reusable facts about weakly convex functions and the Moreau envelope.
The scalar part of the argument ((44)–(46) and the plug-in) is elementary algebra and one Bernoulli inequality. The analytic weight sits in two places. First, the Moreau envelope of a nonconvex function: showing that the real infimum is attained at the prox point, that the envelope is differentiable with gradient , and that this gradient is a subgradient of at with the weak-convexity modulus (not the modulus that the prox inequality gives directly). Second, inequality (32): it is not a consequence of convexity, since is not convex, and it must hold for an arbitrary current point and an arbitrary subgradient, with parameters fixed in advance. The obvious route through descent of itself fails: need not decrease for nonconvex , which is why the potential uses the envelope at the iterates.
The carrier is EuclideanSpace ℝ (Fin d), and is real-valued and defined everywhere. The weak-convexity modulus is normalized to , and the Lean name L is the paper's ; the general class follows by scaling and is not stated. The subdifferential is the weak-convexity inequality above. For weakly convex it equals the Clarke, Fréchet and limiting subdifferentials, so it is the paper's abstract in every admissible instance. The convex subdifferential of is not used: it can be empty for nonconvex and would make the statements vacuous. The run is given by sequences x g y : ℕ → E, with g k an arbitrary subgradient at x k for , and y k tied to x k by IsProxPoint f (1/2) for . is not free: it is . The Moreau envelope is a real ⨅; it is finite and attained in this regime, and the first milestone proves this. The parameters of Theorem 1 are pinned by hypotheses, not chosen existentially.
Two hypotheses are made explicit. Corollary 1 is stated "in the setup of Theorem 1", which requires ; for the prescribed stepsize this is , and it is carried as the hypothesis . It fails for and whenever is large relative to . Inequality (32) is stated for one arbitrary step, under the nonnegativity of the alternate proof's weights (, , ). The minimizer is assumed, as in the paper; the remark on p. 627 that suffices is not used.
Useful contributions include basic lemmas on weakly convex functions (existence of subgradients, strong convexity of the prox subproblem), differentiability of the Moreau envelope for , the weighted-sum identity behind (32), and Bernoulli's upper bound for .
Nash's existence theorem for finite games is a fixed-point theorem: one writes down a continuous map from the set of mixed strategy profiles to itself whose fixed points are exactly the Nash equilibria, and applies Brouwer's theorem. Nash's own map (Nash 1951) divides by , and the choice of map matters as soon as the question is computational rather than existential.
Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) introduce the class FIXP of fixed-point search problems whose maps are given by algebraic circuits over and rational constants, and show that computing a Nash equilibrium of a 3-player game is FIXP-complete. In Section 4 they ask which gates are really needed. Since the Nash problem is complete, it suffices to find, for every game, a map with the same fixed points and a cheaper circuit. They define a division-free map , prove that its fixed points are precisely the Nash equilibria (Lemma 20), show that it is computed by a circuit with gates (Lemma 21), and conclude that FIXP is unchanged if circuits use only and rational constants (Theorem 22). The same map, defined as a Euclidean projection, appears earlier in Gul, Pearce and Stacchetti (1993).
This mission formalizes the game-theoretic content of that section: the map , its well-definedness, and Lemma 20.
A finite game has a finite set of players ; each player has a finite, nonempty set of pure strategies, and a payoff function assigns a real number to every pure strategy profile. A mixed strategy of player is a vector with and ; a mixed profile is one mixed strategy per player, and denotes the set of mixed profiles (the product of the players' unit simplices). The expected payoff is the expectation of when the players draw their strategies independently according to . For , is player 's expected payoff when plays and the others play according to . A Nash equilibrium is a mixed profile such that no player can raise by switching unilaterally to another mixed strategy.
For a vector indexed by pairs , let and . For each player define the function of a real variable
It is continuous, nonincreasing, strictly decreasing below and zero above it, so there is a unique threshold with . The division-free map is
In the Lean development, is DGPNash.NashMap.purePayoff u x i j, is hVal, is fSum, is threshold and is G, all in the namespace FixpNash.DivFree.
For every finite game with nonempty strategy sets and every ,
This last milestone is off the goal's path; it is the formula behind the division-free circuit.
Lemma 20, with Brouwer's theorem and the continuity of , gives an elementary proof of Nash's theorem. With Lemma 21 it shows that the Nash equilibrium problem, and therefore every FIXP problem, is represented by circuits without division; the paper uses this to obtain Theorem 22. The pure-deviation criterion of milestone 3 is the standard test for equilibria and is used throughout equilibrium computation. The closed form of milestone 6 is the threshold of the Euclidean projection onto the simplex, used widely in optimization.
All of these results are proved in the paper. The mission produces machine-checked versions. No platform item states Lemma 20 or the pure-deviation criterion for AGT.IsMixedNash. Related posed items, with other conventions, are credited below rather than reused: the thresholds of the simplex projection in the Condat 2015 series (SimplexProj.Condat.simplex_projection_threshold, threshold_root_bracket, subsequence_mean_le_threshold, stated for the projection on with a radius), and the best-response fixed-point characterization in supermodular games (Supermodularity.Games.equilibrium_iff_fixed_point_v2, a different map). The paper also remarks, without proof, that is the point of closest to . That remark is not a target here.
The map is defined through an implicitly determined threshold. In the formalization the threshold has to be a definition that does not depend on a proof, and every statement about it rests on the existence and uniqueness of the root of . This is an intermediate-value argument for a piecewise linear function of a finite sum of terms. Its strict monotonicity holds only below , and the argument must use that is nonempty.
The equivalence itself needs the multilinearity of the expected payoff: and, more generally, the payoff of a deviation to a mixed strategy is . In the agt_games representation the expected payoff is a sum over all pure profiles of products of probabilities, so this identity must be extracted from the product structure rather than read off.
The game uses the published agt_games vocabulary: players form a finite type ι with decidable equality, the strategies of player i a finite type S i, payoffs are real (the paper's are rational, so this is a generalization), mixed profiles are real weight functions satisfying AGT.IsMixedProfile, and Nash equilibrium is AGT.IsMixedNash (no profitable deviation to any lottery). The pure-strategy payoff is the published DGPNash.NashMap.purePayoff.
The following readings are explicit in the Lean and implicit on the page:
∀ i, Nonempty (S i)). The paper assumes this tacitly; without it is empty and does not exist;AGT.IsMixedNash and the pure-deviation inequalities for a mixed profile;Contributions welcome: proofs of any milestone. The multilinearity of AGT.expectedPayoff in one player's strategy, and the existence and uniqueness of the threshold of a finite sum of hinge functions, are reusable beyond this mission.
Reductions that prove hardness for Nash equilibrium computation encode a computation (a circuit, a fixed-point problem) into the probabilities that players put on their strategies in every equilibrium. For the encoding to be meaningful, the designer has to control how each player distributes probability across groups of strategies, independently of the incentives that carry the computation. A standard tool for this is a generalized matching pennies game: each "computing" player is paired with an adversary who is penalized for guessing which group the computing player is playing, and who therefore forces that player to spread probability evenly over the groups. Versions of this device appear in the PPAD-hardness reductions of Daskalakis, Goldberg and Papadimitriou and of Chen and Deng, and in Etessami and Yannakakis's Theorem 4, which reduces the SQRT-SUM and PosSLP problems to deciding, with a promised gap, whether the unique Nash equilibrium of a 4-player (or 3-player) game plays a given pure strategy (Etessami–Yannakakis, SIAM J. Comput. 2010).
This mission formalizes the version of the device that Etessami and Yannakakis isolate as Lemma 6 (p. 24 of the authors' manuscript), with the explicit constants of their construction.
A finite game has a finite set of players; each player has a finite set of pure strategies, and receives payoff at each pure profile . A mixed profile assigns to each player a probability vector on ; players randomize independently, and is 's expected payoff. Write for the expected payoff of when plays the pure strategy and everyone else plays according to . A Nash equilibrium is a mixed profile such that no player can raise their expected payoff by switching unilaterally to another mixed strategy.
Fix two players . The pure strategies of are partitioned into blocks, in one-to-one correspondence with the pure strategies of . This is recorded by a surjective map : the block of a strategy of corresponds to the strategy of . The total probability of block under is
The payoffs of have the block matching-pennies form with first term , constant and parameter when
does not depend on , , and has at most strategies. Player is rewarded for "matching" the strategy of with the block it plays; player loses when matched. The term is arbitrary otherwise: in the paper it carries the gate gadgets of the circuit.
For every Nash equilibrium of a game in which have the block matching-pennies form,
Part 1 says divides its probability evenly among its blocks (each block gets ); part 2 says the matching player uses every strategy.
In the paper, Lemma 6 is what makes every unprimed player of the 10-player game of Section 3 spread probability (or ) on each block, so that the split of probability inside a block can carry the value of a circuit gate, and the gate gadgets of Lemma 7 act on correctly normalized quantities. Without it, the gadgets' analysis does not apply. The lemma is stated for an arbitrary game containing such a pair, so it is reusable for any reduction that pairs computing players with matching-pennies adversaries.
The result is proved in the paper; nothing in it is open. As far as the platform and its index show, no machine-checked version exists: the platform has the 2×2 matching pennies game (PotentialGames.matchingPennies_no_pureNash, which shows it has no pure equilibrium) and our CalibratedCE.Convergence.MatchingPennies (Foster–Vohra's example), neither of which is the block game. This mission produces a checked version of the lemma with the paper's constants, together with the support property of mixed Nash equilibria for the agt_games vocabulary, a basic fact other game-theory missions can import.
The argument is short; the difficulty is in the accounting. The expected payoff of a pure strategy of mixes the arbitrary term , evaluated under the product distribution of all other players, with the matching term, which depends only on . Separating the two requires that depends only on and that the expected-payoff sum factors over independent players. The constants also interact: the lower bound uses that has at most strategies, so that some strategy of has probability at least , and the comparison of the two bounds needs , which is exactly . A tempting shortcut, comparing only with the average block probability, does not identify which strategies of vanish; the argument goes through the set of maximum-probability blocks.
The game uses the published agt_games vocabulary: players and strategies are arbitrary finite types ι, S : ι → Type*, payoffs are real (u : ι → (∀ k, S k) → ℝ), mixed profiles are families of probability vectors, and AGT.IsMixedNash allows deviations to arbitrary mixed strategies. The pure-strategy payoff is the published DGPNash.NashMap.purePayoff. The block structure is a surjective map ; surjectivity is the "1-1 correspondence" of blocks with strategies of (an empty block would make the lemma vacuous). The definition item packages the form "given above" as FixpNash.Blocks.IsBlockPair.
Explicit readings of the page:
The degenerate case is allowed and reads . A formalization in which has no strategies, or a block is empty, would make the lemma vacuous; the surjectivity of and the definition of a mixed profile exclude this. Contributions welcome: proofs of the support property (reusable well beyond this mission), of the two payoff bounds (a factorization of the expected payoff over independent players), and of the lemma.
For games with three or more players, Nash equilibria can be irrational, so they cannot in general be computed exactly. Bubelis made this precise: any real root of any univariate polynomial arises as the probability of a particular strategy, or the payoff of a particular player, in a Nash equilibrium of a three-player game whose payoffs depend on the coefficients of the polynomial (Bubelis 1979).
Etessami and Yannakakis (SIAM J. Comput. 39 (2010)) restate Bubelis's construction as Lemma 7, in a form that controls the equilibrium probabilities rather than a payoff, and that guarantees the equilibrium is unique. They use it, for linear polynomials, as the single gadget behind every arithmetic operation in their reduction from PosSLP and SQRT-SUM to deciding properties of the unique Nash equilibrium of a three- or four-player game (their Theorem 4). The uniqueness clause is what makes the composed game itself have a unique equilibrium.
Fix an integer and real coefficients , and let
so is the coefficient of ; the leading coefficient may vanish.
The gadget is a game with three players. The primary player 1 has the strategies ; the auxiliary players 2 and 3 each have the strategies . For a pure profile , and with the indicator of a predicate , the payoffs are
The auxiliary payoffs do not depend on and take values in .
A mixed profile assigns to each player a probability vector on its strategies; the players randomize independently. Player 's expected payoff is the expectation of its payoff under the product distribution, and is its expected payoff when it switches to the pure strategy . A Nash equilibrium is a mixed profile in which no player can raise its expected payoff by switching unilaterally to any other mixed strategy. A profile is fully mixed if every pure strategy of every player has positive probability. Throughout, , and , are the equilibrium payoffs of players 2 and 3.
Assume , , and that has a unique root in . Then every Nash equilibrium of satisfies
and if and , then has exactly one Nash equilibrium, and it is fully mixed.
Milestones 2–4 hold for every coefficient vector; only milestone 5 and the goal use the hypotheses on .
The lemma is the arithmetic engine of the hardness results of Etessami and Yannakakis: a polynomial equation in one unknown is solved, exactly and uniquely, by the equilibrium of a fixed-size game whose auxiliary payoffs do not depend on the equation. With linear, the gadget implements addition, multiplication and division of probabilities in ; with higher degree it implements roots and fractional powers. Without the uniqueness clause, the composed games of Theorem 4 could have spurious equilibria, and the reduction would not apply to games promised to have a unique equilibrium.
The result is proved in the paper (pp. 25–26, following Bubelis). As far as is known, no part of it is machine-checked: there is no formal statement of Bubelis's gadget, and the support property of Nash equilibria is not on the platform in this vocabulary. This mission produces the first formal statement and proof of the gadget's equilibrium characterization, including the existence half of "has a unique Nash equilibrium", which the paper takes from Nash's theorem but which here is a concrete profile to check.
The gadget's equilibria are those of a three-player game, so the payoffs are cubic in the probabilities and no linear-programming argument applies. The obvious first idea, writing down the indifference conditions of players 2 and 3 and solving them, presupposes that every strategy of player 2 is played; nothing guarantees that in advance, and the profiles in which some strategies are unplayed have to be excluded. The boundary cases and are not covered by an indifference argument for the primary player and need the sign conditions and separately. The strategy of player 3 is pinned down only when , which is why the uniqueness part of the lemma excludes the endpoints. Finally, existence of the equilibrium is part of the statement and cannot be delegated to Nash's theorem, which is not available on the platform.
The game uses the published vocabulary agt_games (mixed profiles as weight functions, AGT.expectedPayoff, AGT.IsMixedNash with mixed deviations) and DGPNash.NashMap.purePayoff for . The players are a three-element type primary | aux2 | aux3; strategies are Fin 2 and Fin (m+1), 0-based as on the page. The coefficients are c : Fin (m+1) → ℝ and is the explicit sum with natural-number exponent; the congruence is addition in Fin (m+1); for every , including .
Explicit readings committed to:
∃! over mixed profiles);The goal is not trivialized by a pure-strategy notion of equilibrium (deviations are mixed), by dropping uniqueness of the root (without it is false), or by reading "unique equilibrium" as uniqueness alone. For the hypotheses cannot hold, as on the page.
A complete development needs the support property (reusable for any finite game), the linearity of expected payoff in one player's strategy, and finite-sum manipulations for the geometric weights . Contributions of general lemmas about AGT.IsMixedNash and purePayoff are welcome and reusable well beyond this mission.
Methods for smooth unconstrained minimization, , are compared by how many evaluations of and of its gradient they need, in the worst case, to reach an approximately first-order critical point, an iterate with . For steepest descent with a Lipschitz gradient the answer is (Nesterov, Introductory Lectures on Convex Optimization, 2004, p. 29). Nesterov and Polyak (2006) showed that globally minimizing a cubic regularisation of the second-order model, with the exact Hessian and a global Lipschitz constant, improves this to .
The adaptive regularisation with cubics (ARC) framework of Cartis, Gould and Toint makes that idea practical: the Hessian is replaced by an approximation , the Lipschitz constant by an adaptive weight , and the global model minimizer by any step that does at least as well as a Cauchy point. Part I (Math. Program. 127, 2011) proved global convergence; Part II (Math. Program. 130, 2011) counts evaluations. This mission covers the first count of Part II (§§2–3): with only the Cauchy condition on the step, ARC needs iterations, the same order as steepest descent and as trust-region methods (Gratton, Sartenaer and Toint, SIAM J. Optim. 19, 2008).
Let be continuously differentiable (AF.1), , and the Euclidean norm. At iterate , with a symmetric matrix and a weight , the cubic model is
Algorithm 2.1 (ARC) takes parameters , , and a starting point . At iteration it
For , and are the successful and unsuccessful iterations among . The complexity results use three assumptions: AM.1, for all ; AF.4, on an open convex set , with ; and a lower bound . Optionally, (2.10): on very successful iterations, for some . The constants are
Let with , and let be the first iteration with . Then
and, if (2.10) holds,
The constants are kept exactly as printed. The first bound counts gradient evaluations and the second counts all iterations, which is the number of function evaluations.
The corollary establishes that the ARC framework, whatever step it takes beyond the Cauchy point and whatever symmetric it uses, is never worse than steepest descent in evaluation count. It is the baseline against which Part II measures its second-order variant ARC(S), whose bound is the subject of a separate mission in this series. Theorems 2.1 and 2.2 are generic: they convert any per-iteration model decrease and any bound on into iteration counts, and are reused verbatim for ARC(S).
The results are proved in the paper. No machine-checked proof of any of them exists on Prove2Me or, to our knowledge, elsewhere. The work here is to formalize the known proofs: the Cauchy-point analysis of Part I (quoted, not reproved, in Part II), the Taylor-remainder estimate of Lemma 3.2, and the counting arguments. Formalizing also checks the printed statements: two of them need a small correction (see Formalization scope).
Each step is elementary, but the statements are about a nondeterministic algorithm: and are choices, so every bound must hold for all admissible choices, not for one convenient run. The constants are explicit, and the ceilings interact: the printed proof of (3.17) adds the ceilings of (3.15) and (3.22), which does not by itself give ; the bound must be derived from the unrounded estimates. Lemma 3.1 i) requires a careful one-dimensional analysis of with an indefinite . The ratio is a quotient, and its denominator must be shown positive before any comparison with , is meaningful.
The space is EuclideanSpace ℝ (Fin n); is Mathlib's gradient f; is a continuous linear operator with IsSelfAdjoint, and is the operator norm. A run is a predicate IsARCRun on the sequences ; the Cauchy condition is stated as for all , which is equivalent to comparing with the Cauchy point and avoids defining an argmin. The run is infinite; a run that the paper would stop at extends trivially, and every statement only concerns iterations with . Lean's x / 0 = 0 gives (unsuccessful) when ; Theorem 2.2 assumes (2.6), , up to its horizon, and §3's results need nothing extra because makes the denominator positive.
"" is stated as: every with for all satisfies (and similarly for ). This asserts that is finite without presupposing it. Statements with are given for every finite .
Two corrections to the printed text are built in. In Theorem 2.1 the bound is assumed for : as printed () the theorem fails for , iteration unsuccessful, . In AF.4 the set must contain the trial points as well as the iterates, because Lemma 3.2 applies the Lipschitz bound on the segment .
A trivializing formalization is ruled out: the goal quantifies over every admissible step and weight update rather than one particular choice, keeps (2.10) out of the first conclusion, and keeps every constant as printed rather than replacing it by an existential.
A complete development needs the one-dimensional cubic analysis behind Lemma 3.1, a mean-value bound for functions along a segment, and finite counting over Finset.range. The generic counting results (Theorems 2.1, 2.2) are reusable for every ARC variant. Proofs of any milestone, and of the goal from the milestones, are welcome.
Nash proved that every finite game has an equilibrium by exhibiting a continuous map of the set of mixed profiles into itself whose fixed points are exactly the equilibria, and applying Brouwer's fixed point theorem (Nash, 1951). Computationally, the same map is the bridge between games and fixed-point problems: complexity classes for total search problems such as PPAD (Papadimitriou, 1994) and FIXP (Etessami and Yannakakis, 2010) are defined through fixed points, and a game problem is placed in such a class by passing through Nash's map.
For three or more players, equilibria can be irrational, so algorithms produce approximations. Two different notions compete. An -Nash equilibrium is a profile at which no player can gain more than by deviating unilaterally; a weak -approximate fixed point of Nash's map is a profile that the map moves by less than in every coordinate. Proposition 3 of Etessami and Yannakakis shows that the two notions are interchangeable up to polynomially related tolerances. Since weak approximate fixed points of polynomially continuous, polynomially computable maps can be found in PPAD (their Proposition 2), this gives the membership of -Nash equilibria in PPAD, first observed by Daskalakis, Goldberg and Papadimitriou (2009) and by Papadimitriou (1994).
A finite game in normal form has a finite set of players; each player has a finite nonempty set of pure strategies and a payoff function on the pure strategy profiles . A mixed profile assigns to each player a probability vector ; is the set of mixed profiles. The expected payoff of player is , and is the expected payoff of when plays the pure strategy and every other player keeps its mixed strategy. The gain of switching to is
Nash's function is
A profile is an -NE if for every player and every mixed strategy of . A weak -approximate fixed point is an with .
The proof uses three constants of the game: , the maximum number of pure strategies of a player; , the maximum over players of ; and .
is an -NE.
The result says that the "almost at equilibrium" notion of approximation and the "almost fixed" notion attached to Nash's map are the same notion up to polynomial changes of tolerance. It is the reason the weak approximation problem for Nash's function inherits PPAD membership from Proposition 2 and conversely why PPAD-hardness of -NE transfers to weak approximation. The paper contrasts it with strong approximation (being close to an actual equilibrium), which it shows to be much harder; the explicit tolerances make precise which of the two notions a fixed-point algorithm for Nash's map actually delivers.
The result is proved in the paper. To our knowledge neither direction is formalized. On Prove2Me, the Daskalakis–Goldberg–Papadimitriou series contains the analogous Lemma 3.8 (DGPNash.NashMap.approx_fixed_point_is_approx_nash, posed) and its inequality (3) (DGPNash.NashMap.eq_3, posed): they concern the same map, but for games with a common strategy set Fin n, nonnegative payoffs and a different error term, so they are credited rather than reused. This mission states both directions for arbitrary finite strategy families with the paper's own constants.
Neither direction needs advanced mathematics; the difficulty is in the second direction. The obvious reading, that a profile moved little by has small gains, fails as stated: the approximate fixed-point condition controls , the gain of a strategy relative to the player's total positive gain weighted by , not the gain itself. A strategy that carries most of the probability and most of the positive gain can be almost fixed while its gain is large, so the bound on each has to come from information that the coordinatewise condition alone does not contain, with the exact constants and of the paper tracked throughout; the paper's argument is compact and leaves several of these estimates implicit. In Lean, the multilinearity of the expected payoff in a single player's mixed strategy, which underlies both the reduction to pure deviations and the zero-average identity, has to be derived from the product-form definition of the expected payoff.
Games, mixed profiles and expected payoffs are those of the published agt_games bundle: players form a finite type ι, player i has a finite strategy type S i, payoffs are real (u : ι → (∀ i, S i) → ℝ; the paper's payoffs are rational for computational reasons only). is the published DGPNash.NashMap.purePayoff, and the -NE is the published DGPNash.WellSupported.IsEpsApproxNash, which includes that is a mixed profile. New definitions: gain, nashFunction (by the printed formula, the sum over all of ), IsWeakApproxFixedPoint (a mixed profile with every coordinate of of absolute value ), and the constants maxNumStrategies (), payoffSpread () and cConst (), all computed from the game.
Explicit readings of the paper's text:
The constants , , are definitions computed from the game, not free parameters: a formalization that lets them be chosen (for instance a large in the second direction, or so that becomes ) would trivialize the statement and is ruled out. Contributions of reusable lemmas are welcome, in particular the linearity of AGT.expectedPayoff in one player's mixed strategy and the bound , which are useful to every game-theoretic mission built on agt_games.
Quasi-Newton methods minimize a smooth function using gradients only, while building up an approximation to the inverse of the Hessian matrix from the changes of gradient they observe. They are the default algorithms of unconstrained nonlinear optimization: BFGS and its limited-memory variant L-BFGS sit inside most numerical optimization libraries and most large-scale fitting codes in statistics and machine learning.
The family starts with William C. Davidon's Argonne report ANL-5990 of 1959, Variable Metric Method for Minimization, rejected by a journal in 1957 and published only in 1991 as the first article of the SIAM Journal on Optimization, with a preface by the author (DOI 10.1137/0801001). The report's body describes a flowchart algorithm; its Appendix describes "a simplified method embodying some of the ideas" of that algorithm, in one and a half pages. That simplified method is what is now called the symmetric rank-one (SR1) update, and the Appendix contains its quadratic-termination property: on a quadratic, after at most steps the trial matrix equals the inverse Hessian, and the next step lands at the minimum.
Timeline.
Vectors are elements of and matrices are real . Fix a symmetric positive definite matrix and a point , and let
a quadratic with constant Hessian and minimum point . Its gradient is , display (6) of the Appendix.
The method keeps a point and a symmetric trial matrix , which plays the role of . Write . One iteration is
a full step with no line search followed by a symmetric rank-one update. With the two scalars
footnote 2 of the Appendix fixes the coefficient on a quadratic to , which makes the paper's quality measure of (4) vanish. Write for the step and for the change of gradient. The paper writes , , for the current quantities and , , for the updated ones, and uses the letter both for the number of variables and for the scalar ; here the number of variables is .
If is symmetric and for every , then
This is the sentence after (8) on p. 17: "After no more than steps (for which ), will equal and the following step will be to the exact minimum."
The termination theorem says that on a quadratic the rank-one update recovers the exact inverse Hessian from gradient differences, without line searches and without positive definiteness of the trial matrix, and then takes the Newton step. This is the property that justifies the name "variable metric": the metric converges to the one that makes the problem trivial. The secant equation (8) and the persistence of earlier secant equations (7) are the template for the analysis of every later quasi-Newton update, and the SR1 update remains in use in trust-region methods because it does not force positive definiteness.
The result is classical and its proof is short; what this mission adds is a machine-checked version stated in the paper's own form. In particular the hypothesis is the paper's: only that each of the first coefficients is defined. Textbook statements of SR1 termination often assume in addition that the steps are linearly independent; the paper does not, and the formal goal does not either. No Lean formalization of SR1, DFP or BFGS termination was found in Mathlib or on Prove2Me. On Prove2Me, the related open targets are L-BFGS termination (Nocedal 1980) and conjugate-gradient termination (Hestenes–Stiefel 1952); the definitions here are independent of theirs.
Each update changes by a rank-one term, and nothing in a single step forces to be : the coefficient depends on the current iterate and the update could, a priori, destroy what earlier steps achieved, as general rank-one updates do. The obvious count — steps, conditions — does not by itself give independent conditions on ; the steps produced by the method are not chosen to be independent, and the only hypothesis available is that the denominators are nonzero. The difficulty is to get the full conclusion from that hypothesis alone, without assuming independence, positive definiteness of , or a line search.
Vectors are Fin n → ℝ with 0-based indices, matrices Matrix (Fin n) (Fin n) ℝ; is u ⬝ᵥ (H *ᵥ v) and is vecMulVec (H *ᵥ g) (H *ᵥ g). The definition file DavidonVM.Termination.Method provides quad, grad, Nval, Mval, the run predicate IsRunWith for an arbitrary gradient field and coefficients, and IsQuadRun for the quadratic with ; DavidonVM.Termination.Delta provides the update and the quantity of (4).
Committed conventions, each a reading of something the paper leaves implicit:
A statement of the goal with the extra hypothesis " are linearly independent", or with assumed, would be a weaker theorem than the paper's and is ruled out. The case is trivial; the hypotheses are jointly satisfiable for (checked locally).
Welcome contributions: proofs of the four milestones and the goal; general facts about rank-one updates (determinant and positive definiteness, Sherman–Morrison form of the inverse) that the further statements need and that are reusable for DFP, BFGS and trust-region analyses.
Many optimization problems in machine learning, signal processing and distributed computation have an objective that is a sum of a large number of component functions: one per data point, per sensor, or per processor. Evaluating the whole sum, or a subgradient of it, at every iteration is expensive when is large. Incremental methods process one component at a time, cycling through the components or sampling them, and update the iterate after each one. Incremental gradient and subgradient methods go back to the training of neural networks and to least squares; incremental proximal methods replace the subgradient step of a component by a proximal step, which is more stable and handles nonsmooth terms exactly.
Bertsekas (LIDS-P-2847, 2010, rev. 2011; Math. Program. 129 (2011)) proposed a unified family that mixes the two: each component is split as , a proximal step is taken on and a subgradient step on , followed by a projection onto the constraint set. This mission formalizes the convergence analysis of that family under the cyclic order of component selection.
Timeline. Incremental subgradient methods were analysed by Nedić and Bertsekas (SIAM J. Optim. 12 (2001)) for cyclic and randomized orders. Incremental proximal methods were studied by Bertsekas (Optimization for Machine Learning, 2011, ch. 4). The 2011 paper combines the two analyses; its cyclic-order results are Propositions 3–6.
Let carry the Euclidean norm and inner product . The data are a nonempty closed convex set and real-valued convex functions , . The problem is
with optimal value , possibly , and optimal set , possibly empty.
A subgradient of a convex at is a vector with for all ; is the point of nearest to . At iteration one component is processed with stepsize . The three iterations are
The -subgradient is taken at the new point, which makes the -part a proximal step (Proposition 1). In the cyclic order ; a block of consecutive iterations is a cycle, and is constant within a cycle.
The analysis assumes that the subgradients the iteration uses are bounded by a constant and that, at each cycle start , the function values at the intermediate points of the cycle differ from those at by at most times the distance (Assumption 1 for (19), (20); Assumption 2 for (21)). Both hold, for example, when all , are polyhedral or Lipschitz.
If and , then
and if moreover and , then for some . Both parts are one item, as in the paper.
Proposition 6 is the exact-convergence guarantee for the cyclic incremental subgradient-proximal methods: with a diminishing, non-summable stepsize they reach the optimal value whatever the starting point, and with square-summable stepsizes the iterates converge to a single optimal solution. It covers the pure incremental subgradient method () and the pure incremental proximal method () as special cases, and it is the template for the randomized-order analysis of the companion mission. Proposition 4 quantifies what a constant stepsize achieves.
These results are proved in the paper. None of them, nor the underlying estimates, is formalized on the platform or, to our knowledge, in Mathlib. The mission produces machine-checked versions of the proximal-step lemma for extended-real-valued functions on a constrained set, of the cycle estimate (27) with its explicit constants, and of the deterministic supermartingale convergence lemma, all reusable for other incremental and proximal methods.
The obvious argument treats one cycle as one step of a subgradient method on . It fails because within a cycle the subgradients are taken at the intermediate points or , not at , and the proximal steps use subgradients at the points they produce. The error between and at those points must be controlled through the drift of the iterates during the cycle, and the bookkeeping differs between (19)/(20) and (21), which is why differs. For the second part of Proposition 6, convergence of the values in the sense does not by itself give convergence of the iterates, and may contain more than one point.
EuclideanSpace ℝ (Fin n). Components are Fin m (0-based), so is k % m, and the paper's with becomes with z (k + j). is assumed (NeZero m).IsProj: a nearest point of ), not a choice function.Step between , , and the two subgradients it uses, with the -subgradient at the point the paper names. A run records these subgradients, so Assumptions 1–2 bound exactly them. The assumptions are not replaced by Lipschitz continuity, which is only a sufficient condition (p. 9).EReal; is allowed and no boundedness is assumed.MoreauProx.Characterization.GammaZero) and its subgradients, with relative interiors as Mathlib's intrinsicInterior.The goal cannot be satisfied vacuously: a sorry-free check confirms that the hypotheses hold together (for , , , , ). Restricting to Lipschitz components, to bounded-below , or to would state a weaker theorem and is ruled out.
Proofs of any item are welcome, as are general lemmas (the projection theorem as a variational inequality, the subdifferential sum rule under the relative-interior condition) that the proofs need.
Balanced truncation is the standard method for reducing the state dimension of a linear control system while keeping its input–output behaviour: states that are both hard to reach and hard to observe are discarded. Its justification rests on two Gramians, the solutions and of a pair of Lyapunov equations, whose quadratic forms measure how much input energy a state costs to reach and how much output energy it produces. For linear systems the facts are classical: the image of the controllability Gramian is the reachable subspace, and the kernel of the observability Gramian is the unobservable subspace.
Bilinear systems, in which the input multiplies the state, are the simplest nonlinear extension of linear control systems. Their generalized Lyapunov equations have the same form as the Lyapunov equations of linear stochastic systems with multiplicative noise, which is why Benner and Damm treat the two classes together. Balanced truncation was extended to them using the solutions of generalized Lyapunov equations (Al-Baiyat and Bettayeb, 1993; Gray and Mesko, 1998, both as cited by Benner and Damm). Benner and Damm, in Lyapunov Equations, Energy Functionals, and Model Order Reduction of Bilinear and Stochastic Systems (SIAM J. Control Optim. 49(2), 2011, doi:10.1137/09075041X), examine which of the linear-system energy interpretations survive for bilinear systems. Their Theorem 3.1 is the structural result that does survive: the kernels of the Gramians still identify states that are unreachable from the origin and states that produce no output, so these states can be eliminated without changing the transfer behaviour.
Fix and real matrices , , . The bilinear control system (3.1)–(3.2) is
with state , input and output . The homogeneous system (3.5) drops the term : , . The same indexes the bilinear terms and the columns of . Write for a solution with input and initial state , and .
An admissible input is a function that is integrable on every interval . A solution with is a continuous satisfying
The generalized Lyapunov equations (3.6) are
A solution of the first is a controllability Gramian and a solution of the second an observability Gramian. "" means is symmetric nonnegative definite; and are its image and kernel.
(a) If solves the first equation of (3.6), then for every admissible input
(b) If solves the second equation of (3.6) and , then for the homogeneous system (3.5) and every admissible input
The result. Part (a) says that a state outside cannot be reached from the origin by any input, so its controllability energy is infinite; part (b) says that a state in is indistinguishable from the origin at the output, so its observability energy is zero. Together they justify the first step of balanced truncation for bilinear systems (Remark 3.2 of the paper): the system can be restricted to and projected along without changing its input–output map, after which the Gramians are nonsingular and can be balanced. The theorem needs neither stability of nor uniqueness of the Gramians, so it applies to every nonnegative definite solution of (3.6). The rest of §3 of the paper shows that the finer, quantitative energy estimates of the linear case fail for bilinear systems; this qualitative statement is what remains exact.
Formalizing it. The theorem is proved in the paper; no machine-checked version is known. A formal proof yields a reusable invariance principle: a subspace that is invariant under every vector field is invariant under the flow of the input-driven system, for merely integrable inputs. It also yields the linear-algebra lemmas relating kernels of nonnegative definite solutions of generalized Lyapunov equations to the system matrices, which are used throughout model reduction and stochastic stability theory.
The algebraic part (milestones 1, 2, 4) rests on the fact that for a nonnegative definite matrix , forces , applied to the terms of the Lyapunov equation tested against a kernel vector. The passage from the vector field to trajectories is where care is needed. The paper's sentence " whenever , so is invariant" is not by itself an argument: tangency of a vector field to a subspace implies invariance only together with a uniqueness or Gronwall-type estimate, and here the field depends on time through an input that is only integrable, so is merely absolutely continuous and exists only almost everywhere. A pointwise "the derivative points into the subspace" argument therefore does not apply as stated, and the step needs an estimate on the component of orthogonal to the subspace.
The Lean development uses states Fin n → ℝ, matrices Matrix (Fin n) (Fin n) ℝ, the matrix–vector product *ᵥ, and indices as Fin m. and are LinearMap.range and LinearMap.ker of Matrix.toLin' P; "" is Matrix.PosSemidef, which includes symmetry. Admissible inputs are integrable on every (this contains , the input space of the paper's energy functionals). A solution is a function continuous on whose integrand is integrable on every and which satisfies the integral equation for all ; no uniqueness of solutions is presupposed, and the theorem is asserted for every such solution.
Two reading decisions are fixed. First, part (b) is stated for every admissible input , not only for as printed in the theorem: the paper's proof concludes " for all , implying ", and the theorem's clause "i.e., " (with a maximum over inputs) needs this form. The statement contains the printed one. Second, the clauses "i.e., " and "i.e., ", which restate the conclusions through the energy functionals (3.3)–(3.4), are not formalized.
The statements must not be trivialized: assuming positive definite makes (a) empty (), assuming stable or the Gramians unique adds hypotheses the paper does not have, and a solution notion requiring trajectories for integrable inputs would make the solution set empty. None of these is used. A local check confirms the hypotheses have content: for , , , the matrix is a nonnegative definite solution of (3.6) with .
A complete development needs Mathlib's facts on nonnegative definite matrices, interval integrals of vector-valued functions, and a Gronwall inequality with an integrable coefficient. The flow-invariance lemma for input-driven linear-in-state systems is reusable beyond this mission. Contributions welcome: proofs of the five milestones, and the passage from vector-field invariance to trajectory invariance.
Treewidth measures how closely a graph resembles a tree. Many problems that are NP-hard on general graphs can be solved in time linear in the number of vertices once a tree decomposition of bounded width is available, so computing such decompositions quickly is a basic task in algorithmic graph theory. Bodlaender, Drange, Dregi, Fomin, Lokshtanov and Pilipczuk (SIAM J. Comput. 45(2), 2016) gave an algorithm that, for a graph on vertices and an integer , either reports that the treewidth of exceeds or returns a tree decomposition of width at most , in time .
The paper's headline is that algorithm, a statement about pseudo-code and running times. This mission does not formalize it. It formalizes one of the paper's combinatorial lemmas, Lemma 6.5 (p. 369), which the algorithm's data structure uses to answer its balanced-separator query: it turns the search for a small balanced separator into two maximization problems that a dynamic program can solve.
Timeline. Robertson and Seymour (Graph Minors II, J. Algorithms 7, 1986) proved that graphs of treewidth have balanced separators of size (Lemma 2.1 of the paper). Robertson and Seymour (Graph Minors XIII, 1995) used it in an approximation algorithm, Reed (1992) improved the dependence on to , and Bodlaender et al. (2016) reached linear time with a single-exponential dependence on .
All graphs are finite and simple. For , is the graph obtained by deleting ; its components are the vertex sets of its connected components.
A separation of is a partition of (parts may be empty) such that no edge of joins to . Its order is . It is -balanced if .
For and sets of terminals , a terminal separation of the induced subgraph of order (Definition 6.4) is a partition of with
It is left-pushed if is maximum, and right-pushed if is maximum, among all terminal separations of of order with the same terminals.
The treewidth is the least width of a tree decomposition of (Definition 1.1), where the width is the largest bag size minus one.
Let and let be a separation of with . Then there are a partition of and integers with such that, for with terminals ,
In the order of the proof, the milestones are: Lemma 2.1 (balanced -separators of size , cited from Graph Minors II); the packing step of the proof sketch of Lemma 2.2 (components holding at most of each split into two sides holding at most each); the folklore -balanced separation of order ; the restriction of that separation to , which gives part (i); four lower bounds on , ; the dichotomy that two opposite "quadrants" have at least vertices each; the comparison of pushed separations with the restricted one; and the gluing step of part (ii).
Lemma 6.5 is what makes the paper's balanced-separator query computable: given a bag that splits a component in a balanced way, a left-pushed and a right-pushed terminal separation are each the solution of a maximization problem, and the lemma guarantees that gluing them gives a separator of order whose sides are bounded away from . The constant feeds into the approximation ratio of the whole algorithm.
The proof is complete in the paper and elementary given Lemma 2.1. No part of it is formalized in Lean's Mathlib or, as far as a search of the Prove2Me catalog shows, on the platform. Lemma 2.1 itself, Robertson and Seymour's balanced-separator theorem for bounded treewidth, is not in Mathlib; a machine-checked proof of it would be reusable wherever treewidth separators are used (divide-and-conquer on tree decompositions, Lipton–Tarjan style arguments, grid-minor theorems).
Everything after Lemma 2.1 is counting with partitions, but the bookkeeping is the obstacle: the two separations and cut into nine pieces, the induced subgraphs overlap on , and pushedness is a maximum over a family of partitions of a subset, not of .
Lemma 2.1 is the hard milestone. It is a statement about tree decompositions, and any proof has to relate subtrees of the decomposition tree to components of for a bag , infrastructure that does not yet exist in Mathlib.
V : Type with decidable equality; vertex sets are Finset V, is Finset.univ, is Fintype.card V. Universe 0 matches the published definition of treewidth.RobertsonSeymour1986.GM5.TreewidthLE G k: a decomposition tree on a finite type whose bags have at most vertices. Definition 1.1 roots the tree; rooting does not change the width.avoidComp G X u: the vertices reachable from by a walk of none of whose vertices, endpoints included, lies in .Part (i) is part of the goal: without it, left- and right-pushed separations of the chosen orders might not exist and part (ii) would hold vacuously. Choosing does not trivialize the goal, because the size bound and the budget must hold simultaneously.
Welcome contributions: a proof of Lemma 2.1 from tree decompositions (reusable on its own), the packing lemma, and the counting milestones of the proof of Lemma 6.5.
How should a set of indivisible items (courses, shifts, inherited objects) be divided among people who have different entitlements but no money to transfer? A classical answer for divisible goods is the competitive equilibrium from equal incomes (CEEI): give every agent a budget of artificial currency, find prices at which every agent can afford her favourite bundle and the market clears. The resulting allocation is Pareto optimal and fair. With indivisible items a CEEI can fail to exist already for one item and two agents with equal budgets: at any price, either both agents can afford the item or neither can.
Babaioff, Nisan and Talgam-Cohen (arXiv:1703.08150; Math. Oper. Res. 2021, doi:10.1287/moor.2020.1062) study this Fisher market with indivisible goods when budgets are generic: unequal budgets, with a measure-zero set of exceptional budget pairs excluded. Their main result is for two agents with almost equal budgets. This mission formalizes the companion result for two agents with identical additive preferences and arbitrary unequal budgets (Theorem 8.1 of the paper, its informal Theorem 1.4). With identical preferences the division problem is a discrete claims (bankruptcy) problem: one cake of fixed value is split between claimants with different entitlements .
Timeline of the relevant results:
There are indivisible items and two agents. Agent has a valuation that is additive, normalized (), non-negative, monotone and strict (different bundles have different values), and a budget , with . An allocation gives every item to exactly one agent. Item prices price a bundle at .
A bundle is demanded by agent at prices if and for every bundle with . A competitive equilibrium (CE) is a pair in which each is demanded by agent . An allocation is Pareto optimal (PO) if every other allocation is strictly worse for some agent. It is budget-proportional if for both agents, and anti-proportional if for both, strictly for one.
The truncated share of agent is
the best she can get in a PO allocation that gives her at most her budget share; an allocation gives her the truncated share if . The exceptional set (Definition 6.2) consists of the budget pairs for which two PO allocations , consecutive in agent 's order of preference, satisfy . It is finite. The rectangle (Definition 6.1) is a set of allocations between the truncated-share maximizers of the two agents.
In Lean all objects live in GenericBudgets.IdenticalPrefs: bundle, price, IsDemanded, IsCE, IsPO, IsStandardValuation, IsBudgetProportional, IsAntiProportional, GetsTruncatedShare, IsTruncMaximizer, InRectT, InR.
If , , and for some agent , then
Theorem 8.1 shows that the non-existence of CEEI for identical preferences is a knife-edge phenomenon: for every market with identical strict additive preferences, every unequal budget pair outside a finite set admits a CE, and the CE allocation is as close to budget-proportional as indivisibility allows. It gives a market-based solution to the indivisible claims problem with unequal entitlements, and its CE inherits Pareto optimality from the first welfare theorem (Theorem 2.4 of the paper).
The formalization targets three things on top of the paper. First, a machine-checked proof of the paper's main technical tool, Lemma 6.3, which also drives the paper's main Theorem 7.1 (mission 1 of this series), where it is applied to almost equal budgets instead of identical preferences. Second, precise definitions of the truncated share, the rectangle and the exceptional set , whose informal versions leave conventions implicit (the maximization runs over PO allocations only; is indexed by consecutive PO allocations). Third, verification of the proof chain Proposition 5.1 → Lemma 6.3 → Lemma 8.2 → Theorem 8.1. The statements compile, but none of these results has a machine-checked proof yet.
The reduction of Theorem 8.1 to Lemma 8.2 and the proof of Lemma 8.2 from Proposition 5.1 and Lemma 6.3 are short. The substance is in Lemma 6.3, which must exhibit prices supporting a PO allocation when no allocation gives both agents their budget shares. Demand is a condition over all bundles, so a candidate price vector has to be checked against every bundle each agent prefers, and the paper's construction breaks down on the exceptional budget pairs , which is why they are excluded; the argument is a case analysis over the finite Pareto frontier. The easy case, Proposition 5.1, covers only markets with a budget-proportional or anti-proportional PO allocation; with identical preferences and unequal budgets neither typically exists (no allocation is ever anti-proportional), so Lemma 6.3 cannot be avoided.
Items are Fin m; agents are Fin 2, with indices for the paper's agents , so is b 1 < b 0. Valuations are functions Finset (Fin m) → ℝ bundled with the standing assumptions in IsStandardValuation; identical preferences are the hypothesis v 0 = v 1. An allocation is a map Fin m → Fin 2, so every item is allocated exactly once. Budgets are positive reals summing to . All quantities are real.
Committed conventions and disclosed restrictions:
max: for every PO with .Trivializing formalizations are ruled out: the demand condition quantifies over every bundle with strict inequality, allocations must assign every item, prices are non-negative, the truncated share is maximized over PO allocations only (not over all allocations), and the budget hypothesis excludes only the finite set for one agent, never all unequal budgets.
Proposition 5.1 and Lemma 6.3 are posed with the same statement as in mission 1 of this series; a proof of either transfers verbatim. Contributions welcome: the finite-frontier infrastructure (existence and uniqueness of the truncated-share maximizer), Proposition 5.1 through budget-exhausting combination pricing, and Lemma 6.3.
The electroweak interaction is the unified description of electromagnetism and the weak nuclear force in the Standard Model of particle physics. Glashow, Salam and Weinberg shared the 1979 Nobel Prize in Physics for this unification, and its central predictions — neutral weak currents (Gargamelle, 1973) and the massive and bosons (UA1/UA2, 1983) — have been confirmed experimentally. The algebraic core of the theory is short: an gauge theory whose symmetry is broken by the vacuum value of a Higgs doublet, after which the neutral gauge fields are rotated by the weak mixing angle into the photon and the , and the masses satisfy .
This mission formalizes those tree-level algebraic facts as they are stated in the Wikipedia article Electroweak interaction (revision 1360331872), sections Formulation and Lagrangian.
Timeline (as recounted in the article). After the Wu experiment (1956) exposed parity violation, Glashow combined a chiral and an achiral symmetry and predicted a boson; Salam and Ward (1964) proposed a massless photon and three massive gauge bosons with manually broken symmetry; Weinberg (1967) used spontaneous symmetry breaking (Englert–Brout, Higgs, Guralnik–Hagen–Kibble, 1964) and predicted rough and masses; 't Hooft (1971) proved that spontaneously broken gauge theories are renormalizable. Neutral currents were observed in 1973 and the , in 1983.
Fix the weak isospin coupling and the weak hypercharge coupling . The gauge fields at a spacetime point, for one Lorentz component, are real numbers (weak isospin) and (weak hypercharge).
For all real ,
which is the mass part of in the article. The photon field does not appear: it stays massless.
These identities are the content behind the article's statements that "the axes ... have been rotated by the angle ", that , that , and that is unbroken because it does not couple to the Higgs. The formal library produced here (Pauli matrices, the Higgs doublet, the mixing rotation, the mass formulas) can be reused by later missions on the full electroweak Lagrangian, on the Yukawa sector, or on the custodial relation .
All statements are classical tree-level results. None is open; the work is to formalize them.
The mathematics is finite-dimensional linear algebra and trigonometry. The main pitfalls are conventions: the factor in front of the Pauli matrices, the hypercharge normalization (so the Higgs has ), and the sign conventions in the rotation matrix. The goal also requires handling complex doublets, factors and the inverse trigonometric definition of at the same time.
All fields are real numbers at one spacetime point and for one Lorentz component; the Lorentz contraction and the kinetic (derivative) terms are not modeled. The Higgs doublet is a function Fin 2 → ℂ, and its squared norm is written out as (not the sup norm of the product type). The Pauli matrices are defined explicitly. The angle is ; with this agrees with the triangle. The standing convention is a hypothesis wherever appears. The goal is stated as an equation in so that the product appears exactly as in .
All declarations live in the namespace ElectroweakWiki.
In ordinary quantum mechanics, and in quantum field theory on a fixed spacetime, events happen in a definite causal order: an operation either precedes another, follows it, or the two are spacelike separated. Attempts to combine quantum theory with general relativity call this assumption into question. In general relativity the causal structure is dynamical, and a quantum theory of gravity may allow it to be indefinite. Oreshkov, Costa and Brukner (Nat. Commun. 3, 1092 (2012), arXiv:1105.4464) turned this question into a precise mathematical one. They assume that quantum mechanics holds locally in each laboratory and make no assumption about any global causal order. Within that framework they ask which correlations between two laboratories are possible. They find correlations that no definite causal order can produce: these correlations violate a causal inequality, which every causally ordered scenario satisfies.
Timeline.
Alice's laboratory has an input system and an output system , and Bob's has and . All four are finite-dimensional, with dimensions , and operators on are complex matrices indexed by .
A local operation of Alice is described by its Choi–Jamiołkowski (CJ) matrix . The operation is a completely positive trace-preserving (CPTP) map exactly when
A process matrix is a matrix satisfying
(Eqs. (4)–(5) of the source). The probability of a pair of local outcomes is (Eq. (3)).
The task (Eq. (1)). Alice, Bob and a second bit for Bob receive independent uniform bits , and . Alice uses an instrument to produce a guess , and Bob uses to produce a guess . If Bob must communicate to Alice, and if Alice must communicate to Bob:
Causal separability (Eq. (6)). A process matrix of the form allows no signalling from Alice to Bob, written . One of the form allows none from Bob to Alice. is causally separable if for some .
The goal states only that a violation exists, with no hard-coded value. The specific value is a milestone.
is a process matrix. 3. Eq. (8): with the instruments of Eqs. (20)–(23), this gives , for every state that Bob may prepare. 4. p. 5: the matrix of Eq. (7) is not causally separable. 5. Appendix F: every process matrix that is diagonal in a product basis (a classical process) is causally separable. 6. Appendix C, Fig. 3: for Hermitian , the normalization condition (5) holds if and only if and has no Hilbert–Schmidt component of type , , , , , , or . 7. Appendix E, Eq. (26): , and .
The result. Milestones 1 and 3 together show that quantum mechanics, applied locally in each laboratory, does not by itself imply a definite causal order. The causal inequality is a device-independent test of causal order, analogous to a Bell inequality for local realism. Milestone 5 shows that indefinite causal order disappears in the classical limit, and the source reads this as a hint that spacetime causal structure may emerge in a quantum-to-classical transition. The process-matrix framework has since become standard for indefinite causal order. Milestone 6 is the characterization that later work on witnesses and causal inequalities relies on.
Formalizing it. All seven milestones and the goal are proved in the source; none are open mathematics. This mission produces machine-checked versions in a common vocabulary: process matrices, CJ instruments, causal separability and Hilbert–Schmidt type analysis. That vocabulary can be reused for later results such as witnesses of causal nonseparability, multipartite causal separability and the quantum switch.
Status honesty. The formal statements are about matrices. Whether causal-inequality violations can occur in nature is not settled. Laboratory realizations of the quantum switch certify causal nonseparability with witnesses, not with a causal-inequality violation, and the source leaves open whether is the largest possible violation.
The violation itself (milestones 2, 3 and 7) is finite linear algebra on matrices, but the irrational entries rule out a purely computational check. Positivity of is the nontrivial part of milestone 2. The two Pauli strings in anticommute, which fixes its spectrum, but this has to be turned into a positive-semidefiniteness proof.
Milestone 1 needs more than inspecting the definitions. The bound has to be shown for each no-signalling form separately and then carried through convex mixtures, with instruments of arbitrary dimension.
Milestone 4 is a non-existence statement over all decompositions. A direct search is hopeless; it follows from milestones 1 and 3.
Milestone 5 (Appendix F) is the deepest: it builds the two positive parts of the decomposition by an eigenvalue-shifting procedure.
Milestone 6 needs orthogonality computations with arbitrary Hilbert–Schmidt bases on four tensor factors.
⊗ₖ with tensor order . Local operations are represented directly by their CJ matrices, so the transpose in the source's CJ convention never enters the statements. Bits are Bool (false ↦ 0). Probabilities are real parts of traces, which are real whenever all inputs are positive semidefinite.OCB2012_defs: partial trace ptrace₂, IsCPTP_CJ, IsProcessMatrix, prob, IsAliceInstrument, IsBobInstrument, pSucc, the no-signalling forms, IsCausallySeparable, the Pauli matrices, W7, the instruments ξ and η, the structure HSBasis and the predicate AllowedType. Density matrices come from the published PeresTerno.IsDensityMatrix.The Wheeler–DeWitt equation is the quantum version of the Hamiltonian constraint of general relativity. In the canonical formulation, a spacetime is described by the evolution of the metric of a spatial slice, and Einstein's equations include a constraint: the Hamiltonian density vanishes at every point of space. Quantizing this constraint, as DeWitt did (Phys. Rev. 160, 1967), gives a second-order functional differential equation for a wavefunctional with no external time parameter.
Three structural facts make the equation distinctive:
A fourth issue is not settled: consistency. In the continuum, the Poisson bracket of two Hamiltonian constraints is a combination of the momentum constraints, so imposing all constraints is consistent (Dirac's first-class condition). Any regularization of the quantum equation, a lattice for instance, must reproduce this. Generic lattice discretizations do not: the constraints become second class (Bander 1987; Dittrich 2008; Bahr–Dittrich 2009). Whether, and with which anomaly, the Hamiltonian-constraint commutators close as the lattice is refined was singled out as an open question by Loll (Living Rev. Rel. 1998, §2.12).
The first three facts are the standard entry points of quantum geometrodynamics, as reviewed by Kiefer (arXiv 0812.0295): Section 2 for the constraints and their quantization, eqs. (3)–(8), and Section 3 for the Hamilton–Jacobi equation, eq. (10), and the semiclassical approximation, eq. (11).
A spatial metric at a point is a symmetric positive-definite matrix . Write . The DeWitt supermetric is
It is a quadratic form on symmetric momenta. Its inverse acts on velocities.
Space is represented by a finite set of sites; this is a lattice regularization. A configuration assigns to each site a matrix . All nine entries are coordinates, so configuration space is , and physical configurations are those that are symmetric and positive definite at every site. A wavefunction is a function from configurations to . The functional derivative is the partial derivative with respect to the coordinate , with the cell volume normalized to one.
The Wheeler–DeWitt operator at site , with gravitational coupling , cosmological constant , and a supplied potential playing the role of the spatial scalar curvature, is
Write for the potential at site . On the classical phase space of pairs , with conjugate to , the lattice constraints are
with the canonical Poisson bracket. They are first class if each bracket vanishes wherever all constraints vanish.
The supermetric stands to the left of both derivatives (Kiefer, eq. (7), vacuum case; the coupling is , so as in Kiefer's eq. (10)). The kinetic term involves only derivatives at the same site, as in the continuum; it is ultralocal. The potential may couple neighbouring sites.
For with and :
For every real function and :
The -independent part is the Einstein–Hamilton–Jacobi functional of Kiefer's eq. (10), Hamiltonian part, with the eikonal of the WKB form (11) (amplitude ). This is the weakest statement exhibiting the classical limit, and it holds for every potential.
For and sites :
If every depends only on , then identically.
If the symmetric part of is nonzero at a physical , for some , then there is a point of the constraint surface over at which .
Every finite-difference curvature couples neighbouring sites, so the goal applies to every such discretization. It is the weakest statement that the discretized constraint algebra is inconsistent, and it holds uniformly in the discretization.
Tendsto statement.The signature theorem is the mathematical content behind two physical facts: the hyperbolic character of the Wheeler–DeWitt equation, and the instability of the conformal mode (the "conformal factor problem" of Euclidean quantum gravity). DeWitt's cone form identifies the local volume as an intrinsic clock. On this rests the reading of the equation as a wave equation in superspace, with as time. The conformal-sector reduction shows explicitly how the timelike direction appears in the operator, with the sign opposite to the traceless modes. The WKB identity is the precise sense in which the quantum constraint contains classical general relativity: its leading order is the Hamilton–Jacobi form of the Einstein constraint (Peres 1962; Kiefer, eq. (10)), and its next order is the one used in derivations of the Schrödinger equation from quantum gravity.
All of these are classical computations. The drafter knows of no machine-checked version. A formalization fixes conventions that the literature handles loosely:
It does so with genuine derivatives in place of formal symbols.
The constraint-algebra part turns a phenomenon described qualitatively in the literature into a theorem with exact hypotheses. Lattice constraints are second class as soon as curvature couples sites, and the quantum commutator is given in closed form. It also isolates precisely what a consistent discretization would have to cancel. The continuum-limit target addresses an open question in canonical quantum gravity.
The supermetric statements are finite-dimensional, but none is a single computation. The signature requires a positivity argument for on an -traceless subspace. The cone form requires separating the trace part of a velocity in a non-orthonormal frame.
The analytic targets require second derivatives of compositions through the determinant and the matrix inverse. The derivative of at in the direction of a single entry is , and the derivative of produces terms like ; a sign or index slip changes the constant . Treating the nine entries as independent coordinates, rather than the six symmetric ones, changes the numerical coefficients; the conventions below fix this.
For the constraint algebra, the quantum commutator involves up to fourth derivatives of , which cancel only by the symmetry of mixed partials. The classical goal needs a point on the constraint surface where the bracket is nonzero. Each constraint fixes the value of an indefinite quadratic form in the momenta, and the bracket is linear in them, so the proof must use the Lorentzian signature to show that the bracket is not constant on that quadric.
A naive formalization that replaces by an abstract linear map reduces every target to ring arithmetic, and is ruled out by the definitions.
Def_WheelerDeWittSuperspace):
Fin 3 → Fin 3 → ℝ, so that configuration space X → Fin 3 → Fin 3 → ℝ with X a Fintype is a normed space;Matrix.of;fderiv ℝ Ψ h applied to the coordinate direction of ;Real.sqrt of the determinant;Matrix.PosDef includes symmetry);At high energies (, the Regge limit) scattering amplitudes of gauge theories simplify and organise into towers of logarithms . For the four-gluon amplitude of super-Yang–Mills theory with gauge group , the colour structure is what makes the nonplanar (subleading in ) amplitude hard to control. Naculich (2020) builds a basis of colour factors adapted to the Regge limit at every loop order, writes the -loop amplitude in that basis, and uses one of its coefficients, , to motivate a conjectured all-loop relation with the Regge limit of the supergravity four-graviton amplitude. The physics conjecture itself is not a mathematical statement; what is exact and checkable is the colour algebra underlying it — finite-dimensional linear algebra over polynomials in .
Trace basis. Four-gluon colour factors are expanded in six single and double traces of fundamental generators (eq. (2.1)). A colour vector is a column of polynomials in , with complex coefficients.
Colour operators. The -channel Casimir and the crossing-odd combination act on colour vectors as the explicit matrices of eq. (4.15) (entries in ). The tree-level -channel colour factor is . Crossing (exchange of legs 2 and 3) is the permutation : , .
Regge colour factors. With ,
each with exactly operators. The admissible pairs are , , and for .
Extended trace basis. At loops, for and for , giving elements (eq. (2.3)). The colour-ordered amplitudes of an amplitude are its coordinates in this basis (eq. (2.4)).
Regge-basis amplitude. Eq. (4.24):
Null vectors. Four vectors per loop order (eqs. (2.10), (2.12), extended by prepending zeros) encode the group-theory relations among the .
For every even ,
and for , . The paper obtains the even- formula by guessing from explicit results through ; a proof for all is not given there.
The result. Eq. (4.26) is the input to the paper's analysis of the infrared behaviour of (at most , manifest for even because only most-subleading-colour amplitudes appear), and hence to the conjectured all-orders relation between and the Regge limit of supergravity (Sec. 6). An all- proof replaces an extrapolation from nine loop orders by a theorem.
Formalizing it. The low-loop tables (4.16), (4.20), (4.18), (4.22) are finite computations; the goal and milestones 3, 4, 7, 8 are statements for every loop order and need genuine arguments (induction on , structure of the operators on the extended basis).
The coefficient is defined through the whole -element basis: a formula for it must vanish on every other , including the nested commutators and whose components grow in complexity with . Checking the formula loop order by loop order does not give a proof; one needs to control how and act on the two most-subleading slots of the extended basis uniformly in .
Fin 6 → ℂ[X], with the polynomial variable X; operators are Matrix (Fin 6) (Fin 6) ℂ[X] acting by Matrix.mulVec. Coefficients and the prefactor are arbitrary complex numbers; is a function ℕ × ℕ → ℂ of which only the admissible pairs matter.LinearIndependent, finite sums) is used.In February 1998 Witten's paper Anti de Sitter Space and Holography made precise Maldacena's proposal that large- conformal field theories in dimensions are described by gravity on -dimensional anti de Sitter space . The dictionary it proposes identifies boundary values of bulk fields with sources of boundary operators, and reads correlation functions off the dependence of the bulk action on those boundary values. Its most quoted quantitative consequence is the mass–dimension relation: a scalar of mass on corresponds to a boundary operator of conformal dimension
Behind this physics statement sits a piece of classical analysis on hyperbolic space: the Dirichlet-type problem for the operator with prescribed boundary asymptotics, solved by an explicit Poisson-type integral (Section 2 of the paper, eqs. (2.15)–(2.44)). This mission formalizes that analytic core.
Timeline. Maldacena 1997 (hep-th/9711200) conjectured the correspondence; Gubser–Klebanov–Polyakov (hep-th/9802109) and Witten (hep-th/9802150, both February 1998) proposed the precise dictionary; the Euclidean black-hole thermodynamics used in Section 3 goes back to Hawking–Page 1983.
Euclidean is modelled as the upper half space with the hyperbolic metric
Its Laplace–Beltrami operator is
A massive scalar of squared mass solves (eqs. (2.34), (2.37)). The conformal dimension is (eq. (2.44)), the bulk-to-boundary kernel is
and the Poisson-type integral of a boundary datum is (eqs. (2.20), (2.41)).
For there is a constant such that for every bounded continuous on ,
is a solution of on the upper half space and as , i.e. at the boundary (eq. (2.36) with ).
The goal is the analytic statement underlying the mass–dimension relation of the AdS/CFT dictionary: it shows that the boundary datum of a massive field is naturally a density of weight , which is how the paper identifies the dimension of the dual operator. The same kernel is the starting point for the two-point function (2.42). The result is classical mathematics (scattering theory on hyperbolic space), proved informally in the paper; this mission produces a machine-checked version together with reusable infrastructure for the hyperbolic Laplacian in half-space coordinates.
The pointwise identities (milestones 1, 2, 6, 7, 8) are calculus. The substance is analytic: differentiating the Poisson-type integral twice under the integral sign with only boundedness of , and proving the approximate-identity limit with the right normalisation; the scaling integral requires , and the endpoint (where and the kernel is not integrable) must be excluded.
Points are pairs ; partial derivatives are one-variable derivs, so the solution predicate also demands regularity on , which rules out junk values of deriv. Real powers are Real.rpow; integrals are Bochner integrals for Lebesgue measure. Boundary data are bounded continuous functions. All declarations live in the namespace WittenAdSHolography, with the shared definitions in one definition file.
A coupling constant is the number that fixes the strength of an interaction: in the modern formulation it is the parameter weighting the interaction part of a Lagrangian against its kinetic part. In a quantum field theory such a parameter is not constant. Probing a process at a higher energy resolves more of the virtual activity that dresses the interaction, and the value one measures depends on the energy scale at which the measurement is made. This scale dependence is called the running of the coupling, and it is the organising phenomenon behind two of the best-known qualitative facts about the Standard Model: the electromagnetic coupling grows with energy ( at low energy, at the mass, about 90 GeV) and apparently diverges at a finite energy — the Landau pole — while the strong coupling decreases logarithmically at high energy, the asymptotic freedom found by Gross, Politzer and Wilczek and recognised by the 2004 Nobel Prize.
The source treats the running through the beta function, defined there by
and through the one-loop strong coupling
Everything in this mission is the mathematics of those two formulas: an autonomous scalar ordinary differential equation in the logarithm of the energy, and the behaviour of its solutions according to the sign of the one-loop coefficient.
Write for the energy scale of a process and , or , for a real-valued coupling as a function of that scale. The beta function in the energy scale is the logarithmic derivative used by the source,
a function of built from ; a theory whose beta function vanishes identically is scale-invariant, since its coupling then takes the same value at every scale.
A coupling is said to be one-loop running with coefficient on a set of scales when it satisfies, at every ,
equivalently . Here is the asymptotically free sign (QCD) and the sign the source attributes to QED. The equation is the one-loop truncation written in rather than in : both forms appear in the source, and the first milestone is precisely their agreement.
The one-loop strong coupling with one-loop coefficient and QCD scale is the explicit function
the formula the source quotes for . It is defined by an existing platform definition, which this mission reuses rather than restates.
For every reference scale and every positive reference value of the coupling at that scale:
The negative-coefficient half is asymptotic freedom together with the uniqueness of the solution; the positive-coefficient half is the Landau pole, stated as the non-existence of any solution up to the pole scale rather than as a divergence of one chosen formula. The pole scale is the one the one-loop equation itself predicts.
The milestones below range from the definitional identity , through the three qualitative readings of the sign of that the source states in words (vanishing beta function means scale invariance; positive beta function means the coupling grows with energy; negative means it falls), to the identification of the quoted QCD formula as an exact solution of the one-loop equation and the determination of from a single measured value.
The dichotomy is the mathematical content of two physical statements that the source presents side by side. Asymptotic freedom is what makes perturbative QCD predictive at high energy; the Landau pole is the reason the source warns that the perturbative beta function cannot be trusted at strong coupling, since the one-loop equation has no solution reaching the pole scale at all. Formalizing the uniqueness half also pins down what "the" running coupling means: the explicit formula is not merely one solution of the renormalization-group equation but the only one through a given data point.
An earlier public mission on the same source ("Coupling Constant: One-Loop Running, Asymptotic Freedom and the Landau Pole") formalized the one-loop flow in the logarithmic variable with a cubic beta function , and its statements are proved. This mission is stated in the other variable the source uses — the energy scale itself, with the quadratic one-loop equation for — and adds the parts of the source that the earlier mission does not cover: the defining identity between the two forms of the beta function, the sign-to-monotonicity statements for an arbitrary (not necessarily one-loop) coupling, the explicit pole scale, and the determination of the QCD scale from a measurement. Where the earlier mission already settles a statement in the quoted formula's variables, this proposal references the published theorem instead of restating it.
The equation is elementary, and the difficulty is entirely in what the statements quantify over. The negative-coefficient half asserts that every function satisfying the equation on is the explicit one, so it needs a uniqueness argument for a nonlinear scalar ordinary differential equation rather than a verification that a formula works; the substitution that makes the equation linear is legitimate only while is known not to vanish, which is part of what has to be proved. The positive-coefficient half is a non-existence statement on a closed interval reaching the pole, so no local solution can be extended to it; the naive attempt — differentiate the explicit formula and observe that it blows up — proves nothing about the other candidate solutions.
Couplings are total functions , and every statement restricts to the scales it is about: the positive half-line for the beta-function statements, for the explicit QCD formula, or a closed interval for the one-loop flow. Outside those ranges nothing is claimed — in particular at , where the logarithm in the quoted formula vanishes or is negative and the reciprocal returns a junk value. Differentiability is a hypothesis where it is needed, written as a two-sided derivative at each scale of the set, so that a statement cannot be satisfied by a one-sided artefact at an endpoint. The one-loop property is phrased as an exact differential equation, never as an asymptotic approximation, and the Landau-pole milestone is a non-existence claim rather than a divergence claim, so it cannot be discharged by exhibiting a formula with a singularity.
A complete development needs the mean value theorem, Gronwall- or uniqueness-type arguments for scalar ordinary differential equations, and the standard logarithm and exponential API; the uniqueness lemma for and the reciprocal substitution are reusable beyond this mission. Contributions of a general scalar-ODE uniqueness lemma, usable by both this mission and the earlier one, are especially welcome.
The Polyakov action is the standard action for the worldsheet of a bosonic string. It was introduced by Deser and Zumino and independently by Brink, Di Vecchia and Howe in 1976, and is associated with Polyakov after he used it to quantize the string in 1981. Its value over the Nambu–Goto (area) action is that it is quadratic in the embedding fields, which makes quantization tractable, while being classically equivalent to the area action. This mission formalizes the classical facts collected in the Wikipedia article Polyakov action.
A string sweeps out a two-dimensional worldsheet with coordinates . Its embedding in a -dimensional target is ; the target carries a metric , and the worldsheet carries an independent (auxiliary) metric with inverse and determinant . With the induced metric and string tension , the Polyakov and Nambu–Goto actions are
The stress–energy tensor is . Signature convention: timelike , spacelike .
If the auxiliary metric satisfies its equation of motion (with ), then
These are the classical foundations of bosonic string theory: the symmetries (Poincaré, diffeomorphism, Weyl) are what make the conformal gauge reachable, and the equivalence with Nambu–Goto justifies using the quadratic action. All statements are textbook results; the work here is to formalize them with explicit hypotheses (differentiability, integrability, positivity of ) that the physics presentation leaves implicit.
The algebraic statements are matrix identities. The diffeomorphism invariance needs the change-of-variables formula; the infinitesimal Lorentz statement needs care with integrability; the wave-equation milestone needs the fundamental lemma of the calculus of variations; and the light-cone solution is d'Alembert's theorem.
Worldsheet (coordinates Fin 2 → ℝ, index ), target . Actions are Bochner integrals over a region . The inverse metric is Mathlib's matrix inverse. Quantization, Virasoro operators, the Liouville action and string boundary conditions are out of scope.
Whether the many-worlds (Everett) interpretation of quantum mechanics is local in the sense of Bell is a recurring question in the foundations of physics. A number of authors have argued that Everett's theory escapes Bell-type nonlocality theorems because it drops the assumption that each measurement has a single outcome. A. Drezet's paper arXiv:2306.07794 (2023) argues against this claim by revisiting the Greenberger–Horne–Zeilinger (GHZ) nonlocality theorem, which, unlike Bell's inequality, uses only probability-one (perfect) correlations. Its central mathematical step, stated in Section II, is that no locally causal beable model can reproduce the quantum predictions for the GHZ state. The paper's argument is that this step makes no assumption about completeness or hidden variables, and so applies to Everett's theory as well.
Timeline:
Three spin-½ particles are sent to three distant observers, Alice, Bob and Charlie. Each one measures the spin of their particle along a direction and records an outcome . The particles are prepared in the GHZ state
and quantum mechanics predicts the joint outcome probabilities through the Born rule, . Here denotes the eigenvector of with eigenvalue . In Lean this is bornProb n₁ n₂ n₃ α β γ.
A locally causal (Bell-local) model consists of
Such a model predicts
In Lean the model is a LocalCausalModel Λ and its prediction is M.predict. The beables are arbitrary: may be a hidden variable, or the quantum state itself as in the Beltrametti–Bugajski representation, Eq. (15).
No locally causal model reproduces the quantum predictions on the four GHZ settings , , , :
The goal theorem is the mathematical core of the paper's conclusion that any beable account of the GHZ correlations, including one where is just the quantum state, violates Bell's local causality. Milestones 6–8 formalize the paper's separation of notions of locality: non-signalling holds both in quantum mechanics and in every locally causal model, so it cannot tell them apart; and dropping statistical independence (Eq. (18)) is enough to reproduce the correlations. The GHZ theorem itself has been known since 1989. As far as the drafter is aware it has no machine-checked formalization on this platform, and this mission provides one, stated for general measurable beable spaces.
The combinatorial core (milestone 3) is a parity argument. The substance lies in the steps that connect it to probability: showing that perfect correlations force determinism almost surely when is an arbitrary probability measure (null sets, measurability, integrals of nonnegative functions), and computing the Born probabilities exactly in Lean from explicit matrices and eigenvectors.
ℤˣ (exactly ). Settings form a two-element type Setting with values x and y. Qubit index 0 is and index 1 is . Three-qubit operators are Kronecker products.LocalCausalModel Λ has a probability measure ρ on a measurable space Λ and measurable response functions P j λ n α with values in that sum to one over . The fixed state is left implicit. Predictions are Bochner integrals, and all integrands are bounded and measurable.In emergent gravity proposals, spacetime and gravity are macroscopic descriptions of an underlying quantum system. In Verlinde (2016) it is argued that in de Sitter space (a universe with positive dark energy) the entanglement entropy has, besides the usual area-law part, a thermal volume-law part, and that matter displaces this volume-law entropy. The elastic response of the medium to this displacement produces an extra gravitational pull, which the paper proposes as the origin of the effects usually ascribed to dark matter in galaxies and clusters.
The physical derivation is heuristic, but it ends in explicit mathematical relations between the baryonic (visible) mass profile and the apparent dark matter mass profile of a spherically symmetric, isolated system. The central one is the integral relation (7.40),
where is Newton's constant and is the Hubble acceleration scale. For a point mass it reproduces Milgrom's empirical acceleration relation and the baryonic Tully-Fisher relation with .
All quantities are real numbers or real functions of the radius . and are constants. and are the baryonic and apparent dark masses inside radius . The Newtonian accelerations are and (7.42). The averaged density inside radius is (7.45), and the slope parameter is (7.46). A local density gives (7.39).
The paper also uses two purely mathematical facts about elastic strain in spatial dimensions: a bound (7.30) on the largest principal strain of a traceless symmetric strain tensor, and the integration-by-parts identity (7.31) between the squared Hessian and the squared Laplacian.
If is constant and (7.40) holds for every , then for every
The point-mass relation (7.43) is what connects the paper to the observed flat rotation curves and the baryonic Tully-Fisher law; (7.47) is its extension to extended mass profiles, which the paper uses to discuss galaxy clusters. The formal content checked here is the mathematics that turns the stated relation (7.40) into these observable consequences, plus the two elasticity lemmas used on the way to (7.40). The physical steps that lead to (7.40) (the entropy-displacement picture, the elastic interpretation, the identification (7.35)) are not mathematical statements and are outside the scope of this mission. None of these relations is known to have been machine-checked before.
The algebra is short once one may differentiate; the work is in the analysis. (7.40) is an integral identity with a singular weight at the origin, so recovering pointwise information requires the fundamental theorem of calculus on with only continuity there, and care with integrability at . (7.31) is a double integration by parts in that must be justified for the chosen decay class. (7.30) needs the spectral theorem for symmetric matrices, or an equivalent argument.
All statements live in the namespace Verlinde2016. Radial profiles are functions , with hypotheses only on . The integral in (7.40) is Lean's interval integral over ; since it would be for a non-integrable integrand, the positivity of the right-hand side forces integrability. Continuity of (and of densities) on is taken as a standing physical convention. In (7.31) the paper's condition that " falls off rapidly enough" is formalized as smooth with compact support. Spatial dimension is in (7.30); (7.40)–(7.51) use as in Section 7.2. Definitions: avgDensity, slopeParam, partialDeriv.
Liouville field theory is a two-dimensional conformal field theory whose classical equation of motion generalizes Liouville's equation. It is one of the few interacting conformal field theories with a continuous spectrum that has been solved: its three-point function on the sphere is given by the DOZZ formula (Dorn–Otto 1994; Zamolodchikov–Zamolodchikov 1996), proved rigorously from a probabilistic construction of the path integral by Kupiainen–Rhodes–Vargas (2017), with the conformal bootstrap established by Guillarmou–Kupiainen–Rhodes–Vargas (2020). It appears in two-dimensional quantum gravity, non-critical string theory, and log-correlated random energy models.
This mission is the first in a series following the Wikipedia article on Liouville field theory. It formalizes the kinematic layer of the theory: the algebraic relations between the coupling constant, the background charge, the central charge, the conformal dimensions and the reflection coefficient, on which every later statement (the spectrum, the DOZZ formula, the bootstrap) is phrased.
Fix a complex number , the coupling constant. Define
with sign if and otherwise.
Two symmetries act on these data: the reflection and the duality . The spectrum of the theory is the set of dimensions , parametrized by momenta , .
For every , the map is a bijection
These identities are the dictionary between the parameters used in the physics literature (, , , , , ) and fix the conventions for later missions in the series: the DOZZ formula, the pole structure of correlation functions, and the reflection and duality covariance of structure constants are all stated in these variables. None of these statements is open; the value of the mission is a vetted, reusable definition layer with machine-checked consistency of the conventions.
The individual statements are elementary algebra over , together with the non-vanishing of the Gamma function away from its poles. The care needed is in conventions: total functions in Lean (, principal-branch complex powers, Gamma at its poles) must be handled by explicit hypotheses exactly where the source implicitly excludes degenerate values.
All quantities are complex-valued functions of , defined in the namespace LiouvilleFieldTheory. is Lean's inverse (so gives junk values , ; statements that need assume it). is taken to be . The condition is encoded as . is the principal-branch complex power. The analytic content of the article (Virasoro representations, conformal blocks, the special function , the path integral, the DOZZ formula) is out of scope for this mission.