Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
Graph neural networks (GNNs) compute representations of nodes and whole graphs by repeatedly combining each node's state with information from its neighbours. Soon after they became a standard tool, the question arose of what they cannot do. A natural test case is graph isomorphism: given two graphs that are not isomorphic, can the network attach different representations to them? If it cannot, it is hopeless on any task that needs to tell the two graphs apart.
The yardstick for this question is the Weisfeiler–Lehman (WL) test (Weisfeiler and Leman, 1968), a colour-refinement procedure that is a necessary condition for isomorphism. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2) reports, in its historical chapter (Ch. 7, p. 120), the conclusion of Morris et al. (2019) and Xu et al. (2019): any GNN of the three flavours of §5.3 "cannot be more powerful than the WL test". This mission formalizes that claim, together with the surrounding remarks of the book that make it precise.
Timeline. 1968: Weisfeiler and Leman introduce the refinement. 2011: Shervashidze et al. use the WL iteration to build graph kernels. 2017: Gilmer et al. unify many architectures as message-passing neural networks. 2019: Morris et al. and Xu et al. independently prove that message-passing GNNs are bounded by 1-WL, and that injective aggregation attains the bound (the Graph Isomorphism Network). 2020: Corso et al. show that with continuous features injective aggregation needs several aggregators.
A graph has node set and a symmetric, loopless adjacency relation. The neighbourhood of a node is (eq. (11), p. 34); it does not contain .
The WL colour refinement on a featureless graph starts with the same colour for every node and sets
where is a multiset. Colours carry their full history, so colours of nodes of two different graphs can be compared directly. The colour histogram at round is the multiset . The WL test declares two graphs indistinguishable when their histograms agree at every round.
A message-passing layer (eq. (35), p. 79) has a message function , a permutation-invariant aggregator and an update , and updates node features by
A GNN starts from a constant feature and applies layers , with parameters shared by all graphs. Its graph-level output after rounds is a read-out of the multiset .
For every GNN, read-out, depth and pair of graphs , (of possibly different sizes):
The statement fixes no architecture and no feature space: it quantifies over all message, aggregation, update and read-out functions.
If every layer's update is injective, then equal features are exactly equal WL colours (Xu et al.).
The result. The bound says that a GNN's ability to separate graphs is capped by a cheap combinatorial procedure. Every pair of non-isomorphic graphs that WL fails to separate — all regular graphs of the same degree and size, such as and — is also inseparable by every message-passing GNN, whatever its width, depth or training. This limitation motivated the higher-order and subgraph-based architectures discussed later in Ch. 7. The companion result explains why architectures with injective (sum-type) aggregation, such as GIN, are the maximally expressive members of the class, and the max/mean example explains why common aggregators fall short of it.
Formalizing it. The results are proved on paper; to the knowledge of this mission none has a machine-checked proof. The formalization makes explicit what the informal statements leave open: that the comparison needs parameters shared across graphs, that it concerns featureless graphs, which flavour of layer is covered, and in what sense "equivalent to one step" holds. It reuses a published 1-WL colour refinement (WLIdentification), so the GNN results connect to the platform's existing WL statements.
The statements are close to their definitions, and the difficulty is in the bookkeeping rather than in an idea. The comparison is between two different graphs, whose node sets are different types, so the relation between features and colours has to be carried across graphs rather than within one; equalities of colour multisets over neighbourhoods have to become equalities of multisets of messages, and histograms of colours have to become multisets of features. The / example needs the colours of a regular graph at every round and a separate non-isomorphism argument. A tempting shortcut, defining the GNN's features to be the WL colours, proves nothing: the goal quantifies over all GNNs.
Graphs are the published OAI.WLIdentification.Graph (order , Boolean symmetric loopless adjacency on Fin n); the WL test is its neighborColor and neighborHistogram, featureless and with history-carrying colours. The book numbers no theorems, so every item is cited by section, equation and printed page.
Conventions committed to:
Infrastructure needed is light: multiset bijections along equal maps (Multiset.map), induction over rounds, and finite computations on six-node graphs. The induction lemmas relating features to colours across two graphs are reusable for any further GNN-expressivity statement (higher-order WL, subgraph GNNs). Proofs of the milestones, of the companion, and alternative proofs of the goal through the companion are welcome.
A recurrent neural network (RNN) processes an ordered stream while retaining a summary of earlier inputs. The same update rule is applied at every time step, so it is natural to ask whether shifting the input stream simply shifts the resulting sequence of summaries. The answer depends on how the run begins. The first summary is supplied as an initial state, while the first input encountered after a shift can be different. Bronstein, Bruna, Cohen and Veličković use this boundary effect to explain a precise form of temporal translation equivariance for RNNs in §5.7 of Geometric Deep Learning (arXiv:2104.13478v2, pp. 90–93).
The claim matters when the same sequential model is applied to streams presented with different starting times. Without a specified boundary convention, the shared update rule alone does not guarantee that corresponding hidden states agree. The chapter's zero-padding construction makes that convention explicit. Its condition on the initial state can then be stated independently of a particular architecture or training procedure. The book numbers equations but no theorems or lemmas here; the mission's items are cited by section, equation, page, and, for a marginal statement, “side-note.”
Let be the input at time , let be its hidden summary, and let be a shared update map. Given a seed , equation (38) defines a run by
The first processed input is ; is unused. This is the book's time convention, including the named state (Bronstein et al., §5.7, p. 90, equation (38)). The update map is arbitrary: the results concern the recurrence itself, so they do not require the affine layer and activation used as one example in equation (39).
A left shift by steps replaces the input at time with the old input at time . A left-padded input of length is
Here is the zero vector in . The original input begins at time . The two runs being compared use the same update map and the same seed. This is the exact padding convention displayed on p. 93 of the book (Bronstein et al., §5.7, p. 93).
The capstone is the chapter's one-step equivariance claim. For every update map, input sequence, and seed fixed by the zero-input update, one or more zero-padding steps suffice:
The multi-step side note extends the conclusion to every with :
The milestone list also records the book's unpadded boundary counterexample and its observation that a contraction has a unique attracting fixed point. The latter is represented by an already proved, reusable Banach fixed-point theorem rather than a second draft of the same result (Bronstein et al., §5.7, pp. 92–93, equations (40)–(42) and side-note).
The equivariance theorem identifies a checkable condition under which the hidden-state sequence tracks a left-shifted input exactly, including at the first state. It also marks the limit of the informal idea that sharing the same update map across time automatically creates shift equivariance: the unpadded run can fail already at time . The fixed-point condition is therefore part of the mathematical claim, rather than an implementation preference (Bronstein et al., §5.7, pp. 92–93).
The RNN shift statements are targets for machine-checked proofs. The contraction milestone already has a machine-checked proof in the referenced CursoEDO.contraction_fixed_point theorem. A completed development would make the boundary convention and the arbitrary-update-map quantifiers available for later statements about sequential models. The recurrence and padding definitions are reusable whenever a discrete-time state update is compared before and after a shift.
The tempting comparison takes two runs that begin with the same seed, then tries to pair the shifted run's state at with the original run's state at . At the first step, those states have encountered different input histories. Equations (40)–(41) display the mismatch: the original run has applied to its first input, while the shifted run still uses the supplied seed at the corresponding update. For an arbitrary and arbitrary first input, the states need not agree (Bronstein et al., §5.7, p. 92). A shift statement that omits its padding length or seed condition would therefore assert something the chapter explicitly rejects.
Lean represents and as functions on Fin k and Fin m; time and padding lengths are natural numbers. The run uses and consumes at its next update. The padding function returns the zero vector through index and then the correspondingly indexed original input. These definitions cover every finite dimension, including zero-dimensional edge cases, while the unpadded counterexample uses one input and one hidden coordinate.
The target ranges over all update maps and all input sequences; it does not impose a special neural-network parameterization. The seed is any fixed point of , not necessarily the zero state, and the zero-input update need not be the identity map. The formal statements include time and the endpoint . No contraction assumption is needed for shift equivariance itself; contraction enters only the separate existence-and-convergence milestone. The contraction theorem is stated for a nonempty complete metric space, which includes the finite-dimensional real hidden-state spaces used here.
The work requires a small discrete recurrence interface, an exact padding definition, and proofs for the boundary counterexample and shift identities. Those two definitions and the shift results can also support variants with a nonzero padding vector. The LSTM equations of §5.8 have a separate gated state model and are outside this mission's formalization scope. Contributions that keep the full fixed-point hypothesis and the stated boundary cases are welcome.
Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.
This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.
Fix and the ring graph with nodes , arithmetic taken modulo . A signal is a vector with entries in a commutative ring , for instance .
In Lean the index set is ZMod n with [NeZero n], is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.
For every matrix over a commutative ring ,
The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.
With ,
The book prints this with in place of , which is off by a factor for ; the corrected identity is stated. The transform form of the Convolution Theorem, with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.
The goal identifies the space of linear translation-equivariant maps on with the convolutions, an -dimensional space parametrised by the filter . This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.
Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.
The direction "" is a one-line consequence of the commutativity of circulant matrices. The content is "": the equation is an equation between matrices, and it has to be turned into the statement that the entries of are constant along every cyclic diagonal, with the indices handled modulo . The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the -th roots of unity in which is invertible; over a general commutative ring, such as or , the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives used in the exponents and the arithmetic of .
ZMod n with [NeZero n], so and matrices are finite; no lower bound is needed (for , and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val , as on the page.Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on and that on does not commute with .ZMod.dft, and the factor is written out in its statement.No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.
IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778Classical Hamiltonian mechanics describes an observable by a function on a phase space. Its Poisson bracket gives observables a Lie algebra: the bracket is antisymmetric and satisfies the Jacobi identity. In multisymplectic geometry, a higher-degree differential form replaces the symplectic two-form, and the appropriate observables may themselves be differential forms. This occurs in the geometric description of classical field theories, where quantities associated with spatially extended objects are naturally expressed through forms rather than functions. Baez, Hoffnung and Rogers use this setting to examine the classical bosonic string in their paper, §§1 and 5.
The same paper shows why the usual Lie algebra of observables is too narrow for a 2-plectic space. One bracket of Hamiltonian one-forms satisfies the Jacobi identity but is antisymmetric only up to an exact form; another is antisymmetric but has a Jacobi identity only up to an exact form. Theorem 4.3 packages the first bracket and its exact correction into a hemistrict Lie 2-algebra. The result is known mathematically; the mission is to give its construction a machine-checked statement and proof in Lean for a finite-dimensional vector-space model Baez–Hoffnung–Rogers, §§3–4.
Let be a finite-dimensional real normed vector space. A 2-plectic form on is a smooth three-form with such that implies at each point. The interior product places in the first argument of the form. This is the case of Definition 2.1 in the preprint, p. 6.
A smooth one-form is Hamiltonian when a smooth vector field satisfies
Nondegeneracy makes unique. Write for the vector space of these forms. The hemi-bracket is , where is the Lie derivative. On functions its left and right actions are and . The alternator is the function . These formulas are Definitions 3.1 and 3.3 and the data preceding Theorem 4.3 on pp. 11 and 16–17.
A Lie 2-algebra here has a two-term chain complex , a bracket on its available degrees, an alternator witnessing antisymmetry up to chain homotopy, and a Jacobiator witnessing the Jacobi relation up to chain homotopy. Four further coherence diagrams constrain these homotopies. “Hemistrict” means that the Jacobiator is the identity homotopy, represented by the zero degree-one map Definitions 4.1–4.2, pp. 15–16.
For every 2-plectic , Theorem 4.3 constructs a hemistrict Lie 2-algebra with all components fixed:
The existential goal fixes the carriers and every operation; the Lie 2-algebra structure then requires the chain-map identities, the homotopy identities, and all four coherence equations. The milestones isolate the source statements that supply the main geometric identities: uniqueness of , Hamiltonian exact forms, Proposition 3.6, the bracket’s chain-map behavior, a mixed Jacobi identity, and the third coherence diagram Theorem 4.3 and its proof, pp. 17–18.
The theorem identifies the algebraic structure carried by 2-plectic observables. In particular, it retains the exact-form discrepancy in antisymmetry as an explicit operation instead of losing it by quotienting forms. The paper compares this hemistrict construction with a semistrict construction and then studies their relation; the present result is the first of those two constructions Theorems 4.3–4.6, pp. 17–19.
A formal proof would connect Mathlib’s exterior derivative on alternating forms to a reusable calculus of interior products, Lie derivatives, Hamiltonian vector fields, and higher algebraic coherence. The preprint already proves the theorem. The local proposal supplies statements for its finite-dimensional normed-space case; a proof in Lean and an extension from vector spaces to general smooth manifolds are further work. The current mission does not assert the separate semistrict theorem or the string application.
The obvious attempt to make Hamiltonian one-forms into a conventional Lie algebra fails: for the hemi-bracket, can be a nonzero exact form. The correction must also agree with the bracket on functions and with the Jacobi relation across degrees. A degree-zero calculation alone therefore does not establish a Lie 2-algebra. Its chain-map conditions and four coherence diagrams impose further identities involving the exterior derivative, Lie derivatives and the Hamiltonian vector fields Proposition 3.6 and Definition 4.1, pp. 12, 15–16.
Lean uses with NormedAddCommGroup, NormedSpace ℝ E and FiniteDimensional ℝ E, in place of the paper’s arbitrary smooth manifold . Forms, functions and vector fields are defined on all of , and smoothness means ContDiff ℝ smooth with smooth the degree. This is the disclosed scope cut. The Lean name for the paper’s is Ω; this avoids a notation conflict from the imported definition module.
Mathlib represents a -form as a function into a continuous alternating -linear map. Its extDeriv supplies the exterior derivative, while the published ContWeatherall.grad supplies for functions. Interior product inserts in the first slot. The Lie derivative of a one-form uses its derivative and the derivative of the vector field, so Cartan’s identity is a mathematical assertion rather than the definition of the Lie derivative. The bracket of vector fields uses . The two-term chain complex uses the paper’s ordinary graded tensor-product differential and signed switch. Every formal statement about hamVF restricts its form to Hamiltonian inputs, where nondegeneracy gives a unique vector field; the default value on other inputs has no role in the theorem.
The goal requires all operations to have the paper’s values and requires every Lie 2-algebra axiom. An arbitrary pre-existing Lie 2-algebra or a structure with unconstrained operations would not establish this result. Reusable contributions include differential-form identities and the algebraic two-term interface. The separate semi-bracket construction and general-manifold extension remain outside this proposal.
The extension problem for groups asks for a description of all groups that contain a given group as a normal subgroup with quotient isomorphic to a given group . Schreier (1926) answered it by showing that every such extension can be rebuilt from , and two maps: a map and a map , subject to two compatibility conditions. The group built from this data is the crossed product . When is abelian, this becomes the cohomological classification of extensions by ; for nonabelian it is the theory of Eilenberg and MacLane (1947).
The classical classification counts extensions up to isomorphisms that are the identity on and induce the identity on . Agore and Militaru (arXiv:0805.4077v2, 2008) also study a coarser notion, in which the isomorphism may act on and on by arbitrary automorphisms. The resulting classification, their Theorem 3.8, is the target of this mission. It is closer to the question "which groups arise as crossed products of and , up to isomorphisms respecting the extension structure", which is what is needed when listing groups of a given shape. The paper's applications include the description of all morphisms between two crossed products by explicit data.
Let and be groups. For a map write . A crossed system is a pair with such that, for all and ,
Then is called a weak action: it is a homomorphism only up to the inner automorphisms given by . The system is normalized if , and is the set of normalized crossed systems. The crossed product is the set with
which is a group exactly when is a crossed system.
The category has as its objects. A morphism is a triple of group morphisms , and such that and the -component of is .
Two normalized crossed systems are 2-equivalent, , if there are group automorphisms of and of and a map with
with the bijection sending the isomorphism class of to its -class. The statement holds for all groups , , finite or not, abelian or not.
The theorem replaces the categorical question "when are two crossed products isomorphic in " by an explicit system of equations in the data . For finite and the quotient is a finite, computable set, so the theorem turns the description of crossed products of by up to this isomorphism into a finite computation. The intermediate results are of independent use: Corollary 2.3 describes every group morphism between two crossed products, and Theorem 2.1 gives the two universal properties of the crossed product.
The results are proved in the paper. None of them has a machine-checked proof: Mathlib has GroupExtension and its equivalences, which correspond to the finer category of the paper, and SemidirectProduct, the special case with an action, but no crossed product with a cocycle, no weak actions, and no -type classification. Formalizing the mission produces a reusable nonabelian crossed-product layer and an explicit classification of extensions up to automorphisms of both ends.
Each step is elementary group theory, but the computations are long and noncommutative. The central difficulty is Corollary 2.3: every group morphism between two crossed products must be reconstructed from its values on the generators and , and the five compatibility conditions must be shown to be equivalent to multiplicativity, keeping track of the weak action and both cocycles in a nonabelian group. The tempting shortcut of treating as an action fails: (2) only makes multiplicative up to conjugation by , and this twist appears in every identity. In Corollary 3.5 the inverse of must itself be shown to be a morphism of and the map extracted from it.
Everything is in the namespace CrossedProductGroups.Classification, for arbitrary {H G : Type*} [Group H] [Group G].
α : G → MulAut H, not a homomorphism; the cocycle is curried, f : G → G → H.IsCrossedSystem α f records (2) and (3) with the factors in the printed order; Crossed H G is the subtype of pairs with f 1 1 = 1.crossedMul α f on H × G. No group instance is put on it; a morphism of groups between crossed products is a map preserving crossedMul.E2 H G is a type synonym for Crossed H G with a Mathlib Category instance. Its morphisms (E2Hom) record η : H →* H, γ : G →* G and a multiplicative ψ with ψ (h, 1) = (η h, 1) and (ψ x).2 = γ x.2. The paper's inclusion equals on normalized systems, the only objects.Equiv2 is Definition 3.7, with as γ.symm, η.symm.CategoryTheory.Skeleton and Quot Equiv2, includes Equivalence Equiv2, and requires the bijection to send toSkeleton c to the class of c.A bare equality of cardinalities between the skeleton and the quotient, an isomorphism notion in defined as , or morphisms that need not be multiplicative would each make the goal weaker than the paper's statement; the definitions above rule these out.
Contributions welcome: proofs of the milestones in any order, a reusable API for crossedMul (the group structure of Theorem 1.3 on a type synonym), and a bridge to Mathlib's GroupExtension.
A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore want, for a given target unitary, a circuit of the least possible depth, not merely some circuit.
Amy, Maslov, Mosca and Roetteler (arXiv:1206.0758, IEEE TCAD 2013) gave an exact, depth-optimal synthesis algorithm, MITM-factor, based on a meet-in-the-middle search. With it they found the first -depth-3 circuit for the Toffoli gate and improved circuits for several standard gates. Approximate synthesis methods such as the Solovay–Kitaev algorithm (Dawson–Nielsen) produce short circuits but not optimal ones. The paper is a standard reference for exact, optimal synthesis over Clifford+, and later depth- and -count-optimal search methods start from it.
Fix qubits. is the group of complex matrices with , where is the conjugate transpose. An instruction set is a set of gates closed under inversion. A gate acts on some of the qubits and as the identity on the rest.
A depth-one circuit applies gates of to pairwise disjoint sets of qubits at once. is the set of unitaries of depth-one circuits. A circuit of depth is a sequence of layers , and it implements . Let
so is the set of unitaries implementable in depth , and write .
MITM-factor runs . At step it builds and tests whether ; if so it returns the concatenation of the two witnessing circuits. Otherwise it tests in the same way. If no step succeeds, it returns nothing.
In the Lean development the layer set is a finite set V of unitaries standing for , S V i is , circuits V i is the set of circuits of layers (lists over V), and mitmFactor V U l is the algorithm.
For every finite , unitary and , with :
and a returned circuit lies over , implements , has , and for every circuit over of positive depth implementing . For even the decided range is exactly . If , the counted cost satisfies
The goal fixes no instruction set and no gate. It is the paper's correctness and running-time claim for the search itself.
In attack order:
The result. Searching all circuits of depth at most takes steps. MITM-factor needs only about , up to a logarithmic factor: a square-root saving that made exhaustive depth-optimal synthesis of three- and four-qubit gates feasible. Its correctness is what lets a computer search certify optimality: when the search fails up to depth , no shorter circuit exists. The paper's non-existence statements, such as the absence of shallower circuits for particular gates, rest on this.
Formalizing it. The result is proved in the paper, informally and briefly. No machine-checked version is known to exist. The mission produces a checked statement of what the search decides, which repairs two boundary cases of the printed claim (see Formalization scope), and a cost bound with an explicit constant in place of the . Lemma 1 and the generation step are reusable for any meet-in-the-middle search over a monoid generated by a finite set.
The mathematics is elementary; the difficulty is in stating exactly what the algorithm does. The obvious reading, "the algorithm decides depth at most ", is false for odd : the last step also tests depth and may return a circuit of that depth. "Returns a circuit of minimal depth" is false for , whose minimal depth is never tested. A proof therefore has to track the loop's first success through two interleaved tests per step, and connect sets of unitaries to circuits as lists of layers. For the cost bound, the step from per-iteration costs to the total needs the geometric-sum bound in a form the paper misprints: fails at , .
Unitaries are elements of Matrix.unitaryGroup (Fin n → Bool) ℂ; is the group inverse.
The layer set V is an arbitrary Finset of unitaries. The paper's argument uses nothing about beyond finiteness, and milestone 1 relates , defined over the shared QAlgorithms gate and circuit layer, to this setting. Hypotheses on V appear only where used: closure under inverse for milestone 2, for the cost clause.
Circuits are Lists of layers, implementing their List.prod, head leftmost, as "" on p. 4. The algorithm returns a circuit, not a unitary. The "any circuit" of the pseudocode is a choice of witnesses.
Corrections, each disclosed in the items:
Cost model. The running time is a counted cost, built from the sets the run actually generates:
These are summed over the iterations executed, up to the first success. Logarithms are Real.logb 2. The constant is the mission's explicit form of the paper's .
Trivializing readings are ruled out: the cost is not defined from , which would make the bound an identity about powers, and the goal is not an existence claim about some algorithm with that cost. A circuit-valued output compared against every circuit over prevents a content-free minimality clause.
Not covered: Theorem 1 and Theorem 2 with Lemma 2 (controlled- costs and -depth with ancillas), the -depth variant of §3.1, the pruning of §4, and the computational results of §§5–6.
Welcome contributions: proofs of the milestones, lemmas on circuits and S (for instance ), and a list-based model of the sort-and-search cost.
A quantum channel is a completely positive, trace-preserving linear map between matrix algebras; it models the most general physical transformation of a quantum system. When a group acts on the input and output systems, a channel is -covariant if it commutes with the group action. Covariant channels appear whenever a physical process respects a symmetry: rotation-invariant noise on spin systems, optimal cloning and estimation of spin states, and quantum reference frames for orientation. Because the covariant channels between two fixed representations form a convex set, the first structural question is what its extreme points are; they are the channels from which every covariant channel is obtained by mixing.
For acting irreducibly on input and output, the tensor product of the output representation with the dual of the input one is multiplicity free, so the commutant that controls covariant maps is abelian (Vollbrecht and Werner, 2001, arXiv:quant-ph/0010095). M. Al Nuwairan (arXiv:1306.5321, 2013) makes this concrete. She constructs explicit channels , called EPOSIC channels, from Clebsch–Gordan isometries realized on polynomials. She computes their Choi matrices and shows that they are exactly the extreme points of the convex set of SU(2)-irreducibly covariant channels.
For , let be the space of homogeneous polynomials of degree in two variables . The group
acts on by the representation ,
With the inner product , the canonical basis , , is orthonormal and is unitary. The are the irreducible representations of .
The tensor product is realized as the polynomials in and of bi-degree . On these polynomials act the operators
Real coefficients are defined by the recursion and, for , if , if , and if . For and , the map
is an explicit Clebsch–Gordan isometry. The EPOSIC channel is
For , is the set of the channels with and . The set consists of the quantum channels with for all and all .
The statement has no hypotheses and covers the degenerate cases: for the set is a single channel.
In the order of the paper's argument:
The result shows that the covariant channels between two irreducible SU(2) representations form a simplex. Its vertices are given by closed formulas, so optimization problems over SU(2)-covariant channels reduce to finite-dimensional linear programs over the vertex weights: fidelities, output entropies, capacities restricted to covariant encodings. The explicit Choi matrices make the vertices computable in any basis. The same channels are used later in the paper to compute complementary channels and to exhibit a positive map that is not completely positive.
On the formal side, the mission produces the irreducible representations of on homogeneous polynomials, the polarization operators, and explicit Clebsch–Gordan isometries with their equivariance and isometry proofs. It also produces a Choi-matrix criterion for covariance and the extreme-point characterization. Theorem 2.7, Proposition 1.15 and Proposition 3.9 are cited in the paper from Procesi, from [4] and from Vollbrecht–Werner, and are proved neither there nor, as far as is known, in any proof assistant. Nothing in this mission is machine-checked yet.
That is a covariant channel follows from equivariance of . The real content lies elsewhere.
First, is an isometry only because of the specific constants . The paper derives this from the polynomial identity of Theorem 2.7 and Schur's lemma, and neither is available off the shelf for these polynomial models.
Second, the extreme-point statement needs the full commutant of : the projections onto the irreducible summands must span it. Exhibiting the projections is not enough; one must show there is nothing else, which is multiplicity-freeness of the tensor product. This requires the irreducibility of each and the Clebsch–Gordan dimension count.
Third, matching each EPOSIC channel with a single projection (Proposition 3.13) requires a rank argument. The obvious approach, expanding the Choi matrix in coordinates, gives sums of products of signed binomial coefficients whose non-vanishing is the content of Lemma 3.12.
Every space is represented by coordinates in its canonical orthonormal basis, indexed by Fin (k+1) with 0-based indices. So is the algebra of complex matrices, and adjoints for the inner product above are conjugate transposes. The representation and the maps are computed from the polynomials themselves in MvPolynomial (Fin 4) ℂ (variables , derivatives pderiv), then read off in the canonical bases. The action is the row-vector action of the paper. is indexed with the factor first. The conjugate space has the same coordinates and carries the entrywise conjugate matrices. The coefficients are defined by the recursion, not by any closed formula. The input degree of is an explicit argument, constrained by in every statement.
Channels are maps on matrices given by a finite normalized Kraus family (the published QAlgorithms.IsChannel). The partial trace is the published WildeQIT.partialTraceRight, over the factor. The Choi matrix is with the output factor first. Convex hulls and extreme points are taken over in the space of maps.
No statement replaces by an abstract irreducible representation. None defines through extreme points, Choi matrices or projections, defines by its coefficient expansion, or assumes Schur's lemma, the commutant description or Theorem 2.7 as a hypothesis. Each of these would make the goal or a milestone true by definition.
A complete development needs:
The SU(2) representation layer and the Choi-matrix covariance criterion are reusable beyond this mission. Proofs of the cited results (Theorem 2.7, Propositions 1.15 and 3.9) are welcome as independent contributions.
Operators on copies of that commute with every , unitary, are exactly the linear combinations of permutation operators , (Schur–Weyl duality). Many protocols in quantum information carry a different symmetry: the first systems transform by and the last by the complex conjugate . It is the symmetry of port-based teleportation (Ishizaka–Hiroshima 2008), whose optimal performance is computed from the representation theory of exactly this commutant (Studziński et al. 2017). The commutant of is the algebra spanned by the partially transposed permutation operators : the permutation operators with the transpose taken on the last system.
Studziński, Horodecki and Mozrzymas give an explicit operator basis of an ideal of adapted to the irreducible representations of . Their main structural result, Theorem 9, states that this basis and the partially transposed permutation operators are linear combinations of each other, with coefficients that are irrep matrix elements.
Let and . For , the permutation operator on is . The partial transposition transposes the last system: . The algebra is the span of all , . is regarded inside as the permutations fixing the systems after .
Fix with , and write . For labels , the maps are
The standing data are a family of real orthogonal, irreducible, pairwise inequivalent matrix representations of , of dimensions , and a Schur basis: an orthonormal basis of , where ranges over the multiplicity of , such that . With on the last two systems, the paper defines
and . In Lean these are IrrepFamily, SchurBasis, psi, vOp, EOp, with ptLast for , fPerm for and algA for .
For all , , :
and for every , with ,
The goal is the whole theorem, both directions and the membership in .
Theorem 9 shows that the span the same space as the operators with . That space is the ideal of on which the partial transposition acts non-trivially. Because the multiply like block matrices (Lemma 8 of the paper), the theorem converts questions about into finite matrix computations indexed by irreps of . The later constructions of the paper rest on this: the Gram matrices , the biorthogonal basis and the explicit irreps of . The same formalism underlies the eigenvalue analysis of port-based teleportation (Mozrzymas–Studziński–Horodecki 2018).
The result has a published proof but no machine-checked one. This mission adds that check, together with a reusable Lean vocabulary: the partial transpose on one site of , the embeddings , and Schur-basis data for permutation operators. It also pins down the conventions that the printed text leaves inconsistent (see Formalization scope).
The algebraic manipulations are short on paper; the work lies in the bookkeeping they hide. Lemma 26 requires checking that fixes both of the last two systems, which uses in an essential way. The partial transposition is not multiplicative, so every step that moves an operator through needs the specific invariance of milestone 1. Eq. (86) is the identification of the Schur-basis matrix units with group-algebra elements; it needs completeness of the basis together with Schur's orthogonality relations for real irreps, and it is false without irreducibility and inequivalence. Mathlib has Schur's lemma but no coordinate form of the orthogonality relations for matrix representations, and nothing on partial transposes of tensor-power permutation operators.
Equiv.Perm (Fin m), Equiv.Perm (Fin (m+1)), Equiv.Perm (Fin (m+2)). Systems are 0-based, so systems are indices , and labels are Fin (m+1). Permutation products compose right to left.QAlgorithms.Schur.tensorPermutation. is on the last system only. groupAlg is the represented ; algM spans the with .IrrepFamily m contains real orthogonal matrix representations of of positive dimension, irreducible over and pairwise inequivalent over (p. 7 and Notation 32 of the paper). SchurBasis F d is an orthonormal, spanning family of vectors on which acts by the . Multiplicities may be zero. The family is not required to list every irrep of . Every satisfies (Definition 24).ptLast and on liftPerm. Both are reusable beyond this paper.Wilson's numerical renormalization group (NRG) computes the low-energy states of quantum impurity models, such as the Kondo and Anderson models, by diagonalizing a semi-infinite chain one site at a time and keeping only the lowest multiplets after each step (Wilson 1975; review: Bulla, Costi, Pruschke 2008). Dynamical quantities (spectral functions, Green's functions) at finite temperature require, in addition, the reduced density matrix of each shorter chain, obtained by tracing the full density matrix over the sites that come later. This is the density matrix NRG (DM-NRG) (Hofstetter 2000), made exact with the complete basis of Anders and Schiller 2005.
Symmetries make NRG practical: when the Hamiltonian is invariant under a group, every iteration splits into blocks labelled by irreducible representations, and each multiplet is stored once instead of once per internal state. For non-Abelian groups (SU(2) spin, SU(2) charge, SU(3) channel symmetry) the saving is large, but only if the reduced density matrix can also be handled multiplet by multiplet. Tóth, Moca, Legeza and Zaránd (arXiv:0802.4332) show that it can, for essentially any symmetry: the reduced density matrix stays scalar under the symmetry after each tracing step, and its reduced matrix elements obey an explicit recursion, their eq. (45), whose only group-theoretic input is the ratio of multiplet dimensions.
A group acts on every multiplet through a labelled unitary irreducible representation: a label has a dimension and unitary matrices of size , and states of a multiplet are indexed by an internal quantum number . Distinct labels carry inequivalent representations.
At iteration the new space is spanned by states , where runs over the kept multiplets of iteration (block states, label ) and over the local multiplets of site (label ). The symmetry acts as
Generalized Clebsch–Gordan coefficients are, for each label in a coupling set of , the entries of a matrix that is an isometry, intertwines with , and such that the sum to the identity. The canonical basis (21) is
one canonical multiplet per kept multiplet, local multiplet and coupled label; one writes .
An operator on the new space is scalar if for all . Its reduced matrix elements in the canonical basis are defined by . is the partial trace over the local states of site .
For every scalar : is scalar under ; has reduced matrix elements in the canonical basis; for kept multiplets with and every such family of reduced elements,
and the entry vanishes when . The paper's truncated reduced density matrix of its eq. (38) is one instance of ; the statement fixes no Hamiltonian, energies or temperature.
In proof order: the covariance of the partial trace (40); the invariance of and of (39), (41)–(42); the Wigner–Eckart form of a scalar operator (43); orthonormality, completeness and the transformation law of the canonical basis (21); the Wigner–Eckart form in the canonical basis (44); and the Clebsch–Gordan sum rule that produces the factor when the local states are traced out.
The recursion (45) computes the reduced density matrix of every iteration from that of the next, one number per pair of multiplets, so that all DM-NRG expectation values and spectral functions can be evaluated in the reduced (multiplet) representation. Its only group-dependent input is the dimension ratio ; the Clebsch–Gordan coefficients themselves drop out. This is what lets a DM-NRG code, such as the flexible code the paper describes, handle any number and type of symmetries without symmetry-specific density-matrix code.
The result is proved in the paper, in a few lines of physics notation that rely on the Wigner–Eckart theorem and on Clebsch–Gordan orthogonality. It has no machine-checked proof. The mission states it as a theorem about invariant matrices, unitary representations and Clebsch–Gordan isometries; its milestones include a Wigner–Eckart theorem for scalar operators on a space of labelled multiplets and a Clebsch–Gordan sum rule, both stated for an arbitrary group and reusable for other symmetry-adapted tensor-network and many-body computations.
The physics proof cites the Wigner–Eckart theorem; formally this is Schur's lemma in two forms: an equivariant map between inequivalent irreducible representations vanishes, and an equivariant endomorphism of an irreducible representation is a scalar. Neither is a hypothesis here, so both must be derived from irreducibility in its invariant-subspace form. The dimension factor is the second form applied to the partial trace of , together with a trace count. A direct computation from the definition of the canonical basis does not give (45): the Clebsch–Gordan coefficients are arbitrary matrices subject only to the three stated conditions, so no closed formula for them is available, and the dimension ratio appears only through the representation-theoretic argument. The bookkeeping is also non-trivial: internal quantum numbers of different multiplets live in different index types even when their labels coincide, and the tilde sum pairs canonical multiplets built with the same local multiplet.
One abstract group with labelled irreducible unitary representations replaces the paper's product of eqs. (17)–(18); the product case is an instance, with the generalized Clebsch–Gordan coefficients of p. 4 as products. Irreducibility is Mathlib's Representation.IsIrreducible, inequivalence the emptiness of Representation.Equiv. The coupling is multiplicity-free, one Clebsch–Gordan matrix per label triple, exactly as (21) is written; with outer multiplicities (as in SU(3)) the printed (45) would need a multiplicity index. Operators on the new space are matrices indexed by (block, local) pairs, block first, and the partial trace over the site is the published WildeQIT.partialTraceRight; Clebsch–Gordan matrices are indexed local first. All index sets are finite. Internal quantum numbers of multiplets with equal labels are compared by their numerical value. No fermionic sign factors appear: the space is the tensor product in the ordering of (21), and (45) carries no sign.
The statement does not assume Schur's lemma, the Clebsch–Gordan sum rule, or a block form of ; the reduced matrix elements in (45) are not free parameters but any family satisfying the Wigner–Eckart identity for , whose existence is part of the goal. The Wilson chain, the complete basis and density matrix (32)–(38), the Green's function (46)–(48), the numerics of §V and the SU(2) appendix are outside the mission.
A complete development needs a usable Schur's lemma for matrix representations (Mathlib provides the module-theoretic version), Kronecker-product and block-diagonal matrix algebra, and partial-trace identities. Lemmas on partial traces of Kronecker products and on Wigner–Eckart for block-diagonal representations are reusable beyond this mission; contributions of either kind are welcome.
Operators made from a complex matrix and its conjugate occur in the non-chiral sector of gauge theories. Their correlation functions involve many possible pairings of matrix entries, and those pairings become difficult to organize as the number of entries grows. Kimura and Ramgoolam use the walled Brauer algebra to label these operators and to describe their two-point functions in a basis adapted to both the tensor symmetries and the mixed fundamental–conjugate representation. The result targeted here is the orthogonality relation for that basis in the reduced two-matrix quantum mechanics Kimura and Ramgoolam, §7.1, p. 29.
The question is concrete: can the algebraic labels of an operator determine whether its state has zero inner product with another state, without expanding every matrix entry? Equation (7.12) says yes for the paper's symmetric branching operators. It is a known result in the cited paper. This mission asks for a machine-checked formalization of its precise tensor-space content, including the complex Gaussian covariance and the permutation sums on which the two-point function depends.
Let , with basis indexed by . The mixed tensor space has a basis labelled by a pair of index tuples: an -tuple for the legs and an -tuple for the conjugate legs. Its operators are finite complex matrices; is their ordinary matrix trace. The group permutes legs within each block. It is represented by matrices , using the already published tensor-permutation definition used here.
A contraction pairs the th leg with the th conjugate leg. The image of the algebra generated by all such contractions and the permutations is denoted . This is the represented Brauer algebra used in the paper's tensor-space traces §3.2, pp. 8–9. The map exchanges the input and output indices of the conjugate block. In coordinates it is the partial transpose on that block; this matches the reflection shown in Figure 6 §3.3, pp. 11–12.
The paper's symmetric branching operators are denoted . Here labels a Brauer representation, an irreducible representation of , and range over its multiplicity . These operators belong to the represented Brauer algebra, are invariant under conjugation by every , and obey the matrix-unit product . The relation comes from their orthonormal-vector definition in (7.3) §7, pp. 27–28.
For two independent complex matrices , put
Each matrix entry has independent real and imaginary parts of variance . This Bargmann–Fock Gaussian realization gives and reproduces the oscillator normalization of (7.8) p. 28.
The goal is the orthogonality identity of (7.12), with the scalar written as a tensor-space trace:
The paper writes the last factor as after invoking mixed-tensor Schur–Weyl duality. The trace version is the equality reached just before that last step in (7.13) p. 29. The mission's milestones cover the unit covariance (7.8), the Wick permutation formula of Figure 3, the trace sum in the second line of (7.13), symmetry preservation (3.37), the collapse in the third line of (7.13), and the trace-pairing identity (3.20).
The formula assigns orthogonal states to different branching labels and multiplicity indices. It also fixes their norms by an explicit finite-dimensional trace. This makes the representation labels useful for organizing non-chiral two-point functions, rather than merely counting or naming operators §7, pp. 27–29. Without the Wick-to-trace identity, the same claim remains an expanding sum of matrix-entry pairings for each degree.
The paper proves the identity diagrammatically; this mission has no machine-checked proof of it yet. A completed formalization would give reusable finite-matrix interfaces for contractions, partial transpose, Gaussian polynomial states, and permutation-indexed Wick sums. The complex covariance and Wick results can be reused independently of the particular Brauer family. The represented algebra and branching interface can support later formalization of the paper's projectors and finite- examples.
The central obstacle is the passage from a Gaussian expectation of products of matrix entries to a sum of traces indexed by . A direct expansion of the state polynomials creates many indices, and each Gaussian pairing must match the direction of the matrix entries and the inverse permutation in the tensor action. The and matrices are independent, so pairings cannot cross their blocks. After that conversion, the partial transpose and permutation symmetry must agree on the same index convention. A transposed covariance or reversed inverse produces a plausible looking expression with the wrong contractions.
The Lean model uses finite matrices throughout, permits , and uses ordinary unnormalized traces. The index type is a pair of functions from and to ; its second component represents the conjugate legs. is the concrete partial transpose, and is the image subalgebra generated inside the matrix algebra. The oscillator vacuum inner product is the Gaussian integral above, with two independent matrices and unit complex variance. It is defined from the measure, not from the Wick permutation formula. The measure's pushforward map is continuous. Matrix-entry polynomials have finite Gaussian moments, so the integral does not rely on Lean's default value for a non-integrable function.
The branching labels are abstract types, but each valid must satisfy Brauer membership, the paper's symmetry and matrix-unit relations, and the adjoint relation derived from (7.3). Indices are natural numbers with explicit range conditions . No completeness axiom, positivity condition, or lower bound on is added. These declarations exclude a trivialized inner product defined as the target permutation sum. The coefficient and the four-dimensional, normal-ordered version (7.16) are outside this mission. Contributions to the Gaussian Wick conversion, the partial-transpose trace identity, and the symmetric branching calculation are all in scope.
Positive linear maps on complex matrix algebras provide tests for quantum entanglement: applying such a map to one part of a bipartite state can expose a state that cannot be written as a mixture of product states. The distinction between ordinary positivity, positivity with an auxiliary matrix system, and complete positivity is therefore substantive. Collins, Osaka, and Sapra study an explicit two-parameter family that makes these distinctions visible through inequalities in the parameters. Their paper identifies the exact region where a map from three-by-three matrices to nine-by-nine matrices is 2-positive but fails to be completely positive. This is the stated main result of their 2018 paper, rather than an open conjecture.
Write for the algebra of complex matrices. A matrix is positive semidefinite, written , when it is Hermitian and has no negative eigenvalues. A complex-linear map is positive when implies . It is -positive when the same condition holds after the identity map on is tensored with . It is completely positive when it is -positive for every . A map is completely copositive when its composition with transpose on the source is completely positive. These are the paper's definitions on page 2.
Let be the unnormalized Bell vector, and let denote its rank-one projector. For real and , the family on page 3 is
The transpose belongs to the first tensor factor. The mission concentrates on . Its Choi matrix is . For this finite-dimensional setting, the Choi criterion relates complete positivity to ; it does not define complete positivity. The paper also identifies an equivariance property: unitary conjugation of the input corresponds to conjugation of the output by a matrix associated with the same unitary.
For , define two boundary curves and a cubic root:
The goal is Theorem 3.9, page 10:
The left endpoint of the first interval is included and the right endpoint is excluded. The milestones record the paper's earlier criteria for positivity, complete positivity, and 2-positivity, together with its general equivariance criterion and the computation for this family. Their inequalities are separate targets; none is built into the definitions of these map properties.
The goal gives an exact, parameter-level example of 2-positivity without complete positivity. It identifies all such members of this family on , including the boundary cases, rather than only exhibiting one map. The surrounding results locate the positive and completely positive regions and give a criterion for testing -positivity of equivariant maps. Together, they provide a compact source of concrete maps with different strengths of positivity, as described in Sections 2 and 3 of the paper.
The mathematical result was proved in 2018. This mission seeks a machine-checked account of the stated criteria, with the family, Choi matrix, Bell projector, and positivity predicates exposed as reusable declarations. A finished proof would connect elementary matrix positivity and tensor products to explicit real-algebraic parameter bounds. It would also make each boundary independently inspectable. The Lean theorem statements here are draft targets with sorry; they are not existing machine-checked proofs of the paper.
Testing only yields ordinary positivity, not 2-positivity. Testing only the Choi matrix addresses complete positivity, which is stronger than the desired property. The 2-positive condition quantifies over every positive semidefinite matrix in ; the paper's criterion reduces that universal condition under equivariance to positivity of a specific block matrix. The block matrix has parameter-dependent eigenvalues, including roots of a cubic. This makes a simple comparison of the two square-root boundary curves insufficient: the smallest cubic root supplies an additional lower bound on . The endpoint also needs attention because the case descriptions for complete positivity meet there.
The Lean model uses Matrix (Fin n) (Fin n) ℂ for and Fin n × Fin n for the output tensor indices, with the first coordinate corresponding to the transposed factor. The paper's one-based is Matrix.single 0 0 1. Positive semidefiniteness is Mathlib's Matrix.PosSemidef. The shared QAlgorithms.idTensorSuperop applies a map blockwise with the auxiliary index first, and the published QAlgorithms.Entanglement.IsCompletelyPositive quantifies over all auxiliary sizes. Size zero is harmless for that quantifier because the corresponding matrix type is empty. The paper's appears on the general-family results; the main goal fixes .
The Bell projector is unnormalized, matching the paper's . The two square roots have positive radicands on the real parameter range. The cubic root is defined as the infimum of its real root set; the odd-degree cubic has a nonempty, finite set of real roots, so this is its least root. The proof development needs reusable facts about unitary conjugation of positive matrices, Kronecker products, Choi matrices, and positivity of the parameterized block matrix. Direct calculations of the boundary inequalities are also welcome. Defining -positivity by the block criterion, complete positivity by Choi positivity, omitting the transpose in , or treating as an arbitrary parameter would make the targets lose their intended content.
An agentic system may make several slow API calls in sequence: the answer to one call determines what to request next. A speculator can guess the current answer while the real call is running and start likely next calls early. When a guess is correct, the system can reuse a pending result; when it is wrong, it discards that result. This can shorten a run if concurrent calls do not interfere and incorrect calls have no lasting side effects. Ye and coauthors introduce this execution scheme for language-model and tool-using agents in Speculative Actions, §2.
The paper's Proposition 1 quantifies the expected latency of one-step speculation with exponential call times. Its proof in Appendix A states a stochastic timing model and computes a finite-horizon runtime ratio and its limit. The first author's existing Prove2Me mission, Speculative Actions: Cost-Latency Analysis for Agentic Speculation, contains proved algebraic identities for expressions named specTime and seqTime. Those expressions encode the values claimed for the expectations. This mission supplies the missing connection between random executions and those expressions, while reusing the published algebra.
There are real API calls, numbered through . The real-call latency of step is with exponential rate . At a speculation window during step , a speculator has latency with exponential rate . It produces candidate next calls. Each candidate independently matches the actual next call with probability , so a hit means that at least one of the candidates matches. The hit probability is
All latencies and branch-correctness indicators are mutually independent. Proposition 1 assumes and Assumption 1 gives ; as a probability, . Assumption 2 permits concurrent API calls and reversible or side-effect-free pre-launching. The theorem also treats state transitions and construction of API parameters as having negligible duration. These conditions and the exponential laws are stated in §2 and Proposition 1.
The sequential runtime is . The speculative runtime follows Appendix A's timing rule. At a window without a hit, the current step costs . At a hit, the block comprising steps and costs , and step opens no window. The last step cannot open a window. This is the model used in the paper's proof of Proposition 1, Appendix A, pp. 14–15. Its precise timing rule matters: reading Algorithm 1's awaits literally gives a different timeline, as does waiting for validation before accepting an early next-step result.
Let be the expected number of hits in potential windows, with a hit consuming the following window. The paper gives , , and
The new milestones identify the expectation of the sequential runtime, the saving from one correct speculation, and the expected hit count. The total-saving identity is
Here is the expectation of the random count defined by the execution model. The previously published expression SpecActions.specTime has this same algebraic form; proving equality with the integral of the random runtime is the new step. The closed form for and the algebraic ratio are linked as published milestones.
For every integer , the goal is the Proposition 1 ratio for the actual expectations:
The same goal states convergence of this random-runtime ratio as to
The horizon condition protects the denominator: at , the sequential runtime is zero. The number of branches may be zero; then and the ratio is one for positive horizons.
The formula describes how breadth , branch accuracy , and the two latency rates affect expected completion time, both for a finite sequence of calls and in a long run. It makes the expected benefit of extra branches a quantity that can be compared with their resource cost. The paper uses the time expression again in its cost–latency discussion, including Theorem 5, p. 20.
The author's existing mission has machine-checked proofs for the recurrence's closed form and for algebraic identities involving specTime and seqTime. It does not prove that those expressions are expectations of a random execution. Completing this mission adds that probabilistic interpretation and a reusable model of independent calls, branch indicators, skipped windows, and runtime. The proposed stochastic theorems remain open; their statements compile, while the published reference results are already proved.
The main issue is the dependence created by skipping a window after a hit. Hit indicators at different windows are independent, but the number of opportunities actually used is determined by earlier outcomes. Treating the hit count as an ordinary binomial count gives the wrong recurrence. Likewise, multiplying a mean saving by the number of potential windows ignores that skipped windows cannot hit. A formal proof must relate the random execution and hit count while preserving the independence between correctness indicators and latencies.
Lean represents all primitive random variables on one probability space. An index type separates speculator latency, real-call latency, and each of the branch indicators at every window. IsSpecModel requires measurable variables, their exponential or real-valued Bernoulli laws, and mutual independence. A hit is an existential statement over the branch indicators. The runtimes and hit count are recursions on a finite horizon, and expectation is the real Bochner integral. The model has an explicit construction on a product probability space, so its hypotheses are satisfiable.
Windows start at index zero: a -step run has potential windows. The theorem keeps the paper's and conditions, and specifies . It adds wherever a runtime ratio is divided by its sequential denominator. Concurrency without interference and negligible non-call work are represented by the timing recurrence. The claim concerns integrals of those random runtimes; defining an “expected runtime” directly by the paper's closed form would omit the target of this mission.
The definition layer and hit-probability, baseline, saving, hit-count, and total-saving milestones are available as separate contributions. Mathlib supplies exponential probability measures, product measures, independence, and integration; the published SpecActions definition and algebraic theorems are referenced. Work on the probabilistic bridges, integrability, and the final composition is within scope.
Firms with several products often put most of their marketing behind one. The resulting product can become the line's flagship even when another product has a higher unit markup. He, Ke, and Zhang give a supply-side model in which this allocation follows from the relation between consumer taste dispersion and the cost of raising a product's perceived utility. Their main proposition says that a concave transformed marketing cost favors concentrating effort on one product. This mission formalizes that proposition and the fixed-effort claims that support it. He, Ke, and Zhang, A Model of Product Line Marketing, 2021 SSRN version, §2 and Online Appendix C.
The question is operational: a firm chooses marketing effort across its product line while sales move through a multinomial logit choice model. Spending on one product changes its share and also takes sales from the firm's other products. Concentrating marketing effort therefore cannot be inferred from looking at a single product's markup in isolation. The paper's marketing effort allocation index provides a way to compare products at a given total effort. He, Ke, and Zhang, §2.1, pp. 12–15.
A firm sells products. Product has base utility and markup . Consumers either buy one product or select an outside option with utility normalized to zero. A Gumbel taste shock has scale . The firm raises product 's utility by , where is the common lower bound, and pays . The paper assumes the cost is strictly increasing, convex, and continuously differentiable on feasible utility increases. The logit choice formula gives product a share proportional to , with in the denominator for the outside option. He, Ke, and Zhang, §2, pp. 7–9.
Equation (7) uses a nonnegative effort multiplier . A marketing effort allocation, or MEA strategy, is the vector with every . Its total marketing effort, or TME, is . In these coordinates the firm's program (8) maximizes
over every feasible . The first term is revenue and the second is marketing cost. A strategy is concentrated in Definition 1 exactly when one multiplier is positive and all the others are zero. In particular, the zero allocation is a separate case. The transformed cost is . He, Ke, and Zhang, pp. 10–11, equations (7)–(8), Definition 1, Proposition 1.
For positive total effort , product 's MEA index is , where
It equals the revenue when all is assigned to product . This is Definition 2 and the sentence immediately following it. He, Ke, and Zhang, p. 12, Definition 2, equation (9).
The goal is Proposition 1 with its implicit edge cases made explicit. If is concave on , an optimum exists, some optimum is concentrated or zero, and pairwise distinct products have no mixed optimum:
The milestone list follows the source's fixed-effort results. Lemma 3 bounds a weighted ratio by its largest component ratio and characterizes equality. The index interpretation and equation (C–9) connect that inequality to revenue. Lemma 4 concerns revenue at fixed TME, while Lemma 5 concerns cost at fixed TME. Proposition 2 restricts which products can receive positive effort at a profit optimum. Claim 1 and Lemma 6 address tied MEA indices at a positive optimal TME. He, Ke, and Zhang, Online Appendix C, pp. 40–43.
The proposition identifies a class of marketing cost functions under which the firm can choose a single flagship product without giving up optimal profit. Under a distinct-product condition, it characterizes every optimum up to the possibility of zero total effort. The MEA index separately identifies which products can carry positive effort at an optimum. These statements let a solver study effort concentration and product selection within one common optimization model. He, Ke, and Zhang, Propositions 1–2, pp. 11 and 14–15.
The paper proves these results on paper. This mission asks for machine-checked proofs of the model-specific statements, including the edge cases left implicit in the printed wording. It also establishes reusable finite-sum facts, especially the ratio inequality and its equality condition. No machine-checked proof of this paper's marketing-effort theorem is claimed here.
A larger markup does not always make a product the best flagship. Revenue depends on every product's logit attraction and on the outside option, while cost depends on the entire allocation. Maximizing revenue at a fixed total effort therefore does not by itself solve the firm's original problem, whose total effort is also chosen. Ties in the MEA index create another difficulty: at a fixed total, several products can share effort without changing the revenue, so a concentration statement about every optimum needs a separate condition. He, Ke, and Zhang, §2.1 and Online Appendix C.
Products are indexed by Fin n; the book's indices are relabeled from zero. All monetary, utility, and multiplier quantities are real numbers. Strategies range over all nonnegative vectors, and optimality compares profit against every such vector. The outside-option attraction is . The cost assumptions apply on , and transformed-cost concavity applies on , the ranges reached by feasible allocations. The formula is used only for , so its terms never rely on Lean's default value for division by zero. Since , every logarithm in the objective has a positive argument.
The goal includes existence of an optimum so that its statement about all optima has content. It distinguishes zero effort from Definition 1's concentrated allocation: zero effort can be optimal. Pairwise distinct are required for the assertion about every optimum; identical products can support mixed optima. The paper says an optimum is “generically unique” but does not define a generic set or prove uniqueness of the optimal total effort under a specified genericity condition, so that phrase is outside this goal. Lemma 3 separately requires a positive total weight; Claim 1 restricts its rational curves to nonconstant ones. The printed proof of Lemma 6 has a gap for constant tied index curves, noted for reviewers. He, Ke, and Zhang, Definition 1, Proposition 1, Online Appendix C.
The development needs finite sums, real exponentials and logarithms, elementary calculus, and convexity and concavity on intervals. Its model definition is paper-specific; the ratio bound and rational-curve identification are useful beyond this setting. Contributions to any of the stated milestones, including their explicit boundary cases, are in scope.
In this paper, we show the equivalence of the set of unitaries computable by the circuits over the Clifford and T library and the set of unitaries over the ring , in the single-qubit case. We report an efficient synthesis algorithm, with an exact optimality guarantee on the number of Hadamard and T gates used. We conjecture that the equivalence of the sets of unitaries implementable by circuits over the Clifford and T library and unitaries over the ring holds in the -qubit case.
This mission is the statement-level formalization of Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates (arXiv:1206.5236v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact single-qubit H/T synthesis characterization (Theorem 1 (abstract seed): exact single-qubit synthesis characterization, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
7 results of the paper are not stated yet, because the library lacks an interface they need:
A Boolean function can react differently to changing one input coordinate and changing several coordinates together. Measuring this difference is a question about the local complexity of total Boolean functions. The Block Sensitivity vs. Sensitivity campaign records exponents that quantify how large this difference can become along families of functions with increasing sensitivity.
This mission records the exact exponent
Its construction is already accepted and public. The mission expresses that result using the campaign's shared definition, so that its value can enter the same record as earlier entries. The logarithmic expression is the target; the displayed decimal is an approximation. No optimality claim is part of this mission.
A total Boolean function on coordinates is a map , defined on every binary input. For an input and a set of coordinates, write for the input obtained by flipping exactly the bits indexed by .
A coordinate is sensitive at if . The sensitivity counts those coordinates, and is the maximum of over all inputs. A nonempty coordinate set is a sensitive block at if . The block sensitivity is the largest number of pairwise disjoint sensitive blocks at that input. The quantity is its maximum over all inputs.
Every block in one block-sensitivity witness is tested at the same input. The blocks are disjoint as coordinate sets; their sizes need not be equal. These conventions are those of the shared foundation mission, rather than complexity measures defined only on selected inputs or on a promise domain.
The goal is the campaign proposition . Explicitly, for every real and every natural number , there must exist a natural number and a total Boolean function satisfying
Both the dimension and the function may depend on and . The sensitivity threshold is essential: a favorable ratio for one bounded example does not establish this statement. For example, choosing successively smaller positive losses and increasing thresholds produces a sequence of finite total Boolean functions with unbounded sensitivity and exponents approaching .
The exact numerator is the natural number
The denominator inside the logarithm is . Both logarithm arguments exceed one. There is no division by a zero logarithm, and the result uses ordinary real powers. The goal does not assume a finite construction certificate or the existence of a suitable labeling as a hypothesis.
The accepted construction theorem also proves the strict comparison
It improves the earlier public exponent, approximately , by approximately . The full proof constructs actual Boolean functions and establishes the asymptotic quantifiers; the numerical approximation alone is not the evidence for the separation.
The complete construction has passed local Lean kernel verification and Prove2Me verification. Its accepted submission is a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. The source uses ordinary checked proofs with the standard axioms propext, Classical.choice, and Quot.sound. Its final statement spells out sensitivity and block sensitivity directly through finite sets. The campaign goal uses the existing shared definitions for those same quantities, and its proof explicitly establishes the equivalence needed to transfer the accepted result.
A lower bound on block sensitivity at one input must be combined with an upper bound on sensitivity over every input. Local calculations that ignore the latter maximum can overstate the separation. Likewise, overlapping sensitive blocks cannot be counted as a disjoint family. These requirements persist through the construction and the passage to arbitrarily large sensitivity.
The exponent also depends on exact integer growth rates. Rounded numerical scores can identify candidates, but they do not establish the final real-power inequality. A complete proof must account for finite construction constraints, the complexity measures of the resulting functions, and the exponent loss allowed in the asymptotic statement. The accepted result includes these steps. This mission records that established result rather than a proposed stronger threshold awaiting construction.
The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Inputs are functions Fin n → Bool, and outputs are Bool. Sensitivity and block sensitivity are natural numbers obtained by finite maxima. The campaign proposition quantifies over positive real losses and natural sensitivity thresholds.
Dimension zero is permitted by the representation, but its sensitivity is zero and it cannot witness any required threshold . Empty block families contribute zero; every counted block is nonempty. There are no hypotheses that can make the target vacuous. The shared definition and finite-certificate references are retained from the campaign template. The only new result recorded here is the improved separation exponent and its exact campaign formulation. Attribution to the original OpenAI development and Robin Kothari/Codex is retained in the accepted construction source; the new construction is credited to yousofy with Codex.
yousofy with Codex, Six shared defect tolerances improve the sensitivity exponent to 2.1308255794, Prove2Me, 2026. Accepted complete construction.yousofy with Codex, Earlier strict exponent checkpoint, Prove2Me, 2026. Public comparison theorem.Newtonian gravitation can be written in two ways. In Newtonian gravitation (NG), spacetime has a flat derivative operator and a scalar potential obeying Poisson's equation, and bodies are pushed off the straight lines of by the force . In geometrized Newtonian gravitation (GNG), also called Newton–Cartan theory, the potential is absorbed into a curved derivative operator whose geodesics are the trajectories of freely falling bodies. This is the same geometrization that general relativity performs. Trautman (1965) proved that the two pictures pass into each other.
Weatherall (2016) asks whether NG and GNG are the same theory. He represents each theory by a category of models and calls two theories equivalent when there is an equivalence of categories that preserves empirical content. The answer depends on the arrows chosen for NG:
This is the gravitational twin of the electromagnetic question "potentials vs. field strengths" treated in the companion missions on Weatherall's Understanding Gauge. The other side of the Newton–Cartan story, the classical limit of general relativity, is described under Significance.
Following Weatherall (p. 3), spacetime is , here in one global chart E = Fin 4 → ℝ with index 0 for time. The classical metrics are (tt) and (hh). Their slices are complete copies of , as Weatherall requires.
A derivative operator is a smooth field of Christoffel symbols Γ x a b c , symmetric in , acting by
It is compatible when and . Curvature uses Malament's sign convention:
Other notation:
geomΓ).gaugeΓ).The objects of the categories are:
IsNG Γ φ): compatible, flat and a smooth potential . The mass density is .IsGNG Γ): compatible satisfying, for some smooth ,The arrows are diffeomorphisms of that preserve and and carry one derivative operator to the other through the transformation law
(IsGNGArrow). NG₁ arrows also preserve (IsNG1Arrow). NG₂ arrows are pairs with , where carries the gauge-transformed pair to (IsNG2Arrow).
ng2_equiv_gng, Weatherall Prop. 6.1)Geometrization , has these properties:
This is exactly the "full, faithful, essentially surjective" route of Weatherall's proof in App. A. These three properties together are equivalent to an equivalence of categories.
geometrization, Prop. 2.1 (Trautman). For flat compatible and Poisson's equation, has these properties:
recovery, Prop. 2.2 (Trautman). Every classical spacetime satisfying (1)–(3) comes from some flat and potential obeying Poisson's equation.gauge_iff, the non-uniqueness remark after Prop. 2.2. A second pair works iff and . Weatherall states the "if" direction and his proof of Prop. 6.1 uses the "only if" direction. The iff is Malament's Prop. 4.2.5. Note that is allowed: the gauge includes time-dependent uniform accelerations (Corollary VI).geom_naturality, the key computation in App. A. A metric-preserving diffeomorphism carrying to carries to iff it carries to .ng1_not_equiv_gng, the NG₁ row of Table 1 (§6, p. 18). No object map NG₁ → GNG preserves empirical content while inducing bijections of hom-sets. Weatherall states this in prose without a proof. The intended argument is that two NG₁ models related by a nonzero gauge share a geometrization but have no NG₁ arrow between them.We establish what we consider to be the definitive versions of Jensen's operator inequality and Jensen's trace inequality for functions defined on an interval. This is accomplished by the introduction of genuine non-commutative convex combinations of operators, as opposed to the contractions used in earlier versions of the theory. As a consequence, we no longer need to impose conditions on the interval of definition. We show how this relates to the pinching inequality of Davis, and how Jensen's trace inequlity generalizes to C*-algebras..
This mission is the statement-level formalization of Jensen's Operator Inequality (arXiv:math/0204049v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Jensen’s operator inequality: four equivalent conditions (Theorem 2.1 (Jensen’s Operator Inequality), PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
2 results of the paper are not stated yet, because the library lacks an interface they need:
A state on a tripartite quantum system forms a Markov chain if it can be reconstructed from its marginal on by a quantum operation from to . We show that the quantum conditional mutual information of an arbitrary state is an upper bound on its distance to the closest reconstructed state. It thus quantifies how well the Markov chain property is approximated.
This mission is the statement-level formalization of Quantum conditional mutual information and approximate Markov chains (arXiv:1410.0664v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
39 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Relative entropy from dominated approximants (Lemma 2.1, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.
The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.
Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.
6 results of the paper are not stated yet, because the library lacks an interface they need:
A Bell test certifies that correlations between two separated parties cannot be produced by any classical mechanism, that is, by a local hidden variable (LHV) model (Bell 1964). The same tests are the basis of device-independent protocols, where an adversary is only constrained by the no-signaling condition: neither party can learn the other's input from its own statistics (Popescu–Rohrlich 1994).
In experiments detectors fail. If a detector fails often enough, the observed statistics (including the failures) admit a local explanation even when the underlying correlations are nonlocal. This is the detection-efficiency loophole. The question is quantitative: given the numbers of measurement settings, what detector efficiency is required to demonstrate nonlocality?
Timeline of the two-party question, as summarised by Cao–Peng 2016:
A party A receives an input and B an input ; they output and from finite alphabets. A behaviour is a probability distribution on outputs for every pair of inputs. It is no-signaling if does not depend on and does not depend on .
With detector efficiency , each party's output alphabet gains an empty symbol , and the observed behaviour is
A behaviour is LHV-simulable if there is a probability space and measurable local response probabilities , with
The efficiency threshold of a no-signaling behaviour is , and the efficiency bound is
the infimum over all no-signaling behaviours with , inputs and arbitrary finite output alphabets.
For with ,
For a prime the paper defines the Bell expression
with when and , when and , otherwise, and for , for (zero otherwise).
Combined with Theorem 1, the goal identifies the exact detection-efficiency threshold of the maximally nonlocal two-party theory: . In particular the required efficiency tends to as the number of settings grows, so in principle no lower limit on detector quality is imposed by the no-signaling principle alone. The threshold is also a benchmark for quantum theory, where the best known efficiencies for few settings (for example with four settings each) stay well above it.
The result is proved in the paper; it has not been machine-checked. A formal proof yields a verified Bell inequality with outcomes per party together with a checked local bound valid for LHV models over arbitrary probability spaces, and a verified explicit no-signaling witness. The matching lower bound (Theorem 1) rests on a cited construction and is outside this mission.
The algebra of the witness (eqs. (13)–(15)) and the congruence argument (8)–(11) are elementary. The work is in the local bound. The paper disposes of general LHV models in one sentence ("LHV strategies can be regarded as the linear combination of deterministic strategies"). For hidden variables on an arbitrary probability space this is not a finite convex combination, and the step has to be carried out measure-theoretically. A proof that only treats finitely many hidden variables, or only deterministic models, proves a weaker statement. The deterministic case analysis must also be done carefully: the middle equality in the paper's display (12) is only valid when B answers on every input , although the final inequality is true in general.
The bound in the goal is reached through suprema and infima of real numbers. These must be handled through their set-theoretic characterisations; the set of efficiencies with a local model is nonempty because is always local.
Fin MA, Fin MB, and the paper's input is x.val + 1; both the congruence and the tests use this shift. Ordinary outputs of the Bell expression are Fin P read in ZMod P; the empty output is none in an Option type.sSup of a set that contains and is bounded by , and is sInf of the set of values over all output sizes Fin KA, Fin KB and all no-signaling behaviours.The goal cannot be satisfied by a degenerate reading: the efficiency set always contains , the class of behaviours is nonempty (the one-outcome box has ), and the infimum is taken over a set rather than an iterated infimum, so no empty index contributes the junk value .
The development needs finite sums and modular arithmetic from Mathlib, and Bochner integration on probability spaces. The definitions of behaviours, no-signaling, efficiency-degraded behaviours and LHV models are reusable for other Bell-test results, including the multi-party bounds of the same paper. Proofs of any milestone are welcome, as are proofs of the local bound for other Bell expressions built on the same definitions.
Public and healthcare services — driver's licence offices, emergency rooms, testing sites — are spread over a region, and customers choose for themselves which facility to visit. A customer weighs two costs: the travel distance to a facility and the expected wait once there. The wait depends on how many other customers chose the same facility. The resulting division of the region is therefore an equilibrium rather than a geometric given, and it can differ from the division a central planner would impose. Deciding when selfish choices are socially efficient, and how a provider should spend a fixed service budget across facilities, is a basic question in spatial queueing and service-system design.
J. G. Carlsson, X. Peng and I. O. Ryzhov (SSRN 4794156, later published in Manufacturing & Service Operations Management, 2024) model each facility as an M/M/1 queue and show three things. The decentralized equilibrium is an additively weighted Voronoi diagram. Locally optimal centralized partitions are also weighted Voronoi diagrams, with weights given by a gradient. And if the service rates are chosen to minimize total social cost, the decentralized equilibrium is exactly the planner's partition. The last statement is Theorem 6 of the paper and the goal of this mission.
A closed convex region carries a normalized demand : a probability measure on , absolutely continuous with respect to Lebesgue measure (the measure of the paper). Customers arrive at aggregate rate . There are facilities at points . A continuous metric gives travel distances . Facility serves at rate .
A partition of is a family of measurable sets covering whose pairwise intersections are -null. The area of is , the fraction of demand it holds. If facility serves the fraction , its expected waiting cost, scaled by , is
A decentralized demand equilibrium (1) under rates is a partition in which no customer prefers another facility:
For weights , the weighted Voronoi cell of facility is . The equilibria are the diagrams whose weights solve , condition (3).
The social cost (15) of rates and a partition is
minimized subject to the budget , where .
A general partitioning problem (9)–(12) minimizes over partitions. It carries a regularity condition: for , the law of with has a density.
Let be a local optimum of (15) with every area . Then a decentralized equilibrium under exists, and every such equilibrium satisfies
Since a global optimum is a local optimum, the best attainable social welfare is reached by decentralized customer behaviour once the rates are set correctly.
The result separates two sources of inefficiency in spatial service systems. When the rates are fixed badly, decentralized choice can be far from socially optimal: in the paper's §4.2 example, customers crowd a high-capacity facility while a nearby one is underused. Theorem 6 shows that the inefficiency is not in the customers' behaviour but in the capacity allocation. With the rates of (17), a square-root rule in the areas, the planner gains nothing by dictating assignments. Theorem 4 is of independent interest for computational geometry. It identifies the Voronoi weights of a locally optimal partition with the gradient of the area cost, which makes nonconvex area costs tractable.
None of these results has a machine-checked proof. The mission produces formal statements of the paper's chain, from the semi-discrete inner problem (Lemma 6) through the first-order condition (Theorem 4) to the identification (Theorem 6), and invites proofs of each. The rate step is closely related to Kelly's square-root capacity allocation (Kelly 1979, Theorem 4.1), which is already proved on the platform and is included as a referenced item.
The weighted Voronoi part and the algebra of (16)–(17) are elementary. The weight lies in Theorem 4 and Lemma 6. The obvious argument moves a small amount of demand from one cell to another and compares costs to first order. It shows only that no pair of cells can be improved. It does not give a single vector of weights consistent across all cells, and that is what Lemma 6 asserts: the existence of dual constants for a semi-discrete transport problem. Existence of such constants requires the regularity condition and positive areas, and fails without them. Theorem 5 must also cope with a cost that is nonconvex and differentiable only at positive areas, and with a joint neighbourhood in rates and partitions.
Lean works in EuclideanSpace ℝ (Fin n) with ν : Measure. Partitions are families Fin K → Set (E n) of measurable subsets of , covering , with -null pairwise intersections. Areas are (ν A).toReal. The waiting cost is real-valued: every equilibrium, feasibility condition and equilibrium-weight condition carries the stability conjunct , replacing the paper's . Under the goal's rates no equilibrium of the paper is lost by this. A local optimum means: for some , no feasible competitor with and for all is cheaper. Identities between partitions, and the pointwise conclusions of Lemma 6 and Theorems 4–5, hold up to -null sets. A null modification of an optimum is still optimal, so the pointwise readings are false.
Added hypotheses, each disclosed in the item: every (resp. ) is -integrable; the areas of the optimum in Theorems 5–6, and the prescribed areas in Lemma 6, are positive. The paper's positive intensity is dropped, and Theorem 4 asks only for continuous and differentiable at . Both changes weaken the hypotheses. The regularity condition is a push-forward measure absolutely continuous with respect to Lebesgue measure. The maps are continuous, so this condition is not vacuous.
A trivializing formalization is ruled out. The goal does not assume the optimum satisfies the Voronoi condition with weights (16), which would be Theorem 5. It quantifies over every decentralized equilibrium under and asserts that one exists.
Welcome contributions include semi-discrete optimal-transport duality (Lemma 6), nonatomic exchange arguments for partitions, and measure-level facts about weighted Voronoi diagrams. All of these are reusable well beyond this paper.
KellyReversibility.Allocation.optimal_capacity_allocation.The periodic-review inventory problem asks how much stock to order in each of periods when demand is random, unmet demand is backlogged, and both leftover stock and shortages are charged. When the demand distributions are known, a backward dynamic program computes an optimal policy, and the optimal policy is a base-stock policy: in each period, order up to a fixed target level (Zipkin, Foundations of Inventory Management, 2000). In practice the distributions are rarely known; what is available is data, or a simulator that produces demand scenarios.
Levi, Roundy and Shmoys (Math. Oper. Res. 32(4), 2007) asked how many sampled demand scenarios suffice to compute a policy whose expected cost is provably within a factor of optimal, with a sample size that depends on , the confidence , the horizon and the cost parameters, but not on the demand distributions. For the single-period newsvendor problem they proved such a bound for sample average approximation (their Theorem 2.2). For the multiperiod model they designed a new algorithm and proved the bound that this mission targets (Theorem 3.5 of §3.3).
Periods are indexed (the paper counts from ). The demand of period is a real random variable with law and finite mean, possibly negative. Demands of different periods are independent but need not be identically distributed. Orders arrive immediately, there is no ordering cost, and unmet demand is backlogged. Raising the inventory to in period costs, at the end of the period, with .
The algorithm (§3.3, p. 835). Given and , put , and . The paper states:
In stage , consider the function defined above with respect to the previously computed base-stock levels (where ). Use the black box to generate independent samples of the demands and compute . Note that in each stage, the algorithm is using an additional samples that are independent of the samples used in previous stages.
For , , independent demand laws with finite mean, and , the levels computed by the algorithm satisfy
Here is the expected cost of the computed policy and is the optimal expected cost. The constants are those of the paper; the goal fixes the algorithm, not a class of algorithms.
Hoeffding's inequality (Theorem 3.4) enters through Lemma 3.5; Concentration.hoeffding_two_sided is included as a reference item.
The theorem gives sample sizes that grow polynomially in , , and , and are uniform over all demand distributions with finite mean. The analysis shows that a sampled dynamic program need not lose control of convexity: the upper base-stock invariant keeps every stage a convex problem, and relative errors made in later stages multiply rather than compound through the recursion.
The result has been proved on paper since 2007. As far as a search of the platform shows (October 2026), none of its lemmas has a machine-checked proof; the platform has single-period newsvendor material from other papers, and a two-sided Hoeffding inequality. A formalization would supply a finite-horizon stochastic inventory dynamic program and its shadow version as reusable objects, a one-dimensional bridge from approximate first-order optimality to relative error (Lemma 3.3), and an end-to-end checked sample-complexity bound for a multistage stochastic model.
The naive argument estimates each stage's minimizer by sampling and adds up the per-stage errors. It fails twice. First, once a later stage uses an approximate level, the earlier stage's cost-to-go is no longer that of an optimal policy and need not be convex, so "the minimizer" may not exist and its sampled estimate has no guarantee. Second, an additive error in a later stage's cost can be amplified by the earlier stages. The paper's invariant, which requires each computed level to lie above the true shadow minimizer, controls both, and the formalization has to establish this invariant from samples with high probability. Measure-theoretically, the costs are nested expectations of infima, a one-sided derivative must pass through an expectation over a demand path, and stage-wise events must be combined although earlier levels are random.
HasDerivWithinAt on . Probabilities of events are measures of sets, which are outer measures on non-measurable sets.The symmetric traveling-salesman problem asks for a cheapest cycle through all vertices of a complete graph with real edge weights. Every exact method for it rests on lower bounds, and the most widely used one comes from Held and Karp's two papers of 1970–71 (Held & Karp 1970; Part II, 1971). Their bound is built from 1-trees, a slight variant of spanning trees that can be computed greedily, and is improved by perturbing the edge weights with vertex penalties .
The 1970 paper answers the natural question about this bound: when is the best 1-tree bound equal to the optimal tour weight? Its answer ties the combinatorial bound to the classical subtour-elimination linear program of Dantzig, Fulkerson & Johnson (1954): the best bound is the value of that linear program, and it closes the gap exactly when the program has an integral optimum. This identification, "Held–Karp bound = subtour LP value", is used throughout the later literature on TSP relaxations and integrality gaps.
Let be the complete undirected graph on the vertex set , , with an arbitrary real weight on each edge ; no sign, metric or integrality condition is imposed. The weight of a subgraph is the sum of its edge weights. A tour is a cycle through every vertex exactly once. A 1-tree is a tree on the vertex set together with two distinct edges at vertex .
For a real vector the transformed weights are . The gap function is
Write for the weight of a minimum tour under , and, indexing the 1-trees by with weight and degrees ,
Vectors live on the edges of , with and degree at vertex . The integer program (3) asks for degree at every vertex, the subtour constraints for every nonempty proper subset , and integrality; its feasible points are the tours. Its rewritten form (3′) has (i) degree at , written ; (ii) ; (iii) ; (iv) the subtour constraints; (v) ; (vi) ; (vii) integrality. The paper denotes (ii)–(v) by . The linear program (4) is
This is the abstract's headline, " precisely when a certain well-known linear program has an optimal solution in integers", stated in the paper's own form.
The result. Theorem 2 says that the best lower bound obtainable from 1-trees with vertex penalties equals the optimal value of the subtour linear program. The bound can therefore be computed either combinatorially, by ascent over with minimum-spanning-tree computations, or by linear programming, and any statement about the integrality gap of the subtour LP is a statement about the Held–Karp bound. Corollary 1 is the exact criterion for when the bound is tight: the gap closes precisely when the LP has an integral optimal solution, in which case that solution is an optimal tour. Theorem 1, a description of the 1-tree polytope by linear inequalities, is the polyhedral fact underneath.
Formalizing it. The results are classical and proved on paper. As far as the platform's catalog shows, none of them is machine-checked. The published Part II mission (HeldKarp.Ascent) formalizes the ascent method and the bound tour weight; this mission adds the polyhedral side: the subtour LP, the 1-tree polytope, and the equality of the bound with the LP value. A complete development yields a reusable statement of LP-based lower bounds for the TSP on general real weights, which existing metric-TSP items do not cover.
Lemma 1, the identity , Lemma 2 and the tour correspondence are finite bookkeeping over graphs and edge sums. The substance is Theorem 1. The paper proves it as a special case of Edmonds' theorem on matroid base polytopes (§6, p. 1157), applied to the 1-tree matroid; formalizing that route requires the base-polytope theorem for a matroid that Mathlib does not provide. The printed specialization also has a gap (finding F3): the list of spans of the 1-tree matroid on p. 1157 omits the single edges , so the system it lists has a non-1-tree vertex already for . Theorem 1 itself is unaffected, because (3′) contains , but a proof that follows the page sentence by sentence will fail at that step. Theorem 2 rests on linear-programming duality for a program with equality constraints, which has to be available in the form the argument uses, and on Theorem 1; attainment of both the maximum and the minimum is part of the statement and has to be proved, not assumed.
Vertices are Fin n; the paper's vertex is 0 : Fin n and vertex is the last element lastV n. Weights are a function c : Sym2 (Fin n) → ℝ on unordered pairs, so symmetry is built in and the diagonal is never used. Tours, 1-trees, the weight of a subgraph and (oneTreeBound) are the published definitions HeldKarp_Ascent_IsOneTree and HeldKarp_Ascent_oneTreeBound of the Part II mission. The new definitions are HeldKarp_Gap_GapFunction (transformed weights, minimum tour and 1-tree weights, the gap) and HeldKarp_Gap_SubtourLP (edge vectors on the type Edge n of unordered pairs with , degrees, the programs (3), (3′) and (4), optimality, incidence vectors).
Conventions committed to:
These choices rule out the trivializing formalizations: with the gap is identically while (4) is infeasible; with allowed every program is infeasible; with (ii)–(iii) as inequalities Theorems 1 and 2 fail; with optimality among integer points only, the right side of Corollary 1 always holds; and defining as would empty milestone 2.
A complete development needs finite sums over Sym2, simple-graph trees and cycles, extreme points of polyhedra (Set.extremePoints), and linear-programming duality. The 1-tree polytope description and an LP duality statement with equality constraints are reusable beyond this mission. Proofs of any milestone, alternative routes to Theorem 1 that avoid matroids, and a formal account of the §6 matroid theorem are all welcome.
Assignment questions ask whether every member of a family can be served by a different resource: committees that each need a distinct member as representative, or tasks that each need an admissible worker. The classical answer is Hall's theorem (Hall 1935): a family of sets has a system of distinct representatives exactly when every of its sets together contain at least elements. Operations research needs more than that. Representatives may be allowed to serve several sets within prescribed bounds, some elements may be required to appear, two families may have to be served by one common list, and the representatives may have to meet each class of a partition a bounded number of times.
Chapter II, §10 of Ford and Fulkerson's Flows in Networks (RAND Report R-375-PR, 1962; Princeton University Press, 1962) derives all of these as feasibility statements for network flows. The section collects results of Hall (1935), Mann and Ryser (1953), Hoffman and Kuhn (1956) and Ford and Fulkerson (1958). Its last results are the common system of restricted representatives theorem and the partition-constrained theorem of Hoffman and Kuhn.
Fix a fundamental set , with the element identified with its index . A family is a list of subsets of indexed by ; two indices may carry the same set. For , the index set is the set of indices of the elements of , and .
A list of representatives is a choice of elements of , where represents . The number of occurrences of is the number of indices with .
For , denotes the index set of when it refers to .
A common SRR for and in which occurs at least and at most times exists if and only if, for every ,
The bounds are integers with ; the instance reads .
In attack order:
for all and .
These theorems are the combinatorial face of the integral flow theorems of the same chapter. The SRR theorem governs many-to-one assignment with quotas, where each resource must be used between a minimum and a maximum number of times. The marginal-element theorems decide when a prescribed set of resources can all be used; Mann and Ryser applied their sufficient condition for this to Ryser's theorem on extending Latin rectangles to Latin squares (p. 62). The common SRR theorem decides when two families can be served by one list, the setting of simultaneous assignment along two classifications. Theorem 10.10 adds quotas per class of a partition of the resources. Corollary 10.4 is König's edge-colouring theorem for regular bipartite graphs, in matrix form.
All of these results are classical and proved. Hall's theorem is in Mathlib and is referenced here. As far as a search of the platform shows, none of the quota, marginal-element, common-representative or partition versions has a machine-checked statement or proof. The mission produces faithful statements of the book's §10 results on a shared set of definitions, and invites formal proofs of them.
Necessity of each condition is a counting argument. Sufficiency is the content, and the natural first idea does not work. Applying Hall's theorem to a family in which each set is repeated according to its bounds handles upper bounds but not lower bounds. The two families of the common problem cannot be treated separately either: an SRR for and an SRR for with the same occurrence counts need not combine into one list, because the identification of positions must respect both families at once. In the book every sufficiency proof passes through an integral feasible flow or circulation, and the cut conditions of the circulation theorem must be reduced case by case to the stated inequalities.
is Fin m and a family is Fin n → Finset (Fin m), indexed from . A list of representatives is a function Fin n → Fin m, an SDR is an injective one, and the occurrence count is a Finset.card. A common SRR is a pair of a list and an Equiv.Perm (Fin n). The index set is X.biUnion S. The occurrence bounds are natural numbers. The page states only , but the bounds count occurrences, and with real bounds Theorems 10.5 and 10.8 are false. Every inequality involving subtraction is evaluated in , so no term truncates at zero. The partition in Theorem 10.10 has nonempty, pairwise disjoint blocks covering . In Corollary 10.2 the maximum runs over all (); the page prints as the last index. In Theorem 10.10 the first union is over ; the page prints .
The trivializing formalizations are ruled out explicitly. An SRR without the occurrence bounds, and a "common SRR" consisting of two unrelated SRRs, are both excluded: the definitions carry the bounds, and a common SRR is one list whose entries each represent one set of each family through the permutation .
Beyond the paper. Two sharpness probes restate Theorems 10.5 and 10.8 with real bounds . Both are expected to be false: with , , and , , the conditions hold while no list of length one contains both elements. Disproofs are the sought outcome.
A complete development needs Hall's theorem (available in Mathlib) and, for the book's route, an integral flow or circulation feasibility theorem; purely combinatorial proofs by induction are equally welcome. The definitions are reusable for the zero-one matrix results of the following sections. Proofs of individual milestones are welcome, in any order.
A Markov decision process (MDP) with the average cost per unit time criterion models a controller who runs a stochastic system indefinitely and cares about long-run cost rather than any finite horizon: inventory control, queueing control, and maintenance are standard examples. The basic questions are whether an optimal policy exists, whether it can be taken stationary (a fixed measurable rule ), and whether it is characterized by an average cost optimality inequality (ACOI).
For uncountable state spaces the classical answer is Schäl's (Math. Oper. Res. 18, 1993), under weak continuity of the transition probabilities, compact action sets, and a uniform bound on the relative discounted values. Hernández-Lerma replaced compactness by inf-compactness of the cost in the action, but under setwise continuity; Feinberg and Lewis (Math. Oper. Res. 32, 2007) allowed noncompact actions under weak continuity, at the price of inf-compactness of the cost in state and action jointly plus a local boundedness condition. That joint inf-compactness excludes bounded costs on unbounded state spaces, the setting of Ross and of Dynkin and Yushkevich. Feinberg, Kasyanov and Zadoianchuk (Math. Oper. Res. 37(4), 2012) remove both restrictions.
The state space and action space are Borel subsets of Polish spaces. Each state has a nonempty Borel set of available actions; the graph is Borel and has a measurable selector. Choosing at costs (bounded below, measurable) and moves the system according to a transition probability . A policy is a sequence of randomized, history-dependent decision rules concentrated on ; the set of stationary policies consists of Borel maps with .
For the discounted cost is and the average cost is . Optimal values are infima over all policies: , , and . Put , the relative discounted value , and .
The assumptions are:
The candidate relative value function is the joint lower limit
and the candidate optimal actions are .
Under (W*) and (B̲) there is with
and for it for all . Moreover (a) is finite and lower semicontinuous; (b) each is nonempty and compact and is Borel; (c) every selecting from is average cost optimal and satisfies the inequality; (d) some selects from the minimizer sets of ; (e) under (Wu), is inf-compact.
In the paper's order: Theorem 1 (the inequality with implies optimality), Lemma 2 (inf-compactness in the action), Lemma 3 (lower semicontinuity of the minimal value and a Borel minimizer), Lemma 4 (a Fatou lemma for weakly converging measures, already on the platform as Schäl's Lemma 2.3(ii)), Theorem 2 (i), (iv)–(vi) (the discounted problem under (W*)), Lemma 6 (semicontinuity of , and the auxiliary ), Corollary 1, and Lemma 7, the ACOI itself. Schäl's inequality is referenced as an existing platform item.
Theorem 3 gives stationary average-cost optimal policies for weakly continuous MDPs with noncompact action sets and costs that need not be inf-compact in the state, which covers bounded costs on unbounded state spaces and inventory models whose holding costs do not grow without bound. Assumption (B̲) asks only for a finite lower limit of as , weaker than Schäl's uniform bound. The approach was extended to partially observable MDPs and to later work on the average cost optimality equation, which builds on exactly these objects.
The theorem is proved in the literature; nothing here is open mathematically. What the mission adds is a machine-checked proof of the full chain from measurable selection and semicontinuity through the vanishing-discount limit, for Borel spaces and history-dependent randomized policies. Reading the proofs closely has turned up three printed statements that are false as written (see Beyond the paper); a formal development settles exactly which hypotheses each step needs.
The obvious route takes a limit of discount-optimal policies as . With noncompact such a sequence need not have any limit point; (W*)(ii) supplies one only when the costs along it stay bounded, and that has to be extracted from the relative values. The second obstacle is that is controlled only through its lower limit at each point, so is a joint lower limit in and passing it under requires a Fatou-type lemma for weakly converging measures rather than dominated convergence. Finally, selecting a Borel from the sets requires a uniformization theorem for Borel sets with -compact sections (Arsenin–Kunugui), which Mathlib does not have.
The spaces are types with a separable metrizable topology whose Borel -algebra is standard Borel (by Lusin–Souslin, exactly the Borel subsets of Polish spaces up to homeomorphism). The model reuses the published definitions FeinbergLiang_ACOE_MDP (policies, path measures via Ionescu–Tulcea, discounted and average costs) and SchalAvg_AvgOpt_Model (action sets, admissible policies, , , , , , Assumption (G)). Conventions:
HasSelector.Optimal values are infima over all admissible (randomized, history-dependent) policies, not over stationary ones. is the fixed function (21), never a free parameter. All four equalities of (10) are stated for every . (W*), (Wu) and (B̲) constrain and on only. A statement that ranged over a smaller policy class, left free, kept a single equality, or imposed continuity on all of would be a different and easier theorem.
A complete development needs: semicontinuity and inf-compactness calculus for -valued functions; lower semicontinuity of under weak convergence for lower semicontinuous ; the Arsenin–Kunugui uniformization theorem; discounted dynamic programming on Borel spaces; and an Abelian/Tauberian comparison of with Cesàro averages. The first three are reusable well beyond MDPs. Contributions to any milestone, or to these libraries, are welcome.
Beyond the paper. Three corrected variants are posed beside the faithful statements, which stay as printed. Lemma 2, corrected: as printed it assumes only (W*)(ii) (and (iii)), but without lower semicontinuity of a level set such as need not be compact; the variant adds (W*)(i). Lemma 3, corrected: can fail because may be identically for some ; the variant asserts lower semicontinuity only. Corollary 1, corrected: the joint limit need not exist (a one-action example with an indicator cost); the variant uses the lower limit, which is what the proof computes and what Lemma 7 uses. A misprint in the proof of Lemma 3 (p. 598, for ) does not affect its statement.
A convex optimization problem can be handed to a semidefinite programming solver only after its constraints and objective have been written as linear matrix inequalities (LMIs): conditions of the form , where is affine in the decision variables and in auxiliary variables , and means positive semidefinite. A large share of modern engineering optimization is built this way, in robust control, structural design, and statistics and machine learning (nuclear-norm and spectral-norm regularization, eigenvalue optimization). Modeling tools such as CVX and YALMIP rest on a catalog of functions known to admit such a description.
Lecture 4 of A. Ben-Tal and A. Nemirovski, Lectures on Modern Convex Optimization (SIAM, 2001, doi:10.1137/1.9780898718829), builds that catalog for the semidefinite cone. Its central entry is a general rule: a convex function of a symmetric matrix that depends only on the eigenvalues, symmetrically, is expressible by LMIs whenever the underlying function of a vector is. This covers the largest eigenvalue, sums of the largest eigenvalues (Ky Fan, 1949), Schatten norms and powers of the determinant at once. The tool behind it is the theory of majorization (Hardy, Littlewood and Pólya, 1929; Rado, 1952) together with Birkhoff's theorem on double-stochastic matrices (1946).
For a symmetric real matrix , denotes its eigenvalues counted with multiplicity in nonascending order, . is the sum of the largest. For a vector , is the sum of its largest entries, and is the convex hull of the coordinate permutations of . A function is symmetric if permuting the coordinates of its argument leaves its value unchanged. A matrix is double-stochastic if its entries are nonnegative and every row and column sums to .
A function is semidefinite representable (SDr) if there is a map , affine in with values in the symmetric matrices, such that
For a matrix (), the singular values are , and .
Let be symmetric and SDr with representation . Then for every symmetric matrix and real ,
FamousTheorems.birkhoff_von_neumann.A strengthened variant of the goal states that (4.2.3) remains exact when the ordering constraint is removed.
The result itself. Proposition 4.2.1 reduces semidefinite representability of a spectral function on , a space of dimension , to semidefinite representability of a symmetric function on . The extra cost is scalar variables, ordering inequalities, Ky Fan constraints (each an LMI of size by 18.c) and one trace equation. The representation is explicit, so a modeling language can generate it mechanically. Proposition 4.2.2 does the same for functions of singular values, which covers the nuclear norm and the operator norm of rectangular matrices. Fact (D) is the variational description that makes convex (Davis, 1957; Lewis, 1996).
Formalizing it. All results here are classical and proved in the book, partly through exercises (4.14–4.16 for the goal). None of them is formalized on Prove2Me beyond Birkhoff's theorem, which Mathlib has as doublyStochastic_eq_convexHull_permMatrix. A related proved platform item, Matrix.IsHermitian.sorted_eigenvalues_le_add_of_re_dotProduct_le, is a Weyl-type inequality that implies (A) when its slack is zero. Mathlib has sorted eigenvalues of Hermitian matrices (eigenvalues₀) but no Ky Fan sums, no majorization theory and no notion of semidefinite representation. This mission produces them.
The forward direction of every representation is a choice of witness. The content is in the converse: from an arbitrary feasible point of the LMI system one must recover the inequality for the eigenvalues. For (4.2.3) this means showing that partial-sum domination plus equal totals places inside the convex hull of the permutations of the witness . The obvious coordinatewise comparison fails, because is not dominated entrywise by . The hard half of the majorization principle (Exercise 4.15) is this step, and it does not follow from convexity of alone. In Proposition 4.2.2 the witness only dominates the singular values in partial sums, with no equality of totals, so majorization alone does not suffice there.
Vectors are Fin m → ℝ (0-based indices) and matrices Matrix (Fin m) (Fin m) ℝ. Symmetric means Matrix.IsHermitian and means Matrix.PosSemidef, which includes symmetry. is Mathlib's antitone IsHermitian.eigenvalues₀; it is applied only to symmetric matrices. Functions with values in are EReal-valued and never , and only order comparisons with real numbers are made on them. A representation is an explicit affine map with symmetric coefficient matrices. In Proposition 4.2.2 the function , given on only, is extended by outside . The singular values are written as , which equals . Typos on the page are corrected and listed in the items: for in 18.c, and and in Proposition 4.2.2.
The claim " is SDr" admits a trivializing formalization: asserting that some LMI system projects onto the epigraph, with no control over its shape or size, says nothing beyond convexity. Every statement here instead pins the representation down as the book's explicit system (4.2.2), (4.2.3) or (4.2.4), quantified over every symmetric matrix and every real .
Beyond the paper. One strengthened variant is posed: Proposition 4.2.1 with the constraint removed from (4.2.3) (finding F1). The evidence is that never exceeds the sum of the largest entries of , so the remaining constraints already express majorization. The variant is not a milestone, and the book's statement stays the goal.
A complete development needs:
Majorization, the Ky Fan representation and fact (A) are reusable well beyond this chapter, for instance in eigenvalue optimization and the analysis of interior-point methods. Contributions of these as standalone results are welcome.