Pure Mathematics

Primes in progressions, uniformly in the modulus

Applying the circle method to an additive problem about primes requires counting primes in arithmetic progressions with an error term uniform in the modulus: the modulus is not fixed in advance, it grows with the size of the numbers being represented. The Siegel–Walfisz theorem is the classical statement of that uniformity, valid for every modulus up to a fixed power of $\log x$, and it is the one analytic ingredient the standard proof of Vinogradov's three primes theorem cannot do without.

The history is a sequence of partial uniformities:

• 1837. Dirichlet proves that every progression $a \bmod q$ with $(a,q)=1$ contains infinitely many primes, for each fixed $q$, with no rate (Dirichlet's theorem).
• 1896–1899. De la Vallée Poussin proves the prime number theorem with the error term $O(x e^{-c\sqrt{\log x}})$, and extends the zero-free region from $\zeta$ to $L(s,\chi)$, obtaining the prime number theorem in progressions for each fixed $q$ (PNT).
• 1918–1935. Landau and Page isolate the obstruction to uniformity: a single real zero near $s=1$, attached to a quadratic character. Landau shows at most one of two distinct real primitive characters can have such a zero; Page shows at most one modulus below a given bound can, yielding unconditional uniformity for $q$ up to a bounded power of $\log x$ (Page's theorem).
• 1935. Siegel proves $L(1,\chi) \gg_\varepsilon q^{-\varepsilon}$ for real primitive $\chi$, at the price of an ineffective constant (Siegel).
• 1936. Walfisz combines Siegel's bound with the de la Vallée Poussin machinery and obtains uniformity for every fixed power $q \le (\log x)^A$ (Walfisz).
• 1937. Vinogradov proves that every sufficiently large odd integer is a sum of three primes (Vinogradov's theorem).
• 2013. Helfgott removes the "sufficiently large", settling ternary Goldbach for all odd $n > 5$ (arXiv:1312.7748).

Setting

The von Mangoldt function $\Lambda(n)$ equals $\log p$ if $n = p^m$ is a prime power and $0$ otherwise. The Chebyshev function $\psi(x) = \sum_{n \le x} \Lambda(n)$ counts primes with weights; the prime number theorem is the assertion $\psi(x) \sim x$.

A Dirichlet character modulo $q$ is a multiplicative function $\chi : \mathbb{Z}/q\mathbb{Z} \to \mathbb{C}$, supported on the units and taking root-of-unity values there. The principal character $\chi = 1$ is the indicator of the units; a character is quadratic (real) if $\chi^2 = 1$ and $\chi \neq 1$, and primitive if it is not induced by a character of a proper divisor of $q$. The Dirichlet $L$-function $L(s,\chi) = \sum_{n\ge 1}\chi(n)n^{-s}$, defined for $\operatorname{Re} s > 1$, extends meromorphically to $\mathbb{C}$, entire except for a simple pole at $s = 1$ when $\chi$ is principal.

The two counting functions of the mission are the twisted von Mangoldt sum and the progression sum

$$\psi(N,\chi) = \sum_{n < N} \Lambda(n)\chi(n), \qquad \psi(N;q,a) = \sum_{\substack{n < N \\ n \equiv a\ (q)}} \Lambda(n),$$

related by finite character orthogonality. Write $\delta_\chi = 1$ for $\chi$ principal and $\delta_\chi = 0$ otherwise. A zero $\beta \in (0,1)$ of $L(s,\chi)$ lying inside the classical zero-free region is an exceptional zero (a Siegel zero); the set of such zeros for a given $\chi$ is the exceptional set $E$, which the results below constrain to have at most one element.

Formalization targets

The attack path follows Davenport, Multiplicative Number Theory, 3rd ed., §§14, 18, 20, 21, 22.

(1) zero_free_region (§14, pp. 88–96). There is an absolute $c>0$ such that for every $q \ge 1$ and every $\chi \bmod q$,

$$L(s,\chi) \neq 0 \quad\text{for } s \neq 1,\ \operatorname{Re} s \ \ge\ 1 - \frac{c}{\log\big(q(|\operatorname{Im} s| + 2)\big)},$$

with at most one exception, which is real, lies in $(0,1)$, is a simple zero, and can occur only for quadratic non-principal $\chi$.

(2) pnt_dlvp (§18, pp. 111–114). For some $c > 0$ and all $x \ge 2$,

$$\psi(x) = x + O\!\left(x\,e^{-c\sqrt{\log x}}\right).$$

(3) psi_char_of_region (§20, pp. 121–125). For a region constant $c>0$ there are $c_1, c_2 > 0$ such that, whenever $E$ is an exceptional set for $\chi \bmod q$ with respect to $c$ and $q \le \exp(c_2\sqrt{\log N})$,

$$\psi(N,\chi) = \delta_\chi N - \sum_{\beta \in E} \frac{N^\beta}{\beta} + O\!\left(N e^{-c_1\sqrt{\log N}}\right).$$

(4) siegel (§21, pp. 126–131). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

$$L(1,\chi) > C(\varepsilon)\, q^{-\varepsilon}.$$

(5) siegel_zero (§21, second form). For every $\varepsilon > 0$ there is $C(\varepsilon) > 0$ such that for every real primitive non-principal $\chi \bmod q$,

$$L(\sigma,\chi) \neq 0 \quad \text{for all real } \sigma > 1 - C(\varepsilon)q^{-\varepsilon}.$$

(6) siegelWalfisz (§22, pp. 132–134). For every $A > 0$ there are $C, c > 0$ such that for all $q \ge 1$, all $\chi \bmod q$, and all $N \ge 2$ with $q \le (\log N)^A$,

$$\big\lVert \psi(N,\chi) - \delta_\chi N \big\rVert \le C N e^{-c\sqrt{\log N}}.$$

This is literally the platform proposition ThreePrimes.SiegelWalfisz.

A corollary, not a milestone, records the progression form siegel_walfisz_ap: for $(a,q)=1$ and $q \le (\log N)^A$,

$$\psi(N;q,a) = \frac{N}{\varphi(q)} + O_A\!\left(N e^{-c\sqrt{\log N}}\right).$$

Goal (three_primes, §26). There is $N_0$ such that every odd $n \ge N_0$ is a sum of three primes. It follows from milestone (6) by the existing platform theorem deducing ThreePrimes.ThreePrimesExistence from ThreePrimes.SiegelWalfisz. The goal leaves $N_0$ unspecified rather than hard-coding a numeric threshold, so it is not invalidated by later improvements to that threshold.

What the result gives, and what remains to be formalized

Siegel–Walfisz is the standard uniform input downstream of which sit the circle method for ternary Goldbach, the Bombieri–Vinogradov theorem, and much of sieve theory. Without it, the three primes theorem's major-arc analysis has no main term.

Platform status is the reason this mission exists. A complete, machine-checked formalization of the three primes theorem already exists in the namespace ThreePrimes (by user tabbott), following Vaughan, The Hardy–Littlewood Method, Ch. 3, and Davenport §26. It is conditional: it takes Siegel–Walfisz as an explicit hypothesis ThreePrimes.SiegelWalfisz. Discharging that hypothesis makes the three primes theorem unconditional, and is the whole content of this mission.

Mathlib contains the analytic continuation of $L(s,\chi)$ (DirichletCharacter.LFunction), its functional equation, the non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$, Dirichlet's theorem, and the Chebyshev function. It does not contain the zero-free region for $L(s,\chi)$, the explicit formula for $\psi(x,\chi)$, Siegel's theorem, or Siegel–Walfisz. The platform additionally hosts the PNT+ project contour machinery for $\zeta$ — Borel–Carathéodory, the $3 + 4\cos\theta + \cos 2\theta$ inequality, a zero-free rectangle, and MediumPNT, $\psi(x) = x + O(x\exp(-c(\log x)^{1/10}))$. That is a template for the $L(s,\chi)$ analogues, not a proof of them, and its error term is weaker than the de la Vallée Poussin form milestone (2) asks for.

Where the obvious argument fails

The first idea is to run the $\zeta$ argument character by character. It works for complex $\chi$ and breaks for real ones. The positivity device that pushes zeros off $\operatorname{Re} s = 1$ compares $\chi$, $\chi^2$ and the trivial character at nearby points; when $\chi$ is quadratic, $\chi^2$ is principal and contributes the pole of $L(s,\chi_0)$ at $s = 1$ at exactly the height where the putative zero sits, so the inequality degrades from "no zeros" to "at most one zero" and stops there. Every later step inherits that unexcluded zero: milestone (3) can only be stated with the $N^\beta/\beta$ term present, and milestone (6) is exactly the assertion that for $q \le (\log N)^A$ this term is small — which Siegel's ineffective bound supplies and nothing effective is known to.

A second shortcut, deducing uniformity from Mathlib's non-vanishing of $L(s,\chi)$ on $\operatorname{Re} s \ge 1$ together with Dirichlet's theorem, also fails: those results are qualitative, carry no rate, and are not uniform in $q$.

Formalization scope

Sums run over $n < N$ with $N \in \mathbb{N}$, matching Vino.vmSumChar and ThreePrimes.SiegelWalfisz; Davenport sums over $n \le x$. The two differ by the single term $\Lambda(N) \le \log N$, negligible against every error term above. Milestone (2) alone uses a real argument, via Mathlib's Chebyshev.psi. $L(s,\chi)$ is Mathlib's DirichletCharacter.LFunction, so no continuation is reconstructed.

The zero-free region is Davenport.InRegion c q s, namely $\operatorname{Re} s \ge 1 - c/\log(q(|\operatorname{Im} s| + 2))$; the exceptional zero is packaged as IsExceptionalSet c χ E: $E$ is a subsingleton, every element is a real zero of $L(\cdot,\chi)$ in $(0,1)$ and can exist only for quadratic non-principal $\chi$, and $L(s,\chi) \neq 0$ at every $s \neq 1$ of the region outside $E$. Milestone (1) adds simplicity as $L'(\beta,\chi) \neq 0$ for $\beta \in E$.

Milestone (3) takes the region constant $c > 0$ as a parameter rather than importing it from milestone (1), so the milestones can be attempted in any order. For large $c$ the hypothesis IsExceptionalSet c χ E may be unsatisfiable for some $\chi$, making the statement vacuous there — a harmless weakening, not a falsehood, and not a trivializing reading: milestone (1) produces a definite small $c > 0$ with a witness $E$ for every $\chi$, so instantiating milestone (3) at that $c$ discharges the hypothesis rather than voiding it.

Siegel's theorem is stated for χ.IsQuadratic, χ ≠ 1, χ.IsPrimitive characters, with the conclusion a lower bound on $\operatorname{Re} L(1,\chi)$; since $L(1,\chi)$ is real for real $\chi$, this is the value itself, not a weakening. The constants in milestones (4), (5) and (6) are ineffective; the statements are plain existentials, so ineffectivity is invisible to Lean, but no numeric constant can be extracted from anything downstream of them.

The principal character is included in the character-form statements, with main term $N$ (if χ = 1 then (N : ℂ) else 0); milestones (3) and (6) therefore contain the prime number theorem itself and cannot be proved by restricting to non-principal $\chi$. Milestone (6) requires $c > 0$ strictly, which is what makes $Ne^{-c\sqrt{\log N}}$ a genuine saving over the trivial $\psi(N,\chi) \ll N$; with $c = 0$ allowed it would be empty.

Beyond the six milestones, a complete development needs Hadamard factorization for $L(s,\chi)$ as an entire function of order $1$, the zero-counting estimate $N(T,\chi)$ (§16, pp. 101–103), the truncated explicit formula for $\psi(x,\chi)$ (§19, pp. 115–120), Perron-type contour truncation, and the imprimitive-to-primitive reduction $|\psi(N,\chi) - \psi(N,\chi^{*})| \ll (\log q)(\log N)$. All of it is reusable well beyond this mission, being the standard prerequisite for Bombieri–Vinogradov, Linnik's theorem, and effective Chebotarev. Contributions of these supporting results, of alternative routes to milestone (3) following Montgomery–Vaughan Ch. 11, of the $\pi(x;q,a)$ versions, and of sharper constants are welcome.

Selected references

• H. Davenport, Multiplicative Number Theory, 3rd ed., revised by H. L. Montgomery, GTM 74, Springer, 2000. §§14, 18, 20, 21, 22, 26. doi:10.1007/978-1-4757-5927-3
• H. L. Montgomery and R. C. Vaughan, Multiplicative Number Theory I: Classical Theory, Cambridge University Press, 2007. Ch. 11–12 (Theorems 11.3, 11.14, 11.16, 12.10; Corollaries 11.10, 11.12, 11.17, 11.19). doi:10.1017/CBO9780511618314
• R. C. Vaughan, The Hardy–Littlewood Method, 2nd ed., Cambridge University Press, 1997. Ch. 3. doi:10.1017/CBO9780511470929
• C. L. Siegel, Über die Classenzahl quadratischer Zahlkörper, Acta Arithmetica 1 (1935), 83–86. eudml:205054
• A. Walfisz, Zur additiven Zahlentheorie II, Mathematische Zeitschrift 40 (1936), 592–607. doi:10.1007/BF01218882
• I. M. Vinogradov, Representation of an odd number as a sum of three primes, Doklady Akad. Nauk SSSR 15 (1937), 291–294. Vinogradov's theorem
• H. A. Helfgott, The ternary Goldbach conjecture is true, 2013. arXiv:1312.7748
• Siegel–Walfisz theorem, Wikipedia. link
• Page theorem, Encyclopedia of Mathematics. link
• A. Kontorovich et al., PrimeNumberTheoremAnd (PNT+), Lean formalization project. github
• Mathlib, Mathlib.NumberTheory.LSeries.DirichletContinuation. docs

Motivation

Polynomial representations provide a concrete way to study modules over Lie algebras: the underlying vector space is a polynomial ring, while the Lie generators act by explicit multiplication, shift, and differential operators. Chen and Tan classify a family of modules over the symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$ that are free of rank one over the universal enveloping algebra of an abelian nilradical. Their paper determines the family, its isomorphism classes, its weight and simplicity criteria, its finite-length behavior at exceptional parameters, and an application to Hamiltonian Lie algebras. This mission packages those headline results into one common Lean target, corresponding to Theorems 1.1--1.3 of Chen--Tan.

The common-family formulation matters. The source does not assert three unrelated existence theorems: one explicit two-parameter family $\tau(C,\Phi)$ carries all of the classification, simplicity, finite-length, and Hamiltonian consequences. The Lean goal therefore quantifies that family once and requires all headline properties of the same witness.

Setting

Fix $\ell\ge2$ and the complex symplectic Lie algebra $\mathfrak{sp}_{2\ell}(\mathbb C)$. The relevant maximal parabolic subalgebra has an abelian nilradical $\mathfrak n$. Its enveloping algebra is a polynomial algebra in the root generators, represented formally by a multivariate polynomial ring. A rank-one free $U(\mathfrak n)$-module can consequently be modeled on that polynomial ring.

The definition bundle presents the simple Chevalley generators and their action by explicit operators depending on a scalar $C\in\mathbb C$ and a polynomial parameter $\Phi$. Rather than assuming that these formulas already form a representation, the target asks for a generator presentation satisfying the symplectic Lie relations and for a representation family $\tau(C,\Phi)$ realizing the formulas. It also formalizes module equivalence, weight spaces, simplicity, Noetherian and Artinian conditions, finite composition factors, and the Shen--Larsson construction for a Hamiltonian Lie algebra.

Formalization targets

Common polynomial-module family

Prove that for every $\ell\ge2$ there is one generator presentation and one family

$$(C,\Phi)\longmapsto \tau(C,\Phi)$$

of $\mathfrak{sp}_{2\ell}(\mathbb C)$-representations on the polynomial ring, free of rank one over the abelian nilradical, satisfying the explicit generator formulas. Prove the source's classification and isomorphism criteria, including that $\tau(C,\Phi)$ is a weight module exactly when $\Phi$ is constant, and the stated simplicity criterion outside the exceptional arithmetic set

$$\left\{\frac{\ell+1}{2}-\frac{n}{2}:n\in\mathbb Z_{>0}\right\}.$$

For exceptional $C$, prove the Noetherian/Artinian and finite-composition-series conclusions and the weight/nonweight classification of the composition factors. Finally, prove that the canonical Hamiltonian Shen--Larsson construction has the exact degree-weight spaces and the source's simplicity and weight-module consequences. All clauses must be witnessed by the same family $\tau$.

Significance

The result gives a complete algebraic description of a large concrete class of non-highest-weight modules. It separates the generic simple regime from an exceptional finite-length regime and shows how nonweight symplectic modules generate weight modules over an infinite-dimensional Hamiltonian Lie algebra. The explicit formulas make the family suitable for calculation, while the classification prevents duplicate parameter choices from being mistaken for genuinely different modules.

Formalization adds checks that are easy to blur in prose. In particular, the generator formulas cannot be called a Lie representation until the defining relations have been verified, and the same witness must support every later theorem. A completed proof will contribute reusable Lean infrastructure for symplectic root data, polynomial representations, module-theoretic finiteness, exact weight-space descriptions, and Hamiltonian Lie-algebra functors. The paper's proofs are known; the open task is their machine-checked reconstruction.

Difficulty

The first obstacle is structural rather than computational. Checking formulas on individual generators is insufficient: all Chevalley and Serre relations must hold with the correct operator order and signs, after which the action must extend to the full Lie algebra. Classification then requires controlling arbitrary rank-one-free modules, not merely verifying that the displayed examples exist.

The exceptional parameters introduce a second layer. Generic simplicity and exceptional finite length are logically different claims, and the composition-factor statement must be tied to the same parameterized representation. The Hamiltonian application adds another algebra and a tensor construction; exact weight spaces and simplicity cannot be obtained by treating the functor as an opaque interface. The Lean goal deliberately keeps these obligations inside one theorem so that separate convenient witnesses cannot satisfy different portions.

Formalization scope

The mission works over $\mathbb C$ with natural rank $\ell\ge2$. The definition bundle uses concrete multivariate polynomials, matrices and linear maps, a presented symplectic Lie algebra, Lie representations, submodules, and tensor products. The exceptional set is expressed with complex coercions, so no accidental natural-number division is involved. The nilradical action, freeness, parameter equivalence, weight-space equalities, simplicity, finite-length properties, and Hamiltonian brackets are transparent propositions in the bundle.

The final theorem is a single conjunction under one existentially quantified presentation and one existentially quantified family $\tau$. Several convenient corollaries can be projected from it, but they are not independent targets and do not permit different witnesses. The bundle contains no custom axioms or opaque semantic assumptions, and the only admitted term is the main theorem's sorry. Contributions may split the proof into source-numbered lemmas about generator relations, classification, exceptional submodules, or the Shen--Larsson application, provided the shared-family quantifier structure is preserved.

Selected references

• Yang Chen and Haijun Tan, Simple $\mathfrak{sp}_{2\ell}(\mathbb C)$-modules which are free over an abelian nilradical, Journal of Algebra 697 (2026), 341--372, Theorems 1.1--1.3 (formal Theorems 3.7, 3.8, 4.7, 4.9, and 5.2). DOI
• G. Shen, foundational work on mixed-product constructions for modules over Lie algebras of Cartan type, cited in the source paper for the Shen--Larsson functor.

The Monge optimal transport problem on the real line with the classical distance cost $|x-y|$ famously fails to have a unique solution. Juillet (2019) restored uniqueness by considering the strictly concave power costs $|x-y|^p$ with $p<1$ and letting $p\to 1^-$: the limit selects a distinguished optimal plan, the excursion coupling, built from the level sets of the difference $F_\sigma=F_\mu-F_\nu$ of the cumulative distribution functions. This mission formalizes the completed-graph construction, the generalized Banach indicatrix identities of Bertoin-Yor, the alternating crossing structure of almost every level, and the marginal identities for the crossing counting measures. It culminates in Propositions 3.5-3.6: every monotone transport plan is concentrated on the paired routes, and the marginals uniquely determine the coupling carried by those routes, including in the presence of atoms.

This mission formalizes the key implication 3=>4 in Juillet's Main Theorem.

Motivation and history

Compressing an operator to a closed subspace keeps the information visible within that subspace but can discard interactions with its orthogonal complement. The compression-rigidity question asks whether a particular equality detects that no such interactions were present. Its inputs are two commuting positive contractions and an ordinary strictly convex function of two real variables. The issue is the equality case, not the existence of a general operator inequality for every convex function.

The question was contributed by Boris Bilich to the CUHK-Shenzhen AI Math Problems collection and added on June 1, 2026. The original problem asks about operators on a Hilbert space without imposing finite dimension. The first formal target in this mission treated matrices with supplied joint spectral data. That finite-dimensional declaration has a verified proof on Prove2Me, but it does not settle the unrestricted Hilbert-space question. The September 2026 correction restores arbitrary complex Hilbert spaces as the main target and preserves the earlier result as a supporting artifact.

Setting

Let $H$ be a complete complex Hilbert space, and let $\mathcal B(H)$ be its algebra of bounded complex-linear operators. The multiplication $AB$ means composition, with $B$ acting first, and $A^*$ denotes the adjoint. A positive contraction $A$ is self-adjoint, satisfies $\operatorname{Re}\langle v,Av\rangle\geq0$ for every $v\in H$, and has operator norm at most one. Both zero and the identity are permitted.

Write $S=[0,1]^2$. Let $X,Y\in\mathcal B(H)$ be positive contractions satisfying $XY=YX$. Their joint continuous functional calculus assigns an operator $g(X,Y)$ to each continuous real function $g$ on $S$. It is characterized as a continuous unital real star-algebra homomorphism from $C(S,\mathbb R)$ to $\mathcal B(H)$ that maps the two coordinate functions to $X$ and $Y$. The domain has the uniform norm and the codomain the operator norm. The existence and uniqueness of this calculus follow from the standard joint spectral theorem; the relevant source is Dereziński, Lemma 6.6, printed page 43.

An orthogonal projection is an operator $P$ satisfying $P^*=P$ and $P^2=P$. The compressed operators $PXP$ and $PYP$ are still viewed as operators on the original space $H$, not as operators on a separately chosen finite-dimensional range. The question includes the additional hypothesis that these compressed operators commute. The original commutation of $X$ and $Y$ does not remove the need to state this hypothesis.

Formalization targets

The main target is the entire compression implication from the source. Let $f:S\to\mathbb R$ be continuous and strictly convex: for distinct $x,y\in S$ and $0<t<1$, its value at $tx+(1-t)y$ is strictly less than $t f(x)+(1-t)f(y)$. For $X,Y,P$ as above, the question is whether

$$P f(X,Y)P=P f(PXP,PYP)P \quad\Longrightarrow\quad PX=XP\ \text{and}\ PY=YP.$$

Both outer projections on the right are part of the original assertion. There is no hypothesis that $f(0,0)=0$. Commutation of $P$ with each coordinate operator is exactly the reducing-subspace conclusion asked for in the source.

The accompanying standard infrastructure target asserts that, for every commuting pair of positive contractions on $H$,

$$\exists!\,\Phi:C(S,\mathbb R)\longrightarrow\mathcal B(H),\qquad \Phi(x\mapsto x_0)=X,\quad\Phi(x\mapsto x_1)=Y,$$

where $\Phi$ is continuous, unital, real-linear, multiplicative and star-preserving. This is the unit-square, real-valued-function specialization of Lemma 6.6, not a claim that this known theorem is a new research conjecture. Its Lean proof is a separate supporting obligation. The earlier two-dimensional milestone and the proved finite-dimensional capstone remain available; neither replaces the new main target.

Significance

A positive resolution would show that exact preservation of one strictly convex functional-calculus value, under the specified commuting-compression hypothesis, forces both operators to preserve the projection's range and its orthogonal complement. A negative resolution would require an actual Hilbert space, operators and strictly convex function satisfying every hypothesis while at least one of the two reducing identities fails.

The formal development separates this research question from the standard spectral infrastructure needed to express it. The new main declaration is an open proof obligation. The joint-calculus existence-and-uniqueness declaration is also unproved in this contribution, although mathematically standard. Local compilation and server publication check the declarations' well-formedness; they are not proofs of either statement. Only the earlier finite-dimensional result is being reported here as already proved.

Difficulty

Arbitrary bounded commuting self-adjoint operators need not have a joint eigenbasis. Consequently a matrix formulation that records finitely many joint spectral atoms cannot serve as the general operator model. The compressed pair may also have different spectral data from the original pair. The equality involves these two different functional calculi, with a projection on either side of each value.

Strict convexity in this question is ordinary scalar strict convexity on the square. Operator convexity, finite rank of the projection, compactness of the coordinate operators, and a multivariable operator Jensen inequality are not additional assumptions. Introducing any of them would change the requested question. The general formulation must also retain boundary cases rather than exclude them to simplify an argument.

Formalization scope

The Lean model uses actual bounded complex-linear maps on an arbitrary complete inner-product space. It imposes no finite-dimensionality, separability, common-eigenbasis or nonzero-space assumption. It includes $P=0$, $P=I_H$ and the zero Hilbert space. The scalar field convention is complex; a real-Hilbert-space transfer is not separately formalized here.

The function is stored on the ambient real plane, but continuity, strict convexity and evaluation use only its restriction to $S$. Values outside $S$ are irrelevant, and continuity outside the square is not required. Thus storing an ambient function does not exclude any continuous function originally defined only on the square.

Joint evaluation is a total definition. If a representing continuous unital real star-algebra homomorphism exists, it chooses one for the operator pair and then evaluates the supplied function. Otherwise it returns zero. The separate existence-and-uniqueness target establishes that this fallback is inapplicable to commuting positive contractions and that the choice is immaterial. No field in the model assumes the compression-rigidity conclusion. The supporting standard theorem must also apply to the compressed pair using the original projection and positivity hypotheses, without adding representation existence as a new restriction on the main question.

The replacement definition and both statements were built at Lean 4.30.0 with supported Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f, and their final versions received independent blind readbacks. Published older declarations and their proof identities are preserved. They should be cited with their finite-dimensional scope, not described as a solution of the arbitrary-Hilbert-space target.

Selected references

• Boris Bilich, Equality case for compressed convex functional calculus, CUHK-Shenzhen AI Math Problems, Problem 2, added June 1, 2026. Original statement.
• Jan Dereziński, Bounded operators, Warsaw University lecture notes, January 2007, Lemma 6.6, printed page 43. Joint continuous functional calculus.

Motivation

The fundamental group $\pi_1(X, x_0)$ is the first algebraic invariant a student of topology meets, and $\pi_1(S^1)\cong\mathbb{Z}$ is the first computation of it that carries real content. Allen Hatcher's Algebraic Topology (Cambridge University Press, 2002; freely available at pi.math.cornell.edu/~hatcher/AT/AT.pdf) is the standard text on the subject. Its Chapter 1 opens with exactly this computation (Theorem 1.7, p. 29) and immediately draws three classical consequences from it: the Fundamental Theorem of Algebra (Theorem 1.8), the Brouwer fixed point theorem for the disk (Theorem 1.9), and the Borsuk–Ulam theorem for the sphere (Theorem 1.10).

This mission is the opening entry in a series that formalizes Hatcher's book capstone by capstone. It covers the subsection "The Fundamental Group of the Circle" of Section 1.1 (pp. 29–33): the covering-space lifting properties that drive the proof, the theorem itself, and its three applications. Later entries in the series (van Kampen's theorem, the classification of covering spaces, simplicial and singular homology) will build on the declarations introduced here, which all live in the shared Lean namespace Hatcher.

Setting

A path in a topological space $X$ is a continuous map $f : I \to X$, where $I = [0,1]$. A homotopy of paths is a family $f_t : I \to X$, $0 \le t \le 1$, such that the endpoints $f_t(0) = x_0$ and $f_t(1) = x_1$ are independent of $t$ and the associated map $F : I \times I \to X$, $F(s,t) = f_t(s)$, is continuous. A loop at a basepoint $x_0$ is a path with $f(0) = f(1) = x_0$. The set of homotopy classes $[f]$ of loops at $x_0$ is the fundamental group $\pi_1(X, x_0)$; its product is $[f][g] = [f\cdot g]$, where $f\cdot g$ traverses $f$ and then $g$, each at double speed (Hatcher, Proposition 1.3).

The circle $S^1 \subset \mathbb{R}^2$ is realised as the unit circle of $\mathbb{C}$, so the point $(\cos\theta, \sin\theta)$ is $e^{i\theta}$ and the basepoint $(1,0)$ is $1$. Hatcher's map

$$p : \mathbb{R} \to S^1, \qquad p(s) = (\cos 2\pi s, \sin 2\pi s) = e^{2\pi i s}$$

is Hatcher.circleCover. The loops

$$\omega_n(s) = (\cos 2\pi n s, \sin 2\pi n s) = p(ns), \qquad n \in \mathbb{Z},$$

based at $(1,0)$ are Hatcher.omegaLoopN n, and $\omega = \omega_1$ is Hatcher.omegaLoop; its class $[\omega] \in \pi_1(S^1, 1)$ is Hatcher.omegaClass.

A covering space of $X$ is a space $\tilde X$ together with a map $p : \tilde X \to X$ such that every $x \in X$ has an open neighbourhood $U$ for which $p^{-1}(U)$ is a disjoint union of open sets each mapped homeomorphically onto $U$ by $p$ (Hatcher's condition $(\ast)$, p. 29; such a $U$ is evenly covered). A lift of a map $f : Y \to X$ is a map $\tilde f : Y \to \tilde X$ with $p \circ \tilde f = f$.

Formalization targets

Goal (Theorem 1.7)

$\pi_1(S^1, 1)$ is an infinite cyclic group generated by $[\omega]$. In the form stated in Lean:

$$\forall\, g \in \pi_1(S^1, 1)\quad \exists!\, n \in \mathbb{Z}:\quad [\omega]^n = g.$$

Surjectivity of $n \mapsto [\omega]^n$ says $[\omega]$ generates; uniqueness of $n$ says the group is infinite cyclic rather than finite.

Milestones on the road to the goal

1. $p(s) = e^{2\pi i s}$ is a covering space of $S^1$ (Hatcher, p. 29).
2. Homotopy lifting property (c): for a covering space $p : \tilde X \to X$, a map $F : Y \times I \to X$ and a lift of $F|_{Y \times \{0\}}$ extend uniquely to a lift of $F$ (p. 30).
3. Path lifting property (a): a path $f$ starting at $x_0$ and a point $\tilde x_0 \in p^{-1}(x_0)$ determine a unique lift $\tilde f$ starting at $\tilde x_0$ (p. 29).
4. Lifting homotopies of paths (b): a homotopy of paths $f_t$ starting at $x_0$ lifts uniquely to a homotopy of paths $\tilde f_t$ starting at $\tilde x_0$ (p. 29).
5. Every loop in $S^1$ at $(1,0)$ is homotopic to $\omega_n$ for a unique $n \in \mathbb{Z}$ (the reformulation of Theorem 1.7 that Hatcher actually proves, p. 29).
6. $[\omega]^n = [\omega_n]$ for every $n \in \mathbb{Z}$ (Hatcher's remark after Theorem 1.7, p. 29).

Applications (Theorems 1.8–1.10)

$$\text{Every nonconstant } f \in \mathbb{C}[z] \text{ has a root in } \mathbb{C}.$$ $$\text{Every continuous } h : D^2 \to D^2 \text{ has a fixed point.}$$ $$\text{Every continuous } f : S^2 \to \mathbb{R}^2 \text{ satisfies } f(x) = f(-x) \text{ for some } x \in S^2.$$

Significance

The result itself. The computation $\pi_1(S^1) \cong \mathbb{Z}$ assigns to every loop in the circle an integer, its winding number, and shows that this integer is the only homotopy invariant of the loop. It is the seed of degree theory, and in Hatcher's text it is the starting point for every later computation of fundamental groups (products, van Kampen, covering spaces). The three applications are the standard demonstration that a single algebraic invariant can settle purely geometric or algebraic existence questions.

Formalizing it. Mathlib (revision 0df444a) already contains the covering-space infrastructure: IsCoveringMap, path lifting (IsCoveringMap.liftPath, eq_liftPath_iff'), homotopy lifting (IsCoveringMap.liftHomotopy, eq_liftHomotopy_iff'), monodromy, and the fact that Circle.exp is a covering map (Circle.isCoveringMap_exp). It also has FundamentalGroup X x as the endomorphism group of the fundamental groupoid. It does not contain the computation $\pi_1(S^1) \cong \mathbb{Z}$, nor the two-dimensional Brouwer and Borsuk–Ulam theorems. The Fundamental Theorem of Algebra is in Mathlib as Complex.exists_root (proved by Liouville's theorem rather than by Hatcher's argument); it is kept as a milestone because it is one of the section's stated theorems, and a solver may close it directly from Mathlib. Milestones 2–4 are also within reach of the existing lifting API, but they are the lemmas Hatcher states and uses, and a faithful record of them in the mission's own namespace is what later entries in the series will import.

Difficulty

The obvious first idea for the goal is to define the winding number of a loop through the complex argument. That fails because $\arg$ is discontinuous on $S^1$; the integer has to be produced by lifting the loop through $p$ and reading off the endpoint of the lift, which is only well defined because of the uniqueness in the path lifting property. The second difficulty is uniqueness of $n$: this needs lifting of homotopies (milestone 4), not just of paths, together with the observation that a lifted homotopy of paths has constant endpoints.

Connecting the concrete loops to Mathlib's abstract $\pi_1$ is its own obstacle. FundamentalGroup Circle 1 multiplies by composing morphisms of the fundamental groupoid, so identifying $[\omega]^n$ with the class of the explicit loop $\omega_n$ (milestone 6) requires reparametrization arguments for concatenated paths, for negative $n$ as well as positive.

For Theorem 1.9 the difficulty is the construction and continuity of the retraction $r : D^2 \to S^1$ from a fixed-point-free map, and then the non-existence of a retraction, which uses that $\pi_1(S^1) \neq 0$. For Theorem 1.10 Hatcher's proof lifts a loop $g(s) = f(\cos 2\pi s, \sin 2\pi s)/\lvert \cdots \rvert$ through $p$ and shows the lift changes by an odd integer over half a turn; making that parity argument rigorous in Lean is the substance of the milestone.

Formalization scope

• $S^1$ is Circle (the unit circle in $\mathbb{C}$) with basepoint 1; $D^2$ is Metric.closedBall (0 : EuclideanSpace ℝ (Fin 2)) 1; $S^2$ is Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1, with $-x$ the antipodal point.
• A covering space is Mathlib's IsCoveringMap p. This agrees with Hatcher's condition $(\ast)$; neither requires $p$ to be surjective.
• Paths are continuous maps C(I, X) or Mathlib Paths; for homotopies of paths, the square is written I × I with Hatcher's coordinate order $F(s,t) = f_t(s)$: the first coordinate is the path parameter, the second the homotopy parameter. In the general homotopy lifting property the domain is Y × I with $Y$ an arbitrary topological space, as in Hatcher.
• $\pi_1(S^1, 1)$ is Mathlib's FundamentalGroup Circle 1, and $[\omega]$ is FundamentalGroup.fromPath ⟦omegaLoop⟧. Because the goal quantifies over integer powers of a single element, the order of multiplication in FundamentalGroup is immaterial to its truth.
• The goal is stated as $\forall g\, \exists! n,\ [\omega]^n = g$ rather than as an abstract isomorphism with $\mathbb{Z}$, so that the generator is pinned to Hatcher's explicit loop; an isomorphism FundamentalGroup Circle 1 ≃* Multiplicative ℤ sending $[\omega]$ to $1$ is an immediate corollary and a welcome contribution.
• "Nonconstant polynomial" is 0 < f.degree, which excludes both the zero polynomial and nonzero constants.

Contributions welcome: proofs of the milestones from Mathlib's lifting API, a degree homomorphism $\pi_1(S^1,1) \to \mathbb{Z}$ packaged for reuse, and any lemma about concatenation and reparametrization of loops in Circle that later chapters of the series can import.

Selected references

• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002. Section 1.1, "The Fundamental Group of the Circle", pp. 29–33. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf
• L. E. J. Brouwer, Über Abbildung von Mannigfaltigkeiten, Mathematische Annalen 71 (1911), 97–115. https://doi.org/10.1007/BF01456931
• K. Borsuk, Drei Sätze über die n-dimensionale euklidische Sphäre, Fundamenta Mathematicae 20 (1933), 177–190. https://doi.org/10.4064/fm-20-1-177-190
• Mathlib, Mathlib/Topology/Homotopy/Lifting.lean (path and homotopy lifting for covering maps). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Topology/Homotopy/Lifting.lean
• Mathlib, Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean (the fundamental group). https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/AlgebraicTopology/FundamentalGroupoid/FundamentalGroup.lean

Motivation

In one complex variable the Riemann mapping theorem classifies a whole class of domains by topology alone: every nonempty simply connected proper subdomain of $\mathbb{C}$ is biholomorphic to the unit disc. Nothing of the kind holds in several variables. The two most obvious generalizations of the disc to $\mathbb{C}^n$, the unit ball and the unit polydisc, are homeomorphic, yet no biholomorphic map carries one onto the other. This is the first result a student of several complex variables meets that has no one-variable shadow, and it is the standard illustration that the geometry of the boundary, not the topology of the domain, governs holomorphic equivalence.

As recounted in the source, Poincaré (1907) observed the inequivalence by computing the automorphism groups of $\mathbb{D}^2$ and $\mathbb{B}_2$, assuming the maps extend past the boundary; H. Cartan gave the first complete proof in 1931; and Rothstein (1935) proved that there is not even a proper holomorphic map from the bidisc to the ball. This mission follows the presentation in §1.4–1.6 of J. Lebl, Tasty Bits of Several Complex Variables (version 4.4, 2026), where the inequivalence is derived from a general theorem on proper maps out of product domains, followed by Cartan's uniqueness theorem and the basic structure theory of zero sets and injective maps.

Setting

Write $\mathbb{C}^n$ for $n$-tuples $z = (z_1, \dots, z_n)$ of complex numbers, $\mathbb{D} = \{\zeta \in \mathbb{C} : |\zeta| < 1\}$ for the unit disc, and $\|z\| = (|z_1|^2 + \cdots + |z_n|^2)^{1/2}$ for the Euclidean norm. The unit ball and unit polydisc are

$$\mathbb{B}_n = \{ z \in \mathbb{C}^n : |z_1|^2 + \cdots + |z_n|^2 < 1 \}, \qquad \mathbb{D}^n = \{ z \in \mathbb{C}^n : |z_k| < 1 \text{ for } k = 1, \dots, n \},$$

and the unit sphere is $S^{2n-1} = \partial\mathbb{B}_n = \{ z : |z_1|^2 + \cdots + |z_n|^2 = 1 \}$. A domain is a nonempty connected open set. A map between open subsets of complex spaces is holomorphic if it is complex differentiable at every point.

A continuous map $f : U \to V$ is proper if $f^{-1}(K)$ is compact for every compact $K \subset V$. A biholomorphic map $f : U \to V$ is a holomorphic bijection whose inverse is holomorphic; every biholomorphism is proper. An analytic disc is a nonconstant holomorphic map $\varphi : \mathbb{D} \to \mathbb{C}^n$, and a set $S$ contains no analytic discs if no analytic disc has $\varphi(\mathbb{D}) \subset S$. A circular domain is a domain $U$ with $e^{i\theta} z \in U$ whenever $z \in U$ and $\theta \in \mathbb{R}$.

Formalization targets

Goal: Rothstein's theorem (Theorem 1.4.4)

$$\text{there is no proper holomorphic map } f : \mathbb{D}^2 \to \mathbb{B}_2 .$$

The path to the goal

• Proposition 1.4.6. $S^{2n-1}$ contains no analytic discs.
• Lemma 1.4.7. For bounded domains $U \subset \mathbb{R}^n$, $V \subset \mathbb{R}^m$ and continuous $f : U \to V$: $f$ is proper if and only if, whenever $p_k \in U$ and $p_k \to p \in \partial U$, every limit point of $\{f(p_k)\}$ lies in $\partial V$.
• Theorem 1.4.8. If $U = U' \times U'' \subset \mathbb{C}^n \times \mathbb{C}^k$ ($n, k \ge 1$) and $V \subset \mathbb{C}^m$ are bounded domains and $\partial V$ contains no analytic discs, there is no proper holomorphic map $U \to V$.

Further results on the same definitions

• Theorem 1.5.1 (Cartan). If $U \subset \mathbb{C}^n$ is a bounded domain, $a \in U$, $f : U \to U$ holomorphic, $f(a) = a$ and $Df(a) = I$, then $f(z) = z$ on $U$.
• Corollary 1.5.2. A biholomorphism $f : U \to V$ of bounded circular domains with $f(0) = 0$ is the restriction of a linear map.
• Theorem 1.6.1 (Riemann extension). If $g \in \mathcal{O}(U)$ is not identically zero on a domain $U$ and $f \in \mathcal{O}(U \setminus g^{-1}(0))$ is locally bounded in $U$, then $f$ extends uniquely to some $F \in \mathcal{O}(U)$.
• Theorem 1.6.2. The zero set of a holomorphic function that is not identically zero on a domain is, on an open dense subset of itself, locally a graph $z_n = g(z_1, \dots, z_{n-1})$ after reordering the variables.
• Theorem 1.6.6. An injective holomorphic map $U \to \mathbb{C}^n$ on an open $U \subset \mathbb{C}^n$ has nowhere vanishing Jacobian determinant; a holomorphic bijection between open sets of $\mathbb{C}^n$ is biholomorphic.

The goal is chosen as the textbook's headline result of §1.4. Theorem 1.4.8 is strictly more general; it is a milestone, so a solver may prove the goal as its special case.

Significance

Rothstein's theorem implies the biholomorphic inequivalence of $\mathbb{B}_2$ and $\mathbb{D}^2$, the basic example that the Riemann mapping theorem has no analogue in several variables. Theorem 1.4.8 isolates the reason: a boundary that contains analytic discs cannot be mapped properly into a boundary that contains none. Cartan's uniqueness theorem and its corollary are the standard tools for computing automorphism groups of the ball and the polydisc. The Riemann extension theorem, the local graph structure of zero sets and the Jacobian criterion for injective maps are used throughout the theory of analytic varieties and of holomorphic mappings.

All of these results are classical and proved in the source. None of them is formalized in Mathlib or on the platform for $\mathbb{C}^n$ with $n \ge 2$: Mathlib has one-variable Riemann removable singularities and the maximum modulus principle, and the platform has one-variable results on injective holomorphic maps. This mission produces machine-checked statements of the several-variable versions, and infrastructure (proper maps between subsets, analytic discs, holomorphic families) that later chapters of the series reuse.

Difficulty

The goal cannot be reached through topology: $\mathbb{D}^2$ and $\mathbb{B}_2$ are homeomorphic, so any argument must use holomorphy essentially and must see the boundary. The step that needs genuine analysis is passing from properness, a statement about compact sets, to a statement about boundary values of holomorphic functions of one variable along slices of the product domain; this requires normal families (Montel's theorem) in several variables, which Mathlib does not provide in the needed form. Cartan's theorem rests on power-series expansions in homogeneous parts and vector-valued Cauchy estimates on polydiscs. Theorem 1.6.2 needs the holomorphic implicit function theorem and Rouché's theorem, and Theorem 1.6.6 an induction on dimension that runs through Theorem 1.6.2. The Riemann extension theorem needs holomorphy of parameter-dependent Cauchy integrals.

Formalization scope

$\mathbb{C}^n$ is Fin n → ℂ. Mathlib's norm on this type is the sup norm, so Metric.ball 0 1 is the polydisc, not the ball. The ball and the sphere are therefore defined with the explicit Euclidean condition, unitBall n = {z | ∑ k, ‖z k‖ ^ 2 < 1} and unitSphere n = {z | ∑ k, ‖z k‖ ^ 2 = 1}. The polydisc is written coordinatewise as unitPolydisc n. Reading the ball as the sup-norm ball would trivialize the goal (the identity of the bidisc is a proper holomorphic self-map); the definitions exclude that reading. Boundedness is Bornology.IsBounded, and boundaries are Mathlib's frontier; neither depends on the norm. A domain is IsOpen U ∧ IsConnected U, so it is nonempty.

Holomorphic means DifferentiableOn ℂ on an open set. On open sets this is equivalent to the book's Definition 1.1.2 (Proposition 1.1.3 and Theorem 1.2.1). Maps into $\mathbb{C}^m$ are Fin m → ℂ-valued. $Df(a)$ is fderiv ℂ f a, and the Jacobian determinant is LinearMap.det of it. Maps are ambient functions whose values off the relevant set are irrelevant. Consequently:

• Proper is IsProperMapOn f U V: f maps U into V, is continuous on U, and U ∩ f ⁻¹' K is compact for every compact K ⊆ V. This is Definition 1.4.3 for the restricted map. It is not IsProperMap of the ambient map.
• Uniqueness in Theorem 1.6.1 is uniqueness on $U$.
• The inverse of a biholomorphism is a function g holomorphic on $V$ with Set.InvOn g f U V.

Lemma 1.4.7 works in Fin n → ℝ and reads "limit point of the sequence $\{f(p_k)\}$" as a cluster point of the sequence (MapClusterPt). Theorem 1.4.8 uses the product type (Fin n → ℂ) × (Fin k → ℂ) for $\mathbb{C}^n \times \mathbb{C}^k$. In Theorem 1.6.2, "after reordering the variables" means choosing the index j of the solved-for coordinate. The remaining coordinates are indexed by {i // i ≠ j}. Only the open-disc part of Definition 1.4.5 (analytic discs) is formalized, because closed analytic discs are not used here.

A complete development needs Montel's theorem for maps into bounded subsets of $\mathbb{C}^m$, homogeneous expansions and Cauchy estimates on polydiscs, the holomorphic implicit function theorem, Rouché's theorem, and holomorphic parameter-dependent Cauchy integrals. All of it is reusable beyond this mission, and contributions of it are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026, §1.4–1.6 (pp. 32–46). https://www.jirka.org/scv/scv.pdf
• H. Poincaré, Les fonctions analytiques de deux variables et la représentation conforme, Rend. Circ. Mat. Palermo 23 (1907), 185–220. https://doi.org/10.1007/BF03013518
• S. G. Krantz, Function Theory of Several Complex Variables, 2nd ed., AMS Chelsea, 2001 (cited by Lebl as [K]). https://doi.org/10.1090/chel/340

Motivation

Quantizing a Yang–Mills theory by the Faddeev–Popov procedure requires a gauge condition that picks one representative from each gauge orbit. In the Landau gauge the condition is $\partial_\mu A_\mu^a = 0$. Gribov showed in 1978 that this condition is not ideal: a gauge orbit can meet the surface $\partial_\mu A_\mu = 0$ more than once, so gauge-equivalent configurations — Gribov copies — are still being integrated over (V. N. Gribov, Quantization of non-Abelian gauge theories, Nucl. Phys. B139 (1978) 1). Infinitesimally, a copy of a transverse field $A$ corresponds to a zero mode of the Faddeev–Popov operator $M^{ab}(A) = -\partial_\mu D_\mu^{ab}(A)$, which is Hermitian on transverse configurations.

Gribov's proposed remedy is to restrict the functional integral to the Gribov region $\Omega$, the set of transverse configurations at which $M(A)$ is positive definite. The interest of $\Omega$ is not only that it removes infinitesimal copies: the fact that it is a bounded region of field space is the geometric input of Gribov's confinement scenario, because restricting the integration to a bounded region deforms the gluon propagator in the infrared and produces a mass scale. Whether the restriction to $\Omega$ is the physically correct prescription is still debated; the geometric properties of $\Omega$ themselves are not — they are consequences of the algebraic structure of $M(A)$, and they are what this mission formalizes.

Timeline of the properties at issue, as recorded in §2.2.1 (pp. 188–189) of the review by N. Vandersickel and D. Zwanziger, The Gribov problem and QCD dynamics, Phys. Rep. 520 (2012) 175–251 (doi:10.1016/j.physrep.2012.07.003):

• 1978, Gribov: existence of copies infinitesimally across the horizon $\partial\Omega$ (Nucl. Phys. B139 (1978) 1).
• 1982, D. Zwanziger: $\Omega$ is convex and bounded in every direction (Nucl. Phys. B209 (1982) 336).
• 1982, M. Semenov-Tyan-Shanskii and V. Franke: the variational characterization of $\Omega$ by relative minima of $\|A^U\|^2$, and the fact that $\Omega$ still contains copies.
• 1989, G. Dell'Antonio and D. Zwanziger: $\Omega$ is contained in an ellipsoid (Nucl. Phys. B326 (1989) 333).
• 1991, G. Dell'Antonio and D. Zwanziger: every gauge orbit passes inside $\Omega$ (Comm. Math. Phys. 138 (1991) 291–299).

Setting

Fix a real vector space $V$ of gauge-field configurations (in the physical situation, the transverse fields $A_\mu^a$) and a finite index set $\{1,\dots,n\}$ on which the Faddeev–Popov operator acts (colour index times a finite basis of fluctuation modes $\omega$). The formalization works with the algebraic structure that the Faddeev–Popov operator has, and nothing else:

$$M(A) \;=\; M_0 \;+\; M_2(A),$$

where

• $M_0$ is the field-independent part, $M_0 = -\partial^2$ in the physical setting, taken here to be a fixed symmetric positive definite $n \times n$ real matrix;
• $A \mapsto M_2(A)$ is linear in $A$, and each $M_2(A)$ is a symmetric traceless real $n \times n$ matrix. In the physical setting $M_2(A)^{ab} = \partial_\mu f^{abc} A_\mu^c$, which is traceless already in the colour indices.

The Gribov region is

$$\Omega \;=\; \{\, A \in V \;:\; M(A) \text{ is positive definite} \,\}, \qquad M(A) \text{ positive definite} \iff \forall\, w \neq 0,\ w^{\mathsf T} M(A)\, w > 0 .$$

This is Eq. (2.52) of the review, with positivity as in Eq. (2.54). The boundary $\partial\Omega$ is the first Gribov horizon, where the lowest non-trivial eigenvalue of $M(A)$ vanishes.

Formalization targets

Goal — $\Omega$ is a bounded convex set containing the origin

$$0 \in \Omega, \qquad \Omega \text{ convex}, \qquad \forall A \neq 0\ \exists \lambda_0 > 0\ \forall \lambda \ge \lambda_0:\ \lambda A \notin \Omega, \qquad \Omega \text{ bounded}.$$

The last two clauses are stated under the assumption that $A \mapsto M_2(A)$ is injective, i.e. that distinct configurations give distinct field-dependent parts; without it $\Omega$ contains the whole kernel of $M_2$ as a linear subspace and no boundedness statement can hold.

Supporting statements

$$M(\alpha A_1 + \beta A_2) = \alpha M(A_1) + \beta M(A_2) \quad (\alpha + \beta = 1),$$ $$M \text{ symmetric},\ \operatorname{tr} M = 0,\ M \neq 0 \;\Longrightarrow\; \exists w:\ w^{\mathsf T} M w < 0 .$$

These are Eq. (2.53) and Eq. (2.58) of the review; they are the two ingredients from which convexity and directional boundedness follow.

Significance

What the result gives: $\Omega$ is the region to which Gribov's improved gauge fixing restricts the functional integral, and every subsequent construction in this line of work — the no-pole condition, the horizon function and the local Gribov–Zwanziger action — presupposes that the restriction is to a bounded convex region containing the perturbative point $A = 0$. Convexity is what makes the horizon condition a single well-posed constraint; boundedness in every direction is the property from which the infrared suppression of the gluon propagator, and hence Gribov's mass scale, is read off. Without boundedness there is no geometric mechanism for a mass gap in this scenario.

Status honesty: these statements are proved mathematics, not open problems; the arguments in §2.2.1 of the review are short. What is missing is a machine-checked account. No formalization of the Gribov region in Lean is known to the drafter of this proposal; the platform's existing Gribov material concerns Singer's topological obstruction to continuous gauge fixing, which is a different theorem about a different object.

Difficulty

The statements are elementary once the correct hypotheses are isolated, and the mission is calibrated accordingly: it is a faithfulness exercise rather than a depth exercise. The two places where a naive attempt fails are worth naming. First, directional boundedness does not follow from positivity alone: it needs the tracelessness of $M_2(A)$, which is what forces a direction $w$ with $w^{\mathsf T} M_2(A) w < 0$; a positive semidefinite perturbation would give a region unbounded along that ray. Second, "bounded in every direction" does not imply "bounded" for a general set, and the implication used here rests on convexity together with injectivity of $M_2$ — the argument goes through a limit of rescaled configurations and a closure of the positivity condition, not through a uniform bound extracted directly from the ray statement.

Formalization scope

The mission commits to a finite-dimensional linear-algebra model of the Faddeev–Popov operator, packaged as a structure carrying: the matrix $M_0$ together with a proof that it is positive definite; the linear map $A \mapsto M_2(A)$ together with proofs that each $M_2(A)$ is symmetric and traceless. Configurations live in an arbitrary real vector space $V$, which carries a norm and finite-dimensionality only in the two statements where boundedness is asserted. Positive definiteness is Mathlib's notion for real matrices, which includes symmetry; the region is the set of configurations where it holds strictly, so $\Omega$ is the open region and the horizon is not part of it.

This is a model, not the field-theoretic object: it replaces the operator $-\partial_\mu D_\mu$ acting on transverse fields by its finite-dimensional algebraic shadow, and the reviewer should audit it as such. The properties targeted here are exactly those whose proofs in §2.2.1 use only linearity in $A$, symmetry, tracelessness, and positivity of $-\partial^2$; results that genuinely need the infinite-dimensional setting — that every gauge orbit passes inside $\Omega$, and that $\Omega$ still contains copies on its boundary — are deliberately out of scope, since they cannot be stated in this model.

The model is not vacuous: an instance exists already for $V = \mathbb{R}$, $n = 2$, $M_0 = I$ and $M_2(t) = t\,\mathrm{diag}(1,-1)$, with $M_2$ injective, so none of the statements is satisfied vacuously. Nor is any target trivially true: $\Omega$ is a proper nonempty subset of $V$ in that instance.

Infrastructure needed: Mathlib's positive-definiteness API for matrices, the spectral theorem for real symmetric matrices (for the traceless lemma), and basic convexity and boundedness in finite-dimensional normed spaces. The traceless lemma — a nonzero symmetric traceless matrix has a direction of negative quadratic form — is reusable well beyond this mission. Contributions extending the model towards the infinite-dimensional setting, or supplying the explicit ellipsoidal bound of Dell'Antonio–Zwanziger in place of plain boundedness, are welcome.

Selected references

• N. Vandersickel, D. Zwanziger, The Gribov problem and QCD dynamics, Physics Reports 520 (2012) 175–251. https://doi.org/10.1016/j.physrep.2012.07.003
• V. N. Gribov, Quantization of non-Abelian gauge theories, Nuclear Physics B139 (1978) 1.
• D. Zwanziger, Nonperturbative modification of the Faddeev–Popov formula and banishment of the naive vacuum, Nuclear Physics B209 (1982) 336.
• M. Semenov-Tyan-Shanskii, V. Franke, A variational principle for the Lorentz condition and restriction of the domain of path integration in non-abelian gauge theory, 1982.
• G. Dell'Antonio, D. Zwanziger, Ellipsoidal bound on the Gribov horizon contradicts the perturbative renormalization group, Nuclear Physics B326 (1989) 333.
• G. Dell'Antonio, D. Zwanziger, Every gauge orbit passes inside the Gribov horizon, Communications in Mathematical Physics 138 (1991) 291–299.

Motivation

In one complex variable every open set is the natural domain of some holomorphic function. In several variables this fails: by the Hartogs phenomenon, every function holomorphic on some domains extends to a strictly larger one. The domains that are "natural", the domains of holomorphy, are characterised by a convexity condition on the domain. Since the work of Levi (1910), Hartogs, Oka and Cartan–Thullen (1932), the way to state that condition intrinsically has been pseudoconvexity. The tool that makes it work is the plurisubharmonic function, the complex analogue of a convex function.

This mission formalizes the part of that theory that needs no partial differential equations: harmonic, subharmonic and plurisubharmonic functions; smoothing of plurisubharmonic functions; the characterizations of Hartogs pseudoconvexity; and the Cartan–Thullen theorem. The source is §2.4–2.6 of Jiří Lebl's open textbook Tasty Bits of Several Complex Variables (version 4.4, 2026), pp. 78–103.

Timeline, as the book presents it:

• Hartogs (1906) found the extension phenomenon.
• Levi (1910) found the boundary condition now called Levi pseudoconvexity.
• Cartan and Thullen (1932) proved that domains of holomorphy are exactly the holomorphically convex domains.
• Oka (1942–1953), Bremermann and Norguet (1954) solved the Levi problem: every pseudoconvex domain is a domain of holomorphy. The book states this result (its Theorem 2.6.2) but does not prove it.

Setting

Throughout, $\mathbb{C}^n$ carries the Euclidean norm $\|z\| = (|z_1|^2 + \dots + |z_n|^2)^{1/2}$. A domain is a nonempty connected open set. For $K, U \subset \mathbb{C}^n$, $K \subset\subset U$ means that $K$ is relatively compact in $U$: its closure is compact and contained in $U$.

Harmonic and subharmonic functions (one variable). A $C^2$ function $f$ on an open $U \subset \mathbb{C}$ is harmonic if $\nabla^2 f = 0$. A function $f : U \to \mathbb{R} \cup \{-\infty\}$ is subharmonic if it is upper-semicontinuous and, for every disc $B_r(a)$ with $\overline{B_r(a)} \subset U$ and every $g$ continuous on $\overline{B_r(a)}$ and harmonic inside it, $f \le g$ on $\partial B_r(a)$ implies $f \le g$ on $B_r(a)$.

Plurisubharmonic functions. For $U \subset \mathbb{C}^n$ open, $f : U \to \mathbb{R} \cup \{-\infty\}$ is plurisubharmonic if it is upper-semicontinuous and $\xi \mapsto f(a + b\xi)$ is subharmonic on $\{\xi : a + b\xi \in U\}$ for all $a, b \in \mathbb{C}^n$.

Hulls and convexity. For a class $\mathcal{F}$ of extended-real functions on $U$ and $K \subset U$, the hull is

$$\widehat{K} = \{x \in U : f(x) \le \sup_{y \in K} f(y) \text{ for all } f \in \mathcal{F}\}.$$

$U$ is convex with respect to $\mathcal{F}$ if $K \subset\subset U$ implies $\widehat{K} \subset\subset U$. For $\mathcal{F} = \{|f| : f \in \mathcal{O}(U)\}$ this is holomorphic convexity, with hull $\widehat{K}_U$.

Hartogs pseudoconvexity. $f : U \to \mathbb{R}$ is an exhaustion function if $\{z \in U : f(z) < r\} \subset\subset U$ for every $r$. A domain is Hartogs pseudoconvex if it admits a continuous plurisubharmonic exhaustion function.

Analytic discs. A closed analytic disc is a nonconstant holomorphic $\varphi : \mathbb{D} \to \mathbb{C}^n$ that extends continuously to $\overline{\mathbb{D}}$. Its image is $\Delta = \varphi(\mathbb{D})$ and its boundary is $\partial\Delta = \varphi(\partial\mathbb{D})$.

Formalization targets

Goal: Theorem 2.5.6

For a domain $U \subsetneq \mathbb{C}^n$ with $\rho(z) = \operatorname{dist}(z, \partial U)$, the following are equivalent:

$$\text{(i) } -\log\rho \text{ is plurisubharmonic};\quad \text{(ii) } U \text{ is Hartogs pseudoconvex};$$ $$\text{(iii) } U \text{ is convex w.r.t. plurisubharmonic functions on } U;\quad \text{(iv) } \textstyle\bigcup_\alpha \partial\Delta_\alpha \subset\subset U \Rightarrow \bigcup_\alpha \Delta_\alpha \subset\subset U$$

for every collection of closed analytic discs $\Delta_\alpha \subset U$.

Milestones

• Proposition 2.4.3. A continuous $f$ is harmonic iff it has the mean-value property. An upper-semicontinuous $f$ is subharmonic iff $f(a) \le \frac{1}{2\pi}\int_0^{2\pi} f(a + re^{i\theta})\,d\theta$ whenever $\overline{\Delta_r(a)} \subset U$.
• Proposition 2.4.7. Finite suprema of subharmonic functions are subharmonic, and so are arbitrary suprema that are finite and upper-semicontinuous.
• Proposition 2.4.9. A $C^2$ function is plurisubharmonic iff its complex Hessian $[\partial^2 f/\partial\bar z_k \partial z_\ell]$ is positive semidefinite.
• Theorem 2.4.10. Every plurisubharmonic $f$ is the pointwise limit of smooth plurisubharmonic $f_\epsilon \ge f$ on $U_\epsilon = \{z \in U : \operatorname{dist}(z, \partial U) > \epsilon\}$.
• Theorem 2.5.2 (Kontinuitätssatz, second version): (iii) implies (iv).
• Lemma 2.5.7. Hartogs pseudoconvexity is a local property of the boundary.
• Theorem 2.4.12 (Radó): a continuous function holomorphic off its zero set is holomorphic.
• Theorem 2.6.3 (Cartan–Thullen): for a domain $U \subsetneq \mathbb{C}^n$, being a domain of holomorphy, $\operatorname{dist}(K, \partial U) = \operatorname{dist}(\widehat{K}_U, \partial U)$ for all $K \subset\subset U$, and holomorphic convexity are equivalent.

Significance

The result. Theorem 2.5.6 makes pseudoconvexity checkable. Condition (i) involves one explicitly given function of the domain's geometry. Condition (iv) involves only families of discs. Condition (ii) is the form the Levi problem and Hörmander's $L^2$ theory need. From these equivalences one gets, for example, that intersections and increasing unions of pseudoconvex domains are pseudoconvex, that pseudoconvexity is a biholomorphic invariant, and, with Lemma 2.5.7, that it is a local boundary property. In the smooth case that local property is Levi pseudoconvexity (Theorem 2.5.8, chapter III of this series). Cartan–Thullen supplies the other half of the picture for domains of holomorphy.

Formalizing it. All of these results are classical and proved in the book, apart from routine steps left as exercises. As far as is known, none of them is formalized in any proof assistant. Mathlib has harmonic functions (InnerProductSpace.HarmonicOnNhd) and the circle average, but no subharmonic or plurisubharmonic functions, no hulls and no pseudoconvexity. The Prove2Me corpus holds a one-variable subharmonic definition based on the sub-mean-value property and the one-directional mean-value property of harmonic functions; neither is the book's definition or statement. The mission would give Lean a first library of plurisubharmonic functions in $\mathbb{C}^n$, with the definition matching the textbook.

Difficulty

The obvious route to (iv) ⇒ (i) of the goal would show $-\log\rho$ is plurisubharmonic by computing a complex Hessian (Proposition 2.4.9). That fails: $\rho$ is in general not even differentiable, so no Hessian is available. Several other steps also need measure theory with extended-real values. The sub-mean-value property requires Lebesgue integrals of upper-semicontinuous functions that may equal $-\infty$ on large sets. Smoothing requires convolution of such functions with a mollifier, and pointwise convergence in $[-\infty, \infty)$. Suprema of families lose upper semicontinuity in general, which is why Proposition 2.4.7 carries that hypothesis. In Cartan–Thullen, holomorphic convexity alone must produce a holomorphic function on $U$ that extends across no boundary point. Nothing in the hypothesis supplies such a function directly.

Formalization scope

• $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n), so balls, $\rho(z)$ = Metric.infDist z (frontier U), $U_\epsilon$ and $\operatorname{dist}(K, \partial U)$ are all Euclidean, as in the book. They are not sup-norm polydisc quantities.
• Functions with values in $\mathbb{R} \cup \{-\infty\}$ are EReal-valued with $+\infty$ excluded on $U$. Upper semicontinuity is UpperSemicontinuousOn for the order of EReal.
• Hulls take suprema in EReal, and holomorphic hulls in $[0, \infty]$, so no supremum takes a junk value. Set distances are infima in $[0, \infty]$ (Metric.infEDist).
• The circle mean in Proposition 2.4.3 (ii) is the Lebesgue integral of the positive part minus that of the negative part.
• Holomorphic on an open set is DifferentiableOn ℂ, which is equivalent to the book's Definition 1.1.2 there.
• A domain is IsOpen U ∧ IsConnected U. Relative compactness is compact closure contained in $U$.
• Harmonic and subharmonic functions are defined only on open subsets of $\mathbb{C} = \mathbb{R}^2$. The book defines them on $\mathbb{R}^n$, but only uses $n = 2$. This is the one restriction of scope.
• A collection of analytic discs is a set of parametrizing maps, and $\Delta_\alpha = \varphi_\alpha(\mathbb{D})$ as in Definition 1.4.5.
• Definitions 1.4.5 and 2.1.1 are restated locally in the namespace LeblSCV.Pseudoconvex.

Several trivializing formalizations are ruled out. Plurisubharmonicity is not defined through the Hessian condition, so the mission does not reduce to $C^2$ functions. Nor is it defined by the sub-mean-value property, which would make Proposition 2.4.3 (ii) a tautology. $\rho$ is not the sup-norm distance. Suprema, infima and integrals are nowhere allowed to default to $0$ on empty, unbounded or non-integrable input.

A complete development needs:

• mean values of upper-semicontinuous functions and the Poisson integral on discs (Theorem 2.4.2, not a milestone);
• convolution with a radial mollifier on $\mathbb{C}^n$;
• Cauchy estimates on polydiscs.

The subharmonic and plurisubharmonic layer is reusable beyond this mission. Chapters on the Levi problem, the $\bar\partial$-problem and Bergman kernels would all build on it. Proofs of the smaller milestones, and alternative arguments for the goal, are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables: A Whirlwind Tour of the Subject, version 4.4, 2026. https://www.jirka.org/scv/scv.pdf
• L. Hörmander, An Introduction to Complex Analysis in Several Variables, 3rd ed., North-Holland Mathematical Library 7, 1990 (the book's reference [H] for the Levi problem).
• H. Cartan and P. Thullen, "Zur Theorie der Singularitäten der Funktionen mehrerer komplexen Veränderlichen: Regularitäts- und Konvergenzbereiche", Mathematische Annalen 106 (1932), 617–647.

Motivation

When are two scientific theories "the same theory in different words"? Philosophers of science have used two formal criteria. Definitional equivalence (Glymour) is strict: it requires a common definitional extension and therefore cannot relate theories with different numbers of sorts. Categorical equivalence (Halvorson, Weatherall) is liberal: it asks only that the categories of models be equivalent. It has been applied to classical mechanics, electromagnetism and Newtonian gravitation (Weatherall 2016; survey in Weatherall 2019).

Barrett and Halvorson (2016) proposed Morita equivalence as a syntactic criterion between these two. It allows definitions of new sorts (products, coproducts, subsorts, quotients) in addition to the usual definitions of new predicates and function symbols. Their main results place the new criterion strictly between the other two:

• Morita equivalence implies categorical equivalence (their Theorem 5.1).
• The converse fails (their Theorem 5.2).

This mission formalizes that comparison: the semantic core of Morita extensions, the implication, the separating example, and the paper's motivating "two kinds of things" example.

Setting

A signature $\Sigma$ (Sig) consists of a type of sorts, function symbols $f : \sigma_1\times\dots\times\sigma_m\to\sigma$ and predicate symbols $p\subseteq\sigma_1\times\dots\times\sigma_m$. Formulas (Formula L Γ) are built in a typed context $\Gamma$ from $\bot$, $=$, predicates, $\to$ and $\forall$. A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory $T$ is a set of formulas in context, each read as its universal closure; a model of $T$ is a structure satisfying them all.

The category $\mathrm{Mod}(T)$ (Model T) has the models of $T$ as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories $T_1,T_2$ are categorically equivalent (CategoricallyEquivalent) if $\mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2)$.

A Morita extension of a $\Sigma$-theory $T$ (MoritaData L T) adds to $\Sigma$:

• new sorts, each with its defining symbols:
  • a product $\sigma$ of $\sigma_1,\sigma_2$, with projections $\pi_1,\pi_2$;
  • a coproduct, with injections $\rho_1,\rho_2$;
  • a subsort cut out by a $\Sigma$-formula $\varphi(x)$, with an injection $i$;
  • a quotient by a $\Sigma$-formula $\varphi(x_1,x_2)$, with a projection $\varepsilon$;
• new predicates and function symbols, each explicitly defined by a $\Sigma$-formula.

Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension $T^+$ (D.ext) is $T$ together with these axioms. Each definition must satisfy its admissibility condition in every model of $T$:

Definition	Condition
subsort	$\exists x\,\varphi(x)$
quotient	$\varphi$ is an equivalence relation
function symbol	$\forall x\,\exists!y\,\varphi(x,y)$

The reduct gives a functor $\Pi:\mathrm{Mod}(T^+)\to\mathrm{Mod}(T)$ (D.proj).

$T_1$ and $T_2$ are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions $T_1\rightsquigarrow T_1'$ and $T_2\rightsquigarrow T_2'$ (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.

Formalization targets

Goal: Morita equivalence implies categorical equivalence

$$T_1 \text{ Morita equivalent to } T_2 \;\Longrightarrow\; \mathrm{Mod}(T_1)\simeq\mathrm{Mod}(T_2).$$

Milestones

1. Unique expansion. Every model $M$ of $T$ has an expansion $N\models T^+$ with $\Pi N\cong M$, and any two such expansions are isomorphic.
2. $\Pi$ is faithful.
3. $\Pi$ is full.
4. Conservativity. For every $\Sigma$-formula $\alpha$: $T\models\alpha$ iff $T^+\models\alpha$.
5. Translation. Every $\Sigma^+$-formula whose free variables all have old sorts is $T^+$-equivalent to a $\Sigma$-formula.
6. Two kinds of things. $T_1=\{\exists x\,p(x),\ \exists x\,q(x),\ \forall x\,(p(x)\vee q(x)),\ \forall x\,\neg(p(x)\wedge q(x))\}$ over one sort is Morita equivalent to the empty theory over two sorts.
7. Separating example, first half. $T_1=\{\exists^{=1}x\,(x=x)\}$ and $T_2=T_1\cup\{\forall y\,(p_0(y)\to p_i(y)) : i\in\mathbb N\}$, over one sort and countably many unary predicates, are categorically equivalent.
8. Separating example, second half. These two theories are not Morita equivalent.

Milestones 1–3 together say that $\Pi$ is an equivalence of categories. Milestones 6–8 are not needed for the goal; they record the paper's examples, which show that Morita equivalence relates theories with different numbers of sorts and is strictly stronger than categorical equivalence.

Significance

The result itself. The goal makes Morita equivalence a syntactic sufficient condition for categorical equivalence: an explicit dictionary of definitions yields an equivalence of model categories. Milestone 8 shows the converse fails, so categorical equivalence is strictly weaker. Milestone 6 shows that Morita equivalence, unlike definitional equivalence, can relate theories with different numbers of sorts. Together these locate the criterion that later philosophy-of-physics work uses to compare formulations with different ontologies, such as different numbers of kinds of objects.

Formalizing it. The results are proved on paper and, as far as is known, have no machine-checked proofs. Mathlib's ModelTheory library is single-sorted, so none of this is available there. The mission produces a reusable many-sorted first-order logic with:

• syntax, semantics and signature maps;
• elementary embeddings and the category of models;
• Morita extensions with their reduct functors.

The paper's arguments for conservativity and translation are informal in places; for example, the translation in the appendix uses coding of new-sorted variables. A formal proof fixes these details.

Difficulty

The obvious route to the goal composes the reduct functors along the chains. The work lies in showing that each reduct is an equivalence when the arrows are elementary embeddings.

• Fullness. An elementary embedding of reducts extends uniquely to the new sorts. Showing that the extension is again elementary requires the translation of Milestone 5: every $\Sigma^+$-formula has to be pulled back to a $\Sigma$-formula, including formulas that quantify over the new sorts.
• Coproduct and quotient sorts. Quantifiers over these sorts must be eliminated in favour of quantifiers over the old sorts.

For Milestone 8 the difficulty is reversed. One must rule out every pair of chains, including chains that introduce arbitrary new sorts. The paper's proof argues with a single common Morita extension. The definition, however, allows chains, and the paper notes that a chain need not collapse to a single extension. The argument must therefore be run through conservativity and translation along each chain.

Formalization scope

• Self-contained logic. Signatures have dependent arities (Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.
• Theories. A theory is a Set (Axiom L), each axiom being a formula in context read as its universal closure. Because sorts are nonempty, this agrees with the sentence version.
• Nonempty sorts. Every structure has nonempty carriers. This is the paper's convention, and without it Milestone 6 is false: the empty theory over two sorts would have models with an empty sort.
• Morita extensions are built, not recognized. MoritaData L T lists the new sorts and symbols and their defining $\Sigma$-formulas. The signature $\Sigma^+$ (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of $T$. Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.
• A common signature up to renaming. MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of $T_2'$ iff its F-reduct is a model of $T_1'$.
• Universes. Models live in Type.
• Separating example. The paper writes $T_2$ with fresh symbols $q_i$; here $T_1$ and $T_2$ share the signature with predicates $p_i$, which only renames symbols.
• No trivialization. None of the targets holds vacuously: Morita extensions require genuine admissibility proofs, and the arrows are elementary embeddings, not arbitrary maps. Milestone 6 needs explicit chains and an explicit renaming, with arity casts.

A complete development will need:

• the substitution and weakening lemmas for de Bruijn formulas;
• the realization of signature maps;
• the construction of expansions;
• a translation function from $\Sigma^+$-formulas to $\Sigma$-formulas.

These pieces are reusable for any later work on interpretations or theoretical equivalence. Alternative proofs of Milestone 8, for example by counting finitely axiomatized subtheories, are welcome.

Selected references

• T. W. Barrett, H. Halvorson, Morita Equivalence, Rev. Symb. Logic 9 (2016) 556–582. arXiv:1506.04675. Source of all targets: §3–§5 and the appendix; Example 4 and Theorems 4.1–4.3, 5.1, 5.2.
• J. O. Weatherall, Are Newtonian Gravitation and Geometrized Newtonian Gravitation Theoretically Equivalent?, Erkenntnis 81 (2016) 1073–1091. arXiv:1411.5757.
• J. O. Weatherall, Theoretical Equivalence in Physics, Philos. Compass 14 (2019). arXiv:1810.08192.
• H. Halvorson, The Logic in Philosophy of Science, Cambridge University Press, 2019. doi:10.1017/9781316275603.