All missions

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. They proved it for strictly convex spaces, whose unit sphere consists of one-point faces. Angosto, Kadets and Zavarzina (2019) proved it, in the stronger two-space form, when the unit sphere is a union of finite-dimensional polyhedral extreme subsets: then every nonexpansive bijection from the unit ball of any Banach space onto that ball is an isometry. This mission formalizes a theorem that removes the polyhedrality: it suffices that every point of the sphere lies in some finite-dimensional face, of any shape, for instance a round disc. The results come from an unpublished research project on the plasticity problem.

Setting

$X$ and $Y$ are real normed spaces with closed unit balls $B_X,B_Y$ and unit spheres $S_X,S_Y$; the covering and plasticity forms assume them complete. A sphere face of $B_Y$ is a nonempty convex set $C\subseteq S_Y$ that is an extreme subset of $B_Y$: if a point of $C$ lies in the open segment between two points of $B_Y$, both points lie in $C$. Its dimension is that of its affine hull; $\partial C$ and $\operatorname{ext}C$ are its relative boundary and its extreme points. $F\colon B_X\to B_Y$ is a nonexpansive bijection; nothing is assumed about the continuity of $F^{-1}$.

Target

$$\text{(F17)}\quad C\ \text{a finite-dimensional sphere face of}\ B_Y\ \Longrightarrow\ D=F^{-1}(C)\ \text{is a compact sphere face of}\ B_X\ \text{with}\ \dim D=\dim C,$$ $$F^{-1}(-C)=-D,\quad F^{-1}(\partial C)=\partial D,\quad F^{-1}(\operatorname{ext}C)=\operatorname{ext}D,\quad F(tD)=tC\ (0\le t\le1).$$ $$\text{(F17, covering form; goal)}\quad X,Y\ \text{Banach},\ S_Y\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ F\ \text{is the restriction of a surjective linear isometry}\ X\to Y.$$ $$\text{(F17, plasticity)}\quad X\ \text{Banach},\ S_X\ \text{covered by finite-dimensional sphere faces}\ \Longrightarrow\ B_X\ \text{is plastic}.$$

Significance

The result. For a polytope face, the relative boundary is a finite union of smaller polytopes, so an induction on dimension keeps the preimage of the boundary compact; this is the step of Angosto–Kadets–Zavarzina that needs polyhedrality. For a curved face the boundary has a continuum of extreme points, and the inverse map, not known to be continuous, could a priori scatter their preimages. The new step traps the whole boundary preimage in one compact face: the preimage of a relative-interior point is shown to lie strictly between any boundary preimage and another one, by following a path across the scaled boundary, which the induction hypothesis covers exactly. Spaces such as $\ell_p$-sums of a Euclidean space with a three-dimensional space whose ball is a cylinder have only finite-dimensional faces, some of them discs, and are covered by the new theorem but not by the polyhedral one or by strict convexity.

Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. The covering form ends with the project's theorem that a nonexpansive surjection between unit balls mapping the sphere into the sphere is linear, already formalized (card Plasticity.U10); this is the only step that uses completeness.

Difficulty

No regularity of the inverse map, no strict convexity, polyhedrality or separability is assumed, the face theorem does not assume completeness, and the faces may have any finite dimension. The topology needed is classical but absent from Mathlib: invariance of domain and of dimension, and the impossibility of retracting a ball onto its boundary sphere.

Formalization scope

Real scalars. Faces are expressed with Mathlib's IsExtreme, dimensions as Module.finrank ℝ (vectorSpan ℝ C), relative boundaries as intrinsicFrontier ℝ C (definitions Plasticity_Faces). A ball map is a function F : X → Y constrained on the closed unit ball by Set.BijOn and LipschitzOnWith 1; the preimage of $C$ is closedBall 0 1 ∩ F ⁻¹' C. The plasticity form uses HasPlasticUnitBall (definitions Plasticity_Basic). Statements are not to be weakened by assuming continuity of the inverse, polyhedrality or a bound on the face dimensions. Published inputs (the basic facts of Zavarzina's Theorem 2.3, invariance of dimension, no retraction) are separate cards.

Selected references

• C. Angosto, V. Kadets, O. Zavarzina, Non-expansive bijections, uniformities and polyhedral faces, J. Math. Anal. Appl. 471 (2019), arXiv:1808.08534.
• B. Cascales, V. Kadets, J. Orihuela, E. J. Wingler, Plasticity of the unit ball of a strictly convex Banach space, RACSAM 110 (2016), 723–727.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• H. Freudenthal, W. Hurewicz, Dehnungen, Verkürzungen, Isometrien, Fund. Math. 26 (1936), 120–122.
• L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912).

Motivation

Exact vacuum solutions of Einstein's equations are the reference objects of classical general relativity: Minkowski space (flat spacetime), the Schwarzschild solution (1916, static spherically symmetric vacuum) and the Kerr solution (1963, stationary axisymmetric vacuum) are the metrics against which every statement about gravitational fields, black holes and gravitational waves is calibrated. Each of them is written in several coordinate systems, and the catalogue literature (Müller–Grave, Catalogue of Spacetimes, arXiv:0904.4184; Visser, The Kerr spacetime: a brief introduction, arXiv:0706.0622) lists these forms side by side. The verification that a given coordinate expression is Ricci-flat, and that two expressions of the same solution are related by an explicit coordinate change, is routinely delegated to computer algebra and is almost never printed.

Timeline: Schwarzschild (1916) found the static solution; Eddington (1924) and Finkelstein (1958) gave the coordinates regular across $r=2M$; Kerr (1963) found the rotating solution in the ingoing form used here; Boyer and Lindquist (1967) introduced the coordinates of the standard form. A previous Prove2Me mission (Kerr Vacuum Solution Verification in Boyer–Lindquist Coordinates, root KerrBL.vacuum_Kerr, 21 theorems, all Proved) established the coordinate Ricci-flatness of the Boyer–Lindquist form; this mission reuses two of its published theorems and two of its definition bundles unchanged (the remaining nodes stay their platform-side dependencies).

Setting

A coordinate point is $x=(x_0,x_1,x_2,x_3)\in\mathbb R^4$ (in Lean, a function $\{0,1,2,3\}\to\mathbb R$). A coordinate metric is a $4\times4$ matrix $g=(g_{ij})$ of real functions of $x$; a candidate inverse $\hat g$ is another such matrix. The slice derivative $\partial_i f(x)$ is the derivative of $u\mapsto f(x[x_i:=u])$ at $u=x_i$; on the open domains used here every slice is $C^\infty$, so $\partial_i$ is the genuine derivative. With

$$\Gamma^a_{bc}=\tfrac12\sum_k\hat g^{ak}\big(\partial_c g_{kb}+\partial_b g_{kc}-\partial_k g_{bc}\big),\qquad R_{bd}=\sum_i\Big(\partial_i\Gamma^i_{bd}-\partial_d\Gamma^i_{bi}+\sum_j\big(\Gamma^i_{ij}\Gamma^j_{bd}-\Gamma^i_{dj}\Gamma^j_{bi}\big)\Big)$$

(definition bundle Atlas_Core_Basic), the vacuum certificate $\mathrm{VacuumCertificate}(g,\hat g,U)$ for a set $U\subseteq\mathbb R^4$ asserts: $U$ is open and nonempty; $g$ is symmetric on $U$; $\hat g\,g=I$ on $U$; all components of $g$ and $\hat g$ are $C^\infty$ on $U$; at every point of $U$ there is an invertible matrix $E$ with $E^{\mathsf T}gE=\mathrm{diag}(-1,1,1,1)$ (Lorentzian signature, bridged to Mathlib's signature $(3,1)$ of the quadratic form); and every component $R_{bd}$ vanishes on $U$. A coordinate relation $\mathrm{CoordRelation}(g_1,g_2,U,V,\Phi,\Psi,J)$ asserts: $\Psi\circ\Phi=\mathrm{id}$ on $U$, $\Phi\circ\Psi=\mathrm{id}$ on $V$, $\Phi$ maps $U$ bijectively onto $V$, $\Phi$ is $C^\infty$ on $U$ and $\Psi$ on $V$, every entry $J_{ki}(x)$ is the genuine derivative of the slice $u\mapsto\Phi(x[x_i:=u])_k$, and $J^{\mathsf T}(g_2\circ\Phi)J=g_1$ on $U$. Units $G=c=1$, signature $(-,+,+,+)$, $\Sigma=r^2+a^2\cos^2\theta$, $\Delta=r^2-2Mr+a^2$.

These definitions form the registered local definition layer of the project: the pinned Mathlib has no Lorentzian metric, Levi-Civita connection or Ricci tensor, so they are supplied as reviewed coordinate-level definitions on top of Mathlib's deriv, ContDiffOn, Matrix and quadratic-form signature.

Formalization targets

Goal (ExactVacuumAtlas.Release01.main)

$$\begin{aligned} &\mathrm{Cert}(g^{\rm cart}_{\rm Mink},\mathbb R^4)\wedge\mathrm{Cert}(g^{\rm sph}_{\rm Mink},\{r>0,0<\theta<\pi\}) \wedge\forall M\,\mathrm{Cert}(g^{\rm std}_{\rm Schw}(M),\{r>0,r\neq2M,0<\theta<\pi\})\\ &\wedge\forall M\,\mathrm{Cert}(g^{\rm in}_{\rm Schw}(M),\{r>0,0<\theta<\pi\}) \wedge\forall M\,\mathrm{Cert}(g^{\rm out}_{\rm Schw}(M),\{r>0,0<\theta<\pi\})\\ &\wedge\forall M,a\,\mathrm{Cert}(g^{\rm BL}_{\rm Kerr}(M,a),\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}) \wedge\forall M,a\,\mathrm{Cert}(g^{\rm in}_{\rm Kerr}(M,a),\{\Sigma\neq0,\sin\theta\neq0\})\\ &\wedge\mathrm{R1}\wedge\mathrm{R2}\wedge\mathrm{R3}\wedge\mathrm{R4}, \end{aligned}$$

where $\mathrm{Cert}(g,U)$ is $\mathrm{VacuumCertificate}(g,\hat g,U)$ with the explicit candidate inverse $\hat g$ of each row, and R1–R4 are coordinate relations with explicit maps: R1/R2 standard Schwarzschild to ingoing/outgoing Eddington–Finkelstein on $\{r>0,r\neq2M,0<\theta<\pi\}$ with $v=t+r+2M\log\lvert r-2M\rvert$, resp. $u=t-r-2M\log\lvert r-2M\rvert$ (Jacobian determinant $1$; the logarithm is Mathlib's Real.log, for which $\log x=\log\lvert x\rvert$ when $x\neq0$, so one formula covers both sides of $r=2M$); R3 Boyer–Lindquist to ingoing Kerr on $\{\Sigma\neq0,\Delta\neq0,\sin\theta\neq0\}$ with $(t,r,\theta,\varphi)\mapsto(t+r+H_1(r),r,\theta,-\varphi-H_2(r))$, $H_1'=2Mr/\Delta$, $H_2'=a/\Delta$, explicit $H_1,H_2$ for all real $M,a$ (three branches of $M^2-a^2$; Jacobian determinant $-1$); R4 spherical chart $\{r>0,0<\theta<\pi,0<\varphi<2\pi\}$ to $\mathbb R^4\setminus\{y=0,x\ge0\}$ with the usual map (Jacobian determinant $r^2\sin\theta$).

Coverage (ExactVacuumAtlas.Release01.coverage)

For $M>0$ the EF domain contains a point with $r=2M$; for $a^2<M^2$ the Boyer–Lindquist domain contains a point with $\Delta<0$; for $0<M$, $a^2\le M^2$ the ingoing Kerr domain contains a point with $\Delta=0$; at these points all Ricci components vanish. The certified domains are therefore not narrowed to an exterior region.

Signature bridge (ExactVacuumAtlas.sigPos_sigNeg_four)

A Lorentzian $4\times4$ matrix in the frame sense has Mathlib signature $\mathrm{sigPos}=3$, $\mathrm{sigNeg}=1$.

Significance

The result gives machine-checked coordinate Ricci-flatness for the seven standard forms of the three basic vacuum solutions, on explicit open domains whose conditions do not exclude the interior region of Schwarzschild ($0<r<2M$ for $M>0$), either sign of $\Delta$ or negative $r$ for Kerr, the regular-coordinate portion of $r=2M$ with $0<\theta<\pi$ (EF, $M>0$), or the points with $\Delta=0$ at which $\Sigma\neq0$ and $\sin\theta\neq0$ (ingoing Kerr); which of these sets are nonempty depends on the parameters, and the coverage theorem gives sufficient conditions. The Lorentzian signature is verified pointwise. The four coordinate relations are proved as explicit maps with explicit inverses and Jacobians, not as abstract existence statements.

Status: every item of the mission has a kernel-checked proof in the project (axioms propext, Classical.choice, Quot.sound only; no sorry, no native_decide); nothing is open. The mission publishes a finished formalization. What it does not contain: any statement about manifolds, atlases, event horizons, maximal extensions, causal structure or global geometry; any classification claim about four-dimensional vacuum metrics; any coordinate-covariance theorem for the coordinate Ricci tensor; any relation between it and a Mathlib manifold Ricci tensor (which does not exist in the pinned Mathlib). The catalogue is a finite list of seven coordinate representations of three solutions.

Difficulty

The obvious route, a general tensor-calculus library (connection, curvature, pull-back functoriality) over Mathlib manifolds, is unavailable: the pinned Mathlib has no indefinite-metric connection or curvature. Each coordinate representation has a complete formal certificate. The development combines direct coordinate calculations with formally proved parameter specialisations and equality-based reuse: the Cartesian Minkowski, Eddington–Finkelstein and ingoing Kerr rows are verified by direct coordinate calculations; the Boyer–Lindquist row reuses the published KerrBL.ricci_flat_Kerr and KerrBL.ginv_mul_g_Kerr; the standard Schwarzschild row takes its Ricci-flatness from the Boyer–Lindquist result at $a=0$, and the spherical Minkowski row is transported from the standard Schwarzschild certificate at $M=0$, in both cases through proved componentwise equalities of the metric data on the common domain. No coordinate-covariance theorem is used or claimed. The ingoing Kerr row is the hard case: the metric is non-diagonal (the radial coordinate vector is null, $g_{rr}=0$, while for $a\neq0$ the covector $dv$ is not null, since $g^{vv}=a^2\sin^2\theta/\Sigma$), the Ricci components are rational functions whose vanishing holds only modulo $\sin^2\theta+\cos^2\theta=1$, and every derivative must be a genuine derivative, never a default value of deriv. For R3 the antiderivative of $1/\Delta$ has three different closed forms depending on the sign of $M^2-a^2$, all covered without restricting the parameters.

Formalization scope

Lean representation: coordinate metrics on $\mathbb R^4$ as above; ContDiffOn ℝ ∞; Matrix (Fin 4) (Fin 4) ℝ; Mathlib sigPos/sigNeg for the signature bridge. Conventions committed: $G=c=1$, $(-,+,+,+)$, coordinate order $(t\,|\,v\,|\,u,\ r,\ \theta,\ \varphi)$, EF matrix entry $g_{vr}=1$ (from $2\,dv\,dr$), ingoing Kerr entries read off with the half-Hessian convention from Visser eq. (E:K1), $\varphi\in\mathbb R$ (no $2\pi$ identification). No trivialising formalization: every domain is proved nonempty with explicit witnesses; the candidate inverse is verified, never assumed; the Ricci tensor is built from the metric data, not hypothesised.

Reusable infrastructure: the core bundles (Atlas_Core_Basic, Atlas_Core_Certificate, Atlas_Core_Relation), the diagonal-frame criterion isLorentzian_of_diag, the signature bridge sigPos_sigNeg_of_isLorentzian, and the closed-form tables. Welcome contributions (not part of this release): Painlevé–Gullstrand, isotropic, Kruskal–Szekeres, Kerr–Schild and Doran forms; Kasner, pp-waves, Taub–NUT; a coordinate-covariance theorem for the coordinate Ricci tensor.

Selected references

• T. Müller, F. Grave, Catalogue of Spacetimes, arXiv:0904.4184v3 (2010). https://arxiv.org/abs/0904.4184
• M. Visser, The Kerr spacetime: a brief introduction, arXiv:0706.0622 (2007). https://arxiv.org/abs/0706.0622
• R. P. Kerr, Gravitational field of a spinning mass as an example of algebraically special metrics, Phys. Rev. Lett. 11 (1963) 237. https://doi.org/10.1103/PhysRevLett.11.237
• R. H. Boyer, R. W. Lindquist, Maximal analytic extension of the Kerr metric, J. Math. Phys. 8 (1967) 265. https://doi.org/10.1063/1.1705193
• R. M. Wald, General Relativity, University of Chicago Press (1984), eqs. (3.1.30), (3.4.4)–(3.4.5) (cited for the conventions; not independently re-checked by the reviewer).

Motivation

A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; every totally bounded metric space is plastic (Freudenthal–Hurewicz 1936), and Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic. For the sequence space c₀, Leo (2022) proved plasticity of the unit ball of c and, for c₀, under the extra hypothesis that the inverse map is continuous, reducing the general case to a normal form in which the map acts inwardly on each coordinate. This mission formalizes a proof that removes the continuity hypothesis, for c₀(Γ) and c₀₀(Γ) over arbitrary index sets and for nonexpansive bijections between the balls of two spaces sandwiched between c₀₀ and c₀. The results come from an unpublished research project on the plasticity problem.

Setting

For a set $\Gamma$, $\ell_\infty(\Gamma)$ is the space of bounded real functions on $\Gamma$ with the norm $\|x\|=\sup_{i\in\Gamma}|x_i|$; $c_0(\Gamma)$ consists of the $x$ with $\{i:|x_i|\ge\varepsilon\}$ finite for every $\varepsilon>0$, and $c_{00}(\Gamma)$ of the finitely supported $x$. A space between $c_{00}(\Gamma)$ and $c_0(\Gamma)$ is a linear subspace $X$ with $c_{00}(\Gamma)\subseteq X\subseteq c_0(\Gamma)$, with the supremum norm; its closed unit ball is $B_X$. A subspace $Y\subseteq\ell_\infty(\Delta)$ realizes all sign patterns if for every countable $C\subseteq\Delta$ and all signs $\varepsilon_d=\pm1$ ($d\in C$) some $v\in Y$ has $\varepsilon_dv_d>0$ on $C$; $c_0(\Delta)$ does. A signed coordinate bijection is a map $x\mapsto y$ with $y_{\sigma(n)}=\alpha_nx_n$ for a bijection $\sigma\colon\Gamma\to\Delta$ and signs $\alpha_n=\pm1$.

Target

$$\text{(CUB37)}\quad F\colon B_X\to B_Y\ \text{a nonexpansive bijection},\ X=c_{00}(\Gamma)\ \text{or}\ Y\ \text{realizes all sign patterns}\ \Longrightarrow\ F\ \text{is the restriction of a signed coordinate bijection.}$$ $$\text{(CUB35)}\quad \text{the closed unit ball of } c_{00}(\Gamma) \text{ is plastic, for every set } \Gamma.$$ $$\text{(CUB36, goal)}\quad \text{the closed unit ball of } c_0(\Gamma) \text{ is plastic, for every set } \Gamma.$$

Significance

The result. Leo's work reduced plasticity of the unit ball of c₀ to excluding the collapse of a coordinate in a normal form; the unit sphere of c₀ is neither strictly convex nor made of compact faces, and the argument here is the base case of the project's results on c₀-sums of finite-dimensional blocks. The two-space statement CUB37 also shows that for an infinite index set Δ no nonexpansive bijection maps the ball of c₀₀(Γ) onto the ball of c₀(Δ).

Formalizing it. The proofs exist only in the project's notes and were checked by AI referees; a machine-checked proof is the independent confirmation sought. The development needs two classical topological inputs that Mathlib lacks: the theorem of Freudenthal and Hurewicz that a nonexpansive bijection of a compact metric space is an isometry, and a form of invariance of domain in every finite dimension (from Brouwer's fixed-point theorem).

Difficulty

The ball of c₀ is not compact and its unit sphere has large flat faces, so the classical arguments (compactness, strict convexity, smoothness of the norm) do not apply, and no regularity of the inverse map is assumed. The difficulty is concentrated in excluding that the normal form sends a nonzero coordinate to zero.

Formalization scope

Real scalars, arbitrary index sets (no countability or nonemptiness assumed). $\ell_\infty(\Gamma)$ is Mathlib's lp (fun _ : Γ => ℝ) ⊤; $c_0(\Gamma)$ and $c_{00}(\Gamma)$ are submodules of it (definitions Plasticity_SeqSpace), and a ball map is a function on $\ell_\infty(\Gamma)$ constrained on ballIn X by Set.BijOn and LipschitzOnWith 1. CUB35 and CUB36 use HasPlasticUnitBall (definitions Plasticity_Basic) for the submodule types, whose norm is the supremum norm inherited from $\ell_\infty$. Statements are not to be weakened by assuming continuity of the inverse or countable Γ. Published inputs (Freudenthal–Hurewicz, Brouwer or invariance of domain) may be added as separate cards and imported by proof sketches.

Selected references

• B. Cascales, V. Kadets, J. Orihuela, E. J. Wingler, Plasticity of the unit ball of a strictly convex Banach space, RACSAM 110 (2016), 723–727.
• H. Freudenthal, W. Hurewicz, Dehnungen, Verkürzungen, Isometrien, Fund. Math. 26 (1936), 120–122.
• N. Leo, Plasticity of the unit ball of c and c₀, J. Math. Anal. Appl. 507 (2022), arXiv:2106.06276.
• O. Zavarzina, Non-expansive bijections between unit balls of Banach spaces, Ann. Funct. Anal. 9 (2018), arXiv:1704.06961.
• L. E. J. Brouwer, Beweis der Invarianz des n-dimensionalen Gebiets, Math. Ann. 71 (1912).

Motivation

The Cauchy–Riemann operator $\bar\partial=\partial_s+i\,\partial_t$ on $\mathbb{C}$ is the model elliptic operator of symplectic topology: pseudoholomorphic curves solve nonlinear perturbations of $\bar\partial u=0$, and their regularity, compactness and Fredholm theory all start from an $L^p$ a priori estimate for $\bar\partial$. In Hofer–Wysocki–Zehnder's asymptotic analysis of pseudoholomorphic curves in symplectisations, this estimate appears as formula (49): on a disc $B$ of radius $R$, every smooth map $\varphi$ supported in the interior of $B$ satisfies

$$\|\varphi\|_{W^{k,p}(B)}\le M(k,p,R)\,\|\bar\partial\varphi\|_{W^{k-1,p}(B)},\qquad k\ge1,\ p>1 .$$

Hofer–Wysocki–Zehnder cite it from E. M. Stein's Singular Integrals and Differentiability Properties of Functions and from Abbas–Hofer's Holomorphic Curves and Global Questions in Contact Geometry.

This mission formalizes estimate (49), together with the core of the real-variable theory of singular integrals on $\mathbb{R}^d$ from Stein, Chapters I–III, and the $L^2$ and $L^p$ estimates for ar\partial of Abbas–Hofer, § 4.2. None of these results is in Mathlib, which has no Hardy–Littlewood maximal function, no Calderón–Zygmund decomposition, no Marcinkiewicz interpolation theorem and no $L^p$ theory of singular integral operators.

Setting

• $\mathbb{R}^d$ carries Lebesgue measure $m$, and $\|\cdot\|_p$ is the $L^p(\mathbb{R}^d)$ norm for complex-valued functions.
• Maximal function. $Mf(x)=\sup_{r>0}m(B(x,r))^{-1}\int_{B(x,r)}|f|\in[0,\infty]$.
• Weak type. An operator $T$ is of weak type $(q,q)$, $q<\infty$, if $m\{|Tf|>\alpha\}\le(A\|f\|_q/\alpha)^q$ for all $\alpha>0$, and of strong type $(p,p)$ if $\|Tf\|_p\le A\|f\|_p$.
• Truncated singular integrals. For a kernel $K$ on $\mathbb{R}^d\setminus\{0\}$ and $\varepsilon>0$, $T_\varepsilon f(x)=\int_{|y|\ge\varepsilon}f(x-y)K(y)\,dy$.
• Cauchy–Riemann operator. For $\varphi:\mathbb{C}\to\mathbb{C}^n$ and $z=s+it$, $\bar\partial\varphi=\varphi_s+i\varphi_t$ (without the factor $\tfrac12$).
• Sobolev norms of smooth maps on a set $U\subset\mathbb{C}$: $\|\varphi\|_{W^{k,p}(U)}=\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$, where $D^j\varphi$ is the $j$-th derivative.

Formalization targets

Goal: the $W^{k,p}$ estimate for $\bar\partial$ on a disc

For an integer $k\ge1$, $p>1$ and $R>0$ there is $M=M(k,p,R)$ such that for every disc $B\subset\mathbb{C}$ of radius $R$ and every smooth $\varphi:\mathbb{C}\to\mathbb{C}^n$ supported in the interior of $B$, $\|\varphi\|_{W^{k,p}(B)}\le M\|\bar\partial\varphi\|_{W^{k-1,p}(B)}$ (Hofer–Wysocki–Zehnder I, estimate (49), p. 366).

Milestones

1. Maximal theorem. $Mf$ is finite a.e. for $f\in L^p$, $1\le p\le\infty$; $M$ is of weak type $(1,1)$ and of strong type $(p,p)$ for $1<p\le\infty$ (Stein I, § 1.3, Theorem 1).
2. Calderón–Zygmund decomposition. A non-negative integrable $f$ and a height $\alpha>0$ give $\mathbb{R}^d=F\cup\Omega$ with $f\le\alpha$ a.e. on $F$ and $\Omega$ a union of cubes with disjoint interiors on which the average of $f$ lies in $(\alpha,2^d\alpha]$ (Stein I, § 3.2, Theorem 4).
3. Marcinkiewicz interpolation theorem. A sub-additive operator of weak types $(1,1)$ and $(r,r)$, $1<r\le\infty$, is of strong type $(p,p)$ for $1<p<r$ (Stein I, § 4.2, Theorem 5).
4. Convolution kernels with bounded Fourier transform. If $K\in L^2$, $|\hat K|\le B$ and $|\nabla K(x)|\le B|x|^{-d-1}$, then $f\mapsto K*f$ is bounded on $L^p$, $1<p<\infty$, with a constant depending only on $p$, $B$, $d$ (Stein II, § 2.2, Theorem 1).
5. Truncated singular integrals. If $|K(x)|\le B|x|^{-d}$, $\int_{|x|\ge2|y|}|K(x-y)-K(x)|\,dx\le B$ and $K$ has integral zero over every annulus, then the truncations $T_\varepsilon$ are bounded on $L^p$ uniformly in $\varepsilon$ and converge in $L^p$ as $\varepsilon\to0$ (Stein II, § 3.2, Theorem 2).
6. Homogeneous kernels. The same conclusion for $K(y)=\Omega(y)/|y|^d$ with $\Omega$ homogeneous of degree $0$, of mean zero on the unit sphere and Dini-continuous there (Stein II, § 4.2, Theorem 3 (a), (b)).
7. The Cauchy–Riemann estimate on the plane. $\|\partial_1f\|_p+\|\partial_2f\|_p\le A_p\|\partial_1f+i\partial_2f\|_p$ for compactly supported $C^1$ functions $f:\mathbb{R}^2\to\mathbb{C}$, $1<p<\infty$ (Stein III, § 1.3, Proposition 4).
8. $L^2$ identity. $\|\bar\partial\varphi\|_{L^2}^2=\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2$ for smooth compactly supported $\varphi:\mathbb{C}\to\mathbb{C}^n$ (Abbas–Hofer, § 4.2, (4.4)).
9. $L^2$ estimate on a disc. $\|\varphi_s\|_{L^2}^2+\|\varphi_t\|_{L^2}^2+\|\varphi\|_{L^2}^2\le(4R^2+1)\|\bar\partial\varphi\|_{L^2}^2$ for $\varphi$ with compact support in $B_R(0)$ (Abbas–Hofer, Theorem 4.2.1).
10. $L^p$ estimate on a disc. $\|\varphi\|_{W^{1,p}}\le c(p,R)\|\bar\partial\varphi\|_{L^p}$ for $\varphi$ with compact support in $B_R(0)$, $1<p<\infty$ (Abbas–Hofer, Theorem 4.2.2).

Significance

The result. The $W^{k,p}$ estimate for $\bar\partial$ is the analytic input behind elliptic bootstrapping for pseudoholomorphic curves: interior regularity, $C^\infty$ bounds from gradient bounds, removal of singularities, and the Fredholm theory of linearized Cauchy–Riemann operators on Sobolev spaces. In Hofer–Wysocki–Zehnder's work it controls the derivatives of pseudoholomorphic half-cylinders near a nondegenerate periodic orbit.

Formalizing it. The milestones from Stein are the standard real-variable toolkit of harmonic analysis on $\mathbb{R}^d$: the maximal theorem, the Calderón–Zygmund decomposition, Marcinkiewicz interpolation and the $L^p$ theory of singular integrals with smooth or homogeneous kernels. None of them is in Mathlib, and each is reusable well beyond this mission, for instance for elliptic estimates of other operators, Sobolev embeddings in $L^p$, and other $L^p$ estimates.

Difficulty

The statements are quantitative and the order of quantifiers matters: the constants are chosen before the functions, and in milestones 3 and 4 also before the operator or the kernel, with the dependence stated by the source. Several objects take infinite values or are defined only almost everywhere: the maximal function is valued in $[0,\infty]$, the case $r=\infty$ of the interpolation theorem uses a strong-type bound in place of a weak-type one, and the singular integrals are limits in $L^p$ of absolutely convergent truncated integrals. The Dini condition on $\Omega$ is a condition on a supremum over pairs of points of the unit sphere. The Cauchy–Riemann statements involve vector-valued maps $\mathbb{C}\to\mathbb{C}^n$, real derivatives of all orders and Sobolev norms on discs.

Formalization scope

• Namespace DbarRegularity. The definition module DbarRegularity_Setting defines maximalFunction, closedCube, dbar and sobolevNorm. The mission is standalone and imports no definitions from other missions.
• Spaces. $\mathbb{R}^d$ is EuclideanSpace ℝ (Fin d) with volume, functions on it are complex-valued, $\mathbb{R}^2$ in milestone 7 is EuclideanSpace ℝ (Fin 2), and $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Stein's dimension is written $d$ throughout, and $n$ is the dimension of the target $\mathbb{C}^n$.
• Norms and exponents. $L^p$ norms are eLpNorm in ℝ≥0∞. Exponents $1<p<\infty$ are real and enter as ENNReal.ofReal p; exponents allowed to be infinite are in ℝ≥0∞. Constants are in ℝ≥0 or ℝ, never in ℝ≥0∞.
• Derivatives. $\varphi_s$, $\varphi_t$ are fderiv ℝ φ z 1, fderiv ℝ φ z Complex.I; smoothness is ContDiff ℝ ∞ ($C^\infty$, not analytic); higher derivatives are iteratedFDeriv ℝ j. Supports are tsupport.
• Limits. Limits as $\varepsilon\to0$ are along 𝓝[>] 0, in the $L^p$ seminorm.

Contributions welcome: reusable general lemmas of real-variable harmonic analysis on $\mathbb{R}^d$, and calculus lemmas for smooth compactly supported maps on $\mathbb{C}$.

Selected references

• E. M. Stein, Singular Integrals and Differentiability Properties of Functions, Princeton Mathematical Series 30, Princeton University Press (1970), Chapters I–III. ISBN 0-691-08079-8.
• C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser Advanced Texts Basler Lehrbücher, Birkhäuser (2019), § 4.2. https://doi.org/10.1007/978-3-030-11803-7
• H. Hofer, K. Wysocki, E. Zehnder, Properties of pseudoholomorphic curves in symplectisations I: asymptotics, Ann. Inst. H. Poincaré Anal. Non Linéaire 13(3) (1996), 337–379. http://www.numdam.org/item/AIHPC_1996__13_3_337_0/
• A. P. Calderón, A. Zygmund, On the existence of certain singular integrals, Acta Math. 88 (1952), 85–139. https://doi.org/10.1007/BF02392130

Prove2Me mission category: Textbook.

Reusable fast matrix multiplication

Matrix multiplication is often a component of a larger computation. A useful verified routine must return the right product, preserve its caller's data, and bound the work performed by the same returning call. Strassen's algorithm reduces the number of recursive block products from eight to seven, obtaining a subcubic arithmetic bound. This mission connects that algorithm to a mutable array implementation and a reusable Lean contract.

The reference is Introduction to Algorithms (CLRS), fourth edition, Chapter 4, §4.2: Strassen's algorithm for matrix multiplication. CLRS, fourth edition. The underlying algorithm is an established result originating in Strassen's 1969 paper.

Matrices, returned product, and measured work

A matrix is represented by an array of row arrays, written Seq[Seq[Int]]. Each row contains unbounded mathematical integers. Let $k\in\mathbb N$ be the recursion depth and $n=2^k$ the matrix dimension. The mathematical input values are functions $A,B:\mathbb Z\to\mathbb Z\to\mathbb Z$; only their entries inside the $n\times n$ square enter the product.

A heap $h$ stores mutable rows, outer arrays, objects, and named natural-number counters. The predicate MatrixHeap.Stored h a A connects an allocated outer-array reference $a$ to its row contents $A$. Both input arrays must satisfy this representation predicate. Input matrices and their rows may share references, including sharing between the two inputs.

A Call contract supplies a finite execution in the generated semantics: for every suspended caller stack, strassen.Call returns the same result reference $r$ and final heap $h'$. All correctness, preservation, and work conclusions below concern that same $h'$ and $r$.

The counted work $T$ sums the increments of four source clocks: products for scalar leaf products, calls for all Strassen invocations (including the initial call), linear_cells for entrywise combinations, and copied_cells for entries copied during quadrant extraction and joining. Each increment has unit weight. Initial counters may be nonzero; the bound concerns additional work.

Formalization targets

The main correctness-and-running-time theorem already has an accepted proof on Prove2Me under Lean 4.33.1. Its name is CLRS.Chapter4Publication.Strassen.correctness_and_running_time.

For every represented input of dimension $n=2^k$, the contract supplies a finite returning call whose output matrix $R$ satisfies

$$R_{ij}=\sum_{t=0}^{n-1} A_{it}B_{tj}\quad(0\le i,j<n), \qquad R_{ij}=0\quad\text{outside this square}.$$

Every previously allocated row, outer array, and object is preserved. The result's outer array is fresh, and its $n$ in-square rows are fresh and pairwise distinct. One positive natural constant is chosen before all depths, heaps, and matrix inputs:

$$\exists C>0,\quad \forall\text{ represented inputs with }n=2^k,\quad \exists\text{ a correct returning call with }7^k\le T\le C7^k.$$

Thus the main proposition leaves the upper constant available for improvement. The accepted proof supplies $C=13$. On the permitted dimensions this gives the conventional $\Theta(n^{\log_2 7})$ counted-work bound. The checked headline states natural-power inequalities, rather than a real-logarithm asymptotic relation over arbitrary dimensions.

The exact counter schedule is stronger than the displayed upper bound. Writing $Q_0=1$, $Q_{k+1}=1+7Q_k$, $H_0=0$, and $H_{k+1}=4^k+7H_k$, the four increments are

$$\Delta\mathrm{products}=7^k,\quad \Delta\mathrm{calls}=Q_k,\quad \Delta\mathrm{linear\_cells}=18H_k,\quad \Delta\mathrm{copied\_cells}=12H_k.$$

All other clocks remain unchanged. Consequently the total satisfies $T(0)=2$ and $T(k+1)=7T(k)+30\cdot4^k+1$. These are properties of the existing combined contract and its supporting definitions, rather than additional open targets.

What callers can reuse

A later algorithm can invoke the multiplication routine with its existing heap and counters and use the established product, preservation, freshness, and work guarantees. Fresh independent output rows permit subsequent row updates without aliasing another in-square output row or an input row. The surrounding algorithm still proves its own input representation and any new conclusions; it can reuse this multiplication analysis unchanged.

The source development contains the matrix algebra, mutable execution analysis, and exact clock summaries. The contribution is their connection in one importable contract. The mission reuses the published theorem and its existing dependencies. Alternative checked proofs, improved constants, and verified client examples can build on that result.

Where the formalization is demanding

The seven-product identity alone does not establish that a mutable program returns the product. Quadrant copies, intermediate combinations, allocations, and possible input sharing must agree with the mathematical matrices. Equal row contents do not imply independent row references.

Counting only scalar leaf products also omits copying and combination work. A numerical recurrence by itself does not supply a returning program execution. The contract must connect those charges and the returned values to the same finite call while preserving caller storage.

Formalization scope and source

The .algo implementation follows the seven recursive products and block recombination of CLRS §4.2, making quadrant copies and result allocation explicit. The complete source file is shown below.

Sequences are total over integer indices. Stored requires an allocated row at every integer row index, including indices outside the finite square. In a fixed heap only finitely many distinct whole row sequences can be represented; out-of-square rows may share storage. The contract does not assume the desired product, an existing transcript, or an unverified runtime bound. Its execution conclusion is an existential returning-call guarantee; the headline alone does not quantify over every possible execution.

Depth zero gives dimension one and $T=2$. Dimension zero, other dimensions, rectangular multiplication, and automatic padding are outside this contract. Freshness and pairwise distinctness of output rows apply to the finite square. The cost model excludes allocation, uncharged bookkeeping, total generated transition counts, elapsed time, and integer bit complexity. Multiplication by sign in a linear combination is charged to linear_cells, not products.

The exact compiler/source snapshot is fd33cf959b39f9e4a9fcfda4ef31d5a36b784d41, an Algo2Lean development snapshot distinct from public v0.1.4. The repository pins Lean 4.26.0; the accepted platform declarations use Lean 4.33.1 with Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. The publication record records the source and adaptation checks. Platform packaging uses the CLRS namespace and adapted imports. Source generation, declaration comparison, and Lean proof checking are separate checks; the compiler itself has no formal semantics-preservation proof.

examples/matrix_strassen.algo

# Strassen multiplication with correctness and Θ(n^(log₂ 7)) counted work for n = 2^k (CLRS 4.2).
# Preconditions: n = 2^depth for a natural depth; inputs have arbitrary Int entries.
# Every finite output row is fresh. Input matrices and their rows are never modified.

def matrix_linear_row(a: Seq[Int], b: Seq[Int], count: Int, sign: Int) -> Seq[Int]:
    c = const(0)
    i = 0
    # @loop
    while i < count:
        c[i] = a[i] + sign * b[i]
        tick("linear_cells")
        i += 1
    return c


def matrix_linear(a: Seq[Seq[Int]], b: Seq[Seq[Int]], count: Int, sign: Int) -> Seq[Seq[Int]]:
    c: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < count:
        c[i] = matrix_linear_row(a[i], b[i], count, sign)
        i += 1
    return c


def matrix_quadrant_row(a: Seq[Int], h: Int, column: Int) -> Seq[Int]:
    c = const(0)
    i = 0
    # @loop
    while i < h:
        c[i] = a[column + i]
        tick("copied_cells")
        i += 1
    return c


def matrix_quadrant(a: Seq[Seq[Int]], n: Int, h: Int, row: Int, column: Int) -> Seq[Seq[Int]]:
    c: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < h:
        c[i] = matrix_quadrant_row(a[row + i], h, column)
        i += 1
    return c


def matrix_join_row(a: Seq[Int], b: Seq[Int], h: Int) -> Seq[Int]:
    result = const(0)
    i = 0
    # @loop
    while i < h:
        result[i] = a[i]
        result[i + h] = b[i]
        tick("copied_cells", 2)
        i += 1
    return result


def matrix_join(a: Seq[Seq[Int]], b: Seq[Seq[Int]], c: Seq[Seq[Int]], d: Seq[Seq[Int]], h: Int) -> Seq[Seq[Int]]:
    result: Seq[Seq[Int]] = const(const(0))
    i = 0
    # @loop
    while i < h:
        result[i] = matrix_join_row(a[i], b[i], h)
        result[i + h] = matrix_join_row(c[i], d[i], h)
        i += 1
    return result


def strassen(a: Seq[Seq[Int]], b: Seq[Seq[Int]], n: Int) -> Seq[Seq[Int]]:
    tick("calls")
    if n <= 1:
        c: Seq[Seq[Int]] = const(const(0))
        c[0] = const(0)
        c[0][0] = a[0][0] * b[0][0]
        tick("products")
        return c
    else:
        h = n // 2
        a11 = matrix_quadrant(a, n, h, 0, 0)
        a12 = matrix_quadrant(a, n, h, 0, h)
        a21 = matrix_quadrant(a, n, h, h, 0)
        a22 = matrix_quadrant(a, n, h, h, h)
        b11 = matrix_quadrant(b, n, h, 0, 0)
        b12 = matrix_quadrant(b, n, h, 0, h)
        b21 = matrix_quadrant(b, n, h, h, 0)
        b22 = matrix_quadrant(b, n, h, h, h)
        # Seven recursive products replace the ordinary eight.
        p1 = strassen(a11, matrix_linear(b12, b22, h, -1), h)
        p2 = strassen(matrix_linear(a11, a12, h, 1), b22, h)
        p3 = strassen(matrix_linear(a21, a22, h, 1), b11, h)
        p4 = strassen(a22, matrix_linear(b21, b11, h, -1), h)
        p5 = strassen(matrix_linear(a11, a22, h, 1), matrix_linear(b11, b22, h, 1), h)
        p6 = strassen(matrix_linear(a12, a22, h, -1), matrix_linear(b21, b22, h, 1), h)
        p7 = strassen(matrix_linear(a11, a21, h, -1), matrix_linear(b11, b12, h, 1), h)
        c11 = matrix_linear(matrix_linear(matrix_linear(p5, p4, h, 1), p2, h, -1), p6, h, 1)
        c12 = matrix_linear(p1, p2, h, 1)
        c21 = matrix_linear(p3, p4, h, 1)
        c22 = matrix_linear(matrix_linear(matrix_linear(p5, p1, h, 1), p3, h, -1), p7, h, -1)
        return matrix_join(c11, c12, c21, c22, h)

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 4, §4.2. Publisher.
• Volker Strassen, “Gaussian Elimination is Not Optimal,” Numerische Mathematik 13, 354–356, 1969. DOI.
• Algo2Lean, Chapter 4 source and proof development, 2026. Source snapshot. Algo2Lean was created by Lunjia Hu; Chutong Yang is a contributor, and both are software citation authors.

Why short-horizon outcome windows

Randomized experiments (A/B tests) on ride-sharing marketplaces, recommendation systems and digital-health services assign each arriving user to treatment or control. The assignment changes the system state seen by later users, so observations are not independent: this is temporal interference, or carryover. The difference-in-means estimator ignores it, and in Markovian models its bias can be as large as the treatment effect itself (Farias, Li, Peng, Zheng 2022; Hu, Wager 2022). Corrections based on off-policy evaluation or on differences of $Q$-values assume a stationary environment, while real systems have time-varying dynamics and the experimenter observes a single trajectory.

Johari, Peng and Xing propose the truncated policy gradient (TPG) estimator: each instantaneous outcome in the difference-in-means estimator is replaced by the sum of the next $k+1$ outcomes. The paper shows that this estimates, without bias, the derivative of a truncated policy value, and derives bias and variance bounds, a central limit theorem and a consistent variance estimator in nonstationary Markovian environments. This mission formalizes those statements.

Setting

Time is $t=0,1,\dots,T-1$ (the paper's time $t+1$). The state space $S$ is finite and the action $Z_t\in\{0,1\}$ is control or treatment. For each time $t$ and action $z$ there is a transition matrix $P_z^t$ with $\mathbb P(X_{t+1}=x'\mid X_t=x,Z_t=z)=P_z^t(x,x')$; the matrices may change arbitrarily with $t$, which is the nonstationarity. The initial state $X_0$ has distribution $\rho$. The reward $Y_t$ is drawn from a distribution $R(\cdot\mid X_t,Z_t)$ on $\mathbb R$, independently of everything else given $(X_t,Z_t)$, and $R([-M,M]\mid x,z)=1$ for all $x,z$. Write $r(x,z)=\int y\,R(dy\mid x,z)$.

The policy $\pi_\theta$ assigns treatment with probability $\theta$ at every time, independently of everything else. $\pi_1$ is all-treatment, $\pi_0$ is all-control, and the experiment runs $\pi_{1/2}$. Write $P_\theta^t=\theta P_1^t+(1-\theta)P_0^t$ and $\mathbb E_\theta$ for expectation under $\pi_\theta$. The value function and the global average treatment effect (GATE) are

$$J(\theta)=\frac1T\sum_{t=0}^{T-1}\mathbb E_\theta[Y_t],\qquad \tau=J(1)-J(0).$$

The TPG estimator with truncation size $k$ is

$$\widehat\tau_k=\frac1T\sum_{u=0}^{T-1}\Bigl(\frac{\mathbf 1\{Z_u=1\}}{1/2}-\frac{\mathbf 1\{Z_u=0\}}{1/2}\Bigr)\sum_{t=u}^{\min(u+k,\,T-1)}Y_t ,$$

so $\widehat\tau_0$ is the difference-in-means estimator.

Two quantities control the bounds. The mixing assumption (Assumption 1) asks for $\gamma\in(0,1)$ with $\|f'P_z^t-fP_z^t\|_{\mathrm{TV}}\le\gamma\,\|f'-f\|_{\mathrm{TV}}$ for all $t<T$, all $z$ and all probability vectors $f,f'$ on $S$, where $\|f-f'\|_{\mathrm{TV}}=\tfrac12\|f-f'\|_1$. The kernel deviation is $\delta=\max_{t<T}\max_{x}\|P_1^t(x,\cdot)-P_0^t(x,\cdot)\|_{\mathrm{TV}}$.

Formalization targets

Goal: Theorem 1, bias and variance of the TPG estimator

There are absolute constants $C_1,C_2>0$ such that for every environment, every $T\ge1$, every $0\le k\le T$ and every $\gamma\in(0,1)$ and $M$ as above,

$$\bigl|\mathbb E_{1/2}[\widehat\tau_k]-\tau\bigr|\le C_1\Bigl(\frac{1-\gamma^k}{(1-\gamma)^2}\,\delta^2M+\frac{\gamma^k}{1-\gamma}\,\delta M\Bigr),\qquad \operatorname{Var}_{1/2}(\widehat\tau_k)\le C_2\Bigl(\frac{(k+1)^2M^2}{T}+\frac{\gamma\,(k+1)M^2}{T(1-\gamma)}\Bigr).$$

The constants are left unspecified, as in the paper's $O(\cdot)$ statement, so an improvement of the constants does not invalidate the goal.

Explicit constants: Propositions 5 and 6

For data collected under $\pi_\theta$ with $\theta\in(0,1)$, the paper gives both bounds with explicit constants, for the TPG estimator and for a reward-corrected variant. At $\theta=1/2$, Proposition 5 reads

$$\bigl|\mathbb E[\widehat\tau_k]-\tau\bigr|\le\frac{2\delta M\gamma^k}{1-\gamma}+2\delta^2M\,\Psi_k(\gamma),\qquad \operatorname{Var}(\widehat\tau_k)\le\frac{4M^2(k+1)}{T}\Bigl(2k+3+\frac{4\gamma}{1-\gamma}\Bigr),$$

with $\Psi_k(\gamma)=\sum_{j=0}^{k-2}(j+1)\gamma^j$.

Policy-gradient identities: Propositions 1–4

$J$ and its truncated analogue $J_k$ are differentiable at $1/2$, with derivative equal to the horizon average of differences of ($k$-truncated) $Q$-values, and $\mathbb E_\theta[\widehat\tau^{\mathrm{TPG}}_{\theta,k}]$ equals the corresponding derivative for every $\theta\in(0,1)$. Without the mixing assumption, the untruncated estimator satisfies $|\mathbb E[\widehat\tau_T]-\tau|\le C\,T^2\delta^2M$ and $\operatorname{Var}(\widehat\tau_T)\le2M^2(T+1)$.

Asymptotics: Theorem 2, Lemmas 1–5 and Corollary 1

For fixed $k$, under mixing at all times, a positive limit $\sigma_k^2$ of the normalized variance (Assumption 2) and a Cesàro mean-stability condition (Assumption 3),

$$\sqrt T\,\bigl(\widehat\tau_k-\mathbb E[\widehat\tau_k]\bigr)\Rightarrow\mathcal N(0,\sigma_k^2),\qquad \widehat\Omega_T\xrightarrow{p}\sigma_k^2,$$

where $\widehat\Omega_T$ is a Newey–West estimator with bandwidth $L_T\to\infty$, $L_T=O(T^{1/3})$. The supporting statements are a covariance inequality under strong mixing, the bound $\alpha(h)\le\gamma^{h-1}$ on the mixing coefficients of the experimental process and its consequence for the summands of the estimator, the central limit theorem alone, and consistency of the ideal and of the feasible variance estimators.

What the results give

Theorem 1 separates two error sources: a term of second order in $\delta$ that does not grow with $T$, and a term that decays geometrically in $k$. Together with Proposition 2 it shows what truncation buys: a variance bound of order $(k+1)^2/T$ instead of order $T$, at the price of a bias term of order $\gamma^k$. Theorem 2 supplies standard errors for the estimator from a single nonstationary trajectory.

All results of the paper are proved on paper; none has a machine-checked proof. The work of this mission is the formal proofs of the stated results. The definition layer (a finite-state nonstationary Markov decision process with real rewards, its trajectory law under time-varying randomization, total-variation contraction, strong-mixing windows, a Newey–West estimator) can be reused for other results on experiments with Markovian interference.

Where the difficulty lies

The first idea is to bound $|J'(1/2)-(J(1)-J(0))|$ by the second derivative of $J$ on $[0,1]$. Every pair of times contributes to that second derivative, so this route gives the $T^2\delta^2M$ of Proposition 2 and nothing uniform in the horizon. Theorem 1 is uniform in $T$, and its bound has no term of first order in $\delta$ beyond the truncation term; Proposition 5 shows that such a term is present at every allocation $\theta\ne1/2$. Formal proofs have to handle ordered products of time-varying stochastic matrices and signed measures of total mass zero, with a contraction that is assumed one step at a time.

The variance bound and Theorem 2 concern a dependent, non-identically distributed sequence observed once. Mathlib has no central limit theorem for nonhomogeneous Markov chains and no covariance inequality for strongly mixing sequences; the paper relies on Arlotto and Steele (2016) for the former and on an inequality from Doukhan (1994) for the latter.

Formalization scope

TPG.Env S packages $(P,\rho,R)$ for a finite type S. Kernels are real matrices with nonnegative entries and rows summing to one, indexed by all $t\in\mathbb N$; a statement with horizon $T$ uses only the times below $T$. A trajectory is a function Fin T → S × Bool × ℝ, and Env.trajLaw is its law for an arbitrary sequence of treatment probabilities, built as a finite mixture over state and action paths of product reward laws. $J$, $\tau$, $J_k$ and the $Q$-values are defined from this law, and expectations given $\{Z_u=z\}$ are taken under the conditional measure. Rewards are bounded through the hypothesis E.RewardBound M; the standing assumptions of the paper enter each theorem as hypotheses, and S carries the discrete measurable structure.

Statements require $T\ge1$ and $0\le k\le T$, as in the paper. Asymptotic statements compute the law of each statistic under the horizon-$T$ measure: convergence in distribution is tested against bounded continuous functions, and convergence in probability is stated for each $\varepsilon>0$. The limit $\sigma_k^2$ is a parameter constrained by Assumption 2. For $\theta\notin[0,1]$ the law of $\pi_\theta$ is not a probability law and no statement depends on it. The hypotheses are satisfiable for every $T$, $k$ and $\gamma$: an environment with one state and a nonzero constant reward satisfies all of them, including Assumptions 2 and 3, so no statement is vacuous.

Not included: Definition 1 and Lemma 6 of the paper (Dobrushin coefficients and the Arlotto–Steele theorem on general Borel state spaces), the stationary difference-in-$Q$ discussion of Appendix C, the constant-reward example showing that the variance order is attained, and the numerical studies. Formal statements of those, and auxiliary lemmas about Env.trajLaw, ordered matrix products and total-variation contraction, are welcome contributions.

Selected references

• R. Johari, T. Peng, W. Xing, Estimation of Treatment Effects Under Nonstationarity via the Truncated Policy Gradient Estimator, arXiv preprint, 2025–2026. https://arxiv.org/abs/2506.05308
• V. F. Farias, A. A. Li, T. Peng, A. Zheng, Markovian Interference in Experiments, Advances in Neural Information Processing Systems 35, 2022. https://arxiv.org/abs/2206.02371
• Y. Hu, S. Wager, Switchback Experiments under Geometric Mixing, arXiv preprint, 2022. https://arxiv.org/abs/2209.00197
• A. Arlotto, J. M. Steele, A Central Limit Theorem for Temporally Nonhomogeneous Markov Chains with Applications to Dynamic Programming, Mathematics of Operations Research 41(4), 2016. https://doi.org/10.1287/moor.2016.0784
• P. Doukhan, Mixing: Properties and Examples, Lecture Notes in Statistics 85, Springer, 1994. https://doi.org/10.1007/978-1-4612-2642-0

Prove2Me mission category: Textbook.

Reusable minimum spanning forest algorithms

Kruskal builds a cheapest connecting forest by considering edges in weight order and selecting those that join different components. A caller may already have that order, so the cost of sorting should be distinguished from the work that remains. This development provides two callable entry points and two running-time results: the complete algorithm, and the algorithm after sorting.

The .algo implementation closely follows the textbook pseudocode in CLRS. It makes the edge scan, representative tests, edge selection, union by rank, and full path compression explicit. The separate post-sorting entry point lets callers reuse a supplied order without repeating the sorting step.

This mission belongs to the formalization series for Introduction to Algorithms (CLRS), fourth edition: Chapter 21, §21.2 for Kruskal, Theorem 21.1 in §21.1 for safe edges, and Theorem 19.14 in §19.4 for union by rank with path compression. These are established textbook results; the contribution here is their connection to executable-looking source and reusable Lean call contracts. CLRS, fourth edition.

Graph, supplied edge order, and measured work

An undirected weighted graph has vertices 0, …, V−1 and edge identifiers 0, …, E−1. Three integer sequences give each edge's source, target, and weight. Counts are nonnegative, and endpoints lie in the declared vertex range. Edge identifiers distinguish parallel edges. Weights may be negative, and self-loops are permitted.

A minimum spanning forest is an acyclic selection that connects exactly the original graph's connected components and minimizes total weight among all such forests. The returned sequence marks selected identifiers with 1 and every other integer index with 0. For a nonempty connected graph the result is a minimum spanning tree.

The complete entry point is kruskal(size, sources, targets, weights, count). The post-sorting entry point is kruskal_sorted(size, sources, targets, weights, count, order). Its additional sorted order is a permutation of all edge identifiers, in nondecreasing weight order. Equal-weight identifiers may occur in either order; the arrays and output flags retain the original identifiers. The predicate SortIndicesAnalysis.SortedPermutation states this precondition.

A heap stores mutable sequences, objects, collections, and named counters. A Call contract supplies a finite returning execution that can be invoked from another program with its existing heap and counters. Input sequence references must be allocated and may alias. Both entry points preserve all previously allocated caller storage.

Runtime T is the sum of increments of eight natural-number clocks: sort_steps, heap_comparisons, heap_swaps, uf_init, uf_find, uf_compress, uf_union, and kruskal. Each has unit weight. The post-sorting call has zero increments on the three sorting clocks. Let $L(E)=\lfloor\log_2(E+1)\rfloor$ and let $\alpha$ denote the inverse Ackermann function with convention $A_0(r)=r+1$, $A_{k+1}(r)=A_k^{\circ(r+1)}(r)$, and $\alpha(n)=\min\{k>0:A_k(1)>n\}$, where the superscript denotes repeated composition. Its published definition is shared with the data-structure analysis.

Formalization targets

Both main results provide termination, minimum spanning forest correctness, fresh output storage, preservation of caller storage, and a bound on the same call's additional work. Each quantifies one positive constant before all graph inputs and initial heaps.

Entire algorithm, including sorting

$$\exists C>0,\qquad T\le C\bigl(V+1+E L(E)\bigr) \quad\text{for every well-formed graph input.}$$

This is KruskalAnalysis.correctness_and_running_time, with scale KruskalAnalysis.runtimeScale. It gives the conventional total $O(V+E\log(E+1)+1)$ bound; sorting remains charged. The proof absorbs the inverse-Ackermann contribution into the vertex and sorting terms, without requiring connectedness or a density assumption. Thus the total bound has no redundant inverse-Ackermann factor.

After sorting

$$\exists C>0,\qquad T\le C\bigl(V+1+E\alpha(V)\bigr) \quad\text{for every well-formed input and supplied sorted order.}$$

This is KruskalSortedAnalysis.correctness_and_running_time, with scale KruskalSortedAnalysis.runtimeScale. It describes an actual call that skips sorting, including singleton initialization and the entire edge scan. It is not obtained by supplying sorted data to a function that sorts again. The additive unit in both statements covers the empty graph.

The explicit supporting call_contract results retain the budgets

$$T_{\mathrm{sorted}}\le V+2+E\bigl(10\alpha(V)+14\bigr),$$ $$T_{\mathrm{total}}\le 2E\bigl(3L(E)+2\bigr) +V+2+E\bigl(10\alpha(V)+14\bigr).$$

These expressions are the respective runtimeBound definitions. Main statements leave the constant unspecified so improved constants do not change their propositions. The component milestones are independent union-find method contracts, the sorter's permutation/order contract, the post-sorting call contract, and the complete composition.

What callers can reuse

The union-find implementation and its published correctness and inverse-Ackermann analysis are reused unchanged. Its find contract, union contract, and constructor contract apply independently of graphs. They account for the same evolving object's state and amortized potential across calls. Future algorithms can import them without repeating the rank or path-compression analysis. The indexed-heap sorting contract is also reused unchanged.

A caller with its own verified sorted order can invoke kruskal_sorted and receive an allocated, fresh output, its mathematical specification, unchanged caller storage, and the smaller runtime bound. The complete algorithm invokes that same verified entry point after sorting; the two results share the scan and data-structure proofs. Initial counters need not be zero. Ordinary Returns and ReturnsWithCost theorems are convenient views of these reusable Call results.

The revised source analyses have been checked under Lean 4.33.1. Both the complete algorithm result and the post-sorting result have accepted Prove2Me proofs, as do their shared union-find and sorting components. This is a formalization of known algorithms, not a claim of a new mathematical bound.

Where the formalization is demanding

Union by rank bounds an individual parent path logarithmically. Applying that bound independently to every operation does not establish the sharper accumulated inverse-Ackermann bound. Path compression changes future costs, so a usable method contract must describe the actual returned state and the same object's remaining amortized potential.

The component partition must also agree with the concrete selected flags. An abstract forest theorem alone does not show what the source returned. A cost theorem must include the two finds on each edge, the finds inside accepted unions, initialization, and any sorting the entry point performs. These obligations connect the graph result, mutable implementation, and measured work.

Formalization scope and source

The .algo code closely matches textbook MST-KRUSKAL: sort edges, create singleton components, compare endpoint representatives, and mark and join accepted edges. The sorting and following initialization/scan are separate callable functions. Sorting precedes singleton initialization here; neither stage changes the graph arrays. Integer identifiers and zero/one flags represent edge sets, and the constructor performs the MAKE-SET loop. The source retains full path compression, union by rank, and the explicit finds inside union.

Inputs use unbounded mathematical integers and mutable sequences defined at every integer index; finite prefixes describe the graph. Empty and disconnected graphs, negative weights, parallel edges, and self-loops are covered. Invalid counts, out-of-range endpoints, or an invalid supplied order are outside the main contracts. No contract assumes a preexisting successful transcript, an already minimal answer, or unverified data-structure behavior.

The runtime counts the eight named tick events, including imported calls. It does not measure elapsed time, integer bit complexity, or every arithmetic operation, access, allocation, or generated transition. Constructing input arrays and a caller-supplied sorted order is outside kruskal_sorted; the complete entry point includes sorting. The amortized bound does not assert inverse-Ackermann worst-case time for each individual operation.

Definitions and proofs cover the Ackermann hierarchy, rank/partition model, amortized union-find, mutable method contracts, sorting, graph exchange mathematics, and generated call composition. These components support further clients and sharper explicit bounds independently of Kruskal.

The compiler is Algo2Lean v0.1.4, with immutable release commit 0f79d5e. The examples and analyses are frozen separately at public commit 9755b41d188977ae1aafdaf9eccdac0b0edb0420; the compiler version is unchanged. The source and proof guide locates both entry points and their theorems. Raw generated Lean and Prove2Me packaging are distinct: platform packaging adapts module imports and declaration layout. The compiler itself does not yet have a formal semantics-preservation proof, so the source and generated semantics remain part of the reviewable development.

The import root is examples/kruskal. All five source files are shown below, including every imported module.

kruskal.algo

# CLRS MST-KRUSKAL (fourth edition, Section 21.2): sort edge identifiers,
# then scan them using union by rank and path compression.
# The separate kruskal_sorted entry point reuses an order supplied by a caller.
from sort_indices import sort_indices
from kruskal_sorted import kruskal_sorted


def kruskal(size: Int, sources: Seq, targets: Seq, weights: Seq, count: Int) -> Seq:
    order = sort_indices(weights, count)
    return kruskal_sorted(size, sources, targets, weights, count, order)

kruskal_sorted.algo

# The post-sorting phase of CLRS MST-KRUSKAL (fourth edition, Section 21.2).
# order lists every edge identifier once, in nondecreasing weight order.
# Edge identifiers are 0, ..., count - 1; endpoint arrays contain vertices
# in 0, ..., size - 1. The zero/one flag sequence represents the edge set A.
from union_find import UnionFind


def kruskal_sorted(size: Int, sources: Seq, targets: Seq, weights: Seq, count: Int, order: Seq) -> Seq:
    chosen = const(0)
    # Construct one singleton set for each vertex (the textbook MAKE-SET loop).
    sets = UnionFind(size)
    index = 0
    tick("kruskal")
    # @scan
    while index < count:
        edge = order[index]
        a = sources[edge]
        b = targets[edge]
        tick("kruskal")
        left = sets.find(a)
        right = sets.find(b)
        # @test
        if left != right:
            # @select
            chosen[edge] = 1
            # @join
            sets.union(a, b)
        index += 1
    return chosen

union_find.algo

# Disjoint sets over the integer elements 0, ..., size - 1.
# Each root names one component. Union by rank bounds parent paths, and
# find compresses every visited path directly to its root.
# Clients must pass in-range elements. The representation is independent
# of graphs, edge weights, or any particular client algorithm.

class UnionFind:
    parent: Seq
    rank: Seq
    size: Int

    def __init__(self, size: Int) -> None:
        # Batch the CLRS MAKE-SET operation for all elements in [0, size).
        self.parent = const(0)
        self.rank = const(0)
        self.size = size
        vertex = 0
        tick("uf_init")
        # @initialize
        while vertex < size:
            self.parent[vertex] = vertex
            vertex += 1
            tick("uf_init")

    def find(self, vertex: Int) -> Int:
        # CLRS FIND-SET: recursion finds the root, then rewrites every parent
        # along the return path. This is full path compression, not path halving.
        parent = self.parent
        tick("uf_find")
        # @follow
        if parent[vertex] == vertex:
            return vertex
        root = self.find(parent[vertex])
        # @compress
        parent[vertex] = root
        tick("uf_compress")
        return root

    def union(self, a: Int, b: Int) -> Bool:
        # CLRS UNION: find both roots, then apply union by rank (LINK).
        # The Boolean result reports whether two components were joined.
        left = self.find(a)
        right = self.find(b)
        tick("uf_union")
        if left == right:
            return False
        # @link
        if self.rank[left] < self.rank[right]:
            self.parent[left] = right
        elif self.rank[right] < self.rank[left]:
            self.parent[right] = left
        else:
            # Equal ranks may choose either root; here the left root wins.
            self.parent[right] = left
            self.rank[left] = self.rank[left] + 1
        return True

sort_indices.algo

# Order the identifiers [0, count) by their keys using a reusable binary heap.
# This supplies Kruskal's sort-by-weight step: insert every identifier, then
# extract minima. It is not the in-place HEAPSORT procedure from CLRS Chapter 6.
# Only identifiers are reordered; keys are unchanged. Equal-key identifiers
# may appear in either order.
from indexed_heap import MinHeap


def sort_indices(keys: Seq, count: Int) -> Seq:
    queue = MinHeap()
    result = const(0)
    index = 0
    # @insert
    while index < count:
        tick("sort_steps")
        queue.push_or_decrease(index, keys[index])
        index += 1
    index = 0
    # @extract
    while index < count:
        tick("sort_steps")
        result[index] = queue.pop_min()
        index += 1
    return result

indexed_heap.algo

# An indexed binary min-heap for Dijkstra's priority queue.
# vertices[position] and positions[vertex] are inverse on the active prefix.
# keys is indexed by vertex; position -1 means the vertex is not in the heap.
# Clients use nonnegative vertex identifiers, so pop_min can use -1 for empty.

class MinHeap:
    vertices: Seq
    positions: Seq
    keys: Seq
    size: Int

    def __init__(self) -> None:
        self.vertices = const(0)
        self.positions = const(-1)
        self.keys = const(0)
        self.size = 0

    def swap(self, i: Int, j: Int) -> None:
        a = self.vertices[i]
        b = self.vertices[j]
        # @exchange
        self.vertices[i] = b
        self.vertices[j] = a
        self.positions[a] = j
        self.positions[b] = i
        tick("heap_swaps")

    def sift_up(self, i: Int) -> None:
        # @up_loop
        while i > 0:
            parent = (i - 1) // 2
            tick("heap_comparisons")
            if self.keys[self.vertices[parent]] <= self.keys[self.vertices[i]]:
                return
            self.swap(i, parent)
            i = parent

    def sift_down(self, i: Int) -> None:
        # @down_loop
        while 2 * i + 1 < self.size:
            child = 2 * i + 1
            right = child + 1
            if right < self.size:
                tick("heap_comparisons")
                if self.keys[self.vertices[right]] < self.keys[self.vertices[child]]:
                    child = right
            # @compare_child
            tick("heap_comparisons")
            if self.keys[self.vertices[i]] <= self.keys[self.vertices[child]]:
                return
            self.swap(i, child)
            i = child

    def push_or_decrease(self, vertex: Int, key: Int) -> None:
        i = self.positions[vertex]
        if i < 0:
            self.keys[vertex] = key
            i = self.size
            self.vertices[i] = vertex
            self.positions[vertex] = i
            self.size += 1
            self.sift_up(i)
        else:
            tick("heap_comparisons")
            if key < self.keys[vertex]:
                self.keys[vertex] = key
                self.sift_up(i)

    def pop_min(self) -> Int:
        if self.size <= 0:
            return -1
        vertex = self.vertices[0]
        last = self.size - 1
        self.swap(0, last)
        self.size = last
        self.positions[vertex] = -1
        if last > 0:
            self.sift_down(0)
        return vertex

    def is_empty(self) -> Bool:
        return self.size <= 0

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022: Chapter 21, §§21.1–21.2, Theorem 21.1; Chapter 19, §§19.3–19.4, Theorem 19.14; and Chapter 6, §§6.1–6.2 and §6.5. Publisher.
• Algo2Lean, version 0.1.4, Lean-targeting compiler and source examples. Compiler and source repository.
• UnionFindAnalysis.find_amortized and UnionFindAnalysis.union_amortized, independently verified mutable union-find correctness and amortized work. Find and union.
• SortIndicesAnalysis.call, independently verified indexed-heap sorting with a permutation, nondecreasing keys, preserved caller storage, and work budget. Published theorem.

Prove2Me mission category: Textbook.

Reusable minimum spanning tree algorithms

A minimum spanning tree connects a weighted network at minimum total edge cost. When this routine is part of a larger algorithm, its caller also needs termination, preservation of existing data, and a bound on the work performed. These guarantees belong in a reusable contract, together with the returned mathematical result.

Prim reuses the Fibonacci heap already formalized for Dijkstra, including its published correctness and amortized running-time proofs.

This development follows Introduction to Algorithms (CLRS), fourth edition, Chapter 21, §21.2 for Prim and Theorem 21.1 in §21.1 for safe edges. The Fibonacci-heap analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5. That supplement is distinct from printed fourth-edition Chapter 19, which concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, returned tree, and measured work

An undirected weighted graph has vertices 0, …, V−1 and finite adjacency lists. Every edge occurs in both directions with the same integer weight. Weights may be negative. Parallel edges retain separate occurrence identities, and self-loops are permitted. Let m count undirected edge occurrences and E count stored adjacency occurrences: the supplied graph constructor gives E = 2m, including for self-loops. The root satisfies 0 ≤ root < V, and the main result assumes the graph is connected.

The output is a parent sequence, a mutable mathematical function from all integer indices to integers. The root has parent −1; every other declared vertex names its predecessor toward the root. A minimum spanning tree is an acyclic selection of input edges connecting every declared vertex, with minimum total weight among all competing spanning forests. The formal SpanningParents predicate asserts this full property for the returned sequence.

A heap contains mutable sequences, objects, typed collections, and named natural-number counters. A Call contract supplies a finite returning execution in the generated semantics for every caller stack. Runtime T is the increase in clockWork: each of seven Fibonacci-heap event counters and six Prim bookkeeping counters is counted once. This measures explicit source ticks, not elapsed time or integer bit complexity.

Formalization targets

The main target combines termination, minimum spanning tree correctness, preservation of existing caller storage, fresh output allocation, and a bound on the same execution's work. Its statement quantifies a single positive constant before every graph, root, and initial heap:

$$\exists C>0,\quad T\le C\bigl(E+V(\lfloor\log_2 V\rfloor+1)\bigr) \quad\text{for every valid connected input.}$$

The constant is independent of the input and its initial counter values. With E = 2m, this is the conventional $O(m+V\log V)$ bound. The logarithmic unit covers a graph containing only the root. The supporting reusable result retains the explicit estimate

$$T\le 23(E+1)+\bigl(12(2\lfloor\log_2 V\rfloor+2)+3\bigr)V.$$

FibonacciPrimAnalysis.correctness_and_running_time is the uniform-constant main result. FibonacciPrimAnalysis.summary provides the explicit bound and operation counts through prim_fibonacci.Call; runtimeBound and runtimeScale name the two expressions. The ordinary-output consequences are output_exists and output_with_cost_correct.

The component targets are the existing Fibonacci-heap correctness and amortized contract, the pure safe-edge and parent-tree results, the queue-independent Prim call contract, and their concrete composition. Invalid roots additionally return a fresh all-−1 sequence with zero ticks; no tree property is asserted for them.

What callers can reuse

The Fibonacci heap is reused from the Dijkstra formalization. This mission imports the same published implementation, shared definitions, correctness proofs, and amortized running-time contracts used by Dijkstra with a Fibonacci Heap. The existing heap contract keeps its original Prove2Me identity. Prim does not introduce a replacement heap or repeat its structural and amortized analysis; it proves the new algorithm-specific facts and composes them with that established contract. This reuse demonstrates how a verified data structure can support another algorithm without being formalized again.

The result lets a later algorithm invoke Prim on its current heap and receive a valid new parent sequence, an unchanged graph representation, unchanged preexisting sequences, objects, and typed collections, and a bound on the additional work. Initial counters need not be zero. The generic Prim theorem counts queue operations without depending on Fibonacci-heap internals; the concrete theorem discharges its queue assumptions using the existing published contract.

Prim's mathematical correctness and asymptotic complexity are established textbook results. The Algo2Lean development adds proofs about this actual mutable source program, including termination and storage preservation. Its complete Prim analysis has been checked locally under Lean 4.33.1. Prove2Me has accepted all four new Prim proofs, including the main correctness and running-time theorem, which reuses the already accepted Fibonacci-heap contract. The graph definitions are shared with the Kruskal analysis. Later clients can reuse these components without formalizing the data structure again. Alternative queue implementations and improvements to the explicit constants can retain the same mathematical specification.

Where the formalization is demanding

A minimum key alone does not establish that its parent pointer represents an input edge, that the chosen edges connect all vertices, or that their total weight is globally minimal. Those properties must remain connected to the mutable sequences that the source updates, including when weights tie or are negative.

A heap operation also changes shared mutable storage. Correct queue contents alone do not guarantee preservation of the graph or unrelated caller data. Moreover, some individual Fibonacci-heap operations are expensive despite small amortized budgets. The contract must account for the same evolving queue and counters across calls, rather than assume that every operation starts with an empty heap. These obligations distinguish the complete algorithm contract from a mathematical MST theorem or a count of queue calls.

Formalization scope and source

The .algo code closely follows the textbook pseudocode, with initialization, minimum extraction, and adjacency relaxation expressed as source operations and loops. It uses integer vertex handles and queues a vertex when first discovered. A parent of −1 denotes no discovered predecessor, so undiscovered keys require no artificial infinity. The root is selected before any edge is scanned. Relaxation compares an edge's weight directly; it does not add a path distance.

Inputs are finite linked adjacency lists with bounded endpoints and signed, unbounded integer weights. The theorem assumes a valid graph representation, symmetric adjacency, connectedness, and an in-range root. It assumes neither an existing successful transcript, a correct answer, nor an unverified queue-runtime estimate. The conclusion compares the result with every spanning forest. The whole-graph theorem does not apply to disconnected inputs.

The cost model counts the specified heap and Prim ticks. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Constant-sequence and queue construction add no ticks; constructing the input graph is outside the call. The imported queue API covers the insert/decrease, minimum extraction, and emptiness operations used here; meld and arbitrary deletion are outside this contract.

The compiler is Algo2Lean v0.1.4, whose immutable release commit is 0f79d5e. The Prim example and its proofs are versioned separately from this unchanged compiler release. Compiler-output reproduction and Prove2Me import packaging are separate checks: platform-adapted files need not have the raw generated files' hashes. The compiler does not yet have a formal semantics-preservation proof. The Prim source and proof guide identifies the exact statements, definitions, and source files. The separate example source commit is d832a565.

The project import root is examples. These are its three new source files. The other imports are the existing fibonacci_heap.algo and dijkstra/priority_queue.algo; the heap's independent source and analysis belong to the linked published component.

prim/graph.algo

# An undirected graph with integer edge weights. Each edge is stored in both
# adjacency lists. Negative weights, parallel edges, and self-loops are allowed.

class Edge:
    target: Int
    weight: Int
    next: Edge | None

    def __init__(self, target: Int, weight: Int, next: Edge | None) -> None:
        self.target = target
        self.weight = weight
        self.next = next


class Graph:
    size: Int
    heads: Seq[Edge | None]

    def __init__(self, size: Int) -> None:
        self.size = size
        if size < 0:
            self.size = 0
        self.heads = const(None)

    def add_edge(self, source: Int, target: Int, weight: Int) -> Bool:
        if source < 0 or source >= self.size or target < 0 or target >= self.size:
            return False
        self.heads[source] = Edge(target, weight, self.heads[source])
        self.heads[target] = Edge(source, weight, self.heads[target])
        return True

prim/prim.algo

from prim.graph import Graph, Edge
from dijkstra.priority_queue import PriorityQueue

# Prim's key is the cheapest edge from the growing tree to each vertex.
# parent stores the predecessor; -1 means no predecessor has been assigned.
# Vertices enter the queue when first reached, so infinity need not be encoded.
# The caller supplies an empty queue, zero keys and selected flags, and parents
# filled with -1. The root retains parent -1. Queue and client storage are disjoint.

def scan_edges(queue: PriorityQueue, key: Seq, parent: Seq, selected: Seq,
               vertex: Int, edge: Edge | None) -> None:
    # @scan
    while edge is not None:
        tick("edges")
        target = edge.target
        if selected[target] == 0:
            weight = edge.weight
            if parent[target] < 0 or weight < key[target]:
                # @improve
                key[target] = weight
                parent[target] = vertex
                tick("queue_updates")
                queue.push_or_decrease(target, weight)
                tick("improvements")
        edge = edge.next


def prim(graph: Graph, root: Int, queue: PriorityQueue,
         key: Seq, parent: Seq, selected: Seq) -> Seq:
    key[root] = 0
    tick("queue_updates")
    queue.push_or_decrease(root, 0)
    tick("queue_empty_checks")
    # @extract
    while not queue.is_empty():
        tick("queue_pops")
        vertex = queue.pop_min()
        selected[vertex] = 1
        tick("settlements")
        scan_edges(queue, key, parent, selected, vertex, graph.heads[vertex])
        tick("queue_empty_checks")
    return parent

prim/prim_fibonacci.algo

from prim.graph import Graph
from fibonacci_heap import FibonacciHeap
from prim.prim import prim as grow_tree

# On a connected graph, the returned predecessors describe a minimum spanning
# tree rooted at root. The root has predecessor -1. An invalid root returns -1
# everywhere without constructing a queue.
def prim_fibonacci(graph: Graph, root: Int) -> Seq:
    parent = const(-1)
    if root < 0 or root >= graph.size:
        return parent
    key = const(0)
    selected = const(0)
    queue = FibonacciHeap()
    return grow_tree(graph, root, queue, key, parent, selected)

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 21, §§21.1–21.2, Theorem 21.1. Publisher.
• The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 of the third edition, MIT Press, 2009/2022, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
• Algo2Lean, version 0.1.4, Lean-targeting compiler and source examples. Compiler and source repository.
• FibonacciQueueAnalysis.contracts, independently verified Fibonacci-heap queue behavior, preservation, and amortized work. Published Prove2Me theorem.

Prove2Me mission category: Textbook.

Reusable shortest-path algorithms

A shortest-path routine is often one component of a larger algorithm. Its useful contract must describe more than its returned numbers: it must also say that the routine terminates, preserves its caller's data, and incurs a bounded amount of work. Without these guarantees at a reusable boundary, each new caller must repeat parts of the implementation analysis.

This mission belongs to a series formalizing Introduction to Algorithms (CLRS), fourth edition. Its reference is Chapter 22, §22.3, Theorem 22.6, which establishes Dijkstra's correctness for nonnegative edge weights. The chosen queue is a Fibonacci heap, whose analysis is in the publisher's online supplement, retained Chapter 19, §§19.2–19.4, including Corollary 19.5 on degree. The fourth edition moved this material online; its printed Chapter 19 instead concerns disjoint sets. CLRS, fourth edition; official Fibonacci-heap supplement.

Graph, program, and measured work

A directed weighted graph consists of a finite set of vertices and a finite list of weighted outgoing edges for each vertex. Here vertices are integers 0, …, V−1, and every weight is a nonnegative integer. The number E counts adjacency-list entries, so parallel edges are counted separately. A source is in range when 0 ≤ source < V.

The program returns a distance sequence: a mathematical function from integer indices to integers, stored through a mutable reference. Its value is −1 at an unreachable vertex and otherwise is the minimum sum of edge weights over paths from the source. It uses a mutable Fibonacci heap to maintain unsettled vertices and their current distance estimates. A new vertex is inserted; a better estimate decreases its existing key.

A heap records the program's mutable arrays, objects, typed collections, and named natural-number counters. A Call contract relates the initial and final heap in the generated execution model: for every caller stack it supplies a finite execution returning the same final heap and result. The reusable theorem gives one such final state with all correctness, preservation, and cost properties together. The runtime T is the change in the sum of seven heap-event counters and six graph-algorithm counters. It measures the explicitly instrumented source operations, rather than elapsed time or integer bit complexity.

Formalization targets

The main correctness-and-running-time theorem has an accepted proof on Prove2Me under Lean 4.33.1.

The capstone target is one reusable contract giving termination, shortest distances, protected caller storage, a fresh result reference, and a total work bound for the same execution. Its main statement quantifies one positive constant before all graph, heap and source inputs:

$$\exists C>0,\quad T \le C\bigl(E+V(\lfloor\log_2 V\rfloor+1)\bigr) \quad\text{for every valid input.}$$

Thus different proofs may provide different constants without changing the main proposition. The constant cannot depend on the graph or its initial heap. This states the familiar $O(E+V\log V)$ scale while covering small instances. The published Lean statement includes an additional constant $1$ in its runtimeScale. A valid source requires $V\ge1$, so this displayed form absorbs that term into the unspecified constant, at most doubling it. The reusable supporting result retains the explicit estimate

$$T \le 23(E+1) + \bigl(12(2\lfloor\log_2 V\rfloor+2)+3\bigr)V \qquad (V\ge1).$$

The explicit supporting declaration is FibonacciDijkstraAnalysis.summary; its ordinary-output consequence is output_with_cost_correct. Its named runtimeBound has fixed coefficients. The main proposition is a separate corollary that hides those coefficients and retains the same termination, correctness, allocation, preservation and actual-call guarantees.

The component milestones are the independently verified Fibonacci-heap contract, the generic priority-queue Dijkstra contract, and their concrete composition. The heap milestone includes correct insertion of an absent in-range handle or strict decrease of a present key, extraction from a nonempty represented queue, preservation, and constant/logarithmic amortized budgets. Clients maintain the heap representation and the required separation from protected storage. The generic milestone includes shortest distances and counts of queue and edge operations. The concrete milestone removes abstract queue assumptions by using the verified heap. Invalid sources additionally terminate with a fresh all-−1 result and no ticks.

What clients receive

A verified client can call this implementation and immediately use the resulting distance sequence in another algorithm. It receives the graph representation unchanged, all previously allocated sequences, objects, and typed collections unchanged, a valid newly allocated result, and a bound on the work added to arbitrary initial counters. The result is useful for nested calls: the surrounding computation need not restart its clocks or forget its existing heap.

The mathematical algorithm and its asymptotic bound are established textbook results, not new open problems. The Algo2Lean source development contains the correctness, termination, preservation, and runtime proofs. The complete source project and exact submission files have been checked locally under Lean 4.33.1. This mission presents those proofs as importable definition and theorem nodes, with the source program displayed alongside the generated execution semantics. Future contributions can reuse the heap independently, instantiate the generic queue boundary with another implementation, or improve explicit bounds without redoing the complete graph proof.

Where the formalization is demanding

A heap operation changes a shared mutable representation. Correct abstract queue contents alone do not establish that graph storage survived, that an array reference remains allocated, or that the cost argument describes the same execution as the correctness argument. The contract must connect all these facts rather than leave them as independent assumptions.

Fibonacci heaps also have expensive individual calls despite small amortized budgets. A worst-case bound applied separately to every decrease-key loses the intended running time. The reusable boundary must therefore describe the potential of the evolving queue, not a fresh empty queue for each operation. The generic Dijkstra result must remain independent of the internal tree and pointer representation of its chosen heap.

Formalization scope and source

The .algo code closely follows the textbook pseudocode: initialization, minimum extraction, and adjacency relaxation appear as explicit source loops and operations. Representation choices are made explicit: -1 denotes infinity, flags record settled vertices, and only discovered vertices enter the queue. The routine returns distances without a predecessor tree. Thus it preserves the textbook's shortest-distance algorithm for nonnegative weights, while differing from its all-vertices initial queue and literal notation.

The Lean representation includes finite adjacency lists stored as linked Edge objects, a Graph with typed heads, unbounded mathematical integers, and mutable sequences indexed by every integer. Zero-weight edges, self-loops, parallel edges, and shared adjacency suffixes are allowed. The theorem assumes a valid finite graph representation and an in-range source for its shortest-distance claim. It does not assume the desired distances, a pre-existing execution transcript, or an unverified queue-runtime bound.

The cost model sums the stated named ticks over unbounded mathematical integers and total sequences. It does not count every arithmetic operation, sequence access, allocation, or generated transition. Queue and constant-sequence construction add no ticks; input-graph construction is outside the call being analyzed. The independent queue API covers the operations used here, not heap meld or arbitrary deletion.

The compiler is Algo2Lean v0.1.4, at release commit 0f79d5e. The downloaded website compiler reproduces all 15 generated modules for this project exactly; the manifests identify the compiler and every source file. Byte-for-byte reproduction concerns unmodified compiler output. The Prove2Me transplant separately rewrites module imports/names, declaration packaging, and explicit options as required by the platform; its adapted files are not claimed to have the raw output's hashes. The edits and source mapping are recorded, the adapted dependency closure has been checked, and every theorem's elaborated type matches the original. The supplementary analysis archive contains the uniform-constant capstone, a reproducible source build, and an independent statement readback. The handwritten libraries include shortest-path mathematics, finite execution and call composition, heap representation, Fibonacci-heap operations, and reusable queue contracts. These boundaries are intended for later CLRS formalizations. The compiler itself is not yet equipped with a formal semantics-preservation proof.

The project import root is examples. The entry file is dijkstra/dijkstra_fibonacci.algo:

from graph import Graph
from fibonacci_heap import FibonacciHeap
from dijkstra.dijkstra import dijkstra as search

# Construct a Fibonacci heap and bind its operations to generic Dijkstra.
def dijkstra_fibonacci(graph: Graph, source: Int) -> Seq:
    distance = const(-1)
    if source < 0 or source >= graph.size:
        return distance
    settled = const(0)
    queue = FibonacciHeap()
    return search(graph, source, queue, distance, settled)

The companion algorithm description displays the complete five-file source: graph.algo, fibonacci_heap.algo, dijkstra/priority_queue.algo, dijkstra/dijkstra.algo, and this entry wrapper. The Fibonacci-heap component also displays its independent source. Improvements to exposed contracts, client examples, and source-level cost models are welcome when they preserve the stated semantics and remain separately checkable.

Selected references

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein, Introduction to Algorithms, fourth edition, MIT Press, 2022, Chapter 22, §22.3, Theorem 22.6. Publisher.
• The same authors, Fibonacci Heaps, official online supplement to the fourth edition, retained Chapter 19 from the third edition, §§19.2–19.4, Corollary 19.5. Publisher's supplement.
• Algo2Lean, version 0.1.4, compiler and source semantics. Compiler and source repository.

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.