Loading home page…
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
Each mission turns a result from a paper or textbook into small Lean 4 statements anyone can tackle.
Campaigns group missions around a shared mathematical goal. Each one tracks a quantity, such as an upper or lower bound. Have a good candidate in mind? Ping us on Slack, Zulip, or WeChat.
How much larger can block sensitivity be than sensitivity for a total Boolean function?
For a total Boolean function , a block of coordinates is sensitive at if flipping every bit in that block changes . Let count sensitive singletons and be the maximum number of pairwise disjoint sensitive blocks. Define and .
This campaign seeks larger exponents for which there exists an infinite family of total Boolean functions , indexed by , satisfying
Here denotes a quantity tending to zero as . Higher is better. The classical exponent is , and Huang's bound gives a ceiling of .
OpenAI's construction achieves an exponent strictly greater than .
One sufficient way to establish an exponent is to find a single total Boolean function with and . Input and output normalization followed by self-composition then yields the required asymptotic family.
Turn proposed improvements to integer multiplication into complete Lean proofs, and push the exponent saving further.
Harvey and van der Hoeven established an algorithm in 2021. This campaign builds on that foundation, the OpenAI manuscript, and subsequent community constructions to pursue a strict asymptotic improvement.
For two -bit integers, the target is
A positive beats asymptotically; larger is better. Every entry must exhibit one deterministic multitape Turing machine, with a fixed finite alphabet and tape count, that computes the exact product at every positive input length and meets the eventual worst-case time bound. The tracked number measures an asymptotic exponent saving.
Classical algorithms solve 3SUM in time. In a 2026 breakthrough, Alman and Vassilevska Williams gave a deterministic algorithm, refuting the integer 3SUM hypothesis. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for 3SUM on polynomially bounded integers, using a word RAM with -bit words, and pursues smaller exponents.
Classical algorithms solve all-pairs shortest paths in time. In a 2026 breakthrough, Alman and Vassilevska Williams refuted the APSP conjecture with a deterministic algorithm. How low can the exponent go?
Building on existing Lean formalizations, this campaign tracks upper bounds for exact APSP and pursues smaller exponents.
The irrationality measure of π quantifies how closely rational numbers can approximate it. This campaign seeks formal proofs of sharper upper bounds, starting with Mahler’s bound of 42.
The sharp Hlawka inequality for Schatten -norms is a cousin of the triangle inequality: it relates the norms of three matrices to the norms of their pairwise sums and their total sum. For complex diagonal matrices, an exact formula for the best possible comparison constant has been proved in Lean for every real . We conjecture that the same formula holds for all .
What is the smallest cutoff for which this formula holds for every real ?
References:
Is every odd number a sum of primes? This campaign tracks formalized proofs of the smallest that suffices.
Schnirelmann (1930) showed some finite works. Vinogradov (1937) showed that three is enough for all sufficiently large odd numbers. Tao (2012) proved unconditionally. Helfgott (2013) proved that every odd number greater than is a sum of three primes, though the proof is still unrefereed. Ideally, we can formalize this statement here. Note that three is optimal: is neither prime nor + prime.
Schoolbook matrix multiplication takes operations. The exponent is the infimum of all such that two matrices can be multiplied in arithmetic operations; trivially , and is conjectured but open.
Strassen gave the first nontrivial bound, , in 1969, and introduced the laser method in 1986 to reach . Coppersmith and Winograd's 1990 bound of stood for two decades. Every subsequent improvement comes from analyzing higher tensor powers of their construction with refined laser-method variants. That line reached in 2025, and the current record is , from August 2026. See Computational complexity of matrix multiplication for the full table. Can we formalize these results and even improve on them?
A graph homomorphism sends vertices of one graph to another while preserving adjacency. Requiring this map to be continuous makes graph coloring sensitive to topology: each color must occupy an open and closed region. For integer lattice actions, the resulting questions connect finite graph structure with continuous dynamics. The results considered here give an algebraic sufficient condition on a finite target graph that works in every finite lattice dimension. They are Theorem 1.4 and Proposition 7.1 of Ruijun Wang's Continuous graph homomorphisms of higher dimensional abelian group actions, a 2026 research preprint.
Fix an integer . The integer lattice is , with standard generators . Each generator has one coordinate equal to one and all other coordinates zero. An action of on a space assigns maps satisfying and . A continuous action uses the discrete topology on . It is free when implies .
A Polish space has a topology induced by a complete separable metric. It is zero-dimensional when its topology has a basis of clopen sets, meaning sets that are both open and closed. The standard Schreier graph on joins to for each generator, with adjacency understood symmetrically.
Let be a finite simple graph on a vertex set , equipped with the discrete topology. A continuous homomorphism is a continuous function such that
Write when such a map exists for every free continuous lattice action on every zero-dimensional Polish space.
A closed walk starts and ends at the same vertex, and its length counts edges. Repetitions are allowed. The reduced homotopy group identifies based closed walks under cancellation of a spur and cancellation of a closed four-walk, with these relations compatible with concatenation. Its identity is the constant walk. These conventions agree with Section 2.
Theorem 1.4 assumes an odd closed walk whose reduced class has trivial square:
The source statement appears in Section 1.
The main target, Proposition 7.1, permits any finite order:
Here is a positive integer; it need not be the least exponent. The square-trivial case follows by taking . The stronger statement is given in Section 7.1.
These results turn one finite algebraic witness into a conclusion covering all the spaces, actions, and positive dimensions specified above. Once a graph satisfies the hypothesis, an individual action requires no additional dynamical condition beyond the stated assumptions. The conclusion concerns finite discrete targets and the standard generating set.
Both results are established in the cited paper. Complete local Lean proofs now cover their full universal statements. The local project build and kernel audit have passed, and the final declarations use only Lean's standard logical axioms. Prove2Me has accepted the complete uploaded proof dependency graph. Both original headline theorem identities now have status Proved.
The completed development supplies reusable statements and checked infrastructure for lattice actions, reduced graph walks, finite probability distributions, and continuous graph homomorphisms. These components support inspection and reuse beyond the two headline results.
Choosing a homomorphism separately on each orbit does not ensure continuity across nearby points of the space. Freeness identifies each orbit with a lattice once an origin has been chosen, but does not supply continuously chosen origins across all orbits. A proof must therefore establish continuity of the resulting vertex map itself. Restricting attention to one action, one dimension, or an orbitwise map would leave the stated universal conclusion unresolved.
The lattice is represented by , actions use additive notation, and standard adjacency includes both orientations of each generator edge. Reduced homotopy is an inductively generated relation on genuine Mathlib graph walks; powers are repeated concatenations. The target vertex type is arbitrary and finite, with its discrete topology.
Source spaces and target vertex types have independent universe parameters. Empty source spaces are allowed. No connectivity assumption is imposed on the target, and no separate nonemptiness hypothesis is added. The odd-walk witness already forces target nonemptiness. Neither a carrier-construction assumption nor an approximation condition appears in either final theorem.
Finite order refers to the class of the walk, rather than its length. An odd walk can revisit vertices and traverse edges repeatedly, so the hypothesis does not require an embedded cycle. All four-walk relations are included, including those with repeated vertices. The conclusion asserts existence of a continuous adjacency-preserving function; it asserts neither uniqueness nor injectivity. These distinctions matter when comparing a formal declaration with the source: replacing arbitrary closed walks by simple cycles or adding connectedness would change the objects quantified over. The recorded statements retain the wider walk convention used in the paper.
Further contributions can reuse the infrastructure or establish related variants while preserving these conventions. Any changed statement should distinguish its additional hypotheses and its altered conclusion from the two results recorded here.
Ruijun Wang, Continuous graph homomorphisms of higher dimensional abelian group actions, arXiv preprint arXiv:2609.39824v1, 2026. Version and source; Theorem 1.4; definitions; Proposition 7.1.
A metric tensor is a coordinate-free object, but every concrete exact solution of Einstein's vacuum equations is written down in coordinates, and the same spacetime appears in the literature in many charts: Schwarzschild in standard, Eddington–Finkelstein, Painlevé–Gullstrand and isotropic coordinates, Kerr in Boyer–Lindquist and ingoing form, and so on. Checking that a chart is a vacuum solution means computing the Ricci tensor of its metric components; checking that two charts describe the same solution means exhibiting a coordinate change and verifying that the metric components pull back. Release I of the Exact Vacuum Atlas (a separate, earlier mission) certified seven such charts (Minkowski ×2, Schwarzschild ×3, Kerr ×2) together with four coordinate relations.
Release II adds the missing method: a proof that the coordinate Ricci tensor used throughout the Atlas transforms as a tensor under any smooth coordinate change, so that a vacuum certificate can be transported along a coordinate relation instead of being recomputed. It then uses this to certify new Schwarzschild charts (Painlevé–Gullstrand, both signs; isotropic, both radial branches, in spherical and Cartesian form) and to give the Painlevé–Gullstrand certificate two distinct proof routes with an audited separation of their specified dependencies; they still share definitions, data and Mathlib.
All objects are coordinate-level data on open subsets of ( in every application):
a metric is a matrix of real functions, a candidate inverse is another such
matrix, and the coordinate Ricci tensor is defined by the usual Christoffel
formulas from partial derivatives of slices (definition bundle Atlas_Core_Basic of release I). A
vacuum certificate for on an open set records eight obligations: open and
nonempty, symmetric, on , and of class on , an explicit
Lorentz frame with (signature ), and all sixteen Ricci
components zero on . A coordinate relation records a smooth bijection with inverse
, a Jacobian matrix whose entries are genuine derivatives, and the pull-back identity
on . Mathlib provides real analysis, matrices and multivariable
calculus. In the pinned Mathlib revision 0df444a360eaa60ab8c11dca51a86af692955474, the project did not find the complete indefinite-metric connection and Ricci definitions required by this development. The registered B3 coordinate definitions supplement that fixed version; this is not a claim about all current or future versions of Mathlib.
ExactVacuumAtlas.Release02.ricci_law)For any dimension , open sets , a smooth map with a genuine Jacobian and a right inverse ( on ), and regular metric data on (symmetric, genuinely invertible, ; no curvature condition), if and on then
The proof goes through the Christoffel transformation with its second-derivative term (the Christoffel symbols are not a tensor), the tensoriality of the matrix curvature (the and terms cancel), and the contraction to the Ricci tensor. The final Ricci theorem does not assume the Ricci transformation law. The intermediate curvature lemma has an explicit connection-transformation premise, which the proved Christoffel transformation discharges in the metric application. The registered Ricci tensor is not redefined.
certificate_transport — a vacuum certificate on , a coordinate relation , the explicit conditions that is open and nonempty, a right inverse of the genuine Jacobian on , and any genuine left inverse of yield a vacuum certificate on (all eight obligations, 4D).pg_route_direct — Painlevé–Gullstrand metric ,
, , certified on (regular-coordinate points with included when ; no global event-horizon statement)
by direct computation (release-II sprint 01).pg_route_transport — the same statement, proved a second time by transporting the
Eddington–Finkelstein certificate of release I along the PG↔EF relation. The independence of this
route is a constant-level dependency-closure audit (no PG table, PG certificate or PG root is reached),
not a conjunction of two proofs.control_direct, control_transport, control_witness — a non-vacuum control family: the
cylinder metric pulled back by (non-affine for , and the identity for ); the sixteen Ricci components
(, , , rest ;
, ) are proved twice (tables, and the transformation law from the
release-I cylinder values), with the nonzero witness at .isotropic_branches — the two radial relations between the isotropic chart
and the standard chart: outer branch () and inner branch
(), both onto .isotropic_main — isotropic Schwarzschild ,
, , certified for every on (both branches transported from the standard certificate and glued; is
Minkowski).isotropic_sph_cart_relation — the spherical ↔ Cartesian isotropic chart relation on the slit chart
( on the spherical side and on the Cartesian side), with and on both sides and on the spherical side, for every real . This is a relation of the specified coordinate data; the vacuum certificates below are restricted to .isotropic_cartesian — the Cartesian isotropic certificate
for every on the natural domain (no axis or slit cut: the slit
certificate is transported along the reflection and the relabelling
and the three domains are glued).pg_main, pg_coverage, pg_std_restricted — the sprint-01 PG roots: both signs; and the
regular data at for ; the PG↔EF relation on the whole domain and the composite standard → EF → PG relation on only.The transformation law is the reusable link between a full certificate in one coordinate representation and a certificate in another. Transport also discharges the required source-domain, inverse-matrix, regularity and Lorentz-signature obligations; a bare table of zero Ricci components alone is not treated as a full certificate.
The law is a long but elementary computation (second derivatives of the Jacobian, Cramer's rule for the
smoothness of the inverse Jacobian, symmetry of mixed partials, index bookkeeping over Fin n); the
isotropic charts need genuine inverse functions with square roots, arccos and a half-angle arctan,
with smoothness and bijectivity on explicit open domains. Nothing is stated at the manifold level.
Coordinate-level statements on open subsets of (the law itself on ). Not claimed: an identification with a Mathlib manifold Ricci tensor in the pinned development; any global, event-horizon or maximal-extension theorem; PG or isotropic vacuum certificates for negative mass; certification of (for this is the excluded degenerate isotropic sphere, while for it is the excluded origin); that the union of the two isotropic branches is a single bijection; that the inner branch is the interior .
Müller, T., Grave, F.: Catalogue of Spacetimes, arXiv:0904.4184v3 (§2.2.3 isotropic, PG); Martel, K., Poisson, E.: Regular coordinate systems for Schwarzschild and other spherical spacetimes, arXiv:gr-qc/0001069; Carroll, S.: Lecture Notes on General Relativity, arXiv:gr-qc/9712019 (§3, transformation of the connection and curvature); release I of the Exact Vacuum Atlas (platform mission on this site).
New material of release II is released under Apache-2.0; the Kerr, release-I and third-party sources keep their recorded origins and licences. A public Git repository is not yet available: every node's source field cites the local release-candidate commit 11fb317259353b71a41d6daed466c495cffd7db4 with file, line range and SHA-256 of the staged file. Environment: Lean v4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474. Local audits: no sorry, no native_decide; axiom closure ⊆ {propext, Classical.choice, Quot.sound}.
n、任意光滑坐标变换（真实 Jacobian J，显式右逆 K）与任意对称、真实可逆、
C^∞ 的旧度规（不要求真空），R'_{ij}(y) = Σ_{ab} J_{ai} J_{bj} R_{ab}(Φ y)。证明经 Christoffel 变换（含二阶导数项 K ∂J）、
矩阵曲率张量性、收缩。最终 Ricci 定理不把待证变换律作为假设；中间联络变换前提由已证明的定理提供；ricciOf 定义未改。CoordRelation + 源域开且非空 + Jacobian 的显式右逆 + 新度规的真实左逆 ⇒ 新证书（八项逐字段），四维。M ≥ 0、ε² = 1，整个 {r > 0, 0 < θ < π}（M > 0 时包含域内 r = 2M 的正则坐标点），第一阶段表格直接计算。P ∧ P。λ ≠ 0 时非仿射，λ = 0 时为恒等映射） β ↦ β + λ sin α 拉回；16 个 Ricci 分量由表与变换律各证一次：
R₂₂ = 1+λ²c²s²、R₂₃ = R₃₂ = λcs²、R₃₃ = s²、其余 0；λ = 1 时 R₂₃(0,1,π/4,0) = √2/4 ≠ 0；λ = 0 为恒等映射。ρ > M/2（M ≥ 0）、内支 0 < ρ < M/2（M > 0），都映到 r > 2M；互逆、真实 Jacobian、拉回均已证。M ≥ 0，域 ρ > 0, ρ ≠ M/2, 0 < θ < π；两支分别由标准证书传递后并域；M = 0 为 Minkowski。ρ > 0, ρ ≠ M/2；球坐标另有 0 < θ < π, −π < φ < π，Cartesian 一侧另有 r_xy + x > 0；fromCart 用 arccos 与半角 arctan；对所有实 M 成立（不推出负质量真空证书）。M ≥ 0，域 ρ > 0, ρ ≠ M/2，无极轴/切口限制：slit 证书经反射与循环重标传递并并域。M = 0 特例，以及 M > 0 时 r = 2M 正则坐标点的覆盖；PG↔EF 在整个域的双向关系；正向为 standard → EF → PG 的合成关系只在 domStd（r ≠ 2M），单独标示。不声称：流形/全局事件视界/最大延拓；PG或isotropic的负质量真空证书；在ρ = M/2处的证书（M>0为排除的退化球面，M=0为排除的原点）；ricciOf 等于 Mathlib 流形 Ricci；两支并域是一个双射；内支是 r < 2M。
The value of a Dirichlet -function at controls class numbers of quadratic fields, the least quadratic non-residue, and the distribution of primes in arithmetic progressions. For a real character modulo the size of is governed by the zeros of near : a real zero close to (a Siegel zero) would make abnormally small, and no unconditional argument rules this out effectively.
Littlewood's bound (1928) states that under the generalized Riemann hypothesis for ,
which is optimal up to the constant. Explicit constants under GRH were given by Lamzouri, Li and Soundararajan (2015).
The mission The Quasi-Riemann Hypothesis: A Zero-Free Half-Plane Re(s) > 7/8 formalizes a preprint (OpenAI, 30 September 2026) claiming that every Dirichlet -function is zero-free in . That claim is not yet verified. This mission asks what a zero-free half-plane would give: an explicit Littlewood-type lower bound for under the hypothesis for the single character concerned.
Timeline.
A Dirichlet character modulo is a multiplicative function that vanishes off the units. It is primitive if its conductor equals , and real if all its values are real (they then lie in ). Its -function is
continued meromorphically to , with a pole only for the trivial character. For a primitive character modulo the continuation is entire and .
The hypothesis used throughout is
It concerns one character, not a family, and the half-plane is open. For primitive , GRH for implies .
There are constants and such that for every primitive real character modulo satisfying ,
For the constant is admissible:
For the same and ,
With (Mertens' constant), for every real ,
For every primitive character modulo and every with ,
The result. A zero-free half-plane at a fixed distance from makes the Littlewood bound effective with explicit constants. Through the class number formula it gives explicit lower bounds for class numbers of quadratic fields of large discriminant, and it excludes Siegel zeros for the character concerned. The hypothesis is weaker than GRH, and, if the 7/8 preprint is correct, it holds for every primitive character. In that case the goal and the explicit milestones become unconditional explicit theorems.
Formalizing it. The explicit bounds are proved in the preprint by Daugherty, Ryan and Ward (doi:10.5281/zenodo.23400116, Theorem 2), with constants certified in interval arithmetic. None of the statements here has a machine-checked proof. A formalization would give an independently checked conditional result that composes directly with a Lean proof of the zero-free half-plane. It would also add explicit analytic number theory to Mathlib: the convexity bound, explicit prime-sum estimates, and logarithms of -functions on zero-free regions.
The classical proof of Littlewood's bound under GRH uses the zeros' location on the critical line to bound just to the left of . Under the weaker hypothesis only a fixed strip next to is zero-free, and grows like there. The control must be strong enough that an exponentially smoothed prime sum of length dominates, with every constant explicit and uniform in . The prime sums in turn need explicit, not asymptotic, estimates for .
The -function is Mathlib's DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and "real" is stated as for every . The value is compared through its real part, and the two-sided milestone uses the principal complex logarithm. Mertens' constant is written out as with Mathlib's tsum over primes. The hypothesis is a hypothesis on the single character in each statement, never a family-wide assumption. It is satisfiable, for example under GRH, so the conditional statements are not vacuous.
A complete development needs:
The convexity bound and the prime-sum estimates are reusable well beyond this mission. Contributions toward any of these are welcome.
In a two-player one-round nonlocal game, a verifier samples a pair of questions, sends one to each of two players who cannot communicate, and accepts or rejects the pair of answers. The players may share an arbitrary quantum state and measure it; the entangled value of the game is the supremum of their acceptance probability over all such strategies. Nonlocal games are the operational form of Bell's theorem, the model behind device-independent cryptography and self-testing, and the engine of the complexity class of languages decidable by a polynomial-time verifier interacting with entangled provers (Cleve, Høyer, Toner, Watrous, 2004, arXiv:quant-ph/0404076).
With classical provers, multiprover interactive proofs decide exactly (Babai, Fortnow, Lund, 1991, doi:10.1007/BF01200056). For entangled provers the lower bounds grew in steps: (Ito, Vidick, 2012, arXiv:1207.0550), (Natarajan, Wright, 2019, arXiv:1904.05870), and finally (Ji, Natarajan, Vidick, Wright, Yuen, 2020, arXiv:2001.04383): every recursively enumerable language, the halting problem included, has a two-prover one-round interactive proof with entangled provers, and the entangled value of a game cannot be approximated by any algorithm. Through the equivalences of Fritz (2012, arXiv:1008.1168), Junge, Navascués, Palazuelos, Pérez-García, Scholz, Werner (2011, arXiv:1008.1142) and Ozawa (2013, arXiv:1212.1700), the theorem gives a negative answer to Tsirelson's problem and to Connes' embedding problem for von Neumann algebras.
Everything below is defined from scratch; the formal development uses exactly these objects.
A synchronous game has a finite question alphabet and a finite answer alphabet , shared by both players, a probability distribution on , and a decision predicate which, on equal questions , rejects every pair of unequal answers .
A synchronous strategy of dimension assigns to each question a projective measurement on : positive semidefinite matrices summing to the identity, each idempotent. Both players use the same measurements, and probabilities are taken in the normalized trace . The value of the strategy is
the acceptance probability when the players measure a maximally entangled state of dimension . The synchronous value is the supremum of over all synchronous strategies of all dimensions. A synchronous strategy is a tensor-product strategy, so , the entangled value.
A game description is a finite object from which a synchronous game is read off: natural numbers fixing and , a finite list of weighted question pairs and a finite list of accepted tuples . The game has proportional to the total weight listed for (the point mass at if the total weight is zero), and accepts exactly the listed tuples, except that unequal answers to equal questions are rejected. Descriptions are coded as natural numbers, so a map from machines to descriptions can be computable.
Turing machines are Gödel numbers of partial recursive functions, an equivalent model of computation; " halts on the empty input" means that applied to is defined.
There is a computable map from machines to game descriptions such that for every machine ,
This is Theorem 12.2 of arXiv:2001.04383 in synchronous form, with the running time of relaxed from polynomial to computable. It leaves the running time and the choice of value unfixed, and it is the weakest statement that already makes the game value uncomputable: no algorithm decides whether a game has synchronous value or at most .
The paper's statement has computable in polynomial time, and both the synchronous and the entangled value satisfy the two clauses. With polynomial time the goal gives for the class of two-prover one-round proofs with completeness and soundness , and with the elementary inclusion this is . These statements need a model of polynomial time and a definition of tensor-product strategies, and will be added as milestones once those definitions are published here.
The result. Approximating to within a constant is as hard as the halting problem. A hierarchy of semidefinite programs converges from above to the commuting-operator value , so the two values cannot coincide for every game: a negative answer to Tsirelson's problem and, by the equivalences cited above, to Connes' embedding problem, open since 1976. On the complexity side, is the exact characterization of the power of entangled provers.
Formalizing it. The theorem is proved and its proof is machine-checked: HaltingGameValue.halting_reduces_to_gameValue in the Lean 4 development vidick/MIPRE-formalization proves exactly the goal above over Mathlib, with propext, Classical.choice and Quot.sound as its only axioms. The development is about 1,200 modules and 410,000 lines, including vendored components and a separate library for the low individual degree test; its blueprint records every statement, the dependency graph and the correspondence with the paper. This mission makes the result a fixed, auditable target: the definitional layer above is written over Mathlib alone, so the goal can be checked from first principles, and the components of the proof whose developments are self-contained are published as milestones with their proofs, to be imported, reused and re-proved. The first milestone, the recursive compression lemma of Marks, Nezhadi and Yuen (Lemma 5.1 of their manuscript; blueprint node lem:recursive-compression), comes with a complete proof over a dependency tree of 22 definition bundles and 60 theorems: a cost model of computation, an efficient universal machine, the s-m-n and Kleene recursion theorems, succinct descriptions.
The obvious approach fails at once: a verifier runs in time polynomial in its input, while a machine may run for arbitrarily long before halting, so no fixed game can check halting by simulation. What makes reachable is gap-preserving compression: a polynomial-time transformation of verifiers such that the compressed verifier, at index , has value when the original verifier at index does, and value at most when the original does. The compressed game is exponentially cheaper than the game it certifies, and a fixed-point argument through Kleene's recursion theorem, in the abstract form of the recursive compression lemma, turns compression into the halting reduction. Compression rests on three components, each with a central ingredient that is a theorem in its own right: question reduction by introspection, in which the players sample their own questions and a Pauli basis self-test built on the quantum low individual degree test certifies that they did; answer reduction, in which the players prove through a probabilistically checkable proof that their answers would have been accepted; and gap amplification by parallel repetition. In each component soundness must hold against strategies of unbounded dimension, where no finite enumeration or compactness argument is available, and the quantitative losses must compose so that the threshold is preserved exactly.
The goal is stated with the synchronous value, projective measurements on with , and the normalized trace in place of a state vector; the real part of the trace is taken in the strategy value, and the synchronous value is the supremum, in , over all strategies of all dimensions (the values lie in ). Game descriptions are interpreted with the fallback distribution above, so that the interpretation is total. Machines are Mathlib's Nat.Partrec.Code and computability is Mathlib's Computable; polynomial time is not fixed by the goal.
No trivializing formalization is available: the game depends on only through , and the two clauses demand values and at most on complementary sets of machines, so no map that ignores its argument, or produces only descriptions of zero total weight, satisfies the statement.
A complete development needs four layers: (i) a model of computation with costs, with polynomial-time maps, an efficient universal machine, the s-m-n and Kleene recursion theorems and succinct descriptions, which is the recursive compression milestone's dependency tree and is reusable in any undecidability argument by compression; (ii) normal form verifiers, conditionally linear samplers, the Pauli basis test and the quantum low individual degree test; (iii) the three transformations, with answer reduction over a PCP decider built from a succinct Cook–Levin theorem and direct parallel repetition in value form, and their soundness; (iv) the halting reduction from compression and the passage from the tensor-product to the synchronous value. Statements and proofs of these components over the shared definitional layer are welcome, as are alternative proofs of the goal from the same definitions, the polynomial-time and entangled-value strengthenings, and the inclusion .
MIPRE/HaltingGameValue.lean, proof MIPRE/MainTheorem.lean) and its blueprint.A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry.
The mission "Plasticity: c₀ and c₀₀" proved, among other things, that a nonexpansive bijection from the unit ball of a space between and onto the unit ball of a space between and is a signed permutation of coordinates whenever the target matches signs (card Plasticity.CUB37).
A scan of unused hypotheses showed that the first step, the normal form, never uses that the target lies in .
This mission records the consequence: the target may be any space between and , because the existence of such a bijection forces it into .
is a linear subspace with and one with , both real with the supremum norm, for arbitrary index sets (definitions Plasticity_SeqSpace).
is a nonexpansive bijection of the closed unit ball of onto that of ; nothing is assumed about its inverse.
The milestone excludes nonexpansive bijections onto balls that the usual extreme-point argument cannot reach: for the ball has no extreme points, yet no ball between and is mapped onto it by a nonexpansive bijection.
The goal is the card Plasticity.CUB37 without its target hypothesis.
The normal form for targets inside is a separate card (Plasticity.SeqSpace.exists_signed_permutation_inward), the proof of Plasticity.CUB37.normal_form with the unused hypothesis removed; the goal then imports the Proved card Plasticity.CUB37.
A metric space is plastic if every nonexpansive bijection of it onto itself is an isometry; Cascales, Kadets, Orihuela and Wingler (2016) asked whether the closed unit ball of every real Banach space is plastic.
The mission "Plasticity: unit spheres covered by finite-dimensional faces" proved that a nonexpansive bijection between unit balls carries every finite-dimensional face of the target ball back onto a face of the same dimension (card Plasticity.Faces.matchesFace_of_finiteDimensional, stated for normed spaces), and that is a linear isometry whenever the target sphere is covered by finite-dimensional faces, for Banach spaces.
That covering theorem was proved through a sphere-preservation theorem whose proof needs completeness.
This mission removes completeness from the covering theorem and its plasticity corollary, by the ending that Angosto, Kadets and Zavarzina (2019) used for polyhedral faces.
and are real normed spaces, not necessarily complete, with closed unit balls and unit spheres .
A sphere face of is a nonempty convex set that is an extreme subset of (definitions Plasticity_Faces).
is a nonexpansive bijection; nothing is assumed about the continuity of .
The result. Completeness plays no role in the mechanism: the face theorem already holds for normed spaces, and the ending needs only the geometry of planes and the Mazur–Ulam theorem. The steps are: maps into ; by induction on the face dimension, is isometric on each scaled preimage face along chords that end at boundary points where it is already homogeneous (Zavarzina's Lemma 2.5, proved here by differentiating one inequality at a point of a plane where the norm is differentiable along a line, which Rademacher's theorem supplies), and two points of a face at equal distances from all its boundary points coincide, so is homogeneous on every ray; then is an isometry of the balls, and its homogeneous extension is linear by Mazur–Ulam.
Formalizing it. The face theorem is a Proved card in the earlier mission; this mission adds the ending, so that the statements are machine-checked in their natural generality.
Real scalars; the face theorem Plasticity.Faces.matchesFace_of_finiteDimensional and the basic facts Plasticity.BallMap.* are imported Proved cards.
New inputs are separate cards: Zavarzina's isometry lemma for homogeneous points (Plasticity.BallMap.norm_map_sub_map_eq_of_map_smul, using Rademacher's theorem from Mathlib for the density of smooth points), two elementary facts about relative boundaries of bounded sets, and homogeneity on preimage faces (Plasticity.Faces.map_smul_of_map_mem_face).
Statements are not to be weakened by assuming completeness, continuity of the inverse or a bound on the face dimensions.
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.
and are real normed spaces with closed unit balls and unit spheres ; the covering and plasticity forms assume them complete. A sphere face of is a nonempty convex set that is an extreme subset of : if a point of lies in the open segment between two points of , both points lie in . Its dimension is that of its affine hull; and are its relative boundary and its extreme points. is a nonexpansive bijection; nothing is assumed about the continuity of .
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 -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.
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.
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 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.
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 ; 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).
A coordinate point is (in Lean, a function ). A coordinate metric is a matrix of real functions of ; a candidate inverse is another such matrix. The slice derivative is the derivative of at ; on the open domains used here every slice is , so is the genuine derivative. With
(definition bundle Atlas_Core_Basic), the vacuum certificate for a set
asserts: is open and nonempty; is symmetric on ; on ; all components
of and are on ; at every point of there is an invertible matrix with
(Lorentzian signature, bridged to Mathlib's signature of the
quadratic form); and every component vanishes on . A coordinate relation
asserts: on ,
on , maps bijectively onto , is on and on , every entry is the
genuine derivative of the slice , and on . Units
, signature , , .
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.
ExactVacuumAtlas.Release01.main)where is with the explicit candidate inverse of
each row, and R1–R4 are coordinate relations with explicit maps: R1/R2 standard Schwarzschild to ingoing/outgoing
Eddington–Finkelstein on with , resp.
(Jacobian determinant ; the logarithm is Mathlib's Real.log, for which when , so one
formula covers both sides of ); R3 Boyer–Lindquist to ingoing Kerr on with
, , , explicit
for all real (three branches of ; Jacobian determinant ); R4 spherical chart
to with the usual map (Jacobian determinant
).
ExactVacuumAtlas.Release01.coverage)For the EF domain contains a point with ; for the Boyer–Lindquist domain contains a point with ; for , the ingoing Kerr domain contains a point with ; at these points all Ricci components vanish. The certified domains are therefore not narrowed to an exterior region.
ExactVacuumAtlas.sigPos_sigNeg_four)A Lorentzian matrix in the frame sense has Mathlib signature , .
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 ( for ), either sign of or negative for Kerr, the regular-coordinate portion of with (EF, ), or the points with at which and (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.
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 , and the spherical Minkowski row is transported from the
standard Schwarzschild certificate at , 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, , while for the covector is not null, since ), the Ricci components are rational functions whose vanishing holds only modulo ,
and every derivative must be a genuine derivative, never a default value of deriv. For R3 the antiderivative of
has three different closed forms depending on the sign of , all covered without restricting the
parameters.
Lean representation: coordinate metrics on as above; ContDiffOn ℝ ∞; Matrix (Fin 4) (Fin 4) ℝ;
Mathlib sigPos/sigNeg for the signature bridge. Conventions committed: , , coordinate order
, EF matrix entry (from ), ingoing Kerr entries read off
with the half-Hessian convention from Visser eq. (E:K1), (no 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.
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.
For a set , is the space of bounded real functions on with the norm ; consists of the with finite for every , and of the finitely supported . A space between and is a linear subspace with , with the supremum norm; its closed unit ball is . A subspace realizes all sign patterns if for every countable and all signs () some has on ; does. A signed coordinate bijection is a map with for a bijection and signs .
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).
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.
Real scalars, arbitrary index sets (no countability or nonemptiness assumed).
is Mathlib's lp (fun _ : Γ => ℝ) ⊤; and are submodules of it (definitions Plasticity_SeqSpace), and a ball map is a function on 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 .
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.
The Cauchy–Riemann operator on is the model elliptic operator of symplectic topology: pseudoholomorphic curves solve nonlinear perturbations of , and their regularity, compactness and Fredholm theory all start from an a priori estimate for . In Hofer–Wysocki–Zehnder's asymptotic analysis of pseudoholomorphic curves in symplectisations, this estimate appears as formula (49): on a disc of radius , every smooth map supported in the interior of satisfies
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 from Stein, Chapters I–III, and the and 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 theory of singular integral operators.
For an integer , and there is such that for every disc of radius and every smooth supported in the interior of , (Hofer–Wysocki–Zehnder I, estimate (49), p. 366).
The result. The estimate for is the analytic input behind elliptic bootstrapping for pseudoholomorphic curves: interior regularity, 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 : the maximal theorem, the Calderón–Zygmund decomposition, Marcinkiewicz interpolation and the 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 , and other estimates.
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 , the case of the interpolation theorem uses a strong-type bound in place of a weak-type one, and the singular integrals are limits in of absolutely convergent truncated integrals. The Dini condition on is a condition on a supremum over pairs of points of the unit sphere. The Cauchy–Riemann statements involve vector-valued maps , real derivatives of all orders and Sobolev norms on discs.
DbarRegularity. The definition module DbarRegularity_Setting defines maximalFunction, closedCube, dbar and sobolevNorm. The mission is standalone and imports no definitions from other missions.EuclideanSpace ℝ (Fin d) with volume, functions on it are complex-valued, in milestone 7 is EuclideanSpace ℝ (Fin 2), and is EuclideanSpace ℂ (Fin n). Stein's dimension is written throughout, and is the dimension of the target .eLpNorm in ℝ≥0∞. Exponents are real and enter as ENNReal.ofReal p; exponents allowed to be infinite are in ℝ≥0∞. Constants are in ℝ≥0 or ℝ, never in ℝ≥0∞.fderiv ℝ φ z 1, fderiv ℝ φ z Complex.I; smoothness is ContDiff ℝ ∞ (, not analytic); higher derivatives are iteratedFDeriv ℝ j. Supports are tsupport.𝓝[>] 0, in the seminorm.Contributions welcome: reusable general lemmas of real-variable harmonic analysis on , and calculus lemmas for smooth compactly supported maps on .
Prove2Me mission category: Textbook.
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.
A matrix is represented by an array of row arrays, written
Seq[Seq[Int]]. Each row contains unbounded mathematical integers. Let
be the recursion depth and the matrix dimension.
The mathematical input values are functions
; only their entries inside the
square enter the product.
A heap stores mutable rows, outer arrays, objects, and named
natural-number counters. The predicate MatrixHeap.Stored h a A connects
an allocated outer-array reference to its row contents .
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 and final heap . All correctness, preservation, and work
conclusions below concern that same and .
The counted work 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.
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 , the contract supplies a finite returning call whose output matrix satisfies
Every previously allocated row, outer array, and object is preserved. The result's outer array is fresh, and its in-square rows are fresh and pairwise distinct. One positive natural constant is chosen before all depths, heaps, and matrix inputs:
Thus the main proposition leaves the upper constant available for improvement. The accepted proof supplies . On the permitted dimensions this gives the conventional 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 , , , and , the four increments are
All other clocks remain unchanged. Consequently the total satisfies and . These are properties of the existing combined contract and its supporting definitions, rather than additional open targets.
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.
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.
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 . 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)
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 -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 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.
Time is (the paper's time ). The state space is finite and the action is control or treatment. For each time and action there is a transition matrix with ; the matrices may change arbitrarily with , which is the nonstationarity. The initial state has distribution . The reward is drawn from a distribution on , independently of everything else given , and for all . Write .
The policy assigns treatment with probability at every time, independently of everything else. is all-treatment, is all-control, and the experiment runs . Write and for expectation under . The value function and the global average treatment effect (GATE) are
The TPG estimator with truncation size is
so is the difference-in-means estimator.
Two quantities control the bounds. The mixing assumption (Assumption 1) asks for with for all , all and all probability vectors on , where . The kernel deviation is .
There are absolute constants such that for every environment, every , every and every and as above,
The constants are left unspecified, as in the paper's statement, so an improvement of the constants does not invalidate the goal.
For data collected under with , the paper gives both bounds with explicit constants, for the TPG estimator and for a reward-corrected variant. At , Proposition 5 reads
with .
and its truncated analogue are differentiable at , with derivative equal to the horizon average of differences of (-truncated) -values, and equals the corresponding derivative for every . Without the mixing assumption, the untruncated estimator satisfies and .
For fixed , under mixing at all times, a positive limit of the normalized variance (Assumption 2) and a Cesàro mean-stability condition (Assumption 3),
where is a Newey–West estimator with bandwidth , . The supporting statements are a covariance inequality under strong mixing, the bound 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.
Theorem 1 separates two error sources: a term of second order in that does not grow with , and a term that decays geometrically in . Together with Proposition 2 it shows what truncation buys: a variance bound of order instead of order , at the price of a bias term of order . 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.
The first idea is to bound by the second derivative of on . Every pair of times contributes to that second derivative, so this route gives the of Proposition 2 and nothing uniform in the horizon. Theorem 1 is uniform in , and its bound has no term of first order in beyond the truncation term; Proposition 5 shows that such a term is present at every allocation . 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.
TPG.Env S packages for a finite type S. Kernels are real matrices with nonnegative entries and rows summing to one, indexed by all ; a statement with horizon uses only the times below . 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. , , and the -values are defined from this law, and expectations given 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 and , as in the paper. Asymptotic statements compute the law of each statistic under the horizon- measure: convergence in distribution is tested against bounded continuous functions, and convergence in probability is stated for each . The limit is a parameter constrained by Assumption 2. For the law of is not a probability law and no statement depends on it. The hypotheses are satisfiable for every , and : 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- 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.
Prove2Me mission category: Textbook.
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.
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
and let denote the
inverse Ackermann function with convention
, , and
, where the superscript denotes repeated composition. Its
published definition
is shared with the data-structure analysis.
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.
This is KruskalAnalysis.correctness_and_running_time, with scale
KruskalAnalysis.runtimeScale. It gives the conventional total
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.
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
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.
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.
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.
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
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.
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.
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.
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:
The constant is independent of the input and its initial counter values.
With E = 2m, this is the conventional bound. The logarithmic
unit covers a graph containing only the root. The supporting reusable result
retains the explicit estimate
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.
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.
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.
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.algofrom 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.algofrom 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)
FibonacciQueueAnalysis.contracts, independently verified Fibonacci-heap
queue behavior, preservation, and amortized work.
Published Prove2Me theorem.Prove2Me mission category: Textbook.
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.
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.
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:
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 scale while covering small instances.
The published Lean statement includes an additional constant in its
runtimeScale. A valid source requires , so this displayed form absorbs
that term into the unspecified constant, at most doubling it.
The reusable supporting result retains the explicit estimate
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.
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.
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.
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.
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:
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.
A signature (Sig) consists of a type of sorts, function symbols and predicate symbols . Formulas (Formula L Γ) are built in a typed context from , , predicates, and . A structure (Str) assigns a nonempty set to each sort and interprets the symbols. A theory is a set of formulas in context, each read as its universal closure; a model of is a structure satisfying them all.
The category (Model T) has the models of as objects and elementary embeddings as arrows: maps on every sort that preserve and reflect every formula. Theories are categorically equivalent (CategoricallyEquivalent) if .
A Morita extension of a -theory (MoritaData L T) adds to :
Each new symbol gets one defining axiom, and the symbols of one new sort share a single axiom. The extension (D.ext) is together with these axioms. Each definition must satisfy its admissibility condition in every model of :
| Definition | Condition |
|---|---|
| subsort | |
| quotient | is an equivalence relation |
| function symbol |
The reduct gives a functor (D.proj).
and are Morita equivalent (MoritaEquivalent) if two finite chains of Morita extensions and (MoritaReach) end in logically equivalent theories, that is, theories with the same models, over a common signature.
Milestones 1–3 together say that 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.
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:
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.
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.
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.
Fin m → Srt). Terms and formulas use de Bruijn variables in typed contexts Γ : Fin n → Srt; Formula.all binds variable 0.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.MoritaData L T lists the new sorts and symbols and their defining -formulas. The signature (D.sig) and the axioms are generated from it, and admissibility is stated semantically, over all models of . Any Morita extension in the paper's sense is of this form up to renaming of the new symbols.MoritaEquivalent asks for a bijective signature map F between the two chain ends such that a structure is a model of iff its F-reduct is a model of .Type.A complete development will need:
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.
A gauge theory can be formulated in several mathematically different ways: with potentials (connections), with field strengths (curvature), or with holonomies, the parallel transports around closed loops. Philosophers and physicists ask whether these formulations say the same thing, and which one carries "surplus structure".
Category theory makes the question precise. Each formulation is a category of models, and each translation between formulations is a functor. A functor that is faithful and essentially surjective but not full forgets structure. One that is full and faithful but not essentially surjective forgets properties. One that is full and essentially surjective but not faithful forgets stuff. One that is all three forgets nothing and is an equivalence. This taxonomy is due to Baez, Bartels and Dolan (Baez–Shulman, §2.4).
Weatherall (2016) applied it to electromagnetism. Potentials without gauge arrows forget structure relative to field strengths (Proposition 1). The erratum in arXiv v2 (p. 15) corrects his Proposition 2: the principal-bundle formulation, whose arrows include gauge transformations, forgets only stuff, not nothing. Nguyen, Teh and Wells obtain the same verdict for the gauge-orbit functor (their Proposition 3.2.3). In their footnote 26 they identify the forgotten stuff as the constant ("global") gauge transformations. All of this is abelian, U(1) on a contractible spacetime.
The non-abelian counterpart is the holonomy formulation. Barrett's reconstruction and representation theorems, and their categorical upgrade by Rosenstock and Weatherall (Theorem 2), show that on a connected manifold, principal connections and generalized holonomy maps form equivalent categories. On the topological side, Freed and Quinn (eqs. 3.11–3.13) identify the automorphisms of a finite-group gauge field with a centralizer.
This mission states these results for an arbitrary group on a finite graph. There the smooth and topological subtleties disappear, but the categorical content survives intact.
A finite directed graph has vertices , edges , and maps . A step is an edge traversed forwards or backwards, and a walk is a list of steps whose endpoints chain. is connected from if every vertex is reached by a walk from .
This is the discrete, fixed-base-point form of Rosenstock–Weatherall's Theorem 2. In the taxonomy above, potentials-with-gauge and holonomies forget nothing relative to each other. The statement holds for every group , finite or not. The base-point-changing arrows of Rosenstock–Weatherall are not included.
Fin-indexed cells and are not required to be simple. Loops and multiple edges are allowed. A 2-complex adds faces with a base vertex and a boundary walk proved to be a loop.Group; finiteness is not assumed.Functor.Full, Functor.Faithful and Functor.EssSurj. The goal is their conjunction, not an explicitly constructed inverse.The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. Continuous-time reserves connect mortality and financial discounting to the dynamics of insurance liabilities. The standard Thiele differential equation is a recognised result in actuarial mathematics and describes the effect of mortality death strain, premium income and interest force on prospective policy reserves. A significant missing foundation of the preceding primarily discrete-time missions is the exact analytic relationship between a closed-form constant-force reserve and its differential equation. The Oxford actuarial reserve lectures and the Encyclopedia of Mathematics give independent descriptions of the equation.
Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.
An insured is alive at valuation time t, with term insurance expiring at time T. A death benefit B is payable immediately upon death within the contract term. Continuous premiums arrive at annual rate P while the insured is alive. The mortality force μ and financial interest force δ are constant. Survival over u years is exp(-μu), financial discount is exp(-δu), and their product discounts by exp(-(δ+μ)u). The combined force k=δ+μ must be strictly positive for the capstone's conventional closed-form quotient. The prospective reserve at time t is V(t)=(μB-P)(1-exp(-k(T-t)))/k for 0≤t≤T.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ForceDiscount_le_one:
Nonnegative interest force implies ordinary discount factors no greater than one.
This block contributes 11 theorem targets and 5 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ThieleRHS_zero_benefit:
Without insurance benefit, reserve drift includes only premium and liability unwind.
This block contributes 11 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ThieleContinuousValuation_fundamental:
The capstone proves the exact continuous term reserve issue value, terminal zero, nonnegative on the term and the actual Thiele ODE, not merely a definitional rewriting.
The main target is ActuarialValuation.cm1ThieleContinuousValuation_fundamental. The capstone proves the exact continuous term reserve issue value, terminal zero, nonnegative on the term and the actual Thiele ODE, not merely a definitional rewriting.
The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The closed form reserve formula can be verified independently through expected benefit and premium present values, and must satisfy the continuous-time insurance reserve balance at every intermediate time. Thiele's equation states V'(t)=P+δV(t)-μ(B-V(t)), where B−V is the death strain at risk. The terminal reserve vanishes at expiry of the pure term insurance. Proving all conditions together guards against wrong signs in mortality costs, incorrect interest accumulation, and omitting the premium stream. This formal special case may be reusable for continuous-time multi-state reserves or variable force extensions, provided their assumptions are stated explicitly.
The formula is valid under a constant mortality force and a constant financial force and is not a universal solution of a time-varying Thiele equation. Real exp differentiation and finite-term time inversion require correct signs. The quotient involves k=δ+μ, so algebraic cancellation requires k nonzero. For nonnegative reserves one additionally needs μB≥P and t≤T. At t=T the closed form vanishes, but no positive term must be inferred after expiry. The ODE must be established by differentiating the actual prospective reserve, not inserting it as an extra axiom. Zero mortality and zero premiums provide legitimate boundary cases.
The model describes a pure continuous term insurance with immediate death benefit and continuous premium income. Expenses, profit margins, maturity endowments, lapses and stochastic changing forces are excluded. Financial force δ need not individually be nonnegative if the combined k is positive, but for a mortality probability interpretation μ must be nonnegative. The closed-form expected claim and premium PV definitions use the same integrated combined discount factor. The capstone is a nontrivial analytic theorem joining boundary values, PV valuation, reserve nonnegativity and Thiele's linear ODE and is suitable for reuse in richer insurance reserve models.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. Salary growth, defined contribution funding and defined benefit pension accrual are usually treated in separate actuarial calculations, even though they can be joined through a coherent finite cashflow model. The standard pension formula B=alpha times years of service times pensionable salary and the distinction between final salary and career-average revalued earnings are explained by Dickson, Hardy and Waters. A larger formal mission can prove the exact deterministic contribution rate that finances a salary-linked CARE pension, rather than stopping at a definition of accrued pension. This fills a gap not addressed by earlier tranche factor and commutation missions.
Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.
At service year t, salary S(t) is annual pensionable pay. Annual benefit accrual at rate alpha is alpha S(t). The CARE retirement benefit revalues each year's accrual with a tranche-specific real factor R(t), giving B=alpha sum S(t)R(t) over the service period. A pension capitalisation factor a at retirement converts this annual pension to liability L=aB. A DC member or sponsor contributes a fixed fraction c of salary each year, with terminal growth multiplier G(t), producing assets A(c)=c sum S(t)G(t). The relevant salary contribution base F is the last sum. All monetary quantities and multipliers must use the same common terminal valuation date.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 9 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1FinalSalaryPension_nonneg:
Nonnegative service, salary and accrual rate produce a nonnegative final-salary pension.
This block contributes 10 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1CARELiability_add_last:
An additional year of pension accrual adds its own capitalised liability slice.
This block contributes 14 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1SalaryPensionFunding_fundamental:
Capstone proves the unique actuarially consistent contribution threshold funding a CARE pension, with nonnegative surplus for rates above the threshold.
The main target is ActuarialValuation.cm1SalaryPensionFunding_fundamental. Capstone proves the unique actuarially consistent contribution threshold funding a CARE pension, with nonnegative surplus for rates above the threshold.
The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The formal result makes the relation between salary-linked pension promises and their financing explicit. An increasing final-salary pension need not equal a career-average pension, and a DC accumulated account value is not directly an annual pension. CARE revaluation and contribution fund growth can differ significantly, so the unique equivalent rate c=L/F must use the separately defined factors rather than an arbitrary average. The equations can support pension valuation controls, funding reconciliations and salary projection sensitivities. They can become reusable infrastructure for subsequent UK defined benefit funding and DC pension options.
The common time origin for earnings, CARE revaluation and contribution accumulation must be maintained. Each cashflow slice is counted exactly once and the result is not a closed-form salary sum unless growth is genuinely constant. The rate c=L/F is only actuarially meaningful if the accumulation base F is positive; division by zero must not make a false equivalence claim. Zero service, negative growth, increasing salary and nonnegative annuity factors are genuine boundary cases. The capstone must prove monetary matching and the threshold property, not assume either as an axiom.
The model is finite and deterministic. Salary projection uses a constant growth special case, while salary and revaluation cashflow schedules can vary arbitrarily. It does not pretend that a matching terminal DC fund guarantees an identical DB pension after retirement: the annuity capitalisation factor must be agreed and both schemes may have different risk allocation. The final salary formula is a separate valuation component. The nontrivial root proves a contribution-rate funding threshold and is reusable in future stochastic contribution and employer covenant extensions.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
The established IFoA actuarial mathematics syllabus discusses the relevant mathematics (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). CM1 actuarial foundations form the mathematical background. A pension service table projects active members through competing causes of leaving employment, including retirement, death, disability and withdrawal. A comprehensive valuation must account for those mutually exclusive events without creating or destroying pension scheme members. Dickson, Hardy and Waters Chapter 9 discusses pension service tables and Chapter 8 introduces multiple decrement models. Earlier missions consider a single-year decrement law and mortality variance; this mission develops multi-year cohort conservation and a complete reconciliation between two implementations of cause-specific pension benefit valuation.
Exact actuarial equivalence is conditional on the stated model assumptions. The previously known actuarial mathematics in the published textbooks motivates these original-derived Lean targets. They remain unproved until real theorem solutions are accepted. Nontrivial cashflow and probability examples exclude vacuous zero-benefit substitutes, and the resulting identities can support future actuarial missions.
An initial active-service cohort l(0) is projected to year N. For each year t, d(t,j) records the nonnegative number of scheme members leaving active service due to cause j during that year, where causes are mutually exclusive. The service-table accounting law is l(t+1)+sum_j d(t,j)=l(t). Individual cause probabilities conditional on active membership are q(t,j)=d(t,j)/l(t) when l(t)>0. The probability of remaining active at year t is l(t)/l(0). The unconditional probability of a specified exit is d(t,j)/l(0). A benefit amount b(t,j) and a discount factor v(t) attach to that exit event. The expected present value can be constructed either directly from unconditional cause exit mass or by multiplying active survival and conditional cause probability.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 11 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ServiceValid_telescoping:
All exits during the horizon plus active lives at its end exactly reconcile to the initial cohort.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ServiceMassPartition:
The full pension cohort partitions into all competing causes of exit and eventual continued active service.
This block contributes 10 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ServiceCohortValuation_fundamental:
The nontrivial capstone simultaneously proves full multi-year service-table probability conservation, consistent cause-specific pension benefit PV and nonnegative liability.
The main target is ActuarialValuation.cm1ServiceCohortValuation_fundamental. The nontrivial capstone simultaneously proves full multi-year service-table probability conservation, consistent cause-specific pension benefit PV and nonnegative liability.
The professional actuarial syllabus provides the background to this reusable work (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). A service table must reconcile deaths, retirements, withdrawals and remaining active membership throughout the projection. The multi-period accounting result says cumulative decrement counts plus terminal active count equal the original cohort; after normalisation, the corresponding probabilities sum to one. This provides an important actuarial QC invariant. The same model supplies a direct payment valuation and a survival-conditioned valuation, which must match if probability denominators and calendar payment dates are consistently defined. Both the conservation invariant and cashflow equality can be reused for scheme funding, actuarial gain analysis and member-level pension cost models.
Each decrement cause must form a disjoint partition and the yearly cohort equation has no additional inflow from new entrants. To divide by remaining active service, survivor counts must be nonzero in each year where conditional rates are used. At the terminal horizon no more cause payment years are included. The exact finite-sum telescope must account for every annual exit once and only once. Negative claim sizes, negative exit counts or zero initial cohorts cannot support the probability interpretation. The capstone deliberately validates both valuation routes rather than obtaining equality by defining the two formulas identically.
The results model a closed, finite cohort with given competing decrement counts. They do not infer cause-specific hazards from observed data or assume independent causes. Causes are disjoint observed outcomes; the conditional exit probabilities sum with the surviving-in-service probability to one. The service table can later be enhanced by new entrants, state transitions and pension commencement options, but these are outside this precise closed-cohort theorem. The calculations retain common valuation dates and financial units for all benefits. The root establishes probability conservation, PV equivalence and nonnegativity, and is reusable in other pension missions.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). A life-table survival model underpins almost every actuarial life contingent assurance, annuity and pensions result. The earlier actuarial missions concentrate on valuation of given death and survival probabilities. CM1_new_formula.pdf sections on life-table identities, select mortality, fractional-year assumptions, joint lives and contingent annuities motivate a larger proof mission establishing those foundations rather than restating assurance formulas already formalised. The principal application is the correct value of a spouse's reversionary annuity when the original member dies while the beneficiary survives.
The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.
A life table l(x) records survivor counts at integer ages. Conditional survival and death probabilities divide later survivor counts by a nonzero starting cohort. Select rates use within an explicit initial select period, with ultimate rates from the boundary onwards. Within an integer year UDD fractional survival is linear in elapsed fraction, whereas constant force of mortality gives an exponential survival model; neither assumption can be inferred from the other. For two lifetimes, pX(t) and pY(t) are marginal survival probabilities and pBoth(t) is the joint probability of both lives surviving. A valid joint model obeys 0 ≤ pBoth ≤ each marginal probability, but does not need independence. The difference pY(t)−pBoth(t) is the probability of y surviving while x has died. Finite annuity present values sum positive discount factors multiplied by appropriate survival-event indicators.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 12 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1DeferredDeath_nonneg:
Valid cohort life counts yield a nonnegative deferred mortality probability.
This block contributes 12 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1SelectUltimateRate_zero_select:
A select period of zero years uses ultimate rates immediately.
This block contributes 18 theorem targets and 7 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ReversionaryValue_fundamental:
The genuine contingent annuity capstone combines positivity, reversionary partition and inclusion-exclusion for any valid dependent joint survival model, not just independent lives.
The main target is ActuarialValuation.cm1ReversionaryValue_fundamental. The genuine contingent annuity capstone combines positivity, reversionary partition and inclusion-exclusion for any valid dependent joint survival model, not just independent lives.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Pension spouse benefits, contingent pensions, first death and last survivor assurance contracts all depend on correctly partitioning joint and marginal survival events. Using pX pY for all joint probabilities would silently impose independence, which is neither universally correct nor necessary for the most important reversionary identity. The capstone shows a contingent pension to y can be computed as the y-only annuity minus the joint-life annuity, with correct survival-event assumptions and finite payment dates. It also proves the separate last-survivor inclusion-exclusion relation. These foundational results can serve as accepted dependencies for detailed UK DB spouse entitlement and guarantee missions.
Conditional life-table quotients require a positive or nonzero cohort count at the reference age and intermediate age. A monotone life table is needed for probabilities to lie within zero and one. A survival decomposition cannot assume independence across adjoining conditional periods without precise population conditioning, and multiplicativity of constant-force survival cannot be falsely attributed to UDD within the year. Select and ultimate mortality require disjoint endpoints. The reversionary decomposition must keep both-alive and y-alone events distinct and retain the correct payment dates, while allowing arbitrary joint lifetime dependence. The full capstone is the exact conjunction of substantive annuity identities and a meaningful positivity inequality.
The model is a finite discrete collection of integer-age and payment-date statements augmented by separate algebraic fractional-age rules. The UDD and constant-force models are explicitly assumed and are not asserted as general mortality laws. Annuities are generic finite discounted expected payments; contract guaranteed payments or calendar pension increases would enter through schedule-specific weights in a later mission. The theorem capstone does not impose independent lifetimes, and the independent product model is kept as an optional separate special case. There is no double-counting of survivor states or need to invent an average life expectancy.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Actuarial life insurance pricing is incomplete without the link between gross premiums, future reserve liabilities, emerging cashflow profits and risk capital requirements. The IFoA CM1 syllabus explicitly includes gross prospective and retrospective reserves, death strain, mortality profit, profit signatures, profit testing for unit-linked business and elimination of negative non-unit profit cashflows by reserve zeroisation. Dickson, Hardy and Waters (2009), Chapter 11 (Emerging costs for traditional life insurance) supplies the broader profit testing theory. We combine these elements into one connected mission with an optimisation property as its capstone.
The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.
A contract has dated benefit payments, expenses, premiums and probability/discounter weights over a finite horizon N. Gross level premium divides the total expected benefit and expense PV by a nonzero premium annuity factor. A prospective reserve equals expected future outgo less future premiums, and a retrospective reserve uses prior accumulated premiums less outgo on the same valuation basis. Death strain at risk measures the claim amount net of the next reserve release. For unit-linked products the unit fund develops through allocation, charges and investment returns. Non-unit projected cashflow c(t) combines premium and charges less expenses and claims. The non-unit reserve R(t), growth factor g(t)>0 and survival/continuation weight s(t)≥0 determine projected profit Π(t)=c(t)+g(t)R(t)-s(t)R(t+1), with terminal reserve R(N)=0.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ExpectedBenefitPV_add_last:
Finite expected benefit PV recurses correctly when one extra payment term is appended.
This block contributes 11 theorem targets and 5 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1MortalityProfit_favourable:
With positive death strain, fewer actual deaths than expected produce favourable mortality profit.
This block contributes 10 theorem targets and 5 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ProfitMargin_nonneg:
Profit margin is nonnegative if projected profit is nonnegative and the premium base positive.
This block contributes 12 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1ZeroisationOptimality_fundamental:
The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The main target is ActuarialValuation.cm1ZeroisationOptimality_fundamental. The finite-horizon capstone proves that a backwards-zeroised reserve produces nonnegative projected profits and is pointwise minimal among all nonnegative feasible reserve paths with the same terminal boundary.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). The zeroisation recursion can be used to eliminate projected negative future non-unit profits while avoiding excessive reserve financing. It is valuable to show that the backwards reserve is not only feasible but pointwise minimal among all competing nonnegative reserve profiles satisfying the same profit and terminal constraints. Such a theorem is an auditable dynamic optimisation guarantee, not merely a spreadsheet check. It also provides a bridge from earlier finite cashflow PV and insurance reserve missions to modern policy profit testing. The intermediate theorem groups separate gross premium equivalence, death strain, reserve valuation, unit funds, discounted profit signatures and zeroisation.
The formal model carefully distinguishes net benefit cashflows and reserve-adjusted profit, and never calls a gross premium formula universally correct without its equivalence assumptions. In zeroisation, g(t) must be strictly positive before division and multiplication inequalities can be reversed, while s(t)≥0 is necessary to compare different next-year reserve requirements. The floor max(0,(sRnext-c)/g) is a genuine feasibility threshold. The minimality result needs backward induction from the same terminal reserve, not a false forward monotonicity argument. Negative non-unit cashflows and zero survival are meaningful cases. The result does not equate the risk discount rate used for net present value with the investment growth rate g(t).
This is a finite-horizon deterministic expected-cashflow model rather than a fully stochastic regulatory reserve basis. Probability, benefit and expenses schedules enter as given finite arrays. Gross premiums use the simplified actuarial equivalence principle and not arbitrary commission or investment-profit target structures. The non-unit zeroisation capstone is conditional on a reserve path satisfying the specified backward recursion; its existence can be constructed by a later recurrence theorem and should not be replaced by a hidden axiom. All explicitly stated profit constraints and nonnegative reserve bounds are maintained for each pre-terminal valuation date. The theorem is meaningful even when cashflow c(t) is negative.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
This work is motivated by the IFoA CM1 financial and life-contingent mathematics syllabus (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Financial mathematics provides the time-value backbone of actuarial pricing and pension liability management. The CM1 formula sheet records effective interest and discount rates, annuity-certain relationships, loan amortisation and bond duration. These should be proved as one connected mathematical construction culminating in the local Redington immunisation conditions, rather than as separate missions of two-line rearrangements. A correct proof handles actual discounted dated cashflows and the consistency of their rate derivatives. The IFoA 2026 CM1 financial mathematics syllabus provides the subject boundaries.
The established CM1 modelling conventions and previously known actuarial identities provide the conceptual background, while the following larger original-derived Lean results still need accepted proofs. The stated nontrivial capstone excludes vacuous equal cashflow or zero-duration substitutes. Each accepted module could become reusable infrastructure for future actuarial formalisation missions.
Real-valued effective annual interest i is restricted to i greater than minus one where cashflow discount factors need to remain positive. A finite dated cashflow c(k) is payable at time k+1. The annual discount factor is (1+i) raised to the negative integer horizon, implemented as a reciprocal of an accumulated factor. Unit annuities in advance and arrears use dates k and k+1 respectively. The cashflow valuation V(i) is a finite weighted sum. A loan balance at t is the present value of remaining loan installments. Duration and convexity numerators aggregate discounted times and squared-time coefficients of cashflows. Asset and liability streams are compared at a single flat effective rate, so rate derivatives are well-defined on the positive accumulation domain.
All declarations below are original derived CM1-style formal results. The supporting milestone order builds an intentional mathematical chain to a single root theorem.
This block contributes 10 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1NominalInterest_scale:
Nominal rate scales the periodic effective interest input.
This block contributes 11 theorem targets and 3 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1IncreasingImmediate_succ:
Increasing annuity recurrence uses the next arithmetically increasing payment.
This block contributes 10 theorem targets and 2 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1LoanBalance_nonneg:
Remaining positive scheduled loan payments have nonnegative prospective value.
This block contributes 12 theorem targets and 4 definitions. The model distinguishes direct source identities from hypotheses used to extend them to a general cashflow or life-contingent valuation system.
Representative theorem ActuarialValuation.cm1RedingtonImmunisation_fundamental:
The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.
The main target is ActuarialValuation.cm1RedingtonImmunisation_fundamental. The genuine Redington second-derivative test gives a local surplus minimum at the matching effective yield; it does not assert global or arbitrary curve immunisation.
The established actuarial syllabus identifies the relevant relationships and applications (https://actuaries.org.uk/media/yfnkmkbq/cm1_syllabus-2026-_final-proof.pdf). Matching current assets and liabilities without checking interest-rate sensitivity is inadequate. A valuation system should reconcile cashflow present values, annuities, prospective loan balances, duration and convexity, and verify that asset surplus cannot turn negative under sufficiently small yield movements when Redington's strictly positive second-derivative condition holds. These equations are reused in actuarial annuity and pension schemes. The mission formalises genuine financial relationships as a graph: compound accumulation leads to discount factors, then discounted cashflow valuation and rate derivatives, ending with a strict local minimum argument. The latter is more substantial than algebraic definition expansion.
Theorems must preserve distinctions between interest and discount rates and between annuities in advance and arrears. Positive accumulation is essential where inverse factors are cancelled or differentiated. Loan prospective value must include only payments remaining after the valuation date. Duration is a ratio whose denominator must be nonzero. Redington immunisation is a genuinely local twice-differentiable result requiring matched PV, first derivative and strictly positive second derivative at an interior yield. It does not provide protection from arbitrary nonparallel yield-curve shifts or sufficiently large interest-rate movements. A proof must establish smoothness of the finite rational cashflow surplus near i₀, rather than assuming local minimisation as a hidden premise.
The model is deterministic finite cashflow financial mathematics. Mortality-weighted uncertain payments can later be inserted as expected cashflow amounts. Explicit coupon, redemption, loan and annuity terms share the same discounting convention. The capstone uses the actual finite asset-minus-liability discounted cashflows. This is a flat-yield Redington local test only. It is mathematically strong and may be difficult to complete because the second derivative theorem requires calculus and finite-sum differentiability, but no artificial axiom or proof placeholder may count as a solved result.
These are original derived finite/analytic CM1 formalisation targets rather than reproductions of a numbered textbook theorem. Exact Lean binder declarations are authoritative. The complete source uses targeted Mathlib imports and no local Lean compilation. All proof bodies remain genuinely open and do not constitute accepted results. Assumptions about negative rates, survival, policyholder independence, discounting and benefit timing must be preserved exactly.
A defined benefit pension commencement lump sum cannot generally be determined by multiplying the pre-commutation pension by a cash conversion factor without considering the remaining pension. HMRC's Pensions Tax Manual PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) establishes the applicable amount for a DB arrangement and gives a simplified exact solution 20fg/(20+3f) when the pension is partially surrendered at commutation factor f. PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) identifies other statutory allowance restrictions. This mission formalises the HMRC arithmetic under explicit assumptions, and then extends the model to separate pension tranche reductions rather than pretending all pensions must use a single commutation factor.
Let g denote the annual pension before commutation, L the pension commencement cash and f the cash paid per pound of annual pension surrendered. The remaining annual pension is P_B=g−L/f. For the simplified DB arrangement with no disqualifying pension credit and no other relevant linked lump sum, the statutory test becomes 3L≤20P_B. Solving this with f>0 gives the maximum applicable cash L_max=20fg/(20+3f). A real value A can represent an externally determined available allowance, giving the capped amount min(L_max,A). For a collection of tranches, annual reduction x(i) and individual cash factor f(i) generate cash contributions f(i)x(i). The residual annual pension is the sum of P(i)−x(i).
The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.
The named result ActuarialValuation.dbCommutedPension_zero_cash captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. If no pension is commuted, the original annual DB pension remains unchanged. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.dbCappedPCLS_le_max captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The allowance cap cannot increase cash above the base applicable amount. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.dbPCLSMaximum_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone proves the attained basic HMRC cash limit, verifies the allowance-limited cash remains admissible, and retains a nonnegative pension tax headroom. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.
The equations are financially useful because the HMRC basic limit depends on the annual pension remaining after cash has been commuted. Using the original pension instead of P_B would overstate the permitted amount. HMRC PTM063240 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063240) gives the explicit formula and examples, while PTM063230 (https://www.gov.uk/hmrc-internal-manuals/pensions-tax-manual/ptm063230) explains the allowance components of the permitted maximum. The formal result provides a check of cash amount, pension reduction, binding constraint and residual HMRC headroom. Separate tranche cash and residual pension definitions are appropriate when benefit tranches have different commutation factors and noncommutable components. They will support more advanced finite optimisation and pension rights constraints.
Cross multiplication and the residual pension test require f strictly positive. Without this, division by f does not correspond to a legal pension surrender and reversed inequality steps are possible. The formula L_max is required to attain zero HMRC headroom in the simplified case, and every lower nonnegative cash amount must satisfy the same basic maximum relation. Allowance caps must themselves be nonnegative to preserve a nonnegative paid amount. An actual arrangement can also have disqualifying pension credits, other linked lump sums, protected rights, scheme minimum pensions or a finite available lump sum and death benefit allowance. The reduced mathematics must not be misrepresented as covering these cases automatically.
The Lean model uses exact real arithmetic for the single-factor formula and finite sums for the separate-tranche amounts. It proves basic nonnegativity, monetary identities, headroom monotonicity, the cash upper bound and an allowance-capped admissible solution. Noncommutable GMP and scheme-specific rules are deliberately outside this first formal capstone, with reductions of zero available as an abstract representation of such tranches. The external allowance input does not calculate a member's statutory tax allowances. This limits the formal claims to the HMRC simplified applicable-amount formula, while providing separate tranche arithmetic that a subsequent mission can enrich with survivor minimums, GMP guarantees and more involved cash waterfalls.
Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.
The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.
Defined benefit pension schemes may contain multiple legally different benefit tranches. Their pension increases, retirement ages, survivor benefits, guarantees and death-in-deferment provisions need not be identical. Applying one arithmetic average factor to a total pension would ignore differences in complete present value. The controlled UK DB Retirement Factors Mathematical Framework (2026, Chapter 18, equations 58–60) specifies a separately derived factor for each tranche, and treats a shared factor only when scheme provisions actually permit it. Dickson, Hardy and Waters (2009, Pension mathematics, Chapter 9, https://doi.org/10.1017/CBO9780511800146) explain pension cashflows and service-table valuation. This mission defines formal monetary equivalence for every tranche separately, retaining each actuarial package.
Take a finite number n of pension tranches. For each index i, P(i) denotes accrued annual pension measured in pounds per year, A(i) the complete early-date immediate retirement package value in annuity years, and D(i) the alternative normal-retirement comparator in the same units. Each package can itself be the sum of discounted expected payments at tranche-specific dates. The individual factor f(i)=D(i)/A(i) is applied only to the original pension in tranche i, giving R(i)=P(i)f(i). Its immediate monetary value is R(i)A(i). Total retirement pension and total actuarial liability must be formed by summing their respective tranche contributions. The model never substitutes a pension-only average factor.
The following declarations are original derived results, not direct quotations of numbered textbook or statutory theorems. Exact hypotheses and corner cases are fixed by the formal Lean statements.
The named result ActuarialValuation.trancheAnnuityLedgerValue_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. A tranche with no ledger payment dates has zero immediate package value. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.trancheSchemePension_zero captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. No tranches means no payable scheme pension. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
The named result ActuarialValuation.separateTrancheFactors_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone asserts per-tranche and aggregate monetary equivalence simultaneously, without computing or applying a common averaged factor. In the published mission the exact Lean binders and all positivity conditions determine the actuarial model. This proposition is a new derived finite or real-algebraic statement and is not asserted to be a numbered theorem in a pension statute.
Additional supporting theorems establish cancellations, finite-sum identities, positivity and uniqueness. In all cases the generated formal theorem type rather than an informal diagram is authoritative.
Tranche-specific monetary valuation is crucial for pension administration, where two pensions with identical nominal amounts may carry different spouse percentages, indexation and normal retirement dates. The actuarial cost of each unit of pension can consequently vary, and the conditions for equivalence differ. Dickson, Hardy and Waters, pension mathematics (2009, https://doi.org/10.1017/CBO9780511800146), provides the standard actuarial valuation background, while the UK retirement-factor framework 5.3.0 demonstrates the particular multi-tranche application. The resulting identity is useful in migration audits, administering benefit rectifications, reconciling aggregate valuation, and checking that rounding or source ordering has not silently changed benefit values. Separate original benefit rights remain authoritative.
The denominator A(i) must not vanish when cancelling the value ratio. In particular, the real-number convention that division by zero has a defined total Lean value does not make its ordinary actuarial quotient meaningful. Even when total monetary values happen to match, separate per-tranche equality cannot be inferred without additional assumptions. The formal task must retain all individual tranche indices and not count a benefit twice. Zero pension tranches, empty pension schedules and appending another tranche are meaningful cases, rather than mathematical errors. Every unit package must be valued on its own scheme-rule basis, including its relevant discount and contingent cashflows.
The declarations use exact real arithmetic and finite sums. In particular, the discount, survival, pension increases, guarantee and survivor entitlement details may be assembled into each package ledger as inputs. Their stochastic derivation is an additional task and not silently asserted by a generic real-valued annuity factor. The central identity is P(i)f(i)A(i)=P(i)D(i), and the whole scheme result sums these monetary equivalence equations over finite tranches. The derived calculation remains exact before administration rounding, with no common average factor theorem and no claim that all tranches have the same normal retirement age. It is a reusable base for more detailed pension option missions.
Existing actuarial valuation theory gives the financial identities motivating these new formal obligations, but the exact original Lean declarations have no accepted proofs yet. The proposed capstone is nontrivial because arbitrary benefit dates, positivity hypotheses and boundary cases cannot be excluded or replaced with a degenerate zero-cashflow special case. The algebraic components are reusable in future UK scheme valuation and administration missions. For source interpretation, a valuation basis means the explicit package assumptions and a benefit constraint means a scheme-specific rule, not an implicit mathematical axiom.
The pinned Mathlib revision is 0df444a360eaa60ab8c11dca51a86af692955474. All source declarations use targeted imports, with no unrelated namespace opening. An authoring compilation with open sorry targets checks source elaboration but does not prove a mathematical statement. The full actuarial benefit schedule may require further scheme-specific data beyond this theorem graph.