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.
Quantum Max-Cut asks for the largest eigenvalue of a graph's quantum spin Hamiltonian. For a graph with nonnegative rational edge weights, write
This campaign tracks expected approximation ratios for classical polynomial-time energy estimation. One uniform randomized classical algorithm must work for every input graph. For each fixed , let be the algorithm's internal fair random bits, and let be its nonnegative rational output. A ratio requires
The expectation averages the algorithm's internal randomness on a fixed graph. Its running time is bounded by a polynomial on every run. Higher ratios are better.
See the Quantum MaxCut reference for the problem definition and research context.
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?
The main conjecture of Iwasawa theory is an identity between two objects attached to an odd prime and the tower of cyclotomic fields : an algebraic object built from the -parts of their ideal class groups, and an analytic object, the Kubota–Leopoldt -adic -function, which interpolates special values of Dirichlet -functions (generalized Bernoulli numbers). It was formulated by Iwasawa, partly by analogy with Weil's description of the zeta function of a curve over a finite field through the action of Frobenius on its Jacobian: the group plays the role of Frobenius, the inverse limit of class groups plays the role of the Jacobian, and the -adic -function plays the role of the zeta function.
Timeline:
Fix an algebraic closure and a prime . For let (Lean: F p n), and let (Lean: A p n) be the -primary part of the ideal class group of ; by class field theory , with the -Hilbert class field of . The Iwasawa module is
the inverse limit along the norm maps (Lean: Hinf p). It is a -module with a continuous action of through , . Put (Lean: V p).
The cyclotomic character sends to the unique with for every -power root of unity . The subgroup consists of the elements whose character is a -st root of unity, and on the Teichmüller character is . Let be the -eigenspace of on (Lean: eigenspace p i). Let , let be a topological generator, and let be its cyclotomic character: . Let , the characteristic polynomial of on written in the Iwasawa variable (Lean: charPoly p i γ).
On the analytic side, is the generalized Bernoulli number of a character modulo . The Kubota–Leopoldt -adic -function satisfies for , and is the power series with (Lean: IsIwasawaPowerSeries p u j G).
For every odd integer ,
The main conjecture describes the Galois-module structure of the class groups in the whole cyclotomic tower by -adic -functions. The Herbrand–Ribet theorem and the Gras conjecture follow quickly from it, and its generalizations (totally real fields, CM fields, elliptic curves and modular forms, the latter by Skinner–Urban) feed into results on the Birch–Swinnerton-Dyer conjecture. The theorem has been proved (Mazur–Wiles 1984); no machine-checked proof is known. A formal proof requires Iwasawa's structure theory of -modules, the construction of -adic -functions, and either the Eisenstein-ideal argument of Mazur–Wiles or Rubin's Euler-system argument. Each of these is reusable well beyond this mission.
One divisibility can be reduced, via the analytic class number formula, to the other. The hard direction is to show that the characteristic ideal of the class-group side is divisible by the -adic -function. Stickelberger's theorem gives only annihilation, not the characteristic ideal. Divisibility needs a construction of many unramified abelian -extensions: Ribet's method with Galois representations attached to cusp forms congruent to Eisenstein series, or Kolyvagin–Rubin Euler systems. Neither is in Mathlib today.
AlgebraicClosure ℚ generated by the roots of . The groups are the -primary components of ClassGroup (𝓞 (F p n)); the norm maps come from Ideal.relNorm, and the Galois action comes from mapping ideals. The Hilbert class field does not appear: the source's own identification is used.The Selmer group is the main computable invariant attached to the rational points of an elliptic curve (more generally, of an abelian variety) over a number field. J. W. S. Cassels named it in honour of E. S. Selmer, whose numerical work on the curves exposed the limits of descent methods (Selmer 1951). For an elliptic curve over a number field and an integer , the -Selmer group is a finite group, computable in principle, which contains and whose remaining part is the -torsion of the Tate–Shafarevich group . Finiteness of the Selmer group is the cohomological core of the weak Mordell–Weil theorem, and hence of the Mordell–Weil theorem that is finitely generated.
Timeline.
Let be a number field with algebraic closure and absolute Galois group , a profinite group with its Krull topology. Let be an elliptic curve over , given by a Weierstrass equation, and let . For a field write for the group of -points and for the -torsion of ; the group acts on both.
For a topological group acting on an abelian group (regarded as discrete), the continuous first cohomology is the group of locally constant maps with , modulo the maps .
For each place of (finite or infinite), let be the completion, , and fix a -embedding ; it induces the restriction and . The local Kummer map is
The -Selmer group is
and the Tate–Shafarevich group is the set of classes in whose restriction to every is trivial.
The result. Finiteness of gives, through the exact sequence, finiteness of (weak Mordell–Weil) and of . Combined with the theory of heights it yields the Mordell–Weil theorem. The Selmer group is also the object that descent algorithms compute, and the starting point of Iwasawa-theoretic and Bloch–Kato generalisations.
Formalizing it. The finiteness theorem is classical (see e.g. Silverman, Ch. X). A complete development produces continuous Galois cohomology of elliptic curves over number fields, the Kummer sequence, local conditions at all places, and a formal weak Mordell–Weil theorem for arbitrary number fields and arbitrary .
The group itself is infinite, so finiteness can only come from the local conditions, and conditions at all places must be used. The essential input is global arithmetic: the finiteness of the class group and the finite generation of the unit group of a ring of -integers of a finite extension of . The local analysis (behaviour of the Kummer image at places of good reduction not dividing ) and the profinite cohomology must both be built for elliptic curves before that input can be applied.
WeierstrassCurve K with [E.IsElliptic]; is a NumberField. The source treats an isogeny of abelian varieties; this mission specialises to elliptic curves and to the isogeny , .Field.absoluteGaloisGroup L with its Krull topology. is defined from scratch as locally constant 1-cocycles modulo coboundaries (discrete coefficients).v.adicCompletion K; infinite places are InfinitePlace K with completion w.Completion. Restriction uses a fixed embedding chosen by IsAlgClosed.lift.The nontrivial zeros of the Riemann zeta function control the distribution of the prime numbers: the explicit formula expresses the error in the prime number theorem as a sum over these zeros. Almost every quantitative argument about primes therefore needs to know how many zeros there are up to a given height. The Riemann–von Mangoldt formula answers this question, and it is used throughout analytic number theory: in explicit prime-counting estimates, in zero-density arguments, in numerical verifications of the Riemann hypothesis, and in the study of the spacing of zeros.
Timeline.
The Riemann zeta function , defined for , extends to a meromorphic function on with a single pole at . Its zeros with positive imaginary part all lie in the critical strip . For real , the zero-counting function is
where each zero is counted with its multiplicity. The main term is
For a positive integer and a Dirichlet character modulo , is the analytic continuation of , and counts, with multiplicity, its zeros with and . The Lindelöf hypothesis asserts for every , and the Riemann hypothesis asserts that every nontrivial zero has real part .
This asserts only the shape of the asymptotics, with no numerical constants, so it remains valid however the explicit constants are later improved.
For every primitive character modulo and , uniformly in and :
The result itself. The formula shows that the zeros up to height number about , and that their mean spacing at height is . It is the normalisation behind pair-correlation statistics, the input that turns zero-free regions into error terms for the prime number theorem, and the bound that makes sums over zeros in the explicit formula converge. Explicit forms such as Backlund's and Hasanalizade–Shen–Wong's are what numerical work uses: they convert a verified count of zeros up to a height into rigorous statements about primes.
Formalizing it. All the targets are classical, proved theorems; none of them is open. What remains is a machine-checked development: the zero-counting function for Mathlib's riemannZeta, the asymptotic formula, its explicit and conditional forms, and the Dirichlet -function analogue. The platform already contains a related dyadic-window statement for that is conditional on Stirling-type hypotheses. This mission targets the unconditional cumulative count in its standard form.
The obvious approach counts zeros with the argument principle around the rectangle with vertices , , , , using the completed function . The contributions of the Gamma factor and of the right-hand edge are routine. The step that does not go through directly is the top edge: one must show that the change in along is . A naive bound on gives no control of the argument. The classical arguments bound the number of sign changes of on the segment (Backlund's trick via Jensen's formula), or use the Hadamard product with a local zero count. Both need growth estimates for in the strip, Stirling's formula for complex , and a careful treatment of that is the ordinate of a zero. For the explicit bounds, every one of these steps must be carried out with numerical constants. The conditional refinements need the Selberg-type analysis of .
riemannZeta, is DirichletCharacter.LFunction, primitivity is DirichletCharacter.IsPrimitive, and the Riemann hypothesis is Mathlib's RiemannHypothesis.zetaZeroCount) and (dirichletZeroCount) are finite sums of multiplicities (analyticOrderNatAt) over the zeros in the open critical strip, with imaginary part in and respectively. Zeros on the line are counted.finsum over an infinite set would be , so a solver must prove finiteness.Asymptotics.IsBigO / IsLittleO along Filter.atTop. The Lindelöf hypothesis is the one-sided form as , which is equivalent to the two-sided form by conjugate symmetry.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.
Every closed oriented 3-manifold bounds a compact oriented 4-manifold, but asking for a bounding 4-manifold with the homology of a point turns this into one of the long-standing questions of 3/4-manifold topology. The question, recorded on the Open Problem Garden as an outstanding problem of ancient/folklore origin, is whether there is a complete and computable set of invariants that determines which (rational) homology 3-spheres bound (rational) homology 4-balls (Open Problem Garden).
The question organizes the homology cobordism group (integral homology spheres modulo homology cobordism): an integral homology sphere represents zero in exactly when it bounds a smooth integral homology ball. It is also tied to the slice-ribbon problem, listed on the Open Problem Garden as a related problem.
Timeline (as recorded in the source's bibliography).
A closed topological 3-manifold is a compact Hausdorff space locally homeomorphic to . Write and for singular homology. is an integral homology 3-sphere if for all , and a rational homology 3-sphere if the same holds with coefficients.
A smooth integral homology 4-ball is a compact smooth 4-manifold with boundary such that for all ; a rational homology 4-ball is defined with coefficients. bounds if the manifold boundary is homeomorphic to .
The Brieskorn manifold is an integral homology sphere when are pairwise coprime; is the Poincaré homology sphere . The lens space is the quotient of by the -action generated by , .
To speak of algorithms, a 3-manifold is presented by a finite simplicial complex , a list of simplices each given as a list of vertex labels in , with geometric realization . Every closed 3-manifold is triangulable (Moise).
A complete and computable set of invariants is, in particular, a decision procedure; conversely a decision procedure is itself a complete computable invariant. The goal is stated for integral homology spheres and integral homology balls (the title question).
A decision procedure would settle membership in the zero class of for every presented homology sphere. Without one, each new example requires an ad hoc construction (to show bounding) or an obstruction (to rule it out). The known obstructions — the Rokhlin invariant, Siebenmann's -invariant, the Ozsváth–Szabó -invariant and others — are spin or spin cobordism invariants and are not known to be complete.
None of the milestone results is formalized in Lean. Formalizing even the milestones requires substantial infrastructure (smooth 4-manifolds with boundary, intersection forms, Rokhlin's theorem, explicit handle constructions), which is reusable well beyond this mission.
The answer to the goal is unknown; a disproof (undecidability) would equally resolve the mission. On the obstruction side, every known invariant is a homology cobordism invariant that is computable for special families but not known to detect bounding in general. On the construction side, homology balls are produced by explicit handle decompositions with no general recipe. The topological category is no substitute: by Freedman's work every integral homology 3-sphere bounds a contractible topological 4-manifold, so the problem lives entirely in the smooth category.
The generalized Poincaré conjecture asks whether a closed -manifold with the homotopy type of the sphere must be the sphere. In the topological category (conclusion: homeomorphic) it is now known in every dimension: classically, by Smale (and Stallings, Newman), by Freedman (1982), and by Perelman (2003). In the smooth category (conclusion: diffeomorphic) it fails in general: Milnor (1956) found exotic smooth structures on , and Kervaire–Milnor showed that exotic spheres exist in many dimensions. The single case that remains completely open is the smooth one in dimension ; the Open Problem Garden rates it Outstanding.
All manifolds are Hausdorff, compact, without boundary and smooth (). The model sphere is with its standard smooth structure. Two spaces have the same homotopy type if there is a homotopy equivalence between them.
This is the conjecture exactly as stated in the source.
By Freedman's theorem a homotopy 4-sphere is already homeomorphic to , so the conjecture is equivalent to the statement that has no exotic smooth structure. It would complete the generalized Poincaré conjectures in the smooth category in the one dimension where the answer is unknown. A disproof would give the first exotic smooth structure on a closed simply connected 4-manifold with small homology.
The h-cobordism technology that settles dimensions (the Whitney trick) fails in dimension 4. Freedman's topological methods give a homeomorphism but no smoothing, and gauge-theoretic invariants (Donaldson, Seiberg–Witten) give no information on homotopy 4-spheres. Many candidate counterexamples (Gluck twists, Cappell–Shaneson spheres) have since been shown to be standard.
Manifolds use Mathlib's ChartedSpace (EuclideanSpace ℝ (Fin n)) M together with IsManifold (𝓡 n) ∞ M. The model with corners 𝓡 n has no boundary, and ∞ means (not analytic). The sphere is Metric.sphere (0 : EuclideanSpace ℝ (Fin (n+1))) 1 with Mathlib's standard smooth structure. A homotopy equivalence is ContinuousMap.HomotopyEquiv, and diffeomorphisms are Diffeomorph (≃ₘ^∞⟮𝓡 n, 𝓡 n⟯). Closedness is CompactSpace plus T2Space; second countability follows from compactness. The milestones are the known results the source cites: low dimensions, Perelman, Smale, Milnor's exotic spheres, Freedman, and the continuum of exotic 's. They also include the equivalent reformulation "there is no exotic ". Formalizing any of them requires substantial new manifold-topology infrastructure in Mathlib, and that work is welcome.
The Schoenflies problem asks whether a codimension-one sphere sitting smoothly inside a sphere can be knotted. In every dimension except one the answer is known to be "no"; the remaining case, a smooth -sphere in , is listed as an outstanding problem in the Open Problem Garden (source). It is one of the central open questions of smooth -manifold topology, closely tied to the existence of exotic smooth structures on the -ball and to the smooth -dimensional Poincaré conjecture.
Timeline.
For let be the unit sphere with its standard smooth structure, and let be the closed unit ball. In the Lean development is Sph n.
A smooth embedding is a map that is injective and whose differential is injective at every point (an injective immersion; since is compact this is an embedding). Its image is a smooth -dimensional submanifold of diffeomorphic to (Lean predicate IsSmoothEmbeddingSph n f).
By the Jordan–Brouwer separation theorem, has exactly two connected components, and is the frontier of each. Their closures are compact connected -manifolds with common boundary .
A subset is a smoothly embedded closed ball if it is diffeomorphic to (with the smooth structure inherited from ). Concretely, for a map that is injective on and has injective differential at every point of , boundary points included (Lean predicate IsSmoothClosedBallIn n K). The topological counterpart, homeomorphic to , is IsTopClosedBallIn n K.
For every smooth embedding and every point , writing for the connected component of containing ,
Equivalently: is unknotted.
The result itself. By milestone 2, always bounds two topological -balls. So a counterexample to the goal would produce an exotic smooth structure on that embeds in ; a proof would show that no exotic , if one exists, embeds in . The problem is related to, but independent of, the smooth -dimensional Poincaré conjecture. For example, the Poincaré conjecture could hold while carries an exotic smooth structure. The goal also completes the uniform statement "every smooth is unknotted" across all dimensions.
Formalizing it. The goal is open. Milestones 1–5 are classical theorems, and no existing machine-checked proof of them for smooth spheres is relied on here. Formalizing them is substantial independent work and would add basic infrastructure to Mathlib's manifold library: separation theorems, collars, and smoothing of balls.
The topological statement is known in every dimension (milestone 2), so the difficulty is purely smooth. In dimensions the passage from "homeomorphic to a ball" to "diffeomorphic to a ball" goes through the -cobordism theorem. That theorem fails in the smooth category in dimension , because the Whitney trick is unavailable. Freedman's topological methods do not control smooth structures. The naive approach is to apply the high-dimensional argument verbatim, and this breaks at exactly this step. Known partial results (Scharlemann) need strong restrictions on the embedding, such as genus bounds or few critical points of a height function.
EuclideanSpace ℝ (Fin (n+1)), with Mathlib's standard smooth manifold structure modelled on EuclideanSpace ℝ (Fin n). Smoothness means (ContMDiff … ∞), not analytic.mfderiv everywhere). This is equivalent because is compact.connectedComponentIn (Set.range f)ᶜ x for . The conclusion is required for every such , so for both sides of .mfderiv, which is not injective.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.
Retiring earlier changes the number of pension payments and may introduce payments before normal retirement age. Retiring later removes some payments but may entitle the member to an uplift and missed increases. A defensible actuarial equivalence calculation compares complete benefit packages, including contingent benefits, at the same valuation date. The UK DB Retirement Factors Mathematical Framework 5.3.0 (2026, Chapters 8 to 11) explicitly treats early and late benefit routes, guaranteed periods, pension increases and pre-commencement death. Dickson, Hardy and Waters (2009, Chapter 9, https://doi.org/10.1017/CBO9780511800146) provide independent actuarial pension valuation background. This mission first formalises a carefully delimited factor-independent death-benefit model and retains explicit differences between pure and total late-retirement factors.
For early retirement, A_E is the immediate retirement package, D_E the normal retirement comparator, and F_E=D_E/A_E the unrounded reduction factor. The comparator may contain a death-before-retirement component plus survival-to-normal-age probability p times an appropriate discount v and normal pension annuity A_N. For late retirement N is the value of the benefit package at normal retirement, D the value of death benefits payable while commencement is postponed, and A_L the immediate package at the late date. The positive multiplier m represents pension increases that would otherwise have accrued while in payment. The pure LRF F_L solves N=D+pvm A_L F_L. The total pension multiplier M_L=mF_L includes both late uplift and missed increases.
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.pensionEarlyComparator_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. Nonnegative disjoint death and surviving deferred-annuity route values yield a nonnegative comparator. 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.pensionLatePureFactor_nonneg captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The net value available for deferred pension is nonnegative once factor-independent death costs are deducted. 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.pensionRetirementEquivalence_fundamental captures the relevant actuarial relationship. Original derived theorem for UK DB pension valuation. The capstone validates both early and late monetary equivalence and proves that the pure factor and total missed-increase multiplier represent the same late pension liability. 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 distinction prevents a common implementation error: treating the total missed-increase pension multiplier as the pure actuarial LRF and then applying increases a second time. The financial basis and cashflow boundaries must be stated before taking an algebraic ratio. The UK retirement factor methodology v5.3.0 details the pension ledger and explicitly separates pure and total late multipliers. Pension mathematics and contingent annuities in Dickson, Hardy and Waters (2009, https://doi.org/10.1017/CBO9780511800146) explain the broader framework. The resulting small formal theorem can be combined with exact-dated benefit ledgers and numerical models to test early and late valuation reconciliation before rounding. That reuse is important when individual tranches have different dates and benefit conditions.
Both ratio definitions need nonzero annuity packages or survival-weighted denominators. If normal survival probability is zero, a late pension cannot compensate financially in the ordinary quotient model, and Lean division must not hide that failure. The death benefit during late postponement is assumed independent of the eventual pure factor, an explicit limitation. Factor-dependent death benefits require solving a different potentially nonlinear root equation; simply dividing a fixed numerator would be wrong. Increases accrued while waiting are distinct from in-payment increases already present in A_L. All route components are valued at a common date, and different death and survival outcomes are treated as disjoint events.
The theorem graph establishes early comparator positivity, factor existence and uniqueness, and exact equivalence when an annuity denominator is nonzero. It separately proves late pension value and uniqueness under the corresponding nonzero survival-discount-increase-annuity product. The capstone reconciles the early option and the two equivalent late expressions: using the pure late factor and using the total multiplier mF_L. The underlying cashflow package values are abstract real inputs, which enables later missions to supply actual discounted mortality-weighted schedules. The current restricted identity does not claim to model every dependant, guarantee, calendar increase or factor-linked death benefit. Scheme-specific cashflow rights remain controlling.
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.
Philosophers of physics ask when a formulation of a theory carries excess structure: mathematical distinctions between models that make no physical difference. The standard example is electromagnetism written with a vector potential . Potentials that differ by a gauge transformation have the same field strength , and on the usual view they represent the same physical situation.
Weatherall (2016) made this precise with category theory. Each formulation becomes a category of models, and a translation between formulations becomes 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. Weatherall's Proposition 1 says the functor from potentials to field strengths forgets only structure, provided the arrows between potentials are spacetime symmetries that preserve . His Proposition 2 says the principal-bundle formulation, whose arrows include gauge transformations, forgets nothing. His footnote 15 notes that adding gauge transformations as arrows between potentials yields a category equivalent to that of field strengths (Weatherall, arXiv:1411.5757).
These arguments work on Minkowski space, which is contractible. Weatherall's footnote 9 sets topology aside for that reason. The follow-up literature, for example Nguyen, Teh and Wells (2018), compares these and related functors further. This mission states the comparison exactly on a finite cell complex, where topology cannot be set aside. Each of the three ways a functor can forget information then corresponds to one cohomology group.
A finite oriented 2-complex has vertices, edges and faces, together with integer incidence numbers and satisfying for every face and vertex . Nothing beyond this identity is required, so the incidence data need not come from a geometric complex; all results hold for any such integer data. Fix an additive commutative group of coefficients, for example , , or as a discrete stand-in for . The cochains are (gauge parameters ), (potentials ) and (field strengths ). The coboundaries are
and .
There are three categories, with spacetime symmetries taken to be trivial:
The field-strength functors and send . In the second functor every gauge arrow goes to an identity.
Cohomology vanishing is stated elementarily:
For every finite 2-complex and coefficient group , the functor satisfies
circle3 with coefficients, the potential equal to on one edge has the same field strength as . No gauge arrow connects the two, so the functor is not full.The result. The classification turns a qualitative philosophical diagnostic into a cohomological criterion.
Formalizing it. No machine-checked version of the theories-as-categories programme for gauge theory is known to the author of this mission. This mission is the base case of a planned discrete gauge-functor development: non-abelian groups, nontrivial symmetry groups, and holonomy-based equivalences.
The mathematics is elementary once stated. The work is in making the categorical notions line up with the cochain conditions. Three points need care:
The concrete milestones require computations on explicit complexes, including a gauge-invariant obstruction for the Aharonov–Bohm example.
Fin types, and the incidence numbers are integer-valued. The complex is finite but may be empty in any dimension.AddCommGroup, and integers act on it by zsmul.Fld and Pot0 are Mathlib Discrete categories. PotG carries a hand-written Category instance whose arrows are the structure GaugeHom.Functor.Full, Functor.Faithful and Functor.EssSurj.delta0, delta1, ) is proved in the definitions file and is reusable for discrete gauge theory and toric-code missions.The Bühlmann–Straub credibility method allocates weight to individual observed claims experience according to total exposure and variability. It balances the expected value of process variance EPV with the variance of hypothetical means VHM. More exposure raises the statistical information carried by the policyholder's observed rate and should weakly improve the resulting optimal linear prediction error. The established credibility formula and its interpretation are developed in Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). The new mission formalises how these exact deterministic weight and risk formulae change with exposure.
Let P be a nonnegative real representing total risk exposure. EPV is strictly positive, while VHM is nonnegative and may equal zero for a homogeneous risk class. The credibility factor Z(P) is P times VHM divided by the sum of P times VHM and EPV. A credibility premium combines the policyholder's experience rate with the collective mean using weights Z(P) and 1-Z(P). A normalised optimal quadratic prediction error is EPV times VHM over the same positive denominator. A scaled quadratic expression captures the trade-off between random process noise and between-risk heterogeneity.
The formal targets progress from structural boundary identities to financial sensitivity and the full capstone. Supporting theorems remain genuine Open declarations until accepted Lean proofs are submitted; no previously accepted proof is silently assumed.
The exact theorem name is ActuarialValuation.exposureCredibilityWeight_zero. Without any exposure, the experience credibility weight must be zero, provided the process variance is strictly positive.
The exact theorem name is ActuarialValuation.exposureCredibilityPremium_between. As the credibility weight lies in the unit interval, a lower observed claim rate produces a premium bounded by the observed and collective rates.
The exact theorem name is ActuarialValuation.exposureCredibilityAccuracy_fundamental. The capstone reconciles exposure-driven increases in credibility with the monotone decline of minimum expected squared error, including the zero heterogeneity boundary.
The graph also contains separately stated supporting inequalities and exact definitions, with the intended original derived mathematical identity written out in every milestone.
Experience-rating systems can be checked for sensible monotonicity when an additional policy year or risk exposure enters the rating base. Larger exposure should not decrease the weight assigned to otherwise unchanged policy experience and should not increase the theoretically optimal error. The classical structure of Bühlmann credibility and its use of EPV and VHM are described by Loss Data Analytics (https://openacttexts.github.io/LDAVer2/ChapCredibility.html). These precise algebraic statements are reusable for downstream weighted risk models, rating systems and numerical sensitivity checks.
Credibility is a rational function whose denominator could vanish under an invalid zero-process-variance model. The hypotheses impose strictly positive EPV and retain zero VHM as a legitimate boundary. Monotonicity is therefore weak, not strict, since a homogeneous portfolio provides no justification for relying more on experience. Comparisons between two exposures must use the same structural parameters, otherwise a change of class could reverse the effect. The theorem relating quadratic risk and the credibility weight is a genuine completing-square identity, while the mission does not assert that an arbitrary Bayesian posterior has linear form.
Lean uses exact real arithmetic for exposure, EPV, VHM, premium and risk formulae. The finite statistical model is reduced to its deterministic structural-parameter consequences; estimation of the parameters and robustness of individual claims are outside the scope. The theorem graph begins with positivity and zero-exposure boundaries, continues through weight and premium identities, and ends with a conjunction linking increasing credibility to decreasing minimal prediction error. The mathematical framework is known, but the newly stated Lean specialisations have to be proved and exclude vacuous denominator cases.
The pinned Mathlib revision and the precise Lean type of each definition or proposition are authoritative. The imported source must use targeted Mathlib modules; one large aggregate compiler check never substitutes for testing individual definition imports and obsolete namespace openings. The source-specific intermediate statements separate units and hypotheses. The finite index always counts claims, scenarios, or observations according to the declaration, not an implicit probability measure. In an insurance pricing setting the difference between a gross loss, a ceded payment, a net premium and a credibility risk estimate is financially important. A positive coefficient does not by itself imply the coefficients sum to one. Likewise a deterministic algebraic identity does not grant stochastic independence or a forecast model. These restrictions preserve the distinction between a purely algebraic result and a probabilistic interpretation. The formal theorem declarations have to maintain exactly the same quantifiers, arithmetic operations and endpoint conventions as the descriptions, including meaningful boundary cases. Future extensions can introduce richer distributions and dependence without altering the precise finite identities established here.
S. David Promislow, Fundamentals of Actuarial Mathematics, third edition, Wiley, 2015, printed page 489. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/
Frees and colleagues, Loss Data Analytics: Experience Rating Using Credibility Theory, 2024. https://openacttexts.github.io/LDAVer2/ChapCredibility.html