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.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A 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.
In a prophet inequality, a gambler sees prizes one at a time and must decide when to stop, while a prophet knows every realization and takes the largest. A stopping guarantee compares the gambler’s expected prize with the prophet’s. The order of arrival changes the problem: here the prizes are independent but can have different distributions, and every permutation of their arrival is equally likely. Before seeing any prize, the gambler chooses a threshold for each distribution and accepts the first prize above its threshold. Such a rule has no need to update thresholds after observing rejections. Correa, Foncea, Hoeksma, Oosterwijk, and Vredeveld prove that this restricted rule still earns at least a fraction of the prophet’s expected maximum (Theorem 1, pp. 1455, 1459).
The random-arrival stopping model also supplies guarantees for posted-price mechanisms. A posted price gives a buyer a take-it-or-leave-it offer; the first buyer who accepts ends the sale. The paper explains the connection between its stopping rules and expected revenue under random buyer arrival (§1.1 and §5). This mission formalizes the stopping theorem itself, which is the mathematical guarantee used before that economic translation.
Let , and let be independent, nonnegative real random variables with known, possibly different distributions. Their realizations arrive in a uniformly random order. A nonadaptive threshold rule chooses constants before any realization is observed. It accepts the first arriving index with and receives . If no prize crosses its threshold, its reward is zero. An infinite threshold deliberately excludes an index. The strict comparison matches Theorem 1, even though an earlier description in §1.2 uses a weak comparison (pp. 1454–1455).
For fixed realized prizes, write . Conditional on the set of indices with , each accepted index is equally likely to arrive first. The conditional expected reward is therefore
The prophet benchmark is . The theorem compares with , including distributions for which either expectation may be infinite. The variables need no common distribution and no atomlessness assumption.
The paper’s main supporting result is the Bernoulli Selection Lemma. It starts with independent Bernoulli indicators of success probabilities , fixed real prizes , and a chosen subset . Its payoff is the average , again zero when the denominator vanishes. The lemma compares the best subset with a finite linear optimization problem over and (Lemma 1, p. 1455).
The goal is the exact constant of Theorem 1:
The quantifiers range over every finite nonempty family of independent nonnegative variables. The thresholds are deterministic and indexed by the distributions, and the assertion covers atoms as well as continuous laws. This is the paper’s headline nonadaptive result (Theorem 1, p. 1459).
The milestone list includes the paper’s multilinear formulation (4), its substitution (5), Proposition A.1, Lemmas 2 and 3, and the Bernoulli Selection Lemma. The latter states, in particular, that the maximum expected selected average dominates times the optimum over feasible . Two further milestones express the decomposition of the expected maximum and the upper-tail comparison used for continuous distributions (§2–3 and Appendix A). These targets fix the finite selection problem and the probabilistic quantities that the goal must connect.
The guarantee identifies what fixed, distribution-specific thresholds can achieve under random arrival: the expected accepted prize reaches a constant fraction of the prophet’s benchmark for every collection of independent nonnegative distributions. The paper also gives examples showing why a rule that keeps every positive prize is inadequate and studies where the factor is tight (§2.1 and §3.1). These are claims about the performance of a restricted class of stopping rules, not about an optimal adaptive strategy.
The paper proves Theorem 1; a machine-checked proof of this mission’s goal remains to be supplied. The finite Bernoulli model, its subset optimum, and the nonnegative expectation conventions would be reusable for other random-order stopping and allocation results. This mission makes the paper’s claimed constants, event comparisons, and boundary cases explicit in the theorem statements so a later proof has a fixed target.
Taking the first value above a single low threshold can accept a modest prize before a rare large one arrives. Raising every threshold can instead reject too many prizes. The paper’s example with a constant prize and a rare large prize shows that accepting all available values does not meet the claimed factor (p. 1460). The difficulty is obtaining one set of fixed thresholds that balances those risks across different distributions, while the benchmark selects the largest realization after seeing them all. The Bernoulli selection inequality carries the sharp constant; connecting it to general distributions must also account for ties and atoms.
Lean represents the index set by Fin n with , so its index zero is the paper’s index one. The existing published definition SamuelCahnProphet.Median.Setting.maxX supplies the sample maximum; this mission defines the strict accepted set and its real-valued reward ratio. Thresholds live in because the paper explicitly uses to exclude a variable. Expectations are nonnegative extended integrals of ENNReal.ofReal, preserving infinite values and avoiding a default zero for nonintegrable real integrals. The source’s nonnegativity assumption is represented almost surely, which is enough for these expectations and does not restrict the distributions further.
The Bernoulli law is a finite product formula. Its probabilities lie in , while prizes are arbitrary real numbers as in the printed lemma. The feasibility condition includes : these variables are probabilities, and allowing negative values would change the optimization problem. The finite subset optimum is an attained maximum. Proposition A.1 is stated for ; an empty contradicts the budget conclusion for . It also includes the printed case. Lemma 2 includes as printed: the removable division by zero in (6) is assigned its continuous value . The comparison milestones for continuous distributions assume atomlessness explicitly; the goal does not.
The accepted set depends only on fixed thresholds and the realized values. It cannot depend on the sampled arrival order or on prior observations. A constant choice such as accepting every positive prize does not prove the target guarantee. Contributions that establish the finite Bernoulli selection result, its analytic bounds, the random-order reward identity, or the passage from continuous to arbitrary distributions all serve the stated goal. The random-order identity and the discontinuous case are further work beyond the current milestone list.
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.
In a prophet inequality, a decision maker observes random rewards one at a time and must choose without seeing future realizations. The benchmark is a prophet who sees all rewards and selects their maximum. A nonadaptive threshold rule chooses a threshold for each reward before observations begin, then accepts the first arriving reward that crosses its threshold. This model captures a simple class of stopping rules and, through the prophet inequality connection, informs posted price mechanisms in which prices are set before buyers arrive. Correa et al. (2021) prove that under uniformly random arrival order some such rule earns at least a fraction of the prophet's expected reward. The question here is whether that guarantee improves when the reward distributions are identical.
Fix an integer and draw independent rewards from the same three point law. A reward is with probability , is with probability , and is otherwise. The three probabilities are nonnegative and sum to one for . Thus a typical sample contains roughly unit rewards, while a high reward is rare enough that its presence among all draws has probability on the order of . Its magnitude is on the order of , so it still makes a nonvanishing contribution to the prophet's expected reward.
Give each coordinate a predetermined threshold . A uniformly random order reveals the sampled rewards, and the rule accepts the first . Conditional on a sample, let . Each accepted coordinate is equally likely to arrive first among , so the conditional expected reward is
Write for the rule's reward and for the prophet's reward. These are expectations of nonnegative random variables. The thresholds may be infinite, allowing a coordinate to be discarded in advance.
The goal is the paper's i.i.d. tightness claim: for every , sufficiently large members of this explicit family satisfy
The universal quantifier includes every nonadaptive threshold vector, including asymmetric thresholds and coordinates that are never accepted. The proof in Appendix B supports the displayed statement for every sufficiently large , which strengthens the existence of one hard instance stated in Section 3.1. Together with the paper's lower bound, this shows that the factor cannot be raised for this rule class even under identical distributions.
The milestones cover the prophet limit , reduction of arbitrary thresholds to two-level rules, the three contributions to a two-level rule's expected reward according to the number of high observations, Proposition A.3's scalar maximization, and the resulting uniform asymptotic bound on all two-level rules. The first coordinates of a two-level rule accept both and ; the remaining coordinates accept only . These targets correspond to Section 3.1, Proposition A.3, and Appendix B of Correa et al..
The explicit i.i.d. family locates a limit of nonadaptive thresholds under random arrivals. Identical distributions remove heterogeneity as an explanation for the loss against a prophet: the obstruction remains even when every reward has the same law. Consequently, an improved guarantee requires a richer rule class or additional assumptions on the distribution. The paper studies an adaptive threshold rule separately and obtains a stronger i.i.d. guarantee; this mission isolates the upper bound for the nonadaptive class.
Formalizing this result supplies a reusable model for random-order threshold selection on a finite i.i.d. product space, including its conditional reward formula and extended nonnegative expectations. The paper proves the tightness result; the Lean declarations in this proposal state it and its supporting results as proof obligations. The published i.i.d. product-measure model from the Samuel-Cahn development already has machine-checked definitions and is reused here. The proposed upper-bound theorems have not yet been proved in Lean.
Bounding each coordinate's expected contribution in isolation loses the interaction between unit rewards and the rare high reward. When a high reward occurs, accepting many unit rewards can dilute its share of the random-order reward; rejecting unit rewards sacrifices ordinary samples. The reduction to two-level rules must apply to every threshold vector before the count of unit-accepting coordinates can be optimized. Appendix B then controls the cases of zero, one, and at least two high observations uniformly in that count. The one-high-value case contains a printed final inequality that drops a positive term; the formal target uses the preceding, valid bound, whose extra term vanishes in the limit.
Lean represents a sample as Fin (n ^ 2) → ℝ and its law as a finite product measure. The index set is 0-based: the paper's are coordinates . The law is used only for , where it is a probability measure. Thresholds have type , and crossing is strict, matching Theorem 1's indicator . The page describes its two-level rule with weak threshold language; under strict crossing the same acceptance sets use thresholds and . The reward uses the paper's convention. Expectations are lintegrals with values in $[0,\infty]`, avoiding a zero default for nonintegrable real integrals. The goal quantifies over all threshold vectors and uses the actual prophet expectation of the same law; no restricted rule class or surrogate benchmark can replace either one.
The general i.i.d. law, sample maximum, and expected maximum come from SamuelCahnProphet.IID.Setting. The paper's three point law, random-order reward, canonical two-level rule, and high-value count are local definitions. Useful contributions include exact finite-law calculations, dominance of two-level rules, uniform estimates in , and the scalar exponential inequality of Proposition A.3. These parts can also support formal work on other finite-support prophet inequalities.
A prophet inequality compares a gambler who sees nonnegative random rewards one at a time, and must accept or reject each on arrival, with a prophet who knows all values in advance and simply takes . For independent and identically distributed (i.i.d.) rewards the question is the best constant such that some online rule always earns at least . The question matters in operations research and mechanism design because a seller who posts take-it-or-leave-it prices to arriving customers faces exactly this stopping problem on the customers' virtual values; prophet inequalities translate into revenue guarantees for posted price mechanisms relative to Myerson's optimal auction (Chawla, Hartline, Malec and Sivan 2010).
Timeline (as recounted in §1 of the paper):
Let be i.i.d. nonnegative random variables with distribution function . A threshold rule fixes real numbers and stops at
receiving . Because the thresholds may change with the step , the rule is adaptive; for i.i.d. variables the number of variables already seen is all the history the rule needs.
The analysis works with quantiles. The generalized inverse is , and is the threshold that accepts with probability (with a coin toss to break ties at an atom). The function
is the expected reward from a variable accepted with probability . The quantile stopping rule of Algorithm 2 partitions into intervals , draws an acceptance probability with density proportional to , and stops at step with probability ; its value is . The analysis then passes through the normalizations and , the recursion (8)–(9) on , and the differential equation
Let be the unique solution of
For every and every law of nonnegative i.i.d. there are thresholds with
In order: the quantile sandwich ; the representation (7) ; the identity "expected reward of the quantile rule at equals "; Lemma 4 (); Lemma 5 ( when all agree); the equivalence of equal with the recursion (8) and ; the closed form (9)–(10); Lemma 6 on (ODE); Proposition D.1; Lemma 7 (); uniqueness of in (2); optimality of the dynamic-programming thresholds; domination of the randomized rule by them; and .
A companion statement records the numerical guarantee .
The result. Theorem 2 gives the optimal constant of the i.i.d. prophet inequality and, through , shows for every , which settles the problem posed by Hill and Kertz in 1982. Since (Kertz 1986), no rule of any kind achieves a better constant uniformly in . Through the virtual-value connection it implies that, for customers with i.i.d. valuations, an adaptive posted price mechanism earns at least a fraction of the optimal auction's revenue (Corollary 2 of the paper).
Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any of its lemmas is known. The proof combines a measure-theoretic part (quantile functions, randomized tie-breaking at atoms, Tonelli and integration by parts), a combinatorial recursion, and real analysis of an autonomous ODE with a third-derivative Taylor argument. Formal versions of these parts are reusable: the quantile representation of , the expected reward of a quantile rule, and the optimality of dynamic-programming thresholds are standard tools across prophet inequalities and optimal stopping.
The obvious attempt, computing the optimal dynamic-programming thresholds and bounding their value against , does not lead to a closed-form constant: the optimal values satisfy a nonlinear recursion that depends on the whole distribution. The paper avoids it by analysing a randomized rule whose value is exactly a -weighted average of , which reduces the problem to a distribution-free recursion. Two steps then carry the weight. First, randomizing correctly at atoms of so that every step accepts with probability exactly ; without this, is not the step reward. Second, comparing the discrete recursion (9) with the continuous (ODE): the comparison needs strict convexity and , and the latter holds only because , a standing assumption validated at at the end. The existence of the partition with all equal (a solution of (8) with , , ) is taken from Hill and Kertz and is not proved in the paper.
Lean conventions:
SamuelCahnProphet.IID.iidLaw μ n (the published i.i.d. setting), and is its Emax. Coordinates are 0-based; the partition , , and the recursion keep the paper's 1-based index.A degenerate cannot trivialize the goal: is pinned by (2) and , and the goal is stated for every and every nonnegative law, including laws with infinite mean.
A complete development needs the quantile function of a law on , Tonelli's theorem on product measures, uniqueness for ODEs with locally Lipschitz right-hand side (ODE_solution_unique), and Taylor's theorem; the existence of the Hill–Kertz partition is a further proof obligation. Contributions to any milestone, and reusable lemmas on quantile functions and finite-horizon optimal stopping, are welcome.
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.
Boundary control of a transport equation acts at the edge of a spatial interval, while the state evolves throughout the interval. A backstepping transformation connects the original state to a simpler target state by integrating against kernels on a triangular region. The transformation is useful only when those kernels exist with the regularity and uniqueness needed to define a single feedback law. Coron, Vazquez, Krstic and Bastin use this construction for a two-component quasilinear hyperbolic system. Their Appendix A isolates a four-component linear kernel system and proves its well-posedness independently of the later stability arguments (Coron et al., Appendix A).
This mission concerns that appendix result. The paper states a generic system broad enough to include the kernel equations arising from its controller design. Its goal is a unique continuous solution on the closed triangle, assuming continuous coefficients and strictly positive transport speeds. The result supplies the existence and uniqueness premise for the paper's later linear and quasilinear stabilization results. It is a proved result in the source preprint; the work here is to state its analytic content precisely in Lean and leave its proof as a formalization target.
Let . There are four unknown real functions on . Two positive, continuous functions describe the characteristic speeds. Four functions supply forcing, and sixteen functions couple the unknown components. The functions and are continuous on . Boundary functions are continuous on . The paper's equations (A.1)–(A.4) have first-order directional derivatives of on the left and on the right (Coron et al., p. 18).
The boundary data have two forms. Components and are prescribed on the diagonal : and . Components and are prescribed on the lower edge with linear dependence on and . For example, . The fourth component uses in the same way. Those edge couplings are part of the problem, rather than optional side conditions.
For merely continuous , a classical partial derivative need not exist. Accordingly, the mission uses the paper's characteristic integral equations (A.23) as the meaning of solution. The travel-time coordinates are for , with . Each characteristic starts on the prescribed part of the boundary and ends at . The value of equals its starting boundary value plus the forcing and coupling integrals along that characteristic. A continuously differentiable solution of the differential equations and the boundary conditions satisfies this integral form (Coron et al., pp. 19–20).
The goal is Theorem A.1: for every set of data with the continuity and positivity assumptions above, there is a continuous characteristic solution on , and any two such solutions agree at every point of :
Four source results mark the path to that goal. Lemma A.3 keeps every characteristic in and records its continuity and coordinate inequalities. Lemma A.4 bounds the integral of the th power of its first coordinate by . Lemma A.5 bounds one application of the linear integral operator to an increment satisfying a factorial estimate. Proposition A.6 bounds the resulting infinite series by (Coron et al., pp. 19, 21–23). These are the mission's four milestones.
Theorem A.1 fixes a genuine mathematical issue behind the feedback construction: a kernel cannot be treated as an arbitrary coefficient of a controller when its defining boundary problem has not been solved. Existence gives a kernel for the transformation; uniqueness makes that kernel determined by the coefficient data. The theorem is stated for a generic coupled system, so the same result can support several kernels rather than just one equation in the control design (Coron et al., Appendix A).
Formalizing this known proof would add a reusable interface for characteristic coordinates, bounded coefficient functions on a triangle, and coupled Volterra-type integral operators. The present proposal contains statements, not completed proofs. The local prior-art search found no published Goursat kernel item with the same four-component system and boundary conventions. The broader paper's linear and quasilinear stability results are separate missions; this one records their analytic kernel prerequisite without importing their controller definitions.
The mixed boundaries make the usual one-direction transport picture insufficient. Two characteristic families enter from , while two enter from the diagonal. Moreover, the lower-edge values of and depend on the other components at that edge. Thus a bound for one component cannot ignore the other three or assume all boundary values are given independently. A candidate continuous solution must also be shown to agree with the same integral equations at the corner and along both boundary segments. The explicit characteristics involve the inverse of , whose argument and range must be checked throughout (Coron et al., pp. 19–23).
The Lean data bundle contains globally defined real functions, with continuity and positivity imposed only on or . Such functions represent continuous data on those closed domains by extension; values outside the domains do not enter the statements. The four components use Fin 4, indexed in Lean for the paper's . The two lower-edge couplings and the two diagonal values are all included in IsCharSolution. Equality in the uniqueness clause is restricted to , because the extensions outside it are unconstrained.
The coordinate inverses are Function.invFunOn on ; only arguments in their ranges have mathematical meaning here. Lemma A.3 includes the domain facts that keep the characteristics in range. Integrals are over finite characteristic intervals with continuous integrands, and the maxima in (A.35) are suprema of continuous images of compact sets, not suprema over all real inputs. Proposition A.6 asserts summability before using an infinite sum. Lemmas A.4 and A.5 include , a valid base case needed by the source's induction. Lemma A.5 makes the continuity of the increment explicit so its integrals retain their intended values. Existence and uniqueness both remain in the goal; retaining only one would change Theorem A.1. Two formalizations would trivialize or falsify the goal and are ruled out: dropping the boundary conditions (A.5)–(A.7) from the solution notion makes uniqueness false, and reading the PDEs (A.1)–(A.4) classically for a merely continuous would make existence false; the solution notion is the paper's characteristic integral form with all boundary conditions. Contributions to the characteristic and operator estimates, continuity of the constructed limit, and the uniqueness argument are within scope.
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.A quantum algorithm for a system of linear equations must turn operations it can implement into an approximation of the inverse of the system matrix. For a Hermitian matrix, time evolution is such an operation. Childs, Kothari and Somma use a Fourier expansion of the scalar reciprocal to express an approximation to as a finite linear combination of these evolutions. Their paper reports an exponential improvement in the dependence on the requested precision over earlier linear-systems methods. The scalar approximation in Lemma 11 is the mathematical input to their Fourier algorithm and to the query and gate analyses in Theorem 3. This mission isolates that approximation and the Gaussian estimates stated around it. Theorem 3's complexity claims themselves are outside the present formalization. Childs, Kothari and Somma, §3, pp. 10–14.
Fix a condition number . The scalar spectral domain is
It contains the real eigenvalues permitted after the paper's normalization and excludes zero, where the reciprocal is undefined. For an accuracy , two functions are -close on when their difference has magnitude at most at every point of that domain. A complex-valued approximant is compared with as a complex number. The paper gives this domain and closeness convention before the Fourier construction. Childs, Kothari and Somma, pp. 9–10.
The intermediate function is a truncated Gaussian Fourier integral. It integrates over and then over , multiplying by . The finite approximant is a Gaussian Fourier double sum with the same normalization and phase. Its samples are for and for ; each term carries both mesh widths. Thus count the retained samples, while control their spacing. The sign in the phase and the factor are part of the definitions. Childs, Kothari and Somma, (18), p. 10, and (21), p. 11.
Lemma 12 says that for cutoffs of scale
the function is -close to on . The proposal includes the paper's explicit error bound (27) and its Gaussian tail bound (28), as well as the Gaussian Poisson-summation identity of Lemma 13. These are separate reusable targets, not replacements for the approximation theorem. Childs, Kothari and Somma, Lemmas 12–13 and (27)–(28), pp. 11–12.
The goal is Lemma 11:
where
The statements impose upper and lower bounds with absolute constants, uniformly across and . The requested approximation error is exactly , matching the lemma's claim. The four scales specify both the size of the finite expansion and its mesh. Childs, Kothari and Somma, Lemma 11, p. 10.
The finite sum provides the paper's Fourier route from scalar reciprocal approximation to a linear combination of time-evolution operators. Its sample counts and spacings are the quantities that enter the algorithm's implementation costs. A result that only asserted approximation after arbitrarily many samples would not express the bound used there. The truncated integral and Poisson identity also remain useful for other Gaussian quadrature and Fourier-sampling arguments. Childs, Kothari and Somma, §§3.1–3.2, pp. 11–14.
The paper proves these claims on paper. This proposal asks for machine-checked Lean proofs of the scalar statements, including the complex normalization, the finite and infinite sum conventions, and the uniform scale bounds. It does not assert that the quantum algorithm, its Hamiltonian simulation subroutines, or its query and gate complexity theorems have been formalized.
The infinite Gaussian Fourier representation alone does not specify a finite implementable expansion. Restricting both integrals introduces two truncation errors, while replacing them by samples adds discretization and periodic-aliasing effects. These errors have to be controlled simultaneously with , , , and at the scales stated in Lemma 11. Merely taking the mesh arbitrarily fine gives approximation without the theorem's finite-size bounds. The proof also uses a complex Fourier phase although its target is real, and its infinite sums must have their ordinary convergent meaning. Childs, Kothari and Somma, proof of Lemma 11, pp. 13–14.
The Lean development uses for and the cutoff and mesh parameters, for and , and the complex norm for closeness. Finite sums use exactly and ; the integral for is iterated and has nonnegative upper cutoffs. The optional identity (20) is also an iterated integral, with the integral evaluated before the integral. Infinite sums in Lemma 13 are over . The Gaussian integrals and series in the statements are convergent, so Lean's totalized integral and sum conventions do not supply artificial zero values.
The paper's condition-number convention is recorded as and Corollary 10's operating range as . Those conditions keep nonempty and positive. The unnumbered reciprocal-exponential bound from p. 13 has explicitly, because the printed fractions have no value at zero. The bounds quantify their constants before the problem parameters. In particular, choices with unbounded sample counts or vanishing mesh widths cannot satisfy the goal solely by brute-force approximation.
A complete development needs reusable Gaussian integration and tail estimates, complex exponential identities, summability of Gaussian integer series, and Poisson summation in Mathlib's analytic setting. Contributions that establish these general facts, the stated milestones, or Lemma 11 with its original bounds all fit this scope. This mission uses the reviewed shared definition of . Childs, Kothari and Somma, pp. 9–14.
When indivisible goods are shared among people, comparing each person's bundle with another person's bundle is only one way to judge fairness. A second test asks whether a group could repartition the goods it collectively received so that one of its members would reliably obtain more. Groupwise maximin share (GMMS) makes this test for every subgroup. It strengthens the ordinary maximin-share benchmark, which tests only the grand coalition and all goods. Chaudhury, Kavitha, Mehlhorn and Sgouritsa use this distinction to study a complete allocation obtained from their almost envy-free allocation: goods initially left unassigned are given to one unenvied agent. Their Theorem 16 proves that the resulting allocation gives every agent at least four sevenths of her groupwise maximin share under additive valuations. Chaudhury et al., pp. 4–5, 15–16.
The paper first constructs a partial EFX allocation whose unallocated goods have bounded value to every agent. Its Section 3 then assumes additive valuations and derives maximin-share and GMMS guarantees. This mission addresses the GMMS consequence of that construction. The existence of the starting allocation is the subject of the first mission in this series; the present theorem specifies what happens when its pool is donated. Chaudhury et al., Theorems 8 and 16.
Let be a finite set of agents and a finite set of indivisible goods. Each agent has a valuation for a bundle . Here valuations are nonnegative and additive: is the sum of the values of the individual goods in . A partial allocation gives pairwise disjoint bundles to the agents. The remaining goods form its pool, . An allocation is complete when its pool is empty. These are the paper's allocation conventions. Chaudhury et al., pp. 3–4.
An allocation is envy-free up to any good (EFX) if, after any single good is removed from agent 's bundle, agent values that remainder no more than her own bundle: for all and . The envy graph has a directed edge when values 's bundle more than her own. A source is a vertex with no incoming edge, so nobody envies that agent. Chaudhury et al., pp. 3, 8.
For a set and a positive number of parts, is the largest worst-part value agent can secure by partitioning into bundles. A complete allocation is -GMMS when each agent meets an fraction of this benchmark for every subgroup containing her:
The benchmark uses only goods allocated to that subgroup. The paper states it both as a complete-allocation property in its introduction and in Definition 15. Chaudhury et al., pp. 5, 15.
Assume is partial and EFX, every agent satisfies , and is a source of its envy graph. Define and for . The goal states that is complete, that donation does not lower any agent's own value, and that
This is the GMMS bullet of Theorem 16 applied to the particular allocation the authors define immediately before it. The paper obtains a suitable from Lemma 12, which has the relevant properties of Theorem 8. Chaudhury et al., pp. 11–12, 14–16.
The milestones are Proposition 13, the reduction step in Theorem 16's proof, and all three parts of Lemma 17. Proposition 13 compares maximin shares after deleting agents and at most as many goods. Lemma 17 bounds the value of each bad good, the donated bundle, and the other good bundles. They retain the constants and used in the paper. Chaudhury et al., pp. 14, 16–17.
The result turns an almost envy-free partial allocation into a complete allocation with a guarantee for every coalition. A plain maximin-share statement would only compare each agent with a partition of all goods among all agents; here every subgroup and its allocated goods count. The distinction matters even when an ordinary maximin-share bound is easy to meet because there are fewer goods than agents. Chaudhury et al., p. 5.
The paper proves Theorem 16 mathematically. The remaining work for this mission is a machine-checked proof of its stated GMMS consequence and its supporting results. Its definitions of partial allocation, pool, finite maximin share and groupwise guarantee can also serve later formalizations of fair division. The Nash-social-welfare half-guarantee in the printed theorem depends on the starting allocation from Lemma 12; this mission records only the value preservation under donation. Chaudhury et al., pp. 14, 16.
Giving all leftover goods to one agent makes the allocation complete, but it can change how another agent values that enlarged bundle and how a subgroup's benchmark is calculated. EFX alone compares bundles after deleting one good; GMMS compares an agent with every repartition of a subgroup's goods. The difficulty is to control those repartitions while keeping the exact constant. Merely applying an ordinary maximin-share bound to the grand coalition does not establish the required subgroup inequalities. Chaudhury et al., pp. 15–17.
Agents and goods are represented by Fin n and Fin m; Lean numbers agents from zero, and the paper's “agent 1” is an explicit source . Bundles are finite sets. Valuations are real-valued but include nonnegativity alongside additivity, representing the paper's codomain . The pool is computed from , and the donated allocation is a function of and . No independent pool or arbitrary completed allocation is allowed. Completeness is a conclusion. The maximin share is a finite maximum of finite minima over labelled partitions, which may have empty parts. Every use has a positive part count; in the GMMS definition this follows from . Cardinality is converted to real numbers before fractions are formed. These choices exclude zero-part maximin shares and integer division. Chaudhury et al., pp. 3–5, 15–16.
The theorem is conditional on the EFX and pool-value properties of the source allocation, rather than repeating its existence proof. It states the conclusion for every such allocation and every source. The paper's half-optimal-Nash-social-welfare bullet is outside this mission because it invokes the separate black-box starting allocation of Lemma 12. Contributions toward finite-partition comparisons, EFX value bounds, and the groupwise estimate are welcome. Chaudhury et al., pp. 14–17.
An associahedron of dimension is a simple polytope whose nonempty faces correspond, reversing inclusion, to the sets of pairwise non-crossing diagonals of a convex -gon: its vertices are the triangulations of the polygon and its facets are the diagonals. Associahedra appear in the combinatorics of parenthesizations (Tamari, Stasheff), in the theory of cluster algebras of type , where the Chapoton–Fomin–Zelevinsky construction realizes the cluster complex as the normal fan of a polytope, and in the study of secondary polytopes (Gelfand–Kapranov–Zelevinsky).
Many different polytopes realize the associahedron. Ceballos, Santos and Ziegler (arXiv:1109.5544v2) compare them up to normal isomorphism, a linear isomorphism of normal fans. One of the families they study, the "type II" family, is a construction of Santos presented at a conference in 2004 and first published in that paper (§5, pp. 18–23). It produces one associahedron for every triangulation of the -gon, the seed triangulation, and contains the Chapoton–Fomin–Zelevinsky associahedron as the case of the snake seed. This mission formalizes the statement that the construction works for every seed: Theorems 5.1 and 5.2 of the paper.
Let and , and number the vertices of a convex -gon counterclockwise. A diagonal joins two non-adjacent vertices; two diagonals cross when their endpoints are distinct and alternate around the boundary; a triangulation is a maximal set of pairwise non-crossing diagonals, and has elements. Two triangulations differ by a flip when and .
Fix a triangulation and let , with basis vectors , . Santos' vectors (p. 19) are
For a set of diagonals, is the cone spanned by the vectors , . The fan is the collection of the cones for all non-crossing sets , the empty set giving .
The cones of the triangulations form a complete simplicial fan when the vectors of each triangulation are linearly independent, every vector of lies in one of these cones, and any two of them meet in the cone of their common diagonals.
For a polytope and , the exterior normal cone is , where . The normal fan of is the set of all , , one cone for each nonempty face (p. 5).
For every triangulation of the -gon,
A polytope with normal fan is an -dimensional associahedron. The goal fixes no weights and no right-hand sides: it asserts only that some polytope has this normal fan.
Theorems 5.1 and 5.2 are what make Santos' family a family of associahedra at all. Every later statement of the paper about type II, including the classification up to normal isomorphism (Corollary 5.7: seeds agreeing up to rotation and reflection) and the identification of the Chapoton–Fomin–Zelevinsky associahedron as the only realization of both types (Theorem 6.1), compares the fans , and the word "associahedron" in them rests on these two theorems. The construction yields Catalan-many fans with facet normals in -coordinates, and modulo rotations and reflections they are pairwise non-isomorphic.
The theorems are proved in the paper; to the best of a search of the Prove2Me catalogue, nothing about normal fans of polytopes, complete simplicial fans or associahedra has been formalized there, and Mathlib at the pinned revision has no notion of fan. The formalization would provide a machine-checked polytopality criterion for complete simplicial fans (Lemma 5.4), an explicit flip analysis of Santos' vectors (Lemma 5.3), and a polytopal realization of the associahedron for every seed.
Theorem 5.1 is not a direct computation. Linear independence of each triangulation and a sign condition for each flip do not by themselves make a fan; the paper combines them with assertion (1), a region covered by exactly one cone, and appeals to a covering criterion for vector configurations (De Loera–Rambau–Santos, Triangulations, Cor. 4.5.20, properties (ICoP) and (IPP)). A solver will likely need to formalize that criterion, or an equivalent argument that a pseudo-manifold of simplicial cones with these properties covers the space exactly once.
Lemma 5.3 requires a case analysis of how the seed triangulation meets the quadrilateral of a flip; the paper distinguishes four configurations, each with its own dependence (equations (4)–(7), p. 21), and showing that the four are exhaustive is itself a combinatorial statement about triangulations. Lemma 5.4 requires constructing a polytope from weights and identifying all of its normal cones, including the lower-dimensional ones, with the cones of the fan. Finally, the uniform constant has to work for all flips at once; for the dependence (4) the unperturbed weights ( on , elsewhere) give exactly zero, so a perturbation is unavoidable and must not spoil the other cases.
Vertices of the polygon are Fin (n + 3), chords are Sym2 (Fin (n + 3)), and diagonals, crossing and triangulations are reused from the published definition ChvatalArtGallery.FanPartition.Triangulation. The space is {d // d ∈ T₀} → ℝ, coordinate being the coefficient of . Cones are nonnegative hulls (PointedCone.hull ℝ). The fan contains every face, including .
"Normal fan of a polytope" is encoded as: is the convex hull of a finite set, and the set of cones equals with exterior normal cones, functionals identified with vectors by the coordinate pairing. Because is a cone of , the polytope must be full-dimensional; a point, a lower-dimensional polytope, or "some polytope whose facet normals are the rays" does not satisfy the goal. The inner-normal convention would give the fan , which is a different statement. The polytope is specified only through its normal fan, as in the paper.
Lemma 5.4 is stated for fans whose rays are indexed by the diagonals and whose maximal cones are the triangulations, the case in which the paper uses it; adjacent maximal cones are flip pairs. Lemma 5.3 requires the two coefficients to be strictly positive, as assertion (2) does, so the zero dependence is excluded. The ε of milestone 6 is quantified as . The weight is computed on 0-based positions as for , which equals the paper's 1-based .
A complete development needs basic fan theory (simplicial cones, a covering criterion), the polar construction behind Lemma 5.4, and the flip case analysis. The first two are reusable beyond this mission, for any polytopality argument on simplicial fans. Contributions of general lemmas on simplicial cones and on normal cones of polytopes are welcome.
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.
Many matrix algorithms spend most of their time reading their input. A matrix with few nonzero entries should admit routines whose cost scales with that number, rather than with the product of its dimensions. Clarkson and Woodruff study random maps that compress a matrix before a regression or low rank approximation calculation while retaining the geometric information those calculations need. Their sparse embedding has one nonzero entry per input coordinate, so applying it to a sparse matrix can be charged to the matrix's nonzero entries. The probability guarantee for its geometry is Theorem 11 of the preprint, the target of this mission.
The paper proves further results for faster regression and low rank approximation after sketching. Those applications use the subspace guarantee as an input. This mission concentrates on that guarantee and the statements in §3 that support it. The source is the 5 April 2013 arXiv version; theorem and page labels below refer to that version.
Fix a real matrix of rank . Its column space is . A map is a subspace embedding for when it approximately preserves the length of every vector in simultaneously. The dimension , rather than the number of rows , controls the size required of the compressed space.
Here is the sparse embedding matrix . Each input coordinate independently chooses one bucket uniformly. The binary matrix has a at and zero elsewhere in column . Independently, is diagonal with a fair sign or at each coordinate. Thus the output in bucket is the signed sum of input coordinates assigned to . The probability in this mission is over the joint, uniform choice of all bucket assignments and signs, with fixed in advance. This is the construction in §2, p. 7.
For an orthonormal basis matrix of , the leverage score of row is . A threshold separates light coordinates, with , from heavy coordinates, with . The paper describes this split after sorting rows by leverage; the threshold description selects the same coordinates and keeps the input's original order. The bucket event bounds the sum of light leverage scores assigned to each bucket. The heavy event says that distinct heavy coordinates receive distinct buckets. These are properties of alone; the later concentration statements take probability over the independent signs after fixing a suitable .
There is an absolute constant such that for every of rank , every , and every integer ,
The event contains the universal quantifier over : one draw must work for the whole column space. The squared-norm estimate implies the norm formulation printed in Theorem 11, p. 11 on this range of . The paper gives its proof in §3, pp. 7–11.
The milestone list follows the paper's statements: a coordinate bound from §3.1; the weighted bucket estimate of Lemma 2; light-coordinate concentration in Lemma 3; the collision and exact-preservation statement of Lemma 5; the heavy-light cross-term estimate in Lemma 6; fixed-vector preservation in Lemma 7; and the passage to the whole subspace in Lemma 8. Their distinct probability spaces matter. Lemmas 2 and 5 concern bucket assignments, Lemmas 3, 6, and 7 concern signs for a fixed suitable assignment, and Lemma 8 is a general statement about a random linear map.
Theorem 11 gives a single compact random matrix that retains the Euclidean geometry of every vector in a specified rank- column space with probability at least . It supports sketch-and-solve algorithms: a computation performed on can use a much smaller row dimension while reasoning about the original column space. The construction also has exactly one nonzero per column, the structural fact behind its input-sparsity running time. The running-time bound is stated in the paper, but this mission's Lean target concerns the mathematical norm guarantee.
The paper already proves the theorem; the open work here is a machine-checked development of its statement and proof. The finite probability model, explicit squared norms, leverage scores, and bucket events can support later formalizations of other sparse sketching results. No machine-checked proof of Theorem 11 is claimed by this proposal. A complete development may reuse proved concentration inequalities from Mathlib or the platform, but the cited inequalities need their hypotheses checked against the finite-sign and weighted-bucket models used here.
A fixed-vector estimate does not itself imply that one random sketch works for all vectors of an uncountable subspace: the quantifier cannot simply be moved through the probability. Collisions also have different effects on high- and low-leverage coordinates. Heavy coordinates need a no-collision event; light coordinates can share buckets only while their total bucket weight remains controlled. The paper's statements keep these events and probability spaces separate. The final whole-subspace claim requires a uniform estimate whose failure probability accounts for the dimension .
Vectors are functions Fin n → ℝ, matrices are finite real matrices, and and are explicit sums of coordinate squares. The sample space is the product of all bucket maps and all Boolean sign assignments, with counting probability. Every theorem with a freely chosen bucket count assumes ; otherwise a Fin 0 sample space could make division by its cardinality meaningless. The theorem's size threshold forces this automatically when and . Matrix rank is Mathlib's matrix rank.
The formalization fixes in Theorem 11. The upper bound prevents the logarithmic size expression from degenerating near , and keeps its logarithm and division meaningful. Positive and are explicit where needed; Lemma 6 restricts . The heavy/light split uses leverage thresholds rather than a row permutation, and constants described as absolute are quantified before every dimension, matrix, error, and failure parameter. In particular, Theorem 11's event quantifies over all inside the probability, while Lemma 7 fixes before sampling signs. These choices exclude degenerate distributions, vacuous error ranges, and a fixed-vector claim masquerading as the goal.
The refined clause at the end of Theorem 11 is left out: its printed conflicts with the proof's collision requirement , and its threshold parameter is not fixed in the claim. Lemma 1 and the cited Hanson–Wright moment result, Theorem 4, are proof tools outside this proposal's milestone set. Contributions that formalize those tools faithfully, prove the bucket and sign estimates, or connect the finite model to existing probability libraries are useful for the goal.
A set of agents must share a set of indivisible goods, each agent valuing bundles of goods by her own valuation. Two fairness notions dominate the literature. Envy-freeness up to any good (EFX), introduced by Caragiannis, Kurokawa, Moulin, Procaccia, Shah and Wang (EC 2016), asks that no agent prefer another's bundle once any single good is removed from it. The maximin share (MMS), proposed by Budish (JPE 2011), asks that every agent receive at least what she could secure by splitting the goods into bundles herself and taking the worst one.
Neither notion is known to be achievable in full. Whether complete EFX allocations always exist is open in general. Complete MMS allocations need not exist: Procaccia and Wang (EC 2014) gave a counterexample with three agents, and the best known approximation factors for additive valuations are (Ghodsi et al., EC 2018) and (Garg and Taki, arXiv:1903.00029). Amanatidis, Birmpas and Markakis (IJCAI 2018) showed that every complete EFX allocation is a -MMS allocation.
Caragiannis, Gravin and Huang (EC 2019) showed that EFX can be achieved if some goods are left unallocated, with no bound on how many. Chaudhury, Kavitha, Mehlhorn and Sgouritsa (arXiv:1907.04596, SODA 2020, SIAM J. Comput. 2021) relax completeness instead: some goods may be "donated to charity". Their Theorem 8 produces an EFX partial allocation in which nobody envies the donated set and the donated set has fewer goods than there are unenvied agents. This mission formalizes their Theorem 14: such an allocation also gives every agent a maximin-share guarantee that improves as more goods are donated.
Agents are and goods are , . Agent has a valuation , assumed additive: for every .
A (partial) allocation gives agent the bundle , the bundles being pairwise disjoint. The pool of unallocated goods is , and .
the maximum over partitions of into possibly empty bundles. Agent 's maximin share in the instance is .
The three conditions of Theorem 8 on are:
For every allocation with pool satisfying conditions 1–3, and every agent ,
The factor ranges from when to when .
Theorem 14 shows that leaving goods unallocated is not merely a cost: under conditions 1–3, each donated good buys a quantitative improvement of every agent's maximin-share guarantee, interpolating between the factor the bound gives when the pool is empty and a factor tending to when nearly goods are donated. Together with Theorem 8 it shows that a single allocation can be simultaneously EFX, envy-free towards the charity, small in its charity, and approximately MMS. The same reduction (Proposition 13 applied to a carefully chosen sub-instance) is the template for the paper's -groupwise-maximin-share result, Theorem 16, formalized in mission III of this series.
The result is proved in the paper; no machine-checked proof of it, of Proposition 13, or of the existence of EFX allocations with bounded charity is known to exist. The mission produces a formal maximin-share definition on arbitrary subsets of goods with an arbitrary number of bundles, a formal proof of the monotonicity of the maximin share under removal of agents and goods (Proposition 13, which the paper quotes without proof), and the guarantee itself. Combined with mission I of this series (Theorem 8), it yields the printed existence statement.
The guarantee compares an agent's own bundle with a benchmark defined over all partitions of all goods, while EFX and the source condition speak only about the allocation at hand. The obvious attempt, summing over all agents and adding the pool, gives only a factor near and ignores the pool's size. Agents holding a single good are the obstruction: EFX gives no bound on the value of their bundles relative to , and the benchmark is defined on the full instance, which contains them. Proposition 13, the comparison of maximin shares across instances, is a combinatorial statement about all partitions of the original instance and requires nonnegativity of the valuations: with a good of negative value it fails.
Agents are Fin n (0-based) and goods Fin m; the set is the whole of Fin m. Valuations are functions Fin n → Finset (Fin m) → ℝ; additivity is the sum formula together with nonnegativity, which is the paper's codomain . An allocation is a family of pairwise disjoint finsets and the pool is always computed as the complement of their union, never taken as a free parameter. Sources are agents of indegree zero in the envy graph (nobody envies them), not agents who envy nobody. The maximin share is a supremum over labellings Fin m → Fin k' restricted to of the minimum bundle value; it is used only with , which every statement has in its hypotheses or derives from them (in the goal, condition 3 forces ). Every cardinality is cast to before division or subtraction, and under condition 3, so no division by zero occurs.
The goal is posed as an implication for every allocation satisfying conditions 1–3, rather than as the paper's "there exists an allocation"; the paper's proof of the MMS bullet uses only those three conditions, and existence is Theorem 8. The Nash-social-welfare bullet of Theorem 14 is not posed: it depends on Lemma 12, which takes the allocation of an earlier paper as a black box. The goal cannot be trivialized by a free pool, by overlapping bundles, by zero agents (condition 3 excludes them), by a junk maximin share over zero bundles, or by natural-number division; the statement keeps all three conditions, each of which is needed.
Contributions welcome: a library-quality maximin-share API for additive valuations (attainment of the maximum, monotonicity, the proportional bound), which is reusable for other MMS results; proofs of the milestones; and the final assembly.
An associahedron is a polytope whose vertices represent triangulations of a convex polygon and whose edges represent flips between triangulations. The same combinatorial polytope can be realized in different vector spaces with different facet directions. This matters when a construction uses the geometry of the realization, rather than only its face lattice: a linear change of coordinates can preserve its normal fan, while a general combinatorial relabelling need not. Ceballos, Santos and Ziegler compare three constructions and use parallel facets to distinguish them.
Two of those constructions form large families. Hohlweg–Lange choose a word of signs; Santos chooses a triangulation as a seed. Both yield associahedra, and both include the Chapoton–Fomin–Zelevinsky (CFZ) realization. The paper proves that CFZ is their only shared normal-isomorphism class. Its Theorem 6.1 is the target here; the result was announced as Theorem 1.1 in the introduction. Source, pp. 4 and 28.
Fix and a convex polygon with cyclically ordered vertices. A diagonal joins two nonadjacent vertices. Two diagonals cross when their endpoints alternate around the boundary. A triangulation is a maximal collection of pairwise noncrossing diagonals. Every triangulation has diagonals, and replacing one diagonal with the other diagonal of the quadrilateral it borders is a flip. The faces of an associahedron correspond to noncrossing sets of diagonals, while its vertices correspond to triangulations. Source, pp. 5 and 18–19.
A normal fan records the outward normal directions of all faces of a polytope and the cones they span. Two complete fans are linearly isomorphic when a real linear equivalence sends every cone of the first to a cone of the second. Polytopes are normally isomorphic when their normal fans are linearly isomorphic. This is Definition 2.1 of the paper; the comparison is geometric because it requires a linear map. Source, p. 5.
For the Hohlweg–Lange family, choose a sign word and extend it to on the labels . The negative labels, in increasing order, form one boundary chain; the positive labels, in decreasing order, form the other. For a diagonal with endpoint labels , let contain the labels strictly below it. Form by replacing with and with if those labels occur in . The characteristic vector of , considered modulo the all-ones vector, gives its facet normal. Source, pp. 14–16, Definition 4.1.
For the Santos family, choose a seed triangulation and use one basis vector for each seed diagonal . The normal assigned to a diagonal is when . Otherwise it is the sum of over seed diagonals crossing . The cones spanned by compatible diagonal vectors give the fan. The distinguished snake seed joins alternating polygon positions ; this seed gives the CFZ fan. Source, pp. 13 and 18–19.
Let and be the two normal fans, and let be the fixed snake. If is a triangulation, the target says
and it also asserts that . Together these are the uniqueness and existence parts of Theorem 6.1. The result covers dimensions zero and one as well as higher dimensions; Lemma 2.2 uses only for its second sentence, the uniqueness of the inducing symmetry. Source, pp. 6, 16 and 28–29.
The milestone list follows the paper's stated intermediate results: polygon symmetries of the associahedron, the parallel-facet pairs in each family, and the three properties of triangles in the seed that force the snake. Proposition 4.4 supplies the alternating-sign realization used for existence. The parallel-pair targets retain the source's exact count of pairs, through their characterization by the seed flips or the labelled quadrilaterals. Source, pp. 6, 16–17, 23 and 28–29.
Theorem 6.1 gives a complete answer to a comparison question that face-lattice data alone cannot settle: every member of either family has the same associahedral combinatorics, but almost no cross-family pair has linearly equivalent normal fans. It identifies the exceptional class without fixing coordinates for either construction. The characterization of parallel facets also gives a concrete invariant for later comparisons among associahedron realizations. Source, pp. 23 and 27–28.
The paper proves the result mathematically. A complete Lean development would add machine-checked definitions of the two ray systems and a proof of the classification, including the geometric step that a linear fan isomorphism induces a compatible correspondence of facet rays. The polygon triangulation and crossing definitions are already available as a published reusable component; proofs about fans and the two constructions are the remaining work.
An isomorphism of abstract face lattices gives too little information: it exists between all associahedra of the same dimension. The useful comparison must control a linear map on the actual normal vectors. The first obstacle is proving that such a map preserves the rays and therefore preserves which facets are parallel. Then the two explicit descriptions of parallel pairs must be reconciled, and the resulting sign restriction on a triangulation must force alternating turns of its dual path. Showing only that the dual tree is a path is insufficient; path triangulations can make consecutive turns on the same side. Source, pp. 17, 23 and 28–29.
Vertices are Fin (n+3) in counterclockwise positions, with zero-based indexing; Hohlweg–Lange signs apply to labels carried by those positions. Diagonals are unordered pairs. The imported Chvátal triangulation definition gives boundary edges, crossings, maximal noncrossing sets, and their triangles. A cone is the nonnegative span of the vectors assigned to a noncrossing set. The type I vectors are represented in using quotient coordinates ; type II vectors are functions on the seed diagonals. Hohlweg–Lange Proposition 4.3, cited in the paper, identifies the maximal cones of the type I normal fan with triangulations. Source, pp. 15–16.
Normal isomorphism uses a real linear equivalence, dihedral symmetry uses only rotations and reflections of the polygon, and the snake is the explicit alternating triangulation. The cones use the actual facet vectors. These commitments exclude a mere bijection of index sets, an arbitrary permutation of vertices, and a path triangulation with nonalternating turns. The condition appears only where the page has it, in the second sentence of Lemma 2.2 (uniqueness of the inducing symmetry); facet-normal comparisons quantify only over diagonals, exactly the facets represented in the paper. Reusable contributions include combinatorial flip lemmas, linear independence of triangulation rays, and general results about linear maps of simplicial fans.
Two-sided intermediaries charge buyers and pay sellers while trying to match the two groups. A larger arrival stream on one side changes both the number of possible matches and the prices that clear the market. Chen and Hu study this in a model of buyers and sellers who arrive over time and may wait before requesting a match. Their market-size theorem concerns the deterministic fluid benchmark used to choose fixed prices for the dynamic system. This mission formalizes that theorem from the submitted manuscript, main text §6, rather than the performance of the waiting-adjusted policy itself.
The fluid benchmark matters because it supplies an interpretable price and quantity for each pair of arrival rates. When buyers become more numerous, the model predicts that both the buyer price and the seller payment rise. When sellers become more numerous, both prices fall. In either direction, more arrivals raise the maximum matching quantity and the fluid profit. These claims concern the same valuation and cost distributions as the rates vary, so they isolate the effect of market size.
Buyer valuations lie in , with density and distribution function . Seller costs lie in , with density and distribution function . Write . Buyer and seller arrival rates are and , and the horizon has length . A buyer accepts a fixed ask price when the valuation is at least ; a seller accepts a fixed bid price when the cost is at most . Thus and are the corresponding acceptance rates.
The buyer virtual value is , and the seller virtual cost is . Assumptions 1 and 2 of the manuscript say these functions are weakly increasing on their respective supports. The supports overlap in the sense . The density assumptions ensure that the survival and cost distribution functions have inverse quantiles on . For a candidate volume , the virtual surplus is
The optimal fluid matching quantity is the largest in for which . The corresponding fixed prices are and .
The fluid program (D) permits any measurable nonnegative ask and bid price path on that clears the market at every time: . Its value is the supremum of buyer revenue minus seller payments, integrated over the horizon. Proposition 1 states that the constant path attains this value and that .
The goal is Theorem 3, the eight weak comparisons of prices, volume, and fluid profit. For with fixed, it asserts
For with fixed, the two price inequalities reverse while the volume and profit inequalities retain their directions. The goal leaves the rates and the two distributions as variables, so it states the market-size result across all systems meeting the paper's assumptions.
The milestones follow the source's dependency structure: Proposition 1 identifies the fluid optimizer; the proof of Lemma S.5 notes that decreases in ; Lemma S.5 establishes the volume and profit comparisons; and the two parts of the proof of Theorem 3 compare the fractions and served on the growing side. The paper's proofs are in the Supplemental Note, with related proofs in the Online Appendix.
The theorem gives directional predictions without differentiating optimal prices with respect to arrival rates. A platform comparing two otherwise identical markets can infer which way its fluid ask and bid prices move, whether it matches more units, and whether the benchmark profit increases. Proposition 1 also connects the optimization over time-varying paths to a fixed price pair, so the static claims apply to the entire feasible fluid program.
The result is proved in the manuscript; this mission asks for a machine-checked proof of the same statement. The formal development would make the inverse-quantile construction, attainment of the optimal volume, and the nonempty bounded fluid optimization problem explicit. Those objects can be reused in other two-sided pricing or matching models. This mission does not claim that the corresponding stochastic system has identical comparative statics; the manuscript itself focuses on the fluid regime in §6.
Increasing one arrival rate expands the feasible number of matches, but the two optimal prices do not follow from that fact alone. The buyer price depends on the fraction of buyers served, and the seller price depends on the fraction of sellers served. A growing side can have a larger matched volume yet a smaller matched fraction. The proof must control both quantities under the appropriate inverse distribution function. Profit also needs a comparison of two separate fluid optimization problems, rather than only a comparison of their candidate fixed-price formulas.
The Lean model reuses the published bilateral-trade environment for the two positive densities, interval supports, cumulative distributions, and virtual values. The new definitions clamp both cumulative distributions to their supports so a price outside the support still has the correct acceptance probability. Inverse quantiles are supported level-set infima, used only at arguments in . All rates and the horizon are positive; both densities are continuous on their supports; the virtual functions satisfy the paper's regularity assumptions; and . Density continuity is a disclosed addition needed for the asserted inverse-quantile and maximum properties.
The claims involving the value of (D) assume a nonnegative seller cost support. This disclosed domain correction puts the fixed seller price in (D), whose price paths take values in ; the imported bilateral-trade environment itself permits negative supports. The virtual-surplus and served-fraction inequalities hold without this condition. Every feasible path is measurable, nonnegative on , clears the market at every point of that interval, and has integrable buyer and seller revenue terms. The fluid value is defined as the supremum over those paths. It is never defined by Proposition 1's fixed-price identity, which would erase the optimization claim. The volume set is restricted to , so its supremum has the source's intended domain. The source uses “increasing” and “decreasing” in the weak sense.
Useful contributions include lemmas showing the clamped distributions are monotone, their supported inverses have the stated identities, the candidate volume set has a greatest member, the fluid feasible set is nonempty and bounded above, and the two fraction comparisons. These are substantive mathematical obligations: no arbitrary inverse, empty feasible set, non-integrable path, or preassigned fluid value should satisfy the goal by a default value.
The quantum linear systems problem asks, given a sparse Hermitian matrix with condition number and a procedure preparing a state , to prepare a state close to . Harrow, Hassidim and Lloyd (2009) gave a quantum algorithm whose running time is polynomial in and but grows like in the target precision , because it estimates eigenvalues by phase estimation. Childs, Kothari and Somma (arXiv:1511.02306, SIAM J. Comput. 46(6), 2017) reduced the precision dependence to , an exponential improvement.
The reduction has two parts. A quantum part implements a linear combination of unitaries applied to , and turns any function that is -close to on the spectrum of into an approximate preparation of the solution state (Corollary 10 and Proposition 9 of the paper). An analytic part supplies such a function with small degree and small coefficient weight. The paper gives two analytic constructions: a Fourier expansion (Section 3) and an expansion in Chebyshev polynomials (Section 4). This mission formalizes the analytic core of the Chebyshev construction, the input to the paper's Theorem 4. The quantum algorithms and their query and gate counts are not formalized here.
For a real number (a condition number: the ratio of the largest to the smallest singular value), the domain is
A function is -close to on a set if for all .
The Chebyshev polynomials of the first kind are , and ; those of the second kind satisfy the same recursion with , .
For natural numbers let
the probability of more than heads in fair coin flips. The tamed inverse (74) is , and the odd Chebyshev series is
In Lean these are Dκ, coeff b j, fTamed b, and chebSum b n in the namespace QuantumLinSys.Chebyshev; bOf κ ε and j0Of b ε are the parameters and below.
With and , the truncated series
is -close to on , for every and .
Two further statements of the same approach are included as companion theorems: Lemma 16 (p. 17), the closed form of the -th power of the rotation block in terms of and , and Proposition 9 (p. 9), the perturbation bound for normalized states.
Lemma 14 provides a polynomial of degree whose Chebyshev coefficients have total weight , approximating uniformly on the region where a well-conditioned matrix has its eigenvalues. Applied to a Hermitian matrix through a quantum walk, whose powers implement (Lemma 16), it gives the query complexity of Theorem 4. The same polynomial approximation of reappears in later work on quantum singular value transformation and matrix inversion.
All results of this mission are proved in the paper. None of them is machine-checked in Mathlib or on the platform, as far as a search found: Mathlib has the Chebyshev polynomials and the identity , but no Chebyshev expansion of a rational function, no binomial tail bound in this form, and no approximation theorem for . The formalization produces a checked uniform approximation of with explicit, non-asymptotic parameters.
The exact identity (Lemma 18) has no slack: every coefficient, sign and summation bound of (77) must be right for all , and an off-by-one in the inner sum or in the Chebyshev index makes it false. Mathlib's Chebyshev library offers evaluation facts but no expansion of a given polynomial in the Chebyshev basis. The bound (89) is a Chernoff–Hoeffding tail bound for a symmetric binomial distribution, which must be stated for sums of binomial coefficients rather than for random variables. The goal then needs both approximation errors at the page's specific parameters, including the corner cases in which or is negative.
All functions are real functions of one real variable. Chebyshev polynomials are Mathlib's Polynomial.Chebyshev.T ℝ and Polynomial.Chebyshev.U ℝ, indexed by integers. The sum is over Finset.range n, so the series of (55)/(88) truncated at is chebSum b (j₀ + 1) and the full series (77) is chebSum b b.
The formalization commits to the following conventions, each disclosed in the item it affects.
A trivializing reading is ruled out: the goal fixes the page's , and constant , so neither an arbitrarily large truncation nor a weaker constant satisfies it, and the domain excludes the origin, where Lean's would make closeness to meaningless.
Useful infrastructure, reusable beyond this mission: Chebyshev expansions of polynomials on , binomial tail bounds, and uniform approximation of . Contributions of general lemmas of this kind are welcome.
Mobile devices can divide work between local execution, a nearby shared cloudlet, and a remote cloud. A cloudlet has limited capacity, so one user's choice changes the delay faced by the others. Cardellini and coauthors model this as a generalized Nash equilibrium problem, in which each user's feasible choices depend on the aggregate cloudlet load. The shared utilization cap makes a direct distributed solution awkward: a user must know how much capacity all other users consume before choosing a feasible deviation. The paper therefore introduces an additional player who sets a cloudlet price. This mission formalizes the relationship between the original coupled game and that extended, ordinary Nash game Cardellini et al., accepted manuscript, pp. 10–16.
There are users and cloudlet servers. User chooses fractions , , and for local, cloudlet, and remote-cloud execution. These fractions are nonnegative and sum to one. At most a fraction can be offloaded, and a user-specific linear power constraint applies. The set contains these private feasible choices. The cloudlet load and the shared feasible set are
Each user's cost is the response-time expression on p. 10, with coefficients . The VI map is the stack of the user's partial gradients, written in closed form on p. 11. A variational solution belongs to and satisfies for every . The pairing sums all three coordinates for each user. Section 5 assumes and for every user; the model also has and Cardellini et al., pp. 7, 9–11.
The extended game replaces the joint cap in each user's feasible set by a price. User minimizes over . A cloudlet manager chooses to maximize . The manager's choice is part of the Nash equilibrium condition, not a preimposed complementary-slackness equation. The extended game's VI set is and its map is Cardellini et al., p. 15.
The goal is the two-part assertion of Theorem 2. Under the standing assumptions and a strict load bound on the full product of private feasible sets, its equilibrium characterization is
The same goal states that monotonicity of on implies monotonicity of on . The three milestones follow the paper's path: the extended Nash game is equivalent to its VI; the shared affine constraint has a scalar multiplier at a VI solution; and the price-load coupling cancels in the monotonicity pairing. The source states the first as a classical result and gives the last two in its proof Cardellini et al., pp. 15–16.
The characterization lets a variational solution of a game with coupled feasible sets be found as an equilibrium of a game whose users have separate feasible sets. The additional scalar has a concrete interpretation: it is the multiplier of the shared cloudlet-utilization cap. The monotonicity assertion connects the paper's analysis of the original VI to methods for the extended one. The paper uses this relationship as the entry point for its distributed algorithms in the next section Cardellini et al., pp. 16–17.
The result is proved in the paper but is not yet machine checked in this mission. A complete development would give reusable Lean interfaces for a finite-dimensional VI on an intersection of a product polytope and one affine half-space, a multiplier characterization for that intersection, and an equilibrium-to-VI conversion for separable player constraints. Those components could support other capacity-sharing games. The theorem drafts remain proof obligations; the definitions compile locally.
A Nash equilibrium requires each user to be optimal against every privately feasible deviation, including deviations that violate the original shared cap. Consequently, the user's cloudlet cost must remain well defined throughout for the equivalence to hold. A load bound only on does not cover those deviations. The multiplier comparison must also account for the manager's maximization condition and the sign of the load term in . For monotonicity, evaluates on the whole product , a larger domain than . These domain distinctions explain why the statement needs two explicit repairs to the printed theorem Cardellini et al., pp. 15–16.
Lean represents the users as Fin N and the three processing locations as a finite tier type. Indices therefore start at zero. The costs, the map , the private sets, , and are separate definitions. The Euclidean pairing is written as a finite sum; no Pi-type sup norm is used. The extended Nash predicate quantifies over user deviations in and over every nonnegative manager price. The VI predicates are in their own module so the game is not built into their meaning. The theorem's statement remains meaningful at ; no positive-user hypothesis is added to Section 5's assumptions.
The first repair requires at every . The paper's Theorem 1 condition (18) implies this bound, but is stronger than needed. Without the bound, a private deviation can cross the pole of ; Lean's total division then assigns a value at a zero denominator even though the paper's cost has none. In a two-user instance with , and , the pole can lie within one user's private feasible interval. The second repair reads “the original game is monotone” on , because that is precisely the -domain of . Monotonicity on alone is insufficient. Both repairs are disclosed in the item notes, and the source wording remains visible in the milestone quotations.
An empty would make a solution statement vacuous; the formal development should retain concrete feasible parameter instances. The map is the paper's displayed formula, rather than a derivative chosen to make a milestone tautological. The VI uses all user coordinates, and the extended game does not silently reinstate the shared constraint in user deviations. Contributions toward the stated multiplier theorem, Nash-to-VI equivalence, and the cancellation identity are welcome, along with reusable finite-dimensional convex-analysis lemmas.
Firms increasingly account for, and offset, the greenhouse-gas emissions of their entire supply chain, not only their own operations. Emissions in a supply chain are often jointly produced: the footprint of one process (transport, packaging, a molten-bulk delivery) depends on the abatement efforts of several firms at once. When each firm is charged for "its" emissions, the question is how to allocate the footprint of a jointly produced process so that every firm has the right incentive to abate.
Caro, Corbett, Tan and Zuidwijk (working paper, 2012; published in Manufacturing & Service Operations Management 15(4), 2013) model this as a moral-hazard problem in teams. Their §4 shows that a social planner who wants the first-best efforts must, under joint production, double-count emissions: the marginal payments across firms for one process exceed the carbon price. This mission formalizes §5, which looks at a different institutional arrangement observed in practice. One firm, the carbon leader (the paper's example is the cosmetics company Natura), voluntarily pays for all supply-chain emissions at a carbon price and compensates the other firms to induce abatement.
Timeline. Holmström (1982) showed that a budget-balanced sharing rule cannot implement efficient efforts in a team. Strausz (1999) showed that sequential moves can restore efficiency. Battaglini (2006) studied joint production with multidimensional output. Caro et al. (2012) placed the carbon leader in this line: a Stackelberg leader whose commitment plays the role of Strausz's sequential structure.
There are finite sets of firms and processes . Firm chooses efforts , one for each of its abatement actions, and the effort profile lies in the box . Firm earns profit , which is differentiable, concave and componentwise decreasing: effort is costly. Process emits , which is differentiable, convex and componentwise decreasing on the box. The influence matrix has if firm influences process , that is, if , and otherwise.
The first best at carbon price maximizes the social value over the box. At the societal cost its maximizer is , assumed unique.
The carbon leader is a firm , written L in Lean. Every other firm has a reservation profit . The signed transfer is recorded as a payment by firm ; a negative value means compensation from the leader. The leader faces two problems.
Let be optimal for and define, for ,
Then is feasible for , its value equals , and every feasible solution of has value at most :
If , each is supermodular and each is submodular, then componentwise.
The result. Proposition 5 says that, when efforts are unobservable, a carbon leader that can commit loses nothing compared with contracting on efforts. A linear rule, the form footprint accounting already takes in practice, achieves the benchmark. The rule charges each firm the full price on every footprint it influences, so emissions are double-counted internally, yet the supply chain as a whole pays for carbon once. This is how the paper reconciles its §4 impossibility (a planner must double-count) with a footprint-balanced scheme: the leader moves first and is excluded from the incentive constraints. Lemma 6 then says that a leader paying a price below the societal cost induces weakly less effort than the first best.
Formalizing it. Both results are proved in the paper. As far as the platform's catalog shows, neither is machine-checked anywhere. The proof of Proposition 5 combines a reduction of a bilevel problem with a first-order argument for concave games on a box. The appendix compresses these into three sentences, one of which contains a misprint ("since f is concave" for convex). Formalizing it makes the leader–follower conventions explicit: the leader's tie-breaking choice of follower efforts, and the unilateral deviation in (11).
The paper calls a constrained version of , but their feasible sets are not literally nested: 's payments are functions of the emission vector and 's of a firm's own effort. Establishing the common upper bound therefore requires care with the two payment domains and the participation constraint (10).
The incentive compatibility of (12) is the substantive step. It is a global best-response claim on a closed effort box, while the appendix states only a first-order identity at an interior point. The influence indicator also has to agree with every action-level derivative, rather than only their sum. For Lemma 6, the optimum at price need not be unique.
e : (n : ι) → act n → ℝ, and a unilateral deviation is Function.update.deriv along one coordinate. Every theorem that uses one assumes differentiability.sSup. is the objective at an optimal pair.Rule (12) is a function of the emission vector only, and the deviation in (11) moves only firm 's efforts. A formalization in which payments may depend on efforts, or in which a deviation also moves the leader, would make the goal trivial and is ruled out. A sorry-free instance with two firms checks that every hypothesis of the goal can be satisfied. Supermodularity reuses the published Supermodularity.Monotonicity.SupermodularOn. All other definitions live in CarbonDoubleCount.Leader.Setting.
Proofs of the milestones, or alternative routes such as a Lagrangian argument for incentive compatibility, are welcome. A general lemma that a concave differentiable function on a box is maximized at an interior stationary point would be reusable beyond this mission.
Mode-seeking clustering groups data points by the peak of an underlying probability density that they "flow up" to. Methods of this kind (mean-shift, graph-based hill climbing) are widely used, but their output depends heavily on noise: a density estimated from finitely many samples has many spurious local maxima, and each of them becomes a cluster. Chazal, Guibas, Oudot and Skraba (INRIA RR-6968, 2009; journal version J. ACM 60(6), 2013, doi:10.1145/2535927) combine graph-based hill climbing with topological persistence. Persistence measures how prominent each peak is, and peaks of low prominence are merged into their neighbours. The paper's main guarantee says when this algorithm recovers the right number of clusters from random samples. It holds on Riemannian manifolds that may be non-compact, and the clustering method is now known as ToMATo.
Let be an -dimensional Riemannian manifold, possibly with boundary, with geodesic distance and -dimensional Hausdorff measure . The strong convexity radius is the infimum over of the largest such that any two points of the closed ball are joined by a unique shortest path, and that path stays in the ball. Let be a probability density with respect to that is -Lipschitz, and write for its superlevel sets.
Persistence diagram. As decreases from to , path components of are born at peaks of and die when they merge into an older component. The 0-th persistence diagram records each component as a point of the extended plane , with birth and death ; a component that never dies has . The prominence of the peak is . The diagonal is added with infinite multiplicity. is tame when this structure is of finite type. For , is -separated when every off-diagonal point either has prominence (noise), or has prominence and birth (signal).
Algorithm. The input is sample points , the values , the matrix of distances and parameters . The Rips graph joins two points at distance . The algorithm processes the points by decreasing and keeps a union-find structure whose entries are rooted at their highest point. When a point is processed, every neighbouring entry whose root is less than higher than the point is merged into the point's entry. The point's own entry is then merged into the neighbouring entry with the highest root, if its own root is less than higher than the point. The output is the set of final entries whose root has value .
Sampling quantities. is the least number of closed geodesic balls of radius covering , and .
Assume , is a tame -Lipschitz density, is -separated, and . Then for i.i.d. samples from ,
The theorem gives a sample-complexity guarantee for a practical clustering algorithm, with an explicit failure probability. It needs neither compactness of the manifold nor a density bounded away from zero; dense sampling of one superlevel set is enough. The separation hypothesis is a signal-to-noise condition, and it tells the user which range of recovers the true number of clusters.
On the formalization side, the paper's results are proved on paper, but nothing about them is machine-checked. Of the steps, the paper proves Lemma 4.3 and the region analysis. Theorem 4.5 rests on the Rips-filtration analysis of Chazal–Guibas–Oudot–Skraba, SODA 2009, the interleaving and stability results of Chazal et al., SoCG 2009, and the paper's Lemma 4.6. The algorithm-output step (milestone 6) is asserted in the paper, not proved. The mission therefore asks for formal proofs of all six steps. A by-product is the first library of 0-dimensional persistence diagrams, multi-bijections and Rips filtrations on the platform.
The probabilistic step is a union bound over a minimal cover, but it has a gap. Covering balls need not be centred in , while is an infimum over balls centred in , so the comparison between the two is not justified on a general manifold. Theorem 4.5 is the hardest step. The obvious route, a bottleneck stability theorem, does not apply, because the sample covers only one superlevel set and not . This is why the conclusion distinguishes the quadrant above , where both coordinates are controlled, from the quadrant below, where only births are. Milestone 6 is a correctness proof for a union-find procedure with ties: entries are not path components, because prominent entries stay separate after their components meet.
IsRiemannianManifold, a ModelWithCorners for the boundary), so is dist.Fin n → X. "With probability at least " is an upper bound on the outer measure of the failure event. uses and .No formalization in which the number of clusters is defined as a count of diagram points, or in which the diagram is a free parameter, is acceptable: either one empties the goal. The running-time and memory claims of §3, the basin approximation of Theorem 4.9 and the Morse-theoretic material of §2.3 are out of scope. Lemma 4.3 is stated as printed, with covering balls centred anywhere, and its proof gap is an open risk that Theorem 4.8 inherits.
Contributions are welcome on every milestone. The persistence-diagram layer (rank functions, multiplicities, multi-bijections) and the union-find correctness proof are reusable beyond this mission.
Allocating indivisible goods fairly is difficult because a single good can change how an agent compares two bundles. Exact envy-freeness can be impossible (one good, two agents), so the field works with relaxations. Envy-freeness up to any good (EFX) requires each agent to prefer her own bundle to every other agent's bundle after any one good of that other bundle is removed. Whether EFX allocations of all goods always exist is open; the question motivates weakening the requirement that every good be assigned, and asking how little must be left over. Chaudhury, Kavitha, Mehlhorn and Sgouritsa show that leaving a small, unenvied set of goods unallocated (donated to "charity") suffices for every normalized monotone valuation profile (arXiv:1907.04596v3, Theorem 8, pp. 11–12).
Timeline (as recounted on pp. 2–3 of the source):
The two bounds matter separately. The empty allocation is EFX and donates everything; a cardinality bound alone still lets the donated goods carry most of an agent's value; the value bound alone allows almost all goods to be donated. The paper's later maximin-share and groupwise-maximin-share guarantees (Theorems 14 and 16, treated in the next missions of this series) are derived from exactly the allocation produced here.
There are agents, indexed by in the paper, and a finite set of indivisible goods. Agent has a valuation . It is normalized if and monotone if implies . No additivity, submodularity or substitutes condition is assumed. These are the general valuations of §1.1.1, p. 3, and §2 of the source.
A partial allocation consists of pairwise disjoint bundles . Its pool is the goods not assigned to anyone,
The allocation is EFX when
The paper calls allocations partial by default (p. 3, footnote 5). The envy graph has the agents as vertices and an edge when . A source is a vertex with no incoming edge. Its reachability component includes itself. The social welfare of is . These notions are introduced on pp. 8–9 of the source.
For a set of goods, an envied set is one some agent values more than her own bundle. An inclusion-wise minimal envied subset is envied, but no strict subset of is envied by anyone. An agent who envies such a is a most envious agent of ; the paper allows ties. The three update rules U0, U1 and U2 use these sets to change an allocation while maintaining EFX (Definition 3 and Algorithm 2, p. 9).
The goal is the allocation guarantee of Theorem 8:
Both the stronger source-count bound and its consequence are stated. The theorem asserts existence for every normalized, monotone valuation profile, including nonadditive profiles. It does not require the returned envy graph to be acyclic; acyclicity is an invariant used during construction, rather than an additional advertised property of the final allocation.
The attack path consists of the paper's numbered Lemmas 2, 4, 5, 6 and 7. Lemma 2 concerns removal of envy cycles; its Lean form keeps the page's conditional "if is EFX then is EFX" and the unconditional strict welfare increase. Lemma 4 records what U0 does and what its failure implies. Lemma 5 records U1's welfare and EFX guarantees. Lemma 6 supplies the finite source, good and agent data required for U2. Lemma 7 states U2's welfare and EFX guarantees. Their source wording and page locations appear in the milestone list; the Lean statements include the exact allocation updates where those lemmas rely on them.
The theorem guarantees a partial EFX allocation even for general monotone valuations, while limiting the unallocated pool more tightly than the number of agents: its size is below the number of unenvied agents. Every agent also values that entire pool no more than her own bundle. These two bounds distinguish the allocation from a merely EFX partial allocation. They provide the starting point for the paper's later statements on approximate maximin shares under additive valuations (Theorems 14 and 16).
The mathematical result is proved in the paper. The mission asks for a machine-checked proof of its allocation guarantee and of the supporting lemmas, with a reusable Lean account of finite partial allocations, the unallocated pool, envy graphs, minimal envied subsets and the update rules. Such definitions are useful for other fair-division questions involving unallocated indivisible goods.
EFX must hold after the allocation is changed, for every agent pair and for removal of every good from the other agent's new bundle. Simply giving a pool good to an agent may violate that condition, even though it makes the pool smaller. Conversely, replacing a bundle with an envied subset can improve welfare while returning goods to the pool. The source-count bound depends on controlling both kinds of progress. Rule U2 adds a further complication: its bundle moves follow envy paths, so an overlap between selected paths would make the new allocation ambiguous. These are the points at which the straightforward approach of distributing the remaining goods one at a time stops working.
Lean represents agents by Fin n, goods by Fin m, bundles by finite sets of goods, and valuations by real-valued functions on bundles. The paper's one-based subscripts become zero-based Lean indices. Nonnegative values need no separate hypothesis: normalization and monotonicity imply them. The hypothesis is explicit because the paper presumes agents and the strict bound is false when . The pool is computed as the complement of the union of pairwise disjoint assigned bundles. It is never a free set. EFX ranges over every pair , including , and every good of .
The minimal-envied-subset definition checks every strict subset against every agent. The most envious agent is a relation, allowing the paper's arbitrary tie choice. Reachability includes a path of length zero. U2's new allocation is calculated from its paths and chosen subsets. Lemma 6 includes Algorithm 1's acyclic-graph invariant and the ordering property established in its proof. It replaces the printed threshold with , the exact number of fresh goods its construction needs and the threshold used by the goal. Lemma 7 takes that ordering property to make path assignments unambiguous.
The printed U2 pool expression in Algorithm 2, line 13, is malformed; the formal statement uses the pool of the constructed allocation and the corrected union of leftover goods. Theorem 8's final sentence also asserts an iteration bound. This mission poses the allocation conclusions, while a future run-level formalization would be needed to state and check the iteration count. The paper's preceding count of U1/U2 steps and successive U0 steps does not by itself imply the printed number. Definitions and the numbered lemma statements are welcome contributions; a purported proof that uses a free empty pool, overlapping bundles, zero agents or an arbitrary replacement allocation would not establish this target.
Many graph classes are defined by excluding a fixed graph as a minor. A minor can be formed by deleting vertices, deleting edges, and contracting edges. Planar graphs, for example, exclude as a minor. Édouard Bonnet, Eun Jung Kim, Stéphan Thomassé, and Rémi Watrigant proved that every class excluding a fixed clique minor has bounded twin-width, a graph parameter that controls how much adjacency information is lost while vertices are successively combined. Their result connects a classical graph-minor restriction with the contraction parameter used in their first-order model-checking framework. The explicit bound is very large, but it establishes that the width depends only on the excluded clique size, rather than on the graph's number of vertices. Bonnet et al., Twin-width I, Theorem 6.3.
Let be a finite simple graph. A partition of its vertices is a collection of nonempty, disjoint parts covering all vertices. Two distinct parts are homogeneous if every vertex pair across them is adjacent, or every such pair is nonadjacent. Otherwise the pair of parts is marked red. A -partition has at most red neighbours at every part. A contraction sequence begins with singleton parts, merges two parts at each step, and finishes with at most one part. The statement says that such a sequence exists with every intermediate partition a -partition. This partition formulation is equivalent to the paper's original description in terms of trigraph contractions. Bonnet et al., pp. 3:11–3:12, 3:32.
Write for the complete graph on vertices. The graph is -minor free when cannot be obtained from by the minor operations above. The Lean statement uses a branch-set formulation: a minor model consists of disjoint, nonempty, connected vertex sets, with a connecting edge for each edge of the minor. Bonnet et al., p. 3:9.
An ordering of the vertices gives a Boolean adjacency matrix , with entry at an edge and otherwise. A division cuts its rows and columns into nonempty consecutive intervals. A zone is mixed if it is neither constant down its columns nor constant across its rows. A -mixed minor is a division with row intervals and column intervals in which every zone is mixed; a -grid minor requires a in every zone. A matrix is -mixed free or -grid free if the corresponding minor does not exist. A mixed Boolean zone always contains a , so grid freeness implies mixed freeness. Bonnet et al., pp. 3:18–3:19.
The order used in the proof is a depth-first search (DFS). A discovery order lists the vertices; at each time the active vertex is the lastly discovered vertex that still has an undiscovered neighbour, and the next vertex is a neighbour of the active vertex, which becomes its parent in the DFS tree . The Lex-DFS breaks ties: among the connected components of the undiscovered vertices that meet the active vertex's neighbourhood, it enters one whose word (the vector recording which discovered vertices have a neighbour in the component) is lexicographically largest. The proof also uses minimal subtrees of : the union of the tree paths between the vertices of a set. Bonnet et al., pp. 3:26–3:27.
The main target is the explicit excluded-clique-minor bound. With
the goal says
The in follows the value defined and used in the proof of Theorem 6.3 on p. 3:26; the printed theorem statement has . The formal target uses the proof-supported bound and records the printed statement verbatim in its provenance. It does not assert the paper's asymptotic triple-exponential notation as a separate theorem. Bonnet et al., pp. 3:26–3:29.
The milestones follow the proof in order:
The Helly theorem is a reference to an existing open platform statement rather than a duplicate draft. Bonnet et al., pp. 3:22–3:29.
The theorem supplies a uniform contraction-width bound for every fixed excluded clique minor. In particular, the paper applies it to planar graphs through exclusion of . Its numerical value is far from small; the article remarks that the planar specialization has billions of digits. Without the result, excluding a clique minor alone would not yield the particular twin-width certificate required for those applications. Bonnet et al., p. 3:29.
The mathematical result is proved in the cited paper. This mission asks for machine-checked statements and, eventually, proofs of its graph and matrix claims. The reusable output includes a precise partition model of graph twin-width, interval-division models of mixed and grid minors, and a graph statement that converts a mixed-free adjacency order into a contraction-width bound. No machine-checked proof of these new target items is claimed here.
A dense pattern of nonzero matrix zones does not directly give a graph minor. A matrix zone merely contains an edge somewhere between two vertex blocks. Those blocks need not induce connected subgraphs, and contracting them as if they were connected would use operations unavailable to graph minors. The proof also needs a vertex order with strong enough structure to control how the relevant connected sets overlap. These are the points that separate the grid-free milestone from a direct application of the matrix grid theorem. Bonnet et al., pp. 3:26–3:29.
The conversion from a mixed-free adjacency matrix to graph twin-width has a second issue: matrix twin-width permits separate row and column contractions, while a graph contraction merges one vertex partition and must keep the two matrix axes synchronized. Theorem 5.8 addresses the graph case. The milestone uses the explicit constant that the paper applies at the end of Theorem 6.3, while the printed Theorem 5.8 states an asymptotic bound. Bonnet et al., pp. 3:22–3:23, 3:29.
Graphs are finite simple graphs, and twin-width and the number of division parts are natural numbers. The real constants and are compared with natural-number twin-width through ; the explicit value is positive. Vertex orders are equivalences with . Matrix divisions use strictly increasing cut points, so every part is a nonempty consecutive interval. The adjacency matrix has a zero diagonal because simple graphs have no loops. The graph-minor predicate and the subtree representation come from existing published definitions with the same conventions; graph twin-width and the matrix objects are local draft definitions shared across this mission. Bonnet et al., pp. 3:9, 3:12, 3:17–3:19.
The grid-free milestone holds for every Lex-DFS order, as in the paper, and the existence of such an order is a separate milestone. Lemmas 6.4–6.6 are stated in the proof's context: a DFS, and vertices , and blocks with exactly the order and adjacency properties the page uses. Lemma 6.5 is posed for every block except the last. As printed it also covers the last block , and for that block it can fail. A five-vertex example satisfies every hypothesis of the lemma and violates the printed conclusion; it is checked in Lean in the sanity file, and the formal item records the change. The theorem's bound is uniform over all finite graphs on the excluded-minor hypothesis. A twin-width definition using an unrestricted real infimum, a sequence that skips directly to one part, red degree counted over homogeneous pairs, or a grid minor over arbitrary noninterval partitions would change the claim. Components and empty graphs use the endpoint conventions stated above. The hypothesis in the graph conversion milestone rules out the degenerate zero-division case.
Contributions toward the core grid-free order claim, the symmetric contraction bridge, the component theorem, and the reusable minor and division lemmas are within scope. The running-time claims elsewhere in the paper and the pointer construction and the two -minor constructions inside the proof of Theorem 6.3 are not separate milestones: they are unnumbered and their statements need the pointers. They remain part of the grid-free milestone.