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?
An equation driven by fractional Brownian motion can respond to a rapidly varying coefficient even when that coefficient has no useful pointwise limit. Hairer and Li study this issue for fractional Brownian motion with Hurst index above one half. Their Section 3 isolates a deterministic averaging statement: if the time antiderivatives of the coefficients approach those of a limiting coefficient in a suitable negative Hölder norm, the solutions approach the limiting solution in probability. This statement supplies a common target for averaging models whose fast variables have very different origins. The authors use it later with mixing fast processes, and also present a quasi-periodic example. The result and its role in the paper are stated in Hairer and Li, Section 3.
The problem sits at the boundary of two familiar views of differential equations. A pathwise Young equation is defined from individual sufficiently regular paths, whereas the available estimates for the oscillating coefficient and the fractional Brownian driver involve probability and conditional expectation. The mission records the precise point where these descriptions meet. It treats the published article, rather than a preprint, and targets its Theorem 3.13.
An -dimensional fractional Brownian motion with index is a centered Gaussian process with independent coordinates and covariance
The paper works with a two-sided process and . It uses a version whose sample paths are locally -Hölder for every . The mission names that version condition separately, because the covariance law alone does not select particular sample paths. The relevant past sigma algebra at time is generated by increments with . These conventions come from pp. 1826 and 1831–1832 of the article.
For a path on , write for its homogeneous Hölder seminorm and for its supremum norm. The norm on is . A Young integral is the limit of left-point sums over partitions of as the largest cell shrinks to zero. A Young solution from is an -Hölder path satisfying its integral equation at every time, with value at time zero. Here means bounded, twice continuously differentiable maps with bounded derivatives through order two; means -Hölder in time with values in . These are the paper's conventions on pp. 1829 and 1835–1838.
The negative Hölder bound means that the time antiderivative of has increments bounded by , and that the difference of those increments at spatial points is bounded by . Both bounds apply on the time window in question when . This is equation (3.12) in the article. It measures cancellation over time; it does not require itself to be small.
The goal is the part of Theorem 3.13. Let be , let the limiting be autonomous and in , and suppose . The exponents satisfy , , , and . For Young solutions with the same starting point,
the target is
The milestone list follows the statements used around this target: the Hölder composition estimate of Lemma 2.1, the RKHS estimate of Lemma 3.3, the fractional Brownian integral estimate of Lemma 3.4, the stochastic sewing lemma of Lemma 3.5, the Young case of (3.18) from Lemmas 3.10 and 3.12, the Kolmogorov inclusions (3.24), and the deterministic stability estimate of Lemma 2.2. Each is a separate formal theorem. The authors' proofs follow their statements in Sections 2 and 3 and the Appendix; Lemma 3.5 is quoted from Lê, Theorem 2.1 without proof in the article.
The target gives convergence of entire solution paths in a Hölder topology, in probability. In the paper, this lets a model-specific estimate of the negative Hölder distance be used to conclude convergence of the corresponding dynamical system. Theorem A is obtained by adding such an estimate for a stationary mixing fast process; the deterministic statement here isolates the part independent of that model. These uses are described in Sections 1 and 3.
The published paper proves the result. This mission asks for machine-checked proofs of the stated Lean theorems. Its reusable work would include a pathwise Young integral over arbitrary partitions, Hölder norms that retain the value , a two-sided vector fractional Brownian motion interface, and stochastic estimates for time-dependent integrands. The goal and milestones in this proposal are statements with proof placeholders; the local build checks their types, not their proofs.
Pointwise control of is unavailable: a rapidly oscillating function can be large at most times and still have small time antiderivatives. Applying a pathwise Young stability estimate directly to therefore leaves a coefficient norm that need not tend to zero. The integral estimate must connect cancellation measured by with bounds on the driven equation. The dependence on the past of the fractional Brownian motion makes this step more delicate than an estimate for a deterministic integrand. The required estimates and their domains appear in Lemmas 3.4–3.12.
Time is for the two-sided driver; coefficient and solution assertions use with . State spaces are finite-dimensional real Euclidean spaces. The goal takes from the standing setting of Section 3.1, and it assumes the locally Hölder version of described on p. 1826. The solutions are required almost surely to satisfy the Young equation from the same . This requirement fixes the processes to the equations; the convergence claim cannot be obtained by choosing arbitrary paths. Probability of the norm event uses the measure of that set, and the conclusion is convergence in probability in the full norm.
The Lean definitions use for path and process seminorms, so unbounded suprema are not replaced by a default real value. The negative Hölder hypothesis uses real bounds instead of an infimum that could be meaningless on an empty class. The Young integral quantifies over every monotone partition and the mesh limit of its left-point sums. The fBm definition includes Gaussianity, means, and every cross-coordinate covariance; its path version is explicit. Interval integrals in the coefficient bound are applied to time-continuous coefficients in the goal. Lemmas 3.4 and 3.10 use the increment filtration, the case needed for this theorem.
The paper's Lemma 2.2 needs a common initial value for its homogeneous-seminorm estimate; the formal statement includes it and records the printed issue. The paper writes the limiting coefficient with a time argument but uses an autonomous coefficient in (3.23), which the goal adopts. This proposal covers the equation. The final extension in Theorem 3.13 and the conditional-expectation estimate (3.19) remain outside its current items. Contributions that close these gaps, or supply a general conditional Wiener integral matching the article's notation, would extend the development.
Principal component analysis (PCA) asks for the -dimensional affine subspace that best fits a cloud of points in in the least-squares sense. When is very large, or the points arrive as a stream or are spread over many machines, one wants to replace the data by a small summary on which the cost of every candidate subspace can still be evaluated, up to a factor . Such a summary is a coreset. Coresets for the -subspace problem are the building block of the streaming and distributed PCA and projective clustering algorithms of Feldman, Schmidt and Sohler (SIAM J. Comput. 49(3), 2020), whose sizes depend on and only, not on or .
For linear subspaces (through the origin) the paper's Theorem 17 gives a deterministic coreset of points read off the singular value decomposition. Data are rarely centred, though, and subtracting the mean before the computation does not survive the union of coresets with different means (p. 616). Section 4 of the paper repairs this: Theorem 19 gives a coreset for affine -subspaces whose points already carry the mean, at the price of doubling the size and weighting the points. This mission formalizes Theorem 19.
A data set of points in is a matrix whose rows are the points. For a nonempty set and a point , . The cost of is
and for weights on the rows of the weighted cost is . The squared Frobenius norm is .
A singular value decomposition (SVD) of is a factorization with and orthogonal and rectangular diagonal with nonnegative, nonincreasing diagonal entries . keeps the first diagonal entries and sets the rest to ; the -rank approximation is (Definition 1).
The mean row is and the centred matrix is , whose rows are .
Algorithm 1, subspace-Coreset, sets , returns the matrix of the first rows of (all other rows are zero), the weights , and .
Algorithm 2, affine--subspace-Coreset, runs Algorithm 1 on , obtaining with , and returns
together with .
Let , and , and let be the output of Algorithm 2 for any SVD of . Then , , , and for every affine -dimensional subspace of ,
Theorem 17 rests on Corollary 16 and Claim 3 of the paper; those are milestones of the companion mission Turning Big Data into Tiny Data … I and are not posed again here.
The result. Theorem 19 gives a deterministic summary of weighted points and one scalar that preserves the cost of every affine -subspace within , for arbitrary data, with no assumption on the mean. Because its points carry the mean, coresets of different data sets can be merged, which the merge-and-reduce streaming constructions of the paper's later sections need. Any -approximate PCA solution computed on the coreset is then a -approximate solution for the full data.
Formalizing it. The theorem is proved in the paper; no machine-checked proof of it, or of any coreset theorem, exists on the platform. A complete development would produce the cost identities for sums of squared distances to linear and affine subspaces in Lean, the effect of centring and orthogonal translation on these costs, and the use of the SVD truncation as a summary, all of which are reusable for other PCA, low-rank approximation and projective clustering results.
The obvious construction, centring the data, computing the linear coreset of the centred data and adding the mean back, fails: the linear coreset need not have mean , and translating a subspace by changes the cost of a point set by a multiple of that depends on the number of points (p. 617). The paper's construction has to match both the mean and the total weight of the original data while keeping the linear-subspace guarantee, and the formal proof has to carry this through the reduction of an arbitrary affine subspace to a linear one plus an orthogonal translation. Beneath it lies Theorem 17, which needs the SVD-based estimate of the companion mission (Corollary 16) and the passage from the -row matrix to the nonzero rows of . Distances to subspaces in Lean are infima over sets, so the identities for an orthonormal basis of must themselves be established.
Matrix (Fin n) (Fin d) ℝ, read as points of EuclideanSpace ℝ (Fin d). is Metric.infDist. Linear -subspaces are Submodules of finrank ; affine ones are AffineSubspaces whose direction has finrank , and is AffineSubspace.mk' t L. The SVD and are the published ProjLikeRetr.FixedRank.IsSVD and truncSVD. Every statement holds for an arbitrary SVD; none is chosen.A partially observable Markov decision process describes a controlled system whose state is hidden but whose observations are available to a decision maker. The distribution of the hidden state conditional on the observations is the belief state. Replacing the hidden state by this distribution turns the model into a fully observed decision process, provided the resulting belief transition has the regularity needed by the usual existence and dynamic programming results. Feinberg, Kasyanov, and Zgurovsky give sufficient conditions for that regularity in their study of total-cost POMDPs, Theorems 3.6 and 3.7.
Their observation-kernel condition is continuity in total variation. Example 4.1 of the same paper tests its sharpness: the authors construct a two-state model with setwise-continuous observations for which the belief transition fails to be weakly continuous. This matters when selecting assumptions for a POMDP theorem. Setwise convergence already requires convergence of the probabilities of every fixed observation event, so it can look adequate for belief updates. The example shows that it is still too weak for the stated conclusion.
The hidden state space is and the observation space is with Lebesgue probability measure . The action space is , equipped with the topology inherited from . The state does not move: its transition law is the point mass at for every action. Its continuity in total variation is immediate from this fixed-state behavior.
At hidden state 1 the observation law is always . At hidden state 2, action zero also produces . Under action , state 2 produces a law . The density equals zero on the open left half of each cell in the -part dyadic partition and equals two elsewhere, including the cell endpoints. Equation (4.1) gives the exact intervals. These laws oscillate more rapidly as grows, and the paper establishes for every fixed Borel set . Thus the observation kernel is setwise continuous even at the accumulation action zero. Example 4.1, pp. 13–14.
A belief assigns a probability to each hidden state. For a current belief and an action , the joint law covers the next state and its observation, and is the observation marginal. A filter is a conditional law of the next state given observation : it satisfies the disintegration identity (3.3). The belief transition is the law of the random posterior when has law . These objects are defined in (3.1)–(3.5) of the paper. Different versions of agree only almost everywhere for each current belief and action, yet they yield the same belief transition.
At the uniform belief , action zero reveals nothing, while every positive-index action produces the same two-point posterior law:
The mission's goal asserts that is total-variation continuous, is a setwise-continuous probability kernel, a valid filter exists, and the positive-index laws fail to converge weakly to the zero-action law as . It states the failure for every filter satisfying (3.3), so it is a property of the POMDP rather than of a selected version of its conditional distribution. The milestone list follows the paper's assertions: setwise convergence of the dyadic laws, setwise continuity of , the two posterior values almost everywhere, and the explicit laws of .
The example identifies a precise boundary of the sufficient condition in Theorems 3.6 and 3.7. Those theorems use total-variation continuity of the observation law to obtain a weakly continuous belief transition; replacing that premise by setwise continuity makes their continuity conclusion false in this model. The explicit law also shows the size of the discrepancy: the positive-index belief transition has two fixed atoms, while the zero-action transition is concentrated at the original belief. Example 4.1, pp. 13–14.
A machine-checked development would add reusable definitions of sequential kernel continuity, the joint state-observation law, conditional filters, and the belief transition on the Borel space of probability measures. It would also formalize a concrete setwise-convergent sequence of densities whose induced posterior laws do not converge weakly. The paper proves the example; the Lean statements in this proposal are open proof targets, with no completed machine-checked proof claimed here.
Setwise continuity controls for each fixed Borel set . A posterior is a probability measure determined by the observation, and the belief transition tests the distribution of those posterior measures. The observation regions distinguishing the states change with , so convergence on fixed observation sets does not imply convergence of their posterior distributions. This is the gap in the immediate argument that tries to pass from setwise convergence of to weak convergence of .
The conditional filter adds a second precision issue. Equation (3.3) determines its values only almost surely under the observation marginal, and different versions may disagree on null observations. Any claim about a posterior value at every would exceed the source; the posterior milestone therefore has an almost-everywhere qualifier, while the goal quantifies over every valid version of .
Lean represents by Fin 2, with 0 for the paper's state 1 and 1 for state 2; by unitInterval; and by the specified subtype of . Positive integers are a subtype of , so the density and the action are never evaluated at . The measure is volume on unitInterval, which has total mass one. The density follows (4.1) literally, with open zero intervals and density two at their endpoints. The general transition and observation law use Mathlib kernels; the example instantiates them directly. The goal includes the probability-kernel property of the concrete and existence of a valid , guarding the universal filter clause against vacuity.
Weak, setwise, and total-variation convergence are sequential, as on page 4. The weak test class consists of bounded continuous real functions; the setwise test class consists of all Borel sets. The target space of carries the Borel σ-algebra of the weak topology on , stated explicitly because Mathlib's default measurable structure on that type is the Giry σ-algebra. The filter predicate requires measurability in for fixed in both structures. Joint measurability in is described in the paper but is not encoded in this local predicate; only the fixed-parameter property is used by (3.3) and (3.5). This choice and its quantifier effect are recorded in the moderation notes.
No cost, initial observation kernel, initial prior, or discount factor enters Example 4.1. Contributions on the dyadic law, kernel continuity, conditional posterior values, and the resulting belief-law identity are all within scope. A filter hard-coded to return the prior belief, a discrete topology on , or a claim for only one version of would change the counterexample and is excluded by the definitions and goal.
Games with many interacting players appear in economics, epidemiology and network engineering: firms competing in a market, individuals deciding whether to vaccinate, agents in a social network choosing an effort level. When every player interacts with every other player symmetrically, mean field game theory replaces the finite game by a limit with a continuum of players. Real interactions are rarely symmetric: who influences whom is described by a network, and large networks are described in the limit by a graphon (Lovász, Large networks and graph limits, 2012).
Graphon games combine the two ideas. Parise and Ozdaglar (2018) studied deterministic graphon games with continuous strategy sets. Carmona, Cooney, Graves and Laurière (2019) introduced idiosyncratic random shocks, giving a stochastic graphon game in which each player's state is perturbed by independent noise, and proved existence, uniqueness and stability of Nash equilibria as well as convergence of finite network games to the graphon limit. This mission formalizes their existence theorem (Theorem 3.15).
The players form the interval with Lebesgue measure . Each player chooses an action ; a strategy profile is a function , defined up to -null sets.
A graphon is a symmetric, Borel-measurable function with . It acts on through the graphon operator
A state map and a noise law on define the state of a player who takes action , feels aggregate , and receives shock . Assumption 1 asks that and that has mean zero and a finite second moment.
The aggregate felt by the players under a profile is the solution of
A player choosing against aggregate pays . Assumption 4 asks that be continuously differentiable and -strongly convex uniformly in , and that be -Lipschitz in . Assumption 5 asks that be bounded: for some finite . The best response is the unique minimizer of .
A Nash equilibrium is a profile such that, for -a.e. player and every action ,
The statement fixes no constants and asserts no uniqueness.
The existence theorem holds under mild hypotheses: unlike the uniqueness result of the same paper (Proposition 3.17), it needs no smallness condition linking , and . Boundedness of the state map takes its place. Existence of a graphon equilibrium is the starting point for the paper's §4, where graphon equilibria are shown to be limits of equilibria of finite network games and to yield -Nash equilibria for them.
The result is proved in the paper; no part of it is machine-checked. A complete formalization yields reusable pieces beyond this mission: square-integrable kernel operators on with their operator norm, the Hilbert–Schmidt compactness of such operators, Lipschitz dependence of minimizers of uniformly strongly convex functions on a parameter, and Schauder's fixed-point theorem on a Banach space, which is not in Mathlib.
A contraction argument does not apply: the best-response-of-aggregate map is Lipschitz with constant , which may exceed under the hypotheses of the theorem. Existence therefore rests on a compactness fixed-point theorem in the infinite-dimensional space . That requires compactness of the integral operator , which Mathlib does not provide for kernel operators, and Schauder's theorem itself, which Mathlib does not have. A bounded convex set in is not compact, so Brouwer-type finite-dimensional arguments do not transfer directly.
All statements live in the namespace GraphonGames.Existence and share one definitions file.
unitInterval with volume. Profiles and aggregates are functions with MemLp _ 2 volume; equalities between them are almost-everywhere equalities.Trivializing encodings are excluded: the operator norm is not a real supremum that could collapse to ; an equilibrium must come with its aggregate solving (6), be square-integrable, and beat every action for almost every player; and no norm is converted to a real number where it could be infinite.
The results of §4 (Theorems 4.3, 4.7, 4.9 on finite network games) and the uniqueness and stability results (Proposition 3.17, Theorem 3.20) are not posed in this mission. Contributions welcome include Schauder's fixed-point theorem, the compactness of Hilbert–Schmidt integral operators on , and the contraction argument behind Proposition 3.1.
An online decision maker often sees information about a customer, patient, or request before choosing an action. A bandit with covariates models this setting when the reward of every available action is initially unknown and only the reward of the chosen action is observed. A method must learn which action works best for which covariates while paying for exploratory choices. Perchet and Rigollet studied this problem for smooth reward functions and measured how quickly a policy can approach the performance of an oracle that knows every arm's mean reward Perchet and Rigollet, 2013.
A fixed grid divides the covariate space at one resolution everywhere. It can spend pulls distinguishing arms in regions where their difference is already large, while leaving too few observations in regions where they are close. Adaptively binned successive elimination (ABSE) instead refines a region only while several arms remain plausible there. The paper proves a regret rate controlled jointly by the smoothness of the reward functions and the probability of encountering near ties. Its Theorem 5.1 is the target of this mission.
There are arms and covariates in the unit cube , with . At time , the policy sees , chooses an arm, and sees that arm's reward. The random vectors consisting of the covariate and all potential arm rewards are independent across times. Covariates have a common probability law with a density between constants . Every reward lies in ; for arm its conditional mean given is . The paper does not require the complete reward vectors to be identically distributed across time. These conventions come from §3.1, pp. 10–11.
At , write . Write for the largest mean strictly below , and set when every arm ties. The difference is the positive gap wherever a genuinely suboptimal arm exists. The smoothness condition requires for every arm, with the Euclidean norm, , and . The margin condition, with , , and , says
These are the assumptions defining the paper's class §3.2, pp. 12–13.
ABSE starts with the whole cube. Each live dyadic cell runs a copy of successive elimination on its inherited arms. One round pulls each remaining arm once. After a complete round, an arm is eliminated if its empirical mean falls more than twice the radius below the largest empirical mean, where is the cell's side length and uses . The cell splits after its specified stopping round if it has at least two active arms and is below the maximum depth . Each child receives the survivors. The policy takes as parameters and uses the current covariate and rewards it actually observed Policy 3, p. 22.
The goal is the finite- part of Theorem 5.1, p. 22. Fix , , , with , , and . There is one constant , depending on these parameters but not on , or the machine, such that for every , every and every machine of the class,
Here is ABSE and is its cumulative regret against an arm of maximum conditional mean at each covariate. The goal asserts the shape of the rate with an unspecified constant, which is the paper's form.
In attack order:
The result provides a performance guarantee for a policy that adapts its spatial resolution to observed evidence, under a class of nonparametric reward functions. It permits a direct comparison with a fixed-bin policy under the same smoothness and margin conditions. The paper proves the rate and discusses optimality in a minimax sense when §5, pp. 22–27. This mission asks for a machine-checked proof of the stated finite- regime; the Lean goal and milestones are currently open statements, so the paper's proof is the mathematical source rather than a completed formal proof.
A completed development would make the stochastic model, adaptive policy, cell geometry, and concentration estimates reusable for other contextual bandit analyses.
The main difficulty is the feedback loop between decisions and observations. A cell receives samples only when the covariate lands there, and its available arms depend on eliminations in its ancestors. Applying an ordinary concentration inequality to a fixed sequence of arm rewards does not by itself justify the bound at these random birth and stopping times. The formal proof must track the inherited active sets and the samples collected after each birth, then combine local error bounds across the tree. The appendix's maximal inequality controls a range of round counts; the regret argument also uses the small probability of covariates with nearly tied arm means §5, pp. 23–27 and Lemma A.1, p. 28.
Lean uses EuclideanSpace ℝ (Fin d) and a probability measure on its unit cube. The lower density bound ensures every valid dyadic cell has positive probability, so its conditional mean is defined by a real quotient. A consistent half-open boundary assignment turns the paper's cells, which are specified up to Lebesgue-null boundaries, into a partition on every path. The policy is a recursive state machine: at time it receives , chooses an arm from its prior state, and updates with only the reward of that arm. It does not receive the unknown means or any unobserved potential reward. The existential constant in the goal is quantified before , , the sample space, and the machine.
The finite- goal includes . The printed theorem omits it, although the proof uses it. Without it, a two-arm machine with constant means and has regret from the policy's first exploratory round, while the printed bound tends to zero when is large. The clause reads the margin condition as , the limit of for , because the page does not define it. The (5.3) milestone uses : the printed ordinary logarithm can be nonpositive at a finest cell, while the left side is a positive integer. The cell parameter and bursting after a full round follow Policy 3 and the proof where nearby prose or pseudocode differs. Lemma A.1 adds and , both implicit on the page. The constants and are existential and placed after the class parameters, because the page's explicit omits the margin constant .
The probabilistic error displays (5.6)–(5.9) and (5.11)–(5.14) are not milestones. They are statements about the events and , which the page leaves undefined for cells that are never born or never finish rounds. The decomposition (5.8) also leaves out arms of that were eliminated at an ancestor of . A faithful encoding of these events is welcome as a contribution.
A complete proof needs measurable recursive policies, conditional expectations and independence, dyadic-cell volume and nesting facts, concentration for arm observations at adaptive times, and sums over tree depths. Contributions establishing these interfaces and the paper's intermediate bounds are welcome. The result must apply to every machine in the stated class. Each of the following would change the theorem: a policy that reads the unknown or unobserved rewards (the oracle has zero regret), a constant chosen after the machine, a covariate law that is not a probability measure on the cube, Hölder continuity in the sup norm instead of the Euclidean norm, or dropping the density lower bound (cells of zero mass would make a junk value). The paper's proofs are in §5 (pp. 23–27) and its Appendix (p. 28).
Retailers set prices and stock levels without knowing how demand responds to price. They must learn the demand curve from their own sales while still earning money, which is the exploration–exploitation trade-off of dynamic pricing with learning (den Boer 2015). Two features of practice make the problem harder than the textbook bandit. First, demand is censored: when the shelf runs empty, the firm sees only its sales , not the demand . Second, firms change prices rarely, because of menu costs and customer reaction, so a policy may change its price at most times over the whole horizon (Cheung, Simchi-Levi and Wang 2017).
Chen, Chao and Wang study a firm facing both features at once, in a parametric model where the demand distribution is known up to a parameter. For the well-separated case they give an algorithm, Algorithm-I, whose regret grows as , and they show that no admissible policy does better in general. This mission formalizes the upper bound. A companion mission formalizes the lower bound.
A firm sells one product over periods . At the start of period it holds inventory (with ). It chooses a price and an order-up-to level with , and the order arrives at once. Demand then has probability mass function on , where and the parameter lies in , . Unmet demand is lost, and the firm observes only the sales . Leftover stock carries over, . Each unit left over costs and each lost sale costs . The single-period expected profit is
For each , is an optimal price, , and the clairvoyant value is .
A policy's decision in period may depend only on past decisions and past sales. The regret of a policy is
The family is well-separated (Definition 1) if for every price the pmfs , , are pairwise distinct.
Algorithm-I splits the horizon into stages of lengths for , with . Stage uses one price and the order-up-to target . The target equals the planned level , raised by when so that the sales carry information. At the end of the stage the algorithm computes the censored-data maximum-likelihood estimate (5). It then sets the next stage's decisions to a maximizer of (6). It changes its price at most times.
Under Assumption A (regularity of and of near the true ), Assumption 1 (Fisher-information bounds, a positive lower bound on the pmf, strict monotonicity of ), Definition 1, and the condition that every optimal order-up-to level exceeds , there is such that for all large
The constant may depend on the model, the true parameter and the algorithm's inputs. The rate is the content.
The upper bound shows that a budget of price changes costs only a regret even under censoring. With of order the rate drops to logarithmic (Theorem 3 of the paper). Together with the matching lower bound (Theorem 2), it identifies the exact price of limiting price changes in this model. Theorem B1 is a general transfer principle, from a large-deviation bound on an estimate to a optimality gap of the plug-in decision. It allows continuous and discrete decisions together and needs no unique optimizer. It is reusable for any parametric learning problem with that structure. Proposition 1 is a large-deviation bound for maximum likelihood from censored, dependent, non-identically distributed data. The paper notes that such results were not previously available in the statistics literature.
The results are proved in the paper's appendices. None of them has a machine-checked proof. A formalization would check the regret decomposition (23), the stagewise bookkeeping with ceilings, and the large-deviation argument for the censored MLE. It would also make the reading of several loosely stated steps exact (see Formalization scope).
The obvious argument plugs a consistent estimator into the optimizer and bounds the regret by the estimation error. It fails twice. The error of is of order , so a Lipschitz bound on the profit would give regret of order per stage, which is too large. The rate of Theorem B1 needs the first-order condition at an interior optimum and the exact gap between optimal and suboptimal discrete levels. Second, the data are censored and dependent. The censoring level depends on carried inventory, which depends on past demand and on past prices. The classical large-deviation results for maximum likelihood assume i.i.d. uncensored samples (Borovkov 1998) and do not apply. Proposition 1 needs a separate argument that the inventory target is reached in most periods with high probability.
The model is encoded with a scalar parameter. , and are as above. The pmf is positive exactly on and sums to one, and is allowed. The expected profit is built from these sums. is the finite maximum for a price selection , not a real supremum. Periods are 0-based in Lean, while stages keep the paper's indices. Expectations and probabilities are sums over demand paths weighted by , the law of the path under the algorithm, taken in . Every regret summand is nonnegative.
Algorithm-I reads demand only through sales. Step 2's arg max is any maximizer of the censored product likelihood, which exists by compactness. Step 3's arg max is , any maximizer of , together with the price of Assumption A(iii). This is the decision the proof of Theorem B1 analyses. Proposition 1's "large enough " is read as "large enough , uniformly in the stage and in ". Theorem B1 is stated for a scalar price and level and a parameter in .
Three hypotheses are added and disclosed. Differentiability of in is presupposed by Assumption 1. Finiteness of the mean demand is needed for (4) when . The condition is needed because Step 1 defines the target only for . "The optimal order-up-to level exceeds " is read for every optimal level.
A trivializing formalization is ruled out. Regret and probabilities are path sums of nonnegative terms, not Bochner integrals that vanish on non-integrable inputs. is a real power. The hypotheses are jointly satisfiable: a Bernoulli instance with , , , satisfies all of them, together with explicit selections, and this has been verified in Lean.
A complete development needs the following:
Theorem B1 and the model definitions are reusable for the paper's later results (Theorems 3, 5, 6), which repeat these arguments. Contributions to any milestone are welcome, including alternative proofs of Proposition 1.
A queue layout of a graph places its vertices on a line and splits its edges into classes, called queues, so that inside one queue no edge is nested inside another. The minimum number of queues is the queue-number. Queue layouts were introduced by Heath, Leighton and Rosenberg (1992) and Heath and Rosenberg (1992) as the dual of stack layouts (book embeddings): reading the vertex order from left to right, the edges of one queue are opened and closed in first-in first-out order. Queue layouts are closely tied to track layouts and, through them, to three-dimensional grid drawings of graphs (§9 of the paper).
Whether planar graphs have bounded queue-number was asked by Heath, Leighton and Rosenberg in 1992 and stayed open for 27 years. The best general bounds before 2019 grew with the number of vertices: by Heath, Leighton and Rosenberg (1992), by Di Battista, Frati and Pach (2013), and by Dujmović (2015); for Euler genus , Dujmović, Morin and Wood (2017) had . Dujmović, Joret, Micek, Morin, Ueckerdt and Wood (arXiv:1904.04791, J. ACM 2020) proved that every planar graph has queue-number at most (Theorem 1), and extended the result to every graph embeddable in a fixed surface (Theorem 2) and to every proper minor-closed class (Theorem 3).
This mission is Theorem 2: graphs of Euler genus have queue-number at most . It is the second mission of a two-mission series; the first poses Theorem 1.
All graphs are finite and simple. A linear ordering of the vertex set is fixed. Two edges and with four distinct ends nest if (after renaming the ends). A queue is a set of edges no two of which nest. A -queue layout of is a linear ordering together with a partition of into queues, and means that a -queue layout exists.
A layering of is an ordered partition of such that every edge joins two vertices of the same or of consecutive layers. A BFS layering takes one root in each connected component and puts in layer . A BFS spanning tree of a connected graph rooted at is a spanning tree with for every . A path in is vertical if the distance to grows by exactly one at every step.
The Euler genus of the orientable surface with handles is , and that of the non-orientable surface with cross-caps is ; the Euler genus of a graph is the least Euler genus of a surface it embeds in (footnote 2 of the paper). Planar graphs are exactly the graphs of Euler genus . Combinatorially, an embedding of a graph is described by an embedding scheme: a cyclic order of the edges at each vertex (a rotation system) together with a sign on every edge (twisted or not). Tracing faces through the scheme gives a face count , and with vertices, edges and components the scheme has Euler genus .
The paper states Theorem 2 as and proves the explicit bound in §5. The goal poses that explicit bound, for every finite graph, connected or not.
The result. Theorem 2 settles boundedness of the queue-number for every class of graphs embeddable in a fixed surface, with a bound linear in the Euler genus. Through the connection between queue-number and track-number, the paper derives from it (§9, Theorems 54 and 58) that a graph of Euler genus with vertices has track-number and a three-dimensional grid drawing of volume , linear in for every fixed surface. It is also a step on the paper's route to Theorem 3 (proper minor-closed classes), since graphs on surfaces are the basic pieces of the Robertson–Seymour graph minor structure theorem. Lemma 21 is of independent use: it reduces a graph on a surface to a planar graph while controlling BFS layers.
Formalizing it. The result is proved; as far as is known it has no machine-checked proof. A formalization needs queue layouts, layerings, BFS layerings and vertical paths, and, independently of queues, a usable combinatorial theory of graphs on surfaces, which Lean's Mathlib does not have. The Euler genus definition of this mission (embedding schemes and face tracing) and Lemma 21 are reusable well beyond queue layouts.
The obvious reduction, deleting few vertices to make the graph planar, is not enough: a planar subgraph alone does not control how the deleted vertices interact with a queue layout. The deleted set must be thin in every BFS layer, and the planar remainder must carry a BFS layering compatible with the original one, which is what Lemma 21 provides. Its proof cuts the surface along a subgraph made of tree paths and must show that the cut graph is planar by an Euler-characteristic count over face-tracing data, and that distances from a new root agree with the old BFS distances. In Lean, the main obstacle is the surface side: Euler's formula for embedding schemes, the cutting operation on rotation systems, and the passage between the combinatorial notion of Euler genus and the drawing-based notion of planarity. The planar input, Lemma 18, is itself the whole of mission 1's argument (Theorem 15 with Lemmas 5 and 8).
SimpleGraph V on a finite type V : Type with decidable equality and adjacency.HasQueueLayout G k: an injective map ord : V → ℕ (the linear ordering) and an assignment of the edges of (G.edgeSet, not all unordered pairs) to Fin k such that no two edges in one queue nest; nesting uses strict inequalities, so edges sharing an end never nest. Queues may be empty.L : V → ℕ; a BFS layering takes one root per component. Vertical paths are nonempty lists indexed from with distance , .EulerGenusLE G g asks for an embedding scheme (rotation permutation of the darts, cyclic at every vertex, and a symmetric edge signature) whose Euler genus , computed in , is at most . The face count is half the number of face-tracing orbits plus the number of isolated vertices. Equivalence with footnote 2's topological definition is the Heffter–Edmonds–Ringel rotation principle and its non-orientable extension, with additivity over components; it is not part of the mission.RobertsonSeymour1986.GM5.IsPlanar: a crossing-free drawing in by simple arcs. "Euler genus iff planar" is a theorem connecting the two definitions, not built into either.Sym2 V would deny edgeless graphs a -queue layout; non-strict nesting would forbid adjacent edges in one queue; a drawing that tolerates crossings would make every graph planar; a face count without halving, or without isolated vertices, would make the Euler genus too small or too large (the sanity checks confirm has a scheme of Euler genus , a twisted one of genus , and two isolated vertices genus ).First-order hyperbolic systems of balance laws model open-channel flow (the Saint-Venant equations), gas pipelines, traffic and heat exchangers. In most of these applications the state can be acted on only at one end of the domain, so stabilizing an equilibrium is a boundary control problem. For systems without source term (), static boundary feedback built from a Lyapunov function works (Coron–Bastin–d'Andréa-Novel 2008); with a source term, Lyapunov functions of the diagonal form can fail (Bastin and Coron 2011, recalled in Remark 1 of the paper). Backstepping, introduced for parabolic equations by Krstic and Smyshlyaev, replaces the search for a Lyapunov function by an invertible integral change of variables that maps the linearized plant to a target system whose stability is evident.
Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475v1, 2012; SIAM J. Control Optim. 51(3), 2013) design such a feedback for the linearization of a quasilinear system and prove that it stabilizes the nonlinear system locally in . This mission formalizes that main result, Theorem 4.1.
The state is on , , governed by
The standing assumptions (§2) are: , , are ; with on ; ; . Write and ; the paper treats .
The scaling , , , removes the diagonal of the linearization, which becomes with , , , and antidiagonal with entries , . The kernels solve a pair of first-order hyperbolic equations on the triangle with boundary data on its diagonal and on the edge ((3.32), (3.33), (3.36), (3.37)). The gain is .
The closed loop adds a dynamic extension:
with , , and , determined by the initial profile through two linear functionals , . The norm is on .
For every there are such that every classical solution with satisfying the compatibility conditions (4.16), (4.18) obeys
Write for the full kernel , , , and .
Theorem 4.1 shows that a feedback computed entirely from the linearization, by solving linear kernel equations, is a valid local stabilizer of the quasilinear system in , the natural space for classical solutions of quasilinear hyperbolic systems. The dynamic extension is what makes the result usable: without it, the static feedback imposes artificial compatibility conditions (4.17), (4.19) on the initial data.
The result is proved in the paper (§5 and Appendix B); none of it is machine-checked. A formal proof needs a rigorous treatment of the Volterra transformation and its inverse in , the three-level Lyapunov argument (, , ), and the comparison of these functionals with the norm. The formalization also records corrections to the printed formulas: the sign of in (4.1), the entries of in (4.7), the initial values (4.26), and the admissible decay rates (see below).
The obvious argument — the linear closed loop is exponentially stable, so the nonlinear one is locally stable — fails for hyperbolic systems: the nonlinear terms contain a derivative of the state, so they are not small in relative to , and an estimate does not close. One must control , and simultaneously, each with its own Lyapunov functional whose weight depends on the state, and exchange time derivatives for space derivatives through the equation, which is possible only while and stay small.
States are Fin 2 → ℝ, matrices Matrix (Fin 2) (Fin 2) ℝ, indices 0-based. A solution is one function (space first) with the PDE imposed on and the boundary conditions for ; this is the theorem restricted to classical solutions, since Mathlib has no Sobolev spaces. Global existence is not asserted. Coefficient functions are defined on all of with global regularity and sign conditions on . , norms are sums of norms, as on p. 11; uses .
Added or corrected relative to the page, all disclosed in the items:
Trivializing formalizations are ruled out: , and every milestone constant are quantified after the data and before the solution; the kernels are pinned down by all their equations and boundary conditions (unique by Theorem A.1 of the paper); the corrected , are the ones every classical solution has, so no small initial profile is excluded; and the norm contains .
Not formalized: Lemma 5.2 (its printed bound (5.38), , fails for profiles with small and large , and (5.37) compares a matrix with a scalar), and Lemmas B.1–B.4, B.7, B.8. Contributions of a reusable theory of Volterra integral transformations on with kernels, and of the comparison between sup and norms of solutions of hyperbolic systems, are welcome.
The adjacency matrix of an Erdős–Rényi random graph contains a large deterministic mean as well as random fluctuations. The mean affects the largest eigenvalue, while the centered fluctuations determine much of the remaining spectrum. A local spectral law must describe both pieces at a resolution fine enough to distinguish eigenvalues within a narrow energy window. Erdős, Knowles, Yau and Yin established such estimates for a broader class of sparse symmetric matrices and their noncentered rank-one deformations in Spectral statistics of Erdős–Rényi graphs I. This mission formalizes the paper's Theorem 2.9, with the centered-matrix law and eleven intermediate results of the paper as milestones.
The paper treats the graph matrix through a model that also allows other sparse distributions. Its parameters and separate sparsity from the size of the deterministic mean. That separation matters: the normalized resolvent trace can obey a local semicircle law even when the deformation produces a distinguished top eigenvalue. The formal target therefore concerns the deformed matrix itself, rather than replacing it with the centered matrix.
For each size , let be a real symmetric random matrix. Entries indexed by the upper triangle are independent, centered, and have variance . Their higher moments obey
The sparsity parameter lies between and , and the logarithmic parameter satisfies , with and . Define and the noncentered matrix , where . The projection has every entry equal to . These are Definitions 2.1 and 2.2 of the source paper, pp. 5–6.
For a complex number with , the resolvents are and . Their normalized traces are and . The comparison object is the semicircle density and its Stieltjes transform . Put and for a fixed . These definitions appear in Section 2, pp. 7–9.
An -dependent event has -high probability when its failure probability is at most for all sufficiently large . The spectral estimates below refer to single events on which the claimed bound holds at every simultaneously.
Theorem 2.9 assumes and . Its first conclusion is that, with -high probability, every satisfies
Under the additional bound , its second conclusion controls every entry at every :
The constants are universal and positive. The probability exponent may depend on the fixed parameters named in the theorem. Both conclusions, including the extra condition on in the second, are retained from Theorem 2.9, pp. 9–10.
The milestones follow the paper's own sequence of numbered results.
The trace estimate gives quantitative control over spectral mass at local scales, including near the edges . The entrywise estimate says more: each resolvent entry is close to the diagonal semicircle approximation with an error that records both sparsity and finite-size effects. The paper's later results derive density-of-states and eigenvector statements from these local controls. Those consequences are outside this mission's goal.
The intended formal development supplies reusable definitions of sparse symmetric ensembles, high-probability events, semicircle transforms, and complex resolvents, followed by exact statements of the paper's estimates. Mathlib contains no local semicircle law, for Wigner or for sparse matrices, and no Stieltjes transform of the semicircle distribution; the local law, the large deviation bounds and the interlacing lemma are each reusable beyond this paper.
The deterministic rank-one comparison controls the normalized trace but does not by itself control each entry of . The entrywise estimate must account for the deformation and for fluctuations caused by sparse entries. Near the spectral edges, the stability scale of the semicircle transform changes with ; a bound that is uniform in the bulk does not automatically retain the paper's edge behavior. The theorem also asks for one event covering a continuum of values, so a collection of separate fixed- probability bounds has the wrong quantifier order. These are substantive parts of Sections 3–7, beyond algebraic manipulation of resolvents.
Lean represents all on one probability space and takes their entries to be real, symmetric, measurable random variables, independent in the upper triangle. Conditions involving and the moments hold for all sufficiently large ; this avoids impossible small- parameter bounds and matches the asymptotic theorem. The moment order is real, as in the paper. Each finite expectation has an explicit integrability condition. A single positive constant is used for the moment, sparsity, and deformation bounds: replacing several fixed constants by their maximum preserves all three inequalities.
Matrix indices use Fin N rather than the paper's . The resolvent is a complex matrix formed by coercing the real matrix before subtracting . Every result that uses it restricts eventually or explicitly; its inverse at a singular input is never used to make a claim. The semicircle transform is defined by the paper's integral, and uses Lean's nonnegative square root, implementing the positive part. The high-probability predicate evaluates the measure of arbitrary sets, so it can state the intersection over all without a separate measurability assumption on that intersection. Positive and positive square-root arguments follow eventually from the model and .
The deterministic Lemmas 3.2, 3.4, 3.10, 6.1 and 7.1 are stated for every real symmetric matrix and every with (Lemma 3.2 on ); the paper's is contained there. Minors keep the original index names, and is only used for . is the explicit expression of (3.15). Ordered eigenvalues are the sorted roots of the characteristic polynomial. Statements the paper makes "for fixed " (Lemmas 4.1, 7.7, Proposition 7.6) are uniform in : one threshold serves every . The unnamed constants , , are chosen after the fixed parameters and before the random matrices; the universal come first.
Trivializing encodings are ruled out: every resolvent is taken at , so the junk inverse of a singular matrix never enters; the model is satisfiable (independent Rademacher signs divided by with and satisfy it for large ); each event of the goal is one intersection over all , not a family of pointwise bounds; the constants appear in the paper's order; and the goal is about with allowed to be large, so it does not reduce to Theorem 2.8.
Part (iii) of Lemma 3.8 is not a milestone: the printed (3.22) omits the diagonal variance term , without which it fails for Rademacher variables with . Contributions of proofs of any milestone, and of the missing groundwork (Stieltjes transforms of measures, Schur complements of resolvents, moment bounds for sums of independent variables), are welcome.
Deciding whether a bipartite quantum state is entangled is a basic computational problem of quantum information theory, and it is NP-hard in general (Gurvits 2003). The most widely used family of tests is the DPS hierarchy of Doherty, Parrilo and Spedalieri (DPS 2002, DPS 2004): a sequence of semidefinite programs, indexed by an integer level , whose feasible sets shrink to the set of separable states. On the dual side, a matrix that is nonnegative on separable states is an entanglement witness, and certifying such witnesses is the problem of certifying nonnegativity of a biquadratic Hermitian form, a classical question in real algebraic geometry.
That the DPS hierarchy is, dually, a sum-of-squares hierarchy for these forms has been used repeatedly in the literature, but, as Fang and Fawzi note (arXiv:1908.05155v1, p. 4), without a formal and complete proof. Their Theorem 12 gives one. They then combine it with their sum-of-squares convergence rate on the sphere (Theorem 2 of the same paper) to recover the convergence rate of Navascués, Owari and Plenio 2009 for the DPS hierarchy.
Timeline:
Let and . A matrix on has entries (row , column ); is the space of Hermitian ones.
for all and all , with ranging over .
Theorem 12 makes the DPS hierarchy and the sum-of-squares hierarchy for biquadratic forms interchangeable. A convergence bound for one is a convergence bound for the other: the paper uses this to derive the DPS rate (Theorem 15) from a rate for sums of squares on the sphere, and conversely quantum de Finetti arguments give sum-of-squares bounds. Part (iii) separates the two notions of Hermitian sum of squares: dropping the partial transposes corresponds exactly to passing from real to complex sums of squares. This explains, for example, why (rsos but not csos) behaves differently in the two hierarchies.
The results are proved on paper; none is formalized. The mission produces a machine-checked statement and proof of the duality, together with the matrix-analytic infrastructure behind it: partial traces and partial transposes on , the symmetric projector, conic duality for semidefinite cones, and the passage between Gram matrices and sums of squares. Theorem 15 additionally depends on the sphere rate of the companion mission (Theorem 6 there) and on the unproved Lemma 13 and display (26) of the paper.
The inclusion of each sum-of-squares cone in the corresponding dual cone is a direct computation. The reverse inclusions are harder: a certificate involving arbitrary Hermitian polynomials must yield positive semidefinite matrices indexed by the prescribed tensor products, even though its square terms can mix different patterns of complex conjugation. Likewise, weak semidefinite duality alone does not show that every element of has the displayed finite certificate; limits of certificates may require a separate closedness argument. The symmetric-subspace condition adds another constraint because an extension must be supported on that subspace, not merely invariant under permutations.
Fin dA × Fin dB (Mathlib's Kronecker convention); is Fin dA × (Fin ℓ → Fin dB).Matrix.PosSemidef (which includes Hermitian). Dual cones are subsets of with the pairing .MvPolynomial over ) in the real and imaginary parts of ; csos is a finite sum of with complex polynomials in only. Swapping the two, or allowing complex in rsos, would change parts (ii) and (iii).No trivializing reading is available: the cones are defined by their page conditions, the dual cones keep the Hermitian constraint, and no degree bound or extra hypothesis is placed on the sums of squares. Welcome contributions include a general library for partial traces and transposes of multipartite matrices, the spanning property of in the symmetric subspace, and Gram-matrix characterizations of sums of squares of polynomials; all are reusable well beyond this mission.
A decision maker who must choose to minimize an expected cost rarely knows the distribution of the uncertain parameter ; what is available is a sample . Sample average approximation (SAA) replaces by the empirical distribution. Data-driven distributionally robust optimization (DRO) instead minimizes the worst case of the expected cost over a set of distributions built from the data, which protects against the error of the empirical distribution at small . Many such sets have been proposed: moment sets (Delage and Ye, 2010), -divergence balls (Ben-Tal et al., 2013), Wasserstein balls (Mohajerin Esfahani and Kuhn, 2018).
Bertsimas, Gupta and Kallus (arXiv:1408.4445v3; Mathematical Programming, 2018, doi:10.1007/s10107-017-1174-z) observe that each such set can be read as the confidence region of a statistical goodness-of-fit (GoF) test, and call the resulting method Robust SAA. A basic question for any such method is whether, as , its objective, optimal value and optimal solutions converge to those of the full-information problem. The paper answers it for all data-driven DROs at once, with a single property of the test.
The support of is closed, and is the set of Borel probability distributions on with the topology of weak convergence. The data are i.i.d. from an unknown . A data-driven uncertainty set (DUS) map assigns to each sample a set ; it is the confidence region of the test that rejects a hypothesis exactly when . Decisions lie in a closed set , the cost is , and the robust objective is the worst-case expectation
A test is uniformly consistent (Definition 3) if, for every data-generating , almost surely every sequence that does not converge weakly to lies outside for infinitely many . The admissible instances are those satisfying three assumptions: (1) is equicontinuous in uniformly over ; (2) is bounded, or is coercive in uniformly over a set of positive -probability and bounded below off ; (3) is bounded, or there is a growth function with whose expectation the DUS tracks: almost surely. The convergence conditions are (18) uniformly on compact subsets of ; (19) convergence of optimal values; and (20) every sequence of robust minimizers has a limit point, and all its limit points are true minimizers.
For a DUS map with nonempty sets,
The statement carries no rates and no constants; it is a characterization, so it does not depend on any particular test.
The result. Theorem 2 reduces the asymptotic analysis of a data-driven DRO to a property of a statistical test, which can be checked once per test rather than once per optimization model. The paper uses it to classify DUSs: the and G-tests on a finite support and the Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling tests on the line are uniformly consistent (Theorems 4–5, separate missions of this series), while the test of marginals is not even consistent and so cannot give convergence for every cost. The necessity direction makes the property sharp: a weaker test always admits a well-behaved cost on which the DRO fails to converge. Theorem 3 explains the remaining cases where a DRO converges for one given cost.
Formalizing it. The result is proved in the paper (§10.5), but its proof leans on several standard facts used without detail: the portmanteau theorem, uniform integrability arguments from Billingsley's Convergence of Probability Measures, the Lévy continuity theorem with the Cramér–Wold device, and coercivity arguments carried over from the paper's Theorem 1. A machine-checked version would fix exactly which regularity of the cost these steps need; three such conditions are stated explicitly here (see the scope section). No part of the result is formalized elsewhere to our knowledge; the platform has no notion of a data-driven uncertainty set or of uniform consistency.
Uniform consistency is a statement about weak convergence, while (18)–(20) are statements about expectations of an unbounded, -dependent cost under the members of . Weak convergence controls expectations only of bounded continuous functions, so the "only if" side must recover convergence of from Assumption 3, which requires uniform integrability, and then upgrade pointwise convergence to uniform convergence on compacts and to convergence of minimizers when is unbounded. The tempting route through a single limiting minimization problem fails: the sets change with the sample, the worst case is a supremum over infinitely many distributions, and the minimizers of could escape to infinity unless coercivity on transfers to every member of . The "if" side needs, from the mere failure of uniform consistency, a single admissible cost whose worst-case objective detects every failure of weak convergence.
Points are EuclideanSpace ℝ (Fin d), distributions are ProbabilityMeasure ↥Ξ (whose topology is weak convergence), and the data live on the canonical product space with the product law, 0-indexed. "Almost surely" is ∀ᵐ, and in Definition 3 one null set serves every sequence . An expectation over a member of is when the integrand is not integrable, never Lean's default . Minima in (19)–(20) are infima in the extended reals, so the empty and unattained cases need no special treatment; (20) applies to sequences that are minimizers for all large .
Four hypotheses are added to the page, each used by the paper's own proof: every is nonempty (otherwise the worst case is and uniform consistency is vacuous); is continuous on ; the set of Assumption 2b is open; the growth function of Assumption 3b is continuous, with as fixed on p. 10 of the paper. Theorem 3 additionally assumes Assumption 2, which its proof uses. Proposition 4 assumes the rejection events are measurable. A formalization in which the worst case uses the raw Bochner integral, the supremum ranges over a possibly empty set, or (20) requires minimizers at would make the statements false or vacuous, and is ruled out.
A full development needs weak convergence and the portmanteau theorem (in Mathlib), uniform integrability and its relation to convergence of means under weak convergence, the strong law of large numbers for the growth function and the empirical measure, the Lévy continuity theorem in several dimensions (in Mathlib, via characteristic functions), and a countable convergence-determining class of bounded continuous functions. The uniform-integrability step and the path characterization of local uniform convergence (Proposition 9) are reusable beyond this mission. Contributions to any milestone are welcome; Proposition 9 is self-contained and deterministic.
Bayesian inference, statistical physics and machine learning all ask for samples from a probability distribution on whose density is known only up to a constant, . The unadjusted Langevin algorithm (ULA) is the Euler–Maruyama discretisation of the Langevin diffusion, whose invariant law is . It needs only gradients of , has no accept/reject step, and is therefore cheap in high dimension. Without the Metropolis correction, however, the chain does not leave invariant, so its usefulness rests on quantitative bounds: how far, in total variation, the law of the -th iterate is from , as an explicit function of the dimension , the step sizes and the regularity of .
Durmus and Moulines (arXiv:1507.05021, Ann. Appl. Probab. 27(3), 2017) gave such bounds for constant and decreasing step sizes. Earlier work of Dalalyan (arXiv:1412.7392, 2017) treated strongly log-concave targets with constant steps. Durmus and Moulines cover nonincreasing step sequences and, among other regimes, potentials that are only strongly convex outside a ball; this mission formalizes that case.
Write and for the Euclidean norm and inner product of . The total variation norm of a difference of probability measures is
which ranges in .
The potential satisfies two assumptions:
The point is a minimiser of , and .
The Langevin diffusion is , with a standard -dimensional Brownian motion. Its transition semigroup is .
ULA with step sizes is the chain
with i.i.d. standard Gaussian. Its one-step kernel is , and is the law of started at . Write , and let .
The explicit constants use
Let , and let be positive and nonincreasing with . Then for all and ,
The three constants are explicit:
The paper's proofs follow each statement in the body of the paper (§4.1, §4.12, §5, §5.1).
The theorem bounds the sampling error of ULA in total variation non-asymptotically, with a dimension-free contraction rate and constants polynomial in . With steps decreasing to zero and cumulative step size diverging, its bound gives convergence of to ; for constant steps, the paper reports iteration counts of order at a prescribed precision in Table 2. H3 covers log-concave targets whose potential can lack strong convexity inside a ball.
The result is proved in the paper but, as far as the platform's catalogue shows, not formalized anywhere. A formalization adds machine-checked versions of several reusable pieces:
The ULA chain is not reversible with respect to , so the spectral and Dirichlet-form tools of reversible MCMC do not apply to it directly. The bound must instead compare the chain with the continuous diffusion.
That comparison needs Girsanov's theorem on path space and a uniform control of along a time-inhomogeneous chain.
The rate of the diffusion itself is the second obstacle. Without global strong convexity, synchronous coupling gives no contraction inside the ball . An explicit rate requires a reflection coupling together with return-time estimates, and it has to be transferred through the time change between and .
The state space is the published EthierKurtz.SDEState d, i.e. EuclideanSpace ℝ (Fin d), and Brownian motion and strong solutions are the published EthierKurtz.IsStandardBrownian and EthierKurtz.SolvesBrownianSDE. The conventions are:
Measure.bind with the Gaussian kernel . Steps are indexed from , and for .Several hypotheses are added or read in a particular way, and each is disclosed in the item's statement:
The citations [20] (existence of solutions), [27] (Lindvall), [32] (Meyn–Tweedie) and Girsanov's theorem are used inside the proofs and are not restated.
The library work needed is substantial: Itô calculus for the reflection coupling, Girsanov's theorem, Pinsker's inequality in this norm, and generator–drift arguments for the moments of . Contributions of any of these as standalone platform theorems are welcome.
Robust Sample Average Approximation (Robust SAA) is a data-driven approach to stochastic optimization proposed by Bertsimas, Gupta and Kallus (arXiv:1408.4445; Mathematical Programming (2018), doi:10.1007/s10107-017-1174-z). Instead of minimizing the empirical average of a cost, a decision maker minimizes the worst-case expected cost over a distributional uncertainty set: the set of distributions that a statistical goodness-of-fit (GoF) test does not reject at a chosen significance level, given the observed data. Each classical GoF test therefore produces its own robust optimization model.
Whether such a model behaves well as data accumulate depends on a property of the test. Theorem 2 of the paper shows that Robust SAA converges, in objective, optimal value and optimal solutions, for every admissible cost if and only if the underlying test is uniformly consistent. This mission concerns the univariate case: it asks for a proof that the five standard tests on the real line, those of Kolmogorov–Smirnov, Kuiper, Cramér–von Mises, Watson and Anderson–Darling, are uniformly consistent (Theorem 5, p. 14). The companion missions of the series treat the characterization (Theorem 2) and the discrete χ² and G-tests (Theorem 4).
Let be a probability distribution on , and let be independent draws from . As in §3.2 of the paper, is a continuous random variable: has no atoms. For a candidate distribution write for its cdf, and write for the sorted sample of size . With , the five statistics (8) are
For a statistic and a threshold , the confidence region (7) is : the distributions the test does not reject. A test is uniformly consistent (Definition 3, p. 13) if, for every data-generating , almost surely every sequence that does not converge weakly to is rejected infinitely often, i.e. for infinitely many . The Lévy metric between cdfs is , and denotes the empirical cdf.
For thresholds with for some constant and all ,
The statement fixes only the rate of the thresholds, which is all the paper's argument uses; it holds for any sequence with that rate, in particular for the tabulated quantiles .
The result. Together with Theorem 2 of the paper, Theorem 5 guarantees that Robust SAA built on any of these five univariate tests converges for every cost that is equicontinuous in the decision and satisfies the paper's growth conditions. It also feeds Proposition 5, which extends the guarantee to multivariate problems with separable costs by testing marginals. Without it, the univariate tests would carry only the finite-sample guarantee of Proposition 1 and no asymptotic one.
The formalization. The theorem is proved in the paper, but the published argument for the Watson test has a gap. Its last step asserts that whenever , which fails when stays bounded away from (at the expression tends to ). The Watson clause is believed true, but a complete proof needs a different argument. The Anderson–Darling step relies on a cited integral representation rather than an argument on the page. A machine-checked proof would close both points. No part of the theorem is formalized elsewhere, as far as a search of the platform shows.
The Kolmogorov–Smirnov case reduces to deterministic inequalities once the Lévy-metric picture is in place, but each of the other statistics controls only indirectly. The Cramér–von Mises statistic is an quantity, and an bound does not by itself control a supremum. What closes the gap is monotonicity of together with the rate of the threshold, so a threshold that merely tends to is not enough. The Watson statistic is invariant under cyclic rotation of the transformed sample on the circle , so a small leaves the centring term uncontrolled until the boundary constraints are used. The obvious attempt, bounding the centring term by alone, is the step that fails on p. 39.
Distributions are MeasureTheory.ProbabilityMeasure ℝ, with weak convergence as their topology. The cdf is Mathlib's ProbabilityTheory.cdf. The data are the coordinates of the canonical product space ℕ → ℝ under Measure.infinitePi, so the sample of size is . Order statistics are the sorted sample s ∘ Tuple.sort s, and every formula of (8) is written with the paper's 1-based index ( in Lean is the paper's ; is Fin.rev i).
Committed conventions:
IsContinuousLaw), although the paper's proof does not use it;Uniform consistency is quantified over all sequences inside the almost-sure event, as in Definition 3. A pointwise consistency statement for a fixed is a different and weaker theorem and does not count.
A full development needs the Lévy metric and its metrization of weak convergence on , the Glivenko–Cantelli theorem in Lévy form, and elementary order-statistic inequalities. The first two are reusable well beyond this mission. Contributions of independent value include a corrected proof of the Watson step, and a proof of the goal without the atomless hypothesis.
A decision made from sampled data can be sensitive to the distribution chosen to represent future uncertainty. Robust sample average approximation addresses this by optimizing against every distribution that passes a goodness of fit test, rather than against one fitted distribution. The resulting set of plausible laws is a data driven uncertainty set. Its finite sample coverage and its behavior as the sample grows serve different purposes: coverage protects against sampling error at a chosen sample size, while convergence asks whether the uncertainty set eventually stops admitting laws far from the true one. Bertsimas, Gupta, and Kallus distinguish these properties in their Robust Sample Average Approximation paper.
This mission concerns the two tests the paper assigns to a known finite support: Pearson's test and the G test. Both compare the empirical frequencies of the observed support points with the probabilities under a proposed law. Their confidence regions give concrete uncertainty sets for discrete data. The paper's Theorem 4 states that both tests have the stronger convergence property it calls uniform consistency. That property is used in its general characterization of when robust sample average approximation converges for every admissible cost function (Theorem 2 and Table 1, pp. 13–14).
Fix a known set of possible observations, labelled . A probability law on this support is specified by probabilities , each nonnegative and summing to one. A sample of size consists of independent observations from an unknown true law . Its empirical frequency at label is
To assess a hypothetical law with probabilities , Pearson's statistic and the G statistic are, in the paper's normalization,
The confidence region for each test is the set of hypothetical laws whose statistic is at most , where is fixed across sample sizes. An observed point to which assigns zero probability makes either statistic infinite. A term with zero empirical frequency contributes zero to the G sum, including when its hypothetical probability is zero. These conventions make the regions describe the same tests at the boundary of the probability simplex as they do in its interior (§3.1, p. 8; §10.6, p. 38).
A sequence of laws is weakly convergent to when expectations of every bounded continuous function converge. On this finite support, weak convergence can be measured by the total variation distance
The paper's Definition 3 calls a test uniformly consistent when, for every true law , almost surely every sequence that fails to converge weakly to lies outside the confidence region infinitely often (Definition 3, p. 13). The almost sure event applies to all such sequences at once; this is stronger than a statement about one fixed false hypothesis.
For the Pearson and G confidence regions and with fixed , the target is
Here has the quantifier order of Definition 3: every generating , almost every infinite sample, and every nonconvergent sequence . This is Theorem 4, p. 14. Its four milestone claims are the finite support description of weak convergence, almost sure convergence of empirical frequencies, and the paper's total variation bounds for and (§10.6, p. 38).
The result says that distributions retained by either test cannot remain persistently separated from the data generating law as the sample grows. In the paper's framework, that is the statistical condition needed for its general theorem to turn test based confidence regions into convergent robust optimization values and decisions under its separate assumptions on the cost and feasible set (Theorem 2, p. 13). Theorem 4 itself concerns the tests; it does not assume a cost function or assert optimization convergence directly.
The paper proves Theorem 4, so the open work here is its Lean formalization. A complete development would also leave reusable statements for finite probability vectors, their empirical frequencies under an infinite product law, total variation, and the boundary aware Pearson and G divergences. These pieces can support other discrete goodness of fit and distributionally robust optimization results. The mission does not claim that Theorem 4 already has a machine checked proof.
Pointwise convergence of empirical frequencies does not by itself state uniform consistency. The latter quantifies over all moving hypothetical laws on one almost sure sample event, including laws chosen differently at every . A direct argument about one fixed therefore does not address the target. The finite support makes weak convergence concrete, but the formal statement must still relate that topology to a finite total variation sum and keep the quantifiers in the order required by Definition 3.
The boundary of the probability simplex is another source of difficulty. Lean's real division and logarithm have default values at zero. Using those defaults in the test statistics would accept some laws that assign zero probability to an actually observed category. Both statistics must instead retain the paper's infinite penalty there. The G expression also contains individual logarithmic terms that may be negative before summation, so its extended value cannot be built by coercing each term directly to a nonnegative extended real.
The known support is represented by Fin n. Its members are labels for the paper's distinct points ; coordinates in Euclidean space are irrelevant to these tests. Laws use Mathlib's ProbabilityMeasure (Fin n) and its weak topology. The data are coordinates of the canonical infinite product law, with Lean index zero corresponding to the paper's first observation. The empty support has no probability law; all substantive instances have . The empty sample is defined by total operations but has no bearing on an eventual or infinitely often assertion.
Pearson's statistic lives in . The squared G statistic uses extended real arithmetic so finite negative summands can be combined with an infinite boundary term. Its region compares with , equivalent to the paper's at positive . The free stands for a fixed threshold constant, including the paper's chi square quantile; no particular quantile value is built into the theorem. This makes explicit the only property of that threshold used in §10.6: independence from .
Contributions may prove the four milestone statements, connect Mathlib's finite probability and strong law interfaces to the empirical frequencies, or establish finite support versions of Cauchy–Schwarz and Pinsker with the correct infinite boundary cases. A proof of the goal must use the stated regions and preserve simultaneous quantification over every moving sequence of laws; replacing uniform consistency by convergence of would remove its main claim.
A McKean–Vlasov control problem asks a planner to steer a stochastic differential equation whose coefficients depend not only on the current path of the state but also on its (conditional) distribution. Such problems describe the cooperative optimum of a large population of interacting agents: when each agent reacts to the empirical distribution of all others and a social planner chooses everybody's control, the limit as the population grows is a McKean–Vlasov control problem (Lacker 2017). When all agents are also exposed to a common noise (a shared source of randomness, such as a market factor), the relevant distribution is the conditional law of the state given that noise.
Bellman's dynamic programming principle (DPP) is the standard route from a control problem to its Hamilton–Jacobi–Bellman equation and to verification arguments. For McKean–Vlasov dynamics it fails in the naive state variable, because the problem is time-inconsistent; it can be recovered by taking the (conditional) law of the state as the state.
Timeline. Laurière and Pironneau (2014) and Bensoussan, Frehse and Yam (2013–2017) proved a DPP for densities of the state law. Pham and Wei (2017, SICON) proved a DPP over closed-loop controls in a Markovian setting with a common-noise filtration, under regularity assumptions; Pham and Wei (2018, ESAIM:COCV) treated the case without common noise. Bayraktar, Cosso and Pham (2018, Trans. AMS) obtained a randomised DPP, again Markovian and without common noise. Djete, Possamaï and Tan (2022) proved the DPP for the general non-Markovian problem with common noise, under Borel measurability of the coefficients only. This mission formalizes their DPP for the weak formulation.
Fix a horizon , dimensions , a nonempty Polish space of control values, a point and an exponent . Let with the uniform norm, the Borel probability measures on with the weak topology, and the path stopped at time . The coefficients are maps , and ; all are Borel measurable, and depend on the path and the measure only through their restrictions to (non-anticipative).
A weak control with initial condition consists of a probability space carrying two filtrations (the second models the common noise), a state , Brownian motions (idiosyncratic) and (common) on , a predictable -valued control , and measure-valued processes and , such that , an integrability condition of order holds, a compatibility condition between the two filtrations holds, and
The reward and the value function are
with and . Each weak control also carries , where is a Borel isomorphism of onto a subset of , and the continuous conditional-law process of given .
is upper semi-analytic (every superlevel set is analytic), and for every stopping time of the canonical filtration of with values in , setting ,
The canonical reformulation on with weak control rules (Definition 4.1): Lemma 4.4(i) (weak controls and weak control rules correspond), Corollary 4.6 (), Lemma 4.7 (analytic graphs, u.s.a.), Lemma 4.8 (stability under conditioning at a stopping time), Lemma 4.9 (dependence on the initial law only through ), (4.10) (moment truncation , analytic and u.s.a.) and Lemma 4.10 (universally measurable -optimal families and concatenation).
The result. The theorem gives the DPP for McKean–Vlasov control with common noise in a non-Markovian setting, with no regularity on the coefficients beyond Borel measurability and no integrability on the rewards. It is the starting point for the dynamic programming (HJB) equation on the space of probability measures, for the Markovian corollaries of §3.2 of the paper, and, through the equivalence of formulations in the companion work, for the strong formulations treated in the second mission of this series.
Formalizing it. The result is proved on paper; nothing of it is machine-checked. A formal development needs a working theory of weak controls with conditional laws, a controlled martingale problem on a space of measure-valued paths, and analytic-set measurability in continuous time. None of these exists in Mathlib, and the analytic-selection layer on Prove2Me (Bertsekas–Shreve, Chapter 7) is stated but not yet proved.
The obvious argument conditions an optimal-ish control on its information at the stopping time and pastes in near-optimal controls from the conditioned states. Each step fails without additional structure: is not known to be measurable, so is not obviously meaningful; conditioning a weak control on its information at need not yield a weak control, because the conditional-law constraint involves the common-noise filtration and a compatibility condition between filtrations; and choosing a near-optimal control for each conditioned state is a selection problem over an uncountable family of probability spaces. The state of the problem is a law, which is itself defined only up to null sets, so random-time evaluations such as need a continuous version.
The Lean development lives in the namespace MKVDPP.Weak. Conventions:
Type (universe 0).EthierKurtz.HasBrownianItoIntegral) of integrands that are a.s. square integrable on , taken against the shifted Brownian motions , ; no condition, which would shrink .The goal does not mention the canonical space , weak control rules or any selection; a formalization of that is empty, or a value function that is constant, would trivialize it. A sanity file exhibits a weak control in the degenerate case for every , so the structure is satisfiable.
Infrastructure a complete development needs: conditional laws and r.c.p.d. on Polish spaces, the predictable -algebra, stochastic integrals against a filtration, the Stroock–Varadhan martingale problem, Itô's formula, and analytic sets with the Jankov–von Neumann selection theorem. The analytic-selection results and the martingale-problem/SDE correspondence are reusable well beyond this mission. Contributions on any milestone, and on proving the referenced Bertsekas–Shreve selection theorems, are welcome. Out of scope: Theorem 3.4 (it rests on the companion paper), the Markovian results of §3.2, and the HJB discussion of §3.3.
A controller may act on a large population of interacting particles while all particles also experience a shared random disturbance. In the population limit, the state of a representative particle depends on the distribution of states conditional on the common noise. The controller therefore influences both its own state and the conditional population law. The usual state variable for dynamic programming must carry that law, and a future decision may use only information available from common noise. Djete, Possamaï and Tan establish a dynamic programming principle for this setting in McKean–Vlasov optimal control: the dynamic programming principle, Theorem 3.2. Their result permits path dependent coefficients and merely Borel reward functions, so ordinary continuity arguments do not determine the value function's measurability.
The paper distinguishes a weak formulation, in which the stochastic basis varies with the control, from a strong formulation on a fixed space. This mission concerns the latter, restricted to controls predictable from common noise, under the paper's Lipschitz and growth Assumption 2.8. The companion mission treats the weak dynamic programming principle, Theorem 3.1. The present mission asks for a machine checked account of the strong formulation and of the transfer between its intrinsic, fixed space and canonical descriptions.
Fix a horizon . A state trajectory belongs to . The two driving noises are a dimensional idiosyncratic Brownian motion and an dimensional common Brownian motion . The control space is nonempty and Polish. At time , the controlled drift and diffusions may depend on the stopped state path , the control , and the conditional law of the stopped state and control given common noise. The running and terminal rewards are and .
A strong control has a continuous state satisfying the controlled stochastic equation, the conditional laws required by the paper, finite quadratic control energy, and an predictable for the common noise filtration. Its reward is the expected running reward from to plus the terminal reward. The value is the supremum of these rewards over such controls from initial path law . The initial law lies in , the laws with a finite second moment. The coefficient hypothesis uses the quadratic Wasserstein distance and one constant for both a Lipschitz bound and a quadratic growth bound. These conditions are Assumption 2.8 of the source paper, p. 8.
The paper also fixes a canonical probability space carrying an initial path and Brownian increments after . Its common noise predictable controls form . Proposition 2.10 says this fixed space computes the same value as the intrinsic strong formulation. The precise probability law on is characterized by the initial stopped path law and independent standard Brownian increments; the paper does not choose a unique construction.
The goal is Theorem 3.2, p. 10. It first asserts that the value on is upper semi analytic: each strict superlevel set is analytic. For an initial pair and a stopping time for the raw common noise filtration on , it then asserts
Here is the law of the stopped state conditional on information from common noise at . The milestone sequence follows the paper's supporting results: strong solution existence and uniqueness (Theorem A.3(i)); equivalence of intrinsic and fixed space values (Proposition 2.10); induction of canonical rules from strong controls (the forward clause of Lemma 4.4(ii)); the canonical value identity (Corollary 4.6); the Wiener represented rule class and its value (Lemma 4.11); analytic rule graphs and value measurability (Lemma 4.12); and stability of a strong rule under conditioning at a stopping time (Lemma 4.13(i)). Each is a source indexed target, rather than an invented intermediate assertion.
The identity permits the value after a random common noise stopping time to be evaluated from the stopped conditional state law. This is the form needed to compare control decisions before and after a random observation time. Upper semi analyticity supplies measurable superlevel sets for the value even when and lack continuity. The paper proves these statements mathematically; the mission seeks their Lean formalization, not a new theorem about the underlying control problem.
A complete formalization would also provide reusable definitions of conditional measure valued flows, Brownian motion relative to a filtration over a shifted interval, a local Itô equation, and canonical martingale control rules. The two published Ethier–Kurtz definitions supply the local Itô relation and probability augmentation of a filtration. They are shared infrastructure rather than new statements of this paper.
The state law in the coefficients is conditional on common noise and changes with the control. A pathwise solution of the state equation must therefore remain consistent with its own conditional law. A naive argument that restarts an ordinary diffusion at does not establish that consistency for a restarted control. It also does not ensure that a restarted control remains predictable from common noise. The paper's canonical rule formulation and its conditioning and measurability results address those obstructions. The reward may be unbounded and extended real valued, so the expectation convention and its behavior at infinite positive and negative parts matter to the statement itself.
Paths are continuous maps on compact real intervals with uniform norm; is Mathlib's Euclidean space, including . Probability measures carry weak convergence topology, and is its finite second moment subtype. The product of path space and uses Mathlib's product metric; matrix norms are Frobenius. Supremums range over admissible controls, solutions and conditional law versions. They are EReal valued, so the empty supremum is . The signed expectation is positive part minus negative part with , as in the paper. The model fixes a Borel embedding of into and a cemetery control for invalid reconstructed paths.
The Lean statements pin the paper's implicit “well defined” stochastic integral to a pathwise square integrable local Itô relation and almost surely integrable drift. A conditional law equality stated for almost every pair is expressed in Fubini form. The localized processes printed in Definition 4.1 define its local martingale requirement. The terminal law and the stopped law in the target are quantified as versions of their stated conditional distributions. The fixed canonical law is any law satisfying the paper's initial distribution and Brownian conditions; the target is stated for every such family. These conventions rule out free conditional laws, arbitrary future stopping times, and a value that is solely because a formalization made the control class empty. A full development must establish nonemptiness and version independence as part of the cited supporting theory.
The scope ends with Theorem 3.2 and the listed milestones. Lemma 4.13(ii), the more involved measurable selection and concatenation result, remains a future contribution. Theorem 3.4 uses a separate companion result; the Markovian corollaries and the heuristic Hamilton–Jacobi discussion of §3.3 are outside this mission.
Systems of two first-order hyperbolic equations with opposite transport speeds model open-channel flow (the Saint-Venant equations), gas pipelines, heat exchangers and traffic. In such systems one boundary is actuated, the other boundary reflects, and the coupling terms move energy between the two families of waves. Boundary feedback design for them is a standard problem of distributed-parameter control.
The backstepping method designs a feedback by means of an invertible Volterra integral transformation that turns the plant into a target system whose behaviour is known in closed form. Coron, Vazquez, Krstic and Bastin (arXiv:1208.6475; SIAM J. Control Optim. 51(3), 2013) carry out this design for a general linear hyperbolic system with spatially varying speeds and couplings, in §3 of their paper. The resulting linear feedback is the controller they later apply to a quasilinear system. This mission formalizes the linear result.
Timeline:
Let be functions on with , let be continuous, and let . The state solves
so travels to the right and to the left. The boundary conditions are and , where is the control. The norm is .
The kernels are functions on the triangle that solve
with and . The control law (3.48) is
The target system is with and , for . The direct transformation is (3.23), with the full kernel of (3.30)–(3.37). The inverse transformation is (3.38), with solving (3.40)–(3.47). The finite time is
For , every classical solution of the closed loop satisfies
Here depends on and the data but not on the solution.
The theorem shows that a single linear boundary feedback, computed once from the coefficients, drives every state of the system to zero in exactly the time . That time is the sum of the travel times of the two characteristic families across . Exponential stability at every rate follows. The same feedback, rescaled, is the controller of the paper's main result, Theorem 4.1: local exponential stabilization of a quasilinear system, the subject of mission 3 of this series. The well-posedness of the kernel equations, Theorem A.1, is mission 1.
The result is proved in the paper. As far as is known, none of it has been machine-checked. A formal proof needs Volterra transformations of vector-valued functions with differentiation under a variable-limit integral, explicit solutions of transport equations along characteristics, and estimates for integral operators with continuous kernels. These tools apply to backstepping designs well beyond this paper.
Proposition 3.1 and the two mapping statements are calculations: an integration by parts and the explicit solution along characteristics. The difficulty of Theorem 3.2 is the step "the transformation is invertible", which the paper's proof takes for granted. The goal hypothesizes only , so it is not enough to state the mapping and the inverse separately. The solver has to recover the full state from the target state: either build the remaining kernels and the inverse kernel , or argue directly from the closed subsystem. Both routes need existence or uniqueness for Goursat-type problems, which the paper proves only in Appendix A. A second, routine obstacle is that the uniform constant must be extracted from the finite-time interval using bounds on the kernels.
w : ℝ → ℝ → Fin 2 → ℝ, space first, with Lean index 0 for the paper's first component.Three trivializing readings are excluded. The constant is quantified after the data and before the solution, so it cannot depend on the solution. The finite-time claim is vanishing for every , with exactly (3.8), not for some unspecified time. The kernels are pinned down by all four of (3.32), (3.33), (3.36), (3.37). With coefficients a solution exists (the paper's Theorem A.2), and a sanity file checks that the hypotheses admit a non-zero closed-loop solution.
Welcome contributions: lemmas on differentiating , transport equations along characteristics, and the invertibility of Volterra operators with continuous kernels.
The paper's proofs are on pp. 3–5 (Proposition 3.1), p. 5 (§3.2), p. 6 (§3.3) and p. 7 (Theorem 3.2).
A queue layout represents a graph by placing its vertices in a line and assigning edges to queues. The order and assignment must prevent nested edges from sharing a queue. This gives a graph parameter that measures how much queue capacity is needed for a particular graph. Heath, Leighton, and Rosenberg asked whether one fixed number of queues suffices for every planar graph. The question remained open while bounds depending on the graph's number of vertices, degree, or treewidth were known. Dujmović, Joret, Micek, Morin, Ueckerdt, and Wood resolved it by proving a uniform bound of 49. Their paper also develops layered partitions, a structural tool used beyond queue layouts. These claims and the historical account appear in the source paper, pp. 3–5 and 16.
A finite simple graph has vertices and unordered edges . Choose a linear order of . Two disjoint edges nest when their endpoints appear as , with one edge joining to and the other joining to . A queue is a set of edges with no nested pair. A -queue layout is a vertex order together with an assignment of every edge to one of queues; means such a layout exists. Edges sharing an endpoint cannot nest. Empty queues are allowed, so an edgeless graph can use zero queues. These are the paper's definitions in §1, pp. 3–4.
A layering assigns vertices to layers such that endpoints of an edge lie in the same or adjacent layers. A BFS layering starts from one selected root in each connected component and places each vertex in the layer equal to its graph distance from that root. A vertex partition divides into disjoint nonempty parts. Its quotient graph has those parts as vertices; distinct parts are adjacent if an edge of joins them. An -partition may index the parts by vertices of another graph : the quotient's edges must be represented by edges of , while an indexed part may be empty. A partition has layered width at most with respect to a fixed layering if every part contains at most vertices of every layer. The exact definitions are in §2, pp. 7–9.
A graph is planar when it can be drawn in the plane with vertices at distinct points and edges as simple arcs that meet only at shared endpoints. A tree decomposition covers every vertex and edge of a graph by bags indexed by a tree, with the bags containing each vertex forming a connected subtree. Treewidth at most three means that a tree decomposition exists with every bag of size at most four. The paper uses these standard notions in §2 and §4, pp. 7, 12, and 16.
The goal is the explicit upper bound the paper derives for its Theorem 1:
The printed theorem says that planar queue-number is bounded, and the authors state 49 immediately after it. A bound that depends on would not express the result. The goal uses the paper's own constant, as given in Theorem 1 and the following sentence, p. 5.
The structural target is Theorem 15, p. 16: for every BFS layering of a planar graph, there is a partition of layered width at most three whose quotient remains planar and has treewidth at most three. The queue transfer target is Lemma 8, p. 10:
when has an -partition of layered width . Its layout orders vertices layer by layer. The milestone list also includes the rainbow characterization, the blowup lemma, the complete-graph queue number, and the five-queue bound for planar graphs of treewidth at most three. These are the stated supporting results along the route to 49 in §2–§4.1, pp. 7 and 10–16.
The goal establishes a constant queue bound for all planar graphs, independent of their size, degree, and treewidth. Theorem 15 supplies a reusable structural statement: even if the original graph has large treewidth, its quotient by small layer intersections has treewidth at most three while remaining planar. The paper goes on to treat graphs of bounded Euler genus and proper minor-closed classes, and describes connections with graph products and other graph parameters in its abstract and introduction, pp. 1 and 5.
The result is proved in the cited paper. This mission records Lean statements of the goal and six supporting milestones; their proofs remain to be formalized. A completed development would connect finite graph orders, nested-edge combinatorics, layered partitions, planar drawings, and tree decompositions in one machine-checked chain. The queue and partition definitions can also support later work on graph classes beyond the planar case.
A vertex order chosen without regard to a graph's structure can contain large rainbows, forcing many queues in that order. Planarity alone does not specify an order or an edge assignment, and a direct bound from ordinary treewidth does not cover planar graphs with arbitrarily large treewidth. The central structural requirement is to find a partition whose parts remain small in each BFS layer while its quotient has low treewidth. The queue transfer lemma must retain a layer-by-layer vertex order and account for edges within parts and between parts. The paper, pp. 10–11 and 16, identifies these as distinct constraints in its stated results.
Vertices form a finite type and edges are those of a Mathlib simple graph. A vertex order is an injective map into ; strict inequalities on four endpoints encode nesting. Queue assignments are functions on the graph's edge set, so the empty graph's zero-queue case is present. The statements use an existence predicate for , without taking a numerical infimum. Layerings are functions to , with BFS roots chosen separately for disconnected components. Theorem 15 uses a partition into nonempty parts, and the quotient has exactly those parts as vertices. Treewidth at most three uses a published tree-decomposition definition with bags of size at most four.
The locally checked drawing definition has the same fields as the published plane-drawing definition; the published module was unavailable from the local index in this run. Planarity means existence of a crossing-free drawing, not a drawing that permits crossings. The formulation does not use a universal edge carrier that would rule out zero queues, a non-strict nesting test, or a default numerical treewidth. The near-triangulation, Sperner, and tripod statements from the paper's deeper proof are outside this proposal's milestone scope; the partition theorem remains a full milestone. Solvers may contribute the omitted geometric and tree-decomposition infrastructure when proving it.
The characteristic polynomial of an ordinary graph records spectral information in coefficients that can also be described by finite graph configurations. The classical Harary–Sachs theorem is an instance of this connection. For a uniform hypergraph, the adjacency object is a tensor rather than a matrix, and its characteristic polynomial is defined through a multivariate resultant. Clark and Cooper's hypergraph theorem gives a corresponding coefficient formula. It identifies the configurations that replace the elementary subgraphs of the graph case and assigns them weights determined by directed Eulerian structures. The result makes a tensor spectral invariant accessible through finite combinatorial objects.
The article appeared as Gregory J. Clark and Joshua N. Cooper, A Harary-Sachs theorem for hypergraphs, Journal of Combinatorial Theory, Series B (2021), DOI 10.1016/j.jctb.2021.01.002. This mission follows the pinned arXiv version 2, whose page and theorem numbers are used below.
A simple -graph has a fixed vertex set of labeled vertices and a set of distinct edges, each containing exactly vertices. Isolated vertices remain part of . The normalized adjacency hypermatrix gives an ordered -tuple the value when its underlying set is an edge, and zero otherwise. This normalization makes every ordering of the other vertices contribute the intended total weight.
The characteristic polynomial is the multivariate resultant of the coordinates of . The resultant is characterized by three conditions: it vanishes exactly when homogeneous coordinate polynomials have a nonzero common complex root, it evaluates to one on the coordinate monomials, and it is irreducible over the complex coefficient field. Its degree in is . The codegree- coefficient is the coefficient of ; this degree is fixed from the source theorem and is not read from an implementation of .
A multi-hypergraph is a multiset of -element edges. It is Veblen when the degree of every vertex is divisible by . Its flattening discards repeated edges, so is an infragraph of when every edge of its flattening belongs to . Components use only vertices covered by edges; a labeled object may still sit in a larger ambient vertex set with unused vertices.
A rooting of is a sequence of its edges, each assigned a root vertex in that edge, with roots in nondecreasing order. An edge rooted at contributes a directed arc to every other vertex of the edge. Summing these arcs with multiplicity produces a directed multigraph . An Euler rooting has balanced in- and out-degrees and connected positive-degree vertices. Its arborescence number counts spanning trees of these active vertices directed toward a specified root, with parallel arcs distinguished. For connected , its associated coefficient is
For disconnected , is the product of the coefficients of its connected components. These conventions follow Definitions 6–10 in the source.
The supporting targets identify when a monomial differential operator contributes to a matrix trace, and show that an Euler rooting determines a connected Veblen multi-hypergraph. The operator identity is counted by Euler tours with distinguishable parallel arcs. The resultant-to-trace identity quoted in the paper is also a milestone:
Here is the paper's sum over positive compositions of , and is its differential trace from Equation (1).
The goal uses the labeled form of Theorem 14. Let be the set of ordered -tuples of connected labeled Veblen infragraphs whose edge counts sum to . Then
The paper prints the equivalent sum over isomorphism classes, using automorphism groups and the copy weight . The labeled expression is the result before that grouping. The isomorphism-class statement is outside this mission's Lean target and remains a separate formalization task.
The theorem expresses a coefficient of a resultant, defined algebraically over complex common roots, as a finite rational weighted sum over hypergraph configurations. It extends the graph case while preserving the exact normalization, sign, component count, and coefficient index. The formula can be used to study low codegree coefficients by enumerating finite Veblen infragraphs and their Euler rootings. Clark and Cooper also use associated coefficients to compare different hypergraph structures in the paper.
The formal development separates the resultant, the differential trace, and the combinatorial counts into reusable definitions. It would provide machine-checked statements of the paper's main equality and several links between those definitions. The Lean theorems in this draft are open targets with sorry placeholders; compiling their statements does not constitute a machine-checked proof of the paper's claims.
The ordinary matrix determinant has a direct expansion by permutations. A tensor characteristic polynomial is a multivariate resultant, so that expansion does not directly reveal which hypergraphs contribute to a coefficient. The trace side uses repeated partial derivatives, and repeated hyperedges can create several distinct rootings with the same directed arc multiplicities. Counting only a multiset of root assignments loses those orderings and changes the coefficient. The Eulerian condition, arborescence multiplicities, and factorial factors must agree simultaneously for the algebraic and combinatorial expressions to match.
The Lean representation uses Fin n vertices, finite sets of simple edges, multisets of repeated edges, rational adjacency weights, and complex polynomials only for the resultant criterion. It assumes , , and . The source fixes , and the latter two bounds expose the domain in which the printed coefficient expansion and its proof use . An isolated vertex of counts in and in , while isolated vertices do not pad a multi-hypergraph component.
The formalization takes a polynomial satisfying the resultant's common-root, normalization, and irreducibility properties as an input. Separate sanity proofs give witnesses in the one-variable degree-zero and degree-one cases; degree one covers the first goal-domain degree when . The characteristic polynomial is evaluated from this polynomial, never defined by the trace identity. Rootings are sequences, arborescences are directed toward the least positive-degree vertex, and the associated coefficient is calculated on covered vertices. The goal uses the labeled sum, so no automorphism is computed on an ambient padded vertex set. Contributions formalizing the omitted isomorphism-class equivalence, the BEST circuit count, and proofs of the stated targets are welcome.
A graph may have enough symmetry for every edge to look the same while its vertices still fall into two distinct classes. Such a graph is semisymmetric when it has constant valency, is edge-transitive, and is not vertex-transitive. Conder, Zhou, Feng and Zhang study this phenomenon among bi-Cayley graphs, graphs equipped with a group acting freely on two vertex orbits. Their dihedral case supplies examples related to questions of Marušič and Potočnik about semisymmetric tetracirculants. It also asks how small the valency of a semisymmetric graph with this specific group action can be. The paper states that six is the minimum and that examples occur at every valency with odd (Conder et al., Theorem 1.5 and its introduction, p. 3).
The authors develop the bi-Cayley setting and the relevant automorphism actions before reaching the dihedral result. The lower bound appears as Theorem 6.1, while Example 6.2 defines a graph family and Proposition 6.4 gives a semisymmetry criterion for its odd- members (Conder et al., pp. 11–13). This mission targets those claims within a single formal graph model. The final sentence of Theorem 1.5, concerning an edge-regular family, depends on the separate Theorem 6.5 and is outside this goal.
Let be a finite group. Choose subsets with , , , and . The graph has two labelled copies of each element of , written and . For each , it joins to when , joins to when , and joins to when . These are unoriented edges. Right multiplication by preserves the graph and acts regularly on each of its two vertex copies (Conder et al., pp. 1 and 4).
A bi-dihedrant is a bi-Cayley graph whose group is dihedral. Write for the dihedral group of degree . Graph valency is the number of neighbours of a vertex. Connectedness is required throughout the paper. For a semisymmetric graph the common valency exists by definition, but the formal statements quantify over every vertex so that the numerical claims refer to the actual graph degree (Conder et al., definitions on p. 4 and Theorem 6.1 on p. 11).
The constructed family uses , , and a residue of multiplicative order modulo whose even-power sum vanishes: . For , put and . Set . Then (Conder et al., Example 6.2, pp. 12–13).
Right multiplication gives a subgroup , and is its normaliser. For and the paper's permutations are and ; the sets and of (2.2) collect those that preserve the edge rules. A graph is normal edge-transitive when , not merely , is transitive on edges (Conder et al., pp. 4–5).
The milestones, in attack order, are Proposition 2.1(b) (one may assume ), Proposition 2.2 (the normaliser ), the opening step of the proof of Theorem 6.1 ( for a semisymmetric graph), Theorem 6.1, the claims of Example 6.2, and Proposition 6.4.
For every connected semisymmetric bi-dihedrant over , , and every vertex ,
This is Theorem 6.1 and the first claim of Theorem 1.5. The milestone for the proof's opening step records that semisymmetry forces ; the theorem itself still ranges over all valid (Conder et al., Theorem 6.1, p. 11).
For each odd integer , there is a connected semisymmetric bi-dihedrant such that
Example 6.2 is the first milestone toward this claim: under its hypotheses is connected, , every vertex has degree , and for lies in and permutes the neighbours of cyclically, so the graph is normal edge-transitive (Conder et al., p. 13). Proposition 6.4 is the second: under the defining conditions for , odd and modulo imply semisymmetry (Conder et al., Proposition 6.4, p. 13). An auxiliary arithmetic theorem states the parameter existence needed to apply it for every odd .
The lower bound excludes semisymmetric bi-dihedrants of valency at most five. The existence assertion says that six is attained and places examples at an infinite sequence of larger valencies. Together these claims distinguish the restrictions imposed by a dihedral bi-Cayley action from edge transitivity alone. The construction also gives a concrete family on which questions about stronger automorphism properties can be posed (Conder et al., §6, pp. 11–14).
The result is proved in the cited paper; this mission seeks a machine-checked version of its first two Theorem 1.5 claims. The definition of a bi-Cayley graph, the precise graph symmetry predicates, and the arithmetic parameter family are reusable beyond this particular lower bound. The statements here are open proof targets in Lean, with their mathematical content fixed before proof development. The edge-regular claim from the theorem's final sentence requires additional source results and remains a separate formalization target.
Edge transitivity alone does not make a graph vertex-transitive: a semisymmetric graph is precisely the regular case where that inference fails. The lower bound therefore cannot be obtained by treating every vertex as lying in one automorphism orbit. In the dihedral case, the proof must account for both the rotations and reflections in the connection set, and for the constraints that connectedness and graph automorphisms impose on low-valency possibilities (Conder et al., proof of Theorem 6.1, pp. 11–12).
The existence statement has a distinct arithmetic requirement. Proposition 6.4 is conditional on satisfying Example 6.2 and . The paper asserts examples for every odd without spelling out parameters for all such . The auxiliary arithmetic statement records that remaining obligation explicitly; a proof of the conditional proposition alone would not establish the quantified existence claim.
Lean represents the two vertex copies by H ⊕ H and the dihedral group by Mathlib's DihedralGroup n. The graph is a SimpleGraph built from the three edge rules above, with the inverse-closure and loop-exclusion conditions retained in BiCayData. Semisymmetry uses the full graph automorphism group, unoriented edge transitivity, and constant graph degree. The source's standing finite, connected, simple, and undirected conventions are explicit through finite groups, simple graphs, and connectedness hypotheses. The goal and Theorem 6.1 use , the range of dihedral groups in §6; the existence examples are also required to be connected.
The definitions do not set valency equal to , replace a graph degree by a formula, or make an edge-transitivity claim true by ranging over an empty edge set. The setting requires valid inverse-closed side sets rather than silently symmetrising an invalid one. The arithmetic hypothesis uses the multiplicative order in and enumerates the indices of by . Normal edge-transitivity in Example 6.2 is stated for the subgroup and semisymmetry for the full group ; the two are not interchanged. The restriction in the lower bound is that of Theorem 6.1 and is a disclosed hypothesis of the goal: and are abelian, and the paper treats bi-Cayley graphs over abelian groups separately. The auxiliary parameter statement is not in the paper; it is supplied so that the existence claim has a complete proof path. The third sentence of Theorem 1.5 is not formalized. Contributions establishing the structural lower bound, the family criterion, or the arithmetic existence statement are all within scope.
A graph is symmetric when its automorphism group moves any vertex, edge or arc to any other, and -arc-transitive when it moves any walk of length without immediate backtracking to any other. Tutte's work on cubic graphs made -arc-transitivity a central measure of symmetry in algebraic graph theory, and most constructions of highly symmetric graphs start from a group acting regularly on vertices (Cayley graphs) or semiregularly with a few orbits.
Bi-Cayley graphs are the case of two orbits: a group acts semiregularly by right multiplication with exactly two vertex orbits. The Petersen graph, the Gray graph (the smallest cubic semisymmetric graph) and the smallest member of Bouwer's family of half-arc-transitive graphs are all bi-Cayley graphs, and all of them are edge-transitive. Deciding edge-transitivity of a bi-Cayley graph is hard in general, but the subgroup of automorphisms that normalise the semiregular group is explicitly known, which makes the "normal" version of the question tractable.
C. H. Li asked whether 3-arc-transitive bi-normal Cayley graphs exist and asked for a description of the 2-arc-transitive ones (Li, Proc. Amer. Math. Soc. 133, Question 1.2(a) and Problem 1.3(b), as cited in the paper, p. 2). M. Conder, J.-X. Zhou, Y.-Q. Feng and M.-M. Zhang answered both through their Theorem 1.1 (arXiv:1606.04625v1; J. Combin. Theory Ser. B, 2020). This mission formalizes that theorem and the lemmas its proof uses.
Let be a finite group with identity . Let with , and . The bi-Cayley graph has vertex set , two disjoint copies of (the copy of in is ), and edges , and for , , , . The main theorem concerns , where is bipartite with parts , and every vertex has neighbours.
For , is an automorphism of ; these form the subgroup , and
is its normaliser. For (written as an exponent, ) and the paper defines the permutations
and the sets of those with , , , and of those with , , .
An -arc is a sequence of vertices in which consecutive vertices are adjacent and . A subgroup is transitive on -arcs if any -arc can be mapped to any other by an element of ; 1-arcs are arcs. is normal edge-transitive if is transitive on edges, and normal locally arc-transitive if the stabiliser is transitive on the neighbourhood . acts semisymmetrically if it is edge-transitive but not vertex-transitive. is the setwise stabiliser of in .
Let be connected, with and . Then
where (a) for some ; (b) is transitive on ; (c) for some and . Furthermore, if , is not transitive on the 3-arcs of .
A companion item, Lemma 3.1, shows that a connected normal edge-transitive has ; it explains why the goal is stated for .
Combined with Lemma 3.1, Theorem 1.1 reduces 2-arc-transitivity of the normaliser of to three conditions on and the single set , all checkable in the group without building the graph. Its second part rules out normal 3-arc-transitive bi-Cayley graphs of valency at least 3, which settles Li's question on 3-arc-transitive bi-normal Cayley graphs negatively. Proposition 3.3 is the arc-transitive versus semisymmetric dichotomy for normal locally arc-transitive bi-Cayley graphs, the starting point of the paper's later constructions of semisymmetric and half-arc-transitive examples.
All results are proved in the paper (Proposition 2.2 by citation). None of them has a machine-checked proof that this mission knows of. Mathlib has simple graphs, graph isomorphisms and normalisers, but no bi-Cayley graphs, no -arcs and no transitivity notions for subgroups of . A formal proof would supply the first verified description of the normaliser of a semiregular group with two orbits, reusable for any bi-Cayley or bi-circulant result.
The bulk of the work is Proposition 2.2. That and preserve edges exactly under the conditions of (2.2) is a direct computation. The converse is harder: every automorphism normalising must be one of these permutations composed with some . That needs the conjugation action of on to induce an automorphism of , and to preserve the partition into -orbits.
The 3-arc clause looks like a stabiliser count, but it holds only once has at least two neighbours besides : for the graph is a cycle of length , the normaliser is the whole dihedral automorphism group, and that group is transitive on 3-arcs. Any proof must use at exactly this step.
The vertex set is H ⊕ H (Sum.inl h , Sum.inr h ). The data is a structure of three Finsets carrying the side conditions , , , and . Adjacency is given directly by the three edge rules. is the group Γ ≃g Γ, is the subgroup generated by the , and is its Subgroup.normalizer. Automorphisms of are MulAut H, and is the image of under . and are permutations of H ⊕ H, and "" means that some element of has as its vertex map. Products are written pointwise to avoid the composition-order convention of the group of graph automorphisms. An -arc is a function on Fin (s+1).
The paper assumes throughout that groups and graphs are finite and graphs connected; each theorem carries Fintype H and connectivity. Three hypotheses are added to the printed Theorem 1.1, each needed for the statement to be true or non-vacuous: (the paper's normalisation of a bi-Cayley triple, used by conditions (b) and (c) and by the proof); (for the graph is , which has no 2-arcs, so 2-arc-transitivity would hold vacuously while (c) fails); and for the 3-arc clause (false for cycles). Lemma 3.2 carries the same and , and Proposition 3.3 carries .
Trivializing formalizations are ruled out in four ways. 2-arc-transitivity is never vacuous, since guarantees 2-arcs. and are never symmetrised silently, since the side conditions are data rather than repairs. Every transitivity statement is about , not the full . Valency is the degree in the graph, never a formula in .
Contributions are welcome at every level: proofs of the milestones, a general library of bi-Cayley graphs and their normalisers, and lemmas on -arcs and stabilisers in SimpleGraph. The definitions are repeated identically in the companion missions on bi-abelian graphs and bi-dihedrants.
A Cayley graph turns multiplication in a group into adjacency between vertices. Every Cayley graph is vertex transitive: multiplying every vertex by the same group element moves any chosen vertex to any other. A bi-Cayley graph starts with two copies of a group and permits edges both within and between the copies. Its built-in group action is transitive on each copy, but it need not exchange them. This makes bi-Cayley graphs a setting for distinguishing edge, vertex, and arc transitivity. Conder, Zhou, Feng and Zhang study these distinctions and their consequences for graph constructions in Edge-transitive bi-Cayley graphs.
For abelian groups, the paper proves a strong restriction: once a connected bi-Cayley graph is edge transitive, it is also vertex transitive. Its half-arc-transitive examples face additional local restrictions, including a minimum valency of six. The paper exhibits a graph of valency six in Example 4.3, so the numerical bound is attained in its class. The result separates these graphs from semisymmetric graphs, which are edge transitive but not vertex transitive. The claims and example appear in Proposition 1.3 and §4.
Let be a finite group and let be subsets of . Require , , , and . The graph has vertices , two labelled copies of . For , an element gives an edge from to ; an element gives an edge from to ; and an element gives an edge from to . The inverse closure of and makes the within-copy edges undirected. Excluding from those two sets excludes loops. This is the construction on p. 1.
Every acts by right multiplication . The subgroup of graph automorphisms has two vertex orbits, and . Its normaliser in is useful for describing further symmetries. For a group automorphism and group elements , the paper defines permutations , which preserve the two copies, and , which exchange them. Their precise edge-preservation conditions are the sets and of equation (2.2). The mission includes those definitions and the relevant part of the normaliser characterization, Proposition 2.2.
A graph is vertex transitive if its full automorphism group can move any vertex to any other, and edge transitive if it can move any undirected edge to any other. Arc transitivity asks the same for ordered adjacent pairs. A graph is half-arc-transitive when it is vertex and edge transitive but not arc transitive. A semisymmetric graph has constant valency, is edge transitive, and is not vertex transitive. These are the paper's definitions on p. 4. Valency means the actual number of neighbours of a vertex.
The central target is the corrected reading of Proposition 1.3: for connected over an abelian ,
and, if is half-arc-transitive,
The attack path records the normaliser characterization in Proposition 2.2, both parts of Proposition 4.1, its explicit bipartition step, and Proposition 4.2. The companion Corollary 4.4 expresses the absence of connected semisymmetric examples over abelian groups.
The vertex-transitivity conclusion collapses one apparent possibility in the symmetry classification: an edge-transitive bi-Cayley graph over an abelian group cannot be semisymmetric. For half-arc-transitive graphs, the theorem rules out involutions in the within-copy connection sets, forces even set sizes, and excludes valencies below six. Example 4.3 supplies an attained bound, with and valency six. These are concrete restrictions on any later classification or construction in this family; they follow from §4.
The mathematical results are proved in the cited paper. The mission asks for machine-checked Lean proofs of their statements and for a reusable finite bi-Cayley graph interface. The setting includes the right regular action, its normaliser, the two families of candidate automorphisms, and the transitivity predicates. The proof obligations are open in this local proposal; a successful development would make the abelian argument and its underlying graph-action lemmas available for later formalizations of bi-Cayley graphs.
The right multiplication action gives only two known vertex orbits, one for each copy of . Edge transitivity alone does not name an automorphism that swaps them. Inversion is an automorphism of an abelian group, but its induced copy-swapping permutation preserves graph edges directly only in the relevant bipartite case . The paper must account for edge-transitive graphs whose connection sets initially allow edges inside the copies. For the valency bound, the absence of arc transitivity restricts how a vertex stabiliser can permute its neighbours; degree counting without those orbit constraints cannot yield . These are the points at which a proof must use the full automorphism action rather than just the visible right regular subgroup.
Lean uses the vertex type , with Sum.inl h for and Sum.inr h for . The group and graph are finite; the graph is simple and undirected by construction, and every theorem assumes it is connected. The finite sets retain the conditions , , , and . The graph's degree, rather than a separately defined cardinality formula, represents valency. “Involution” means an element of order exactly two. All graph-level transitivity predicates quantify over the full automorphism group; the normaliser appears only in the separate Proposition 2.2 milestone. The paper's exponent notation for group automorphisms is rendered as function application, while remains right multiplication.
The printed first sentence of Proposition 1.3 says every connected bi-Cayley graph over an abelian group is vertex transitive. That sentence is false: the connected generalized Petersen graph is a bi-Cayley graph over and is not vertex transitive. Proposition 4.1(b), which the paper uses to establish Proposition 1.3, includes the missing edge-transitivity condition. The Lean goal states that corrected condition explicitly. It does not add an assumption to the half-arc-transitive clause, since half-arc-transitivity already entails edge transitivity. Proposition 4.2 prints two clauses labelled “(a)”; they are treated as distinct clauses while its quotation retains the printed labels.
The definition of the graph keeps and inverse closed as data; no graph constructor silently symmetrises arbitrary sets. Transitivity is taken over actual edges or arcs, and the degree bound is checked at every vertex. Contributions to the graph-action lemmas, the normaliser result, Proposition 4.1, and the vertex-stabiliser analysis behind Proposition 4.2 are all within scope. The Cayley-graph isomorphism in Proposition 2.2(b) is outside this mission's stated milestone because it is not used by the target.
Ride-hailing, freelancing and delivery platforms are intermediaries that post a price to buyers and a price to sellers and then match the two sides. Both sides are forward-looking: an agent who arrives can wait before requesting, and an agent who requests waits until she is matched, at a cost per unit of time. Chen and Hu, Pricing and Matching with Forward-Looking Buyers and Sellers (SSRN 2859864; Manufacturing & Service Operations Management 22(4), 2020, doi:10.1287/msom.2018.0769), measure simple pricing and matching policies against an upper bound that holds for every policy. This mission formalizes that upper bound in its mechanism-design form: no incentive-compatible two-sided dynamic mechanism earns more than the expected value of a clairvoyant assignment problem in virtual values.
The bound extends the virtual-value approach of Myerson (1981) and its bilateral-trade version by Myerson and Satterthwaite (1983) from a single static trade to a market with random arrivals on both sides, waiting costs and a timing constraint that matched units change hands at the same instant.
Over a horizon , buyers arrive as a Poisson process of rate . A buyer has type : arrival time and valuation , drawn with continuous positive density and c.d.f. , independently of the arrival time. Sellers arrive as an independent Poisson process of rate , with types and costs of continuous positive density and c.d.f. . The paper assumes and that the virtual value and the virtual cost are increasing (Assumptions 1–2). Write for the realized arrivals.
A direct mechanism assigns to every buyer an outcome : the time at which she leaves, the indicator that she receives a unit, and her payment . Every seller receives likewise, now paid to her. The balancing condition requires that at every the number of buyers who receive a unit at equals the number of sellers who deliver one at . The buyer's utility is and the seller's is , with waiting costs . The intermediary's profit is
Incentive compatibility (ICd) asks that no buyer gain, in the interim expectation over all other agents, by reporting another valuation or a later arrival time ; individual rationality (IRd) asks that her interim utility be nonnegative. (ICs) and (IRs) are the seller counterparts. Problem (B′) maximizes over feasible mechanisms subject to these constraints; its value is .
The comparison object is the clairvoyant assignment problem (B): knowing in advance, choose a partial matching of buyers to sellers maximizing
its optimal value is .
For every feasible, well-defined mechanism satisfying (ICd), (IRd), (ICs) and (IRs),
with integrable. This is the last display of the proof of Lemma 1 (Online Appendix p. 4), .
Lemma S.3 (Supplemental Note p. 3), the seller envelope bound with information rent , is posed as a further theorem of the mission, the mirror image of Lemma S.1; it is not listed as a milestone.
Here (ICd′) and (ICs′) are the one-dimensional constraints in which the reported arrival time is the true one; Lemmas S.1–S.4 are stated under these weaker hypotheses, as in the paper.
Lemma 1 of the paper, for every pricing policy and matching policy , is the benchmark against which the paper's main theorem measures its waiting-adjusted fixed-price policy, and is in turn bounded by a deterministic fluid value (Lemma 2). Lemma 1 is the composition of two facts: the revelation principle (Lemma 3) and the mechanism-design bound posed here. The second carries the analytic content: it is where the envelope theorem, the exchange of integrals that turns payments into virtual values, and the timing argument appear.
The result is proved in the paper; its proofs are in the Online Appendix (Section A.2) and the Supplemental Note (Section A). No machine-checked proof of it, or of a dynamic two-sided Myerson bound of this kind, is known. A formal proof would also yield a reusable two-sided, Poisson-arrival version of the interim envelope and revenue-equivalence identities.
Each agent's type is two-dimensional, an arrival time and a valuation or cost, and arrival can only be misreported later. The relaxation to (ICd′)/(ICs′) makes the screening problem one-dimensional, but the interim expectation ranges over a random population whose size is itself random. Turning into an integral of interim payments requires the Mecke formula for the Poisson process, and the envelope argument must be carried out for interim utilities that are only known to be suprema of affine functions, using no differentiability of the mechanism. The pathwise step is combinatorial: the balancing condition at each instant pairs buyers with sellers discharged together, and those pairs must be compared with an optimal matching of (B), with duplicate types and unmatched agents handled.
A frequent first idea, bounding payments by valuations directly, gives only the first-best surplus , which is not the target; the information rents must be extracted.
The primitives are the published bilateral-trade environment MechanismDesign.BilateralTrade.Environment (densities on intervals, cdfB, cdfS, psiB , psiS , Regular Assumptions 1–2), and (B) is AssignmentGame.CoreLP.worth of the published assignment game, with sellers as rows and buyers as columns. The conventions committed to are:
WellDefined: outcomes are Borel in the listed types, interim payments are integrable, and total absolute payments are integrable. Integrability of and of the virtual-surplus sums is part of each conclusion.A trivializing formalization is ruled out: the mechanism class is not restricted beyond the paper's feasibility, the constraints are not vacuous (the null mechanism satisfies them, so ), and expectations are of integrable functions. The goal quantifies over mechanisms rather than taking a supremum, which is equivalent because the class is nonempty.
A complete development needs the Mecke formula for the Poisson-count representation, an envelope theorem for suprema of affine functions on an interval, Fubini on the type space, and an exchange argument for matchings. All of these are reusable beyond this mission. Contributions of any of them, of the milestones in any order, or of alternative proofs are welcome.
The associahedron is the -dimensional simple polytope whose faces correspond to the sets of pairwise non-crossing diagonals of a convex -gon, ordered by reverse inclusion: its vertices are the triangulations of the polygon and its facets are the diagonals. It appears in homotopy theory (Stasheff), in the theory of cluster algebras of type , and as the secondary polytope of a convex polygon. Many explicit realizations are known, and a natural question is which of them are genuinely different.
Ceballos, Santos and Ziegler (arXiv:1109.5544, Combinatorica 2014) compare realizations up to normal isomorphism: two polytopes are normally isomorphic if some linear isomorphism of the ambient spaces sends every cone of one normal fan to a cone of the other (their Definition 2.1). This notion ignores the right-hand sides of the defining inequalities and keeps only the linear structure of the facet normals, which is what the classical constructions fix.
One family of realizations is due to Hohlweg and Lange (arXiv:math/0510614, Discrete Comput. Geom. 2007): one associahedron for every sign sequence . The constant sequence gives Loday's associahedron (arXiv:math/0212126), and the alternating sequence gives, up to normal isomorphism, the Chapoton–Fomin–Zelevinsky associahedron (arXiv:math/0202004). This mission formalizes the classification of the Hohlweg–Lange family up to normal isomorphism, Theorem 4.9 of Ceballos–Santos–Ziegler.
Fix . The vertices of a convex -gon are its positions in counterclockwise order. A diagonal joins two distinct non-adjacent positions; two diagonals cross when their endpoints are distinct and alternate around the boundary. The dihedral symmetries are the maps and modulo .
For , the sign word assigns signs to the labels . The polygon places the labels from left to right, positive ones above a horizontal line and negative ones below; going counterclockwise, it visits the negative labels in increasing order and then the positive labels in decreasing order. For a diagonal with labels , the set consists of the labels strictly below the diagonal, and is obtained from it by replacing by and by . The facet of for the diagonal has normal vector , the characteristic vector of taken modulo . In coordinates this is the vector
The normal fan of is the collection of cones , one for each set of pairwise non-crossing diagonals. Two facets are parallel when their normals are negative multiples of each other. The reflection of is (all signs flipped), and its reversal is read backwards.
For all ,
Both directions are content.
The theorem gives an exact count. The number of normally non-isomorphic Hohlweg–Lange associahedra equals the number of sign sequences of length up to reflection and reversal, which is for (OEIS A005418). Together with Hohlweg–Lange's identification of the constant and alternating sequences, it shows that Loday's associahedron and the Chapoton–Fomin–Zelevinsky associahedron are not normally isomorphic for . It is one of the two classifications on which the paper's main result (Theorem 6.1, that the Hohlweg–Lange and Santos families meet only in the Chapoton–Fomin–Zelevinsky associahedron) rests.
Bergeron, Hohlweg, Lange and Thomas (Isometry classes of generalized associahedra, Sém. Lothar. Combin. 61A, 2009) classified the same family up to isometry of normal fans and obtained the same classes. As Remark 4.10 of the paper explains, that classification does not imply this one, because a normal isomorphism need not be an isometry. Combining the two gives Proposition 4.11, that normal isomorphism and isometry coincide for this family.
Theorem 4.9 is proved in the paper; no machine-checked version is known. A formalization would supply the first formal treatment of the crossing graph of polygon diagonals and its automorphisms (Lemma 2.2), of the Hohlweg–Lange normal vectors, and of linear isomorphisms of simplicial fans given by rays on diagonals.
The "if" direction needs two explicit linear isomorphisms. Their action on the sets is not diagonal by diagonal: and have different boundary edges, so the matching of diagonals goes through a mirror image and through the sign swaps of Remark 4.2. One must show that this matching preserves the cone structure, not just the set of normals.
The "only if" direction cannot compare the two polygons by label, since and order their labels differently around the boundary. A linear isomorphism of fans first has to be turned into a combinatorial object. Linearity has to be used twice: it maps rays to rays and preserves cones, which yields a crossing-preserving bijection, and it preserves opposite pairs of normals. Lemma 2.2 then reduces that bijection to one of dihedral symmetries. The remaining step is a case analysis showing that a symmetry preserving the parallel pairs, and the four distinguished diagonals they determine, is a reflection or reversal of . Comparing the multisets of normal vectors alone is not enough: every gives exactly parallel pairs with the same normals .
Fin (n + 3), diagonals are Sym2 (Fin (n + 3)), and crossing, diagonal and triangulation come from the published definition ChvatalArtGallery.FanPartition.Triangulation, used as a reference item. Signs are Bool, and is a function Fin (n - 1) → Bool. Positions and labels are kept apart: hlLabel n σ p is the label at position p.LinearEquiv that sends every cone of the first fan to a cone of the second.An associahedron is a polytope whose faces encode ways to dissect a convex polygon without crossing diagonals. Its vertices represent triangulations. Associahedra occur in geometric combinatorics because the same combinatorial object admits many geometric realizations. Ceballos, Santos and Ziegler ask when two such realizations have the same normal fan up to a linear change of coordinates. This question distinguishes geometric constructions that have identical face lattices but different arrangements of facet normals. Their Santos family is indexed by seed triangulations, so its classification asks exactly how much of a seed can be recovered from its fan. Ceballos, Santos and Ziegler, §5.3.
Santos' construction was presented at a conference in 2004 and first appeared in print in this paper. The paper proves that the number of normal-isomorphism classes in this family is the number of polygon triangulations modulo rotations and reflections. It also explains a useful limit of the result: the set of normal vectors alone determines only the abstract dual tree of the seed triangulation, while the fan retains the further information needed for classification. Ceballos, Santos and Ziegler, §5 and Proposition 5.8.
Take a convex polygon with vertices in cyclic order and label its positions . A diagonal joins two nonadjacent vertices. A triangulation is a maximal collection of diagonals with no crossings. Each triangulation has diagonals. A flip removes one diagonal shared by two triangles and inserts the other diagonal of their quadrilateral.
Choose a seed triangulation . Let , with a coordinate for each seed diagonal . Santos assigns a vector to every polygon diagonal :
For each noncrossing set of diagonals, take the cone spanned by the vectors , , with nonnegative real coefficients. The collection of these cones is the fan . The paper proves that it is complete and is the normal fan of an associahedron. This mission uses that explicit fan as the meaning of , following the paper's own convention in §5.3. Ceballos, Santos and Ziegler, pp. 19, 23, Theorems 5.1–5.2.
Two fans are normally isomorphic here when an invertible real linear map sends every cone of the first to a cone of the second. A dihedral symmetry is a rotation or a reflection of the cyclically ordered polygon. It acts on a triangulation by relabelling both endpoints of each diagonal. Write when such a symmetry sends to .
For every and triangulations of the -gon, the goal is Corollary 5.7:
The left side compares all cones of the two fans through a linear isomorphism. The right side permits only the rotations and reflections of the polygon. It makes no choice of an ordering for the diagonals within either seed.
The milestone list follows the paper's argument: the polygon symmetry theorem for the associahedron's face lattice (Lemma 2.2); the induced crossing and parallelism preserving bijection of diagonals; the description and count of parallel facet pairs for Santos fans (Proposition 5.5); the injectivity of , where contains a seed and all single-flip insertions (Lemma 5.6); and invariance under rotations and reflections. Ceballos, Santos and Ziegler, pp. 6, 23–24.
The classification says precisely which apparent choices of seed triangulation are redundant. In particular, different dihedral orbits produce different normal-fan geometries even though all the resulting polytopes have the associahedron's face lattice. Parallel facet pairs supply an intrinsic geometric trace of the seed: they correspond to each seed diagonal and its flip. Lemma 5.6 then separates distinct seeds from their collections of these pairs. Ceballos, Santos and Ziegler, Proposition 5.5, Lemma 5.6 and Corollary 5.7.
The result is proved in the paper. The formalization work is to give a machine-checked account of its fan model and classification, including the polygon combinatorics and the linear-algebraic implications of a fan isomorphism. The supplied statements are proof targets, with sorry at theorem bodies; a complete Lean proof of the classification is not yet claimed. The explicit diagonal and crossing representation and the seed-indexed vector construction can also be reused to formalize the paper's fan and polytopality theorems.
A face-lattice isomorphism alone does not identify the seed: every associahedron in the family has the same face lattice. A first attempt to compare only the vectors also loses information. Proposition 5.8 shows that two different seed triangulations with isomorphic dual trees can yield linearly equivalent vector sets. The full fan records which vectors span cones together. The central task is to recover a crossing-preserving map of diagonals from a linear map of fans, then use the opposite directions of facet normals to recover . Ceballos, Santos and Ziegler, pp. 23–24, Propositions 5.5 and 5.8.
Lean represents polygon positions by Fin (n + 3) and unordered diagonals by Sym2; crossings and triangulations come from the published Chvátal triangulation definition. The ambient real vector space for a seed is the function space on the subtype of its actual diagonals. This makes the basis intrinsic to . A cone is the nonnegative real hull of the Santos vectors attached to a noncrossing diagonal set. NormallyIsomorphic demands a real linear equivalence of these ambient spaces. The classifying symmetry is explicitly or modulo .
No premise asserts the classification, and the fan is built from the paper's vectors rather than from a chosen list of abstract cones. Arbitrary permutations of diagonals, nonlinear maps, and an abstractly isomorphic dual tree do not satisfy the target's symmetry condition. The goal and the diagonal-action clause of Lemma 2.2 cover every ; the separate group-order clause in Lemma 2.2 applies for . Lemma 5.6 carries the printed bound . The triangular and quadrilateral cases are included in the goal and require their own boundary treatment in a proof. Contributions on crossing preservation, ray distinctness, linear independence of maximal cones, single-flip combinatorics, and dihedral equivariance are welcome.