Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
The Schur basis on n d-dimensional quantum systems is a generalization of the total angular momentum basis that is useful for exploiting symmetry under permutations or collective unitary rotations. We present efficient (size poly(n,d,log(1/ε)) for accuracy ε) quantum circuits for the Schur transform, which is the change of basis between the computational and the Schur bases. These circuits are based on efficient circuits for the Clebsch-Gordan transformation. We also present an efficient circuit for a limited version of the Schur transform in which one needs only to project onto different Schur subspaces. This second circuit is based on a generalization of phase estimation to any nonabelian finite group for which there exists a fast quantum Fourier transform.
This mission is the statement-level formalization of Efficient Quantum Circuits for Schur and Clebsch-Gordan Transforms (arXiv:quant-ph/0407082v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The qubit CG step is three logical register operations (Eq.(6), Fig.1; continued on PDF p.3, 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.
6 results of the paper are not stated yet, because the library lacks an interface they need:
Graph neural networks and geometric learning on meshes rely on operators that combine the features of a node with those of its neighbours. The graph Laplacian is the oldest such operator: it is the discrete analogue of the Laplace–Beltrami operator of a surface, and its eigenvectors play the role of a Fourier basis on a graph. Early spectral graph networks (Bruna et al., 2013) learned filters directly in that eigenbasis. Such filters are expensive, since they need an eigendecomposition, and they do not transfer between graphs. Defferrard, Bresson and Vandergheynst (2016) replaced them with polynomial filters . These are computed with sparse matrix products, and their output at a node depends only on a bounded neighbourhood of that node.
This mission formalizes Section 4.6 of the book Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges by Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2). The section introduces the weighted Laplacian (24) and the spectral and polynomial filters built on it, and states that a polynomial filter of degree is localised in the -hop neighbourhood. The section closes with the view of meshes as operators , which leads to remeshing invariance and to the result of Wang et al. (2019a) that remeshing-invariant functions depend only on the spectrum. The book numbers no theorems, lemmas or definitions, so every item of this mission is cited by section, equation number and printed page.
There are nodes . A weight matrix assigns a weight to each ordered pair of nodes. The neighbourhood of is . Node features form a matrix whose row is the -dimensional feature vector of node .
The degree of is , and the degree matrix is . The Laplacian is
The graph is undirected when ; then is symmetric and has an orthonormal eigenbasis with and . The Fourier coefficients of are .
Given a degree and real coefficients , the polynomial filter is
Hops are measured in a simple graph on the nodes that carries the weights: with implies that and are adjacent. A node is within hops of if some walk in from to has length at most .
A permutation of the nodes acts by its permutation matrix , with and . A function of matrices is remeshing invariant if for every orthogonal . A matrix-valued is remeshing equivariant if .
If and agree at every node within hops of , then
for every choice of . This is the book's sentence "since the Laplacian is local, a polynomial filter of degree is localised in -hop neighbourhood". The statement fixes no coefficients and no graph family.
The result. Locality is what separates polynomial filters from general spectral filters. A spectral filter with an arbitrary transfer function is a dense matrix: every output depends on every input. A degree- polynomial filter has support inside the -hop neighbourhood, so it costs sparse matrix products and has a receptive field controlled by . Milestone 4 shows that the same object is also a spectral filter, with transfer function . A polynomial filter is therefore both a spectral filter and a message-passing operation. The book's discussion of rational filters on the same page, which have exponential decay but no local support, uses this contrast. The remeshing companions give the reason spectral constructions are used across different meshes: a remeshing-invariant function of the operator sees only the spectrum.
The formalization. The mathematics is classical, and the mission is about formalizing it. Mathlib has the unweighted combinatorial Laplacian SimpleGraph.lapMatrix and the spectral theorem for Hermitian matrices. The platform has a proved theorem counting walks with powers of an unweighted adjacency matrix. Neither gives the support of powers of a weighted Laplacian, whose nonzero diagonal is not covered by walk counts of a fixed length. None of the statements here is formalized on the platform. The mission produces a reusable support lemma for matrix polynomials of a graph-supported matrix, and a link between spectral and polynomial filters in the matrix language used by graph neural networks.
A first attempt identifies with a count of walks of length exactly , as for the adjacency matrix. That identification fails here. has the diagonal entries , so sums over walks that may pause at a node, and it can be nonzero for at any distance up to . The claim is therefore "within at most hops", and the induction has to track walks of length at most through a matrix with nonzero diagonal. Two encodings make the claim easy and wrong. Mathlib's SimpleGraph.dist is for unreachable pairs, so "" would place every unreachable node inside the neighbourhood. A filter defined through the eigendecomposition is not visibly local, so the locality statement has to be about itself. For the companions, the difficulty is the spectral theorem and the fact that two symmetric matrices with the same characteristic polynomial are orthogonally similar, which requires matching eigenvalue lists up to a permutation.
Matrices are Matrix (Fin n) (Fin n) ℝ, and features are Matrix (Fin n) (Fin d) ℝ, with rows as nodes. The Laplacian is the published definition SpectralSparsify.Sampling.lapMat (degree matrix minus weight matrix), referenced rather than redefined and used under the local name lap. It imposes no condition on . A diagonal weight cancels in . Symmetry is assumed only where the book needs it: the side-note on p. 64. The polynomial filter is the explicit sum with coefficients indexed by . "Within hops" is the existence of a walk of length at most in a simple graph that contains the support of . The goal is stated for every such and for non-symmetric . Both are generalisations of the book's undirected setting, where is the graph of . Permutation matrices act by moving row to row . Remeshing invariance quantifies over all of Mathlib's orthogonalGroup. "The same spectrum" is equality of characteristic polynomials of symmetric matrices.
A trivializing formalization is ruled out: the filter is not defined through an eigendecomposition, "localised" is not defined as "is a polynomial in ", and the hop condition is not stated through the junk-valued SimpleGraph.dist.
A complete development needs the support of products of graph-supported matrices, the spectral theorem in orthogonal form (Mathlib's Matrix.IsHermitian.eigenvectorUnitary), and orthogonal similarity of symmetric matrices with equal characteristic polynomials. The support lemma is reusable for any message-passing operator that is a polynomial in a local matrix. Contributions of these lemmas, and alternative proofs (for example through Polynomial.aeval), are welcome.
Many graphs that graph neural networks (GNNs) are applied to are embedded in space. In a molecular graph the nodes are atoms, and each atom carries both chemical information (its type) and its three-dimensional position. A prediction about the molecule (an energy, a binding affinity) must not depend on where the molecule sits or how it is oriented, and a predicted geometry must move with the molecule. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2, 2021) treats this in §5.5, Equivariant Message Passing Networks: a layer on such graphs should be equivariant to the Euclidean group E(3) of rigid motions "in addition to the standard permutation equivariance discussed before" (p. 83). The book presents the layer of Satorras, Hoogeboom and Welling, E(n) Equivariant Graph Neural Networks (ICML 2021, arXiv:2102.09844), and asserts that it has this property.
The layer is built from the most general of the three "flavours" of GNN layer that §5.3 uses to organise the literature: convolutional, attentional and message passing. This mission therefore also formalizes the two claims of §5.3 that the E(3) layer relies on: message passing is permutation equivariant, and it contains the other two flavours.
The book numbers no theorem, lemma or definition. Every item of this mission is cited by section, equation number (where there is one) and printed page.
A graph on the nodes is given by an adjacency matrix , with an edge whenever . The neighbourhood of is (eq. (11), p. 34). Each node carries a feature ; collected as rows they form the feature matrix . A permutation of the nodes, with permutation matrix , acts by and . A layer is permutation equivariant if (eq. (10), p. 33).
A permutation-invariant aggregator is a function of the multiset of incoming values ("sum, mean, or maximum", p. 78). The three flavours of §5.3 (p. 79), with an update function , are
convolutional with fixed coefficients , attentional with an attention mechanism of the features, and message passing with a message function of receiver and sender.
In §5.5 each node carries features and spatial coordinates . An element acts on coordinates by , "where is an orthogonal matrix modeling rotations and reflections, and is a translation vector" (p. 83). The equivariant message-passing layer (p. 84) is
with and "two distinct (learnable) functions", scalar-valued. The book's desired property (p. 83): if the spatial input is transformed by , "the spatial component of the output transforms in the same way (as ), whereas remains invariant."
For every orthogonal and , applying the layer to gives with
The statement holds for arbitrary , , and ; nothing about the learnable functions is fixed.
The equivariance of the layer is what lets a network built from it be applied to molecules and point clouds without data augmentation over rotations, reflections and translations: invariant outputs are unaffected by the placement of the input, and coordinate outputs move with it. Satorras et al. use the layer, stacked, for molecular property prediction, dynamical systems and graph autoencoders; the equivariance of the stack follows from that of each layer. The containment of the three flavours explains why the book can discuss GNN expressivity (Ch. 7, chunk IX of this series) for message passing alone.
The results are known and their proofs are short computations; none of them has a machine-checked proof on the platform. Formalizing them pins down what the claims mean exactly: that the reflections in are included, that the translation enters the coordinate update only through the leading , and under which condition on the features the containment "convolution ⊆ attention" actually holds.
The mathematics is elementary; the difficulty is in stating the claims at the generality the book uses. The coordinate update is not a function of distances alone: it is linear in the difference vectors , and equivariance rests on being scalar-valued and on the translation cancelling in every difference but surviving in the leading term. The containment "convolution ⊆ attention" fails as a literal identity when two nodes have equal features but different coefficients , since an attention mechanism sees only features; the book's look-up table needs features that identify the nodes. The two halves of the layer aggregate over different index sets ( and all ), so the layer is message passing on two different graphs.
Nodes are Fin n. Node features are a family Fin n → α (for this is the book's matrix , Matrix (Fin n) (Fin d) ℝ). The aggregator is an arbitrary function Multiset M → M' of the multiset of messages, so its permutation invariance holds by construction. A permutation acts by (PX)_u = X_{σ⁻¹(u)} and (PAPᵀ)_{uv} = A_{σ⁻¹(u)σ⁻¹(v)}. Coordinates live in EuclideanSpace ℝ (Fin 3); ranges over Matrix.orthogonalGroup (Fin 3) ℝ, the whole of including reflections, acting through Matrix.toEuclideanLin. The squared norm is kept as printed. No standing assumption of the section restricts or ; is allowed.
The layer takes the coordinates themselves as input. A formalization that fed the layer only the distance matrix would make the feature half trivially invariant and drop the coordinate half; that encoding is ruled out.
One hypothesis is added relative to the page, in milestone 3 only: the features must be pairwise distinct (Function.Injective X) for convolution to be represented by attention or by message passing. Without it the claim is false, and a two-node counterexample is checked in Lean. The inclusion of attention in message passing needs no hypothesis.
The definitions of this mission (neighbourhoods, the permutation action, the three flavours) duplicate objects of chunk II of this series; drafts cannot import drafts, and the duplicates are to be merged after the series is published. Proofs of every item are welcome; the distance lemma, the orthogonal-matrix isometry and the multiset reindexing under a permutation are reusable beyond this mission.
A finite-energy pseudoholomorphic curve in the symplectization of a strictly star-shaped hypersurface approaches, near a non-removable puncture, a periodic Reeb orbit . The previous mission in this series formalizes this in the form of C. Wendl's Lectures on Symplectic Field Theory, Theorem 9.8: along suitable sequences of loops around the puncture the curve converges to the orbit. Most applications need much more precise information about the end. H. Hofer, K. Wysocki and E. Zehnder showed in 1996 (Ann. IHP 13) that at a nondegenerate orbit the convergence holds for the whole end and is exponentially fast, and that the leading term of the difference is times an eigenvector of the asymptotic operator ; R. Siefring sharpened the formula to its present form. The asymptotic eigenvector is the input for winding numbers, fast planes and the intersection theory of punctured curves, for example in U. Hryniewicz's characterization of the Reeb orbits that bound disk-like global surfaces of section (arXiv:1105.2077).
This mission formalizes these asymptotic results in general dimension, in the setting of the previous mission. It follows Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, § 2.2.3 (Definitions 2.5 and 2.9, Theorem 2.11, Lemma 2.12), and the linear theory of C. Wendl's Lectures on Symplectic Field Theory (2026 notes, §§ 4.6 and 4.8). It is the eighth mission in a series on symplectic field theory.
All objects are those of FiniteEnergyPlane_Setting: , a strictly star-shaped level with Reeb field and contact planes , a compatible complex structure on , the symplectization structure on , and finite-energy curves.
Let be a finite-energy -holomorphic curve on the punctured unit disk , and let be a nondegenerate puncture of , asymptotic to a periodic Reeb orbit with sign . Then converges to the trivial cylinder over exponentially fast in . If moreover does not vanish identically near , then has an asymptotic eigenvalue with and an asymptotic eigenvector of at (Hryniewicz, Theorem 2.11 and Lemma 2.12).
HryniewiczCriterion setting.The results. The goal is the standard description of a finite-energy end used throughout symplectic field theory: it is what makes the asymptotic eigenvalue, the winding of the asymptotic eigenvector, the asymptotic Conley–Zehnder index and the asymptotic intersection theory of punctured curves meaningful. The goal does not assume that the limit orbit is nondegenerate, only that the end decays exponentially; this hypothesis is part of the definition of fast planes over possibly degenerate orbits (Hryniewicz, Definition 2.14). Milestone 12 is the form in which planes asymptotic to nondegenerate orbits are used, and milestone 13 connects it to the open HryniewiczCriterion mission. Milestones 6–8 are results about linear Cauchy–Riemann equations on a half-cylinder, independent of the geometry.
Formalizing them. All results are classical and proved in the cited sources (the linear results in Wendl's notes and in R. Siefring, Relative asymptotic behavior of pseudoholomorphic half-cylinders, CPAM 61 (2008)). None of them has been formalized in a proof assistant, as far as a literature search shows; Mathlib has no asymptotic operators of Reeb orbits and no theory of Cauchy–Riemann equations on cylinders.
The asymptotic operator acts on sections of along the orbit, defined intrinsically in with no preferred frame, and its spectral theory lives on loops in a moving subspace. The hypothesis of the goal is only exponential convergence, while the conclusion is convergence and a precise leading term with a single eigenvector. The eigenvector formula is stated in a tube around the orbit with its own phase function , so the leading term is measured transversally to the orbit rather than against the parametrization . For multiply covered orbits the tube is only a covering of a neighbourhood of the orbit, and the phase is a real lift.
FiniteEnergyPlane; the definition module FiniteEnergyPlane_Asymptotics imports FiniteEnergyPlane_Setting (previous mission) and CauchyRiemannIndex_Setting (fifth mission) for Mat n, J₀ n, Vec n, IsSymLoop, IsNondegenerate and crOp. The bridge item also imports HryniewiczCriterion_ConleyZehnder.iteratedFDeriv and require smoothness on some . Matrix-valued convergence is entrywise.Contributions welcome: general lemmas on linear ODEs along periodic orbits and on smooth families of subspaces over the circle.
Max Tegmark's letter "On the dimensionality of spacetime" (Classical and Quantum Gravity 14 (1997) L69-L75) is the standard reference for the anthropic selection argument on the dimensionality of spacetime. Many superstring theories and inflationary models predict not a single classical spacetime but an ensemble of effective low-energy worlds with different numbers n of space and m of time dimensions, together with a probability distribution over the pairs (n, m). Tegmark argues that this failure to predict (n, m) = (3, 1) uniquely is a strength rather than a weakness: the selection effect arising from the fact that only some worlds contain self-aware observers collapses the distribution, so that such an ensemble theory may predict that we should find ourselves inhabiting a (3 + 1)-dimensional spacetime with 100% certainty, the Bayesian prior probabilities being completely irrelevant.
The letter's argument has three prongs, and the mission formalizes the mathematical content of each. More or less than one time dimension destroys predictability: the partial differential equations of nature have the hyperbolicity property that makes initial-value problems well posed only when m = 1; with no time dimension the equations are elliptic and an observer could not make any inferences at all about other parts of space from local data; with two or more time dimensions no hypersurface carries well-posed data. More than three space dimensions destroys stability: the Green's function of the Poisson equation scales as the (2 - n)-th power of the radius, the two-body problem has no stable orbit solutions for n > 3, and, by the quantum counterpart the letter cites (Tangherlini), no traditional atoms exist. Fewer than three space dimensions destroys complexity: the letter conjectures that such worlds are too simple and barren to contain observers, citing the absence of gravitational force in general relativity with n < 3 and the topological problems of two-dimensional organisms.
The goal statement of the mission is the Bayesian capstone: in a world ensemble whose observer worlds satisfy the three prongs, the probability of being an observer in a (3, 1)-dimensional world equals the probability of being an observer, so that conditional on observerhood the dimensionality is (3, 1) with probability one. The milestones are the classification trichotomy of the field equations, the space-time symmetry of the classification, the hyperplane obstruction behind the letter's Asgeirsson discussion, the spacelike slice of the single-time world, the predictability equivalence, the harmonicity of the Green profile, and the orbit-stability dichotomy.
The source document is the uploaded letter (tegmark1997.pdf in the mission materials).
The formalization is a three-layer development in the namespace Tegmark. The signature layer (Tegmark_sig) fixes the coordinate model: a world with n space and m time dimensions is the coordinate space over the disjoint union of the n space directions and the m time directions, carrying the quadratic form teg that counts space coordinates positively and time coordinates negatively, so that a single minus sign distinguishes space from time. The layer defines the spacelike and timelike classification of vectors and submodules, the elliptic, hyperbolic, and ultrahyperbolic classes of the field equations, the hyperplanes on which initial data can be posed, and the predictability requirement. The physics layer (Tegmark_phys) carries the Newtonian potential of a point mass in n dimensions — the Green's-function scaling of the Poisson equation — the effective potential of the two-body problem with its circular-orbit and stability criteria, and the radially reduced Laplace equation with the Green profile. The ensemble layer (Tegmark_ensemble) carries the probability space of worlds with the two dimension counts and the measurable observer event.
The following choices are disclosed explicitly.
Compile verification by CI substitution. The authoring environment has no local Lean toolchain, so the compile check demanded by the mission is performed by the continuous integration of the repository (Lean 4.33 with Mathlib): all Lean code below was compiled there before this proposal was submitted, and the code attached to the items is byte-identical to the compiled modules.
The theorem drafts carry sorry. The eight theorem statements are submitted as drafts for human review; each proof body is a single sorry marking the work the mission proposes to complete. The compilation therefore succeeds with exactly one "declaration uses 'sorry'" warning per theorem file.
The coordinate model. A world with (n, m) dimensions is the flat coordinate space over the disjoint union of the n space directions and the m time dimensions, with the signature form. This is the linear-algebra skeleton of the letter's discussion: the classification of the field equations by the eigenvalue signs of the principal symbol is a pointwise, linear matter, and the data-surface and Asgeirsson arguments take place on the hypersurfaces of the tangent space. The mission formalizes the letter's argument in this flat model, which carries it exactly; curved manifolds are not formalized (disclosure 13).
The covariant case of the letter's equation (1). The letter classifies a general second-order linear partial differential equation by the signs of the eigenvalues of the coefficient matrix A of its displayed equation (1), with A, b, and c given functions of the coordinates. The mission formalizes the covariant case, the case the letter's dimensionality argument is about: for the wave equation and the Klein-Gordon equation the principal symbol has the same eigenvalue signs as the metric, so the class of the field equations is a function pdeClass of the pair (n, m) alone. The trichotomy milestone states the three equivalences this yields. Variable-coefficient equations, lower-order terms, and the nonlinear systems the letter mentions are out of scope; the letter's remark there (that no nonlinear terms can make a locally ill-posed problem well posed) is commentary on the classification, not a formalized claim.
Well-posedness represented by the classification. The letter's predictability requirement is that the equations be hyperbolic, so that initial-value problems are well posed, and that the data can be posed on a spacelike hypersurface. The mission does not formalize the PDE theory behind this — Hadamard's well-posedness, the energy estimates, or Asgeirsson's theorem — but takes the classification as the formal content: the predicate Predictable is the conjunction of hyperbolicity of the class and the existence of a spacelike hyperplane. The milestone predictable_m1 then shows that the requirement holds exactly in the single-time worlds with at least one space dimension, which is the letter's time-dimension argument.
Hyperplanes as data surfaces. A hypersurface on which initial data is posed is modeled as a hyperplane: the kernel of a nonzero linear functional; spacelike and timelike hyperplanes are the positive- and negative-definite kernels. The letter's statement that there are no space-like and no time-like hypersurfaces in the ultrahyperbolic case is formalized as the hyperplane obstruction: with at least two time dimensions no hyperplane is spacelike, and with at least two space dimensions no hyperplane is timelike. The deeper Asgeirsson phenomenon of the letter's figure 3 — data in an effectively one-dimensional region determining the solution in a higher-dimensional region, the free-lunch symptom of ill-posedness — is out of scope; the obstruction is the part of the discussion that is linear algebra, and it is what the predictability prong needs.
The Green profile and the Newtonian potential. The potential of a point particle in n space dimensions is the Green's function of the Poisson equation, which scales as the (2 - n)-th power of the radius for n > 2 (Ehrenfest 1917, as the letter cites); the inverse-square law of electrostatics and gravity is the three-dimensional case, an inverse-cube law the four-dimensional one. The physics layer carries the Green profile and the radially reduced Laplace operator; the milestone green_harmonic verifies that the profile is harmonic away from the origin, the defining property of the fundamental solution. The Newtonian potential of the two-body problem is the coupling times the profile, up to sign. Real powers, real division, and deriv are noncomputable in the pinned Mathlib; the definitions of the physics layer that use them are marked noncomputable accordingly.
Classical stability and the quantum counterpart. The letter argues the n > 3 instability with both the classical two-body problem (no stable orbits; the figure-2 swarm either escaping to infinity or spiralling into a cataclysmic collision) and the quantum hydrogen atom (no bound states, Tangherlini 1963). The mission formalizes the classical dichotomy in the effective-potential form: for n at least 3, stable circular Newtonian orbits exist exactly when n is 3. A circular orbit is a positive critical point of the effective potential (the centrifugal barrier plus the Newtonian potential); a stable one has positive curvature there, the linear stability of the orbit. The quantum atom, and the letter's remark that the general-relativistic situation is analogous, are out of scope, as disclosed in the exclusions.
The complexity prong carried as a bound. The letter's third prong — that worlds with fewer than three space dimensions are too simple and barren to contain observers — is supported by citations the mission does not formalize (the absence of gravitational force in general relativity with n < 3; the crossing of nerves argument). The ensemble layer carries the prong as the abstract hypothesis on the observer worlds: at least three space dimensions, the complexity requirement, on a par with the stability requirement of at most three. The goal theorem quantifies over the ensembles satisfying the letter's three premises; it does not derive them, and the letter itself is explicit that it has "not attempted to rigorously demonstrate that observers are impossible for other dimensionalities".
The ensemble layer and the capstone. A world ensemble is a measurable space of worlds with a probability measure, the two effective dimension counts of each world, and the measurable event of the worlds containing observers; nothing further is assumed. The goal theorem: if the observer worlds have positive measure and satisfy the predictability, stability, and complexity requirements, then the measure of the observer worlds inside the (3, 1) region equals the measure of all observer worlds. The positive-measure hypothesis is carried so that the equality reads as the letter's conditional statement ("with 100% certainty"); the measure equality itself is the division-free form of that conditional.
Effective dimensionalities. The letter's n and m are the numbers of non-compactified space and time dimensions, or more generally the effective dimensionalities relevant to the low-energy physics; the mission's dimension counts are these effective numbers, as the letter's first footnote fixes.
Definition names and module stems. The three definition bundles are published under names equal to their module stems (Tegmark_sig, Tegmark_phys, Tegmark_ensemble), so that the platform imports Definitions.Def_Tegmark_* in the theorem preambles resolve, in dependency order sig, then phys, then ensemble.
Exclusions. Out of scope: the general variable-coefficient second-order PDE of the letter's equation (1) with arbitrary coefficient matrix; Hadamard well-posedness and Asgeirsson's theorem; curved manifolds and the general-relativistic no-gravity claim for n < 3 (Deser, Jackiw and 't Hooft, as the letter cites); the quantum hydrogen atom of Tangherlini and the letter's general-relativistic analogue; the particle-decay kinematics with m > 1 (Dorling) and the tachyon physics (Feinberg) beyond the classification symmetry; the superstring compactification and inflationary mechanisms behind the letter's ensembles; the topological nerve-crossing argument; and the null-hypersurface caveat of the letter's footnote (data posed on a light-cone hypersurface).
The mission has eleven items: three reference definitions and eight theorem drafts, in the following order.
Reference definitions (the formalization fragment):
Tegmark_sig: the signature layer. The point space of an (n, m) world, the quadratic form with its spacelike and timelike classifications of vectors and submodules, the three PDE classes with the classifier read off the pair (n, m), the spacelike and timelike hyperplanes (the kernels of nonzero linear functionals on which the form is definite), and the predictability requirement: hyperbolic field equations together with a spacelike hyperplane.Tegmark_phys: the physics layer. The Newtonian potential of a point mass in n dimensions, the effective two-body potential with its circular-orbit and stability criteria, the existence predicate for stable circular orbits, the radially reduced Laplace operator, and the radial Green profile.Tegmark_ensemble: the ensemble layer. The probability space of worlds with a probability measure, the two effective dimension counts, and the measurable observer event.Theorem drafts (milestones in attack order, then the goal):
Tegmark.pde_trichotomy: the class of the field equations of an (n, m) world is elliptic exactly when there are no space or no time dimensions, hyperbolic exactly when there is at least one dimension of each kind and exactly one of one kind, and ultrahyperbolic exactly when there are at least two of each (pages L72-L73).Tegmark.tachyon_symmetry: the class is symmetric under exchanging the numbers of space and time dimensions (page L74).Tegmark.no_spacelike_hyperplane: with at least two time dimensions no hyperplane of the point space is spacelike, and with at least two space dimensions no hyperplane is timelike (page L74).Tegmark.spacelike_slice: every world with exactly one time dimension has a spacelike hyperplane, the spatial slice (pages L73-L74).Tegmark.predictable_m1: for a world with at least one space dimension, the predictability requirement holds exactly when the number of time dimensions is one (pages L72-L74).Tegmark.green_harmonic: for n at least 3, the radial Green profile satisfies the radially reduced Laplace equation at every positive radius (page L70).Tegmark.orbit_stability_31: for n at least 3, the Newtonian two-body problem admits stable circular orbits exactly when n is 3 (pages L70-L71).Tegmark.selection_31 (the goal): in a world ensemble whose observer worlds have positive measure and satisfy the predictability, stability, and complexity requirements, the measure of the observer worlds in the (3, 1) region equals the measure of all observer worlds (pages L69-L70).Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.
The letter is the canonical modern statement of the argument that the dimensionality of spacetime is an anthropic prediction, and the standard citation for its three mathematical prongs: Ehrenfest's 1917 observation on the instability of worlds with more than three space dimensions, the Green's-function scaling behind the dimension-dependence of the force laws, and the hyperbolicity classification behind the predictability of worlds with exactly one time dimension. These prongs rest on classical results — Ehrenfest 1917, Tangherlini 1963, Asgeirsson 1936, the Courant-Hilbert classification — which exist in the physics and PDE literature but have not been formalized together in a proof assistant. The mission packages them as one Lean development with a shared coordinate model, and its capstone is a precise, checkable statement of the letter's Bayesian conclusion: the selection argument is exactly the measure-theoretic fact that a positive-measure event contained in a region carries the region's conditional probability. A formal account also disciplines the argument's edges: the mission's theorems hold exactly where the letter's prose is exact, and the letter's conjectural steps (the complexity prong, the barrenness of n < 3) enter the capstone as explicit hypotheses rather than as unexamined facts.
The trichotomy and symmetry milestones are definitional: the unfolding of the classifier and its symmetry, verifying that the mission's encoding matches the letter's three signature examples. The hyperplane milestones are genuine linear algebra: the obstruction argument must, for every nonzero functional on a space whose time block has at least two dimensions, exhibit a nonzero vector of its kernel inside the time block — a case split on whether the functional vanishes on the block — and the slice milestone evaluates the form on the projection's kernel. The physics milestones are calculus with real powers: harmonicity differentiates the (2 - n)-th power twice and cancels against the (n - 1)/r correction, and the orbit dichotomy reduces the curvature at a circular orbit to the factor (n - 2)(4 - n), whose sign is the three-case analysis n = 3, n = 4, n at least 5. The capstone is measure-theoretic bookkeeping over the ensemble: the collation of the predictability equivalence (which forces one time dimension), the stability bound (at most three space dimensions), and the complexity bound (at least three), pinning every observer world into the (3, 1) region.
Included: the letter's pages L69-L75 at the statement level — the coordinate model of an (n, m) world and its signature form; the covariant PDE classification by the numbers of space and time dimensions; the hyperplane obstruction for multi-time worlds and the spacelike slice of single-time worlds; the predictability equivalence; the harmonicity of the Green profile in n at least 3 dimensions; the effective-potential orbit-stability dichotomy for n at least 3; and the Bayesian capstone over world ensembles.
Excluded, as disclosed in item 13 of section 2: the general second-order PDE of the letter's equation (1) with variable coefficients; the well-posedness theory (Hadamard, the energy estimates, Asgeirsson's theorem) behind the classification; curved spacetimes and the general-relativistic claims; the quantum atom and its general-relativistic analogue; the m > 1 decay kinematics and the tachyon physics beyond the classification symmetry; the compactification mechanisms of the superstring and inflationary ensembles; the topological nerve-crossing argument; and the null-hypersurface caveat.
We define "coherent communication" in terms of a simple primitive, show it is equivalent to the ability to send a classical message with a unitary or isometric operation, and use it to relate other resources in quantum information theory. Using coherent communication, we are able to generalize super-dense coding to prepare arbitrary quantum states instead of only classical messages. We also derive single-letter formulae for the classical and quantum capacities of a bipartite unitary gate assisted by an arbitrary fixed amount of entanglement per use.
This mission is the statement-level formalization of Coherent Communication of Classical Messages (arXiv:quant-ph/0307091v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
18 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 1: coherification of one-way classical communication (Proposition 1: coherification of one-way classical communication, PDF p. 1). 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:
We show that the following five categories are equivalent: (1) the opposite category of commutative von Neumann algebras; (2) compact strictly localizable enhanced measurable spaces; (3) measurable locales; (4) hyperstonean locales; (5) hyperstonean spaces. This result can be seen as a measure-theoretic counterpart of the Gelfand duality between commutative unital C*-algebras and compact Hausdorff topological spaces.
This mission is the statement-level formalization of Gelfand-type duality for commutative von Neumann algebras (arXiv:2005.05284v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Continuous and completely additive finite valuations (Lemma 2.21, PDF p. 10). 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.
51 results of the paper are not stated yet, because the library lacks an interface they need:
It is not a problem to complement a classical bit, i.e. to change the value of a bit, a 0 to a 1 and vice versa. This is accomplished by a NOT gate. Complementing a qubit in an unknown state, however, is another matter. We show that this operation cannot be done perfectly. We define the Universal-NOT (U-NOT) gate which out of N identically prepared pure input qubits generates M output qubits in a state which is as close as possible to the perfect complement. This gate can be realized by classical estimation and subsequent re-preparation of complements of the estimated state. Its fidelity is therefore equal to the fidelity F= (N+1)/(N+2) of optimal estimation, and does not depend on the required number of outputs. We also show that when some additional a priori information about the state of input qubit is available, than the fidelity of the quantum NOT gate can be much better than the fidelity of estimation.
This mission is the statement-level formalization of Optimal Manipulations with Qubits: Universal NOT Gate (arXiv:quant-ph/9901053v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal universal NOT error (Theorem (unnumbered), PDF p.3: optimal universal NOT error, 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.
We construct the unique optimal quantum device for turning a finite number of d-level quantum systems in the same unknown pure state σinto M systems of the same kind, in an approximation of the M-fold tensor product of the state σ.
This mission is the statement-level formalization of Optimal Cloning of Pure States (arXiv:quant-ph/9804001v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The unique optimal pure-state cloner (§4, unnumbered Theorem: unique optimal pure-state cloner, PDF p. 9). 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.
1 results of the paper are not stated yet, because the library lacks an interface they need:
This paper develops an abstract framework for constructing ``seminormal forms'' for cellular algebras. That is, given a cellular R-algebra A which is equipped with a family of JM-elements we give a general technique for constructing orthogonal bases for A, and for all of its irreducible representations, when the JM-elements separate A. The seminormal forms for A are defined over the field of fractions of R. Significantly, we show that the Gram determinant of each irreducible A-module is equal to a product of certain structure constants coming from the seminormal basis of A. In the non-separated case we use our seminormal forms to give an explicit basis for a block decomposition of A. The appendix, by Marcos Soriano, gives a general construction of a complete set of orthogonal idempotents for an algera starting from a set of elements which act on the algebra in an upper triangular fashion. The appendix shows that constructions with "Jucys-Murphy elements"depend, ultimately, on the Cayley-Hamilton theorem.
This mission is the statement-level formalization of Seminormal forms and Gram determinants for cellular algebras (arXiv:math/0604108v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.
31 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gram determinants are products of seminormal structure coefficients (Abstract; Theorem 3.12 determinant consequence, PDF p. 1). 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.
8 results of the paper are not stated yet, because the library lacks an interface they need:
The cyclotomic Birman-Wenzl-Murakami algebras are quotients of the affine BMW algebras in which the affine generator satisfies a polynomial relation. We study admissibility conditions on the ground ring for these algebras, and show that the algebras defined over an admissible integral ground ring are free --modules and isomorphic to cyclotomic Kauffman tangle algebras. We also determine the representation theory in the generic semisimple case, obtain a recursive formula for the weights of the Markov trace, and give a sufficient condition for semisimplicity.
This mission is the statement-level formalization of Cyclotomic Birman--Wenzl--Murakami algebras, II: Admissibility Relations and Freeness (arXiv:math/0612065v5). 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 Conditional expectation of a canonical path idempotent (Lemma 2.19: expectation of a path idempotent, PDF p. 16). 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.
19 results of the paper are not stated yet, because the library lacks an interface they need:
An action of an affine algebraic group on an affine variety is observable when invariant regular functions see every nonzero -stable ideal of the coordinate ring: if is a nonzero -stable ideal, then . The notion goes back to Grosshans' theory of observable subgroups (F. D. Grosshans, Observable groups and Hilbert's fourteenth problem, Amer. J. Math. 95, 1973): a closed subgroup is observable exactly when the action of on by left translations is observable (p. 2 of the paper), and observable subgroups are the ones for which is quasi-affine.
L. Renner and A. Rittatore (arXiv:0902.0137) characterise observability geometrically. Their Theorem 3.10 states that an action on an irreducible affine variety is observable if and only if (1) every invariant rational function is a quotient of invariant regular functions, and (2) the set of closed orbits of maximal dimension contains a nonempty open set. Section 4 of the paper specialises this to reductive groups, where the answer becomes a single condition on closed orbits, and identifies a canonical closed subvariety, the socle, on which the action is observable. This mission formalizes that section.
Timeline:
Let be an algebraically closed field. An affine algebraic group is given by its coordinate ring , a reduced, finitely generated, smooth -algebra whose -points form a group with regular multiplication and inversion. An affine variety is given by its coordinate ring , a reduced finitely generated -algebra; its points are the -algebra maps . A regular action is a group homomorphism whose evaluation is a regular function of ; points move by .
For reductive acting on an irreducible affine variety :
and is the maximum -stable closed subset such that the restricted action is observable.
The result. For reductive groups observability is decided by one closed orbit of maximal dimension, with no condition on invariant rational functions. This simplification fails for general groups: a Borel subgroup acting on a semisimple group by left translation has every orbit closed of maximal dimension, yet the action is not observable (Example 3.11 of the paper). The second sentence gives every reductive action a canonical observable piece, the socle, computed from the closed orbits alone, and Proposition 4.8 of the paper then identifies its ideal as the largest -stable ideal without nonzero invariants.
Formalizing it. The results are proved in the paper (Proposition 4.4 is Popov's theorem, cited there). None of them is machine-checked. Theorem 3.10 and Lemma 3.1 are open goals of an existing public mission on the same paper, which covers §§2–3 and defers §4; this mission states §4 on the same definitions, so a proof of either referenced statement serves both. A complete development needs the basic geometric invariant theory of reductive groups: finite generation of invariants, separation of closed -stable sets by invariants, the existence of a unique closed orbit in each orbit closure, and semicontinuity of orbit dimension. None of this is in Mathlib.
The direction "observable " follows from Theorem 3.10. The converse is where reductivity enters: given a nonzero -stable ideal, one must produce a nonzero invariant in it, and the natural route is to separate the closed orbits in from the zero set of the ideal by invariant functions. That separation is a theorem about reductive groups (closed disjoint -stable sets are separated by invariants), not available for arbitrary groups, and it must be combined with the openness of . For the maximality of the socle, the paper reduces to irreducible components through Lemma 3.1, which assumes connected; Theorem 4.7 makes no such assumption, so a disconnected needs a reduction to the stabiliser of a component.
All statements are built on the public definitions module QAlgorithms_Papers_Independent_Support21_P10 for this paper: points are -algebra maps, is a coordinate ring H with a group structure on its points (IsAffineAlgebraicGroup), is a coordinate ring A (IsAffineVariety, finite type and reduced), the action is rho : Point k H →* (A ≃ₐ[k] A) with IsRegularAction. Closure is the Zariski closure on -points (classicalClosure), and is the set of -points of with the restriction map (quotientPoint). No finite generation of is assumed.
Conventions committed to:
IsDomain A) in Theorems 4.6 and 4.7, the paper's standing assumption for §4 (p. 2). Without it the first sentence of 4.7 is false. Lemmas 4.3, 4.5 and Proposition 4.4 are stated for arbitrary affine , as printed.IsReductiveGroup k H: every Zariski-closed normal subgroup of with prime vanishing ideal and consisting of unipotent points is trivial. Unipotence is local unipotence of right translation on .classicalClosure {x | IsClosedOrbit rho x}.rhoZ on A ⧸ coordinateVanishingIdeal Z compatible with the quotient map (IsRestrictionOf). For the socle its existence is part of the conclusion; for a competitor , compatibility is a hypothesis. No statement quantifies over an uncoupled action.(omegaLocus rho).Nonempty. This is strictly weaker than Theorem 3.10's condition that contain a nonempty open set.A trivializing reading is excluded: the socle is computed from the closed orbits and is never defined as "the largest closed set with observable restricted action", which would make the maximality claim a tautology.
Welcome contributions: proofs of the milestones, and reusable infrastructure for reductive group actions (finite generation of invariants, separation of closed invariant sets, orbit-closure structure).
Quantum Max Cut asks for the highest energy of a two-qubit interaction Hamiltonian placed on the edges of a weighted graph. It is a quantum analogue of Max Cut: a classical cut assigns one of two labels to each vertex, while a quantum state can use correlations and entanglement across the qubits. Lee studies an approximation algorithm that first solves a semidefinite program and then uses its vectors to choose both a bit string and the angles of a quantum circuit. The result applies to arbitrary nonnegatively weighted simple graphs, without a degree or regularity restriction. The guarantee is an approximation ratio of for the energy of the algorithm's random output in expectation Lee, 2022, pp. 9–13.
The paper places this algorithm alongside earlier approaches that round a level-one or level-two quantum Lasserre program. Its distinguishing object is a circuit with one parameter per graph edge, computed from the SDP vectors rather than optimized over circuit angles after rounding. The parameter rule makes a global approximation guarantee possible even when neighboring edge gates interfere Lee, 2022, pp. 3–5, 9.
Let be a finite simple graph with nonnegative weights . Associate one qubit with each vertex. On qubit , let be the standard Pauli operators, and let be the identity. Each edge contributes
For a unit state , its energy is . The Quantum Max Cut optimum is the largest eigenvalue of , equivalently the largest energy over all unit states Lee, 2022, Definition 2, p. 2.
The paper's canonical Lasserre program at level uses a real positive semidefinite matrix indexed by Pauli strings of weight at most . Its constraints make matrix entries consistent with products of Pauli strings. At level two, its objective has one term for each of , , and on every edge. Lemma 1 places all quantum-state energies below feasible Lasserre objectives. The paper then introduces a vector semidefinite program (S). It uses a unit vector , vectors for vertices and , and vectors for pairs of distinct vertices. Relations (1)–(8) fix their norms and inner products. Writing , its objective is
Lemma 2 shows that (S) relaxes the level-two Lasserre program Lee, 2022, Definitions 3–5 and Lemmas 1–2, pp. 3–6.
Algorithm 1 takes an optimal feasible solution of (S). It picks uniformly, chooses a random direction , and sets bit by the sign of . For each edge it computes the normalized correlation
It starts in the computational basis state and applies the commuting edge gates , with when and when . The result is a random state Lee, 2022, Algorithm 1, p. 9.
The goal is the expectation form of Theorem 1. For every nonnegatively weighted graph, every globally optimal feasible SDP solution , and every unit quantum state ,
The goal also states that the random energy is integrable. Because the inequality holds for every unit , it is exactly the comparison with times the maximum eigenvalue. The printed theorem omits the expectation sign, while its proof explicitly averages the rounded output Lee, 2022, Theorem 1 and proof, pp. 10–11.
The milestones are the source's relaxation lemmas, the feasible-vector identities, the star monogamy bound, the hyperplane cut-probability bound, the circuit's edge-energy bound, equations (19) and (21)–(24), the final scalar minimum, and the per-solution expected-energy bound. Their order moves from the Hamiltonian and SDP model to the output of Algorithm 1. The coefficient and the parameter are the paper's values, not tunable placeholders.
Together, the two relaxation lemmas connect the quantum optimum to the objective optimized by (S). The rounding results then connect a feasible SDP value to a physically represented output state. The theorem certifies a constant approximation ratio for arbitrary weighted graphs in the model of the paper. The star monogamy inequality and edge-energy lemma also isolate claims useful for analyzing related rounding circuits Lee, 2022, Lemmas 1–6, pp. 4–10.
This result is proved in the cited paper. The mission asks for machine-checked proofs of its statements and for the model that makes those statements precise. Its definitions of Pauli strings, the quantum Hamiltonian, canonical Lasserre feasibility, the vector SDP, and the rounded circuit can support later comparisons of SDP-based quantum approximation algorithms. The draft statements compile, but a compiling sorry is not a proof; the theorem and milestones remain open formalization targets.
Bounding the probability that a rounded bit string cuts an edge is only one part of the argument. Its circuit gate acts on the same qubits as gates at neighboring edges. Consequently, a good cut probability alone does not determine the energy on that edge. The monogamy bound limits how much SDP value can be concentrated around a vertex, while the edge-energy statement accounts for the neighboring gate parameters. A formal proof must also connect matrix feasibility, vector feasibility, Gaussian rounding, and complex matrix expectations without losing the edge weights or the factor Lee, 2022, pp. 7–13.
Vertices are Fin n, computational basis labels are bit strings Fin n → Fin 2, and Pauli strings are maps Fin n → Fin 4. The graph is simple; each edge occurs once, with its smaller endpoint first. Only that orientation's weight is read. The vector SDP uses Fin N → ℝ, and its feasibility predicate states relations (1)–(8) with distinct-index conditions. The ordered-pair implementation of includes symmetry, making the paper's undirected edge indexing explicit. Optimality in the goal compares feasible solutions across every finite dimension, so a solution optimal only in a small dimension cannot satisfy the intended premise.
The random direction is a standard Gaussian vector. Its signs have the same distribution as the signs from a direction uniform on the sphere; a zero projection gives bit zero. The circuit uses the cosine-sine form of each Pauli-product exponential and a lexicographic edge order. Its gates commute, so the chosen order represents the paper's product. The expectation averages the three choices of and integrates over the Gaussian vector. The goal includes integrability, and its universal unit-state comparison avoids a supremum with a default value on a bad domain.
Three source boundaries are stated explicitly. The Lasserre objective requires because it indexes two-qubit Pauli strings. Lemma 6 requires on edges; the printed nonnegative-angle condition is too broad, while Algorithm 1 always gives angles in that interval. Definition 4's repeated objective term is read as , as required by the Hamiltonian and its appendix calculation. The Goemans–Williamson quotient uses since the printed closed endpoint gives . A single arbitrary feasible SDP solution cannot replace the globally optimal one in the final comparison with the quantum optimum, and a deterministic bound for every random outcome is not asserted.
Contributions that establish the two relaxation maps, the vector identities, the Gaussian cut bound, the circuit's local energy bound, and the final expected-energy comparison all belong to this mission. Proofs of the paper's polynomial running-time claim and cited hardness results are outside the formal statements here.
The generalized Stieltjes transform of order of a non-negative measure on is the function . For this is the classical Stieltjes transform, whose functions (Stieltjes functions) appear in moment problems, in the theory of completely monotone and Bernstein functions, in the spectral theory of positive operators, and in the functional calculus of sectorial operators. The classes of order were studied by Widder, Hirschman and Widder, Sokal, and Schwarz, among others, and appear in work on functional calculi of sectorial operators (Batty, Gomilko and Tomilov, arXiv:1309.0318).
D. Karp and E. Prilepkina, Generalized Stieltjes transforms: basic aspects (arXiv:1111.4271), collect and prove the basic real- and complex-variable properties of these classes. One elementary but structural fact is that the classes are nested: a function of order is also of every larger order . This raises a natural question that the paper answers: given in the class of order , is the smallest order available, or can it be lowered? The paper introduces the exact Stieltjes order and gives a criterion of exactness phrased purely in terms of the representing measure of . This mission formalizes that criterion (Theorem 16) together with the results its proof relies on.
For , write for the set of non-negative Borel measures on with
The generalized Stieltjes class consists of the functions of the form
with a constant and . The paper writes the atom of at separately as a term (its formula (1)); here it is part of . The pair is a representation of in , and is its representing measure. Write .
For a measure on , its left-continuous distribution function is , so . For , the left-sided Riemann–Liouville fractional integral (Definition A1) is the measure on with Lebesgue density
The exact Stieltjes order of is
Finally, for with representing measure and a parameter , set
For and with representing measure ,
The order is exact precisely when no admissible makes monotone.
The result. Theorem 16 reduces the question "is the order of optimal?" to a monotonicity test on a single function built from the representing measure. The paper derives two practical corollaries from it: if has a limit below , then is exact (Corollary 1), and if has compact support, then is exact (Corollary 2). Both are immediate once Theorem 16 is available and are natural follow-up targets. The milestones are of independent use: Theorem 3 is the nesting of the classes with an explicit formula for the new representing measure, and Theorem A1 is the integrability and inversion theory of fractional integrals of measures, which the paper's appendix develops because the authors found no reference treating measures rather than functions.
Formalizing it. The results are proved in the paper; none is formalized. The platform has the generalized Stieltjes class itself (a published definition from the Batty–Gomilko–Tomilov formalization) and the half-line Beta integral, but no fractional integrals of measures, no inversion formula, and nothing on the exact order. A complete development provides a reusable Riemann–Liouville calculus for measures on the half-line and the uniqueness of the representing measure in , which milestone 5 contains.
The forward direction of Theorem 16 looks like a computation: pass from to a smaller order and read off the measure. The obstacle is that one must know that the representing measure in is unique, since is built from the representing measure and the inversion formula (11) must apply to it; milestone 5 states the inversion for an arbitrary representing measure for this reason. The converse direction must produce a measure from a function: a non-decreasing is a distribution function, and one must show the resulting measure satisfies (2) at the lower order, which is claim (26) and needs a careful tail estimate rather than a direct comparison. Throughout, interchanges of integration are carried out for measures with atoms (including an atom at ), where the naive differentiation formula of (11) and (29) for higher breaks down at jumps.
Functions are real-valued on (PositiveReal), and the classes and representations are the published StieltjesClass and StieltjesRepresentation (QAlgorithms_Papers_Independent_Renew46_P11), reused unchanged. Representing measures are measures on ℝ≥0; the paper's atom at is the constant . All orders are positive. All kernel integrals and the functions and take values in (lower Lebesgue integrals), so a divergent integral is , not ; "non-decreasing" is monotonicity in . The exact order is the real infimum of , which is nonempty and bounded below whenever . Densities are with respect to Lebesgue measure on pushed to ℝ≥0.
Corrected readings, each disclosed in the item: (25) is taken over , while the paper prints ; with the theorem fails for , whose representing measure is the unit mass at . Formulas (11) and (29) are stated only for , the case Theorem 16 uses; as printed for they differentiate a function at its jumps. Claim (26) is stated for the distribution function of an arbitrary measure, the generality its proof gives.
A trivializing formalization is ruled out: must be built from the representing measure of the given (not from an arbitrary measure), over (over an atom at makes identically ), and in (a real-valued Bochner would be wherever the integral diverges).
Contributions welcome: proofs of any milestone, a reusable Riemann–Liouville integral of measures on ℝ≥0 with its Tonelli computations, uniqueness of generalized Stieltjes representations, and the corollaries of Theorem 16.
Topological quantum computing represents a gate operation by moving anyons around one another. A compiler must turn a requested single-qubit unitary into a finite braid or gate word, with enough accuracy and a length that grows slowly as the error tolerance shrinks. For Fibonacci anyons, the matrices generated by the standard elementary braids have algebraic entries, which makes exact arithmetic available during compilation. Kliuchnikov, Bocharov and Svore gave an approximation algorithm whose output length scales logarithmically with inverse precision, the asymptotic scale required by their worst-case lower bound. Their method joins a sample from a cyclotomic integer ring to an exact-synthesis routine Kliuchnikov–Bocharov–Svore, 2013.
The result concerns what every successful run outputs. Its additional claim about average runtime depends on a number-theoretic conjecture and is separate from the output-quality theorem. Keeping these assertions distinct matters: a short accurate circuit conditional on finding a solvable norm equation does not imply that a sample can be found quickly.
Fix the tenth root of unity , , and . The ring contains expressions with integer coefficients. Arithmetic is reduced using and . The automorphism sends to . The Gauss complexity of is . This quantity controls the number of steps in exact synthesis §III, pp. 3–5.
An exact unitary is the paper's two-by-two complex matrix built from , an integer phase , and the normalization . Its gates are , , and the scalar phase . A circuit is a finite sequence of these gates, evaluated by matrix multiplication in sequence order. Its length counts and gates; the scalar phase has no braid cost in the paper's convention.
The target rotation is . Approximation uses the phase-invariant distance
Figure 15 approximates a real input by through Fibonacci numbers. Figure 13 combines two such approximations into a cyclotomic integer in a specified geometric region. Figure 12 scales and rotates , asks for a solution of a norm equation to obtain , and runs Figure 4's exact-synthesis loop on the resulting exact unitary Figures 4, 12, 13 and 15.
For every angle , every precision , every allowed sample index, and every norm-equation solution used by Figure 12, its returned circuit satisfies
for one positive absolute constant . The statement is about all possible outputs, including all allowed tie and solution choices. It does not assert that the norm equation has a solution for every input. This is the first sentence of Theorem 21, p. 14.
The milestone list records Proposition 4's integer-valued complexity gap, Lemma 5's decreasing step and asymptotic ratio bound, Theorem 6's exact synthesis and length estimates, the §V distance identity, Lemma 18's real-approximation bounds, and Lemma 19's count of equiprobable samples, their membership in the parallelogram of Figure 14, and the corrected complexity bound. They describe the interfaces needed to connect algebraic synthesis to geometric approximation. The source text is preserved in each milestone even where the formal statement makes a documented correction.
The target gives a finite circuit whose accuracy is specified by a matrix distance rather than by a coordinate surrogate. Its length bound is uniform in the rotation angle, the sample choice, and the norm-equation solution. Consequently, once a suitable sample and solution are supplied, exact synthesis cannot silently add a superlogarithmic number of gates. The paper's conditional runtime sentence concerns how quickly such a sample is obtained and remains outside this theorem Theorem 21, p. 14.
A machine-checked development would produce reusable coordinate arithmetic for , a verified implementation of the exact synthesis loop, Fibonacci-based real approximation, and a phase-invariant matrix-distance calculation. These are useful beyond this single target wherever the Fibonacci-anyon gate set is used. The present files contain compiled statements and definitions; the theorem proofs remain open. Contributions proving the stated milestones, establishing ring and matrix identities, and checking the sampler's geometric inequalities are welcome.
The obvious idea of rounding the target phase does not by itself give an exactly implementable unitary: the upper-left entry must be extendable to a matrix satisfying . The sampler must keep in a narrow region while leaving a norm equation for that can be solved. Even after that, a short exact circuit requires a decrease in at each synthesis step. The length bound cannot follow merely from the fact that some finite circuit exists. These are the separate mathematical constraints reflected by the milestones §§III–V, pp. 3–14.
Lean represents as four integer coordinates. Its multiplication uses the paper's cyclotomic relations, and its conjugation and bullet automorphism are coordinate maps. Matrices have type . The synthesis output is a list of , , and gates. The first minimizing exponent in breaks ties in Figure 4; the angle-reduction integer may be any valid one. Rounding in APPROX-REAL uses Lean's nearest-integer operation.
The formalization corrects two printed algorithm signs: Figure 12's final matrix is instead of , and Figure 13's uses a plus sign before the sine term. The first is required by the displayed distance formula; the second by the geometry of the sampled region. Lemma 18 is restricted to , since its bound fails at . Lemma 19's Gauss-complexity bound is , because is already of order ; its formal statement covers every with , and renders "each output occurs with the same probability" as equal fibre sizes of the explicit sample index. These corrections and scope choices are documented next to the affected items pp. 11–14.
Random sampling is represented by an explicit index in its allowed range. SOLVE-NORM-EQUATION is represented by any satisfying its output equation; EASY-SOLVABLE is omitted from the output guarantee because it filters samples without changing the claimed quality of one successful output. The goal's constant precedes all angles, precisions, samples, and solutions. The output must be the circuit produced by the defined Figure 4 loop applied to Figure 12's data; choosing an arbitrary short circuit or making the norm-equation hypothesis impossible would not state the paper's result.
In quantum field theory the vacuum is entangled between any two regions of space, and the amount of entanglement between nearby regions is infinite: the algebras of observables of regions that touch admit no normal separable state at all. For regions at a positive distance the question becomes quantitative. How much entanglement does the vacuum carry between a region and a second region at distance , and how does it depend on and on the field content of the theory? Questions of this type underlie area laws for entanglement entropy, the thermodynamics of black holes, and the information-theoretic approach to quantum field theory.
S. Hollands and K. Sanders, Entanglement measures and their properties in quantum field theory (arXiv:1702.04924, SpringerBriefs in Mathematical Physics, 2018), define entanglement measures directly on the von Neumann algebras of local observables, without assuming a tensor product structure, and prove upper and lower bounds for them in several classes of theories. For conformal field theories in dimensions, , they bound the relative entanglement entropy of the vacuum between a ball of radius and the outside of a concentric ball of radius by the partition function of the conformal Hamiltonian (Theorem 13, p. 79).
Let be a Hilbert space and commuting von Neumann algebras, with join . A normal state on the join is separable if for , , with positive normal functionals and . Araki's relative entropy of two positive normal functionals generalizes . The relative entanglement entropy of a normal state is
equal to when there is no separable state. Two auxiliary measures enter: the logarithmic dominance , and the modular entanglement measure , where , is the modular operator of at the vector of , and is the 1-nuclear norm.
A conformal field theory in dimensions is given, in its vacuum representation, by a net of von Neumann algebras on a Hilbert space indexed by causal diamonds of Minkowski space , a unitary representation of a covering group of the conformal group that acts covariantly on the net, and an invariant vacuum vector with vacuum state . The conformal Hamiltonian is the generator of the rotation of , the sum of the energy and the generator of special conformal transformations in the time direction; generates dilations. For , is the algebra of the double cone over the ball of radius about the origin, and that of the domain of dependence of the complement of the ball of radius .
for every conformal field theory satisfying the axioms, every and every . The right side is when the trace diverges.
Theorem 13 bounds the vacuum entanglement of two regions by a quantity of the theory's spectrum alone. Combined with the paper's identification of with over the spectrum of operator dimensions (Theorem 14, p. 83), it shows that for the entanglement decays like with the smallest non-zero dimension, and for it diverges at most like . The general results on the way, and the nuclearity estimates, apply to any pair of commuting von Neumann algebras and underlie all upper bounds of the paper, including those for free and integrable models.
The results are proved in the paper, at the level of rigour of mathematical physics, with some steps cited (the Hislop–Longo theorem, the Heinz–Löwner inequality for unbounded operators, the edge-of-the-wedge theorem, the Reeh–Schlieder theorem). None of them is machine-checked. A formal proof would also make precise which axioms each step uses, for instance where statistical independence of and , which is not an axiom here, enters.
The obvious route, comparing the vacuum with product states through a tensor product decomposition , is not available: the local algebras are type III factors and there is no such decomposition. Every step must work with modular operators of the local algebras and normal functionals on their join. The analytic core is the operator identity (212): and are unbounded, Lemma 13 holds for real only, and reaching requires analytic continuation in a strip, domain control through the Heinz–Löwner inequality, and the edge-of-the-wedge theorem. Separately, needs that products of normal functionals on and are normal on the join, which in the conformal setting follows from modular nuclearity rather than from an axiom.
The general layer (Definitions 5, 7, 10–13) is stated for von Neumann algebras in Mathlib's VonNeumannAlgebra, with functionals as maps of which only the values on the relevant algebra matter. Normal functionals are given by vector sums . The relative entropy is Araki's, in Kosaki's variational form, which is defined for all pairs of positive normal functionals. , , , take values in EReal and norms in ℝ≥0∞, so empty infima are , as Definitions 5, 12 and 13 require. Separability is defined on the join, as in Theorem 2 c); no split property is assumed in the goal. Lemma 4 and Theorem 4 carry the §3 standing assumption of statistical independence, in the form that products of positive normal functionals are normal on the join. Modular operators are the published StandardModularData of BoundedRecovery; is the limit of spectral cut-offs.
The conformal layer is a structure CFTVacuum d H₀: the net with isotony and locality (the algebra of a region such as contains those of the double cones inside it and commutes with those spacelike to it, without an additivity assumption the paper does not make) and weak additivity; a covering group of presented by a covering homomorphism with discrete kernel and an exponential map; a strongly continuous unitary representation with local covariance a3′); a unique invariant vacuum vector, cyclic for the quasi-local algebra (the GNS representation of a4′)); the generators , and as spectral calculi; and the Hislop–Longo theorem for the unit double cone as a disclosed field. The projective representation of the paper is taken as a true representation of the cover (Bargmann). Generator signs are fixed so that generates forward time translations and shrinks regions, consistent with (217), (219) and p. 84. is the bounded function of the conformal Hamiltonian, whose spectrum is non-negative (footnote 42), and the trace is taken in . The goal assumes (§4.4, p. 78).
No conclusion of the paper is a field of the structure: not modular nuclearity a5′), not the split property, not (212) or (219), so the goal is not a restatement of its hypotheses. Theorem 14 (the field-content form ) is not stated: a faithful encoding of the operator-valued fields, their conformal transformation law (224) and descendants is left for a later mission.
Reusable beyond this mission: the entanglement measures on general von Neumann algebras, the 1-nuclear norm, , and the conformal structure. Contributions are welcome on the Kosaki formula (scaling, monotonicity, ), on Heinz–Löwner for unbounded operators, and on the analytic continuation of modular groups.
The Brauer algebra packages pairings of points into an algebra whose multiplication records how pairings join when diagrams are stacked. It was introduced by Brauer as the centralizer algebra of orthogonal and symplectic groups acting on tensor powers of their natural representation (Brauer 1937), and is semisimple for generic (Wenzl 1988). It provides an example where diagram combinatorics and the choice of coefficient ring affect the same algebraic question. King, Martin, and Parker study central idempotents that separate the diagrams with few propagating lines from the remaining part of the algebra. Their construction works over a ring designed to retain useful specializations of the parameter ; a solution obtained only in the field would lose that arithmetic information. King–Martin–Parker, §1–§2
The mission concerns their main result, Theorem 14. It asks for the precise bridge between a diagram equation, coefficients constrained to , and an idempotent that splits an ideal quotient. The source is the 2016 arXiv version; all page and result numbers here refer to that version. King–Martin–Parker, Theorem 14
A Brauer diagram on strands is a perfect matching of two rows of nodes. A strand joining the rows is a propagating line; a strand within one row is a horizontal arc. The set of all such diagrams is a basis for , here over , where is an indeterminate. To multiply diagrams and , place over and identify the adjacent rows. The resulting outer pairing is another diagram . If connected components close entirely in the middle row, then
This loop factor is part of the algebra, even when no loop is visible in a particular example. The span of diagrams with at most propagating lines is a two-sided ideal. Simultaneous relabelling of the upper and lower rows by partitions diagrams into orbits . The orbit sum uses each original, unnormalised diagram once. King–Martin–Parker, §2.2–§2.3
The source works with a coefficient ring inside :
For and even , let be the diagram with cups at in each row and vertical lines elsewhere. The paper uses the normalized element . Its required equation has the same solutions as over . King–Martin–Parker, §2.2, equation (4), and §3, equation (5)
The goal is Theorem 14. For orbit coefficients and , it asserts a unique solution with to
It further asserts that satisfies and , and is central and idempotent. By Lemma 10, these properties identify the splitting of . King–Martin–Parker, Lemma 10 and Theorem 14
The milestones follow the paper's proof, in attack order: the general bimodule splitting criterion (Lemma 10); the basis of the -centralizer given by the orbit sums (Lemma 11); the paper's assertion that for the splitting idempotent exists with coefficients in (p. 8); the fact that fixes every diagram carrying its cups and maps no other diagram onto without a negative power of (Proposition 12); the independence of the linear equations in the , i.e. injectivity of on orbit-sum combinations (equation (6)); and membership of every solution coefficient in (Proposition 13). Lemma 10 is reusable beyond diagram algebras. King–Martin–Parker, §3
The idempotent separates the ideal of diagrams with few propagating lines from the quotient as bimodules. Its centrality means this separation is compatible with multiplication on either side. Specifying the coefficients in also preserves information about specializations of that a field-only existence statement would omit. The paper uses the resulting splitting idempotents in its discussion of primitive central idempotents and Brauer algebra representations. King–Martin–Parker, §4
The theorem is proved in the cited paper. This mission supplies a machine-checkable interface for its definitions and statements; the theorem proofs remain open. A completed development would verify the diagram multiplication, the ideal and orbit descriptions, the ring-theoretic splitting criterion, and the coefficient claim in one Lean environment. These components can support later formalizations involving diagram algebras or central idempotents.
An equation over alone does not give a splitting idempotent with coefficients in . The coefficient restriction is sensitive to the exact loop factor in multiplication and to whether orbit sums use normalized or original diagrams. The equations indexed by diagrams also need to determine the orbit coefficients uniquely, while the two-sided annihilation requirement concerns every element of the ideal, not just the displayed cup diagram. These are distinct claims in the source; checking one of them does not silently establish the others. King–Martin–Parker, §3
Lean represents a diagram as a fixed-point-free involution on Fin n ⊕ Fin n; the left summand is the upper row. A three-row graph defines its composite and loop count. The Brauer space is the finite-dimensional function space Diagram n → RatFunc ℚ, with an explicit bilinear multiplication bmul; the statements do not assume a ring instance whose associativity has not yet been proved. The parameter is RatFunc.X, representing the indeterminate . The ideal is the -span of exactly the basis diagrams with propagating count at most .
The goal fixes and additionally assumes even (the existence milestone, stated on the page for every , does not). That parity condition makes the paper's displayed product well defined. Lean uses zero-based indices, so the paper's cup is represented by . The equation uses unnormalised but has the same solutions as the paper's normalized equation because is nonzero in . Orbit sums are unnormalised, as in the printed Theorem 14. The centralizer is the set of elements commuting with every diagram having propagating lines. The index set of the goal consists only of orbits of diagrams with at most propagating lines; it is equivalent to the paper's Spore-tableau index set, without introducing that classification into this mission.
The statement constructs as from coefficients , rather than postulating an arbitrary splitting idempotent. Neither the ideal nor the equation is replaced with a degenerate special case: with condition (ii) would force , and with it would be vacuous, so the ideal is exactly the span of the diagrams with at most propagating lines, and the loop factor is kept in the product. The main reusable infrastructure comprises finite diagrams, the loop-weighted product, orbit sums, and the generic bimodule splitting lemma. Contributions may establish these structural facts, the milestone statements, and the final theorem.
A quantum dynamical semigroup describes the irreversible evolution of an open quantum system: a family , , of normal completely positive maps on the algebra of bounded operators, with and weakly continuous. When the generator is bounded its structure is given by the Lindblad–Gorini–Kossakowski–Sudarshan form (Lindblad 1976). For unbounded generators, the bounded-generator formula alone does not settle trace preservation or describe the generator's domain.
W. Arveson (The domain algebra of a CP-semigroup, 2002) attached to every such semigroup its domain algebra, the set of observables for which , and all lie in the domain of the generator. This is the largest set on which the generator can be handled algebraically, through derivations and the "dissipation function". Arveson computed it for one explicit example built from the shift on with a rank-one rebound to a pure state , found that its strong closure consists of the operators commuting with , and asked whether there exist dynamical semigroups whose domain algebra is as small as .
A. S. Holevo (arXiv:1706.04866v5, §2) generalizes Arveson's example to a rebound into an arbitrary density operator and answers the question positively: when is nondegenerate, the domain algebra is .
Let and let be the semigroup of left shifts. On trace-class operators put , with dual semigroup on bounded operators, and let be the generator of . The shift moves probability out of through the endpoint , so is not trace preserving.
Fix an arbitrary density operator (positive, trace class, ). The rank-one reset
re-injects the lost probability in the state . For with absolutely continuous with square-integrable derivative (), . Let be the minimal perturbed semigroup generated by (constructed by a resolvent series), its dual, and the ultraweak generator of : means as for every trace-class . The generator of is defined in the same way. Arveson's domain algebra is
For every ,
and if is nondegenerate, . The goal is the existing Open platform theorem QAlgorithms.Papers.Independent.Renew46.P06.shiftReset_domainAlgebra, which this mission references rather than restates.
The milestones follow the paper's proof, in order:
shiftDual_nonunitalStarDomain).shiftReset_centeredGenerator).The goal and Lemmas 3 and 4 are Open platform theorems posed from this paper without a mission; this mission supplies the remaining milestones of the paper's proof and the attack path connecting them.
Theorem 2 answers Arveson's question: there are quantum dynamical semigroups on whose domain algebra contains only the scalars. For such a semigroup, no non-scalar lies in the generator domain together with both and , so algebraic tools built on the domain algebra (derivations, the dissipation function) see only scalars. For degenerate the theorem still forces every element of to act as a scalar on the range of , extending Arveson's computation for a pure to every density operator.
The result is proved in the paper; nothing here is open mathematically. None of it has a machine-checked proof. The mission produces, on top of Mathlib, a formal account of weak generators of semigroups on (the Favard-class criterion (11)), a Duhamel formula for a minimal perturbation, and the equality case of the Cauchy–Schwarz inequality for density operators, each of which is reusable outside this paper.
The algebra of the proof of Theorem 2 is short once its inputs are available; the inputs are the work. Criterion (11) is a statement about the ultraweak generator: with the operator-norm derivative in its place it is false, since the bounded difference quotients describe the Favard class, which is in general larger than the norm domain. Its reverse direction must connect uniform operator-norm bounds with a limit against every trace-class operator. Unitality of depends on the minimal resolvent series of the perturbation actually conserving trace, which can fail for general unbounded perturbations (explosion). The integral equation (12) requires knowing that the minimal semigroup satisfies the Dyson-type equation on rank-one operators built from functions, together with the evaluation , which uses boundary values of functions that only continuous representatives possess.
All statements use the published definitions module QAlgorithms_Papers_Independent_Renew46_P06 and its imports: is HalfLine as an Lp space; semigroups are Evolution (normal, CP, subunital, weakly continuous) with times in NNReal, real times entering through t.toNNReal only for ; trace-class operators and density operators are TraceClass and State b, with the trace operatorTrace b taken in a fixed Hilbert basis ; and the graph of are the ultraweak dualGeneratorDomain and InDualGeneratorGraph; the shift, the pair and the reset construction are IsLeftShift, IsShiftPair and IsResetConstruction; is domainAlgebra; is identityObservable. Every semigroup milestone uses exactly the goal's binders, so the milestones compose with the goal. In (12), are encoded by classes with named locally absolutely continuous representatives, and only those representatives are evaluated at a point; is Mathlib's inner product, conjugate-linear in the first slot. The Cauchy–Schwarz milestone is stated on an arbitrary complex Hilbert space.
A formalization that takes a local semigroup in place of the published construction, an operator-norm generator in place of the ultraweak one, or that turns (12) into a definition of , would not state the paper's results and is ruled out.
The setting of the semigroup milestones is satisfiable exactly when a reset construction exists, which is part of the separate Open platform theorem shiftReset_standard_nonclosable; contributions proving that existence are welcome alongside the milestones. Also welcome: general Favard-class results for weak-continuous semigroups, Duhamel formulas for minimal perturbations in the sense of the published IsMinimalPerturbation, and trace inequalities for State.
Let be the natural representation of and its dual. The walled Brauer algebra describes the endomorphisms of mixed tensor space that commute with , through mixed Schur–Weyl duality. It was introduced in this role independently by Turaev, Koike and Benkart–Chakrabarti–Halverson–Leduc–Lee–Stroomer around 1989–1994. It is also a diagram algebra in its own right, defined for every parameter in the ground field. Its representation theory controls the decomposition of mixed tensor space, and it serves as a test case for the cellular and "tower of recollement" methods used for the Brauer and partition algebras.
Cox, De Visscher, Doty and Martin (arXiv:0709.0851, 2007) determine the blocks of in characteristic zero. They also classify the semisimple walled Brauer algebras and give a linkage principle in positive characteristic. Their characteristic-zero answer has the shape familiar from algebraic Lie theory: blocks are orbits of a Weyl group, , under a dot action shifted by a vector . The analogous result for the ordinary Brauer algebra, with the Weyl group of type , is due to Cox, De Visscher and Martin (arXiv:math/0601387, 2009).
Fix , an algebraically closed field and . A Brauer diagram on strands pairs up nodes, northern and southern. Lines joining the two rows are propagating lines; the others are arcs. Put a wall after the first nodes of each row. A diagram is walled if no propagating line crosses the wall and every arc does. Two diagrams are multiplied by stacking the first above the second. Each closed loop formed in the middle row is removed and contributes a factor . The walled Brauer algebra is the -span of the walled diagrams with this product. The permutation diagrams span the group algebra of .
The algebra is cellular. Its cell modules are indexed by bipartitions with and , for . Here is the number of northern arcs. In characteristic zero the simple modules , the heads of the cell modules, are indexed by the same set. The one exception is , which is excluded when and . At , the algebra is and its unique simple has the empty bipartition as label. Two simple modules lie in the same block when no central idempotent of separates them.
A box in row and column of a Young diagram has content . Two bipartitions are -balanced when the boxes of can be paired with those of , and the boxes of with those of , so that the contents in each pair sum to .
For , the weight lattice is , with coordinates indexed by . Put
The group permutes the coordinates and acts by the dot action . A bipartition is sent to the weight .
For of characteristic , , and labels of simple -modules,
For every in characteristic , two labels are in the same block if and only if they are -balanced, and each block contains a unique minimal weight.
The milestones, in proof order, are the following.
The goal reduces the block structure of to a combinatorial test. Two weights are in the same block exactly when their -shifted vectors are permutations of each other, a check that takes linear time. Within a block there is a unique minimal weight. The Weyl-group description is the starting point for the paper's positive-characteristic linkage principle, in which the affine Weyl group takes the place of . It also places the walled Brauer algebra alongside the Brauer algebra and the algebraic groups as an algebra whose characteristic-zero blocks are governed by a reflection group.
The result has been proved since 2007. As far as is known, no part of it has been machine-checked. This mission produces three things.
The obvious first idea is to treat the walled Brauer algebra through mixed Schur–Weyl duality, as a centraliser algebra. That gives only a quotient of when is a small integer, and nothing at all when is not a natural number, so it cannot reach the full statement. The obstruction is the non-semisimple regime (, ), where cell modules have nontrivial composition factors.
The necessary condition is a scalar computation, obtained by evaluating a central-like element on cell modules. Sufficiency is the hard direction. It needs explicit nonzero homomorphisms between cell modules that differ by a removable strip of boxes, built from the two-box homomorphisms of Theorem 6.2 by an induction using restriction and induction along the tower . The final step, matching balance with dot orbits, is a combinatorial argument on edges of skew diagrams in which the shift by must be tracked exactly.
YoungDiagram, with 0-based cells; contents are unchanged by the shift. Nodes are Fin (r+s). The weight lattice is Fin r ⊕ Fin s → ℤ, where Sum.inl i is the paper's coordinate and Sum.inr j is coordinate . is Equiv.Perm (Fin r ⊕ Fin s).Two corrections to the printed text are adopted. Lemma 8.1 is stated "for all ", and the reflection formula on p. 31 is read as , the transposition of two coordinates. The label exception in Theorem 2.7(iii) is applied only when ; its literal wording would incorrectly leave without a simple module.
A trivializing formalization would replace the block relation by a relation defined through contents or orbits, or would replace the algebra by a centraliser algebra or by . Both are excluded: the block relation is the algebra's own central-idempotent relation, and the algebra is the diagram algebra itself.
Contributions are welcome at every layer. Useful general infrastructure includes associativity of diagram composition, Young symmetrizers and Specht modules over a field of characteristic , and the Jucys–Murphy content formula. Proofs of the combinatorial Section 8 results and of the cellular structure of are also needed.
A strongly continuous unitary representation turns each group element into a unitary operator on a Hilbert space. Averaging those operators against a smooth, compactly supported function gives a bounded operator. When every such average is trace class, its trace defines a distribution character. The trace condition is therefore a bridge from an operator representation to a scalar distribution that can be studied by harmonic analysis. Van Dijk, Neeb, Salmasian and Zellner collect and extend characterizations of this condition for finite-dimensional Lie groups in their 2015 preprint. Their Theorem 1.3 is the target here.
The authors identify one of the equivalences, between the trace class property and a trace class negative power of the Nelson Laplacian, with an earlier statement of Cartier that had appeared without a proof or reference. Their further conclusion that one finite degree of differentiability suffices is presented as a new result; it gives finite order for the distribution character. These are claims about the cited preprint, not claims of prior machine verification. Source: introduction and Theorem 1.3, pp. 2–5.
Let be a finite-dimensional real Lie group, let be a complex Hilbert space, and let be a strongly continuous unitary representation. Fix a left Haar measure . For a compactly supported continuous function , the integrated operator is for each . Write for compactly supported functions with continuous derivatives and for smooth compactly supported functions. Write and for the trace class and Hilbert–Schmidt ideals of bounded operators on .
Choose a basis of the Lie algebra . The Nelson Laplacian is in the enveloping algebra. The derived representation applies on smooth vectors. Its closure is a non-positive self-adjoint operator, and is bounded. The choice of basis determines , while the theorem holds for an arbitrary fixed basis. Source: §1 and proof of Theorem 1.3, pp. 3–4.
The mission goal is the complete five-way equivalence in Theorem 1.3:
The continuity clauses are part of the target; they cannot be inferred merely from the displayed inclusions. The milestone list includes the four nontrivial implications named in the paper's proof, its finite-order claim and the two displayed identities needed to connect the function and operator Laplacians. Source: Theorem 1.3 and proof, pp. 3–5.
Condition (iii) is formulated using every smooth compactly supported function. Condition (i) replaces smoothness by one finite differentiability order that works uniformly for the representation, while retaining continuity into the trace class ideal. This is the form needed to conclude that the distribution character has finite order. Condition (v) tests the same property with one operator associated with the Lie algebra basis. These consequences are stated by the authors in the introduction and derived in §1. Source: pp. 2–5.
A formal proof would connect Lie-group differentiation, Bochner integration, Schatten ideals and the topology of compactly supported function spaces in one reusable development. The target and milestones here are open Lean statements: compilation checks their types, not their proofs. The previously posed Lemmas 1.1 and 1.2 of the same paper remain separate open platform items, and can be used by solvers without being re-posed here.
Showing that each is trace class does not immediately give continuity of in trace norm: operator-norm convergence alone does not control trace norm. The paper also needs to pass from trace class images of smooth functions to an operator statement about , and then back to functions with only finitely many derivatives. The obvious shortcut of treating as a bounded operator fails because its natural domain is the smooth-vector space and its closure is generally unbounded. The proof therefore has substantial analytic content beyond elementary ideal inclusions. Source: proof of Theorem 1.3, pp. 4–5.
Lean represents as a Hausdorff finite-dimensional Lie group modelled on a finite-dimensional real normed space , equipped with a regular left Haar measure. It represents as a complete complex inner-product space, without a separability assumption, and the representation by a strongly continuous monoid homomorphism into unitary continuous linear equivalences. The Lie algebra is the tangent space at the identity, and the basis is an arbitrary finite basis of . The quantifiers for and include explicit lower bounds and , matching the paper's convention .
Smooth vectors are exactly those whose orbit maps are smooth. The derived action is the manifold derivative of that orbit map at the identity, used only on smooth vectors. The function-side Laplacian uses right-invariant directional derivatives; its second-order sign agrees with the paper's action. A bounded operator is characterized by on every smooth vector. The paper's essential self-adjointness and density statement identifies this uniquely with ; the theorem carries that characterization as a hypothesis. The hypothesis must be satisfiable, and the interpretation must remain the paper's resolvent.
Continuity on is encoded by a bound on the Schatten -norm for every compact support set, with one constant for all functions supported there. For , the derivative order may depend on the compact set. The Schatten norms and classes are reused published definitions, with norm values in ; no alternate trace norm is introduced. Equation (1) is an identity of distributions tested against smooth compactly supported functions. A complete proof needs the smooth-vector integration lemma, Lie-group test-function approximation, the function-side parametrix and operator ideal estimates. These components are useful beyond this mission.
Surfaces of three-dimensional objects are stored in computer graphics, vision and geometry processing as triangular meshes: finitely many points glued together by triangles. Geometric deep learning on such data needs a discretisation of the Laplace–Beltrami operator, because spectral filters, diffusion and many graph neural network layers on meshes are built from a Laplacian. The standard choice is the cotangent Laplacian, whose edge weights are cotangents of the angles of the mesh. It goes back to MacNeal's 1949 thesis and was popularised by Pinkall and Polthier (1993) and Meyer, Desbrun, Schröder and Barr (2003).
Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2), §4.6, pp. 61–63, introduces this operator and states that, although it is defined through angles, it can be written entirely in terms of edge lengths. This is what makes it intrinsic: invariant under every deformation of the surface that preserves the lengths of the edges. This mission formalizes that claim. The book numbers no theorems, lemmas or definitions, so every item is cited by section, equation and printed page.
A mesh on the nodes is a finite set of ordered triplets of distinct nodes, the faces; the order of a triplet is the orientation of the face, and each triangle occurs once. As assumed in §4.6, each edge belongs to two faces and the faces incident to each node form a single loop. The nodes are placed at points of a Euclidean space (the book's ). The mesh carries the metric
A quantity is intrinsic if it can be expressed through alone.
For a face with vertices , the angle is the angle at between the directions to and ; it is the angle opposite the edge . The area of the face is . The face is non-degenerate when its three vertices are affinely independent, that is, not collinear.
The local area element of a node is , one third of the total area of the faces incident to . For an interior edge shared by exactly two faces and , the cotangent weight of equation (25) is
In general, sums the cotangents of the angles opposite over the faces containing that edge. The Laplacian of equation (24) is the matrix , where holds the weights off the diagonal and with .
Heron's expression of three lengths, with semiperimeter , is
For an interior edge whose two faces and are non-degenerate, with and given by Heron's expression,
and the weight of (25) is this right-hand side divided by .
The printed display sets the right-hand side equal to itself. That omits the factor of (25), so the goal states the corrected identity.
The Laplacian with the unnormalised weights is symmetric and positive semidefinite for every manifold mesh of non-degenerate triangles (p. 63, after Wardetzky et al. 2007).
The intrinsic form of the cotangent weights is what makes the cotangent Laplacian, and everything derived from it, invariant under isometric deformations of a mesh. This includes its eigenvalues and eigenvectors, and hence spectral descriptors, heat kernels and spectral convolutions. A bent or articulated shape and its rest pose then give the same operator, which is the reason for the operator's use in shape analysis and in geometric deep learning on meshes.
The individual facts (the law of cosines, Heron's formula, the Dirichlet-energy form of the cotangent Laplacian) are classical and proved in the literature. None of them is stated on the platform for meshes. Mathlib has the law of cosines (EuclideanGeometry.law_cos) but Heron's formula only in its non-importable Archive, and it has no mesh Laplacian. This mission adds a mesh layer to the platform: triangulated faces, edge lengths, face areas, local area elements, the cotangent weights (25) and the Laplacian (24). It also corrects two slips on p. 63: the normalisation in the intrinsic display, and the symmetry claim for (25)'s weights.
The per-face identities are classical trigonometry. The difficulty is not the trigonometry but connecting an extrinsic quantity, an angle between vectors of the ambient space, to a square root of a polynomial in lengths, with the sign under the square root controlled for every triangle, degenerate ones included.
The mesh-level statements need bookkeeping that the page leaves implicit. A face is stored with one orientation, so an edge can appear as inside it, and the angle opposite must be found at whichever vertex is left. The sum defining ranges over all faces, and the hypothesis that is interior has to reduce it to exactly two terms. Isometry invariance must also cover degenerate faces, where Lean assigns junk values to angles. Positive semidefiniteness is the hardest item: obtuse angles have negative cotangents, so the weights can be negative and the usual argument for graph Laplacians with nonnegative weights does not apply.
Nodes are Fin n. The embedding x : Fin n → P takes values in an arbitrary Euclidean affine space P (a real inner product space torsor), of which is an instance. A mesh (TriMesh n) is a Finset of ordered triplets with three distinct nodes per face and no triangle listed twice. The mesh-level theorems assume IsManifoldMesh: a nonempty face set, two faces per edge, and a connected loop of incident faces at each node. Angles are Mathlib's EuclideanGeometry.angle, with the vertex in the middle argument, and is Real.cot. The face area is defined geometrically as and not by Heron's formula; with the latter, Heron's formula and the intrinsic claim would hold by definition and lose their content. The local area element sums the areas of the faces incident to , each counted once. This is the book's formula read over unoriented faces.
The book assumes non-degenerate triangles throughout. Lean's returns the junk value at the angles and , and the Heron area of a degenerate triangle is . So the cotangent identities assume that the triangles in their denominators are non-degenerate (affinely independent vertices). The goal assumes this for the two faces of the edge, and the companion for every face. Heron's formula and isometry invariance also hold for degenerate triples. Every mesh-level theorem carries the standing manifold-mesh condition of pp. 61–62; the goal additionally identifies the two faces of its chosen interior edge.
Contributions welcome: proofs of Heron's formula for points of a Euclidean space, of the per-face cotangent identity, and of the per-face positive semidefinite form. These three are reusable for any discrete differential geometry on the platform.
Geometric deep learning is the programme, set out by Bronstein, Bruna, Cohen and Veličković in Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), of deriving neural network architectures from the symmetries of the domain on which the data live. Convolutional networks on images, permutation-invariant networks on sets, graph neural networks and equivariant networks for molecules are presented there as instances of one template. Chapter 3 of the book, Geometric Priors, gives that template: it fixes what a symmetry of a signal is, what it means for a function to respect it, and how invariant functions are assembled from simpler blocks. This mission formalizes the definitions and the elementary claims of Chapter 3. Its goal is the observation the book uses to explain why such networks must be non-linear.
The book numbers no theorem, lemma or definition. Its only labels are the sections, the equations (1)–(53) and the figures. Every item of this mission is therefore cited by section, equation number (where there is one) and printed page of the arXiv v2 text; a margin note is cited as "side-note, p. n".
A domain is a set . A signal on with values in a set of channels is a function ; the signals form the space (equation (1)), written when .
A group acts on through a map with . It then acts on signals by equation (3):
On real signals this action is linear, so defines a representation of on .
A function is -invariant if for all and . A map between signal spaces on which acts is -equivariant if . A map acts on signals element-wise, .
For a measure on with , the -average of a real signal is
The book takes to be the Haar measure of the group.
The metric distortion of a map between metric spaces is (§4.4, p. 51). A self-map with distortion at most is an -isometry.
The Geometric Deep Learning Blueprint (§3.5, p. 29) builds functions
from equivariant linear layers , element-wise nonlinearities , poolings onto coarser domains, and an invariant global pooling .
For a finite domain , a finite nonzero measure on , and a linear -invariant map from into a real Banach space, for every signal ,
A linear invariant therefore depends on only through .
With and , , so .
The goal is the book's reason for non-linearity. Linear invariant models collapse to functions of the group average, so they cannot tell apart two images with the same mean colour. Expressive invariant models must interleave equivariant linear layers with non-linear maps. Milestones 5–7 are the positive half of the same argument: element-wise nonlinearities keep equivariance, the average turns equivariance into invariance, and stacking such blocks gives the blueprint that the later chapters instantiate on grids, groups, graphs and manifolds. Milestone 4 is the book's reason for leaving exact symmetry behind: small deformations do not form a group, so it replaces invariance to deformations by stability to them.
Each claim of the chapter is proved in one or two lines on the page, and none is new mathematics. What a formalization adds is the precise setting in which they hold. The book names the Haar measure but its identity needs no invariance of ; the average's invariance needs right invariance, which the page does not state; and the printed blueprint is invariant only if the poolings are equivariant. As far as a search of the platform and Mathlib shows, none of these statements has a machine-checked proof. The definitions here (the action on signals, invariance, equivariance, the average, the blueprint) are reusable by every later mission of this series.
The obvious argument for the goal pulls through the integral, which uses linearity in the form "a continuous linear map commutes with the Bochner integral". That needs continuity of and integrability of , and neither is stated on the page. On a finite domain both follow from the setting, finite dimension for continuity and boundedness with measurability for integrability. The measurability of has to be assumed of the group and the action.
For the average's invariance, the substitution is valid only for a right-invariant measure. For the blueprint, the composite's invariance fails for a non-equivariant pooling, so the box's claim is false as printed. For the -isometries, the subtle half is the negative one: exhibiting a deformation that is an -isometry while its square is not.
Ω → C. The goal and the average use real signals on a finite domain ([Fintype Ω]), following the book's side-note on p. 15 that one must always discretise to a finite grid in practice; the other milestones allow any domain and any channel types.act g x := fun u => x (g⁻¹ • u) for [MulAction G Ω], not a MulAction instance on Ω → C.μ with [IsFiniteMeasure μ] and μ ≠ 0. Without those hypotheses Lean's (μ univ).toReal⁻¹ would be and the goal false. The goal assumes no invariance of μ. Milestone 6 adds [μ.IsMulRightInvariant], which the Haar measure of a compact group satisfies.[MeasurableInv G], [MeasurableSMul G Ω] and the discrete σ-algebra on Ω; integrability of g ↦ g.x is a consequence, not a hypothesis. A finite group with the counting measure and a compact group with its Haar measure both fit.The goal cannot be satisfied trivially. groupAverage is defined from μ and the action alone, the goal quantifies over every linear invariant f, and the measure hypotheses exclude the degenerate case in which the average is . Proofs, finite-sum encodings of the average, and versions for complex or vector-valued channels are welcome.
Many learning problems take an unordered collection as input: the points of a point cloud, the particles of a physical system, the atoms of a molecule, the nodes of a graph. Storing such data in memory fixes an order of the elements, but the order carries no information, and a model whose output changes when the rows of its input are shuffled is answering a different question from the one posed. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), §4.1, make this the first instance of their blueprint: the domain is a set (or a graph) of nodes, and the symmetry group is the symmetric group of all reorderings.
Two architectures used in practice follow this pattern. Deep Sets (Zaheer et al., NeurIPS 2017) and PointNets (Qi et al., CVPR 2017) process sets; message-passing graph neural networks process graphs. The design question in both cases is which layers respect the symmetry. For linear layers the question has a complete answer, and the answer determines the layer used by Deep Sets. For graphs, Maron, Ben-Hamu, Shamir and Lipman (2018) counted the linear layers acting on adjacency matrices.
A set of nodes carries node features , stacked as the rows of a matrix . A graph adds an adjacency matrix , eq. (8), whose nonzero entries are the edges.
A permutation acts through its permutation matrix by reordering rows: row of is row of . On adjacency matrices it acts by , reordering rows and columns together.
A function is permutation invariant if for every permutation matrix , and a matrix-valued function is permutation equivariant if . On graphs the book's definitions (9) and (10) are
for any permutation matrix .
The section's constructions are the sum readout (6); the shared node-wise linear map (7); the neighbourhood (11) and the multiset of neighbourhood features (12); and the local layer whose -th row is (13). For one feature channel the two linear generators are the identity and the average , every entry of which is the mean .
The book numbers no theorems, lemmas or definitions; every item of this mission is cited by section, equation number and printed page.
For and a linear map ,
This is the book's sentence on p. 33: any linear equivariant "can be written as a linear combination of two generators, the identity … and the average". Both directions are stated; the content is the "only if" direction.
The result. The goal classifies the linear layers of a set network. Any equivariant linear layer on scalar node features mixes each node's own value with the mean of all values, and nothing else; with several channels the two scalars become two weight matrices, which is exactly the Deep Sets layer. Read the other way, the theorem says that the commutant of the permutation representation of on is two-dimensional (for ), the algebraic fact behind the decomposition into two irreducible pieces. The Maron et al. count does the same for layers acting on adjacency matrices and fixes the size of the parameter space of invariant graph networks. The milestones give the elementary invariance and equivariance facts on which the graph-network chapter rests, including the constant aggregate on a complete graph.
Formalizing it. All results here are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no statement about the commutant of the permutation representation or about equivariant layers on sets. The mission produces a vocabulary of permutation actions on feature and adjacency matrices, and the invariance and equivariance definitions (9)–(10), that later missions of this series (the WL comparison, the E(3)-equivariant layer) also use. Two of the book's printed claims need correction to be true, and the formal statements record the corrected versions.
The milestones are short reindexing arguments; the work is in choosing encodings that keep them faithful. The goal's "if" direction is a one-line computation. The "only if" direction is where an argument is needed: equivariance under all of must force the matrix of to have one value on the diagonal and one value off it. Equivariance under a smaller group does not suffice: commuting with the cyclic shift alone gives all circulant matrices, an -dimensional space, so the argument must use permutations beyond the shifts. The channel version adds a tensor-product layer to the same argument. The Maron et al. count is a dimension statement, so it needs both a spanning family and its independence, and the count is sensitive to : for the dimension is strictly smaller than 15, so any argument must use somewhere.
Node features are Matrix (Fin n) (Fin d) ℝ (rows are nodes); a single channel is Fin n → ℝ. A permutation is σ : Equiv.Perm (Fin n), acting by X.submatrix σ.symm id (row of is row ) and on adjacency matrices by A.submatrix σ.symm σ.symm; this one convention is used in every statement. Adjacency matrices are real; the edge set is the set of nonzero entries, which for the book's 0/1 matrix (8) is its edge set and also admits weighted graphs. The function of (13) and the aggregator of §5.4 take a Multiset, so their invariance to the order of the neighbours holds by construction. The average is written with , and the goal and channel version assume . Equivariance quantifies over every permutation of , never a generating subset. The complete-graph item states the identical-aggregate clause of §5.4. The page's later claim of equal expressive power across inputs is false: with , , , and , changing changes while stays fixed, which no node-only map can reproduce.
A trivializing formalization is ruled out: "equivariant" is the commutation property itself, never defined as "of the form ".
Two printed claims are corrected. On p. 33 the two-generator form is stated for matrices with channels; it is false for (the map of (7) is a counterexample), so the goal is single-channel and the multi-channel statement uses weight matrices. On p. 34 the fifteen generators are said to be independent of ; the dimension is 1, 8 and 14 for , so that item assumes , and it is stated for adjacency-to-adjacency maps as the side-note on p. 33 specifies.
The development needs Mathlib's Equiv.Perm, Matrix.submatrix, Finset sums and reindexing (Equiv.sum_comp), Multiset.map, and Module.finrank. Proofs of the commutant statements, of the multi-channel version and of the dimension count are welcome; the permutation-action and invariance lemmas proved along the way are reusable by any later development on graph networks.
Convolutional networks use the same filter at many locations. A shift of the input then shifts the output in a predictable way, allowing one set of filter coefficients to serve every location. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, §4.3, pp. 40–43 ask how this idea extends when the transformations form a group and the signal domain need not be the group itself. A grid and its cyclic shifts are one example; a sphere and its rotation group are another. In the latter example, a rotation is an output index even though it is not a point of the sphere. This distinction matters when a second convolutional layer processes the first layer's output.
The chapter places this construction within its general account of geometric deep learning: symmetries specify how inputs transform, and a compatible map should transform its outputs in a corresponding way. Here the concrete question is whether the integral defining group convolution has that compatibility. The source calls this property equivariance and gives it immediately after equation (14). The book numbers equations but no theorems, lemmas, propositions, or definitions, so the items below are cited by section, equation, and printed page.
Let be a group acting transitively on a domain ; write for the image of . The section makes this homogeneous-domain assumption explicit on p. 43. A signal is a scalar function , and a filter is another such function . The group acts on signals by the inverse action on their arguments:
This convention makes a left group representation on functions. Let be a measure on invariant under the action of every element of . The book states this measure convention beside its pairing formula on p. 41. The pairing and group convolution are
The convolution is indexed by , so it is a signal on , even when and are different spaces. Signals use the regular action . On the cyclic grid , the source uses for the action of a shift on an index . These conventions are the ones used throughout this mission. Equation (14) and the surrounding definitions, §4.3, pp. 41–43.
For every and scalar signals on , the main target is
The theorem keeps the domain action and the output regular action distinct. The invariant measure and transitive action are part of the source's setting. §4.3, equation (14) and the following displayed identity, p. 41; homogeneous-domain assumption, p. 43.
The milestone list records three claims from the same section. First, the pairing matches a transformed filter to the inversely transformed signal: . Second, the signal action satisfies . Third, for on the cyclic grid, the finite-sum instance of group convolution has the form . The source's side-note calls the last expression cross-correlation. §4.3, pp. 41–42.
The equality specifies what happens to every output coordinate after a group transformation of the input. Its output is a function on , so the statement also fixes which action later layers must use. In the sphere example, the first convolution produces a function on the rotation group rather than a function on the sphere; the book then describes applying a second group convolution on that output. §4.3, pp. 42–43.
The result is proved in the source. The remaining work here is to make the invariant measure, the two actions, and the real integral into separately inspectable Lean definitions and to supply machine-checked proofs of the open theorem statements. The cyclic example checks the sign convention at a concrete boundary: using for the group action yields after applying the inverse shift. Those definitions can also support later formalizations of group-indexed layers. This mission does not assert results for learned networks or approximation power; its target is the mathematical convolution identity displayed in the book.
The two occurrences of in the printed identity act on different function spaces. On the left, transforms a signal on ; on the right, the regular action transforms a function on . Treating both as a single action obscures the type and can silently reverse the group multiplication order. The group need not be commutative, so this order matters. The measure must also be invariant: a Dirac measure concentrated at a point that moves under the group generally changes the pairing and breaks the claimed equivariance. In the cyclic example, an inverse shift changes the sign again, which is why the output has rather than .
Lean represents a signal as a function , the group action using MulAction, and the measure as a measure on . The action on signals, the pairing, group convolution, and the output regular action are explicit functions. The integral theorems require a transitive action, as the section specifies on p. 43, plus measurable spaces on and , a measurable group action, and an invariant measure. These are the conditions under which the source's change of variables is meaningful. The cyclic example applies the same group convolution to the counting measure on ZMod n, , with the shift group acting by . It does not identify a cyclic convolution with a planar convolution or assume the group and domain coincide in the general theorem.
The source describes as a Hilbert space. The Lean theorem states the integral identity for arbitrary real functions; on integrable products the pairing has its ordinary meaning, while Lean assigns zero to a nonintegrable integral. The identity remains valid at those totalized inputs because the same measure-preserving transformation relates the two integrands. No integrability hypothesis is used to reduce the stated range. The zero measure is included, but the theorem is universal over invariant measures, including nonzero counting measure on finite group actions; it cannot be proved by choosing a zero measure or an empty domain. Reusable contributions include properties of the signal action, invariant integration under actions, and finite cyclic examples. The transform-and-convolve equation (32) and the second-layer composition on are outside this chunk's milestone list.
Many spaces used in differential geometry are described by the maps permitted into them from simple domains. For a diffeological space, the domains are open subsets of Euclidean space; for a Chen space, they are convex subsets. A map between spaces is smooth when it sends permitted plots to permitted plots. Baez and Hoffnung use the language of concrete sheaves to put these examples in one setting and to explain why their categories share certain categorical properties (Baez–Hoffnung, §§1 and 4). A common theorem matters because it identifies which properties follow from the site of domains and its covers, without relying on a coordinate presentation of either kind of smooth space.
The paper first defines a quasitopos in Definition 8 and states the smooth-space application as Theorem 9, both on page 17. It then builds the general theory of concrete sites and spaces in §§4–5. Theorem 52 on page 40 is the general result from which the smooth-space application follows, using the paper's identifications of Chen and diffeological spaces with suitable categories of spaces (Baez–Hoffnung, Theorems 9 and 52). This mission targets that general theorem.
A site consists of a category of domains and a coverage . A covering family of a domain is a family of arrows into . The coverage requires that a cover can be refined after pulling it back along any arrow. A presheaf assigns a set of plots to each domain and restricts plots along arrows. It is a sheaf when every compatible family of plots over a cover has exactly one amalgamating plot. Compatibility tests equality after further restriction along arrows into two members of the cover (Baez–Hoffnung, Definitions 10–15).
A concrete site has a terminal domain . Maps are the points of , and maps between domains are determined by their action on points. Every point of a covered domain must lift through some covering arrow. The site is also subcanonical: each representable presheaf is a sheaf. These are exactly the conditions of Definition 18, including the subcanonicity of Definition 17 (Baez–Hoffnung, p. 19).
A plot has an underlying function , defined by . The presheaf is concrete if no two distinct plots have the same underlying function. A space is a concrete sheaf, and a map of spaces is a natural transformation of presheaves. Their category is written (Baez–Hoffnung, Definitions 19–20). Its underlying-set functor evaluates a space at .
The goal is the full assertion of Theorem 52:
A quasitopos is locally cartesian closed, has finite colimits, and has a weak subobject classifier. A weak classifier consists of an object and a truth arrow ; each strong monomorphism is the pullback of along a unique characteristic arrow . Local cartesian closure means that for every space , the slice is cartesian closed: it has finite products, and product with any object over has a right adjoint. The paper gives these notions in Definitions 8, 38, 42, and 43 (Baez–Hoffnung, pp. 17, 30, 32–33).
The milestones follow the paper's proof, in order. Four of them are the results cited in the proof of Theorem 52: Proposition 39 (all small limits, computed pointwise), Proposition 40 (the weak subobject classifier), Proposition 45 (local cartesian closure), and Proposition 50 (all small colimits). Together they cover every clause of the target. The others are the results these four rest on:
The classifier in Proposition 40 is the paper's of Proposition 30; the milestone states the existence property (Baez–Hoffnung, pp. 24–40).
The theorem provides a single categorical setting for several plot-based smooth-space constructions. All small limits and colimits allow diagrams of spaces to be assembled within the same category. Local cartesian closure gives parametrized mapping spaces over an arbitrary base, while the weak classifier describes strong subspaces through characteristic maps. These are the specific convenient properties singled out by the paper, and Theorem 9 transfers them to the paper's smooth-space examples (Baez–Hoffnung, §§3 and 5).
The mathematical theorem is already proved in the cited preprint. This mission supplies Lean statements for its general hypotheses, categorical notions, the thirteen results of §5 its proof uses, and its final conclusion. The drafted theorem bodies contain sorry; the work remaining is to prove them and build reusable support for concrete sheaves, pointwise limits, parametrized mapping spaces, and concrete sheafification. A machine-checked development would permit later applications to particular sites without restating the same categorical infrastructure. The present draft does not claim a machine-checked proof.
Presheaf categories already have pointwise limits and colimits, but a pointwise construction need not visibly retain both the sheaf and concreteness conditions. In particular, pointwise colimits of concrete sheaves do not by themselves establish Proposition 50; the result must return to the category of concrete sheaves. For local cartesian closure, constructing a mapping object in the unsliced category handles only the case of a terminal base. Proposition 45 requires the corresponding statement in each slice and for each object over that base. A classifier for every monomorphism would ask for a different property: the paper classifies strong monomorphisms, while it gives examples showing that arbitrary monomorphisms need not be subspaces (Baez–Hoffnung, pp. 10 and 26–37).
The Lean development fixes a universe , a small category with SmallCategory D, a coverage , and a chosen terminal domain with proof that it is terminal. Presheaves are . A covering family is represented by a Mathlib presieve; repeated arrows have no effect on the sheaf or point-covering conditions. The sheaf predicate uses Presieve.IsSheafFor for each member of the coverage. Subcanonicity, faithfulness of , and pointwise surjectivity of covers are all clauses of the concrete-site predicate. The smallness restriction and choice of are explicit scope decisions: the preprint states its theorem for any concrete site, while this development works in Mathlib's small-site setting.
DSpace is the full subcategory of presheaves satisfying the sheaf and concreteness predicates. Its morphisms are natural transformations. The truth-value object uses Bool; the paper's set has the same two elements. Concretization is represented by the image of the map sending a plot to its underlying function, which is canonically the quotient described in Definition 46. The weak-classifier predicate carries a terminal object as existence data; the quasitopos predicate takes finite limits as an instance, reflecting the ambient assumption in Definition 38. The goal's limits clause supplies this instance. In the slice predicate, is used; symmetry identifies it with the paper's .
The classifier must classify strong monomorphisms, and local cartesian closure must range over every slice. Mathlib's Classifier, which classifies all monomorphisms, would make the goal false: the paper's example of the reals with the discrete structure mapping to the standard reals (p. 10) is a monomorphism that is not a subspace. Ordinary cartesian closure is only the case of a terminal base. A model with functions between underlying sets as morphisms would not be Definition 20 and would make Proposition 28 trivial. The complete proof will need Mathlib's coverage and sheaf APIs, strong monomorphisms, pullbacks, slice categories, adjunctions, and limit and colimit interfaces. The concrete-site and -space definitions can be reused for further results of this paper. Lemma 44 takes the existence of the pullback and product as instance arguments, which Proposition 39 supplies; Lemma 47 states the adjunction as the universal property of the quotient map ; Lemma 49 uses Mathlib's plus construction for the Grothendieck topology generated by , as the paper's proof does. Contributions toward the milestone proofs are in scope; the site-specific equivalences used for Theorem 9 are outside this mission.