Motivation

A system of users sharing resources may have no stable configuration: whenever the users settle on their choices, somebody may prefer to change. Weighted congestion games describe this question when different users place different demands on the resources they choose. Routing and scheduling provide examples, but the mathematical question here does not impose a particular network or scheduling structure. It asks which resource cost functions guarantee stability regardless of the finite population, its demands, and its feasible choices. Harks and Klimm give a classification of such functions in their 2012 paper, Theorem 5.1.

There are two distinct requirements. A stable configuration may exist even when some sequences of individually profitable moves cycle forever. Guaranteeing that every sequence terminates is generally stronger. The result identifies the continuous function classes for which these two universal guarantees coincide. The word “universal” matters: the assertion concerns all games generated by a class of costs, rather than the behavior of one specified game.

Setting

A weighted congestion game has a nonempty finite set of players $N$ and a nonempty finite set of facilities $F$. Each player $i$ has a positive real demand $d_i$ and a nonempty finite collection $S_i$ of available strategies. A strategy is a subset of facilities; it may itself be empty. A profile $s$ chooses one strategy $s_i\in S_i$ for every player. Facility $f$ has a real-valued cost function $c_f$ defined on the nonnegative half-line. Its load and a player's private cost are

$$\ell_f(s)=\sum_{j:\,f\in s_j}d_j, \qquad \pi_i(s)=\sum_{f\in s_i}d_i c_f(\ell_f(s)).$$

Costs can have either sign, and the game model imposes no monotonicity. A pure Nash equilibrium is a profile $s$ satisfying $\pi_i(s)\le\pi_i(t_i,s_{-i})$ for every feasible unilateral change $t_i$. A strict improvement lowers the deviating player's cost. The finite improvement property, or FIP, excludes improvement cycles, equivalently infinite improvement paths in this finite profile space. These conventions follow §2 and Definition 2.1.

For any set $C$ of cost functions, write $\mathcal G(C)$ for all such games with $c_f\in C$ at every facility. The class is consistent if every game in $\mathcal G(C)$ has a pure equilibrium, and FIP-consistent if every such game has the FIP. The class can be infinite or empty. In the results below, continuity always includes the endpoint zero. “Monotonic” means nondecreasing or nonincreasing, with the direction allowed to differ between functions.

Formalization targets

The goal is Theorem 5.1, p.427. For a set $C$ of continuous functions, the following are equivalent:

$$C\text{ is consistent};\qquad C\text{ is FIP-consistent};$$ $$\left[\forall c\in C\ \exists a_c,b_c\in\mathbb R\ \forall x\ge0,\ c(x)=a_cx+b_c\right] \quad\text{or}\quad \left[\exists\varphi\in\mathbb R\ \forall c\in C\ \exists a_c,b_c\in\mathbb R\ \forall x\ge0,\ c(x)=a_ce^{\varphi x}+b_c\right].$$

The exponential rate is shared by the entire class. No coefficient or rate is subject to a sign or nonzero restriction. The disjunction is inclusive, as printed in the theorem: classes of constant functions satisfy both alternatives.

Six source milestones support this target. Lemma 3.1 characterizes monotonicity by local right-hand comparisons with $c(0)$. Lemma 3.2 supplies positive loads $0<x<y$ with either $c(y-x)<c(y)<c(x)$ or the reversed inequalities. Lemma 3.4 asserts monotonicity of the integer hull with offsets

$$\mathcal L_{\mathbb Z}(C)=\left\{x\mapsto\sum_{k=1}^{K}a_kc_k(x+b_k):a_k\in\mathbb Z,\ b_k\ge0,\ c_k\in C\right\}$$

under unrestricted consistency. Proposition 5.1 uses consistency for exactly three players to obtain monotonicity of both restricted hulls

$$\mathcal L_{\mathbb Z}^2(C)=\{a_1c_1+a_2c_2:a_1,a_2\in\mathbb Z,\ c_1,c_2\in C\},$$ $$\mathcal L_{\mathbb Z}^3(C)=\{x\mapsto a_1c(x)+a_2c(x+\delta):a_1,a_2\in\mathbb Z,\ c\in C,\ \delta>0\}.$$

Lemma 4.1 equates monotonicity of every integer combination of two continuous monotonic nonconstant functions with affine dependence between them. Lemma 5.1 equates monotonicity of the translated-function hull with each function being affine or exponential; its rate may depend on the function. The source locations are pp.422–427, §§3–5.

Significance

The classification separates structural guarantees from favorable individual instances. A class that fails the displayed alternatives cannot guarantee a pure equilibrium for every admissible game. Conversely, either alternative guarantees termination of strict improvement paths as well as equilibrium existence. This gives a precise answer to the unrestricted consistency question posed by Harks and Klimm, without imposing nonnegative or increasing costs.

The mathematical results are published results, not new conjectures. The remaining task is their machine-checked proof. This draft supplies compiled definitions and theorem statements; the seven theorem bodies remain proof targets. Its reusable components include the finite weighted game model, universal class predicates, and three different integer hulls. Published pure-equilibrium and improvement-path definitions are reused through their existing interfaces.

Difficulty

Monotonicity of individual resource costs does not settle the unrestricted problem. The selected statements impose conditions on combinations of functions, and those conditions distinguish the allowed class-wide structure. In particular, separate exponential representations for every member do not establish the common-rate alternative. Another logical obstacle is that an improvement cycle alone need not rule out an equilibrium elsewhere in a game's profile space. The source's nonexistence arguments must exclude every feasible equilibrium, not just exhibit cycling behavior. These distinctions are visible in §§3–5.

The findings accompanying this mission record local issues in printed proofs separately from their theorem statements. Such issues do not authorize stronger hypotheses or weaker conclusions in the faithful targets.

Formalization scope

Players and facilities are indexed by finite initial segments with strictly positive sizes. Strategies are finite subsets, and feasible strategies are subtypes of the specified nonempty families. This represents every finite game up to relabeling. Demands are strictly positive nonnegative reals, loads are finite sums, and private costs are ordinary reals. Payoff-maximizing published definitions receive the negative of the private cost. Finite profile spaces justify the equivalence of the published infinite-path FIP convention and the paper's cycle convention.

Consistency is defined by quantification over all admissible games; neither potentials nor the classification are included in admissibility. The hulls are constructed from integer coefficients and the stated translates, without selecting only their monotonic members. Continuity is imposed on the whole nonnegative domain. These choices exclude vacuous proxy models and restricted strategy classes. The empty class and constant functions remain included. No asymptotic estimates or extracted constants occur.

The twelve new definition items precede the seven theorem items, and the six numbered source milestones retain their provenance. No optional variant is posed. The independent two-player characterization and the network and singleton results are outside the mission. In particular, the correction notice on p.436 concerning finite rather than polynomial termination does not introduce an algorithmic target here. Contributions should complete the faithful statements and their needed supporting theory while preserving these conventions.

Selected references

• Tobias Harks and Max Klimm, On the Existence of Pure Nash Equilibria in Weighted Congestion Games, Mathematics of Operations Research 37(3), 419–436, 2012. Published article and correction notice. All theorem numbering and quotations use this published artifact.

Reliable linear constraints under uncertain data

A production or allocation decision can satisfy a linear constraint for nominal data and violate it when those data change. Robust optimization asks for a decision that satisfies the constraint for every realization in a prescribed uncertainty set. The uncertainty set is part of the model: the requirement does not attach probabilities to its elements, and it does not permit a small violation at an unfavorable realization. Chapter 1 of Ben-Tal, El Ghaoui and Nemirovski, Robust Optimization develops this interpretation for linear optimization.

This requirement initially gives infinitely many inequalities, even when the decision vector has only a few coordinates. The chapter's representation results identify uncertainty descriptions for which those inequalities can be replaced exactly by finite systems. The replacement matters to applications because it preserves the set of admissible decisions while expressing it in the language of linear, conic quadratic, or semidefinite optimization.

Affine uncertainty and lifted descriptions

Let $x\in\mathbb R^n$ be the decision vector and $z\in\mathbb R^L$ the perturbation. The nominal coefficients are $a^0\in\mathbb R^n$ and $b^0\in\mathbb R$, with shifts $a^\ell,b^\ell$ for each perturbation coordinate. The robust linear constraint is

$$(a^0)^Tx+\sum_{\ell=1}^Lz_\ell(a^\ell)^Tx \le b^0+\sum_{\ell=1}^Lz_\ell b^\ell \qquad\text{for every }z\in Z.$$

A lifted conic description specifies the perturbation set by

$$Z=\{z\in\mathbb R^L:\exists v\in\mathbb R^u,\ Pz+Qv+p\in K\}.$$

Here $P,Q$ are linear coefficient arrays, $p$ is an offset, and $K$ is a cone. The variable $v$ describes the uncertainty set; it is not a decision made after uncertainty is observed. The general theorem assumes that $K$ is closed, convex and pointed, with nonempty interior. The perturbation set is nonempty. For a nonpolyhedral cone, the description must have a point strictly inside the cone.

An equivalent representation has additional variables but projects to precisely the original feasible set. The interpretation is existential: a feasible decision $x$ must admit a certificate, and every feasible pair must project to a robust feasible $x$. This is Definition 1.3.1 of the source, not a sufficient-condition approximation.

Formalization targets

The goal is Corollary 1.3.5, printed page 21. If the description uses a nonnegative orthant, a product of Lorentz cones, or a positive semidefinite cone, the robust constraint has an explicit LP, SOCP, or SDP representation, respectively. Strict feasibility is required for the latter two cases. With auxiliary variable $y$, the system is

$$p^Ty+(a^0)^Tx\le b^0,\qquad Q^Ty=0,$$ $$(P^Ty)_\ell+(a^\ell)^Tx=b^\ell\quad(1\le\ell\le L),\qquad y\in K.$$

The goal includes the polynomial size of this representation and the explicit dependence of its coefficients on the input data. It also records preservation of the set of feasible objective values for an objective depending only on $x$.

Theorem 1.3.4 is the general supporting target. It gives the same system with $y\in K^*$, where $K^*=\{y:y^Tz\ge0\text{ for every }z\in K\}$, and allows either a polyhedral cone or a strictly feasible description. The two introductory examples give concrete representation targets:

$$(a^0)^Tx+\sum_\ell|(a^\ell)^Tx-b^\ell|\le b^0 \quad\text{for }Z=[-1,1]^L,$$ $$(a^0)^Tx+\Omega\sqrt{\sum_\ell((a^\ell)^Tx-b^\ell)^2}\le b^0 \quad\text{for }Z=\{z:\|z\|_2\le\Omega\}.$$

The box target includes its further representation by finitely many linear inequalities with auxiliary upper bounds on the absolute values. These are Examples 1.3.2 and 1.3.3, not additional general duality assumptions.

What the representation provides

The result identifies the finite certificate system appropriate to each uncertainty model. It distinguishes an exact reformulation from a conservative replacement that could exclude valid decisions. Because the original decision variables remain present, an objective can be retained without interpreting the auxiliary certificate as an additional physical decision.

The mathematical results are established textbook results. The work requested here is their formal proof against explicit Lean statements. The resulting definitions expose affine uncertainty, lifted perturbation sets and finite certificate systems for reuse. Published good-cone and dual-cone definitions are already available and are imported; the theorem statements in this mission remain open proof targets.

Difficulty and boundary behavior

The equivalence requires existence of a finite certificate, not merely a sequence approaching a limiting objective value. Nonpolyhedral descriptions can fail to admit the asserted certificate without strict feasibility. In contrast, the polyhedral case does not need a strictly feasible point, so imposing that condition uniformly would lose part of the source result.

There is also a distinction between a finite worst-case value and a perturbation attaining it. The proof on printed page 20 writes a maximization problem and then discusses its optimal value; this does not require primal attainment. The formal target uses universal feasibility directly. The local findings record an explicit nonattainment example, without establishing a gap in the duality argument.

Formalization scope

All coordinates are real and finite. Nominal coefficients are stored separately from perturbation shifts. Lorentz blocks contain a distinguished scalar coordinate and a finite vector part; their Euclidean norm is the square root of a sum of squares. PSD coefficients are symmetric matrices, and pairings sum all matrix entries, giving the trace pairing for symmetric inputs. Strict feasibility in that case means positive definiteness in the symmetric ambient space.

The representation is built from the coefficient arrays themselves. Robust feasibility is defined independently by universal quantification over perturbations; it is never defined as certificate existence. No rank condition is imposed on $P$ or $Q$. Nonnegative ball radii include zero, and zero-dimensional coordinate lists retain their ordinary empty-sum interpretation.

Formalization Note The explicit system has one scalar inequality, $u+L$ scalar equalities, and one standard cone block. If $N$ is its number of auxiliary scalar coordinates and $q$ its structural cone description length, the chosen dense counts are

$$I=1+n+L+u+N+(L+1)(n+1)+(L+u+1)N+q,$$ $$O=n+N+(u+L+1)(n+N+1)+q.$$

The size target is $O\le4I^2$, an explicit witness to the book's polynomial-size assertion. The constant is encoding bookkeeping, not a numerical complexity constant quoted from the book. PSD storage uses $k^2$ coordinates, including symmetric duplicates. These counts concern the finite representation, not bit complexity or the time needed to solve it.

Selected references

• Aharon Ben-Tal, Laurent El Ghaoui and Arkadi Nemirovski, Robust Optimization, Princeton University Press, 2009, Chapter 1, Definition 1.3.1, Examples 1.3.2–1.3.3, Theorem 1.3.4 and Corollary 1.3.5, printed pages 17–21. DOI.

Motivation

We present in this paper a set of routines constructed to compute the rank of a matrix Lie algebra and also to determine a Cartan subalgebra from a given list of elements

This mission is the statement-level formalization of Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica (arXiv:math/0205235v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

16 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is so(n): BSo ordered basis (so(n): BSo ordered basis, PDF p. 5). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

2 results of the paper are not stated yet, because the library lacks an interface they need:

• Abstract and introduction: rank/Cartan extension algorithm: A valid and fully specified exact Cartan-extension routine on the advertised real semisimple matrix embeddings, including guards and symbolic branch/parameter selection. (source-ambiguity)
• Introduction, unnumbered Teorema: claimed Cartan characterization: A valid Cartan characterization with the original quantification over all real semisimple matrix embeddings and all their Cartan subalgebras. (source-ambiguity)

Selected references

• Algorithm to compute the rank and a Cartan subalgebra of a matrix Lie algebra with Mathematica, arXiv:math/0205235v1, https://arxiv.org/abs/math/0205235v1

Motivation

In this paper, we introduce the notion of a normal form of one qubit quantum circuits over the basis $\{H, P, T\}$, where $H$, $P$ and $T$ denote the Hadamard, Phase and $π/8$ gates, respectively. This basis is known as the {\it standard set} and its universality has been shown by Boykin et al. [FOCS '99]. Our normal form has several nice properties: (i) Every circuit over this basis can easily be transformed into a normal form, and (ii) Every two normal form circuits compute same unitary matrix if and only if both circuits are identical. We also show that the number of unitary operations that can be represented by a circuit over this basis that contains at most $n$ $T$-gates is exactly $192 \cdot (3 \cdot 2^n - 2)$.

This mission is the statement-level formalization of Representation of Quantum Circuits with Clifford and $π/8$ Gates (arXiv:0806.3834v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1 (seed paper result): unique exact normal form (Theorem 1 (seed paper result): unique exact normal form, PDF p. 6). 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.

Selected references

• Representation of Quantum Circuits with Clifford and $π/8$ Gates, arXiv:0806.3834v1, https://arxiv.org/abs/0806.3834v1

Motivation

Matsumoto and Amano (2008) showed that every single-qubit Clifford+T operator can be uniquely written of a particular form, which we call the Matsumoto-Amano normal form. In this mostly expository paper, we give a detailed and streamlined presentation of Matsumoto and Amano's results, simplifying some proofs along the way. We also point out some corollaries to Matsumoto and Amano's work, including an intrinsic characterization of the Clifford+T subgroup of SO(3), which also yields an efficient T-optimal exact single-qubit synthesis algorithm. Interestingly, this also gives an alternative proof of Kliuchnikov, Maslov, and Mosca's exact synthesis result for the Clifford+T subgroup of U(2).

This mission is the statement-level formalization of Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators (arXiv:1312.6584v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

26 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is §1 main result: MA existence, uniqueness, optimality and effective normalization (§1 main result: MA existence, uniqueness, optimality and effective normalization, 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.

Deferred results

4 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 5.1: matrix-input optimal exact synthesis: An operational exact-arithmetic synthesis machine over encoded quadratic/cyclotomic coefficients, implementing parity-driven U -> N^{-1}U recursion with a fixed Clifford lookup and charged arithmetic operations, while preserving absolute phase (or the specified Bloch image) and returning actual normal-form/elementary-word data. (hard)
• Theorem 6.5: SO(3) ring characterization and synthesis: An operational exact-arithmetic synthesis machine over encoded quadratic/cyclotomic coefficients, implementing parity-driven U -> N^{-1}U recursion with a fixed Clifford lookup and charged arithmetic operations, while preserving absolute phase (or the specified Bloch image) and returning actual normal-form/elementary-word data. (hard)
• Remark 6.6: linear SO(3) synthesis: An operational exact-arithmetic synthesis machine over encoded quadratic/cyclotomic coefficients, implementing parity-driven U -> N^{-1}U recursion with a fixed Clifford lookup and charged arithmetic operations, while preserving absolute phase (or the specified Bloch image) and returning actual normal-form/elementary-word data. (hard)
• Section 8.1 Clifford E/X/S/omega coordinates: A correct coordinate range for the claimed unique E^a X^b S^c omega^d parametrization. (source-ambiguity)

Selected references

• Remarks on Matsumoto and Amano's normal form for single-qubit Clifford+T operators, arXiv:1312.6584v2, https://arxiv.org/abs/1312.6584v2

Motivation

A direct proof of the relation between the one-shot classical capacity and the minimal output entropy for covariant quantum channels is suggested. The structure of covariant channels is described in some detail. A simple proof of a general inequality for entanglement-assisted classical capacity is given.

This mission is the statement-level formalization of Remarks on the classical capacity of quantum channel (arXiv:quant-ph/0212025v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Irreducible covariance gives bistochasticity and the capacity–entropy identity (§1, theorem; (1)–(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.

Selected references

• Remarks on the classical capacity of quantum channel, arXiv:quant-ph/0212025v1, https://arxiv.org/abs/quant-ph/0212025v1

Motivation

This paper investigates properties of noisy quantum information channels. We define a new quantity called {\em coherent information} which measures the amount of quantum information conveyed in the noisy channel. This quantity can never be increased by quantum information processing, and it yields a simple necessary and sufficient condition for the existence of perfect quantum error correction.

This mission is the statement-level formalization of Quantum data processing and error correction (arXiv:quant-ph/9604022v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Coherent information bound and environment factorization criterion (§4, Eq.(4) and equality criterion, 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.

Selected references

• Quantum data processing and error correction, arXiv:quant-ph/9604022v1, https://arxiv.org/abs/quant-ph/9604022v1

PRIMES is in P: the polynomial Fermat congruence, the introspective groups, and the correctness of the Agrawal-Kayal-Saxena algorithm

1. Motivation

Agrawal, Kayal, and Saxena's "PRIMES is in P" (Annals of Mathematics 160 (2004) 781-793) settled a question open since the birth of complexity theory: primality has an unconditional, deterministic, polynomial-time test. The paper's algorithm is elementary - six steps: reject perfect powers; fix a small r; reject trivial factor witnesses; accept small inputs; test the congruence (X + a)^n = X^n + a modulo X^r - 1 for a = 1, ..., ell; accept. The mathematical heart is Lemma 2.1, a generalization of Fermat's Little Theorem to polynomial rings: for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X]. The correctness of the harder direction runs through the introspective machinery of Section 4: for a prime factor p of n with o_r(p) > 1, the numbers of I = {(n/p)^i p^j} are introspective for the polynomials of P = {the products of the generators X, X+1, ..., X+ell}; the residues of I generate a group G modulo r of size t > log^2 n; the images of P generate a group G-cal in the field F = F_p[X]/(h), h an irreducible factor of the r-th cyclotomic polynomial over F_p; Lenstra's lower bound and the Kalai-Sahai-Sudan upper bound on the size of G-cal collide unless n is a power of p, and step 1 excludes prime powers, so n is prime. Section 5 bounds the arithmetic work: O~(log^(21/2) n), unconditionally.

The mission formalizes the paper's mathematical content in Lean 4. The goal statement is Theorem 4.1: the algorithm of the algorithm layer returns PRIME if and only if n is prime. The milestones are the ingredients in attack order: the polynomial Fermat characterization (Lemma 2.1); the lcm lower bound (Lemma 3.1); the existence of a small r with large order (Lemma 4.3); the closure of introspection under multiplication (Lemmas 4.5 and 4.6); Lenstra's injectivity bound (Lemma 4.7); the Kalai-Sahai-Sudan collision bound (Lemma 4.8); and the polynomial work bound of Section 5 (Theorem 5.1, in generous integer form).

The source document is the uploaded paper (annals-v160-n2-p12.pdf in the mission materials).

2. The formalization fragment and conventions

The formalization is a two-layer development in the namespace AKS. The polynomial layer (AKS_poly) carries the congruences: congruence (1) as an equality in Z_n[X], congruence (2) as divisibility by X^r - 1 in Z_n[X], Definition 4.4's introspection relation over F_p[X], and the set P of products of the generators. The algorithm layer (AKS_alg) carries the arithmetic scaffolding and the algorithm itself: the integer logarithm, the multiplicative order, the lcm of the first numbers, the perfect-power predicate, the search for r, the loop bound, the six-step decision function, the set I and the residue group G, and the work measure of Section 5.

The following choices are disclosed explicitly.

1. 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.

2. 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.

3. Generous integer encodings of the logarithms. The paper's real-valued log n appears in the algorithm only through the threshold o_r(n) > log^2 n of step 2 and the loop bound ell = floor(sqrt(phi(r)) log n) of step 5. The mission encodes both with logUp n = floor(log2 n) + 1, which is strictly larger than log2 n: step 2 searches for the smallest r with ordR r n > logUp(n)^2, and ell is the floor of the product of the square root of phi(r) and logUp n, encoded exactly as the floor of the square root of phi(r) logUp(n)^2. Both encodings are generous in the directions that preserve correctness: primes pass congruence (2) for every a and r, so a larger threshold and a longer loop never reject a prime; and for the converse the larger threshold and loop only strengthen the group bounds that force composites out. The integer bookkeeping of the final chain - floor(sqrt t) logUp n + 1 at least sqrt t log2 n - is part of the proposed work of the goal, with the generosity supplying the slack.

4. The algorithm layer transcribes the six steps literally, with computable searches inside provable windows and classical decision where only the extension matters. ordR r a is the least k < r with a^k = 1 (mod r) - the window k < r is faithful because every multiplicative order divides phi(r) < r - and 0 when gcd(a, r) > 1. smallestR n searches the window bounded by the r_exists milestone's bound. aksDecide is stated with classical decision (open Classical, noncomputable): no execution of the test is ever needed, only its extensional behavior. aksWork is a computable schoolbook work measure charging logUp(n)^6 for step 1, r(logUp n + 1) for the searches of steps 2 and 3, and ell r n (logUp n + 1)(r + 1)^2 for the congruence loop of step 5.

5. The groups are encoded by witness windows, and the two bounds are stated in the paper's forms. G is the Finset of residues modulo r of the numbers of I, encoded by the witness window i, j < r - faithful under the coprimality of n/p and p to r, because both orders then divide phi(r) at most r, so every residue of an I-number is achieved inside the window. Lemma 4.7 is stated in the paper's form: two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h) (the field is AdjoinRoot h; the hypotheses carry h dividing X^r - 1, the primitivity - h not dividing X^k - 1 for 0 < k < r - irreducibility by instance, the introspectivity of I for P, and t at most the size of G). Lemma 4.8 is stated in the collision form: unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2. The cardinality bookkeeping between these forms and the size of G-cal - stars-and-bars for the lower bound with the unique factorization of the generator products, and the root bound of a polynomial over a field for the upper - is carried by Mathlib and is part of the goal's proposed work.

6. The field F = F_p[X]/(h) is taken with its factor h as an explicit parameter. The statements do not construct h; they carry h dividing X^r - 1, primitivity, and irreducibility as hypotheses (the latter two as Fact-class instances). The existence of h - an irreducible factor of the r-th cyclotomic polynomial over F_p of degree o_r(p), the standard fact of Lidl and Niederreiter cited as [LN] - is part of the mission's proposed work toward the goal.

7. The "is in P" claim is anchored by an explicit work measure, with the bit-cost correspondence in prose. Milestone 7 bounds aksWork by C logUp(n)^15, a generous integer form of Theorem 5.1's O~(log^(21/2) n) - the generous exponent absorbs the schoolbook charging model and the logUp slack. The correspondence between arithmetic-work measures and Turing-machine bit complexity - the standard O~(m) arithmetic on m-bit numbers of the paper's Section 5 - is carried in prose; a machine-level formalization is out of scope.

8. Pruned content. The paper's Section 5 refinements (Fouvry's Lemma 5.2 and the O~(log^(15/2) n) of Theorem 5.3, and the Lenstra-Pomerance variant), the conjectures (Artin's, the Sophie Germain density, Conjecture 6.1), and the historical survey of Section 1 are out of scope; the mission carries the unconditional Section 5 analysis only, in generous integer form, and the correctness theorem (Theorem 4.1) as the goal.

9. Due diligence. Before creating the proposal, the creation script searches the platform for prior definitions and theorems matching the paper's ingredients; the search results are recorded in the repository's results directory for the reviewer.

10. Definition names and module stems. The two definition bundles are published under names equal to their module stems (AKS_poly, AKS_alg), so that the platform imports Definitions.Def_AKS_* in the theorem preambles resolve, in dependency order poly, then alg (which imports poly).

3. Formalization targets

The mission has ten items: two reference definitions and eight theorem drafts, in the following order.

Reference definitions (the formalization fragment):

• AKS_poly: the polynomial layer. Congruence (1) as the equality (X + a)^n = X^n + a in Z_n[X]; congruence (2) as divisibility by X^r - 1 in Z_n[X]; Definition 4.4's introspection relation over F_p[X]; and the set P of products of the generators X, X+1, ..., X+ell.
• AKS_alg: the algorithm layer. The integer logarithm logUp; the multiplicative order ordR; the lcm of the first numbers; the perfect-power predicate; the six-step decision function aksDecide with its search smallestR and loop bound ell; the set I and the residue group G; and the work measure aksWork.

Theorem drafts (milestones in attack order, then the goal):

1. AKS.poly_fermat: Lemma 2.1 - for n at least 2 and a coprime to n, n is prime if and only if (X + a)^n = X^n + a in Z_n[X] (Section 2).
2. AKS.lcm_lower: Lemma 3.1 - the lcm of the first m numbers is at least 2^m for m at least 7 (Section 3).
3. AKS.r_exists: Lemma 4.3 - for n > 1 there is an r with 1 < r at most max 3 (logUp n)^5 and ordR r n > logUp(n)^2 (Section 4).
4. AKS.introspective_closure: Lemmas 4.5-4.6 - introspective numbers are closed under products, and introspectivity is closed under products of polynomials (Section 4).
5. AKS.group_inj: Lemma 4.7 (Hendrik Lenstra Jr.) - two distinct polynomials of P, both of degree less than t, map to distinct elements of F = F_p[X]/(h), under the primitivity and introspectivity hypotheses, with t at most the size of the residue group G (Section 4).
6. AKS.group_upper: Lemma 4.8 (Kalai-Sahai-Sudan) - unless n is a power of p, there are m2 < m1 at most n^(floor(sqrt t)), colliding modulo r inside the bounded set I-hat, such that every image of P in F satisfies y^m1 = y^m2 (Section 4).
7. AKS.poly_time: the work bound - there is a constant C with aksWork n at most C logUp(n)^15 for every n, the generous integer form of Theorem 5.1 (Section 5).
8. AKS.prime_iff (the goal): Theorem 4.1 - aksDecide n = PRIME if and only if n is prime (Section 4).

Milestones 1 to 7 correspond to the theorem drafts 1 to 7; the goal is draft 8.

4. Significance

The paper is one of the landmark results of computational number theory: a problem open since the 1960s - an unconditional, deterministic, polynomial-time primality test - solved by elementary means, in a proof whose only ingredients are the binomial theorem, Euler's function, and the root bound of a polynomial over a field. The formal account forces exactly what the prose leaves to convention: the precise ring in which each congruence lives, the precise windows in which the searches find their witnesses, the precise generosity of each integer rounding, and the precise content of the two group bounds. The paper's difficulty lies not in any single deep theorem but in the assembly of many small lemmas under one bound chain; a formalization makes each link explicit and checkable, and the mission's readback discipline gives an independent restatement check of every statement before review.

5. Difficulty

Milestone 1 is a commutation: the forward direction is the freshman's dream in Z_p[X] plus Fermat's little theorem for the base; the backward direction isolates the coefficient of X^q for a prime q with q^k dividing n exactly and computes its q-adic valuation below k. Milestone 2 is Nair's argument: the product of the primes in (m/2, m] divides the lcm. Milestone 3 is the counting argument: every bad r divides a single product below the lcm of the window, so some r in the window escapes. Milestone 4 is two ring commutations: f^(m m') = f(X^(m m')) along f(X^m)^(m') = f(X^(m m')), and the product rule for introspectivity. Milestone 5 is Lenstra's argument: from a collision in F and introspection, f(Y) - g(Y) acquires the t distinct primitive r-th roots indexed by G, exceeding its degree. Milestone 6 is the pigeonhole of I-hat against G, the non-power distinctness, and the collision equation transported by introspection. Milestone 7 is arithmetic over the windows. The goal assembles: Lemma 4.2's direction is the congruences for primes; the step-4 case is the factor below the square root; and the step-6 case is the chain of Lemma 4.9 - the injectivity lower bound, the collision upper bound, and the integer bookkeeping that the generous encodings close with slack.

6. Scope

Included: the two congruences and the introspection relation; the set P and the set I with the residue group G; the six-step algorithm; and the eight statements - the Fermat characterization, the lcm bound, the small-r existence, the two closure lemmas, the two group bounds, the work bound, and the correctness theorem.

Excluded, as disclosed in items 7 and 8 of section 2: the machine-level bit-cost formalization of "is in P" (carried in prose, anchored by the explicit aksWork measure); the Section 5 refinements (Fouvry's Lemma 5.2, the O~(log^(15/2) n) of Theorem 5.3, the Lenstra-Pomerance variant of [LP1]); the conjectures of Section 5 and Conjecture 6.1; and the historical survey of Section 1.

7. References

• Manindra Agrawal, Neeraj Kayal, and Nitin Saxena, "PRIMES is in P", Annals of Mathematics 160 (2004) 781-793. The source document is the uploaded paper (annals-v160-n2-p12.pdf).
• M. Nair, "On Chebyshev-type inequalities for primes", American Mathematical Monthly 89 (1982) 126-129 (the reference for Lemma 3.1).
• Rudolf Lidl and Harald Niederreiter, Introduction to Finite Fields and their Applications, Cambridge University Press, 1986 (the reference [LN] for the factorization of the cyclotomic polynomial over F_p).
• Hendrik W. Lenstra Jr., "Primality testing with cyclotomic rings", unpublished, August 2002 (the source of Lemma 4.7).
• Adam Kalai, Amit Sahai, and Madhu Sudan, private communication, August 2002 (the source of the proof of Lemma 4.8).

Mission: The CODATA 2022 adjustment — least squares, covariance propagation, and the self-consistency of the recommended values

Motivation

Every value of a fundamental constant used in science — the fine-structure constant, the Newtonian constant of gravitation, the Rydberg constant — comes from one place: the least-squares adjustment periodically carried out by the CODATA Task Group on Fundamental Constants. The 2022 adjustment (P. J. Mohr, D. B. Newell, B. N. Taylor and E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022) takes 133 input data, determines 79 adjusted constants by weighted least squares with 54 degrees of freedom, applies expansion factors 1.7 and 2.5 to the uncertainties of certain groups of data to reduce all normalized residuals to two or less, obtains a final chi-square of 44.2 with Birge ratio 0.90, treats the sixteen values of the Newtonian constant of gravitation separately (16 data, one adjusted constant, 15 degrees of freedom, chi-square 12.9, expansion factor 3.9, Birge ratio 0.93), and obtains the recommended values from the adjusted constants by propagating their uncertainties and covariances.

The mission formalizes the mathematical skeleton of this process in Lean 4 and audits a representative slice of its output by exact rational arithmetic: the equivalence between minimizers of the chi-square statistic and solutions of the normal equations, the weighted mean as the rank-one case (the situation of the separate adjustment of G), the printed degrees of freedom and Birge ratios, the effect of uncertainty expansion on covariances and correlations, the algebraic laws of relative-uncertainty propagation, the exact derived constants determined by the exact defining values of h, e, k and N_A, and the mutual consistency of the printed uncertainties of the alpha family. The goal theorem packages these into the statement that the 2022 adjustment is self-consistent.

What is being formalized is the statistics and the arithmetic of the adjustment, not any physical measurement: the input data enter only through the abstract structure of a weighted least-squares problem, and the numerical audits compare exact rationals with the digit strings printed in the report's tables.

The fragment and its conventions

The source is the 2022 CODATA report in its two identical published versions: J. Phys. Chem. Ref. Data 54, 033105 (2025), doi 10.1063/5.0279860, and Rev. Mod. Phys. 97, 025002 (2025), doi 10.1103/RevModPhys.97.025002. The mission formalizes section XII, "Least-squares adjustment", and the exact and recommended values of Tables XXXII and XXXIII, under the following disclosed conventions.

Twelve conventions deserve disclosure. First, the platform publishes definitions as modules, so the three definition bundles — the least-squares model, the correlations and uncertainty propagation, and the exact rational values — are published as platform definitions (CODATA_lsa, then CODATA_uncert which imports it, and CODATA_values), attached to the proposal as reference items; the theorem drafts import them; and the creation script reads the definition code and the theorem statements directly from the repository modules that the CI has just compiled, so the code posted to the platform is byte-identical to the code whose compilation the CI verified. Second, the two uploaded PDFs are the same paper in its two published versions; citations reference both, and the table numbering follows the Rev. Mod. Phys. version (Tables XXXII-XXXIII, section XII). Third, the observational equations are taken in linear form; the report's observational equations are linear in the adjusted constants to begin with, but the values of the input data, the design matrix entries and the offset vector are interface data, not formalized: the theorems quantify over all weighted least-squares problems of the recorded dimensions. Fourth, the chi-square distribution and the printed probability values (83 percent for the main adjustment, 61 percent for G) are statistical statements about the chi-square distribution; they are printed data of the report and are not constructed, and no probability theory enters the mission. Fifth, the Newtonian constant of gravitation is treated separately, exactly as in the report: a second least-squares structure with sixteen input data and one adjusted constant, its own expansion factor 3.9, and its own Birge ratio; the goal theorem relates the two adjustments only through their common formalism. Sixth, the expansion factors 1.7 and 2.5 of the main adjustment are recorded in the description but not formalized, because the data they modify are interface data; the expansion factor 3.9 of the G adjustment is formalized through the covariance expansion law applied to the abstract covariance matrix of the sixteen values. Seventh, matrix inversion is expressed by two-sided inverse predicates, written entry by entry against the Kronecker delta, rather than through an inverse operator; this keeps the statements elementary and avoids any dependence on matrix inverse lemmas. Eighth, all arithmetic is rational or real: the exact constants are rationals, the derived quantities K_J, R_K, Phi_0, G_0, G_0⁻¹, F, R and the electronvolt are exact rationals, and the printed digit strings are captured by rational rounding intervals; exact quantities carrying a factor of pi (hbar, the Stefan-Boltzmann constant) and quantities with experimental uncertainty outside the audited family (the dalton, the Newtonian constant itself) are excluded because they are not rational. Ninth, the Birge ratios are captured by the rounding intervals [0.895, 0.905) and [0.925, 0.935), which the printed two-digit values 0.90 and 0.93 determine; the true values are sqrt(44.2/54) and sqrt(12.9/15). Tenth, the alpha family audit is an existential: the printed two-significant-digit uncertainties of alpha, 1/alpha, mu_0, eps_0 and Z_0 are jointly reproduced by a single rational relative-uncertainty witness of order 1.6 × 10⁻¹⁰, supplied explicitly by the prover (for example 156/10¹²); this witnesses consistency without asserting the (irrational, distribution-laden) exact relative uncertainty of alpha. Eleventh, the read-backs attached to the theorem drafts were authored by the same model that produced the statements (readback_model glm-5-latest-short); they are a self-check, not an independent audit, and human review of every item is required before submission. Twelfth, everything is developed against the platform's Mathlib build (0df444a); the compilation check of every item is the repository CI, which builds all definitions and theorem drafts with the same Mathlib version (no local Lean toolchain is available to the drafting agent, and this is disclosed).

Formalization targets

Eleven items: three published definition bundles attached as references, seven milestone theorem drafts, and the goal theorem.

• The least-squares model of the adjustment (reference): the LSQ structure with data, uncertainties, correlations, design matrix, offsets and the weight matrix as a two-sided inverse of the covariance matrix; residuals, the chi-square statistic, the normal equations, the minimization property, the normal matrix and its two-sided inverses, strict positive definiteness, the covariance matrix, the degrees of freedom N - M, and the Birge ratio sqrt(chi²/nu) (section XII).
• Correlations and uncertainty propagation (reference): the correlation coefficient of a covariance matrix, the expansion of a covariance matrix by per-entry factors, and the relative-variance functional of the propagation law (section XII).
• The exact rational values (reference): c, h, e, k and N_A exactly as fixed by the SI revision, the derived exact quantities 2e/h, h/e², h/2e, 2e²/h, h/2e², N_A e, N_A k, the electronvolt and h/e, and the 2022 rational values of alpha, 1/alpha, mu_0, eps_0 and Z_0 (Tables XXXII-XXXIII).
• The normal equations characterize the minimizers, and the solution is unique at full column rank — milestone.
• The single adjusted constant is the weighted mean with variance the inverse of the total weight, uniquely determined — milestone.
• The printed degrees of freedom and Birge ratios: 133 - 79 = 54, 16 - 1 = 15, and the rounding intervals of sqrt(44.2/54) and sqrt(12.9/15) — milestone.
• Expansion of uncertainties: a common factor squares the covariances and preserves every correlation; equal factors on the two members of a pair suffice — with the expansion factor 3.9 of the G adjustment as the instance — milestone.
• The laws of propagation of relative uncertainty: unit self-correlations, single-component variances, quadratic scaling, and addition of variances for uncorrelated inputs — milestone.
• The exact derived constants agree with the printed digit strings of Table XXXIII: K_J, R_K, Phi_0, G_0, G_0⁻¹, F, R, the electronvolt and h in eV Hz⁻¹ — milestone.
• A single rational relative-uncertainty witness reproduces the printed uncertainties of the whole alpha family — milestone.
• The 2022 adjustment is self-consistent: the goal, packaging the degrees of freedom, the two minimizations, the two Birge ratios, the correlation preservation under the expansion factor 3.9, the alpha-family witness, and the derived-value audit — the goal.

Significance

The CODATA adjustment is the mechanism by which the values of the fundamental constants become internationally accepted, self-consistent numbers; every precision measurement and every physical theory that quotes a constant inherits from it. The mission makes the three layers of the mechanism checkable by a proof assistant: the statistics (the least-squares theorem that the adjustment procedure is, by construction, the unique minimum of the chi-square statistic), the data hygiene (the effect of uncertainty expansion on covariances and correlations, and the propagation laws by which the recommended values and their uncertainties are derived), and the arithmetic (an exact rational audit confirming that the printed digit strings of the derived constants and the printed Birge statistics are consistent with the exact defining values and the reported chi-squares). Because the 2019 SI revision fixed h, e, k and N_A exactly, a growing family of derived constants is a pure rational computation; the mission verifies a representative slice of that family to the printed precision.

Difficulty

The milestones are honest and of mixed difficulty. The normal-equations milestone is the mathematical heart: the chi-square statistic is a quadratic form in the adjusted constants, strict positive definiteness of the weight matrix makes it convex, and the equivalence with the normal equations plus uniqueness at full column rank is a complete weighted least-squares existence-uniqueness argument, carried out entry by entry without matrix inverse lemmas. The weighted-mean milestone is a direct computation in the rank-one case, complicated only by the bookkeeping of the two-sided inverse predicate for the one-by-one normal matrix. The Birge milestone is real arithmetic: two subtractions and two square-root bounds, each reducible to exact rational comparisons by squaring. The expansion and propagation milestones are algebra over the reals: square roots of products of positive reals and the cancellation of equal factors; their difficulty is bookkeeping, not ideas. The derived-values and alpha-family milestones are exact rational computations with numerators and denominators up to thirty digits; they are fully decidable, and their difficulty is the size of the arithmetic — the prover must exhibit the witness ur and verify fifteen rational interval inclusions — for which norm_num-style automation is intended. The goal assembles the parts. Nothing in the mission requires mathematics beyond convexity of a quadratic form and exact rational arithmetic, and this is the point: the CODATA adjustment, the most authoritative computation in metrology, is at its core an auditable exact computation.

Formalization scope

Every theorem quantifies only over abstract least-squares structures and rational values; no measurement, no physical theory, and no probability distribution enters. The fragment excludes: the 133 input data as concrete vectors and the 79 adjusted constants as concrete quantities; the chi-square distribution and all probability statements; the least-squares fitting of the theoretical expressions (atomic transition frequencies, muonic Lamb shifts, magnetic-moment anomalies); the 2022-versus-2018 value comparisons and the historical narrative; the mises en pratique and the experimental methods; the electroweak and particle-physics input data; the quantities whose exact values involve pi (hbar, the Stefan-Boltzmann constant) or whose values carry experimental uncertainty outside the audited family; and the correlations among the input data as concrete numbers. What is formalized is the statistical skeleton, the covariance algebra, and the exact rational audit of the printed output.

Selected references

• P. J. Mohr, D. B. Newell, B. N. Taylor and E. Tiesinga, CODATA recommended values of the fundamental physical constants: 2022, J. Phys. Chem. Ref. Data 54, 033105 (2025), doi 10.1063/5.0279860; Rev. Mod. Phys. 97, 025002 (2025), doi 10.1103/RevModPhys.97.025002 — the mission's source (uploaded by the proposer in both versions): section XII and Tables XXXII-XXXIII.
• Resolution 1 of the 26th CGPM (2018) — the exact defining values of h, e, k and N_A on which the derived-value audit rests.
• B. N. Taylor and C. E. Kuyatt, Guidelines for evaluating and expressing the uncertainty of NIST measurement results (1994), and the Guide to the Expression of Uncertainty in Measurement (JCGM 100) — the law of propagation of uncertainty that the propagation milestones formalize.
• R. T. Birge (1932) and the subsequent least-squares tradition of the constants — the Birge ratio R_B = sqrt(chi²/nu) and the normalized-residual criterion that the expansion factors implement.

Motivation

Graph neural networks (GNNs) compute representations of nodes and whole graphs by repeatedly combining each node's state with information from its neighbours. Soon after they became a standard tool, the question arose of what they cannot do. A natural test case is graph isomorphism: given two graphs that are not isomorphic, can the network attach different representations to them? If it cannot, it is hopeless on any task that needs to tell the two graphs apart.

The yardstick for this question is the Weisfeiler–Lehman (WL) test (Weisfeiler and Leman, 1968), a colour-refinement procedure that is a necessary condition for isomorphism. Bronstein, Bruna, Cohen and Veličković's Geometric Deep Learning (arXiv:2104.13478v2) reports, in its historical chapter (Ch. 7, p. 120), the conclusion of Morris et al. (2019) and Xu et al. (2019): any GNN of the three flavours of §5.3 "cannot be more powerful than the WL test". This mission formalizes that claim, together with the surrounding remarks of the book that make it precise.

Timeline. 1968: Weisfeiler and Leman introduce the refinement. 2011: Shervashidze et al. use the WL iteration to build graph kernels. 2017: Gilmer et al. unify many architectures as message-passing neural networks. 2019: Morris et al. and Xu et al. independently prove that message-passing GNNs are bounded by 1-WL, and that injective aggregation attains the bound (the Graph Isomorphism Network). 2020: Corso et al. show that with continuous features injective aggregation needs several aggregators.

Setting

A graph $G$ has node set $V = \{0, \dots, n-1\}$ and a symmetric, loopless adjacency relation. The neighbourhood of a node is $\mathcal N_u = \{v : (u, v) \in E\}$ (eq. (11), p. 34); it does not contain $u$.

The WL colour refinement on a featureless graph starts with the same colour $c^0(u)$ for every node and sets

$$c^{s+1}(u) = \big(c^s(u), \{\!\{c^s(v) : v \in \mathcal N_u\}\!\}\big),$$

where $\{\!\{\cdot\}\!\}$ is a multiset. Colours carry their full history, so colours of nodes of two different graphs can be compared directly. The colour histogram at round $s$ is the multiset $\{\!\{c^s(u) : u \in V\}\!\}$. The WL test declares two graphs indistinguishable when their histograms agree at every round.

A message-passing layer (eq. (35), p. 79) has a message function $\psi$, a permutation-invariant aggregator $\bigoplus$ and an update $\phi$, and updates node features $h$ by

$$h_u \leftarrow \phi\Big(h_u, \bigoplus_{v \in \mathcal N_u} \psi(h_u, h_v)\Big).$$

A GNN starts from a constant feature $h^0_u = c$ and applies layers $t = 0, 1, \dots$, with parameters $(\psi_t, \bigoplus_t, \phi_t)$ shared by all graphs. Its graph-level output after $T$ rounds is a read-out of the multiset $\{\!\{h^T_u : u \in V\}\!\}$.

Formalization targets

Goal: GNNs are bounded by WL

For every GNN, read-out, depth $T$ and pair of graphs $G$, $G'$ (of possibly different sizes):

$$c^t_G(u) = c^t_{G'}(v) \implies h^t_G(u) = h^t_{G'}(v) \quad (t \le T),$$ $$\{\!\{c^T_G(u)\}\!\}_u = \{\!\{c^T_{G'}(v)\}\!\}_v \implies \mathrm{readout}\big(\{\!\{h^T_G(u)\}\!\}_u\big) = \mathrm{readout}\big(\{\!\{h^T_{G'}(v)\}\!\}_v\big).$$

The statement fixes no architecture and no feature space: it quantifies over all message, aggregation, update and read-out functions.

Milestones

1. Injective $\phi$ is one WL step (§4.1, p. 34): for the local layer $h_u \mapsto \phi(h_u, \{\!\{h_v : v \in \mathcal N_u\}\!\})$ with $\phi$ injective, if equal features are exactly equal round-$s$ colours, then equal new features are exactly equal round-$(s+1)$ colours.
2. Isomorphic graphs (side-note p. 119): a GNN attaches identical representations to isomorphic graphs.
3. $C_6$ versus $2K_3$ (side-note p. 120): the 6-cycle and two disjoint triangles have equal WL histograms at every round but are not isomorphic.
4. Max and mean (side-note p. 120): the multisets $\{\!\{a, b\}\!\}$ and $\{\!\{a, a, b, b\}\!\}$ differ but have the same maximum and the same mean.

Companion: reaching the bound

If every layer's update $(x, S) \mapsto \phi_t(x, \bigoplus_{y \in S} \psi_t(x, y))$ is injective, then equal features are exactly equal WL colours (Xu et al.).

Significance

The result. The bound says that a GNN's ability to separate graphs is capped by a cheap combinatorial procedure. Every pair of non-isomorphic graphs that WL fails to separate — all regular graphs of the same degree and size, such as $C_6$ and $2K_3$ — is also inseparable by every message-passing GNN, whatever its width, depth or training. This limitation motivated the higher-order and subgraph-based architectures discussed later in Ch. 7. The companion result explains why architectures with injective (sum-type) aggregation, such as GIN, are the maximally expressive members of the class, and the max/mean example explains why common aggregators fall short of it.

Formalizing it. The results are proved on paper; to the knowledge of this mission none has a machine-checked proof. The formalization makes explicit what the informal statements leave open: that the comparison needs parameters shared across graphs, that it concerns featureless graphs, which flavour of layer is covered, and in what sense "equivalent to one step" holds. It reuses a published 1-WL colour refinement (WLIdentification), so the GNN results connect to the platform's existing WL statements.

Difficulty

The statements are close to their definitions, and the difficulty is in the bookkeeping rather than in an idea. The comparison is between two different graphs, whose node sets are different types, so the relation between features and colours has to be carried across graphs rather than within one; equalities of colour multisets over neighbourhoods have to become equalities of multisets of messages, and histograms of colours have to become multisets of features. The $C_6$ / $2K_3$ example needs the colours of a regular graph at every round and a separate non-isomorphism argument. A tempting shortcut, defining the GNN's features to be the WL colours, proves nothing: the goal quantifies over all GNNs.

Formalization scope

Graphs are the published OAI.WLIdentification.Graph (order $n$, Boolean symmetric loopless adjacency on Fin n); the WL test is its neighborColor and neighborHistogram, featureless and with history-carrying colours. The book numbers no theorems, so every item is cited by section, equation and printed page.

Conventions committed to:

• Featureless graphs. The GNN's initial features are a constant, matching the featureless WL refinement (the WL analyses "almost always consider featureless or categorically-featured graphs", side-note p. 120). The featured version is not stated.
• The message-passing flavour. The goal is posed for layers (35). It covers the attentional flavour (34) and the convolutional flavour (33) when the coefficient $c_{uv}$ is a function of the features of $u$ and $v$. A coefficient that is an arbitrary function of the graph is outside the claim; with $c_{uv}$ the number of triangles through $u$, a convolutional layer separates $C_6$ from $2K_3$.
• Shared parameters. One GNN is evaluated on both graphs. A formalization in which each graph receives its own parameters would be trivially satisfiable and is ruled out.
• Aggregation on multisets. The aggregator is a function of the multiset of messages, so permutation invariance holds by construction; message, aggregate and feature types are arbitrary types.
• Neighbourhoods exclude the node itself; the node's own state enters through the first argument of $\phi$.
• The page's slips. The WL test is described (p. 120) as "randomly hashing their sums"; the refinement used hashes the multiset injectively. "With summation being a key representative" is not formalized: on real features summation is not injective on multisets, and Xu et al.'s result uses a chosen feature embedding.

Infrastructure needed is light: multiset bijections along equal maps (Multiset.map), induction over rounds, and finite computations on six-node graphs. The induction lemmas relating features to colours across two graphs are reusable for any further GNN-expressivity statement (higher-order WL, subgraph GNNs). Proofs of the milestones, of the companion, and alternative proofs of the goal through the companion are welcome.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021. https://arxiv.org/abs/2104.13478v2
• B. Weisfeiler, A. Leman, The reduction of a graph to canonical form and the algebra which appears therein, Nauchno-Technicheskaya Informatsia, 1968 (English translation). https://www.iti.zcu.cz/wl2018/pdf/wl_paper_translation.pdf
• K. Xu, W. Hu, J. Leskovec, S. Jegelka, How Powerful are Graph Neural Networks?, ICLR, 2019. https://arxiv.org/abs/1810.00826
• C. Morris, M. Ritzert, M. Fey, W. L. Hamilton, J. E. Lenssen, G. Rattan, M. Grohe, Weisfeiler and Leman Go Neural: Higher-order Graph Neural Networks, AAAI, 2019. https://arxiv.org/abs/1810.02244
• J. Gilmer, S. S. Schoenholz, P. F. Riley, O. Vinyals, G. E. Dahl, Neural Message Passing for Quantum Chemistry, ICML, 2017. https://arxiv.org/abs/1704.01212
• N. Shervashidze, P. Schweitzer, E. J. van Leeuwen, K. Mehlhorn, K. M. Borgwardt, Weisfeiler-Lehman Graph Kernels, JMLR 12, 2011. https://www.jmlr.org/papers/v12/shervashidze11a.html
• G. Corso, L. Cavalleri, D. Beaini, P. Liò, P. Veličković, Principal Neighbourhood Aggregation for Graph Nets, NeurIPS, 2020. https://arxiv.org/abs/2004.05718

Why sequence boundaries matter

A recurrent neural network (RNN) processes an ordered stream while retaining a summary of earlier inputs. The same update rule is applied at every time step, so it is natural to ask whether shifting the input stream simply shifts the resulting sequence of summaries. The answer depends on how the run begins. The first summary is supplied as an initial state, while the first input encountered after a shift can be different. Bronstein, Bruna, Cohen and Veličković use this boundary effect to explain a precise form of temporal translation equivariance for RNNs in §5.7 of Geometric Deep Learning (arXiv:2104.13478v2, pp. 90–93).

The claim matters when the same sequential model is applied to streams presented with different starting times. Without a specified boundary convention, the shared update rule alone does not guarantee that corresponding hidden states agree. The chapter's zero-padding construction makes that convention explicit. Its condition on the initial state can then be stated independently of a particular architecture or training procedure. The book numbers equations but no theorems or lemmas here; the mission's items are cited by section, equation, page, and, for a marginal statement, “side-note.”

RNN runs and padded sequences

Let $z(t)\in\mathbb R^k$ be the input at time $t$, let $h(t)\in\mathbb R^m$ be its hidden summary, and let $R:\mathbb R^k\times\mathbb R^m\to\mathbb R^m$ be a shared update map. Given a seed $h_0$, equation (38) defines a run by

$$h(0)=h_0,\qquad h(t+1)=R\bigl(z(t+1),h(t)\bigr).$$

The first processed input is $z(1)$; $z(0)$ is unused. This is the book's time convention, including the named state $h(0)$ (Bronstein et al., §5.7, p. 90, equation (38)). The update map is arbitrary: the results concern the recurrence itself, so they do not require the affine layer and activation used as one example in equation (39).

A left shift by $s$ steps replaces the input at time $t$ with the old input at time $t+s$. A left-padded input of length $d$ is

$$\bar z(t)= \begin{cases} 0,&t\le d,\\ z(t-d),&t>d. \end{cases}$$

Here $0$ is the zero vector in $\mathbb R^k$. The original input begins at time $d+1$. The two runs being compared use the same update map and the same seed. This is the exact padding convention displayed on p. 93 of the book (Bronstein et al., §5.7, p. 93).

Formalization targets

The capstone is the chapter's one-step equivariance claim. For every update map, input sequence, and seed fixed by the zero-input update, one or more zero-padding steps suffice:

$$d\ge1,\qquad R(0,h_0)=h_0 \quad\Longrightarrow\quad h_{\bar z(\cdot+1)}(t)=h_{\bar z}(t+1) \quad\text{for every }t\ge0.$$

The multi-step side note extends the conclusion to every $s$ with $0\le s\le d$:

$$h_{\bar z(\cdot+s)}(t)=h_{\bar z}(t+s) \quad\text{for every }t\ge0.$$

The milestone list also records the book's unpadded boundary counterexample and its observation that a contraction $\gamma(h)=R(0,h)$ has a unique attracting fixed point. The latter is represented by an already proved, reusable Banach fixed-point theorem rather than a second draft of the same result (Bronstein et al., §5.7, pp. 92–93, equations (40)–(42) and side-note).

What the result supplies

The equivariance theorem identifies a checkable condition under which the hidden-state sequence tracks a left-shifted input exactly, including at the first state. It also marks the limit of the informal idea that sharing the same update map across time automatically creates shift equivariance: the unpadded run can fail already at time $1$. The fixed-point condition is therefore part of the mathematical claim, rather than an implementation preference (Bronstein et al., §5.7, pp. 92–93).

The RNN shift statements are targets for machine-checked proofs. The contraction milestone already has a machine-checked proof in the referenced CursoEDO.contraction_fixed_point theorem. A completed development would make the boundary convention and the arbitrary-update-map quantifiers available for later statements about sequential models. The recurrence and padding definitions are reusable whenever a discrete-time state update is compared before and after a shift.

The boundary difficulty

The tempting comparison takes two runs that begin with the same seed, then tries to pair the shifted run's state at $t$ with the original run's state at $t+1$. At the first step, those states have encountered different input histories. Equations (40)–(41) display the mismatch: the original run has applied $R$ to its first input, while the shifted run still uses the supplied seed at the corresponding update. For an arbitrary $R$ and arbitrary first input, the states need not agree (Bronstein et al., §5.7, p. 92). A shift statement that omits its padding length or seed condition would therefore assert something the chapter explicitly rejects.

Formalization scope

Lean represents $\mathbb R^k$ and $\mathbb R^m$ as functions on Fin k and Fin m; time and padding lengths are natural numbers. The run uses $h(0)=h_0$ and consumes $z(t+1)$ at its next update. The padding function returns the zero vector through index $d$ and then the correspondingly indexed original input. These definitions cover every finite dimension, including zero-dimensional edge cases, while the unpadded counterexample uses one input and one hidden coordinate.

The target ranges over all update maps $R$ and all input sequences; it does not impose a special neural-network parameterization. The seed is any fixed point of $h\mapsto R(0,h)$, not necessarily the zero state, and the zero-input update need not be the identity map. The formal statements include time $t=0$ and the endpoint $s=d$. No contraction assumption is needed for shift equivariance itself; contraction enters only the separate existence-and-convergence milestone. The contraction theorem is stated for a nonempty complete metric space, which includes the finite-dimensional real hidden-state spaces used here.

The work requires a small discrete recurrence interface, an exact padding definition, and proofs for the boundary counterexample and shift identities. Those two definitions and the shift results can also support variants with a nonzero padding vector. The LSTM equations of §5.8 have a separate gated state model and are outside this mission's formalization scope. Contributions that keep the full fixed-point hypothesis and the stated boundary cases are welcome.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen and P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021, arXiv:2104.13478v2, §5.7, pp. 90–93.

Why convolution, and why the shift

Convolutional neural networks process images, audio and time series with layers whose weights are shared across positions. The Geometric Deep Learning programme of Bronstein, Bruna, Cohen and Veličković (arXiv:2104.13478v2) explains this architecture by symmetry: on a grid the relevant symmetry is translation, and a linear layer that respects translations is forced to be a convolution. Section 4.2 of the book makes this precise in the simplest setting, a one-dimensional periodic grid, and then derives the discrete Fourier transform from the same symmetry, as the common eigenbasis of all convolution operators. The material is classical in signal processing (see the tutorial of Bamieh, arXiv:1805.05533), and the book uses it as the template that the later chapters generalise to groups, graphs and manifolds; for example, graph signal processing (Sandryhaila and Moura, arXiv:1210.4752) replaces the shift by an adjacency matrix.

This mission formalises the characterisation the book calls the basis of "the overall philosophy of Geometric ML": a matrix is circulant if and only if it commutes with the shift (§4.2, p. 37). It is the third mission of a series on the book. The book numbers no theorems, lemmas or definitions; every item is cited by section, equation or position, and printed page.

Setting

Fix $n \ge 1$ and the ring graph with nodes $\mathbb Z_n = \{0, 1, \dots, n-1\}$, arithmetic taken modulo $n$. A signal is a vector $x = (x_0, \dots, x_{n-1})$ with entries in a commutative ring $R$, for instance $\mathbb R$.

• The circulant matrix of a vector $\theta = (\theta_0, \dots, \theta_{n-1})$ is $C(\theta) = (\theta_{u - v \bmod n})_{u, v}$: each row is the previous one shifted circularly by one position.
• The circular convolution of a signal $x$ with a filter $\theta$ is $(x \star \theta)_u = \sum_{v=0}^{n-1} x_v\, \theta_{u - v \bmod n}$.
• The right shift $S$ is the circulant matrix of $\theta = (0, 1, 0, \dots, 0)^\top$. It moves a vector one position to the right, $(Sx)_u = x_{u-1}$.
• Over $\mathbb C$, the discrete Fourier basis is $\varphi_k(u) = n^{-1/2} e^{2\pi i k u / n}$ for $k = 0, \dots, n-1$. The Fourier matrix $\Phi = (\varphi_0, \dots, \varphi_{n-1})$ has the $\varphi_k$ as columns, and $\Phi^*$ is its conjugate transpose.

In Lean the index set is ZMod n with [NeZero n], $C(\theta)$ is Mathlib's Matrix.circulant θ, and the mission's definitions GeomDL.Grids.conv, GeomDL.Grids.shift, GeomDL.Grids.fourierVec and GeomDL.Grids.fourierMatrix are the four objects above.

Formalization targets

Goal: commuting with the shift characterises circulant matrices

For every $n \times n$ matrix $M$ over a commutative ring $R$,

$$M S = S M \iff M = C(\theta) \text{ for some } \theta \in R^n .$$

The book states the converse direction tentatively ("the opposite direction appears to be true as well"); it is a theorem, and it is stated here without the hedge.

Milestones, in attack order

1. Circulant matrices are convolutions, $C(\theta)x = x \star \theta$, and $S = C(0, 1, 0, \dots, 0)$ shifts right, $(Sx)_u = x_{u-1}$ (p. 37).
2. The left shift is $S^\top$, and $S^\top S = S S^\top = I$ (side-note, p. 37).
3. Shift equivariance of convolution, $S\,C(\theta)\,x = C(\theta)\,S\,x$ (p. 37).
4. The Fourier basis vectors are eigenvectors of $S$: $S\varphi_k = e^{-2\pi i k/n}\varphi_k$, with eigenvalues that are $n$-th roots of unity (p. 38 and side-note).
5. These eigenvalues are pairwise distinct (side-note, p. 37).
6. $\Phi^*\Phi = I$ (side-note, p. 38).

Companion: the Convolution Theorem

With $(\mathcal F\theta)_k = \sum_w \theta_w e^{-2\pi i k w/n}$,

$$C(\theta)\varphi_k = (\mathcal F\theta)_k\,\varphi_k, \qquad C(\theta) = \Phi\,\operatorname{diag}(\mathcal F\theta)\,\Phi^* .$$

The book prints this with $\hat\theta = \Phi^*\theta = n^{-1/2}\mathcal F\theta$ in place of $\mathcal F\theta$, which is off by a factor $\sqrt n$ for $n \ge 2$; the corrected identity is stated. The transform form of the Convolution Theorem, $\mathcal F(u \star v) = \mathcal F u \cdot \mathcal F v$ with Mathlib's ZMod.dft, is already Proved on the platform as IntMul.HvdH.dft_cyclic_conv and is included as a reference item.

Significance

The goal identifies the space of linear translation-equivariant maps on $R^{\mathbb Z_n}$ with the convolutions, an $n$-dimensional space parametrised by the filter $\theta$. This is the statement that lets the book define convolution as a translation-equivariant linear operation, and it is the grid case of the general principle the book develops in §4.3 and §5: a linear map that commutes with a group action is a group convolution. Milestones 4–6 and the companion are the other half of §4.2: the shift has distinct eigenvalues, so every matrix commuting with it is diagonal in the shift's eigenbasis, and that eigenbasis is the Fourier basis; hence the Fourier transform diagonalises every convolution.

Mathlib contains circulant matrices, their commutativity (Matrix.circulant_mul_comm) and the discrete Fourier transform on ZMod n, but neither the converse characterisation nor the diagonalisation of circulant matrices by the normalised Fourier matrix. The mission adds these, in a form that later missions of the series (group convolutions, graph Fourier transforms) can be compared against.

Difficulty

The direction "$\Leftarrow$" is a one-line consequence of the commutativity of circulant matrices. The content is "$\Rightarrow$": the equation $MS = SM$ is an equation between matrices, and it has to be turned into the statement that the entries of $M$ are constant along every cyclic diagonal, with the indices handled modulo $n$. The spectral argument of the book (commuting matrices with a common eigenbasis) only applies over a field containing the $n$-th roots of unity in which $n$ is invertible; over a general commutative ring, such as $\mathbb Z$ or $\mathbb Z/2$, the goal has to be proved without it. For the Fourier statements the work is in the geometric sums of roots of unity and in the bookkeeping between the representatives $\{0, \dots, n-1\}$ used in the exponents and the arithmetic of $\mathbb Z_n$.

Formalization scope

• Indices live in ZMod n with [NeZero n], so $n \ge 1$ and matrices are finite; no lower bound $n \ge 2$ is needed (for $n = 1$, $S = I$ and every matrix is circulant, so the goal holds). Exponents use the representatives ZMod.val $\in \{0, \dots, n-1\}$, as on the page.
• The goal and milestones 1–3 are stated over an arbitrary commutative ring $R$; milestones 4–6 and the companion are over $\mathbb C$.
• "Circulant" means equal to Matrix.circulant θ for some θ. Defining a matrix to be circulant when it commutes with $S$ would make the goal true by definition; the mission does not do that. A sanity file checks that the shift moves vectors to the right on $\mathbb Z_3$ and that $\operatorname{diag}(1, 0)$ on $\mathbb Z_2$ does not commute with $S$.
• The side-note on p. 38 calls $\Phi$ "orthogonal"; the property it writes, $\Phi^*\Phi = I$ with the conjugate transpose, is unitarity, and that is what is stated.
• The Fourier normalisation is the book's $n^{-1/2}$ in $\varphi_k$; the eigenvalues in the companion use Mathlib's unnormalised ZMod.dft, and the factor $\sqrt n$ is written out in its statement.

No new infrastructure beyond Mathlib is required. Proofs of any item, and proofs of the goal that avoid the spectral argument, are welcome; the shift and Fourier lemmas are reusable for the graph Fourier transform later in the book.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021 (v2). §4.2, pp. 35–38. https://arxiv.org/abs/2104.13478
• B. Bamieh, Discovering Transforms: A Tutorial on Circulant Matrices, Circular Convolution, and the Discrete Fourier Transform, arXiv preprint, 2018. https://arxiv.org/abs/1805.05533
• A. Sandryhaila, J. M. F. Moura, Discrete Signal Processing on Graphs, IEEE Transactions on Signal Processing, 2013. https://arxiv.org/abs/1210.4752
• D. Harvey, J. van der Hoeven, Integer multiplication in time O(n log n), Annals of Mathematics, 2021 (source of the platform's proved IntMul.HvdH.dft_cyclic_conv). https://hal.science/hal-02070778

Motivation

The extension problem for groups asks for a description of all groups $E$ that contain a given group $H$ as a normal subgroup with quotient isomorphic to a given group $G$. Schreier (1926) answered it by showing that every such extension can be rebuilt from $H$, $G$ and two maps: a map $\alpha : G \to \mathrm{Aut}(H)$ and a map $f : G \times G \to H$, subject to two compatibility conditions. The group built from this data is the crossed product $H \#_\alpha^f G$. When $H$ is abelian, this becomes the cohomological classification of extensions by $H^2(G, H)$; for nonabelian $H$ it is the theory of Eilenberg and MacLane (1947).

The classical classification counts extensions up to isomorphisms that are the identity on $H$ and induce the identity on $G$. Agore and Militaru (arXiv:0805.4077v2, 2008) also study a coarser notion, in which the isomorphism may act on $H$ and on $G$ by arbitrary automorphisms. The resulting classification, their Theorem 3.8, is the target of this mission. It is closer to the question "which groups arise as crossed products of $H$ and $G$, up to isomorphisms respecting the extension structure", which is what is needed when listing groups of a given shape. The paper's applications include the description of all morphisms between two crossed products by explicit data.

Setting

Let $H$ and $G$ be groups. For a map $\alpha : G \to \mathrm{Aut}(H)$ write $g \triangleright h = \alpha(g)(h)$. A crossed system is a pair $(\alpha, f)$ with $f : G \times G \to H$ such that, for all $g_1, g_2, g_3 \in G$ and $h \in H$,

$$g_1 \triangleright (g_2 \triangleright h) = f(g_1, g_2)\,\big((g_1g_2) \triangleright h\big)\,f(g_1, g_2)^{-1}, \qquad f(g_1, g_2)\, f(g_1g_2, g_3) = \big(g_1 \triangleright f(g_2, g_3)\big)\, f(g_1, g_2g_3).$$

Then $\alpha$ is called a weak action: it is a homomorphism only up to the inner automorphisms given by $f$. The system is normalized if $f(1,1) = 1$, and $\mathrm{Crossed}(H, G)$ is the set of normalized crossed systems. The crossed product $H \#_\alpha^f G$ is the set $H \times G$ with

$$(h_1, g_1)\cdot(h_2, g_2) = \big(h_1\,(g_1 \triangleright h_2)\,f(g_1, g_2),\; g_1g_2\big),$$

which is a group exactly when $(\alpha, f)$ is a crossed system.

The category $\mathcal{E}_2(H, G)$ has $\mathrm{Crossed}(H, G)$ as its objects. A morphism $(\alpha, f) \to (\alpha', f')$ is a triple $(\eta, \psi, \gamma)$ of group morphisms $\eta : H \to H$, $\gamma : G \to G$ and $\psi : H \#_\alpha^f G \to H \#_{\alpha'}^{f'} G$ such that $\psi(h, 1) = (\eta(h), 1)$ and the $G$-component of $\psi(h, g)$ is $\gamma(g)$.

Two normalized crossed systems are 2-equivalent, $(\alpha, f) \approx_2 (\alpha', f')$, if there are group automorphisms $\eta$ of $H$ and $\gamma$ of $G$ and a map $t : G \to H$ with

$$g \triangleright' h = \eta\Big(t(g)\big(\gamma^{-1}(g) \triangleright \eta^{-1}(h)\big)t(g)^{-1}\Big), \qquad f'(g_1, g_2) = \eta\Big(t(g_1)\big(\gamma^{-1}(g_1) \triangleright t(g_2)\big) f\big(\gamma^{-1}(g_1), \gamma^{-1}(g_2)\big) t(g_1g_2)^{-1}\Big).$$

Formalization targets

Goal: Theorem 3.8

$$\approx_2 \text{ is an equivalence relation on } \mathrm{Crossed}(H, G), \qquad \mathrm{Ob}\,\mathrm{Sk}\,\mathcal{E}_2(H, G) \;\cong\; \mathrm{Crossed}(H, G)/\!\approx_2,$$

with the bijection sending the isomorphism class of $(\alpha, f)$ to its $\approx_2$-class. The statement holds for all groups $H$, $G$, finite or not, abelian or not.

Milestones, in the order of the paper

• Lemma 1.2: the values $f(g, 1)$, $f(1, g)$ and $1 \triangleright h$ in a crossed system.
• Theorem 1.3: (8) is associative if and only if $(\alpha, f)$ is a crossed system, and then $H \#_\alpha^f G$ is a group with unit $(f(1,1)^{-1}, 1)$.
• Theorem 2.1: the crossed product is an initial object of one category and a final object of another.
• Corollary 2.2 (1)–(2): group morphisms out of and into a crossed product.
• Corollary 2.3: group morphisms $H \#_\alpha^f G \to H \#_{\alpha'}^{f'} G$ correspond to quadruples $(u, r, v, s)$ of maps.
• Proposition 3.4: morphisms of $\mathcal{E}_2(H, G)$ with given $\eta$, $\gamma$ correspond to maps $r : G \to H$ satisfying two conditions.
• Corollary 3.5: a morphism of $\mathcal{E}_2(H, G)$ is an isomorphism iff $\eta$, $\gamma$ are isomorphisms and the 2-equivalence conditions hold for a unique $t$ compatible with $\psi$.
• §3, p. 21: $\approx_2$ coincides with isomorphism in $\mathcal{E}_2(H, G)$ and is an equivalence relation.

Significance

The theorem replaces the categorical question "when are two crossed products isomorphic in $\mathcal{E}_2(H, G)$" by an explicit system of equations in the data $(\alpha, f)$. For finite $H$ and $G$ the quotient $\mathrm{Crossed}(H, G)/\!\approx_2$ is a finite, computable set, so the theorem turns the description of crossed products of $H$ by $G$ up to this isomorphism into a finite computation. The intermediate results are of independent use: Corollary 2.3 describes every group morphism between two crossed products, and Theorem 2.1 gives the two universal properties of the crossed product.

The results are proved in the paper. None of them has a machine-checked proof: Mathlib has GroupExtension and its equivalences, which correspond to the finer category $\mathcal{E}_1(H, G)$ of the paper, and SemidirectProduct, the special case $f = 1$ with $\alpha$ an action, but no crossed product with a cocycle, no weak actions, and no $\mathcal{E}_2$-type classification. Formalizing the mission produces a reusable nonabelian crossed-product layer and an explicit classification of extensions up to automorphisms of both ends.

Difficulty

Each step is elementary group theory, but the computations are long and noncommutative. The central difficulty is Corollary 2.3: every group morphism between two crossed products must be reconstructed from its values on the generators $(h, 1)$ and $(1, g)$, and the five compatibility conditions must be shown to be equivalent to multiplicativity, keeping track of the weak action and both cocycles in a nonabelian group. The tempting shortcut of treating $\alpha$ as an action fails: (2) only makes $\alpha$ multiplicative up to conjugation by $f$, and this twist appears in every identity. In Corollary 3.5 the inverse of $\psi$ must itself be shown to be a morphism of $\mathcal{E}_2$ and the map $t$ extracted from it.

Formalization scope

Everything is in the namespace CrossedProductGroups.Classification, for arbitrary {H G : Type*} [Group H] [Group G].

• The weak action is a plain map α : G → MulAut H, not a homomorphism; the cocycle is curried, f : G → G → H.
• IsCrossedSystem α f records (2) and (3) with the factors in the printed order; Crossed H G is the subtype of pairs with f 1 1 = 1.
• The crossed-product multiplication is the function crossedMul α f on H × G. No group instance is put on it; a morphism of groups between crossed products is a map preserving crossedMul.
• E2 H G is a type synonym for Crossed H G with a Mathlib Category instance. Its morphisms (E2Hom) record η : H →* H, γ : G →* G and a multiplicative ψ with ψ (h, 1) = (η h, 1) and (ψ x).2 = γ x.2. The paper's inclusion $i_H(h) = (h f(1,1)^{-1}, 1)$ equals $(h, 1)$ on normalized systems, the only objects.
• Equiv2 is Definition 3.7, with $\gamma^{-1}, \eta^{-1}$ as γ.symm, η.symm.
• The goal uses Mathlib's CategoryTheory.Skeleton and Quot Equiv2, includes Equivalence Equiv2, and requires the bijection to send toSkeleton c to the class of c.
• Theorem 2.1's categories are not built: initial and final are unfolded into existence and uniqueness of morphisms. In Corollary 3.5, the uniqueness of $t$ is stated together with the formula for $\psi$, since (38) and (39) alone do not determine $t$. The bijection of Corollary 2.3 is pinned to the paper's formula for $\psi$.

A bare equality of cardinalities between the skeleton and the quotient, an isomorphism notion in $\mathcal{E}_2$ defined as $\approx_2$, or morphisms $\psi$ that need not be multiplicative would each make the goal weaker than the paper's statement; the definitions above rule these out.

Contributions welcome: proofs of the milestones in any order, a reusable API for crossedMul (the group structure of Theorem 1.3 on a type synonym), and a bridge to Mathlib's GroupExtension.

Selected references

• A. L. Agore, G. Militaru, Crossed product of groups. Applications, arXiv preprint, 2008. https://arxiv.org/abs/0805.4077v2
• O. Schreier, Über die Erweiterung von Gruppen I, Monatshefte für Mathematik und Physik 34 (1926), 165–180.
• S. Eilenberg, S. MacLane, Cohomology theory in abstract groups. II. Group extensions with a non-Abelian kernel, Annals of Mathematics 48 (1947), 326–341.
• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer, 1982 (Chapter IV).

Motivation

A quantum algorithm is run as a quantum circuit: a sequence of elementary gates drawn from a fixed instruction set, such as the Hadamard, phase, controlled-NOT and $T$ gates. On fault-tolerant hardware every layer of gates costs time and error-correction overhead, so the depth of a circuit, its number of layers, is a primary cost measure. Compilers therefore want, for a given target unitary, a circuit of the least possible depth, not merely some circuit.

Amy, Maslov, Mosca and Roetteler (arXiv:1206.0758, IEEE TCAD 2013) gave an exact, depth-optimal synthesis algorithm, MITM-factor, based on a meet-in-the-middle search. With it they found the first $T$-depth-3 circuit for the Toffoli gate and improved circuits for several standard gates. Approximate synthesis methods such as the Solovay–Kitaev algorithm (Dawson–Nielsen) produce short circuits but not optimal ones. The paper is a standard reference for exact, optimal synthesis over Clifford+$T$, and later depth- and $T$-count-optimal search methods start from it.

Setting

Fix $n$ qubits. $U(2^n)$ is the group of $2^n \times 2^n$ complex matrices $U$ with $UU^\dagger = U^\dagger U = I$, where $U^\dagger$ is the conjugate transpose. An instruction set $\mathcal G$ is a set of gates closed under inversion. A gate acts on some of the qubits and as the identity on the rest.

A depth-one circuit applies gates of $\mathcal G$ to pairwise disjoint sets of qubits at once. $\mathcal V_{n,\mathcal G}$ is the set of unitaries of depth-one circuits. A circuit of depth $m$ is a sequence of layers $U_1, \dots, U_m \in \mathcal V_{n,\mathcal G}$, and it implements $U_1U_2\cdots U_m$. Let

$$S_0 = \{I\}, \qquad S_i = \mathcal V_{n,\mathcal G}\, S_{i-1},$$

so $S_i$ is the set of unitaries implementable in depth $i$, and write $S_i^\dagger U = \{X^\dagger U : X \in S_i\}$.

MITM-factor$(\mathcal G, U, l)$ runs $i = 1, \dots, \lceil l/2\rceil$. At step $i$ it builds $S_i$ and tests whether $S_{i-1}^\dagger U \cap S_i \ne \emptyset$; if so it returns the concatenation of the two witnessing circuits. Otherwise it tests $S_i^\dagger U \cap S_i \ne \emptyset$ in the same way. If no step succeeds, it returns nothing.

In the Lean development the layer set is a finite set V of unitaries standing for $\mathcal V_{n,\mathcal G}$, S V i is $S_i$, circuits V i is the set of circuits of $i$ layers (lists over V), and mitmFactor V U l is the algorithm.

Formalization targets

Goal: the main result (§2, p. 4)

For every finite $V$, unitary $U$ and $l \ge 0$, with $h = \lceil l/2\rceil$:

$$\text{MITM-factor}(U,l) = \text{none} \iff U \notin S_1 \cup \cdots \cup S_{2h},$$

and a returned circuit $c$ lies over $V$, implements $U$, has $1 \le |c| \le 2h$, and $|c| \le |c'|$ for every circuit $c'$ over $V$ of positive depth implementing $U$. For even $l$ the decided range is exactly $1 \le d \le l$. If $|V| \ge 2$, the counted cost satisfies

$$\mathrm{cost}(U,l) \le 8\,|V|^{h}\log_2 |V|^{h}.$$

The goal fixes no instruction set and no gate. It is the paper's correctness and running-time claim for the search itself.

Milestones

In attack order:

1. $\mathcal V_{n,\mathcal G}$ is closed under adjoint (proof of Lemma 1).
2. $S_i^\dagger = S_i$ when the layer set is closed under adjoint.
3. The sets the algorithm generates are exactly the depth-$i$ circuits and their unitaries.
4. Lemma 1: $U$ has a depth-$l$ circuit iff $S_{\lfloor l/2\rfloor}^\dagger U \cap S_{\lceil l/2\rceil} \ne \emptyset$.
5. Iteration $i$ tests depth $2i-1$, then depth $2i$.
6. The algorithm stops at the least positive depth.
7. $|S_i| \le |V|^i$.
8. The two sum bounds of the running-time analysis.

Significance

The result. Searching all circuits of depth at most $l$ takes $|\mathcal V_{n,\mathcal G}|^l$ steps. MITM-factor needs only about $|\mathcal V_{n,\mathcal G}|^{\lceil l/2\rceil}$, up to a logarithmic factor: a square-root saving that made exhaustive depth-optimal synthesis of three- and four-qubit gates feasible. Its correctness is what lets a computer search certify optimality: when the search fails up to depth $l$, no shorter circuit exists. The paper's non-existence statements, such as the absence of shallower circuits for particular gates, rest on this.

Formalizing it. The result is proved in the paper, informally and briefly. No machine-checked version is known to exist. The mission produces a checked statement of what the search decides, which repairs two boundary cases of the printed claim (see Formalization scope), and a cost bound with an explicit constant in place of the $O$. Lemma 1 and the generation step are reusable for any meet-in-the-middle search over a monoid generated by a finite set.

Difficulty

The mathematics is elementary; the difficulty is in stating exactly what the algorithm does. The obvious reading, "the algorithm decides depth at most $l$", is false for odd $l$: the last step also tests depth $l + 1$ and may return a circuit of that depth. "Returns a circuit of minimal depth" is false for $U = I$, whose minimal depth $0$ is never tested. A proof therefore has to track the loop's first success through two interleaved tests per step, and connect sets of unitaries to circuits as lists of layers. For the cost bound, the step from per-iteration costs to the total needs the geometric-sum bound in a form the paper misprints: $\sum_{i \le h} m^i \le m^h(1 + 1/(m^h - 1))$ fails at $m = 2$, $h = 2$.

Formalization scope

• Unitaries are elements of Matrix.unitaryGroup (Fin n → Bool) ℂ; $U^\dagger$ is the group inverse.

• The layer set V is an arbitrary Finset of unitaries. The paper's argument uses nothing about $\mathcal V_{n,\mathcal G}$ beyond finiteness, and milestone 1 relates $\mathcal V_{n,\mathcal G}$, defined over the shared QAlgorithms gate and circuit layer, to this setting. Hypotheses on V appear only where used: closure under inverse for milestone 2, $|V| \ge 2$ for the cost clause.

• Circuits are Lists of layers, implementing their List.prod, head leftmost, as "$U_1U_2\cdots U_m$" on p. 4. The algorithm returns a circuit, not a unitary. The "any circuit" of the pseudocode is a choice of witnesses.

• Corrections, each disclosed in the items:

  • the decided range is $1 \le d \le 2\lceil l/2\rceil$;
  • minimality is among circuits of positive depth;
  • the second sum bound uses $1/(|V| - 1)$.

• Cost model. The running time is a counted cost, built from the sets $S_i$ the run actually generates:

  • $|V|\,|S_{i-1}|$ to generate $S_i$;
  • $|S_i|\log_2|S_i|$ to sort it;
  • $(|S_{i-1}| + |S_i|)\log_2|S_i|$ for the lookups.

  These are summed over the iterations executed, up to the first success. Logarithms are Real.logb 2. The constant $8$ is the mission's explicit form of the paper's $O$.

• Trivializing readings are ruled out: the cost is not defined from $|V|^i$, which would make the bound an identity about powers, and the goal is not an existence claim about some algorithm with that cost. A circuit-valued output compared against every circuit over $V$ prevents a content-free minimality clause.

• Not covered: Theorem 1 and Theorem 2 with Lemma 2 (controlled-$U$ costs and $T$-depth with ancillas), the $T$-depth variant of §3.1, the pruning of §4, and the computational results of §§5–6.

• Welcome contributions: proofs of the milestones, lemmas on circuits and S (for instance $S_{i+j} = S_iS_j$), and a list-based model of the sort-and-search cost.

Selected references

• M. Amy, D. Maslov, M. Mosca, M. Roetteler, A meet-in-the-middle algorithm for fast synthesis of depth-optimal quantum circuits, IEEE Trans. Computer-Aided Design 32(6), 2013; arXiv:1206.0758v3. https://arxiv.org/abs/1206.0758
• C. M. Dawson, M. A. Nielsen, The Solovay–Kitaev algorithm, Quantum Inf. Comput. 6(1), 2006; arXiv:quant-ph/0505030. https://arxiv.org/abs/quant-ph/0505030

Motivation

In this paper, we show the equivalence of the set of unitaries computable by the circuits over the Clifford and T library and the set of unitaries over the ring $\mathbb{Z}[\frac{1}{\sqrt{2}},i]$, in the single-qubit case. We report an efficient synthesis algorithm, with an exact optimality guarantee on the number of Hadamard and T gates used. We conjecture that the equivalence of the sets of unitaries implementable by circuits over the Clifford and T library and unitaries over the ring $\mathbb{Z}[\frac{1}{\sqrt{2}},i]$ holds in the $n$-qubit case.

This mission is the statement-level formalization of Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates (arXiv:1206.5236v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Exact single-qubit H/T synthesis characterization (Theorem 1 (abstract seed): exact single-qubit synthesis characterization, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

7 results of the paper are not stated yet, because the library lacks an interface they need:

• Conjecture 1: n-qubit extension with one clean ancilla: Conjecture 1: n-qubit extension with one clean ancilla (source-ambiguity)
• §2 unnumbered examples: rotations requiring approximation: §2 unnumbered examples: rotations requiring approximation (source-ambiguity)
• Corollary 1: synthesis size, arithmetic cost and bit cost: Canonical input encoding, resource-counted Algorithm-1 execution, and uniform length/arithmetic/bit bounds in the true minimum exact H/T length. (hard)
• §5 unnumbered: finite exhaustive verification claim: §5 unnumbered: finite exhaustive verification claim (source-ambiguity)
• Proposition 2: base extraction property: Proposition 2: base extraction property (source-ambiguity)
• Theorem 2: simultaneous H/T optimality and exact count formulas: Returned-word G synthesis/HT-normalization interface with simultaneous H/T optimality and the two exact count formulas. (hard)
• Conclusion unnumbered: combined Pauli-X/Y output bound: Conclusion unnumbered: combined Pauli-X/Y output bound (source-ambiguity)

Selected references

• Fast and efficient exact synthesis of single qubit unitaries generated by Clifford and T gates, arXiv:1206.5236v4, https://arxiv.org/abs/1206.5236v4

Comparing single-coordinate and block changes

A Boolean function can react differently to changing one input coordinate and changing several coordinates together. Measuring this difference is a question about the local complexity of total Boolean functions. The Block Sensitivity vs. Sensitivity campaign records exponents that quantify how large this difference can become along families of functions with increasing sensitivity.

This mission records the exact exponent

$$\alpha=\frac{\log(14055^8)}{\log(3738277295413674)} =2.130825579397823947629976285043\ldots.$$

Its construction is already accepted and public. The mission expresses that result using the campaign's shared definition, so that its value can enter the same record as earlier entries. The logarithmic expression is the target; the displayed decimal is an approximation. No optimality claim is part of this mission.

Boolean functions and sensitive blocks

A total Boolean function on $n$ coordinates is a map $f:\{0,1\}^n\to\{0,1\}$, defined on every binary input. For an input $x$ and a set $B$ of coordinates, write $x\oplus B$ for the input obtained by flipping exactly the bits indexed by $B$.

A coordinate $i$ is sensitive at $x$ if $f(x\oplus\{i\})\ne f(x)$. The sensitivity $s(f,x)$ counts those coordinates, and $s(f)$ is the maximum of $s(f,x)$ over all inputs. A nonempty coordinate set $B$ is a sensitive block at $x$ if $f(x\oplus B)\ne f(x)$. The block sensitivity $\operatorname{bs}(f,x)$ is the largest number of pairwise disjoint sensitive blocks at that input. The quantity $\operatorname{bs}(f)$ is its maximum over all inputs.

Every block in one block-sensitivity witness is tested at the same input. The blocks are disjoint as coordinate sets; their sizes need not be equal. These conventions are those of the shared foundation mission, rather than complexity measures defined only on selected inputs or on a promise domain.

Formalization target

The goal is the campaign proposition $\operatorname{AchievesExponent}(\alpha)$. Explicitly, for every real $\varepsilon>0$ and every natural number $S\ge2$, there must exist a natural number $n$ and a total Boolean function $f:\{0,1\}^n\to\{0,1\}$ satisfying

$$s(f)\ge S,\qquad \operatorname{bs}(f)\ge s(f)^{\alpha-\varepsilon}.$$

Both the dimension and the function may depend on $\varepsilon$ and $S$. The sensitivity threshold is essential: a favorable ratio for one bounded example does not establish this statement. For example, choosing successively smaller positive losses and increasing thresholds produces a sequence of finite total Boolean functions with unbounded sensitivity and exponents approaching $\alpha$.

The exact numerator is the natural number

$$14055^8=1522813785050025472152230187890625.$$

The denominator inside the logarithm is $3738277295413674$. Both logarithm arguments exceed one. There is no division by a zero logarithm, and the result uses ordinary real powers. The goal does not assume a finite construction certificate or the existence of a suitable labeling as a hypothesis.

Improvement and verification status

The accepted construction theorem also proves the strict comparison

$$\frac{\log(14055^8)}{\log(3738289747988852)}<\alpha.$$

It improves the earlier public exponent, approximately $2.130320333220366$, by approximately $0.000505246$. The full proof constructs actual Boolean functions and establishes the asymptotic quantifiers; the numerical approximation alone is not the evidence for the separation.

The complete construction has passed local Lean kernel verification and Prove2Me verification. Its accepted submission is a9d25c46-43bd-4fb1-826b-0ed075b8cf0a. The source uses ordinary checked proofs with the standard axioms propext, Classical.choice, and Quot.sound. Its final statement spells out sensitivity and block sensitivity directly through finite sets. The campaign goal uses the existing shared definitions for those same quantities, and its proof explicitly establishes the equivalence needed to transfer the accepted result.

Why the full statement matters

A lower bound on block sensitivity at one input must be combined with an upper bound on sensitivity over every input. Local calculations that ignore the latter maximum can overstate the separation. Likewise, overlapping sensitive blocks cannot be counted as a disjoint family. These requirements persist through the construction and the passage to arbitrarily large sensitivity.

The exponent also depends on exact integer growth rates. Rounded numerical scores can identify candidates, but they do not establish the final real-power inequality. A complete proof must account for finite construction constraints, the complexity measures of the resulting functions, and the exponent loss allowed in the asymptotic statement. The accepted result includes these steps. This mission records that established result rather than a proposed stronger threshold awaiting construction.

Formalization scope

The development targets Lean 4.33.1 and Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474. Inputs are functions Fin n → Bool, and outputs are Bool. Sensitivity and block sensitivity are natural numbers obtained by finite maxima. The campaign proposition quantifies over positive real losses and natural sensitivity thresholds.

Dimension zero is permitted by the representation, but its sensitivity is zero and it cannot witness any required threshold $S\ge2$. Empty block families contribute zero; every counted block is nonempty. There are no hypotheses that can make the target vacuous. The shared definition and finite-certificate references are retained from the campaign template. The only new result recorded here is the improved separation exponent and its exact campaign formulation. Attribution to the original OpenAI development and Robin Kothari/Codex is retained in the accepted construction source; the new construction is credited to yousofy with Codex.

Selected references

• Prove2Me community, Block Sensitivity vs. Sensitivity, collaborative campaign, 2026. Campaign and template.
• Prove2Me community, Sensitivity foundation, formal definitions. Shared foundation mission.
• yousofy with Codex, Six shared defect tolerances improve the sensitivity exponent to 2.1308255794, Prove2Me, 2026. Accepted complete construction.
• yousofy with Codex, Earlier strict exponent checkpoint, Prove2Me, 2026. Public comparison theorem.

Motivation

Newtonian gravitation can be written in two ways. In Newtonian gravitation (NG), spacetime has a flat derivative operator $\nabla$ and a scalar potential $\varphi$ obeying Poisson's equation, and bodies are pushed off the straight lines of $\nabla$ by the force $-\nabla^a\varphi$. In geometrized Newtonian gravitation (GNG), also called Newton–Cartan theory, the potential is absorbed into a curved derivative operator $\tilde\nabla$ whose geodesics are the trajectories of freely falling bodies. This is the same geometrization that general relativity performs. Trautman (1965) proved that the two pictures pass into each other.

Weatherall (2016) asks whether NG and GNG are the same theory. He represents each theory by a category of models and calls two theories equivalent when there is an equivalence of categories that preserves empirical content. The answer depends on the arrows chosen for NG:

• NG₁ treats the potential as physical. Its arrows are diffeomorphisms preserving $t_a$, $h^{ab}$, $\nabla$ and $\varphi$, and NG₁ is not equivalent to GNG.
• NG₂ treats the potential as a gauge quantity, as Newton's Corollary VI suggests. Its arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$, and NG₂ is equivalent to GNG (Prop. 6.1).

This is the gravitational twin of the electromagnetic question "potentials vs. field strengths" treated in the companion missions on Weatherall's Understanding Gauge. The other side of the Newton–Cartan story, the classical limit of general relativity, is described under Significance.

Setting

Following Weatherall (p. 3), spacetime is $\mathbb R^4$, here in one global chart E = Fin 4 → ℝ with index 0 for time. The classical metrics are $t_a = dx^0$ (tt) and $h^{ab} = \mathrm{diag}(0,1,1,1)$ (hh). Their $t = \text{const}$ slices are complete copies of $\mathbb R^3$, as Weatherall requires.

A derivative operator is a smooth field of Christoffel symbols Γ x a b c $=\Gamma^a{}_{bc}(x)$, symmetric in $b,c$, acting by

$$\nabla_b\xi^a = \partial_b\xi^a + \Gamma^a{}_{bn}\xi^n .$$

It is compatible when $\nabla_a t_b = 0$ and $\nabla_a h^{bc} = 0$. Curvature uses Malament's sign convention:

$$\xi^bR^a{}_{bcd} = -2\nabla_{[c}\nabla_{d]}\xi^a, \qquad R_{bc} = R^n{}_{bcn}.$$

Other notation:

• Geometrization: $\tilde\nabla = (\nabla, -t_bt_c\nabla^a\varphi)$, that is $\tilde\Gamma^a{}_{bc} = \Gamma^a{}_{bc} + t_bt_c\,h^{an}\partial_n\varphi$ (geomΓ).
• Gauge transformation: $(\nabla, t_bt_c\nabla^a\psi)$ (gaugeΓ).
• Curves: a massive body has unit timelike tangent, $t_a\xi^a = 1$. Curves are smooth on an open interval.

The objects of the categories are:

• NG (IsNG Γ φ): compatible, flat $\nabla$ and a smooth potential $\varphi$. The mass density is $\rho = \nabla^a\nabla_a\varphi/4\pi$.
• GNG (IsGNG Γ): compatible $\tilde\nabla$ satisfying, for some smooth $\rho$,

$$(1)\ R_{ab} = 4\pi\rho\,t_at_b,\qquad (2)\ R^a{}_b{}^c{}_d = R^c{}_d{}^a{}_b,\qquad (3)\ R^{ab}{}_{cd} = 0 .$$

The arrows are diffeomorphisms $f$ of $\mathbb R^4$ that preserve $t_a$ and $h^{ab}$ and carry one derivative operator to the other through the transformation law

$$\partial_b\partial_c f^a + \Gamma'^a{}_{de}(f(x))\,\partial_bf^d\,\partial_cf^e = \partial_nf^a\,\Gamma^n{}_{bc}(x)$$

(IsGNGArrow). NG₁ arrows also preserve $\varphi$ (IsNG1Arrow). NG₂ arrows are pairs $(f,\psi)$ with $\nabla^a\nabla^b\psi = 0$, where $f$ carries the gauge-transformed pair $\big((\nabla,t_bt_c\nabla^a\psi),\ \varphi+\psi\big)$ to $(\nabla',\varphi')$ (IsNG2Arrow).

Formalization targets

Goal: NG₂ ≃ GNG (ng2_equiv_gng, Weatherall Prop. 6.1)

Geometrization $E(\nabla,\varphi) = \tilde\nabla$, $E(f,\psi) = f$ has these properties:

1. It sends NG₂ objects to GNG objects with the same allowed trajectories, and NG₂ arrows to GNG arrows.
2. It is full and faithful: every GNG arrow $f : E(A)\to E(A')$ is $E(f,\psi)$ for a unique $\psi$.
3. It is essentially surjective: every GNG object is isomorphic to a geometrization.

This is exactly the "full, faithful, essentially surjective" route of Weatherall's proof in App. A. These three properties together are equivalent to an equivalence of categories.

Milestones (source order)

1. geometrization, Prop. 2.1 (Trautman). For flat compatible $\nabla$ and Poisson's equation, $\tilde\nabla$ has these properties:
   • it is a classical spacetime;
   • its timelike geodesics are exactly the curves with $\xi^n\nabla_n\xi^a = -\nabla^a\varphi$;
   • it is the unique derivative operator with that property;
   • it satisfies (1)–(3).
2. recovery, Prop. 2.2 (Trautman). Every classical spacetime satisfying (1)–(3) comes from some flat $\nabla$ and potential $\varphi$ obeying Poisson's equation.
3. gauge_iff, the non-uniqueness remark after Prop. 2.2. A second pair $(\varphi',\nabla')$ works iff $\nabla^a\nabla^b(\varphi'-\varphi)=0$ and $\nabla' = (\nabla, t_bt_c\nabla^a(\varphi'-\varphi))$. Weatherall states the "if" direction and his proof of Prop. 6.1 uses the "only if" direction. The iff is Malament's Prop. 4.2.5. Note that $\psi = g(x^0)\,x^1$ is allowed: the gauge includes time-dependent uniform accelerations (Corollary VI).
4. geom_naturality, the key computation in App. A. A metric-preserving diffeomorphism carrying $\varphi$ to $\varphi'$ carries $\nabla$ to $\nabla'$ iff it carries $\tilde\nabla$ to $\tilde\nabla'$.
5. ng1_not_equiv_gng, the NG₁ row of Table 1 (§6, p. 18). No object map NG₁ → GNG preserves empirical content while inducing bijections of hom-sets. Weatherall states this in prose without a proof. The intended argument is that two NG₁ models related by a nonzero gauge share a geometrization but have no NG₁ arrow between them.

Significance

• Philosophy of physics. This is the standard worked example for categorical criteria of theoretical equivalence: Glymour's criterion versus equivalence of categories. It also shows how "excess structure" (here the potential) is detected by fullness.
• Physics. Newton–Cartan geometry is the non-relativistic limit of general relativity. Fletcher, Manchak, Schneider and Weatherall (2018), Thm 8 restates Malament's (1986) theorem in Künzle's (1976) framework. If a family $g_{ab}(\lambda)$ of Lorentzian metrics has $g_{ab}\to t_at_b$ and $\lambda g^{ab}\to -h^{ab}$, and its Einstein tensors converge, then the limit derivative operator satisfies (1) and (2), but not necessarily (3). GR limits therefore land in a slightly larger class than GNG, and condition (3) is exactly what the recovery theorem needs. This makes the present mission the Newtonian half of a planned GR-limit mission.
• Lean. This is a reusable coordinate model of Galilean/Newton–Cartan structures, Christoffel transformation laws and curvature, none of which exist in Mathlib.

Difficulty

• Milestones 1, 3 and 4 are long but elementary tensor computations. The uniqueness clause in 1 needs local existence of solutions of the trajectory ODE (Mathlib's Picard–Lindelöf).
• Milestone 2 is the heart. Compatibility forces $\tilde\Gamma$ to be a rotation field $\omega_{ij}$ plus an acceleration field $g_i$. Condition (3) forces $\omega$ to be spatially constant, and condition (2) makes $g$, minus the inertial terms of a rotating frame, a closed form on each slice. The Poincaré lemma, smoothly in the time parameter, then produces $\varphi$. The degree-1 Poincaré lemma on convex sets is in Mathlib, and the companion mission Weatherall 2016: Potentials vs. Field Strengths (continuum) develops the homotopy operator.
• The goal then assembles 2, 3 and 4.

Formalization scope

• Single global chart. Weatherall's spacetime is $\mathbb R^4$ with arbitrary $t_a, h^{ab}$. Here $t_a$ and $h^{ab}$ are fixed to their standard form in one global chart, a choice of Galilean coordinates; the derivative operators remain arbitrary. Arrows are genuine diffeomorphisms of $\mathbb R^4$.
• Normalized curves. Massive bodies have unit tangent $t_a\xi^a = 1$, as in Malament (Ch. 4). Without this normalization the geodesic and force laws are not equivalent.
• No category instances. Categories are encoded by their hom-predicates, and "equivalence of categories" by the full / faithful / essentially-surjective data of App. A. Composition laws are not required by any item.
• Out of scope: Weatherall's footnote 32 (spatially compact matter), Glymour's criterion, and the GR limit (planned as a separate mission).

Selected references

• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. Primary source: Props. 2.1, 2.2, 6.1, Table 1, App. A.
• D. B. Malament, Topics in the Foundations of General Relativity and Newtonian Gravitation Theory, University of Chicago Press (2012), Ch. 4 (Props. 4.2.1, 4.2.5). Conventions.
• D. B. Malament, Classical General Relativity, in Handbook of the Philosophy of Physics (2007).
• A. Trautman, Foundations and current problems of general relativity, in Brandeis Summer Institute 1964, Prentice-Hall (1965).
• S. C. Fletcher, J. B. Manchak, M. D. Schneider, J. O. Weatherall, Would Two Dimensions be World Enough for Spacetime?, Stud. Hist. Philos. Mod. Phys. 63 (2018) 100–113. Thm 8 is the Newtonian limit.
• H. P. Künzle, Covariant Newtonian limit of Lorentz space-times, Gen. Rel. Grav. 7 (1976) 445–457.