Algebra

Motivation

Kleene's theorem (Kleene 1956; McNaughton–Yamada 1960) is a cornerstone of formal language theory: over a free monoid, the languages recognized by finite automata are exactly the regular ones — those built from finite languages by union, concatenation, and the Kleene star. Mezei and Wright (1967) lifted recognizability off strings, calling a subset of an arbitrary algebra recognizable when it is the preimage of a subset of a finite algebra under a homomorphism. Replacing strings by terms — finite trees labelled by operation symbols — gives the theory of recognizable tree languages and finite tree automata of Gécseg and Steinby (1984), where the Kleene correspondence reappears with a tree concatenation and an iteration operation in the role of the star.

Many computational structures are inherently many-sorted: typed lambda calculi, structured programming languages, process calculi, XML schemas — data and operations organized into distinct sorts. In the many-sorted setting a signature assigns to each operation symbol the sorts of its arguments and of its value, variables carry sorts, and a language is a sort-indexed family of term sets. The predecessor of this mission, Climent Vidal–Cosme Llópez 2020 (CVCL20), established that recognizability over free many-sorted algebras is preserved — and, where applicable, reflected — by substitution, iteration, quotient, inverse tree-homomorphic image, and direct linear image, via finite-index congruences. What CVCL20 left open is the regular side: whether a natural class of many-sorted regular expressions captures exactly the recognizable languages. This mission closes that gap.

Setting

Fix a finite set of sorts $S$. An $S$-sorted set $A = (A_s)_{s\in S}$ is a family of sets; it is finite when $\coprod_{s\in S} A_s$ is finite. An $S$-sorted signature $\Sigma$ assigns to each pair $(\mathbf{s}, s) \in S^\star \times S$ a set $\Sigma_{\mathbf{s},s}$ of operation symbols of arity $\mathbf{s}$ and coarity $s$. A $\Sigma$-algebra $\mathbf{A}$ is an $S$-sorted set $A$ together with, for each $\sigma \in \Sigma_{\mathbf{s},s}$, an operation $\sigma^{\mathbf A}\colon A_{\mathbf s} \to A_s$, where $A_{\mathbf s} = \prod_{j} A_{s_j}$. A homomorphism commutes with all operations sortwise.

The free $\Sigma$-algebra $\mathbf T_\Sigma(X)$ on an $S$-sorted set $X$ of variables has as its sort-$s$ carrier $\mathrm T_\Sigma(X)_s$ the set of $(X,s)$-terms; every $S$-sorted map $X \to A$ extends uniquely to a homomorphism $\mathbf T_\Sigma(X) \to \mathbf A$. Following automata-theoretic tradition, subsets of $\mathrm T_\Sigma(X)$ are called languages. For a sort $s$, a language $L \subseteq \mathrm T_\Sigma(X)_s$ is $s$-recognizable when there are a finite $\Sigma$-algebra $\mathbf N$, a homomorphism $f\colon \mathbf T_\Sigma(X) \to \mathbf N$, and a subset $M \subseteq N_s$ with $L = f_s^{-1}[M]$. Write $\mathrm{Rec}_s(\mathbf T_\Sigma(X))$ for the set of all such $L$.

Two operations on languages, both performed sortwise, generate the regular expressions. Given a variable $z \in X_u$ and a language $L \subseteq \mathrm T_\Sigma(X)_u$, $z$-substitution $\left(\!\begin{smallmatrix}z\\ L\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s$ replaces, in every term of an input language of sort $s$, each occurrence of $z$ independently by a term of $L$. The $z$-iteration is $L^{\star z} = \bigcup_{i\in\mathbb N} L^{i\,z}$, where $L^{0\,z} = \{z\}$ and $L^{i+1\,z} = L^{i\,z} \cup \left(\!\begin{smallmatrix}z\\ L^{i\,z}\end{smallmatrix}\!\right)^{\sharp\mathsf p}_s(L)$. For a finite $S$-sorted set $Z$, the regular signature $\mathrm{Reg}(S,\Sigma,Z)$ expands $\Sigma$ by an empty constant $\varnothing_s$, a binary sum $+_s$, a unary $z$-iteration $(\cdot)^{\star z}$ for each $z\in Z_s$, and a $z$-substitution operation for each $z\in Z_t$. Its terms are the regular expressions over $(S,\Sigma,Z)$; the power algebra $\mathbf T_\Sigma(Z)^\wp$ carries a canonical $\mathrm{Reg}(S,\Sigma,Z)$-algebra structure, and interpreting a regular expression there yields a language $\{R\}^{Z\sharp}_s$. A language $L\subseteq \mathrm T_\Sigma(X)_s$ is $s$-regular when $L = \{R\}^{Z\sharp}_s$ for some finite $Z\supseteq X$ and some regular expression $R$ of type $s$; write $\mathrm{Reg}_s(\mathbf T_\Sigma(X))$.

Formalization targets

Goal — the many-sorted Kleene theorem

$$\forall\, s\in S,\qquad \mathrm{Rec}_s(\mathbf T_\Sigma(X)) \;=\; \mathrm{Reg}_s(\mathbf T_\Sigma(X)).$$

The statement fixes no automaton model and no normal form for regular expressions: it asserts only that the two classes of languages coincide, at every sort, for every finite $S$, every finite $S$-sorted signature $\Sigma$, and every finite $S$-sorted set $X$. It splits into $\mathrm{Reg}_s \subseteq \mathrm{Rec}_s$ (Corollary 4.8) and $\mathrm{Rec}_s \subseteq \mathrm{Reg}_s$ (Proposition 4.10).

Significance

The result completes the Kleene–Myhill–Nerode correspondence on the side of universal algebra, uniformly over an arbitrary finite many-sorted signature: it names the exact operations — those of $\Sigma$, plus empty language, union, sortwise substitution, and sortwise iteration — that generate precisely the finite-state behaviours. Over non-free structures the correspondence is known to fail (recognizable but non-rational subsets of a monoid, Eilenberg 1974), which is what makes the free many-sorted algebra the natural home for an exact statement. The forward direction organizes the regular languages into a $\mathrm{Reg}$-algebra and instantiates the closure properties of CVCL20; the converse gives a constructive, syntactic procedure — from a recognizing homomorphism it builds a regular expression denoting the language — generalizing Lemma 2.5.7 of Gécseg–Steinby, itself descended from McNaughton–Yamada.

The paper is new (June 2026) and has no machine-checked proof. This mission produces the first formalization: a reusable Lean development of finite many-sorted universal algebra — signatures, algebras, free term algebras and their universal property, the Artinian subterm order, power algebras, recognizability, and the substitution/iteration calculus — together with the two inclusions and the state-elimination argument. Everything below the §4 headline results is infrastructure of independent value for many-sorted formal language theory.

Difficulty

The converse inclusion is the substance. The single-sorted proof eliminates automaton states one at a time along a single axis; the naive port to the many-sorted case — fix a linear order on all states and eliminate — loses track of the sort at which each elimination happens and does not terminate cleanly. The argument instead carries a sortwise budget: an $S$-sorted family $K \le N$ recording, for each sort $t$, the set $K_t$ of state values still admissible at internal subterms. The induction is on $\lVert\lVert K\rVert\rVert = \sum_{s\in S} k_s$, and each step removes the top state of one chosen sort, so the recursion branches over the sorts whose budget is nonzero and the key identity (Equation (E)) is a union over those sorts. The inductive invariant — the family of auxiliary languages $L_u(C,K,l)$ with its budget bookkeeping — is what separates the many-sorted argument from its ancestor; it is also the part Gécseg–Steinby declare "obvious from the construction" and this proof spells out in full (Claims C1–C6).

Formalization scope

Proposed Lean representation: $S$ a type with [Fintype S]; an $S$-sorted set as S → Type; a signature as a family List S → S → Type with finiteness where the theorems need it; the free algebra as an inductive term type; the power algebra with sort-$s$ carrier Set (T_Σ Z s); $s$-recognizability as the existence of a finite $\Sigma$-algebra, a homomorphism, and a subset whose sortwise preimage is the language. Committed conventions: $S$ finite throughout; $\Sigma$ finite and $X$ finite for the §4 results (so that only finitely many basic terms exist and the budget induction is well-founded); the regular operations are exactly $\{\varnothing, +, (\cdot)^{\star z}, z\text{-subst}\}$ together with the operations of $\Sigma$ — not an unrestricted Boolean or closure algebra, which would trivialize the statement.

A complete development needs: the many-sorted UA core (sorted sets and maps, signature, algebra, homomorphism, subalgebra, congruence); the free algebra with unique readability (Proposition 3.4) and universal property (Proposition 3.5); the Artinian subterm order (Proposition 3.6); the power algebra; recognizability and $s$-recognizability with the CVCL20 closure results (Propositions 3.29, 3.30, 3.33); the substitution and iteration calculus (Lemmas 3.23, 3.25, 3.28, Corollary 3.17, Lemma 3.18); and the §4 regular-expression layer (Definition 4.1, Proposition 4.3, Corollary 4.4, Definition 4.6). The UA core and the substitution calculus are reusable beyond this mission. Contributions are welcome at every level — the definitions, the closure results, the auxiliary claims C1–C6, and either inclusion.

Selected references

• L. Gong, R. Ruiz Mora, N. Sanmartín Vich, E. Cosme Llópez, A Kleene theorem for free many-sorted algebras, 2026.
• J. Climent Vidal, E. Cosme Llópez, Congruence-based proofs of the recognizability theorems for free many-sorted algebras, Journal of Logic and Computation 30(2) (2020), 561–633. https://arxiv.org/abs/1808.08217
• F. Gécseg, M. Steinby, Tree Automata, Akadémiai Kiadó, Budapest, 1984.
• R. McNaughton, H. Yamada, Regular expressions and state graphs for automata, IRE Transactions on Electronic Computers EC-9 (1960), 39–47.
• S. C. Kleene, Representation of events in nerve nets and finite automata, in Automata Studies, Princeton University Press, 1956, 3–42.
• J. Mezei, J. Wright, Algebraic automata and context-free sets, Information and Control 11 (1967), 3–29.
• S. Eilenberg, Automata, Languages, and Machines, Vol. A, Academic Press, New York, 1974.

Arithmetic relations among elliptic-function values

Formalization status, 29 September 2026: the main theorem and all nine linked milestones are Proved, with zero Open leaves. The selected proof uses the now-Proved Philippon Theorem 2.1 and the completed Weierstrass application bridges. The linked statements retain their explicit formalization conventions and intermediate variants.

Algebraic independence measures whether several complex numbers satisfy a polynomial relation with rational coefficients. For two numbers, independence means that no nonzero polynomial in two variables vanishes at that pair. This is stronger than asking that each number separately be transcendental: two transcendental numbers can still satisfy a polynomial relation with each other. The distinction matters when describing the arithmetic information carried jointly by periods, lattice invariants, and values of analytic functions.

The completed target is Theorem 1 of Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions (2026). It concerns ten numbers attached to a complex lattice and two evaluation points. The conclusion selects an algebraically independent pair from those ten entries; it does not specify that the pair must consist of two particular function values. The mathematical result is published, and this mission now supplies its checked Lean proof. A source comparison on 29 September 2026 checked the main theorem’s hypotheses, ten values, full-period quasi-period normalization and pair-independence conclusion. The main statement needs no correction.

A lattice and its canonical functions

Take complex numbers $\omega_1,\omega_2$ that are linearly independent over the real numbers. Their integer linear combinations form the period lattice

$$\Omega=\mathbb Z\omega_1+\mathbb Z\omega_2.$$

The formal representation is Mathlib's PeriodPair. Its lattice determines the Weierstrass elliptic function $\wp$ and invariants $g_2,g_3$, using Mathlib's existing definitions. Thus the lattice, function, and invariants are linked by their construction; they are not unrelated parameters.

The Weierstrass zeta function is fixed by the lattice series

$$\zeta_\Omega(z)=\frac1z+\sum_{\lambda\in\Omega\setminus\{0\}} \left(\frac1{z-\lambda}+\frac1\lambda+\frac{z}{\lambda^2}\right).$$

This is the normalization in DLMF equation 23.2.5. For a lattice element $\omega$, its quasi-period is represented by

$$\eta_\Omega(\omega)=\zeta_\Omega(\omega_1/2+\omega)-\zeta_\Omega(\omega_1/2).$$

Both arguments lie outside the lattice. Relating this fixed increment to the increment at an arbitrary regular point is part of the established analytic infrastructure. The normalization concerns the full period $\omega$; references using half-periods require the corresponding factors of two, as in DLMF equation 23.2.11.

Formalization targets

Theorem 1: an algebraically independent pair

Let $\omega\ne0$ belong to $\Omega$. Suppose $u_1,u_2,\omega$ are linearly independent over $\mathbb Q$ and

$$(\mathbb Z u_1+\mathbb Z u_2)\cap\Omega=\{0\}.$$

Define the indexed tuple

$$V=(g_2,g_3,\omega,\eta_\Omega(\omega),u_1,u_2, \wp(u_1),\zeta_\Omega(u_1),\wp(u_2),\zeta_\Omega(u_2)).$$

The proved conclusion is

$$\exists i,j\in\{0,\ldots,9\},\quad i\ne j\quad\text{and}\quad (V_i,V_j)\text{ is algebraically independent over }\mathbb Q.$$

These are the hypotheses and conclusion of the paper's Theorem 1. No algebraicity assumption is imposed on $g_2$ or $g_3$, and the conclusion does not assert independence of all ten entries.

Equations (5) and (6): supporting addition identities

The initial supporting targets are the two identities used in §4 of the paper. For $z,v,z+v\notin\Omega$, write $\Delta=\wp(v)-\wp(z)$. They assert

$$2\Delta\zeta_\Omega(z+v) =2(\zeta_\Omega(z)+\zeta_\Omega(v))\Delta+\wp'(v)-\wp'(z),$$

and

$$4\Delta^2\wp(z+v) =-4(\wp(z)+\wp(v))\Delta^2+(\wp'(v)-\wp'(z))^2.$$

The statements preserve the paper's multiplied-out forms. They do not require $\Delta\ne0$. These targets supply reusable identities; proving them alone does not establish the arithmetic conclusion of Theorem 1.

Nine completed milestones

Milestone	Linked result
Equation (5) — zeta addition identity	Proved
Equation (6) — elliptic addition identity	Proved
Lemma 6 — entire regularization and interpolation bounds	Proved
Lemma 8 — bounded auxiliary polynomial (formal-grid variant)	Proved
Appendix A.2 — Weierstrass model realization (application bridge)	Proved
Appendix A.2 / Lemma A.1 — subgroup degrees (application bridge)	Proved
Proposition A.1 — zero estimate on the mission’s rank-one grid	Proved
Lemma 9 — bounded-order nonvanishing on the enlarged grid	Proved
Lemma 10 — nonzero small arithmetic elements (linear-degree variant)	Proved

The grid and degree variants are described in the linked statements. The two application bridges identify the Weierstrass objects with the general group-theoretic objects used by Philippon’s theorem.

What the completed formalization establishes

The completed goal certifies that every period pair and every triple satisfying the stated hypotheses yields an independent pair in the precise ten-entry tuple. In particular, a proof must handle arbitrary complex lattice invariants and arbitrary admissible evaluation points. A result for a preferred lattice, algebraic arguments, or a predetermined choice of indices would leave the requested statement unresolved.

The definitions provide a reusable interface for elliptic zeta values: a canonical series, a fixed quasi-period convention, and an explicit finite-family independence predicate. The main theorem and all nine milestones have checked proofs; the theorem pages record their accepted submissions and dependencies.

Analytic identities and arithmetic independence

The central difficulty in the proof is passing from identities of analytic functions to exclusion of rational polynomial relations among selected complex values. Periodicity and the addition identities describe how values are related, but do not by themselves rule out algebraic dependence. Consequently, finishing the elementary function interface is only one part of the development.

The development also addresses a concrete analytic obligation in the chosen representation. An infinite-sum expression is a total Lean term even before summability is proved. Using it as the canonical analytic zeta function requires the appropriate convergence and differentiation results. The classical convergence statement is recorded in DLMF §23.2(ii); it is not introduced as an extra hypothesis of the main theorem.

Formalization scope and conventions

All custom declarations use the namespace WeierstrassEllipticZeta. The lattice intersection is an equality of $\mathbb Z$-submodules of $\mathbb C$. Rational linear independence and real linear independence have different roles: the first constrains the three inputs to the theorem, while the second is built into the period pair. Neither is replaced by numerical noncollinearity checks or approximate arithmetic.

The ten values form a Fin 10 family. The selected pair uses Mathlib's AlgebraicIndependent over $\mathbb Q$, so repeated numerical values cannot supply an independent pair merely by occupying different indices. The existing assumptions imply that both evaluation points are outside the lattice; no extra exclusion hypothesis is needed for the goal. Supporting addition identities state their pole exclusions explicitly because Lean's totalized division also assigns values at zero denominators.

The linked intermediate targets identify the variants sufficient for the completed main proof: Lemma 8 uses the stated formal-grid formulation; Proposition A.1 concerns the mission’s rank-one grid; and Lemma 10 uses linear coordinate-degree bounds rather than the source’s sharper O(N/log N) bounds. These distinctions are explicit in the milestone statements. They do not add assumptions to the main theorem. Further contributions can simplify the checked proofs, improve these intermediate bounds, or extend the general results beyond the existing mission target.

Extensions beyond the paper

Theorem 1 with only individual pole exclusions is an Open follow-up target. It retains the same nonzero period, rational linear independence, and ten-entry algebraic-independence conclusion, while replacing the lattice-intersection hypothesis with $u_1,u_2\notin\Omega$.

This extension is an additional deduction to formalize, not a numbered result of the paper, and no mathematical novelty is claimed. Its planned proof combines the completed Theorem 1 with a separate Chudnovsky period theorem and an arithmetic lemma recovering the quasi-period of an integer combination. These additional dependencies remain to be formalized. The mission's completed main goal and nine paper-related milestones continue to record the original scope.

Selected references

• Senthil Kumar K, Algebraic independence of values of Weierstrass elliptic and zeta functions, Proceedings of the Edinburgh Mathematical Society, published online 17 June 2026, pp. 1–33. DOI. Target: Theorem 1; supporting identities: §4, equations (5) and (6).
• NIST Digital Library of Mathematical Functions, Chapter 23, §23.2: Definitions and Periodic Properties, accessed 4 September 2026. Zeta normalization: equation 23.2.5; quasi-period convention: equation 23.2.11.
• Mathlib contributors, Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass, pinned revision 0df444a360eaa60ab8c11dca51a86af692955474 (Lean 4.33.1).