Missions · Prove2Me

Completed

Garrett Functional Analysis Notes I: Completeness and Quasi-completenessTextbook

Motivation

Completeness of a normed or metric space is the property behind most existence theorems in analysis: limits of approximations, fixed points, integrals. Many of the spaces that matter in analysis and in the theory of distributions are not metrizable, though: the space $C_c^\infty(\mathbb R^n)$ of test functions, weak-star duals, and spaces of operators with the strong or weak operator topology. For such topological vector spaces the right replacement for sequences is nets, and the plain notion "every Cauchy net converges" turns out to be too strong. Weak-star duals of infinite-dimensional Fréchet spaces, for example, never satisfy it.

Paul Garrett's lecture notes Completeness and quasi-completeness (PDF) argue that the right general notion is quasi-completeness: every bounded Cauchy net converges. They show that it holds for Hilbert, Banach, Fréchet and LF-spaces, for their weak-star duals, and for spaces of continuous linear maps with the topology of pointwise convergence. In the notes, one stated purpose is to justify Gelfand–Pettis integrals of compactly supported continuous functions with values in such spaces, for instance distribution-valued functions.

The results are classical. Boundedness in strict inductive limits goes back to Dieudonné and Schwartz, and the incompleteness of weak duals to Grothendieck (1950). See Bourbaki, Topological Vector Spaces, III.5, and Schaefer, Topological Vector Spaces.

Setting

All vector spaces are over $\mathbb K=\mathbb R$ or $\mathbb C$ and all topological vector spaces are Hausdorff. A set $B$ in a topological vector space $V$ is bounded if every neighbourhood of $0$ absorbs it. A net is a map $v:I\to V$ from a directed partially ordered set. It is Cauchy if for every neighbourhood $N$ of $0$ there is $i_0$ with $v_i-v_j\in N$ for all $i,j\ge i_0$ . $V$ is complete if every Cauchy net converges, and quasi-complete if every bounded Cauchy net converges.

A Fréchet space is a locally convex, metrizable, complete topological vector space. A locally convex space $V$ is the strict colimit of a chain $V_0\subsetneq V_1\subsetneq\cdots$ of subspaces if $V=\bigcup_n V_n$ , each $V_n$ is closed in $V_{n+1}$ , and the topology of $V$ is the finest locally convex topology inducing the given topology on every $V_n$ . Concretely, a balanced convex set $U$ is a neighbourhood of $0$ in $V$ as soon as every trace $U\cap V_n$ is a neighbourhood of $0$ in $V_n$ . An LF-space is a strict colimit of Fréchet spaces; $C_c^\infty(\mathbb R^n)$ is the standard example.

For topological vector spaces $X,Y$ , write $\mathrm{Hom}^o(X,Y)$ for the continuous linear maps $X\to Y$ with the topology given by the seminorms $p_{x,U}(T)=\inf\{t>0: Tx\in tU\}$ , for $x\in X$ and $U$ a convex balanced neighbourhood of $0$ in $Y$ . When $Y$ is locally convex this is the topology of pointwise convergence. A set $E$ of linear maps is equicontinuous if for every neighbourhood $U$ of $0$ in $Y$ there is a neighbourhood $N$ of $0$ in $X$ with $T(N)\subseteq U$ for all $T\in E$ .

Formalization targets

Goal: quasi-completeness of operator spaces (Theorem 4.1.1)

X \text{ Fréchet or LF},\quad Y \text{ locally convex and quasi-complete}\ \Longrightarrow\ \mathrm{Hom}^o(X,Y)\ \text{is quasi-complete.}

Supporting results (the milestones, in the order of the notes)

Bounded sets and equicontinuous sets in strict colimits are detected on the steps $V_n$ (Propositions 2.1.1 and 2.2.1).
Banach–Steinhaus for Fréchet and LF domains, its Baire-category form, and joint continuity of separately continuous bilinear maps on Fréchet spaces (Theorem 3.0.1, Remark 3.0.2, Corollary 3.0.3).
Sequential completeness implies completeness for nets in metric spaces (Proposition 4.0.1). Quasi-completeness of Fréchet spaces, of closed subspaces and of products. Strict colimits of quasi-complete spaces and test-function spaces are quasi-complete (Proposition 4.0.3 and the remarks around it).
The weak dual of $V$ is complete exactly when every linear functional on $V$ is continuous (Theorem 5.0.1), so weak duals of infinite-dimensional Fréchet spaces are not complete (Corollary 5.0.2). Weak duals of Fréchet and LF-spaces are nonetheless quasi-complete (Remark 5.0.3). The finest locally convex topology $V_{\rm init}$ and the weak-dual claims 5.0.4–5.0.7 are also included.

Significance

Theorem 4.1.1 makes the strong-operator and weak-operator topologies on bounded operators between Hilbert spaces quasi-complete, and does the same for operators out of test-function spaces. Combined with quasi-completeness of weak-star duals of LF-spaces (Remark 5.0.3), it is what lets vector-valued integration and Cauchy–Goursat-type complex analysis be applied to families of distributions and operators. Banach–Steinhaus for LF-spaces (Theorem 3.0.1) and the Dieudonné–Schwartz description of bounded sets (Proposition 2.1.1) are among the most frequently used facts about distributions.

Mathlib has the Banach–Steinhaus theorem for Banach spaces and barrelled spaces, the topology of pointwise convergence on continuous linear maps, weak duals, and the test-function space $\mathcal D(\Omega)$ . It has no general theory of strict inductive limits and no quasi-completeness results of this kind. This mission formalizes that layer: the results are proved on paper, not yet formalized.

Difficulty

The obvious argument for Theorem 4.1.1 takes pointwise limits. That gives a linear map, but continuity of the limit is the real issue: it needs equicontinuity of a merely pointwise-bounded net of operators, which is a Baire-category statement and fails for general domains. For LF domains the Baire argument does not apply directly, because an LF-space is never metrizable when the chain is strictly increasing. The argument has to pass through the steps $V_n$ , which needs the description of bounded and equicontinuous sets in a strict colimit. That description depends on each $V_n$ being closed in $V_{n+1}$ and uses Hahn–Banach separation.

Formalization scope

Definitions (namespace GarrettFA, shared by any later missions on these notes):

IsQuasiComplete 𝕜 E and IsNetComplete E follow the notes literally, with nets indexed by directed partial orders. The index type is taken in the universe of E, which is no restriction because Cauchy nets correspond to Cauchy filters.
IsEquicontinuousSet S encodes equicontinuity at $0$ as in §2.2.
IsStrictColimit 𝕜 F is a predicate on a chain F : ℕ → Submodule 𝕜 V and the given topology on V, and IsLFSpace and IsFrechetSpace are built from it. The steps carry the subspace topology from $V$ . By the Dieudonné–Schwartz theorem this is the same as giving the steps their own topologies, so the class of spaces is the source's.
IsInitTopology 𝕜 V says that the topology of $V$ is $V_{\rm init}$ . Its existence is a separate theorem item, which rules out a vacuous predicate.

Local convexity is real local convexity (LocallyConvexSpace ℝ, with IsScalarTower ℝ 𝕜), as in Mathlib's distribution theory. $\mathrm{Hom}^o(X,Y)$ is Mathlib's X →Lₚₜ[𝕜] Y. Its topology is the source's $p_{x,U}$ -topology because $Y$ is locally convex.

Two statements of the notes are corrected. Theorem 3.0.1 is stated there for arbitrary linear maps; it needs continuous ones, since a single discontinuous functional is pointwise bounded but not equicontinuous. Corollary 5.0.2 claims incompleteness of weak duals of all infinite-dimensional LF-spaces. That fails for the LF-space $\mathbb C^\infty$ of Example 1.3.1, whose topology is the finest locally convex one, so its weak dual $\mathbb C^{\mathbb N}$ is complete. The LF statement is therefore made for LF-spaces with an infinite-dimensional step. Proposition 1.3.5 is built into the formalization, where the steps are subspaces of $V$ .

Contributions of reusable infrastructure on strict inductive limits and barrelled spaces are welcome.

Selected references

P. Garrett, Completeness and quasi-completeness, lecture notes, 2014. http://www.math.umn.edu/~garrett/m/fun/notes_2012-13/07d_quasi-completeness.pdf
N. Bourbaki, Topological Vector Spaces, Chapters 1–5, Springer, 1987. https://doi.org/10.1007/978-3-642-61715-7
H. H. Schaefer, M. P. Wolff, Topological Vector Spaces, 2nd ed., Springer GTM 3, 1999. https://doi.org/10.1007/978-1-4612-1468-7
A. Grothendieck, Sur la complétion du dual d'un espace vectoriel localement convexe, C. R. Acad. Sci. Paris 230 (1950), 605–606.

28 thms2 active usersReviewed

Analysis Functional Analysis·Captain: Lucas

Invariant Subspace ProblemOpen Problem

Motivation

The invariant subspace problem asks whether every bounded linear operator on an infinite-dimensional separable complex Hilbert space leaves some non-trivial closed subspace invariant. It is listed as a high-importance open problem in analysis in the Open Problem Garden (entry) and is widely regarded as one of the most famous open problems in functional analysis. Invariant subspaces are the infinite-dimensional replacement for eigenvectors: in finite dimensions every complex matrix has an eigenvector, and the structure theory of matrices (triangular and Jordan forms) is built from chains of invariant subspaces. Whether any such structure is available for an arbitrary bounded operator on Hilbert space is exactly what the problem asks.

Timeline

1930s (von Neumann, unpublished). Compact operators on Hilbert space have non-trivial closed invariant subspaces.
1954 (Aronszajn–Smith). The compact case on arbitrary Banach spaces (doi:10.2307/1969637).
1966 (Bernstein–Robinson; Halmos). Polynomially compact operators on Hilbert space.
1973 (Lomonosov). Every non-zero compact operator has a non-trivial closed hyperinvariant subspace; consequently every operator commuting with a non-zero compact operator has a non-trivial closed invariant subspace (doi:10.1007/BF01080698).
1975 announced / 1987 published (Enflo). A bounded operator on a separable Banach space with no non-trivial closed invariant subspace (doi:10.1007/BF02392260).
1985 (Read). Such an operator on the classical space $\ell^1$ (doi:10.1112/blms/17.4.305).
2011 (Argyros–Haydon). An infinite-dimensional Banach space on which every operator is a scalar plus a compact operator, so that every operator on it has a non-trivial closed invariant subspace (arXiv:0903.3921).

The Hilbert-space question remains open.

Setting

Let $\mathbb{K}$ be $\mathbb{R}$ or $\mathbb{C}$ , let $E$ be a normed space over $\mathbb{K}$ , and let $T\colon E\to E$ be a bounded linear operator. A linear subspace $S\subseteq E$ is invariant under $T$ if $T(S)\subseteq S$ . It is a non-trivial closed invariant subspace if moreover $S$ is closed in the norm topology and $\{0\}\neq S\neq E$ . A closed subspace $S$ with $\{0\}\neq S\neq E$ is a non-trivial closed hyperinvariant subspace of $T$ if $A(S)\subseteq S$ for every bounded operator $A$ with $AT=TA$ .

A Hilbert space $H$ is a complete complex inner product space; it is separable if it has a countable dense subset. An operator $K$ is compact if it maps bounded sets to relatively compact sets, and $T$ is normal if $T^*T=TT^*$ . In the Lean development these notions are IsInvariantSubspace, IsNontrivialClosedInvariantSubspace, HasNontrivialClosedInvariantSubspace and HasNontrivialClosedHyperinvariantSubspace (namespace InvariantSubspaceProblem), together with Mathlib's IsCompactOperator and IsStarNormal.

Formalization targets

Goal: the invariant subspace problem

\forall\, H \text{ separable, } \dim H=\infty,\ \forall\, T\in\mathcal{B}(H):\quad \exists\, S\subseteq H \text{ closed},\ \{0\}\neq S\neq H,\ T(S)\subseteq S .

The source poses a yes/no question; the goal states the affirmative answer, and a formal proof of its negation equally settles the problem.

Milestones (known results)

Finite-dimensional case: every operator on a complex space of dimension $\ge 2$ has a non-trivial invariant subspace.
Non-separable case: every operator on a non-separable complex normed space has a non-trivial closed invariant subspace.
Normal operators on a complex Hilbert space of dimension $\ge 2$ .
Aronszajn–Smith: compact operators on infinite-dimensional real or complex Banach spaces.
Lomonosov: non-zero compact operators have non-trivial closed hyperinvariant subspaces.
Lomonosov: operators commuting with a non-zero compact operator.
Enflo: a separable infinite-dimensional complex Banach space with an operator having no non-trivial closed invariant subspace.
Read: such an operator on $\ell^1$ .
Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator is $\lambda I+K$ with $K$ compact.
Argyros–Haydon: a separable infinite-dimensional real Banach space on which every operator has a non-trivial closed invariant subspace.

Significance

The result itself. A positive answer would give every bounded operator on Hilbert space a non-trivial piece of structure and would be the first step towards triangular-form type theorems for general operators. A negative answer would, after Enflo and Read, show that even the Hilbert-space geometry does not force invariant subspaces. Either answer resolves a question that has organised much of operator theory since the 1930s.

Formalizing it. The goal is open; no proof, formal or informal, is known. The milestones are proved results whose formal proofs would build reusable infrastructure absent from Mathlib: the Aronszajn–Smith and Lomonosov theorems (the latter through Schauder's fixed point theorem), invariant subspaces from the spectral theorem for normal operators, and the large explicit constructions of Enflo, Read and Argyros–Haydon. None of these results is formalized in Mathlib at the time of writing.

Difficulty

The obvious approach, taking the closed linear span of an orbit $\{x, Tx, T^2x,\dots\}$ , fails exactly when every non-zero vector is cyclic, which is the situation that has to be ruled out; for separable spaces nothing prevents this a priori. Spectral methods fail because an operator can have a one-point spectrum and no eigenvectors (quasinilpotent operators). Methods that work on Hilbert space must use the inner-product structure in an essential way, since Enflo's and Read's examples show that the statement is false on some Banach spaces. Lomonosov's technique needs a non-zero compact operator in the commutant, which a general operator need not have.

Formalization scope

Hilbert spaces are Mathlib types H with [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]; separability is TopologicalSpace.SeparableSpace H and infinite dimension is ¬ FiniteDimensional ℂ H. Operators are continuous linear maps H →L[ℂ] H. Scalars are complex in the goal. Subspaces are Submodules, and closedness is required explicitly: without it the statement is trivially true in infinite dimensions (the algebraic span of an orbit is a proper invariant subspace), and a published platform statement that omits closedness should not be confused with this problem. Existential milestones quantify over spaces in Type.

Useful infrastructure includes: Schauder's fixed point theorem, Riesz theory of compact operators, the spectral theorem for normal operators, and $\ell^1$ machinery for Read's construction. Contributions of reusable lemmas, partial results (for instance further classes of operators known to have invariant subspaces), and proof sketches for the milestones are welcome.

Selected references

Open Problem Garden, Invariant subspace problem, posted by T. Chow, 2009. http://www.openproblemgarden.org/op/invariant_subspace_problem
N. Aronszajn, K. T. Smith, Invariant subspaces of completely continuous operators, Ann. of Math. 60 (1954) 345–350. https://doi.org/10.2307/1969637
V. I. Lomonosov, Invariant subspaces for the family of operators which commute with a completely continuous operator, Funct. Anal. Appl. 7 (1973) 213–214. https://doi.org/10.1007/BF01080698
P. Enflo, On the invariant subspace problem for Banach spaces, Acta Math. 158 (1987) 213–313. https://doi.org/10.1007/BF02392260
C. J. Read, A solution to the invariant subspace problem on the space $\ell_1$ , Bull. London Math. Soc. 17 (1985) 305–317. https://doi.org/10.1112/blms/17.4.305
S. A. Argyros, R. G. Haydon, A hereditarily indecomposable $\mathcal{L}_\infty$ -space that solves the scalar-plus-compact problem, Acta Math. 206 (2011) 1–54. https://arxiv.org/abs/0903.3921
H. Radjavi, P. Rosenthal, The invariant subspace problem, Math. Intelligencer 4 (1982) 33–37.
B. S. Yadav, The present state and heritages of the invariant subspace problem, Milan J. Math. 73 (2005) 289–316.

12 thms2 active usersReviewed

Completed

Number Theory·Captain: Lucas

Euler Systems (Wikipedia): Relations of the Cyclotomic Euler SystemTextbook

Motivation

An Euler system is a family of cohomology classes, indexed by abelian extensions of a base field, whose members are tied together by norm relations whose correction factors look like the Euler factors of an $L$ -function. Euler systems were introduced by Kolyvagin (Kolyvagin 1990), building on Thaine's work on cyclotomic fields (Thaine 1988), and they are one of the main tools for bounding Selmer groups and ideal class groups: Kolyvagin used them to prove finiteness of some Tate–Shafarevich groups, and Rubin used them for a new proof of the main conjecture of Iwasawa theory (Rubin 2000).

The simplest Euler system, and the model for all others, is the cyclotomic Euler system of cyclotomic units $\alpha_n = 1-\zeta_n$ . Kolyvagin used it to give an elementary proof of the Gras conjecture. This mission formalizes the two defining relations of this system as stated in the Wikipedia article Euler system.

Timeline (as summarized in the source): Thaine (1988) annihilators of class groups of real abelian fields; Kolyvagin (1988, 1990) Heegner-point and general Euler systems; Kato (2004) Euler system of Beilinson elements; Rubin (2000) monograph Euler Systems; Mazur–Rubin (2004) Kolyvagin systems.

Setting

For every square-free positive integer $n$ fix a primitive $n$ -th root of unity $\zeta_n\in\mathbb C$ , chosen compatibly: $\zeta_{mn}=\zeta_m\zeta_n$ whenever $m,n$ are coprime. Put

\alpha_n = 1-\zeta_n \in \mathbb Q(\zeta_n).

For a prime $l\nmid n$ , the Frobenius $\mathrm{Fr}_l$ is the automorphism of $\mathbb Q(\zeta_n)/\mathbb Q$ with $\mathrm{Fr}_l(\zeta_n)=\zeta_n^{\,l}$ . The norm $N_{\mathbb Q(\zeta_{nl})/\mathbb Q(\zeta_n)}$ is the field norm of the extension $\mathbb Q(\zeta_{nl})/\mathbb Q(\zeta_n)$ , and a prime $\mathfrak P$ of $\mathbb Q(\zeta_{nl})$ lies above $l$ if it is a prime ideal of the ring of integers containing $l$ .

Formalization targets

Goal: the cyclotomic Euler system relations

For square-free $n$ and a prime $l\nmid n$ :

N_{\mathbb Q(\zeta_{nl})/\mathbb Q(\zeta_n)}(\alpha_{nl})=\alpha_n^{\mathrm{Fr}_l-1}\quad(n>1),\qquad \alpha_{nl}\equiv\alpha_n \pmod{\mathfrak P}\ \text{ for all } \mathfrak P\mid l.

Milestones

Existence of a compatible system $(\zeta_n)$ (the "pick" step).
The norm relation.
The congruence relation.

Significance

The two relations are exactly the axioms that later, more abstract Euler systems (Gauss sums, elliptic units, Heegner points, Kato's elements) are modelled on; the cyclotomic case is where the Euler-system machinery for class groups of abelian fields starts. Both relations are classical and proved; what remains is formalizing them. Mathlib provides cyclotomic fields, primitive roots of unity, field norms and rings of integers; the mission builds the relations on top of these and provides a reusable definition layer for cyclotomic units.

Difficulty

The norm relation requires identifying the Galois group of $\mathbb Q(\zeta_{nl})/\mathbb Q(\zeta_n)$ with $(\mathbb Z/l)^\times$ — which uses the irreducibility of the $l$ -th cyclotomic polynomial over $\mathbb Q(\zeta_n)$ for $l\nmid n$ — and then computing the norm as a product over conjugates inside $\mathbb C$ , transported along the intermediate-field coercions. The congruence relation requires working in the ring of integers of a subfield of $\mathbb C$ and showing that $1-\zeta_l$ lies in every prime above $l$ . Neither is conceptually deep, but both involve substantial bookkeeping between subfields of $\mathbb C$ , abstract cyclotomic extensions, and rings of integers.

Formalization scope

All fields are subfields of $\mathbb C$ : $\mathbb Q(\zeta_n)$ is IntermediateField.adjoin ℚ {ζ n}, and $\mathbb Q(\zeta_{nl})$ over $\mathbb Q(\zeta_n)$ is IntermediateField.adjoin (ℚ(ζ_n)) {ζ (n*l)}. The norm is Algebra.norm; $\alpha_n^{\mathrm{Fr}_l-1}$ is written as $\mathrm{Fr}_l(\alpha_n)/\alpha_n$ ; $\mathrm{Fr}_l$ is any $\mathbb Q$ -algebra automorphism of $\mathbb Q(\zeta_n)$ with $\zeta_n\mapsto\zeta_n^l$ . Roots of unity are required to be primitive. Two deviations from the literal text of the source, both forced: the norm's base field is $\mathbb Q(\zeta_n)$ (the source's $\mathbb Q(\zeta_l)$ is a typo), and the norm relation assumes $n>1$ (for $n=1$ , $\alpha_1=0$ ). The existence milestone rules out a vacuous reading of the compatibility hypothesis. Welcome contributions: lemmas on Galois groups of compositums of cyclotomic fields inside $\mathbb C$ , and on primes above $l$ in $\mathbb Q(\zeta_{nl})$ .

Selected references

Wikipedia, Euler system, revision 1353502478. https://en.wikipedia.org/w/index.php?title=Euler_system&oldid=1353502478
V. A. Kolyvagin, Euler systems, The Grothendieck Festschrift II, Progr. Math. 87, Birkhäuser, 1990. https://doi.org/10.1007/978-0-8176-4575-5_11
F. Thaine, On the ideal class groups of real abelian number fields, Ann. of Math. 128 (1988), 1–18. https://doi.org/10.2307/1971460
K. Rubin, Euler Systems, Annals of Mathematics Studies 147, Princeton University Press, 2000. https://books.google.com/books?isbn=0691050767
B. Mazur, K. Rubin, Kolyvagin systems, Mem. Amer. Math. Soc. 168 (2004), no. 799. https://doi.org/10.1090/memo/0799

5 thms2 active usersReviewed

Completed

Algorithmic Game Theory Economics·Captain: Lucas

Rural Hospitals Theorem (Wikipedia): All Stable Matchings Fill the Same PositionsTextbook

Motivation

In centralized labour markets such as the US National Resident Matching Program, doctors are assigned to hospital residency positions by a mechanism that produces a stable matching. There are more positions than doctors, so some hospitals end up with empty positions; these are typically rural hospitals, which are less sought after than urban ones. This raised the question of whether a different mechanism could help these hospitals (Roth 1986). The rural hospitals theorem answers this negatively, provided all preferences are strict.

Timeline.

1970: McVitie and Wilson prove the one-to-one case (each hospital has one position): all stable matchings match the same doctors and the same hospitals (doi:10.1007/BF01934199).
1984: Roth proves Part 1 for many-to-one markets: the set of assigned doctors and the number of filled positions at each hospital are the same in all stable matchings (doi:10.1086/261272).
1986: Roth proves Part 2: a hospital with an empty position in some stable matching receives exactly the same doctors in all stable matchings (doi:10.2307/1913160).
2014: Klijn and Yazıcı extend the theorem to many-to-many matching (doi:10.1016/j.jmateco.2014.09.003).

Setting

A market has a finite set $D$ of doctors and a finite set $H$ of hospitals; hospital $h$ has $q_h$ positions. Every doctor strictly ranks the hospitals together with the option of staying unmatched, and every hospital strictly ranks the doctors together with the option of leaving a position empty. An assignment $\mu$ sends each doctor to a hospital or to nothing; $\mu(h)$ is the set of doctors at $h$ . It is a matching if $|\mu(h)|\le q_h$ for every $h$ .

A matching is stable if (i) no doctor is placed at a hospital she ranks below staying unmatched, and no hospital holds a doctor it ranks below an empty position, and (ii) there is no blocking pair $(d,h)$ : a doctor $d$ who prefers $h$ to her assignment, while $h$ finds $d$ acceptable and either has an empty position or prefers $d$ to one of its current doctors.

Formalization targets

Goal: the rural hospitals theorem

For any two stable matchings $\mu,\nu$ :

\mu(d)\ne\varnothing \iff \nu(d)\ne\varnothing\ \ (d\in D),\qquad |\mu(h)|=|\nu(h)|\ \ (h\in H),\qquad |\mu(h)|<q_h \implies \nu(h)=\mu(h).

Milestones

One position per hospital: a doctor unmatched in one stable matching is unmatched in every stable matching.
One position per hospital: a hospital unmatched in one stable matching is unmatched in every stable matching.
Part 1: the same doctors are assigned, and every hospital fills the same number of positions, in all stable matchings.
Part 2: a hospital with an empty position in some stable matching receives the same set of doctors in all stable matchings.

Significance

The result itself. Changing the matching mechanism, as long as it outputs stable matchings, cannot give under-subscribed hospitals more doctors or different doctors, and cannot change which doctors are employed. Hence policy aimed at rural hospitals must change preferences, capacities, or abandon stability, not merely switch between stable mechanisms.

Formalizing it. The theorem is classical and proved in the cited papers; this mission asks for a machine-checked proof in Lean 4 with Mathlib, for the general many-to-one model with capacities and acceptability, together with the one-position special case.

Difficulty

Comparing two stable matchings one agent at a time does not work: a single doctor moving between hospitals says nothing about how many positions each hospital fills, and the statements concern every agent of the market simultaneously. Stability of both matchings has to be used at once, and Part 2 is strictly stronger than Part 1 (equal numbers of doctors at an under-filled hospital do not imply equal sets of doctors). The existence of a stable matching is not needed for these statements.

Formalization scope

Doctors and hospitals are finite types D, H. Preferences are injective rank functions on Option H (for a doctor) and Option D (for a hospital), smaller rank meaning more preferred and none meaning unmatched or an empty position; injectivity encodes strictness. Hospital preferences over groups are responsive. Capacities are natural numbers and may be zero. An assignment is μ : D → Option H. Stability is Market.IsStable: capacity constraints, individual rationality, and no blocking pair. All statements quantify over arbitrary stable matchings, so they are not vacuous: stable matchings exist in every such market (Gale–Shapley), though existence is not part of this mission.

Contributions welcome: proofs of the milestones, an existence theorem for stable matchings in this model, and lemmas about stable matchings reusable in other matching missions.

Selected references

D. G. McVitie, L. B. Wilson, Stable marriage assignment for unequal sets, BIT Numerical Mathematics 10 (1970) 295–309. https://doi.org/10.1007/BF01934199
A. E. Roth, The evolution of the labor market for medical interns and residents: a case study in game theory, Journal of Political Economy 92 (1984) 991–1016. https://doi.org/10.1086/261272
A. E. Roth, On the allocation of residents to rural hospitals: a general property of two-sided matching markets, Econometrica 54 (1986) 425–427. https://doi.org/10.2307/1913160
F. Klijn, A. Yazıcı, A many-to-many 'rural hospital theorem', Journal of Mathematical Economics 54 (2014) 63–73. https://doi.org/10.1016/j.jmateco.2014.09.003
Wikipedia, Rural hospitals theorem, revision 1064508418. https://en.wikipedia.org/w/index.php?title=Rural_hospitals_theorem&oldid=1064508418

6 thms2 active usersReviewed

Completed

Algorithmic Game Theory Combinatorics Economics·Captain: Lucas

Stable Matching Problem (Wikipedia) I: The Gale–Shapley AlgorithmTextbook

Motivation

The stable matching problem asks for a pairing between two equally sized groups in which no two participants would both rather be matched with each other than with their assigned partners. It was posed and solved by Gale and Shapley in 1962 in the context of college admissions and marriage (Gale–Shapley 1962). Their deferred acceptance algorithm underlies centralized clearinghouses such as the assignment of graduating medical students to hospital residencies, and the theory of stable allocations was recognized by the 2012 Nobel Memorial Prize in Economic Sciences awarded to Shapley and Roth.

Timeline of the results targeted here:

1962 — Gale and Shapley: a stable matching always exists, and the men-proposing deferred acceptance algorithm finds one; its outcome is the best stable matching for every man.
1971 — McVitie and Wilson: the men-optimal stable matching is simultaneously the worst stable matching for every woman.
1981–1982 — Dubins–Freedman and Roth: the men-proposing algorithm is strategy-proof (indeed group strategy-proof) for men, while women can gain by misreporting.
1987 — Gusfield (after Knuth and Conway): the stable matchings of an instance form a finite distributive lattice.

Setting

Fix $n \ge 0$ . There are $n$ men and $n$ women, both indexed by $\mathrm{Fin}\,n$ . Each man $m$ ranks all women strictly: $\mathrm{manRank}_m(w) \in \mathrm{Fin}\,n$ is the position of $w$ in $m$ 's list, position $0$ being most preferred; symmetrically each woman $w$ has $\mathrm{womanRank}_w$ . Both are bijections. A matching is a bijection $\mu$ from men to women. A pair $(m, w)$ blocks $\mu$ if $\mathrm{manRank}_m(w) < \mathrm{manRank}_m(\mu(m))$ and $\mathrm{womanRank}_w(m) < \mathrm{womanRank}_w(\mu^{-1}(w))$ ; $\mu$ is stable if no pair blocks it.

The Gale–Shapley algorithm runs in rounds. A state records, for every man, how many women he has proposed to so far, and for every woman, her current provisional fiancé (if any). In each round every unengaged man proposes to the most preferred woman he has not yet proposed to, and every woman keeps the most preferred among her current fiancé and this round's suitors, rejecting the others. The Gale–Shapley outcome is the matching read off from the state after $n^2$ rounds.

Formalization targets

Goal: the algorithm produces a stable matching

\forall I,\ \exists \mu,\ \mu \text{ is the Gale–Shapley outcome of } I \ \wedge\ \mu \text{ is stable for } I.

This contains termination (all men are engaged after $n^2$ rounds), the fact that the final engagements form a bijection, and stability.

Milestones

Termination: after $n^2$ rounds every man is engaged.
Existence: every instance has a stable matching.
Man-optimality: for the Gale–Shapley outcome $\mu_0$ and every stable $\mu$ , $\mathrm{manRank}_m(\mu_0(m)) \le \mathrm{manRank}_m(\mu(m))$ for every man $m$ .
Woman-pessimality: $\mathrm{womanRank}_w(\mu^{-1}(w)) \le \mathrm{womanRank}_w(\mu_0^{-1}(w))$ for every woman $w$ .
Truthfulness for men: no single man obtains a strictly better partner (by his true list) by misreporting.
Group strategy-proofness for men: no nonempty coalition of men can misreport so that all its members are strictly better off.
Weak coalitional manipulation: some coalition can misreport so that some members are strictly better off and the rest keep their partners.
Women can manipulate: some woman can obtain a strictly better partner by misreporting.
The 3×3 example: the instance $A: YXZ$ , $B: ZYX$ , $C: XZY$ , $X: BAC$ , $Y: CBA$ , $Z: ACB$ has exactly the three stable matchings $(AY,BZ,CX)$ , $(AX,BY,CZ)$ , $(AZ,BX,CY)$ .
Lattice structure: the stable matchings of any instance form a distributive lattice under "every man weakly prefers".

Significance

Existence of stable matchings is the foundation of two-sided matching theory, and the algorithmic proof is constructive. Man-optimality and woman-pessimality show that the proposing side is systematically favored, which is the reason the choice of proposing side matters in practice, as in the 1995 redesign of the residency match. The incentive results (milestones 5–8) explain why participants on the proposing side can safely report their true preferences while the receiving side cannot, and the lattice structure underlies efficient algorithms for enumerating and optimizing over stable matchings.

All results in this mission are classical and proved in the literature. The work here is formalization: a precise model of the round-based algorithm, machine-checked proofs of its correctness and optimality, and the incentive properties, which are usually argued informally.

Difficulty

The goal requires reasoning about an iterated state transformer rather than an abstract existence statement. The step that is usually waved away is the invariant that an unengaged man still has a woman left to propose to, which is what makes the $n^2$ bound and the bijectivity of the final engagements work. Man-optimality needs the invariant that no man is ever rejected by a woman who is his partner in some stable matching, which is not visible from the output alone. Group strategy-proofness is substantially harder than individual truthfulness: the known proofs go through a "blocking lemma" about matchings that are weakly preferred by all men.

Formalization scope

Men and women are Fin n; preferences are strict total orders given as rank bijections Fin n ≃ Fin n; matchings are bijections Fin n ≃ Fin n. The algorithm is the round-based version described in the source: all unengaged men propose simultaneously in each round. The algorithm's output is fixed as the state after exactly $n^2$ rounds; termination within that bound is itself a milestone, so a wrong bound would make the goal false rather than vacuous. The case $n = 0$ is included and is trivial. Incentive results compare Gale–Shapley outcomes of two instances that differ only in the lists of the deviating participants, with gains measured by the deviators' true lists.

The definitions are reusable for further missions on the same article (rural hospitals theorem, hospitals/residents problem). Contributions welcome: invariants of the algorithm, the blocking lemma, and alternative proofs of existence.

Selected references

D. Gale, L. S. Shapley, College Admissions and the Stability of Marriage, American Mathematical Monthly 69(1), 1962, 9–14. https://doi.org/10.2307/2312726
D. G. McVitie, L. B. Wilson, The stable marriage problem, Communications of the ACM 14(7), 1971, 486–490. https://doi.org/10.1145/362619.362631
L. E. Dubins, D. A. Freedman, Machiavelli and the Gale–Shapley Algorithm, American Mathematical Monthly 88(7), 1981, 485–494. https://doi.org/10.2307/2321753
A. E. Roth, The Economics of Matching: Stability and Incentives, Mathematics of Operations Research 7(4), 1982, 617–628. https://doi.org/10.1287/moor.7.4.617
D. Gusfield, Three fast algorithms for four problems in stable marriage, SIAM Journal on Computing 16(1), 1987, 111–128. https://doi.org/10.1137/0216010
Wikipedia, Stable matching problem. https://en.wikipedia.org/wiki/Stable_matching_problem

12 thms2 active usersReviewed

Completed

Optimization Probability·Captain: Lucas

Secretary Problem: the 37% RuleTextbook

Motivation

The secretary problem is the standard example of an optimal stopping problem with partial information. It is also known as the marriage problem, the sultan's dowry problem, the fussy suitor problem, the googol game and the best choice problem. It is studied in applied probability, statistics and decision theory. Its solution is often called the 37% rule: a simple rule picks the single best of $n$ applicants with probability about $1/e \approx 0.368$ , whether there are 100 or 100 million applicants (Wikipedia: Secretary problem). The problem is a standard example of the exploration–exploitation dilemma.

Timeline (as recounted in the Wikipedia article's History section, following Ferguson 1989):

1949: Merrill M. Flood introduces the problem (as the "fiancée problem") in a lecture. It then spreads as folklore through the 1950s.
1958: Flood circulates a letter outlining a proof of the optimal strategy. Its appendix by R. Palermo proves that every strategy is dominated by one of the form "reject the first $p$ unconditionally, then accept the next candidate who is better".
1960: First publication, in Martin Gardner's Scientific American column (February 1960), with the analysis supplied by Leo Moser and J. R. Pounder.
1966: Gilbert and Mosteller, "Recognizing the maximum of a sequence", a detailed study of the problem and many variants.
1989: Ferguson, "Who solved the secretary problem?", a historical survey.
2000: Bruss's odds theorem, which the article calls the shortest rigorous proof known.

Setting

There is a single position and there are $n$ applicants, where $n$ is known. If seen together, the applicants can be ranked from best to worst with no ties. They are interviewed one at a time in a uniformly random order: each of the $n!$ orders is equally likely. Right after each interview the applicant is either accepted, which ends the process, or rejected for good. The decision may depend only on the relative ranks of the applicants interviewed so far. The objective is to maximize the probability of selecting the best applicant of the whole group.

An order is a permutation $\sigma$ of $\{0,\dots,n-1\}$ . The applicant interviewed at time $i$ has quality $\sigma(i)$ , where larger means better. The relative rank of the applicant interviewed at time $j$ is the number of applicants interviewed before time $j$ who are worse than them. A stopping rule $s$ maps the list of relative ranks observed so far to "accept" or "reject". Its success probability $P_n(s)$ is the fraction of the $n!$ orders on which the applicant accepted by $s$ is the overall best. A rule that never accepts anyone fails. The optimal success probability is

V_n = \sup_s P_n(s).

A candidate is an applicant who is better than every applicant interviewed before them. The cutoff rule with cutoff $r$ rejects the first $r-1$ applicants and then accepts the first candidate after that point.

Formalization targets

Goal: the 37% rule

\lim_{n\to\infty} V_n = \frac1e .

Milestones (following the article's derivation)

$P_n(\text{cutoff } 1) = 1/n$ .
For $2\le r\le n$ : $P_n(\text{cutoff } r) = \dfrac{r-1}{n}\displaystyle\sum_{i=r}^{n}\frac{1}{i-1}$ .
Some cutoff rule with $1\le r\le n$ is optimal among all rank-based stopping rules.
The table of optimal cutoffs and optimal success probabilities for $n=1,\dots,10$ .
If $r_n/n\to x\in[0,1]$ , then $P_n(\text{cutoff } r_n)\to x\int_x^1 \frac{dt}{t} = -x\log x$ .
On $[0,1]$ the function $-x\log x$ has maximum value $1/e$ , attained only at $x=1/e$ .
Optimal cutoffs satisfy $r_n/n\to 1/e$ .
$V_n \ge 1/e$ for every $n\ge 1$ .

Significance

The result. The 37% rule is the classical result of optimal stopping. It shows that a fixed fraction of the best possible success probability survives as the number of options grows without bound, and that a simple threshold policy achieves it. The structure of its solution has three parts: optimal rules may be taken to be threshold rules, there is an exact formula in terms of the records of a uniformly random permutation, and a limit turns a harmonic sum into an integral. This structure recurs throughout the best-choice literature, including the prophet-secretary and multi-choice secretary problems.

Formalizing it. The result has been proved since the late 1950s and early 1960s. The remaining work is to formalize the known proof: a model of rank-based stopping rules over uniformly random permutations, the exact success probability of cutoff rules, the optimality of cutoff rules among all rank-based rules, and the asymptotics.

Difficulty

The success probability of a fixed cutoff rule and the calculus limit are elementary. The central step is the optimality of cutoff rules (Milestone 3). A stopping rule may depend arbitrarily on the whole history of relative ranks, and one has to show that no such rule beats the best cutoff rule. Evaluating cutoff rules alone does not prove the goal, because $V_n$ is a supremum over all rank-based rules. A second, smaller difficulty is that the limit statements need control of the harmonic sums along a varying cutoff $r_n$ , not only along a fixed ratio.

Formalization scope

The sample space is the finite set Equiv.Perm (Fin n) with uniform weights. successProb n s is the ratio (number of winning permutations) / $n!$ in $\mathbb R$ .
A stopping rule is a deterministic function List ℕ → Bool, applied to the list of relative ranks observed so far. Through the length of the list it also knows the current time. It never sees absolute qualities. Randomized rules are not modelled. A randomized rule is a mixture of deterministic ones, so it cannot do better.
optimalProb n is the real supremum of successProb n s over all such rules. The values lie in $[0,1]$ , so the supremum is the usual least upper bound.
Times are 0-based in Lean (Fin n). Cutoffs $r$ are 1-based, as in the article: cutoffRule r accepts at time $i$ exactly when $i+1 \ge r$ and the current applicant is a candidate.
$1/e$ is written Real.exp (-1).
The 1/e-law of best choice (unknown number of applicants, Bruss 1984), the odds algorithm, cardinal-payoff variants and the other generalizations in the article are outside this mission.

All declarations live in the namespace ClassicalSecretary. Reusable contributions are welcome, in particular facts about records of uniformly random permutations (independence of relative ranks, the probability that position $i$ is a record) and a backward-induction principle for finite-horizon stopping problems.

Selected references

Wikipedia contributors, Secretary problem, sections "Formulation" and "Deriving the optimal policy". https://en.wikipedia.org/wiki/Secretary_problem
T. S. Ferguson, Who solved the secretary problem?, Statistical Science 4(3), 282–289, 1989. https://doi.org/10.1214/ss/1177012493
J. Gilbert, F. Mosteller, Recognizing the maximum of a sequence, Journal of the American Statistical Association 61(313), 35–73, 1966. https://doi.org/10.2307/2283044
F. T. Bruss, Sum the odds to one and stop, Annals of Probability 28(3), 1384–1391, 2000. https://doi.org/10.1214/aop/1019160340

10 thms2 active usersReviewed

Algebraic Topology Geometry & Topology·Captain: Lucas

Smale's question: the homotopy type of Diff(S⁴)Open Problem

Motivation

The diffeomorphism group $\mathrm{Diff}(M)$ of a closed smooth manifold $M$ , topologized so that two diffeomorphisms are close when they and all their derivatives are uniformly close, is a basic invariant of the smooth structure of $M$ . Its set of path components $\pi_0\,\mathrm{Diff}(M)$ is the group of isotopy classes of diffeomorphisms (the smooth mapping class group), and its higher homotopy groups classify smooth fibre bundles with fibre $M$ . For spheres, the natural comparison is with the orthogonal group $O(n+1)$ of isometries of the round metric, which sits inside $\mathrm{Diff}(S^n)$ .

S. Smale asked how far $\mathrm{Diff}(S^n)$ is from $O(n+1)$ . The question was settled positively in dimensions $n \le 3$ and has been studied extensively in dimensions $n \ge 5$ , where surgery theory and pseudo-isotopy theory apply. Dimension $4$ is the remaining case, and it is where the least is known. The question is recorded on the Open Problem Garden (problem page) with importance "Outstanding".

Timeline.

1959 — S. Smale: $\mathrm{Diff}(S^2) \simeq O(3)$ .
1963 — M. Kervaire and J. Milnor compute the groups $\Theta_n$ of homotopy spheres; combined with Cerf's pseudo-isotopy theorem this computes $\pi_0\,\mathrm{Diff}(S^n)$ for many $n \ge 5$ (for example $\pi_0\,\mathrm{Diff}^+(S^6) \cong \Theta_7 \cong \mathbb Z/28$ ).
1970s — the Cerf–Morlet comparison theorem $\mathrm{Diff}(D^n) \simeq \Omega^{n+1}(PL_n/O_n)$ (Kirby–Siebenmann, Foundational Essays).
1978 — F.T. Farrell and W.C. Hsiang compute $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q$ in a stable range of degrees for large $n$ .
1983 — A. Hatcher: $\mathrm{Diff}(S^3) \simeq O(4)$ (the Smale conjecture).
2007 — R. Budney: $\mathrm{Diff}(D^4)$ is a $5$ -fold loop space, via little cubes acting on spaces of long knots.
2018 — T. Watanabe: $\pi_*\,\mathrm{Diff}(D^4)\otimes\mathbb Q \ne 0$ ; the $4$ -dimensional Smale conjecture is false (arXiv:1812.02448).

Whether $\mathrm{Diff}(D^4)$ is connected is still unknown.

Setting

Write $\mathbb R^n$ for Euclidean space with the Euclidean norm, $D^n$ for the closed unit ball and $S^n \subset \mathbb R^{n+1}$ for the round unit sphere.

$\mathrm{Diff}(D^n)$ is the group of diffeomorphisms of the $n$ -ball rel boundary. Concretely it is the group of smooth diffeomorphisms $f\colon \mathbb R^n \to \mathbb R^n$ with $f(x) = x$ whenever $\|x\| \ge 1$ . Two such maps are close when their $k$ -th derivatives are uniformly close for every $k$ (the $C^\infty$ topology). The base point is the identity.
$\mathrm{Diff}(S^n)$ is the group of all smooth diffeomorphisms of $S^n$ (orientation-preserving or orientation-reversing), with the $C^\infty$ topology. Derivatives are measured through the degree-one homogeneous extension $x \mapsto \|x\|\, f(x/\|x\|)$ , taken on the sphere.
$O(n)$ is the group of real orthogonal $n\times n$ matrices with the matrix topology.
$X \simeq Y$ means that $X$ and $Y$ are homotopy equivalent. $\pi_0 X$ is the set of path components, and $\pi_i(X,x)$ is the $i$ -th homotopy group. $\Omega^k(Y,y)$ is the $k$ -fold loop space, the space of maps $[0,1]^k \to Y$ sending the boundary of the cube to $y$ .

The source states that $\mathrm{Diff}(S^4) \simeq O(5) \times \mathrm{Diff}(D^4)$ , so the homotopy type of $\mathrm{Diff}(S^4)$ is determined by that of $\mathrm{Diff}(D^4)$ .

Formalization targets

Goal: connectivity of $\mathrm{Diff}(D^4)$

\pi_0\,\mathrm{Diff}(D^4) = 0, \qquad\text{i.e. } \mathrm{Diff}(D^4) \text{ is path-connected.}

The source asks to "determine some (any?) homotopy or homology groups of $\mathrm{Diff}(D^4)$ " and singles out connectivity as unknown. The goal is the yes/no question for $\pi_0$ . It can be settled either way: a proof shows that every diffeomorphism of $D^4$ rel boundary is isotopic to the identity, and a disproof exhibits one that is not.

Milestones

$\mathrm{Diff}(S^4) \simeq O(5)\times\mathrm{Diff}(D^4)$ (problem statement).
$\mathrm{Diff}(D^4) \simeq \Omega^5(Y,y)$ for some pointed space $(Y,y)$ (Cerf–Morlet, Budney).
$\mathrm{Diff}(D^4)$ is not contractible (Watanabe).
$\mathrm{Diff}(S^2) \simeq O(3)$ (Smale).
$\mathrm{Diff}(S^3) \simeq O(4)$ (Hatcher).
$|\pi_0\,\mathrm{Diff}(S^6)| = 56$ (Kervaire–Milnor and Cerf).
For $2 \le i < \min\{\tfrac{n-4}{3}, \tfrac{n-7}{2}\}$ : $\pi_i\,\mathrm{Diff}(D^n)\otimes\mathbb Q \cong \mathbb Q$ if $n$ is odd and $4 \mid i+1$ , and $0$ otherwise (Farrell–Hsiang).

Significance

The result itself. A positive answer would mean $\pi_0\,\mathrm{Diff}(S^4) \cong \mathbb Z/2$ , detected by orientation alone, matching dimensions $1$ , $2$ and $3$ . A negative answer would give an exotic diffeomorphism of $S^4$ : one that is topologically isotopic to the identity (by the Alexander trick) but not smoothly isotopic. By the Cerf–Morlet theorem, $\pi_0\,\mathrm{Diff}(D^4) \cong \pi_5(PL_4/O_4)$ , so the question is equivalent to a question about the homotopy of $PL_4/O_4$ , the space controlling smoothings of PL $4$ -manifolds. The source lists the smooth $4$ -dimensional Schoenflies problem as a related problem.

Formalizing it. No part of this theory is currently formalized in Lean or Mathlib: there is no $C^\infty$ topology on diffeomorphism groups and no known homotopy equivalence involving one. The milestones are classical theorems (Smale 1959, Hatcher 1983, Kervaire–Milnor 1963, Farrell–Hsiang 1978, Watanabe 2018). Formalizing any of them is new work, independent of the open goal.

Difficulty

In dimensions $\ge 5$ , $\pi_0\,\mathrm{Diff}(D^n)$ is computed by combining Cerf's pseudo-isotopy theorem with the $h$ -cobordism theorem. Both rely on the Whitney trick, which fails in dimension $4$ . In dimension $4$ one also cannot reduce to a lower-dimensional problem as Smale and Hatcher did. The known invariants that detect non-trivial elements of $\pi_*\,\mathrm{Diff}(D^4)$ (Watanabe's configuration-space integrals) are rational and live in positive degrees, so they say nothing about $\pi_0$ . Smale's and Hatcher's arguments for $n = 2, 3$ rely on understanding spaces of embedded spheres in $S^n$ of one lower dimension; the corresponding spaces of $3$ -spheres in $S^4$ are not understood, so those arguments do not carry over.

Formalization scope

All statements import the single definition file SmaleDiffS4_Basic and live in the namespace SmaleDiffS4.

DiffDisk n is the subtype of Mathlib's Diffeomorph 𝓘(ℝ, ℝⁿ) 𝓘(ℝ, ℝⁿ) ℝⁿ ℝⁿ ∞ (smooth = C^∞) of maps fixing every point of norm $\ge 1$ . Its topology is induced by the family of iterated derivatives iteratedFDeriv ℝ k f, $k \in \mathbb N$ , each with the topology of uniform convergence on $\mathbb R^n$ . This "identity outside the open ball" model is the standard model of $\mathrm{Diff}(D^n \text{ rel } \partial)$ and is homotopy equivalent to the "identity on the boundary" and "identity near the boundary" variants.
DiffSphere n is Mathlib's Diffeomorph (𝓡 n) (𝓡 n) (sphere 0 1) (sphere 0 1) ∞ on the unit sphere of $\mathbb R^{n+1}$ . Its topology is induced by the iterated derivatives of the radial extension, restricted to the sphere and uniformly topologized.
OrthGroup n is Matrix.orthogonalGroup (Fin n) ℝ with the subspace topology.
Homotopy equivalence is ContinuousMap.HomotopyEquiv. $\Omega^5$ is GenLoop (Fin 5) Y y, $\pi_0$ is ZerothHomotopy, and $\pi_i$ is HomotopyGroup (Fin i). $\pi_i\otimes\mathbb Q$ is TensorProduct ℤ ℚ (Additive π_i), and " $\cong\mathbb Q$ " is stated as $\mathbb Q$ -rank $1$ .
The Farrell–Hsiang milestone covers only $i \ge 2$ , where $\pi_i$ is abelian in Mathlib. It includes the parity hypothesis " $n$ odd" of the original theorem, which is lost in the source page's rendering.

A trivializing formalization is ruled out: the topology is the genuine $C^\infty$ topology rather than the discrete or indiscrete one, and the goal is not vacuous because DiffDisk 4 is nonempty (it contains the identity).

A complete development needs reusable infrastructure: the $C^\infty$ topology and topological-group structure on diffeomorphism groups, isotopy extension and fibration theorems (Cerf–Palais), restriction to a disc, and the Alexander trick. Contributions of this infrastructure as separate theorems are welcome.

Selected references

Open Problem Garden, What is the homotopy type of the group of diffeomorphisms of the 4-sphere? (posted 2009). http://www.openproblemgarden.org/op/what_is_the_homotopy_type_of_the_group_of_diffeomorphisms_of_the_4_sphere
S. Smale, Diffeomorphisms of the 2-sphere, Proc. Amer. Math. Soc. 10 (1959), 621–626. https://doi.org/10.1090/S0002-9939-1959-0112149-8
M. Kervaire, J. Milnor, Groups of homotopy spheres I, Ann. of Math. 77 (1963), 504–537. https://doi.org/10.2307/1970128
R. Kirby, L. Siebenmann, Foundational Essays on Topological Manifolds, Smoothings, and Triangulations, Princeton University Press, 1977.
F.T. Farrell, W.C. Hsiang, On the rational homotopy groups of the diffeomorphism groups of discs, spheres and aspherical manifolds, Proc. Sympos. Pure Math. 32 (1978), 403–415.
A. Hatcher, A proof of a Smale conjecture, $\mathrm{Diff}(S^3)\simeq O(4)$ , Ann. of Math. (2) 117 (1983), 553–607. https://doi.org/10.2307/2007035
R. Budney, Little cubes and long knots, Topology 46 (2007), 1–27. https://arxiv.org/abs/math/0309427
T. Watanabe, Some exotic nontrivial elements of the rational homotopy groups of $\mathrm{Diff}(S^4)$ , 2018. https://arxiv.org/abs/1812.02448

11 thms2 active usersReviewed

Geometry & Topology Topology·Captain: Lucas

Slice–ribbon conjectureOpen Problem

Motivation

A knot is a smooth simple closed curve $K$ in the $3$ -sphere $S^3$ . Since $S^3$ is the boundary of the $4$ -ball $B^4$ , one can ask whether $K$ bounds a smoothly embedded disc in $B^4$ ; if so, $K$ is called slice. Slice knots are the identity element of the smooth knot concordance group, so deciding which knots are slice is a central question of $4$ -dimensional topology. A more restrictive and more combinatorial notion is that of a ribbon knot: a knot bounding an immersed disc in $S^3$ whose only self-intersections are ribbon singularities (arcs of double points whose two preimages are an interior arc and an arc running across the disc from boundary to boundary). Every ribbon knot is slice: pushing the interior of a ribbon disc into $B^4$ removes the double points. In 1962 R. H. Fox asked for the converse ([F]). The Open Problem Garden lists this slice–ribbon problem as Outstanding (source): given a knot in $S^3$ which is slice, is it a ribbon knot?

Timeline

1962 — Fox, Some problems in knot theory ([F]): asks whether every slice knot is ribbon.
1966 — Fox–Milnor: the Alexander polynomial of a slice knot factors as $f(t)f(t^{-1})$ , the first obstruction to sliceness.
1982 — Gilmer ([G], Invent. Math. 66): lower bounds on the slice genus from Casson–Gordon invariants.
1983 — Hass ([H], Math. Proc. Cambridge Philos. Soc. 94): studies the problem through minimal surfaces in $B^4$ ; a knot bounding a minimal disc in $B^4$ is ribbon.
2007 — Lisca: the slice–ribbon conjecture holds for all $2$ -bridge knots.
2008–2015 — Owens (arXiv:0802.2109), Greene–Jabuka (odd $3$ -strand pretzel knots), Lecuona (families of Montesinos knots, arXiv:0910.4601): further families where slice implies ribbon.
2010 — Gompf–Scharlemann–Thompson: candidate counterexamples arising from fibered knots and Property 2R.
The general question remains open.

Setting

Write $\mathbb R^4$ for Euclidean $4$ -space (R4), $S^3=\{x:\|x\|=1\}$ , $B^4=\{x:\|x\|\le1\}$ , and $D^2=\{z\in\mathbb R^2:\|z\|\le 1\}$ for the closed unit disc in the parameter plane $\mathbb R^2$ (R2).

Knot (IsKnot γ). A map $\gamma:\mathbb R\to\mathbb R^4$ which is $C^\infty$ , $1$ -periodic, takes values in $S^3$ , is injective on $[0,1)$ , and has nowhere-vanishing velocity. The knot is the image $K=\gamma(\mathbb R)$ .
Slice disc (IsSliceDisk γ F). A $C^\infty$ map $F:\mathbb R^2\to\mathbb R^4$ that is injective on $D^2$ with injective differential at every point of $D^2$ , maps the open disc into the open ball, maps the unit circle onto $K$ , and is transverse to $S^3$ along the boundary: $\langle F(z), dF_z(z)\rangle>0$ for $\|z\|=1$ . A knot is slice (IsSlice γ) if it has a slice disc.
Ribbon disc (IsRibbonImmersedDisk γ f, Fox's definition). A $C^\infty$ map $f:\mathbb R^2\to\mathbb R^4$ that maps $D^2$ into $S^3$ with injective differential on $D^2$ , maps the unit circle injectively onto $K$ , has no triple points, has transverse double points, and whose double-point set in $D^2$ is a disjoint union of arcs $a_1,b_1,\dots,a_n,b_n$ with $f\circ a_i=f\circ b_i$ , each $a_i$ contained in the open disc and each $b_i$ running from the boundary circle through the open disc back to the boundary circle. A knot is ribbon (IsRibbon γ) if it bounds a ribbon disc.
Ribbon slice disc (IsRibbonSliceDisk γ F). A slice disc on which the squared radial function $r_F(z)=\|F(z)\|^2$ is Morse in the open disc with no local maxima.
Minimal disc (IsMinimalOnDisk F). With $E=\langle\partial_0F,\partial_0F\rangle$ , $G'=\langle\partial_0F,\partial_1F\rangle$ , $G=\langle\partial_1F,\partial_1F\rangle$ , the vector $G\,\partial_0\partial_0F-2G'\,\partial_0\partial_1F+E\,\partial_1\partial_1F$ is tangent to the surface at every interior point, i.e. the mean curvature vector of $F$ vanishes on the open disc.

Formalization targets

Goal: slice implies ribbon

\forall\,\gamma,\quad \mathrm{IsKnot}(\gamma)\ \wedge\ \mathrm{IsSlice}(\gamma)\ \Longrightarrow\ \mathrm{IsRibbon}(\gamma).

Milestones

[F] Ribbon knots are slice — the converse direction, observed by Fox.
Ribbon discs in $S^3$ versus ribbon discs in $B^4$ — a knot is ribbon iff it bounds a slice disc on which the radial function is Morse without local maxima.
[H] Hass — a knot bounding a minimal slice disc in $B^4$ is ribbon.

A further (non-milestone) sanity item asserts that the round unknot $t\mapsto(\cos 2\pi t,\sin 2\pi t,0,0)$ is a ribbon knot, which shows that the definitions are not vacuous.

A supporting (non-milestone) item isolates the maximum-principle step behind [H]: on a minimal disc, the radial function $\|F\|^2$ has no local maximum in the open disc.

Significance

A positive answer would make sliceness, a $4$ -dimensional property defined by the existence of an embedded disc in $B^4$ , equivalent to a $3$ -dimensional property that can be certified by a finite diagrammatic object (a ribbon presentation). A counterexample would exhibit a slice knot whose slice discs all need local maxima of the radial function; several proposed candidates (Gompf–Scharlemann–Thompson) are tied to the smooth $4$ -dimensional Poincaré conjecture and to Property 2R. The problem is closely related to the question of which homology $3$ -spheres bound homology $4$ -balls.

On the formal side no part of this theory is in Mathlib: there are no knots, no slice or ribbon discs, no Morse functions on surfaces and no minimal surfaces. The milestones (Fox's easy direction, the $3$ D/ $4$ D equivalence, Hass's theorem) are classical theorems that have not been machine-checked; formalizing them builds the infrastructure any later attack needs.

Difficulty

Turning a slice disc into a ribbon disc requires removing the local maxima of the radial function on the disc. Cancelling a maximum against a saddle is possible only when the handles are in suitable position, and there is no known procedure that achieves this in general; the known positive results rely on classifying the rational homology balls bounded by branched double covers, using Donaldson's diagonalization theorem, which applies only to special families of knots.

Formalization scope

Everything is stated in Euclidean coordinates: knots are periodic parametrisations $\mathbb R\to S^3\subset\mathbb R^4$ , discs are $C^\infty$ maps $\mathbb R^2\to\mathbb R^4$ whose restriction to $D^2$ is the disc in question. Smoothness is $C^\infty$ ; slice discs are required to be smooth up to the boundary and transverse to $S^3$ there (the standard notion of a properly embedded disc). The knot enters only through its image, so orientation and parametrization play no role. The problem is the smooth one; topologically locally flat slice discs are not allowed. Definitions under which the conjecture holds trivially (for example, a ribbon condition implied by the slice condition by definition) are excluded: the goal uses Fox's $3$ -dimensional ribbon discs, and the $4$ -dimensional characterisation is a separate milestone.

Contributions welcome: smooth embedded discs and their collars, Morse theory for functions on $D^2$ , the push-in construction, and minimal-surface tools (the maximum principle for $\|x\|^2$ on minimal surfaces).

Selected references

[F] R. H. Fox, Some problems in knot theory, Topology of 3-manifolds and related topics (Proc. Univ. of Georgia Institute, 1961), Prentice-Hall, 1962, pp. 168–176.
[G] P. M. Gilmer, On the slice genus of knots, Invent. Math. 66 (1982), 191–197.
[H] J. Hass, The geometry of the slice-ribbon problem, Math. Proc. Cambridge Philos. Soc. 94 (1983), 101–108.
A. G. Lecuona, On the slice-ribbon conjecture for Montesinos knots, arXiv:0910.4601.
B. Owens, On slicing invariants of knots, arXiv:0802.2109.
P. Lisca, Lens spaces, rational balls and the ribbon conjecture, Geom. Topol. 11 (2007), 429–472. https://doi.org/10.2140/gt.2007.11.429
R. E. Gompf, M. Scharlemann, A. Thompson, Fibered knots and potential counterexamples to the Property 2R and slice-ribbon conjectures, Geom. Topol. 14 (2010), 2305–2347. https://doi.org/10.2140/gt.2010.14.2305
Open Problem Garden, Slice-ribbon problem (posted by rybu, 2009). http://www.openproblemgarden.org/op/slice_ribbon_problem

7 thms2 active usersReviewed

Complexity Theory Mathematical Logic·Captain: Lucas

F_d versus F_{d+1}: fixed-depth separation of bounded-depth FregeOpen Problem

Motivation

Bounded-depth Frege systems are the proof systems of propositional logic in which every formula of a proof has depth bounded by a fixed constant $d$ ; the resulting system is written $F_d$ . They are the proof-theoretic counterpart of the circuit class $\mathrm{AC}^0$ and of the bounded arithmetic theories $I\Delta_0$ and its relatives: short $F_d$ -proofs of a family of tautologies correspond to proofs of the corresponding first-order statement in bounded arithmetic. Lower bounds for $F_d$ are among the strongest lower bounds known for any natural proof system.

A basic structural question is whether the depth hierarchy $F_1 \subseteq F_2 \subseteq F_3 \subseteq \dots$ is strict in a strong sense. It is known that one extra level of depth can give an exponential speed-up, but in all known separations the tautologies themselves have depth growing with $d$ . J. Krajíček asked whether there is a single fixed depth $k$ at which tautologies witnessing the separation of $F_{d+1}$ from $F_d$ exist for every $d$ (Open Problem Garden, F_d versus F_{d+1}; [Krajíček 1995, p. 243]). The question is closely related to conservativity relations among bounded arithmetic theories.

Timeline.

1987 — Buss: the pigeonhole principle $\mathrm{PHP}^{n+1}_n$ has polynomial-size Frege proofs (of unbounded depth).
1988 — Ajtai: $\mathrm{PHP}^{n+1}_n$ has no polynomial-size $F_d$ -proofs for any fixed $d$ .
1993/1995 — Pitassi–Beame–Impagliazzo and Krajíček–Pudlák–Woods: $F_d$ -proofs of $\mathrm{PHP}^{n+1}_n$ require size $2^{n^{\varepsilon_d}}$ .
1994 — Krajíček: for each $d$ there are tautologies of depth $d$ with polynomial-size $F_{d+1}$ -proofs requiring exponential-size $F_d$ -proofs, i.e. the problem is solved when $k$ may depend on $d$ ( $k := d$ ).
2002 — Impagliazzo–Krajíček relate the question to conservativity among bounded arithmetic theories.

Setting

Formulas. A formula is in negation normal form over variables $p_0, p_1, \dots$ : a literal $p_i$ or $\neg p_i$ , a conjunction $\bigwedge(A_1,\dots,A_m)$ or a disjunction $\bigvee(A_1,\dots,A_m)$ of any finite number $m \ge 0$ of formulas. The depth of a literal is $0$ , and the depth of $\bigwedge(A_1,\dots,A_m)$ or $\bigvee(A_1,\dots,A_m)$ is $1+\max_j \operatorname{depth}(A_j)$ (so clauses have depth $1$ and CNFs depth $2$ ). The size $|A|$ is the number of symbols (literals and connectives). A tautology is a formula true under every assignment. The negation $\overline{A}$ of a formula is obtained by De Morgan's laws.

The system $F_d$ . Lines of a proof are sequents: finite lists $\Gamma$ of formulas, read as their disjunction. The rules are: (axiom) any $\Gamma$ containing both $p_i$ and $\neg p_i$ ; ( $\wedge$ ) from $A, \Gamma$ for every $A \in \{A_1,\dots,A_m\}$ infer $\bigwedge(A_1,\dots,A_m), \Gamma$ ; ( $\vee$ ) from $A_j, \Gamma$ infer $\bigvee(A_1,\dots,A_m), \Gamma$ ; (weakening) from $\Gamma$ infer any $\Delta$ containing every member of $\Gamma$ ; (cut) from $A,\Gamma$ and $\overline{A},\Gamma$ infer $\Gamma$ . An $F_d$ -proof of $A$ is a sequence of sequents, each following from earlier ones by a rule (lines may be reused), in which every formula has depth at most $d$ , and which contains the sequent consisting of $A$ alone. Its size is the total size of all formulas in it.

Formalization targets

Write $\tau = (\tau_m)_{m\in\mathbb N}$ for a family of tautologies of depth at most $k$ with $|\tau_m| \ge m$ . It requires exponential $F_d$ -size if for some $\varepsilon>0$ and all large $m$ every $F_d$ -proof of $\tau_m$ has size at least $2^{|\tau_m|^{\varepsilon}}$ .

Goal

\exists k\ \forall d \ge k\ \exists \tau:\quad \tau_m \text{ has } F_{d+1}\text{-proofs of size } 2^{C(\log_2|\tau_m|)^C} \text{ and } \tau \text{ requires exponential } F_d\text{-size.}

The goal takes the weaker of the two upper bounds allowed by the problem (quasi-polynomial); the polynomial version implies it.

Milestones

Soundness of $F_d$ : every formula with an $F_d$ -proof is a tautology.
Completeness of $F_d$ for depth- $d$ formulas: every tautology of depth $\le d$ has an $F_d$ -proof.
Exponential $F_d$ lower bound for $\mathrm{PHP}^{n+1}_n$ : size $\ge 2^{n^{\varepsilon_d}}$ .
The depth-dependent separation: for all large $d$ , depth- $d$ tautologies with polynomial-size $F_{d+1}$ -proofs requiring exponential $F_d$ -size.

Significance

A positive answer would show that the extra power of depth $d+1$ over depth $d$ is visible already on formulas of a fixed, small depth, in particular that the hierarchy of bounded-depth Frege systems does not collapse on (for example) CNF tautologies. Through the correspondence with bounded arithmetic it bears on conservativity of theories of increasing quantifier complexity over a fixed class of low-complexity statements. A negative answer would say that for low-depth tautologies the bounded-depth Frege hierarchy collapses up to quasi-polynomial size.

Status: the goal is open. Milestones 1–2 are standard; milestones 3–4 are published theorems that, to the best of current knowledge, have no machine-checked proofs. Formalizing them requires switching-lemma machinery that would be reusable across proof complexity.

Difficulty

The known lower bounds for $F_d$ go through switching lemmas that simplify depth- $d$ formulas under random restrictions. In the known separations of $F_{d+1}$ from $F_d$ the hard tautologies have depth growing with $d$ . Keeping the formulas at one fixed depth $k$ while $d$ ranges over all values requires a lower-bound argument whose strength depends on the depth of the proof lines alone, uniformly in $d$ ; the switching-lemma arguments used for depth-dependent separations do not directly provide this.

Formalization scope

Formulas are the Lean inductive type FdVersusFdSucc.Formula over variables ℕ, with conjunctions and disjunctions of lists (so and [] is true and or [] is false). Depth counts literals as $0$ . $F_d$ is the dag-like one-sided sequent calculus described above; sequents are lists, weakening is by list inclusion. Proof size counts symbols of all formulas in all lines. Exponential lower bounds are asked only for all sufficiently large indices. The goal quantifies over $d \ge k$ : for $d+1 < k$ no $F_{d+1}$ -proof of a depth- $k$ formula exists, so "every $d$ " cannot be meant literally. A family whose formulas have depth $> d$ would satisfy the lower bound vacuously; this is excluded because the formulas must have depth at most $k \le d$ . The size condition $|\tau_m| \ge m$ rules out finite families.

Contributions welcome: proofs of soundness and completeness, a formalized switching lemma, and the classical lower bounds.

Selected references

J. Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59(1), 1994, 73–86.
J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and Its Applications 60, Cambridge University Press, 1995 (p. 243).
Open Problem Garden, F_d versus F_{d+1}, http://www.openproblemgarden.org/op/f_d_versus_f_d_1
M. Ajtai, The complexity of the pigeonhole principle, FOCS 1988.
J. Krajíček, P. Pudlák, A. Woods, An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle, Random Structures & Algorithms 7(1), 1995.
T. Pitassi, P. Beame, R. Impagliazzo, Exponential lower bounds for the pigeonhole principle, Computational Complexity 3, 1993.
S. Buss, Polynomial size proofs of the propositional pigeonhole principle, J. Symbolic Logic 52, 1987.
R. Impagliazzo, J. Krajíček, A note on conservativity relations among bounded arithmetic theories, Math. Logic Quarterly 48, 2002.

6 thms2 active usersReviewed

Operations Research Probability·Captain: Lucas

Symmetric Rendezvous on the LineOpen Problem

Motivation

Rendezvous search asks how two agents who cannot communicate should move so as to meet as quickly as possible. It was introduced as a mathematical problem by Alpern (The rendezvous search problem, SIAM J. Control Optim. 1995) and developed systematically in Alpern and Gal's monograph The Theory of Search Games and Rendezvous (Kluwer, 2003). Besides its game-theoretic interest, it is a model for coordination without prior agreement: robots or searchers that must find each other with no shared map or orientation.

The simplest non-trivial domain is the line. Even there, the version in which both agents must follow the same strategy remains open, and it is listed on the Open Problem Garden with importance "High".

Timeline:

1995. Alpern formulates symmetric rendezvous search problems, in which the players must use the same mixed strategy.
1995. Alpern and Gal (Rendezvous search on the line with distinguishable players, SIAM J. Control Optim. 33(4)) solve the asymmetric problem on the line, where the players may use different strategies: the optimal expected meeting time is $3.25$ .
1995–2008. A series of papers improve upper and lower bounds on the symmetric value.
2008. Han, Du, Vera and Zuluaga (Improved bounds for the symmetric rendezvous search problem on the line, Operations Research 56(3)) show that strategies moving at full speed and turning only at integer times dominate, reducing the problem to a discrete one, prove $4.1520 < R < 4.2574$ , and conjecture $R = 4.25$ .

Setting

Two players are placed on the real line at distance $2$ ; player I starts at $0$ and player II at $2$ . Each player has a private sense of "forward", fixed by an independent fair coin, so neither knows in which direction the other lies. Both move with speed at most $1$ .

A feasible path is a function $f$ with $f(0)=0$ and $|f(s)-f(t)|\le |s-t|$ for $s,t\ge 0$ , describing a player's position in its own frame. A mixed strategy $S$ is a probability distribution over feasible paths, realised as a probability space $(\Omega,P)$ and a random path $\omega\mapsto f_\omega$ whose position at each fixed time is measurable.

If player I follows $f$ with orientation $\varepsilon_1\in\{\pm1\}$ and player II follows $g$ with orientation $\varepsilon_2$ , their positions are $\varepsilon_1 f(t)$ and $2+\varepsilon_2 g(t)$ . The meeting time is

T=\inf\{t\ge 0:\ \varepsilon_1 f(t) = 2+\varepsilon_2 g(t)\}\in[0,\infty].

For strategies $S_1,S_2$ with independent randomisations, the expected meeting time $E(S_1,S_2)$ averages $T$ over $f\sim S_1$ , $g\sim S_2$ and the four equally likely orientation pairs. The symmetric rendezvous value and the asymmetric rendezvous value are

R=\inf_{S} E(S,S),\qquad R^a=\inf_{S_1,S_2}E(S_1,S_2).

An integer zigzag is a path that on each interval $[n,n+1]$ , $n\in\mathbb N$ , moves with velocity $+1$ or $-1$ ; $R_{\mathrm{disc}}$ denotes the infimum of $E(S,S)$ over strategies supported on integer zigzags.

Formalization targets

Goal: the conjectured value

R=\frac{17}{4}.

This is the Han–Du–Vera–Zuluaga conjecture and answers the Open Problem Garden question. A formal disproof is equally valuable.

Milestones from the literature

Alpern–Gal: $R^a = \dfrac{13}{4}$ .
Han–Du–Vera–Zuluaga reduction: $R = R_{\mathrm{disc}}$ .
Han–Du–Vera–Zuluaga lower bound: $4.1520 < R$ .
Han–Du–Vera–Zuluaga upper bound: $R < 4.2574$ .

Significance

The value $R$ measures the cost of symmetry in the most basic rendezvous problem: $R^a = 3.25$ when roles can be pre-assigned, while the best known symmetric strategies need about $4.25$ . Determining $R$ exactly would settle a problem that has been open since 1995 and would calibrate numerical methods (linear and semidefinite relaxations over discretised strategies) used for related search games.

None of these results is formalized. The milestones are proved on paper; formalizing them requires a measure-theoretic treatment of mixed strategies over path space, a rigorous version of the discretisation argument, and certified numerical bounds. The goal itself is open.

Difficulty

The obvious approach is to optimise over finitely many turning times, but a symmetric strategy must be randomised (any deterministic symmetric strategy fails to meet with probability $1/2$ , when both players face the same way), so the optimisation is over probability distributions on infinite paths and the objective is a quadratic, non-convex function of the distribution. Truncating to finite horizons gives upper bounds by explicit strategies, but lower bounds require controlling all strategies, including those that delay indefinitely, and the known gap $4.1520$ – $4.2574$ has resisted closing.

Formalization scope

All values live in $[0,\infty]$ and expectations are Lebesgue integrals of non-negative functions; a strategy that fails to meet with positive probability has value $\infty$ . Sample spaces range over a fixed universe, which loses no generality. Paths are required to be $1$ -Lipschitz on $[0,\infty)$ with $f(0)=0$ , and positions at fixed times are measurable, so meeting times are random variables. The four orientation pairs are weighted equally. The infimum in $R$ ranges over all such strategies, not only over integer zigzags; the restriction appears only in $R_{\mathrm{disc}}$ . A trivializing reading (e.g. a meeting time of $0$ or an unrestricted speed) is excluded: by construction every strategy pair has expected meeting time at least $1$ .

Contributions are welcome on: measurability of hitting times for continuous processes, the discretisation argument, explicit strategies with certified expected meeting times, and certified lower-bound certificates.

Selected references

S. Alpern, The rendezvous search problem, SIAM J. Control Optim. 33(3) (1995), 673–683.
S. Alpern, S. Gal, Rendezvous search on the line with distinguishable players, SIAM J. Control Optim. 33(4) (1995), 1270–1276.
S. Alpern, S. Gal, The Theory of Search Games and Rendezvous, International Series in Operations Research & Management Science 55, Kluwer, 2003.
Q. Han, D. Du, J. C. Vera, L. F. Zuluaga, Improved bounds for the symmetric rendezvous search problem on the line, Operations Research 56(3) (2008).
Open Problem Garden, Rendezvous on a line. http://www.openproblemgarden.org/op/rendezvous_on_a_line

9 thms2 active usersReviewed

Probability·Captain: Lucas

KPZ Universality Conjecture: Ballistic Deposition Height Fluctuations of Order t^{1/3}Open Problem

Motivation

A large family of random growth models, interacting particle systems and directed polymers in one space dimension share a common, non-Gaussian fluctuation theory: observables of size $t$ fluctuate on the scale $t^{1/3}$ (instead of the central-limit scale $t^{1/2}$ ), with spatial correlations on the scale $t^{2/3}$ . This family is the Kardar–Parisi–Zhang (KPZ) universality class, named after the 1986 physics paper of Kardar, Parisi and Zhang. The KPZ universality conjecture (Open Problem Garden, posted 2020, importance "High") asks for a central limit theorem for this class: any one-dimensional growth model with a smoothing mechanism, short-range noise and slope-dependent ("lateral") growth should exhibit KPZ fluctuations.

KPZ fluctuations have been proved only for models with exact algebraic structure, such as the corner growth model / totally asymmetric exclusion process (Johansson, 2000) and the polynuclear growth model (Prähofer–Spohn, 2002). The Open Problem Garden entry describes ballistic deposition (Vold, 1959) as a concrete growth model with the KPZ features. Corwin's survey states the prediction that its column heights fluctuate like $t^{1/3}$ and notes that "this prediction has not been proved" (Corwin 2012, §1.1.1). Ballistic deposition has no known exact solvability, so it tests universality itself rather than one integrable instance of it.

Timeline.

1959 — Vold introduces ballistic deposition as a sediment model.
1986 — Kardar–Parisi–Zhang predict the exponents $1/3$ and $2/3$ .
2000 — Seppäläinen proves a strong law of large numbers (hydrodynamic limit) for the ballistic deposition interface (arXiv:math/9906193).
2008 — Penrose proves linear growth of the mean height, $L^p$ laws of large numbers, polynomial moment bounds, a duality with a seed-grown process, and the only known lower bound on fluctuations: $\operatorname{Var}\xi_t(0)\gtrsim\log t$ in $d=1$ (arXiv:math/0608540).
2021 — Chatterjee proves existence of a stationary measure for the gradient process (arXiv:2110.10294).
2026 — Sudijono proves exponential concentration and the upper bound $\operatorname{Var}\xi_t(0)\le Ct$ (arXiv:2609.24056).

The gap between $\log t$ and $t$ is open; the predicted order is $t^{2/3}$ .

Setting

Columns are indexed by $x\in\mathbb Z$ . Each column carries an independent rate-one Poisson clock: on a probability space $(\Omega,P)$ the inter-arrival times $\tau_{x,k}$ , $(x,k)\in\mathbb Z\times\mathbb N$ , are independent and $\mathrm{Exp}(1)$ -distributed, and the $n$ -th ring of column $x$ (counting from $n=0$ ) is at time $T_{x,n}=\tau_{x,0}+\dots+\tau_{x,n}$ .

Random deposition. The height $N_t(x)$ of column $x$ at time $t$ is the number of rings of its clock in $[0,t]$ . Columns are independent and $N_t(x)$ is Poisson with mean $t$ .

Ballistic deposition (nearest-neighbour model, flat initial surface). Write $\xi_t(x)\in\mathbb N$ for the height of column $x$ at time $t$ , with $\xi_0\equiv0$ . When the clock of column $x$ rings at time $t$ , a unit block falls in column $x$ and sticks at the first point of contact, so

\xi_t(x)=\max\{\xi_{t-}(x)+1,\ \xi_{t-}(x-1),\ \xi_{t-}(x+1)\},

and all other columns are unchanged. On the finite substrate $Q_L=[-L,L]$ only clocks in $Q_L$ ring and columns outside $Q_L$ stay at height $0$ ; the finitely many rings in $[0,t]$ are applied in time order. The height on $\mathbb Z$ is the monotone limit $\xi_t(x)=\lim_{L\to\infty}\xi^{Q_L}_t(x)=\sup_L\xi^{Q_L}_t(x)$ . The next-arrival height is $\eta_t(x)=\max\{\xi_t(x)+1,\xi_t(x-1),\xi_t(x+1)\}$ . This is the model of Penrose (2008) with $d=1$ and the nearest-neighbour displacement function, and the model (1) of Sudijono (2026) with $d=1$ .

Formalization targets

Goal: the KPZ fluctuation exponent

\exists\,c,C>0,\ T:\qquad c\,t^{2/3}\ \le\ \operatorname{Var}\xi_t(0)\ \le\ C\,t^{2/3}\qquad(t\ge T).

This is the statement "the column height fluctuates around its mean like $t^{1/3}$ " (Corwin 2012, §1.1.1; Sudijono 2026, §1). The constants are left unspecified because they are model-dependent.

Stronger (not formalized here)

The predicted scaling limit: $(\xi_t(0)-\rho t)/(\sigma t^{1/3})$ converges in law to the Tracy–Widom GOE distribution for some model-dependent $\rho,\sigma>0$ .

Milestones (known results)

Random deposition CLT: $(N_t(0)-t)/\sqrt t\Rightarrow\mathcal N(0,1)$ , the Gaussian class, for contrast.
Penrose, Prop. 2.1: $\xi_t(0),\eta_t(0)<\infty$ a.s. and $E[\xi_t(0)^k],E[\eta_t(0)^k]=O(t^k)$ .
Penrose, Thm. 2.1: $E\xi_t(0)/t\to\rho_1\in(0,\infty)$ and $\xi_t(0)/t\to\rho_1$ in every $L^p$ , $p\ge1$ .
Seppäläinen, Thm. 1 (as noted in Penrose, p. 5): $\xi_t(0)/t\to\rho_1$ almost surely.
Penrose, Thm. 2.2: $\liminf_t\operatorname{Var}\xi_t(0)>0$ and $\liminf_t\operatorname{Var}\xi_t(0)/\log t>0$ .
Sudijono, Thm. 1.1 (2): $P(|\xi_t(0)-E\xi_t(0)|\ge r)\le C\exp(-c\,r^2/(t+r))$ for $t\ge1$ , $r\ge0$ .
Sudijono, Thm. 1.1 (3): $\operatorname{Var}\xi_t(0)\le Ct$ for $t\ge1$ .

Significance

A proof of the goal would establish the KPZ exponent for a growth model without exact solvability, which is the content of the universality conjecture as opposed to its integrable special cases. For ballistic deposition only $\log t\lesssim\operatorname{Var}\xi_t(0)\lesssim t$ is currently known.

On the formal side, the milestones are known results with published proofs; formalizing them requires a library for continuous-time interacting particle systems on $\mathbb Z$ (graphical constructions, monotone couplings, finite speed of propagation), subadditive ergodic theory, and concentration inequalities for Poisson-driven processes. These pieces are reusable for first-passage percolation and other growth models. The goal itself is open.

Difficulty

The standard tools give the wrong exponents. Bounded-difference concentration applied to a last-passage representation fails because adding one clock ring can change future heights by an unbounded amount (Sudijono 2026, §1); martingale hitting-time arguments reach only the diffusive bound $O(t)$ . Lower bounds of Pemantle–Peres type reach only $\log t$ , as in first-passage percolation, where the analogous gap is also open. The exact formulas (determinantal structure, Bethe ansatz) behind the proved instances of KPZ fluctuations are not available for ballistic deposition.

Formalization scope

The model is encoded on a general probability space $(\Omega,P)$ with inter-arrival times τ : ℤ → ℕ → Ω → ℝ satisfying IsPoissonClocks P τ (measurability, mutual independence over ℤ × ℕ, each law expMeasure 1). The finite-substrate process boxHeight τ L t ω sorts the rings in $[-L,L]\times[0,t]$ lexicographically by (time, column) and folds the update rule bdStep; bdHeight τ t x ω : ℕ∞ is the supremum over $L$ . Real-valued statements use bdHeightReal, which is bdHeight cast to ℝ with the value $0$ on the event $\{\xi_t(x)=\infty\}$ ; this event is null (Milestone 2), so the convention does not affect any distributional statement. Ties between rings and non-divergent arrival times are null events and receive junk values. Variances are Mathlib's variance, which returns $0$ for non-square-integrable variables; the lower bound in the goal therefore also forces square-integrability, so the goal cannot hold vacuously. Moments in Milestone 2 are lower Lebesgue integrals in $[0,\infty]$ , so they are not trivialised by non-integrability.

Contributions welcome: the graphical construction and its basic properties (monotonicity in $L$ and $t$ , a.s. finiteness), the duality with seed-grown deposition, subadditivity of hitting times, and the Poisson CLT.

Selected references

I. Corwin, The Kardar–Parisi–Zhang equation and universality class, Random Matrices Theory Appl. 1 (2012). https://arxiv.org/abs/1106.1596
M. Kardar, G. Parisi, Y.-C. Zhang, Dynamic scaling of growing interfaces, Phys. Rev. Lett. 56 (1986). https://doi.org/10.1103/PhysRevLett.56.889
T. Kojar (poster), KPZ Universality Conjecture, Open Problem Garden (2020). http://www.openproblemgarden.org/op/kpz_universality_conjecture
M. D. Penrose, Growth and roughness of the interface for ballistic deposition, J. Stat. Phys. 131 (2008). https://arxiv.org/abs/math/0608540
T. Seppäläinen, Strong law of large numbers for the interface in ballistic deposition, Ann. Inst. H. Poincaré Probab. Statist. 36 (2000). https://arxiv.org/abs/math/9906193
T. Sudijono, A linear variance bound for ballistic deposition, preprint (2026). https://arxiv.org/abs/2609.24056
S. Chatterjee, Existence of stationary ballistic deposition on the infinite lattice, preprint (2021). https://arxiv.org/abs/2110.10294
K. Johansson, Shape fluctuations and random matrices, Comm. Math. Phys. 209 (2000).
M. J. Vold, A numerical approach to the problem of sediment volume, J. Colloid Sci. 14 (1959).

9 thms2 active usersReviewed

Dynamical Systems Topology·Captain: Lucas

C^r Stability Conjecture (Palis–Smale)Open Problem

Motivation

Structural stability asks when the qualitative behaviour of a dynamical system survives small perturbations. A diffeomorphism $f$ of a closed manifold is structurally stable if every diffeomorphism $g$ close enough to $f$ is topologically conjugate to $f$ : some homeomorphism $h$ of the manifold satisfies $h\circ f=g\circ h$ , so that $h$ carries orbits of $f$ onto orbits of $g$ . Systems that model physical phenomena are only known up to small errors, which is the original reason for interest in this notion (Andronov–Pontryagin, 1937).

In the 1960s Smale introduced Axiom A, a uniform-hyperbolicity condition on the nonwandering set, and showed that it yields a detailed description of the dynamics (spectral decomposition, symbolic dynamics). Palis and Smale conjectured that structural stability forces this hyperbolic structure. The conjecture appears on the Open Problem Garden as the $C^r$ Stability Conjecture (openproblemgarden.org/op/c_r_stability_conjecture, rated Outstanding): any $C^r$ structurally stable diffeomorphism is hyperbolic. The same page describes the higher-regularity case as one of the most important and difficult problems in dynamical systems.

Timeline.

1967 — D. V. Anosov proves that Anosov diffeomorphisms (the whole manifold is a hyperbolic set) are structurally stable (Proc. Steklov Inst. Math. 90).
1970 — J. Palis and S. Smale prove that Morse–Smale diffeomorphisms are structurally stable and state the stability conjecture: $f$ is structurally stable if and only if $f$ satisfies Axiom A and the strong transversality condition (Global Analysis, Proc. Sympos. Pure Math. 14, AMS).
1971 — J. Robbin proves the "if" direction for $C^2$ diffeomorphisms (Ann. of Math. 94); J. Franks obtains necessary conditions for $C^1$ stability, including hyperbolicity of periodic points (Trans. Amer. Math. Soc. 158).
1976 — C. Robinson proves the "if" direction for $C^1$ diffeomorphisms (J. Differential Equations 22).
1988 — R. Mañé proves the "only if" direction in the $C^1$ topology: a $C^1$ structurally stable diffeomorphism satisfies Axiom A (Publ. Math. IHÉS 66). In the same volume J. Palis derives the $C^1$ $\Omega$ -stability conjecture.
1997 — S. Hayashi proves the analogous $C^1$ statements for flows (Ann. of Math. 145).

For every $r\ge 2$ the "only if" direction remains open.

Setting

Let $M$ be a closed manifold: a compact Hausdorff smooth manifold without boundary, of dimension $n$ . For an integer $r\ge 1$ , $\mathrm{Diff}^r(M)$ is the set of $C^r$ diffeomorphisms $f\colon M\to M$ , with the $C^r$ topology: $g$ is close to $f$ when, in finitely many charts and on compact sets, $g$ and its derivatives of order $\le r$ are uniformly close to those of $f$ .

A point $x$ is nonwandering for $f$ if for every neighbourhood $U$ of $x$ there is $k\ge 1$ with $f^k(U)\cap U\neq\emptyset$ . The nonwandering points form the compact invariant set $\Omega(f)$ . Every periodic point lies in $\Omega(f)$ .
A compact set $\Lambda$ with $f(\Lambda)=\Lambda$ is hyperbolic if, for a continuous Riemannian metric, each tangent space $T_xM$ , $x\in\Lambda$ , splits as $E^s(x)\oplus E^u(x)$ , the splitting is carried to itself by $Df$ , and there are $C>0$ and $0<\lambda<1$ with

\|Df^k_x v\|\le C\lambda^k\|v\|\ (v\in E^s(x)),\qquad \|Df^{-k}_x v\|\le C\lambda^k\|v\|\ (v\in E^u(x)),\qquad k\ge 0 .

$f$ satisfies Axiom A if $\Omega(f)$ is hyperbolic and the periodic points of $f$ are dense in $\Omega(f)$ . $f$ is Anosov if $M$ itself is hyperbolic.
$f$ is $C^r$ structurally stable if some $C^r$ neighbourhood of $f$ consists of diffeomorphisms topologically conjugate to $f$ . It is $C^r$ $\Omega$ -stable if for all $g$ in some $C^r$ neighbourhood, $f|_{\Omega(f)}$ and $g|_{\Omega(g)}$ are topologically conjugate.

Formalization targets

Goal: the $C^r$ stability conjecture

For every closed manifold $M$ , every $r\ge 1$ and every $f\in\mathrm{Diff}^r(M)$ ,

f \text{ is } C^r \text{ structurally stable} \;\Longrightarrow\; f \text{ satisfies Axiom A}.

The case $r=1$ is Mañé's theorem; the cases $r\ge 2$ are open.

Milestones

Franks (1971). A $C^1$ structurally stable diffeomorphism has only hyperbolic periodic points.
Consequence of Pugh's closing lemma. For a $C^1$ structurally stable $f$ , $\overline{\mathrm{Per}(f)}=\Omega(f)$ .
Mañé (1988). The goal for $r=1$ .
Palis (1988). A $C^1$ $\Omega$ -stable diffeomorphism satisfies Axiom A.
Anosov (1967). For every $r\ge1$ , an Anosov $C^r$ diffeomorphism is $C^r$ structurally stable.

Significance

The result. A positive answer would give a dynamical characterization of structural stability in every regularity: together with the theorems of Robbin and Robinson (Axiom A plus strong transversality implies stability), it would show that structurally stable diffeomorphisms are exactly the hyperbolic ones with transverse stable and unstable manifolds. Every structurally stable system would then inherit Smale's spectral decomposition and its symbolic models. In the $C^1$ topology this picture is complete (Mañé); in higher regularity it is not known whether a structurally stable system can fail to be hyperbolic.

Formalizing it. The mission produces a common Lean vocabulary for hyperbolic sets, Axiom A, and structural and $\Omega$ -stability of diffeomorphisms of closed manifolds, compatible with the existing $C^r$ topology and nonwandering-set definitions on the platform. The proved cases (Anosov, Franks, Mañé, Palis) are milestones whose formal proofs would be new contributions; the goal itself is open for $r\ge 2$ .

Difficulty

The known $C^1$ proof rests on perturbation tools that work only in the $C^1$ topology: Franks' lemma (realizing any small change of the derivative along a periodic orbit by a $C^1$ -small perturbation), Pugh's closing lemma and Mañé's ergodic closing lemma. In the $C^r$ topology, $r\ge 2$ , a perturbation that changes the derivative by a fixed amount on a small ball has large higher derivatives, so these local constructions are not $C^r$ -small; Gutierrez's examples on the torus show that the local perturbation schemes used for the $C^1$ closing lemma cannot work in the $C^2$ topology. Whether periodic points are even dense in $\Omega(f)$ for a $C^r$ structurally stable $f$ is a case of the $C^r$ closing problem, itself open.

Formalization scope

$M$ is a type with [TopologicalSpace M] [T2Space M] [CompactSpace M], a ChartedSpace structure over EuclideanSpace ℝ (Fin n) and IsManifold (𝓡 n) ∞ M (smooth, no boundary). $\mathrm{Diff}^r(M)$ is ClosingLemma.Diff n M r with the weak $C^r$ topology ClosingLemma.crTopology r (published definition ClosingLemma_DiffeoCrTopology); on compact $M$ it coincides with the strong topology. $r$ is a natural number with $r\ge 1$ ; $r=\infty$ is not covered.
$\Omega(f)$ is PughClosingLemma.nonwanderingSet (published definition PughClosingLemma_nonwandering).
Hyperbolicity uses mfderiv and an arbitrary continuous Riemannian metric (Bundle.ContinuousRiemannianMetric on the tangent bundle); since $M$ is compact, the choice of metric only changes $C$ . Continuity of the splitting is not assumed, being a consequence of the estimates. A periodic point is hyperbolic when its finite orbit is a hyperbolic set, which is equivalent to the eigenvalue condition.
Axiom A requires density of periodic points in $\Omega(f)$ as a separate condition, following Smale's definition.
Structural stability asks only for a conjugating homeomorphism, without requiring it to be close to the identity. The strong transversality part of the Palis–Smale conjecture is not part of the goal.
Infrastructure needed: stable manifold theory for hyperbolic sets, shadowing, Franks' lemma and closing lemmas on manifolds. These are reusable beyond this mission, and contributions of them are welcome.

Selected references

Open Problem Garden, $C^r$ Stability Conjecture, posted December 20, 2007. https://www.openproblemgarden.org/op/c_r_stability_conjecture
D. V. Anosov, Geodesic flows on closed Riemannian manifolds with negative curvature, Proc. Steklov Inst. Math. 90, 1967.
J. Palis, S. Smale, Structural stability theorems, Global Analysis, Proc. Sympos. Pure Math. 14, AMS, 1970.
J. Robbin, A structural stability theorem, Ann. of Math. 94, 1971.
J. Franks, Necessary conditions for stability of diffeomorphisms, Trans. Amer. Math. Soc. 158, 1971.
C. Robinson, Structural stability of $C^1$ diffeomorphisms, J. Differential Equations 22, 1976.
R. Mañé, A proof of the $C^1$ stability conjecture, Publ. Math. IHÉS 66, 1988.
J. Palis, On the $C^1$ $\Omega$ -stability conjecture, Publ. Math. IHÉS 66, 1988.
S. Hayashi, Connecting invariant manifolds and the solution of the $C^1$ stability and $\Omega$ -stability conjectures for flows, Ann. of Math. 145, 1997.
C. Pugh, An improved closing lemma and a general density theorem, Amer. J. Math. 89, 1967.

12 thms2 active usersReviewed

Dynamical Systems·Captain: Lucas

Palis Conjecture: Denseness of Finitude of AttractorsOpen Problem

Motivation

A basic aim of the theory of dynamical systems is to describe the long-term behaviour of typical orbits of typical systems. In the 1960s Smale's programme hoped that hyperbolic (structurally stable) systems would be dense, so that the asymptotic behaviour of a dense set of systems would be described by finitely many hyperbolic pieces. This hope fails: there are open sets of diffeomorphisms none of which is hyperbolic. Jacob Palis proposed a replacement global picture, in which hyperbolicity is replaced by a statistical requirement: for a dense set of systems, the asymptotics of Lebesgue-almost every orbit is captured by finitely many attractors. The problem appears on the Open Problem Garden (page), rated Outstanding, with the monograph of Bonatti, Diaz and Viana as reference.

Timeline.

1962 — Peixoto: on a compact orientable surface, structurally stable vector fields (which are Morse–Smale) form an open and dense subset of $\mathfrak X^r(M)$ , $r\ge1$ . In particular the flow version of the conjecture holds on orientable surfaces (Topology 1, 1962).
1970s — Sinai, Ruelle and Bowen: for $C^2$ Axiom A systems, Lebesgue-almost every point lies in the basin of one of finitely many hyperbolic attractors (Bowen, Equilibrium States and the Ergodic Theory of Anosov Diffeomorphisms, LNM 470, 1975; Bowen–Ruelle, Invent. Math. 29, 1975).
1974 — Newhouse: there are open sets of $C^2$ surface diffeomorphisms in which a residual subset has infinitely many sinks. Hence finitude of attractors cannot hold on an open and dense set in general, and dense is the natural quantifier.
2000 — Palis states the global conjecture on the denseness of finitude of attractors (Astérisque 261), together with companion conjectures on physical measures and stochastic stability.
2000 — Pujals–Sambarino: every $C^1$ surface diffeomorphism can be $C^1$ -approximated by a hyperbolic one or by one with a homoclinic tangency (Ann. of Math. 151).

The conjecture is open in general.

Setting

Let $M$ be a compact, connected, boundaryless smooth manifold of dimension $n$ . For $r\ge1$ let $\mathrm{Diff}^r(M)$ be the space of $C^r$ diffeomorphisms of $M$ and $\mathfrak X^r(M)$ the space of $C^r$ vector fields, both with the $C^r$ topology (uniform convergence of the maps and of their derivatives up to order $r$ in charts).

For a diffeomorphism $f$ and $p\in M$ , the $\omega$ -limit set $\omega(p)$ is the set of accumulation points of the forward orbit $f^k(p)$ , $k\to\infty$ ; for a flow $(\varphi_t)_{t\in\mathbb R}$ it is the set of accumulation points of $\varphi_t(p)$ as $t\to+\infty$ . The basin of a set $\Lambda\subset M$ is

B(\Lambda)=\{p\in M:\ \omega(p)\subset\Lambda\}.

Following the source, $\Lambda$ is an attractor if it is invariant ( $f(\Lambda)=\Lambda$ , resp. $\varphi_t(\Lambda)=\Lambda$ for all $t$ ), transitive (some point of $\Lambda$ has a forward orbit dense in $\Lambda$ ), and $B(\Lambda)$ has positive Lebesgue measure. A set has Lebesgue measure zero in $M$ if its image in every chart has Lebesgue measure zero in $\mathbb R^n$ ; this notion does not depend on the smooth atlas.

Formalization targets

Goal: the Palis conjecture

For every $r\ge1$ there is a dense set $D\subset\mathrm{Diff}^r(M)$ such that every $f\in D$ has finitely many attractors $\Lambda_1,\dots,\Lambda_k$ with

\mathrm{Leb}\Big(M\setminus\bigcup_{i=1}^k B(\Lambda_i)\Big)=0,

and likewise there is a dense set $D\subset\mathfrak X^r(M)$ such that the flow of every $X\in D$ has finitely many attractors whose basins cover Lebesgue-almost all of $M$ .

Milestones

The diffeomorphism version and the flow version of the conjecture, separately.
Dimension one: the diffeomorphism version on the circle.
Peixoto: the flow version on compact orientable surfaces.
Basic facts fixing the meaning of the definitions: a hyperbolic sink is an attractor; the identity map (dimension $\ge1$ ) does not have finitely many attractors covering almost all of $M$ ; every $C^r$ vector field on a compact boundaryless manifold has a unique global flow.

Significance

The result. A positive answer would give a dense set of systems whose statistical behaviour is completely described by finitely many invariant pieces, providing a global substitute for the failed density of hyperbolicity. It underlies Palis' companion conjectures on the existence of finitely many physical (SRB) measures and their stochastic stability.

Formalizing it. The full conjecture is open. The mission produces a reusable formal language for $C^r$ diffeomorphisms and vector fields of compact manifolds, $C^r$ density, Lebesgue-null sets on manifolds, $\omega$ -limit sets, basins and attractors, together with formal statements of the classical cases (circle diffeomorphisms; Peixoto's theorem on orientable surfaces).

Difficulty

The obvious route — perturb to a hyperbolic system and invoke the Axiom A theory — fails because hyperbolic systems are not dense in dimension $\ge2$ for diffeomorphisms (Newhouse phenomenon, robust homoclinic tangencies and heterodimensional cycles). One must control systems near which non-hyperbolic phenomena persist on open sets, where generic systems can have infinitely many sinks, and still find dense subsets with finitely many attractors. Even in the classical cases the proofs require the full machinery of hyperbolic critical elements, stable manifolds and the Kupka–Smale theorem.

Formalization scope

$M$ is a Hausdorff, compact, connected topological space with a charted-space structure modelled on EuclideanSpace ℝ (Fin n) and a $C^\infty$ manifold structure IsManifold (𝓡 n) ∞ M; the model has no boundary, so $M$ is boundaryless.
$r$ is a natural number with $r\ge1$ (the $C^\infty$ topology is not covered). $\mathrm{Diff}^r(M)$ is M ≃ₘ^r⟮𝓡 n, 𝓡 n⟯ M; vector fields are sections (x : M) → TangentSpace (𝓡 n) x, of class $C^r$ when $x\mapsto(x,X(x))$ is $C^r$ into the tangent bundle.
Density is expressed with sequences: every element is the $C^r$ limit of a sequence from $D$ (equivalent to topological density since the $C^r$ topology on a compact manifold is metrizable). $C^r$ convergence of maps is compact-open convergence plus uniform convergence on compact subsets of chart domains of all derivatives of order $\le r$ of the chart representatives; for vector fields, the same for the chart representatives $y\mapsto De(e^{-1}y)\,X(e^{-1}y)$ .
A set is Lebesgue-null if its image under every chart of the atlas has Lebesgue outer measure zero. $\omega$ -limits use Mathlib's omegaLimit along atTop. Transitivity means the closure of a forward orbit of a point of $\Lambda$ equals $\Lambda$ .
Flows: the flow statements quantify over every global flow $\Phi$ of $X$ ( $\Phi_0=\mathrm{id}$ , each orbit an integral curve of $X$ ); a milestone states that such a flow exists and is unique, so these statements are not vacuous.
The goal is not trivialized by taking $D$ to be all systems: the identity milestone shows that the finitude property fails for some diffeomorphisms.
Reusable infrastructure: Lebesgue-null sets on manifolds, $C^r$ convergence and density, attractors and basins, flows of vector fields on compact manifolds. Contributions such as hyperbolic fixed points and periodic orbits, stable manifold theorems, rotation numbers of circle diffeomorphisms, and Morse–Smale systems are welcome.

Selected references

J. Palis, A global view of dynamics and a conjecture on the denseness of finitude of attractors, Astérisque 261 (2000), 335–347.
J. Palis, A global perspective for non-conservative dynamics, Ann. Inst. H. Poincaré Anal. Non Linéaire 22 (2005), 485–507.
C. Bonatti, L. J. Díaz, M. Viana, Dynamics Beyond Uniform Hyperbolicity, Encyclopaedia of Mathematical Sciences 102, Springer, 2005.
M. M. Peixoto, Structural stability on two-dimensional manifolds, Topology 1 (1962), 101–120.
S. E. Newhouse, Diffeomorphisms with infinitely many sinks, Topology 13 (1974), 9–18.
R. Bowen, Equilibrium States and the Ergodic Theory of Anosov Diffeomorphisms, Lecture Notes in Math. 470, Springer, 1975.
R. Bowen, D. Ruelle, The ergodic theory of Axiom A flows, Invent. Math. 29 (1975), 181–202.
E. R. Pujals, M. Sambarino, Homoclinic tangencies and hyperbolicity for surface diffeomorphisms, Ann. of Math. 151 (2000), 961–1023.
J. Palis, W. de Melo, Geometric Theory of Dynamical Systems: An Introduction, Springer, 1982.
W. de Melo, S. van Strien, One-Dimensional Dynamics, Springer, 1993.
Open Problem Garden: https://www.openproblemgarden.org/op/jacob_palis_conjecture_finitude_of_attractors_dynamical_systems

13 thms2 active usersReviewed

Dynamical Systems Topology·Captain: Lucas

C^r Closing Lemma for DiffeomorphismsOpen Problem

Motivation

A central question in smooth dynamics is how much of the long-term behaviour of a system is captured by its periodic orbits. Every periodic point is nonwandering (each of its neighbourhoods returns to itself under some iterate), but a nonwandering point need not be periodic. The closing lemma asks whether this gap can be removed by an arbitrarily small perturbation: given a nonwandering point $p$ of a diffeomorphism $f$ , is there a diffeomorphism $g$ , as close to $f$ as desired, for which $p$ is a periodic point?

The answer controls the generic picture of dynamics. Pugh's General Density Theorem, which rests on the closing lemma, says that for a generic $C^1$ diffeomorphism of a closed manifold the periodic points are dense in the nonwandering set. Results of this kind underlie the $C^1$ -generic theory of dynamical systems (stability conjectures, generic properties of homoclinic classes). Whether the same holds for smoother perturbations is open; the question appears on the Open Problem Garden (closing lemma for diffeomorphisms, rated Outstanding) and is Problem 10 on Smale's 1998 list of mathematical problems for the next century.

Timeline.

1967 — C. Pugh proves the closing lemma for $C^1$ perturbations of diffeomorphisms of a compact manifold, together with the General Density Theorem (Amer. J. Math. 89).
1983 — C. Pugh and C. Robinson extend the $C^1$ closing lemma to flows and to conservative and Hamiltonian systems (Ergodic Theory Dynam. Systems 3).
1987 — C. Gutierrez constructs examples on the torus showing that the local perturbation schemes used for $C^1$ cannot work in the $C^2$ topology (Ergodic Theory Dynam. Systems 7).
1997 — S. Hayashi proves the $C^1$ connecting lemma (Ann. of Math. 145); the Open Problem Garden credits him with the $C^1$ case for flows.
2016 — M. Asaoka and K. Irie prove a $C^\infty$ closing lemma for Hamiltonian diffeomorphisms of closed surfaces (arXiv:1512.06336), a special conservative setting in which the closing is obtained near a given open set rather than at a prescribed point.

For general diffeomorphisms and every $r > 1$ the problem remains open.

Setting

Let $M$ be a closed manifold: a compact Hausdorff smooth manifold without boundary, of dimension $n$ . For $r \ge 1$ , $\mathrm{Diff}^r(M)$ is the set of $C^r$ diffeomorphisms of $M$ .

The $C^r$ topology on $\mathrm{Diff}^r(M)$ is defined through charts. For $f \in \mathrm{Diff}^r(M)$ , smooth charts $(\varphi, U)$ and $(\psi, V)$ of $M$ , a compact set $K \subseteq U$ with $f(K) \subseteq V$ , and $\varepsilon > 0$ , the basic set

\mathcal N^r(f;\varphi,\psi,K,\varepsilon) = \Big\{ g : g(K)\subseteq V,\ \big\|D^k(\psi g \varphi^{-1})(x) - D^k(\psi f \varphi^{-1})(x)\big\| < \varepsilon \text{ for all } x \in \varphi(K),\ 0 \le k \le r \Big\}

collects the diffeomorphisms whose local representative has all derivatives of order at most $r$ uniformly within $\varepsilon$ of those of $f$ on $\varphi(K)$ . These sets generate the (weak) $C^r$ topology; on a closed manifold it coincides with the Whitney $C^r$ topology.

For a map $f\colon M\to M$ , a point $p$ is nonwandering if every neighbourhood $U$ of $p$ satisfies $f^k(U)\cap U\neq\emptyset$ for some $k\ge 1$ ; the set of such points is the nonwandering set $\Omega(f)$ . A point $p$ is periodic for $g$ if $g^m(p)=p$ for some $m\ge1$ .

Formalization targets

Goal: the $C^r$ closing lemma

For every closed manifold $M$ , every $r\ge 1$ , every $f\in\mathrm{Diff}^r(M)$ and every $p\in\Omega(f)$ :

\forall\, \mathcal V \ni f \text{ a } C^r\text{-neighbourhood},\quad \exists\, g\in\mathcal V,\ \exists\, m\ge 1:\ g^m(p)=p .

Milestones

Compatibility of $C^1$ topologies. The $C^1$ topology defined above through charts coincides with the $C^1$ topology induced by the tangent maps $g\mapsto Tg$ (compact-open topology on maps of the tangent bundle), used by the published statements of Pugh's theorems. Together with milestone 2 it yields the goal for $r = 1$ .
Pugh's $C^1$ closing lemma (1967) — the case $r=1$ (published platform statement).
Pugh's General Density Theorem (1967) — for a residual set of $g\in\mathrm{Diff}^1(M)$ , $\overline{\mathrm{Per}(g)}=\Omega(g)$ (published platform statement).

Significance

A $C^r$ closing lemma for $r\ge2$ would give, through the same Baire-category argument as in Pugh's work, a $C^r$ General Density Theorem: $C^r$ -generic diffeomorphisms would have periodic points dense in the nonwandering set. Much of the $C^1$ -generic theory would then become available in the smoother topologies used in smooth ergodic theory, where distortion estimates need at least $C^{1+\alpha}$ regularity.

On the formal side, the mission produces a reusable definition of the $C^r$ topology on diffeomorphism groups, which Mathlib does not currently provide. The $r=1$ case is a theorem (Pugh 1967) without a machine-checked proof; formalizing it, and the compatibility of the two $C^1$ topologies, are concrete sub-goals. The case $r\ge 2$ is open, so a proof of the goal would be a new mathematical result.

Difficulty

A perturbation that makes an almost-returning orbit close up must move the orbit by a distance comparable to how close it comes back. With $C^1$ control, the perturbation can be spread over many iterates, and its $C^1$ size stays small because derivatives are only constrained to first order. For $r\ge2$ , the $C^r$ norm of a bump of displacement $\delta$ supported on a set of diameter $\rho$ scales like $\delta/\rho^r$ , and spreading the perturbation along the orbit no longer keeps it small. Gutierrez's examples show that the local perturbation schemes that work for $r=1$ do fail in the $C^2$ topology, so the natural first idea of copying Pugh's argument is ruled out.

Formalization scope

$M$ is a type with a charted-space structure modelled on EuclideanSpace ℝ (Fin n) and a $C^\infty$ manifold structure (IsManifold (𝓡 n) ∞ M), assumed compact and Hausdorff. Because the model space has no corners, $M$ has no boundary.
$\mathrm{Diff}^r(M)$ is Mathlib's Diffeomorph (𝓡 n) (𝓡 n) M M r, with $r$ a natural number.
The $C^r$ topology ClosingLemma.crTopology r is generated by Hirsch's basic sets, using charts of the maximal $C^\infty$ atlas and Fréchet derivatives of order $0,\dots,r$ of the local representatives at points of $\varphi(K)$ . The goal quantifies over all neighbourhoods of $f$ for this topology.
The nonwandering set is the published PughClosingLemma.nonwanderingSet, shared with the existing statements of Pugh's theorems; periodic points are Mathlib's Function.periodicPts (period at least $1$ ).
The hypothesis $r\ge1$ matches the source; $r=1$ is included in the goal, so the goal is a uniform statement for all finite $r\ge1$ .

Infrastructure that would help: a usable API for the $C^r$ topology (basic neighbourhoods, compatibility under change of charts, the Baire property of $\mathrm{Diff}^r(M)$ ), and local perturbation lemmas (bump-function perturbations of the identity supported in a chart, with $C^r$ estimates). Contributions of these as separate lemmas are welcome.

Selected references

C. C. Pugh, An improved closing lemma and a general density theorem, Amer. J. Math. 89 (1967), 1010–1021. https://doi.org/10.2307/2373414
C. C. Pugh and C. Robinson, The $C^1$ closing lemma, including Hamiltonians, Ergodic Theory Dynam. Systems 3 (1983), 261–313.
C. Gutierrez, A counter-example to a $C^2$ closing lemma, Ergodic Theory Dynam. Systems 7 (1987), 509–530.
S. Hayashi, Connecting invariant manifolds and the solution of the $C^1$ stability and $\Omega$ -stability conjectures for flows, Ann. of Math. 145 (1997), 81–137.
M. Asaoka and K. Irie, A $C^\infty$ closing lemma for Hamiltonian diffeomorphisms of closed surfaces, Geom. Funct. Anal. 26 (2016). https://arxiv.org/abs/1512.06336
S. Smale, Mathematical problems for the next century, Math. Intelligencer 20 (1998), 7–15.
M. W. Hirsch, Differential Topology, Springer GTM 33, Ch. 2 (definition of the $C^r$ topologies).
Open Problem Garden, Closing Lemma for Diffeomorphism (Dynamical Systems). https://www.openproblemgarden.org/op/closing_lemma_for_diffeomorphism_dynamical_systems

5 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Carneiro 2012: Inflation and Decaying Vacuum from Particle CreationResearch Paper

Motivation

In a spatially flat Friedmann–Lemaître–Robertson–Walker (FLRW) universe the expansion is described by the Hubble parameter $H(t)=\dot a/a$ . A long-standing line of work treats the vacuum energy density $\Lambda$ not as a constant but as a quantity that decays as particles are created out of the vacuum in the expanding spacetime. If total energy is conserved, a time-varying vacuum density must be accompanied by particle production, and conversely the creation rate fixes how $\Lambda$ depends on $H$ .

S. Carneiro's 2012 paper (DOI 10.1142/S2010194512008173) applies this idea at both ends of cosmic history. At late times, creation of ultra-light non-relativistic dark particles gives a vacuum density $\Lambda\propto H$ , the law expected for the QCD vacuum condensate in a low-energy expanding spacetime. At early times, creation of relativistic particles gives $\Lambda\propto H^2$ and an inflationary solution with constant slow-roll parameter. The paper also recalls a non-singular model in which $\Lambda = 3H^4$ drives a transition from a de Sitter phase to a radiation phase.

Setting

Units are $8\pi G=c=1$ . All quantities are real functions of cosmological time $t$ on an open time interval $I$ :

$H$ , the Hubble parameter;
$\rho_m$ , the energy density of the created matter, with pressure $p_m$ (either $p_m=\rho_m/3$ for relativistic matter or $p_m=0$ for non-relativistic matter);
$\Lambda$ , the vacuum energy density, with pressure $p_\Lambda=-\Lambda$ .

The total density and pressure are $\rho=\rho_m+\Lambda$ and $p=p_m-\Lambda$ . The equations used are:

the flat Friedmann equation $\rho_m+\Lambda=3H^2$ ;
total energy conservation $\dot\rho+3H(\rho+p)=0$ ;
a balance equation for the created matter: $\dot\rho_m+3H\rho_m=\Gamma\rho_m$ with constant rate $\Gamma$ (late times, Eq. (7)), or $\dot\rho_m+3H(\rho_m+p_m)=\gamma H\rho_m$ with constant $\gamma$ (early times, Eq. (13)).

The slow-roll parameter is $\varepsilon=-\dot H/H^2$ , and the matter fraction is $\Omega_m=\rho_m/(3H^2)$ . In the equivalent scalar-field description, $H$ is regarded as a function of a field $\varphi$ , and the field equations are $3H^2=V+2H'^2$ and $\dot\varphi=-2H'$ , with $'$ the derivative with respect to $\varphi$ .

Formalization targets

Goal: the inflation solution (Eq. (17))

If $\dot\rho_m+4H\rho_m=\gamma H\rho_m$ , $\rho_m+\Lambda=3H^2$ and $\Lambda=\tfrac{3\gamma}{4}H^2$ with $\gamma\neq 4$ , then on any time interval where $H\neq0$ ,

\frac1H=\varepsilon t+\frac1{H_0},\qquad \varepsilon=\frac{4-\gamma}{2},

for an integration constant $H_0$ .

Milestones

Eq. (4): with $\Lambda=3H^4$ and relativistic matter, $\dot H+2H^2-2H^4=0$ .
Eq. (5): $2t=1/H-\operatorname{artanh}H$ defines a solution with $0<H<1$ that tends to de Sitter ( $H\to1$ ) as $t\to-\infty$ and to a radiation phase ( $Ht\to1/2$ ) as $t\to\infty$ .
Eq. (10): at late times, energy conservation holds if and only if $\Lambda=2\Gamma H+\lambda_0$ .
Eq. (11): if $\Lambda=2\Gamma H$ , then $\Gamma=\tfrac32(1-\Omega_m)H$ .
Eq. (16): at early times, energy conservation holds if and only if $\Lambda=\tfrac{3\gamma}{4}H^2+\Lambda_0$ .
Text after Eqs. (17)–(18): $-\dot H/H^2=\varepsilon$ is constant and $\Omega_m=\varepsilon/2$ .
Eq. (23): in the scalar-field description with $V=3\gamma H^2/4$ , $1/H=\varepsilon t+1/H_0$ with $\varepsilon=\tfrac32\cdot\tfrac{4-\gamma}{2}$ .
Eq. (24): $V(\varphi)=\tfrac{3\gamma H_0^2}{4}e^{\pm\sqrt{2\varepsilon}\,\varphi}$ and $V''/V=(V'/V)^2=2\varepsilon$ .

Significance

Eq. (17) is the paper's central claim that particle creation with backreaction produces inflation with constant $\varepsilon$ , and so with a scale-invariant spectrum and spectral index $n_s=1-2\varepsilon$ . Eqs. (10)–(11) give the late-time decaying-vacuum law behind the paper's concordance model, and Eqs. (4)–(5) give the non-singular de Sitter-to-radiation transition. These derivations have not been machine-checked before. A formal development makes explicit the regularity assumptions and side conditions the paper leaves implicit, such as $H\neq0$ , $\gamma\neq4$ , and the non-degeneracy condition $3H\neq\Gamma$ in Eq. (10).

Difficulty

Most steps are short calculations, but each one hides analytic content. Deriving relations between functions from equations between derivatives (Eqs. (10), (16), (17), (23)) needs the fact that a function with zero derivative on a connected open set is constant. Eq. (5) defines $H$ implicitly, so the existence, differentiability and asymptotics of the inverse function must be established. Eq. (24) requires showing that the sign in $H'=\pm\sqrt{\varepsilon/2}\,H$ cannot switch, even though $H'$ is not assumed continuous.

Formalization scope

Functions are maps $\mathbb R\to\mathbb R$ , time derivatives are Mathlib's deriv, and differentiability is assumed at every point of the time interval $I$ . The interval is an open, preconnected subset of $\mathbb R$ , because the solutions of the paper generally exist only on a half-line: for example, $1/H=\varepsilon t+1/H_0$ vanishes at a finite time. A statement assuming a global-in-time solution would be vacuous. Constants of integration are existentially quantified. The integration constant $H_0$ enters only through $1/H_0$ , and Lean's convention $1/0=0$ makes this the same as an arbitrary real constant. The numerical and observational parts of the paper (data fits, $n_s\approx0.97$ ) and the perturbation analysis (Eqs. (19)–(20)) are out of scope.

Selected references

S. Carneiro, Cosmological Concordance Model with Particle Creation, Int. J. Mod. Phys. Conf. Ser. 18 (2012) 38–47. https://doi.org/10.1142/S2010194512008173

9 thms2 active usersReviewed

Completed

Mathematical Physics·Captain: Lucas

Carneiro 2006: From de Sitter to de Sitter — a non-singular universe driven by vacuumResearch Paper

Motivation

The cosmological constant problem is the mismatch between the vacuum energy density predicted by quantum field theory in flat space–time and the small value of the cosmological term inferred from observations (Weinberg 1989). One line of work replaces the constant by a decaying vacuum: a time-dependent cosmological term $\Lambda(t)$ that falls as the universe expands, while the energy it loses is transferred to matter so that total energy is conserved.

S. Carneiro's essay From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum (Int. J. Mod. Phys. D 15 (2006) 2241–2247, honorable mention in the 2006 Gravity Research Foundation essay competition) derives such a law from a semi-classical argument, $\Lambda\approx(m+H)^4-m^4$ , and studies the cosmologies it produces. In the early-time regime $\Lambda\approx H^4$ it finds a universe with no initial singularity: an eternal quasi-de Sitter phase at the Planck scale, followed by a fast transition to a radiation era. In the late-time regime $\Lambda\approx m^3H$ it finds a dust era that tends again to a de Sitter universe. The calculations in the paper are explicit closed-form computations, which makes them a good target for a complete machine-checked development.

Setting

All quantities are in Planck units, and space is flat. The expansion is described by the Hubble parameter $H(t)=\dot a(t)/a(t)$ of a scale factor $a(t)$ . The cosmic fluid has total energy density $\rho_T=\rho_m+\Lambda$ and total pressure $p_T=p_m-\Lambda$ , where $\rho_m,p_m$ are the matter density and pressure and $\Lambda$ is the vacuum term. The Friedmann equation is $\rho_T=3H^2$ and the conservation equation is

\dot\rho_T+3H(\rho_T+p_T)=0 .

Radiation has $p_m=\rho_m/3$ and dust has $p_m=0$ . The relative energy densities are $\Omega_m=\rho_m/\rho_T$ and $\Omega_\Lambda=\Lambda/\rho_T$ , and the deceleration parameter is $q=-1-\dot H/H^2$ .

The vacuum term comes from a massless scalar field $\phi$ obeying $\ddot\phi+3H\dot\phi-\nabla^2\phi=0$ . For slowly varying $H$ this has the damped radial plane-wave solution $\phi=\phi_0e^{-br}e^{-i(\omega t-kr)}$ , with $k(\omega,H)$ and $b(\omega,H)$ given by explicit square-root formulas (Eqs. (7)–(8)), and energy density $(\omega^2+b^2)|\phi|^2$ . Shifting the cutoff $m$ of the thermally regularized vacuum integral $\int_0^\infty\omega^3\,d\omega/(e^{\omega/m}-1)$ by $b\approx H$ and subtracting the flat-space value gives the vacuum term $\Lambda(m,H)=(m+H)^4-m^4$ . In the mission's Lean development these objects are waveNumber, dampingRate, planeWave, vacuumTerm, dustScaleFactor and decelerationParameter, all in the namespace CarneiroDeSitter.

Formalization targets

Goal: the non-singular early universe

With radiation and $\Lambda=3H^4$ , the evolution equation is $\dot H+2H^2-2H^4=0$ (Eq. (12)). The goal asserts that it has a solution defined for all times, given implicitly by Eq. (13):

\exists\,H:\mathbb R\to(0,1),\quad 2t=\frac1{H(t)}-\operatorname{artanh}H(t),\quad \dot H=-2H^2+2H^4,\quad H\xrightarrow[t\to-\infty]{}1,\quad H\xrightarrow[t\to+\infty]{}0 .

Milestones (in the order of the paper)

Eq. (2): $\int_0^\infty\frac{\omega^3\,d\omega}{e^{\omega/m}-1}=\frac{\pi^4}{15}m^4$ .
Eqs. (5)–(8): the damped plane wave solves $\ddot\phi+3H\dot\phi-\partial_r^2\phi=0$ for constant $H$ .
Eqs. (9)–(10): its energy density is $(\omega^2+b^2)|\phi|^2$ .
Eq. (11): $(m+H)^4-m^4\sim H^4$ as $H\to\infty$ and $\sim4m^3H$ as $H\to0^+$ .
Eq. (12): the conservation equation with $\rho_T=3H^2$ , $\Lambda=3H^4$ , $p_m=\rho_m/3$ gives $\dot H+2H^2-2H^4=0$ .
Eq. (13): every solution on $\mathbb R$ with $0<H<1$ satisfies $2(t-t_0)=1/H-\operatorname{artanh}H$ .
p. 2245: $\Omega_m=1-H^2$ , $\Omega_\Lambda=H^2$ , $q=1-2H^2$ .
Eq. (14): $a=C(e^{\sigma t/2}-1)^{2/3}$ solves the dust era with $\Lambda=\sigma H$ .
Limits of (14): $a\sim C(\sigma/2)^{2/3}t^{2/3}$ as $t\to0^+$ and $H\to\sigma/3$ as $t\to\infty$ .
Eq. (15): $\int_0^\infty\frac{\omega^2\,d\omega}{e^{\omega/(m+H)}-1}=2\zeta(3)(m+H)^3$ .

Significance

The goal is the paper's central claim: under the stated vacuum law the universe has existed for an infinite past, in a quasi-de Sitter phase with $H\approx1$ , and leaves it through a transition in which $H$ and $\Lambda$ fall towards zero, producing radiation. The milestones cover the steps the paper uses to reach it (the vacuum law, the evolution equation and its integration) and the late-time picture (the dust solution and its de Sitter limit, which the paper links to the Eddington–Dirac large-number relation $H\approx m^3$ ).

The results are proved by hand calculation in the paper. The same evolution equation and implicit solution reappear in Carneiro's later paper Cosmological Concordance Model with Particle Creation (2012), whose statements are also on the platform (namespace CarneiroParticleCreation); this mission formalizes the 2006 paper, its vacuum law and its late-time dust solution. Formalizing them produces a verified account of which statements are exact identities and which are approximations. Where the paper writes " $\approx$ ", the milestones state the exact identity or asymptotic equivalence behind it.

Difficulty

The algebraic milestones (5, 7) are routine. The goal concerns a function known only implicitly: the solution is the inverse of $H\mapsto\frac12\big(1/H-\operatorname{artanh}H\big)$ on $(0,1)$ , and its existence on the whole line, its differentiability and its end behaviour all have to be established for an inverse function, not read off a formula. Milestone 6 is a uniqueness statement on all of $\mathbb R$ , so it cannot be checked by substitution. Milestones 1 and 10 are improper integrals whose values involve $\zeta(4)=\pi^4/90$ and $\zeta(3)$ , and they need integrability arguments near $0$ and $\infty$ . Milestones 2, 3, 8 and 9 involve derivatives of complex exponentials, square roots and real powers, where Lean's conventions for $\sqrt{\cdot}$ and $x^{2/3}$ at non-positive arguments must be handled.

Formalization scope

Real numbers throughout; the scalar field is complex-valued, and derivatives are one-variable derivatives in $t$ or $r$ .
In milestones 2–3 the Hubble parameter is a constant and the Laplacian of the radial plane wave is $\partial_r^2$ , which is the paper's approximation.
$\operatorname{artanh}$ is Mathlib's Real.artanh, the real power $x^{2/3}$ is Real.rpow, $\sim$ is Asymptotics.IsEquivalent, and $\zeta(3)$ is written as $\sum_{n\ge0}1/(n+1)^3$ .
Every statement that divides by $\omega$ or $H$ assumes $\omega>0$ or $H(t)\neq0$ . The goal requires the solution on the whole real line and states both limits, so a solution on a half-line or a constant function does not satisfy it.
Approximate steps of the paper that are not exact statements (the identification $b\approx H$ , the radiation law $a\propto t^{1/2}$ quoted from earlier work, and the holographic entropy estimates) are not formalized.

Contributions are welcome on all milestones. The inverse-function and Bose-integral arguments can be reused outside this mission.

Selected references

S. Carneiro, From de Sitter to de Sitter: a non-singular inflationary universe driven by vacuum, Int. J. Mod. Phys. D 15 (2006) 2241–2247. https://doi.org/10.1142/S0218271806009510
S. Weinberg, The cosmological constant problem, Rev. Mod. Phys. 61 (1989) 1–23. https://doi.org/10.1103/RevModPhys.61.1

12 thms2 active usersReviewed

Completed

Algebraic Geometry·Captain: Lucas

Noetherian Schemes: Definition, Basic Properties and Non-examplesTextbook

Motivation

Noetherian schemes are the standard finiteness condition of algebraic geometry. Almost every scheme met in practice is Noetherian: affine and projective varieties over a field, schemes of finite type over $\mathbb Z$ , and many moduli spaces. Many basic theorems about schemes (finiteness of irreducible components, quasi-compactness of morphisms, good behaviour of coherent sheaves and their cohomology) are proved under a Noetherian hypothesis, so the notion appears in the hypotheses of a large part of the literature, starting with Hartshorne's Algebraic Geometry, Chapter II, and the Stacks Project.

This mission formalizes the foundational statements in the Wikipedia article "Noetherian scheme": the definition and its equivalent forms, the basic topological and ring-theoretic consequences, the stability of the notion under morphisms of finite type, and the standard non-examples.

Setting

A scheme $X$ is a locally ringed space that is locally isomorphic to spectra of commutative rings. For an open subset $U \subseteq X$ write $\Gamma(X,U) = \mathcal O_X(U)$ for its ring of sections. An open subset $U$ is an open affine if $U \cong \operatorname{Spec} A$ for a commutative ring $A$ ; then $A \cong \Gamma(X,U)$ .

$X$ is locally Noetherian if every point of $X$ lies in an open affine $U$ with $\Gamma(X,U)$ a Noetherian ring (NoetherianScheme.IsLocallyNoetherianScheme).
$X$ is Noetherian if $X = U_1 \cup \dots \cup U_n$ for finitely many open affines $U_i$ with each $\Gamma(X,U_i)$ Noetherian (NoetherianScheme.IsNoetherianScheme).

A topological space is a Noetherian space if every descending chain of closed subsets stabilizes. A morphism $f : X \to S$ is quasi-compact if preimages of quasi-compact opens are quasi-compact, locally of finite type if it is given locally by finitely generated algebras, and of finite type if it is both.

Formalization targets

Goal

X \text{ Noetherian} \iff X \text{ quasi-compact and } \Gamma(X,U) \text{ Noetherian for every open affine } U \subseteq X.

This combines the article's statements that a scheme is Noetherian iff it is locally Noetherian and compact, and that every open affine of a locally Noetherian scheme has a Noetherian ring of sections. It shows the definition does not depend on the chosen cover.

Milestones

$X$ Noetherian $\iff$ $X$ locally Noetherian and compact.
If $X$ is locally Noetherian and $U \subseteq X$ is any open affine, then $\Gamma(X,U)$ is Noetherian.
$\operatorname{Spec} A$ is Noetherian $\iff$ $A$ is a Noetherian ring.
If $X$ is locally Noetherian, every local ring $\mathcal O_{X,x}$ is Noetherian.
A Noetherian scheme is a Noetherian topological space.
The converse fails: there is a non-Noetherian valuation ring $R$ such that $\operatorname{Spec} R$ is a Noetherian space but not a Noetherian scheme.
A Noetherian scheme has finitely many irreducible components.
Every morphism $X \to S$ with $X$ Noetherian is quasi-compact.
If $f : X \to S$ is locally of finite type and $S$ is locally Noetherian, then $X$ is locally Noetherian.
If $f : X \to S$ is of finite type and $S$ is Noetherian, then $X$ is Noetherian.
The adele ring $\mathbb A_K$ of a number field $K$ is not Noetherian.
The ring of integers of $\mathbb Q(\mu_\infty)$ (all roots of unity adjoined) is not Noetherian and has Krull dimension $1$ .

Significance

The goal is what makes the notion usable: it allows checking Noetherianity on any affine cover and using it on every affine open. Milestones 1–5 and 7–8 are the facts invoked whenever a Noetherian hypothesis is used. Milestones 9–10 are the source of most examples, since they show that every scheme of finite type over a field or over $\mathbb Z$ is Noetherian. Milestones 6, 11 and 12 show the limits of the notion: Noetherianity is not a topological property, and natural rings in number theory (adeles, rings of integers of infinite extensions) fall outside it, even in dimension one.

Mathlib already contains its own versions of several of these facts, phrased through AlgebraicGeometry.IsLocallyNoetherian and AlgebraicGeometry.IsNoetherian, which take "every open affine has Noetherian sections" as the definition. The statements here use the source's cover-based definition, so connecting the two is part of the work.

Difficulty

The central point of the goal is that a cover-based condition must be transferred to an arbitrary open affine $U$ , which in general is not one of the covering opens and is not covered by finitely many standard opens of a single covering affine. The obvious argument (intersect $U$ with the cover) produces opens that are not affine, or are affine in different rings, so a local-to-global argument for the property "Noetherian" on affine opens is needed. The non-examples (milestones 6, 11, 12) each require building or analysing a specific non-Noetherian ring that Mathlib does not yet study from this angle.

Formalization scope

Schemes are Mathlib's AlgebraicGeometry.Scheme in a fixed universe u. Open affines are X.affineOpens; rings of sections are Γ(X, U); local rings are stalks X.presheaf.stalk x.
"Covered by $\operatorname{Spec} A$ with $A$ Noetherian" is encoded as "covered by affine opens whose rings of sections are Noetherian", using $A \cong \Gamma(X,U)$ . The empty scheme is Noetherian.
"Compact" means Mathlib's CompactSpace on the underlying space (quasi-compact, no Hausdorff condition).
Morphisms of finite type are written as LocallyOfFiniteType f together with QuasiCompact f.
The adele ring is Mathlib's NumberField.AdeleRing (𝓞 K) K. The field $\mathbb Q(\mu_\infty)$ is any field $K$ of characteristic zero with IsCyclotomicExtension {n | 0 < n} ℚ K; such fields exist (for example inside an algebraic closure of $\mathbb Q$ ), so the hypothesis is not vacuous.
Milestone 6 is an existence statement in the lowest universe, because not every non-Noetherian valuation ring has a Noetherian spectrum.
A formalization that simply reuses Mathlib's IsNoetherian as the definition would make the goal close to a restatement; the definitions here deliberately follow the source.
Not included: the sections on dévissage, Čech and sheaf cohomology, compatibility of cohomology with colimits, derived direct images, quasi-projective varieties, infinitesimal deformations, the maximal unramified extension example and the infinite polynomial-ring quotient. These need coherent sheaves, sheaf cohomology and derived categories of schemes, which are not yet available in Mathlib in the required form, and several of their formulas are not legible in the supplied copy of the source. They are candidates for follow-up missions.

Selected references

Wikipedia, Noetherian scheme, revision 1372079294. https://en.wikipedia.org/w/index.php?title=Noetherian_scheme&oldid=1372079294
R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977. https://doi.org/10.1007/978-1-4757-3849-0
The Stacks Project, Lemma 28.5.7 (Tag 0BA8), Lemma 28.5.8 (Tag 01P0), Lemma 29.15.6 (Tag 01T6). https://stacks.math.columbia.edu
B. Conrad, Weil and Grothendieck approaches to adelic points. http://math.stanford.edu/~conrad/papers/adelictop.pdf

14 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXVIII: Stochastic Investment Returns and Regular Contribution MomentsTextbook

Motivation

Uncertain financial returns affect funded pensions, DC saving and endowment adequacy. A single investment rate selected once and held fixed for the full projection is fundamentally different from a genuinely independent sequence of annual investment returns. The former produces expected powers of a single random variable while the latter factorises independent annual gross-return moments. These distinctions underpin the financial risk assumptions in stochastic finance models. Existing actuarial missions cover discounted deterministic cashflows but not these stochastic accumulation and contributions.

Setting

Annual gross returns equal one plus their annual net investment returns. A finite probability space has actual scenario masses with total one, so expectation and variance are weighted finite sums. The fixed-rate accumulation raises the same scenario gross factor to the investment horizon. For independent years the model explicitly constructs a product joint mass p(a)q(b) and verifies the first and second product moments. A real pension fund receives a contribution at the beginning of the year before earning its realised gross return.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Finite-scenario investment returns and fixed random rates

A finite discrete fixed-rate model begins at a sure one.

S_n=(1+I)^n,\quad \mathbb{E}[S_n]=\sum_{\omega}p_{\omega}(1+I_{\omega})^n

Independent annual returns on actual product scenarios

Actual joint product probability laws establish two independent annual accumulation moments.

\mathbb{E}[G_1G_2]=\mathbb{E}[G_1]\mathbb{E}[G_2]

Regular contributions and fund first/second-moment recursions

The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.

A_{n+1}=(A_n+c)G_{n+1},\quad m_{n+1}=(m_n+c)\bar G

Capstone theorem

The independent-return pension accumulation recursions reconcile first and second fund moments including contribution cross terms.

A_{n+1}=(A_n+c)G_{n+1},\quad m_{n+1}=(m_n+c)\bar G

Significance

As discussed in Shreve's stochastic-finance treatment, The capstones distinguish random fixed returns from actually independent annual returns without presupposing a target identity. For the latter, the true two-year joint probability law factorises the expected growth and its second moment. Under subsequent iid moment factorisation, a multi-year first and second return moment model yields an exact variance recursion. The fund valuation then derives consistent one-step mean, second-moment and variance formulae with contributions, including the cross-term from previously accumulated assets. The model is useful for genuine stochastic saving, actuarial adequacy and projected pension risk.

Difficulty

It is mathematically false in general that expected compound returns equal the power of the expected rate for a fixed but random interest assumption. Genuine product probability weights, not a definition of independence as the desired conclusion, support the two-year factorisation. For a regular savings fund, the contribution is invested with the previous fund, so the second moment includes a cross term twice the contribution times the prior expected fund. The variance has to be derived from the two independently defined moments with positive gross-return second-moment bounds. All signs and independence restrictions should be preserved at every step.

Formalization scope

Fixed stochastic-rate model and independent annual returns are distinct mathematical constructs in this model. A future substantial probability model could construct fully independent n-year return families and an exact savings accumulation probability distribution, rather than stopping at the two-year product law. The present source has nontrivial results because it independently calculates both moments of an actual joint scenario distribution and reconciles the cross terms in the savings fund variance. Existing stochastic insurance claims calculations alone do not provide an investment growth scenario model. This finite product model and fund recursion are reusable for defined contribution pensions, insurance asset adequacy testing and later cashflow simulations.

For a random interest rate sampled once at issue and held fixed, the expected n-year accumulation is an expectation of a random power, not generally a power of the expected return. If annual investment returns instead vary independently, the gross growth factors are multiplied across years and their expected product factorises. This mission proves the two-year factorisation from genuine independent finite product-state probability masses, without taking independence to mean the target moment identity by definition. For regular savings, contribution timing matters because a beginning-of-period contribution earns that period's return. The second-moment recursion must therefore contain the mixed term twice the contribution times the previous expected fund. These identities provide an actuarial basis for testing pension fund accumulation and capital adequacy, but do not justify a normal or lognormal fund distribution merely from calculated means and variances.

The principal independence derivation is from an actual finite two-year product scenario model, while the general n-year variance is stated as an explicit algebraic moment-factorisation law. Deriving n-way stochastic independence under a full probability measure, lognormal approximate fund distribution and path-dependent contributions remains work for subsequent substantial probability theory. No normal approximation or lognormality is assumed from mean and variance alone. These open theorem targets are not accepted proofs.

These are original derived finite/analytic Actuarial 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.

Selected references

S. E. Shreve (2004), Stochastic Calculus for Finance I: The Binomial Asset Pricing Model, Springer. https://link.springer.com/book/10.1007/978-0-387-22527-2
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Wiley, accumulation and stochastic investment model chapters. https://www.wiley.com/en-us/Fundamentals+of+Actuarial+Mathematics%2C+3rd+Edition-p-9781118782521

53 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics XCII: Unit-Linked Fund Charges, Non-Unit Cashflows and Profit TestingTextbook

Motivation

Unit-linked life and pension policies require careful accounting for where gross premiums go, which underlying fund units are purchased and which charges are received by the insurer. The FCA's unit-linked review identifies allocation, management, surrender and other policy charges as distinct insurer cashflows. Earlier actuarial missions XLVI and LXIX already formalise simple unit funds and guarantees, but lack explicit offer/bid unit pricing and a fully reconciled insurer non-unit profit signature.

Setting

A policyholder pays a gross premium, of which an allocation percentage is invested at the offer price and the remainder is retained by the insurer. Unit-holders value their existing holdings using the bid price. Management and fixed administration charges reduce fund assets; a guaranteed minimum death benefit creates an insurer mortality risk above the unit-linked fund. The insurer's non-unit account collects charges and premium differences and separately pays expenses, commissions and mortality guarantee strain.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Premium allocation, bid and offer prices and fund charges

Cancelling no more units than held retains a nonnegative unit account.

U_t=U_{t-1}+\frac{a_t P_t}{O_t}-\frac{C_t}{B_t}

Risk guarantees, surrender payments and reserve strain

A nonnegative surrender charge cannot increase the positive fund value.

B_t^{\text{death}}=\max(F_t,G_t),\quad R_t=(G_t-F_t)^+

Non-unit profit signatures and discounted insurer margins

Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.

\Pi=\sum_t v^t p_t\left(\text{income}_t-\text{outgo}_t\right)

Capstone theorem

Actual unit premium allocation and bid-offer cost reconcile with the insurer's separate death guarantee obligations and complete non-unit cashflow profit account.

\Pi=\sum_t v^t p_t\left(\text{income}_t-\text{outgo}_t\right)

Significance

As discussed in the FCA's unit-linked review, The target reconciles every gross premium unit purchase and retained amount; it values immediate bid-offer spread costs, decomposes guaranteed death benefits into the invested fund plus net insurer amount at risk, and establishes an independent non-unit profit cashflow balance. Additional supporting theorems make the risk discount present value additive across the profit signature, with correct timing of beginning-year premium allocations and end-year fund costs. This provides an exact starting point for insurance policy profit testing and the analysis of charge sensitivity.

Difficulty

Bid and offer prices cannot be interchanged: a unit bought at offer is valued at bid and a positive spread produces a real cost even with unchanged market prices. A premium allocation percentage is not identical to the percentage of bid value created. Death insurance cost is the excess guaranteed benefit above the fund, rather than the total benefit, because fund assets already cover the remainder. The non-unit income and the actual expenses/commission/insurance risk must be kept separate rather than silently netted inside fund performance. The proof must impose suitable positivity on offer prices and fund values.

Formalization scope

Bid-offer spread and non-unit profit signature are distinct mathematical constructs in this model. A future extension will include surrender probabilities, partial withdrawal, guaranteed annuity options and stochastic policyholder behaviour, together with a non-unit reserve liability under the prospective profit-testing basis. The current identities are nontrivial because they distinguish bid-valued units bought at an offer price, actual management charges, underlying expenses and the top-up death cost. Existing unit account and zeroisation missions do not include all these separate components in one coherent insurer profit signature. The explicit fund and charge functions are reusable for product pricing sensitivities, reserve testing and financial reporting.

Insurance premiums credited to unit-linked funds are converted into units at the offer price, but the policyholder's fund is valued using the bid price. A positive spread therefore creates an immediate difference even when financial markets have not moved. Management fees and policy administration charges reduce the unit fund, whereas amounts charged to policyholders generate insurer non-unit income and are not synonymous with the actual expenses incurred. A guaranteed death benefit creates mortality cost only on the positive excess above the linked fund value; it would double-count fund assets to charge the full guaranteed amount as non-unit insurer cost. The non-unit profit signature then recognises unallocated premiums, spreads and management and administration charges less commission, expenses, additional death cover and any guarantee cost. Future cashflows are discounted year by year. These identities form a precise accounting model, not a regulatory determination of fair consumer value.

The mission develops one-period unit accounting and finite annual expected profit signatures. It is not a market conduct or compliance assessment of a particular insurer. Fund return and projected mortality are explicit model inputs and do not assert a complete stochastic-policy profit distribution. Complex paid-up terms, partial surrender and non-unit reserve zeroisation have related earlier mission infrastructure and require further integration. Every Lean theorem remains open.

These are original derived finite/analytic Actuarial 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.

Selected references

Financial Conduct Authority (2026), Unit-linked pensions and savings: price and value practices. https://www.fca.org.uk/publications/multi-firm-reviews/unit-linked-pensions-and-savings-multi-firm-review-consumer-duty-price-and-value-practices
Financial Conduct Authority (2016), Fair treatment of long-standing customers in the life insurance sector, TR16/2. https://www.fca.org.uk/your-fca/documents/thematic-reviews/tr16-02

53 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXVII: Inflation-Adjusted Claim Triangles and Average Cost ReservingTextbook

Motivation

General-insurance reserving methods must distinguish development of claim payments from changes in their price level. The IFoA inflation reserving guidance distinguishes implicit and explicit inflation adjustments. Its earlier claims reserving report identifies inflation and average cost per claim methods alongside standard chain ladder. Earlier actuarial missions LIII and LIX cover volume chain ladder and reserve variances but not these two methods.

Setting

Incremental claims are paid in calendar years determined by accident year plus development year. A strictly positive index converts nominal claims into a constant valuation-year price level before applying development factors. The projected real future claim payment is then reinflated to its expected future calendar-year cost. Separately, an average cost per claim development triangle and a count triangle project ultimate claim frequency and mean severity.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Inflation indices and real-claims transformations

A price index remains positive for growth greater than minus one.

C^{\text{real}}_{i,j}=C_{i,j}\frac{I_{\text{base}}}{I_{i+j}}

Incremental triangles and cumulative development

Sufficient projected ultimate value gives nonnegative outstanding reserve.

C_{i,j}=\sum_{k=0}^{j}X_{i,k},\quad U_i=C_{i,j}f_j

Average-cost-per-claim projection and reserve reconciliation

The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.

U_i=N_i^{\text{ult}}A_i^{\text{ult}},\quad R_i=U_i-P_i

Capstone theorem

The inflation-adjusted chain-ladder projection and the independently developed average-cost claim reserve both reconcile nominal cashflows, real development and ultimate claims without treating the projection as an observed fact.

U_i=N_i^{\text{ult}}A_i^{\text{ult}},\quad R_i=U_i-P_i

Significance

As discussed in the IFoA claims-reserving literature, The target establishes exact no-loss conversion between nominal and real claims, proper telescoping between incremental and cumulative triangles, the composition of real development factors, and the multiplication of projected ultimate claim numbers by projected average severity. It then reconciles both ultimate and outstanding amounts in an independent combined capstone. A payment-year inflation assumption is distinguishable from a development-year link factor, which guards against projecting historical calendar-year inflation twice.

Difficulty

The proof must preserve accident-year, development-year and calendar-year indexing and impose positivity on every ratio's index, claim count and growth denominator before invoking any reconstruction identity. The dollar value of a claim that has already been paid must never be reinflated as if it were a future payment. Volume development and average-cost development use different denominators and cannot be conflated in a single grossing-up factor without an additional model assumption. The capstone reconciles separately constructed projections rather than defining reserves by the desired equality.

Formalization scope

Historical inflation adjustment and claim-development factors are distinct mathematical constructs in this model. A future extension could integrate stochastic calendar-year inflation factors, accident-year trends, and parameter-estimation uncertainty into a single insurer liability distribution. The current exact algebraic target is nontrivial because it reconstructs nominal cashflows after applying conversion and development operations to independently constructed real and count-based projections. Known chain-ladder methods do not eliminate the need to prove that the resulting factors and projected reserve components reconcile. The finite triangle definitions and their transformations are reusable for other claims reserving methods, including tail development and multiple accident years.

A loss development triangle involves three separate notions of time: accident-year origin, settlement development lag and payment calendar year. Past inflation must be removed according to the actual payment year before development is extrapolated. Only after the real-valued development has been projected should future expected payment-year inflation be reinstated, and only once. A claim volume development factor does not represent a price inflation rate. The average-cost-per-claim method separately projects ultimate claim numbers and average claim sizes, then multiplies them. This decomposition distinguishes frequency development from claim inflation and severity development. The actuarial motivation is substantial, as long-tailed insured losses can have irregular calendar-year price patterns. The mathematical statements in this source are exact projection identities, not claims that past development patterns predict future claim payments without residual risk.

This is a mathematically exact deterministic claims triangle and projected cashflow formalisation, not a claim that chain-ladder assumptions hold for a particular line of business or that the selected inflation index is statistically correct. The index rate and link factors are model inputs, and the full stochastic process/reserve estimation error remains covered only in related Mack mission LIX. Interactions of separate inflation by payment type and stochastic calendar effects are future research problems. All Lean theorem bodies are open.

These are original derived finite/analytic Actuarial 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.

Selected references

Institute and Faculty of Actuaries (2025), High-level Methods for Incorporating Changing Inflation into Claims Reserve Estimates. https://vle.actuaries.org.uk/pluginfile.php/168696/mod_resource/content/1/Reserving%20During%20Volatile%20Inflation%20v1.9.pdf
Institute and Faculty of Actuaries (2004), Claims reserving, §5. https://www.actuaries.org.uk/system/files/documents/pdf/0353-0413.pdf

49 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXI: Stochastic First-Passage Ruin and Stopped Exponential BoundsTextbook

Motivation

The Cramér–Lundberg model describes insurer capital invested in premium revenue while discrete random claims are paid at unpredictable arrival times. The model's classical adjustment coefficient and ruin probability are treated in risk theory and in modern ruin-probability bounds. Earlier mission LXXVIII derives a candidate ruin formula satisfying a renewal equation, but does not model the actual first-passage event. This mission supplies genuine stochastic first passage and measurable ruin events with an explicit stopped exponential-moment route to a rigorous bound.

Setting

Let W_j and Y_j be random waiting times and severities on a measurable probability space. At n-th claim arrival, cumulative elapsed time is the sum of W_0 through W_{n−1}, aggregate paid claims are the corresponding sum of Y_j, and the surplus is initial capital plus premium rate c times elapsed time minus claims. Ruin means surplus strictly less than zero and is only tested at claim boundaries, where a positive continuous premium slope allows a crossing to occur. The first-hit event excludes every earlier ruin, and its union over n is ultimate ruin.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Embedded Poisson-arrival capital paths and first-passage partition

Larger capital cannot create pathwise ruin.

U_n=u+c\sum_{j<n}W_j-\sum_{j<n}Y_j

Probability of ruin, monotonicity and severity overshoot

Observation of more arrivals can only increase probability of ruin.

\psi_N(u)=\mathbb{P}(\min_{n\le N}U_n<0)

Stopped exponential-loss process and conditional Lundberg capital bound

The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.

\mathbb{E}[M_{\tau\wedge N}]\le1\ \Longrightarrow\ \psi_N(u)\le e^{-Ru}

Capstone theorem

The actual stochastic first-passage event and stopped exponential moment condition derive a nonvacuous ultimate Lundberg capital bound.

\mathbb{E}[M_{\tau\wedge N}]\le1\ \Longrightarrow\ \psi_N(u)\le e^{-Ru}

Significance

The mission establishes a real measured probability of ultimate ruin, monotonicity under capital and arrival horizon, and a disjoint partition by the first claim causing ruin. It then uses a stopped exponential loss process and an explicit moment upper bound to derive a Lundberg inequality for finite and ultimate ruin probabilities. The auxiliary stopped expectation condition is an independent martingale-style hypothesis, not an assumption of the desired probability bound. This helps distinguish authentic probability claims from an explicit exponential candidate whose equation has been verified. The risk-theory literature motivates the exponential-capital tail.

Difficulty

Nontrivial probability analysis is required to link a finite first-passage indicator to a stopped exponential transform. The first-hit sum cannot count multiple ruin dates on the same path, and the no-ruin terminal term must appear exactly once. Strict ruin, equality at zero and an observed negative surplus require distinct treatment. The finite-horizon inequality then uses measurability, positivity of exponential loss and a moment expectation hypothesis. Passing to ultimate ruin requires the countable union of nested ruin events and probability measure continuity, without assuming the theorem's conclusion.

Formalization scope

Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.

The pathwise event uses a strict negative surplus, not failure on equality at zero. The first-passage index is a disjoint union of finite-arrival failure events, and the increasing union gives ultimate ruin. A conditional moment hypothesis provides a nontrivial route to an exponential capital inequality. It is not the same assertion as the inequality on the ultimate ruin probability. The model does not claim to establish the Poisson arrival distribution or full independence of exponential severities from this conditional input. Those must be proved in a later, more elaborate stochastic source model.

The capstone proves the conditional stopped-moment Lundberg inequality for an actual measurable first-passage event, not yet the complete exponential-claims distributional identification. Independent exponential waiting times and independent claim severities supply the classical route to the stopped moment hypothesis but are not themselves constructed or verified in this graph. A future mission should derive that moment condition from fully specified iid waiting and severity distributions and prove uniqueness of the exact ruin probability. The pathwise framework is reusable for continuous-time embedding, overshoot losses, first-passage service tables and capital assessment. All Lean proof obligations remain open.

These are original derived finite/analytic Actuarial 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.

Selected references

S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 23. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
Hanspeter Schmidli (2017), Risk Theory, first edition, Springer. https://link.springer.com/book/10.1007/978-3-319-72005-0
Bounds for the Ruin Probability in the Sparre–Andersen Model (2024), Risks 12(2), 28. https://www.mdpi.com/2227-9091/12/2/28

58 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXIX: Time-Varying Competing Exits and Multi-State Thiele ReservesTextbook

Motivation

Continuous-time multi-state life insurance uses a generator of competing decrement intensities and prospective reserves for status-dependent benefits. The time-dependent state equations appear in multi-state insurance research; Promislow (2015), Chapter 19, provides actuarial fundamentals. The existing LXXVI mission constructs general conservative generator rows but only solves the stationary alive/dead reserve. This mission adds time-varying competing risks and derives a genuine contingent-payment reserve from its cashflows.

Setting

Three mutually exclusive states consist of active insurance, termination by cause one and termination by cause two. The latter are absorbing. The common exit intensity is a nonstationary force λ(t)=a+bt with cumulative hazard H(t)=at+bt²/2. A fixed proportion p of the exit force belongs to the first cause; 1−p belongs to the second. Nonnegative a, b and future dates and p in the unit interval make the transition probabilities stochastic. The model admits two distinct termination payments, one for each cause, and a separately specified maturity endowment.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Nonstationary intensity, exact absorption and generator conservation

Generator no-exit diagonal is minus total force.

\lambda(t)=a+bt,\quad H(t)=at+\frac{bt^2}{2}

Three-state transition probabilities and Chapman–Kolmogorov

Forward cause-two flow equals complementary hazard share times active membership.

P_{00}(s,t)=e^{-(H(t)-H(s))},\quad P_{01}(s,t)=p(1-P_{00}(s,t))

Cause-contingent insurance and integral Thiele reserves

A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.

V'(t)=(\delta+\lambda(t))V(t)-\lambda(t)\bigl(pB_1+(1-p)B_2\bigr)

Capstone theorem

A genuinely nonstationary three-state absorbing model conserves probability and its independently integral-defined prospective liability obeys the cause-contingent Thiele equation.

V'(t)=(\delta+\lambda(t))V(t)-\lambda(t)\bigl(pB_1+(1-p)B_2\bigr)

Significance

The prospective reserve is an independently defined sum of a terminal-survival present value and a bona fide interval integral of the time-discounted, competing-exit claim intensity. The capstone proves its terminal boundary and differentiates it to obtain a nonstationary, three-status Thiele ODE, with an explicit cause-mix death strain. The result includes complete Chapman–Kolmogorov composition and transition normalisation for two absorbing exits. Research on multi-state actuarial equations explains how these equations fit into the broader general reserve framework.

Difficulty

The proof must establish a nontrivial inhomogeneous probability structure, not simply define reserve cashflows by the desired ODE. The cumulative-force derivative must be combined with the exponential survival chain rule, and the transition matrix must be composed across different calendar intervals. The integral of discounted cause-specific benefits must then be differentiated with a moving lower endpoint and a valuation-date-dependent exponential factor. Several steps rely on genuine interval integral differentiation and the finite-timestamp boundary conventions; no closed-form fixed-intensity substitution is assumed.

Formalization scope

The model imposes fixed cause allocation while the total force changes with time. It therefore admits a genuine conditional transition matrix with two absorbing states. This provides a nonstationary counterexample to treating all transition intensities as constant; forcing an arbitrary time-dependent kernel to satisfy the desired generator equation by assumption would be vacuous. The interval-integral benefit value is independently defined before differentiating it. Its terminal boundary depends on the maturity payment, and no death benefit is payable at maturity beyond the contractual endpoint. The formalisation does not assume a general matrix-exponential formula for time-dependent noncommuting generators.

The mission establishes a nonstationary three-state absorbing competing-decrement model, not an arbitrary intercommunicating time-dependent finite-state generator or a semi-Markov duration-reset model. This restriction is important because its exact transition matrix and reserve integrals can be constructed without assuming the answer. Later actuarial missions can reuse the resulting conditional survivor functions and Thiele equation as a basis for disability recovery and wider inter-state transfers. Lean statements are open research targets, not accepted formal proofs, and the mathematical identity must be obtained from the originally defined valuation.

These are original derived finite/analytic Actuarial 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.

Selected references

S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 19. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml
Multi-state modeling in the mathematics of life insurance: meditations and applications (2020), research thesis, pp. 17–35. https://www.math.ku.dk/bibliotek/arkivet/phd-theses/phd20cf.pdf
Kristian Buchardt, Thomas Møller and Kristian Bjerre Schmidt (2015), Cash flows and policyholder behaviour in the semi-Markov life insurance setup. https://doi.org/10.1080/03461238.2013.879919

59 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXIII: Cox Survival Regression and Censored Risk-Set LikelihoodsTextbook

Motivation

Actual insurer mortality and withdrawal observations are censored and may differ systematically with explanatory covariates. Cox's original 1972 proportional-hazards paper treats an arbitrary baseline hazard combined with covariate-relative-risk multipliers and constructs a conditional partial likelihood. Existing actuarial missions cover lifetimes, Kaplan–Meier/Greenwood and mortality graduation, but not regression risk-set estimation.

Setting

A life with scalar covariate z and regression parameter beta has hazard λ0(t) exp(beta z). The cumulative baseline hazard determines the survival function. At each distinct observed failure time there is a finite nonempty at-risk set, including the life that died, and censoring removes deaths that are not observed without treating them as failures. This mission assumes no tied failures in its conditional likelihood graph; more general Efron and Breslow ties require a separate coherent treatment.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Positive proportional hazards and cumulative survival

A zero covariate reduces to baseline survival.

\lambda(t\mid z)=\lambda_0(t)e^{\beta z},\quad S(t\mid z)=e^{-\Lambda_0(t)e^{\beta z}}

Censored risk sets and event conditional likelihood

A censored observation must not simultaneously be a failure contribution.

L(\beta)=\prod_{i\in D}\frac{e^{\beta z_i}}{\sum_{j\in R(t_i)}e^{\beta z_j}}

Log-partial likelihood, weighted risk scores and inference

Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.

U(\beta)=\sum_{i\in D}\left(z_i-\frac{\sum_{j\in R_i}z_je^{\beta z_j}}{\sum_{j\in R_i}e^{\beta z_j}}\right)

Capstone theorem

Cox covariates alter baseline hazard multiplicatively, survival stays within probability bounds, and the nontrivial risk-set score is derived as the derivative of the conditional partial likelihood.

U(\beta)=\sum_{i\in D}\left(z_i-\frac{\sum_{j\in R_i}z_je^{\beta z_j}}{\sum_{j\in R_i}e^{\beta z_j}}\right)

Significance

The mission formally separates a common arbitrary baseline hazard from the relative hazard of each observed insured life. The partial likelihood uses event-specific risk sets, not a single fixed cohort denominator, and the model derives the true conditional event probabilities and analytic score from the independently defined likelihood. As in the original Cox model, the mathematical outcome provides essential foundations for credible, covariate-sensitive life contingent predictions and statistical mortality investigations.

Difficulty

The risk sets must remain nonempty and include observed failures when interpreting their shares as probabilities. Finite products with changing risk sets combine with a log-likelihood that is differentiated using an exponential weighted denominator. The central theorem must obtain the score from a derivative and must not define score equality as a model axiom. Positive covariate multipliers and boundary survival values are derived separately. The model does not assert a numerical maximum likelihood estimator exists without concavity or identifiability conditions.

Formalization scope

The conditional partial likelihood is based on one observed failure at a time. Each event has its own finite risk set. A life censored before the event time is excluded from that later set, but an individual censored after the time remains exposed at that instant. Censoring patterns therefore change the risk sets, even though the baseline force drops out of the conditional event ratio. With a scalar coefficient, this model is an actuarially meaningful specialisation of the Cox regression formulation. The score derivative is substantive because its risk-weighted average contains the current coefficient in both the numerator and denominator. The numerator and denominator must each be differentiated, the denominator must remain strictly positive and the log derivative must not assume the target identity. Only after these facts have been proved can the formula for the score be justified. Extending the analysis to a score vector and information matrix would involve covariance matrices weighted by dynamic risk sets, and the nonnegativity of observed information is not a pointwise algebraic identity without proper hypotheses. Reusable consequences of this foundation include estimation with life-assurance underwriting covariates, statistical investigation of pensioner mortality, cause-specific decrements and a later treatment of time-dependent covariates. This graph deliberately treats distinct failure times rather than asserting a tied-events formula that has not yet been formally justified; Efron and Breslow corrections motivate future work, not assumptions of the current model.

The model treats a single scalar covariate and untied observed failures. It neither assumes a parametric distribution for the baseline mortality force nor confuses censored lives with observed deaths. It does not prove martingale asymptotics, proportional-hazard diagnostics, time-varying regression coefficients or Efron tied-event corrections. These are legitimate larger follow-on missions. Its theorem statements and source are unproved formal targets.

These are original derived finite/analytic Actuarial 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.

Selected references

D. R. Cox (1972), Regression Models and Life-Tables, JRSS Series B 34, 187–202. https://doi.org/10.1111/j.2517-6161.1972.tb00899.x
D. R. Cox (1975), Partial Likelihood, Biometrika 62, 269–276. https://doi.org/10.1093/biomet/62.2.269

50 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXX: Infinite Compound Frequencies and Corrected Panjer RecursionsTextbook

Motivation

Panjer recursions allow compound claim distributions to be computed without enumerating many severity convolutions. The original Panjer paper and the Sundt–Jewell family extension establish the actuarial context. The previous LXXVII mission covers finite-support frequency distributions with zero claim amounts. Here the claim count ranges over all nonnegative integers, so correct series convergence and coefficient interchange become new formal obligations.

Setting

Let N be Poisson with claim count intensity λ≥0 or geometric with parameter q in [0,1). Independently distributed claim severities are nonnegative integer valued, with pmf f_j and possibly f_0>0. For each claim count n, the distribution f^{*n} is formed using genuine convolution; the empty portfolio assigns mass one to zero. The compound mass g_k is defined as the infinite sum of p_n times the n-fold convolution coefficient, independently of any Panjer formula.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Countably infinite count laws and convolution powers

True infinite aggregate mass is nonnegative.

p_n^{\mathrm{Poi}}=e^{-\lambda}\frac{\lambda^n}{n!}

Probability generating functions, mass normalisation and zero atoms

Compound Poisson zero mass comes from thinning.

g_k=\sum_{n=0}^{\infty}p_n(f^{*n})_k,\quad g_0=G_N(f_0)

Full Poisson and geometric infinite Panjer recurrence

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}

Capstone theorem

The genuinely infinite Poisson and geometric aggregates obey their independently derived corrected Panjer laws.

(1-qf_0)g_k=q\sum_{j=1}^kf_jg_{k-j}

Significance

The capstone derives both infinite frequency families' entire positive-aggregate recurrence. For Poisson frequency the kernel includes a severity-size factor λj/k; for geometric frequency it contains an essential zero-claim correction 1−qf_0. The zero aggregate mass itself is the count PGF evaluated at severity f_0, not merely the probability of having no claims. The 1981 ASTIN literature underpins these equations, while a countably supported Lean formalisation makes their analytic conditions explicit.

Difficulty

Unlike the finite claim count in LXXVII, an infinite frequency model requires genuine convergence before double series may be rearranged. Proving the Poisson and geometric frequency normalisations is distinct from proving convergence of the actual aggregate pmf. At a fixed amount k a finite inner convolution remains, but summation over the count n is infinite. The nontrivial step is justifying probability-generating function composition and extracting the correct severity coefficients without assuming the desired recurrence or silently truncating Poisson claims. Special cases with all claim sizes zero are included.

Formalization scope

Existing actuarial theory establishes the analytical principle, whereas the formal work here must prove the stated identities in Lean using the true distribution and event definitions. Some prior mission targets describe finite distributions or a candidate valuation, but they do not establish these stronger infinite-support or measured first-passage results. The boundary assumptions are part of each mathematical statement and cannot be replaced by a tautological definition. A complete proof requires independent source lemmas, explicit handling of the limiting case and verification of every transformation before concluding the capstone.

The generating-function series is defined from the probability mass of each count; the count law is genuinely infinite, not a finite upper cutoff with a hidden tail. In particular, the positive Panjer recursion cannot be used to define its own aggregate coefficients: the aggregate mass must first be constructed from convolution powers and the count weights. At claim size zero, the event of positive frequency with all zero-valued claims contributes to the true aggregate zero probability. Geometric count and Poisson count require distinct coefficient functions, even though they share the same actuarial notation for the severity distribution.

This mission addresses actual infinite Poisson and geometric count laws, with arbitrary properly normalised discrete severities. It does not cover noninteger-shape negative-binomial frequency, complex-domain analytic continuation or continuous claim sizes. The formal target makes probability nonnegativity and summed severity mass explicit, and all Lean proofs remain open. The resulting count/compound transforms can be reused in later collective-risk, stop-loss and capital modelling applications. It deliberately excludes vacuous proof strategies that define the aggregate distribution as the recurrence answer.

These are original derived finite/analytic Actuarial 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.

Selected references

Harry H. Panjer (1981), Recursive Evaluation of a Family of Compound Distributions, ASTIN Bulletin 12(1), pp. 22–26. https://doi.org/10.1017/S0515036100006796
Bjørn Sundt and William S. Jewell (1981), Further Results on Recursive Evaluation of Compound Distributions, ASTIN Bulletin 12(1), pp. 27–39. https://doi.org/10.1017/S0515036100006802
S. David Promislow (2015), Fundamentals of Actuarial Mathematics, Chapter 21. https://www.oreilly.com/library/view/fundamentals-of-actuarial/9781118782521/ftoc.xhtml

58 thms2 active usersReviewed

Completed

Actuarial Science Probability·Captain: WillR

Actuarial Mathematics LXXXV: Insurance GLM Pricing, Likelihood Scores and DevianceTextbook

Motivation

Actuarial claim counts and average costs depend on policy exposure, customer characteristics and risk-factor selection. The foundational Nelder–Wedderburn GLM formulation derives exponential-family maximum likelihood through a predictor and link, including Poisson count and Gamma response examples. Existing actuarial missions cover finite exposures and rating relativities, but not a unified log-likelihood score, information and deviance calculation.

Setting

An exposed group contributes E positive insured person-years. The count predictor η produces expected claims μ=E exp η, so log exposure is a compulsory offset rather than a fitted regression coefficient. The model defines observed claims per exposure, the Poisson log-likelihood up to a response-only factorial constant, its scalar score, expected information and saturated deviance. A separate Gamma mean and variance model describes positive insurance severity.

Formalization targets

The formalisation develops a connected set of actuarial identities, beginning with precise model definitions and ending with the prospective valuation result.

Positive claim rates, log links and exposure offsets

Nonnegative frequency and severity produce nonnegative pure premium.

\mu=E e^\eta,\quad \log \mu=\log E+\eta

Poisson log-likelihood, score and information

Poisson log-likelihood attains a global maximum at the fitted canonical count for strictly positive observations.

\ell(\eta)=y\log(Ee^\eta)-Ee^\eta,\quad U(\eta)=y-Ee^\eta

Claims deviance, premium relativity and model comparison

A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.

D_{\text{Poi}}=2\left[y\log\left(\frac{y}{\mu}\right)-(y-\mu)\right]

Capstone theorem

A genuine positive-exposure Poisson GLM has the correct canonical offset, score and Fisher derivative, nonnegative saturated deviance and consistent severity-loaded insurance premium.

D_{\text{Poi}}=2\left[y\log\left(\frac{y}{\mu}\right)-(y-\mu)\right]

Significance

Following Nelder–Wedderburn, the capstone derives the Poisson model's canonical offset, identifies the score as a genuine derivative of the log-likelihood, and proves that its derivative is negative Fisher information. A nonnegative deviance measures disagreement with saturated data and integrates with multiplication of expected frequency and severity to obtain the insurer's pure premium. This is the mathematical basis for estimating tariff frequency relativities and verifying model fit.

Difficulty

A real-valued logarithm is not automatically the log of a positive expected count: exposure positivity must be explicit. Count zero is handled with a separate non-log-deviance expression, avoiding undefined logarithmic ratios. The score and information identities must follow by differentiation rather than by an assumed GLM normal equation. It is a nontrivial analytic task: a vacuous definition of a zero score would not establish any likelihood derivative. The deviance inequality uses the logarithmic convexity inequality and requires positive expected and observed claims, while the finite exposure boundary avoids any mistaken claim of an informative zero-exposure observation.

Formalization scope

The Poisson GLM score is the derivative of a log-likelihood rather than an arbitrary residual statistic. The exposure offset shifts the logarithm of expected claim counts, so changing exposed policy-years modifies the fitted expected count without changing the per-exposure class rate. This is a defining issue in insurance rating where two policyholders with the same expected annual frequency can have different months insured. The score derivative gives the negative Fisher information, leading to the familiar concavity of the scalar canonical log-likelihood under positive exposures. Identifying a maximum-likelihood estimate, however, also requires adequate observed data and a nondegenerate model: at zero observed claims, the MLE can be approached only as the predicted rate tends to zero, not necessarily at a finite linear predictor. The scaled deviance measures disagreement with saturated data; it is nonnegative by the logarithmic inequality when observed and fitted counts are strictly positive. The zero-count case has to be handled by a limiting convention outside the positive-count formula. This is actuarially material in sparse claim classes and high-frequency policy segments. Gamma severity uses a different conditional variance function, so its dispersion and positivity conditions are not inherited directly from the Poisson count model. This graph is a reusable foundation for multivariate tariff construction, fitted pure premiums, exposure offsets and later iterative weighted regression algorithms. Its source model follows Nelder and Wedderburn while making every claim-count positivity hypothesis explicit.

This is the scalar Poisson frequency and Gamma severity foundation, not a full numerical fitting algorithm or a general matrix-valued IRLS solver. The categorical design matrix, multivariate coefficient normal equations, dispersion estimation, residual-based diagnostics and parameter-inference asymptotics are reserved for follow-on missions. There is no assertion that positive claims always exist or that every rate model is identifiable. All Lean proof statements remain open.

These are original derived finite/analytic Actuarial 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.

Selected references

J. A. Nelder and R. W. M. Wedderburn (1972), Generalized Linear Models, JRSS A 135(3), 370–384. https://doi.org/10.2307/2344614
Casualty Actuarial Society, Generalized Linear Models for Insurance Rating, https://www.casact.org/sites/default/files/2021-03/05-Goldburd-Khare-Tevet.pdf

54 thms2 active usersReviewed

All missions

Garrett Functional Analysis Notes I: Completeness and Quasi-completenessTextbook

Motivation

Setting

Formalization targets

Goal: quasi-completeness of operator spaces (Theorem 4.1.1)

Supporting results (the milestones, in the order of the notes)

Significance

Difficulty

Formalization scope

Selected references

Invariant Subspace ProblemOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal: the invariant subspace problem

Milestones (known results)

Significance

Difficulty

Formalization scope

Selected references

Euler Systems (Wikipedia): Relations of the Cyclotomic Euler SystemTextbook

Motivation

Setting

Formalization targets

Goal: the cyclotomic Euler system relations

Milestones

Significance

Difficulty

Formalization scope

Selected references

Rural Hospitals Theorem (Wikipedia): All Stable Matchings Fill the Same PositionsTextbook

Motivation

Setting

Formalization targets

Goal: the rural hospitals theorem

Milestones

Significance

Difficulty

Formalization scope

Selected references

Stable Matching Problem (Wikipedia) I: The Gale–Shapley AlgorithmTextbook

Motivation

Setting

Formalization targets

Goal: the algorithm produces a stable matching

Milestones

Significance

Difficulty

Formalization scope

Selected references

Secretary Problem: the 37% RuleTextbook

Motivation

Setting

Formalization targets

Goal: the 37% rule

Milestones (following the article's derivation)

Significance

Difficulty

Formalization scope

Selected references

Smale's question: the homotopy type of Diff(S⁴)Open Problem

Motivation

Setting

Formalization targets

Goal: connectivity of Diff(D4)\mathrm{Diff}(D^4)Diff(D4)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Slice–ribbon conjectureOpen Problem

Motivation

Timeline

Setting

Formalization targets

Goal: slice implies ribbon

Milestones

Significance

Goal: connectivity of $\mathrm{Diff}(D^4)$

Goal: the $C^r$ stability conjecture

Goal: the $C^r$ closing lemma