Topology

Our goal

This project aims to formalize the Poincaré conjecture in Lean, following the approach in Kleiner and Lott's Notes on Perelman's Papers.

Important references

Poincare-Conjecture and DifferentialGeometry are important references for this project, providing existing work on proof planning and foundations in differential geometry. We thank the authors and contributors of both projects. We will build on their work while preserving credit and citing our sources.

OpenGA's role

OpenGA focuses on manual review, curation and reuse: checking existing code, adapting it to the required versions, and organizing reusable definitions and theorems in the library.

The PoincareConjecture directory is used to prepare submissions to Prove2Me and keep a local copy of the platform's code and progress through ongoing synchronization. Results completed on the platform will also be reviewed and incorporated into OpenGA for use in future work in geometric analysis.

We thank the Prove2Me team for running the platform and exploring collaboration between humans and AI in mathematical formalization. We are honored to take part.

The set

For a complex parameter $c$, iterate the quadratic map

$$f_c(z) = z^2 + c$$

starting at the critical point $z = 0$. The Mandelbrot set is the set of parameters for which this orbit stays bounded:

$$M = \{\, c \in \mathbb{C} \ : \ \sup_{k \in \mathbb{N}} \left| f_c^{\,k}(0) \right| < \infty \,\}.$$

Equivalently -- and this is the first milestone of the mission -- $c \in M$ if and only if $|f_c^{\,k}(0)| \le 2$ for every $k$, which exhibits $M$ as a compact subset of the plane.

$M$ is the parameter-space picture of the simplest non-trivial family in complex dynamics, and it acts as a dictionary: the shape of $M$ near a parameter $c$ encodes the dynamics of $f_c$ on its Julia set, so structural questions about $M$ are questions about the whole quadratic family at once. Douady and Hubbard proved in 1982 that $M$ is connected, by exhibiting a conformal isomorphism

$$\Phi : \mathbb{C} \setminus M \longrightarrow \mathbb{C} \setminus \overline{\mathbb{D}}$$

between the complement of $M$ and the exterior of the closed unit disk.

The question

MLC conjecture. $M$ is locally connected: every point of $M$ has a neighbourhood basis, in the subspace topology, consisting of connected sets.

By Caratheodory's theorem, MLC is equivalent to the statement that $\Phi^{-1}$ extends continuously to the unit circle. That extension would deliver a complete combinatorial description of $M$ -- the pinched disk model of Douady and Thurston -- in which every boundary point is labelled by the external rays landing on it. Two headline consequences follow: the density of hyperbolicity in the quadratic family (Fatou's conjecture: every quadratic polynomial can be perturbed to one with an attracting cycle), and zero area for $\partial M$.

MLC has been open since the early 1980s and is regarded as the central problem of one-dimensional complex dynamics.

Timeline

• 1982 -- Douady and Hubbard prove that $M$ is connected, via the Boettcher uniformisation of its complement, and formulate MLC.
• 1984/85 -- The Orsay notes develop the combinatorics of external rays and the pinched-disk model, and show that MLC implies the density of hyperbolicity in the quadratic family.
• 1990 -- Yoccoz proves MLC at every finitely renormalizable parameter without an indifferent periodic point, introducing the Yoccoz puzzle and the rigidity techniques that dominate later work.
• 1997 -- Lyubich extends local connectivity to infinitely renormalizable parameters of bounded type, using complex bounds for quadratic-like renormalization.
• 1997 -- Graczyk-Swiatek and Lyubich prove density of hyperbolicity in the real quadratic family.
• 1998 -- Shishikura proves that $\partial M$ has Hausdorff dimension $2$, by parabolic implosion. Whether $\partial M$ has positive area remains open.
• 2005 -- Buff and Cheritat construct quadratic Julia sets of positive area, showing that the analogous area question in the dynamical plane has a negative answer.
• Today -- MLC is known at large classes of parameters, but the general case, and with it the density of hyperbolicity, remain open.

What this mission asks for

The goal theorem is MLC itself, in the form "the Mandelbrot set, as a topological subspace of $\mathbb{C}$, is a locally connected space".

The milestones are of three kinds, and are ordered accordingly:

1. Foundations provable today -- the escape criterion (in the quadratic and the general unicritical degree) and compactness. These make the filter-theoretic definition usable and are the natural entry point for a solver new to the mission.
2. Known theorems from the literature -- connectedness of $M$ (Douady-Hubbard), the implication MLC $\Rightarrow$ density of hyperbolicity (Douady-Hubbard), and $\dim_H(\partial M) = 2$ (Shishikura). These are hard but settled, and formalizing them builds the infrastructure -- Boettcher coordinates, external rays, parabolic implosion -- that any attack on the goal will need.
3. The open companions -- density of hyperbolicity in the quadratic and unicritical families, zero area of $\partial M$, and MLC for all Multibrot sets $M_n$, the parameter sets of $z \mapsto z^n + c$.

All statements are phrased against a single shared definition file, so a solver can move between milestones without re-fixing conventions.

Motivation

Gelfand duality identifies compact Hausdorff spaces with commutative unital C*-algebras: a space $X$ corresponds to the algebra $C(X)$ of continuous complex functions, and continuous maps correspond contravariantly to unital *-homomorphisms (Gelfand 1941; in categorical form, Negrepontis 1971). Measure theory has an analogous expectation. A measurable space with a σ-ideal of negligible sets yields the commutative von Neumann algebra $L^\infty$ of bounded measurable functions modulo equality almost everywhere, and every commutative von Neumann algebra should arise in this way. Making that expectation precise as an equivalence of categories requires deciding which measurable spaces to allow and which maps between them to identify.

Timeline. Stone (1936–1937) established the duality between Boolean algebras and Stone spaces, and between complete Boolean algebras and extremally disconnected ones. Segal (1951) introduced localizable measure spaces. Dixmier (1951) characterized the Gelfand spectra of commutative von Neumann algebras as the hyperstonean spaces. Loomis (1947) and Sikorski (1948) represented σ-complete Boolean algebras as measurable sets modulo meager sets on their Stone spaces. Von Neumann (1932), Maharam (1958), Ionescu Tulcea (1965), Vesterstrøm–Wils (1969), Edgar (1976) and Graf (1980) gave criteria for lifting homomorphisms of measure algebras to point maps. Pavlov (arXiv:2005.05284, J. Pure Appl. Algebra) assembled these ingredients into one equivalence of categories. That equivalence is the subject of this mission.

Setting

An enhanced measurable space $(X,M,N)$ is a set $X$, a σ-algebra $M$ of subsets of $X$, and a σ-ideal $N\subseteq M$ of the power set $2^X$, the negligible sets. A premap $f\colon(X,M,N)\to(X',M',N')$ is a map defined on a conegligible subset of $X$ with $f^*M'\subseteq M$ and $f^*N'\subseteq N$. Two premaps are weakly equal almost everywhere, $f\approx g$, when $f^*m\oplus g^*m\in N$ for every $m\in M'$. The space is compact if some compact class $K\subseteq M$ (a family with the finite intersection property for all subfamilies) has a non-negligible member inside every non-negligible measurable set. It is strictly localizable if it is isomorphic, through premaps, to a coproduct of a small family of spaces carrying faithful finite measures. CSLEMS is the category of compact strictly localizable spaces with $\approx$-classes of premaps.

A frame is a complete lattice in which finite meets distribute over arbitrary joins; the category of locales is the opposite of the category of frames. A complete Boolean algebra is localizable if $1$ is the supremum of the elements $a$ for which $aA$ carries a finite faithful continuous valuation. MLoc, the category of measurable locales, is the full subcategory of locales on the localizable Boolean algebras. A hyperstonean locale is a Stonean locale (coherent, regular, $\neg x\vee\neg\neg x=1$) in which every nonzero open has a positive normal valuation not vanishing on it. A hyperstonean space is a sober space whose locale of opens is hyperstonean. HStoneanLoc and HStonean take open maps as morphisms. CVNA is the category of commutative von Neumann algebras (C*-algebras with a predual) and normal unital *-homomorphisms.

Formalization targets

Goal: Theorem 1.1

$$\mathsf{HStonean}\simeq\mathsf{HStoneanLoc},\qquad \mathsf{HStoneanLoc}\simeq\mathsf{MLoc},\qquad \mathsf{CSLEMS}\simeq\mathsf{MLoc},\qquad \mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}.$$

The goal is the existence of the four equivalences. It does not fix the functors.

The four equivalences with their functors

• Proposition 2.72: the equivalence $\mathsf{HStonean}\simeq\mathsf{HStoneanLoc}$ is implemented by the locale of opens $\Omega$.
• Proposition 2.73: the equivalence $\mathsf{HStoneanLoc}\simeq\mathsf{MLoc}$ is implemented by the compact opens $\mathrm{COpen}$.
• Theorem 3.20: the equivalence $\mathsf{MLoc}\simeq\mathsf{CVNA}^{\mathrm{op}}$ has inverse $\mathsf{ProjLoc}$, given by projections and restriction.
• Theorem 5.19: the equivalence $\mathsf{CSLEMS}\simeq\mathsf{MLoc}$ is implemented by $\mathsf{ML}$, the functor $(X,M,N)\mapsto M/N$, $f\mapsto f^*$.

Supporting milestones

The supporting milestones, in proof order:

• normal valuations versus continuous valuations on compact opens (Lemma 2.58);
• localizability through valuations (Lemma 2.53);
• completeness of $\mathsf{ProjAlg}(A)$ (Proposition 3.8);
• $A_*$ as continuous valuations (Proposition 3.9);
• $\mathsf{ProjAlg}$ as a functor (Lemma 3.11);
• σ-complete algebras with faithful valuations (Lemma 4.55);
• strict localizability implies localizability (Proposition 4.54);
• compactness of induced subspaces (Lemma 4.61);
• measurable images (Proposition 4.65);
• $\mathrm{TM}$ on hyperstonean spaces (Proposition 5.4);
• $\mathsf{ML}$ on morphisms (Lemma 5.11);
• the isomorphism $(X,M,N)\cong\mathrm{Spec}(\mathsf{ML}(X,M,N))$ (Proposition 5.16).

Significance

The result. Theorem 1.1 replaces commutative von Neumann algebras, a class of operator algebras, by measurable locales, which are pointless spaces. It also gives a point-set model, CSLEMS, in which morphisms are measurable maps modulo a null relation. With it, constructions on commutative von Neumann algebras can be carried out measure-theoretically and transported back: products, pushforwards of measures, and the identification of the predual with valuations. It also explains why the obvious choices fail. With localizable instead of strictly localizable spaces, with equality almost everywhere instead of weak equality, or without compactness, the measure-theoretic category is not dual to CVNA (Remarks 4.23 and 5.18).

Formalization. The theorem is proved in the paper. None of the five categories, and none of the equivalences, has a machine-checked form in Mathlib or on the platform. Mathlib has W*-algebras (WStarAlgebra), locales, Stonean spaces and Baire-measurable sets, but no normal homomorphisms, measure algebras or lifting theorems. The published module QAlgorithms_Papers_Independent_Support21_P20 formalizes this paper's valuations, enhanced measurable spaces and premaps, and poses several lemmas, three of which are milestones here. Completing the mission means formalizing Stone and Stonean duality for locales, the spectral theory of commutative von Neumann algebras through projections, and the von Neumann–Maharam lifting theorem for strictly localizable spaces.

Difficulty

The equivalences in §2 restrict classical dualities and are mostly bookkeeping once those dualities are available. Even so, Mathlib's Stone duality is not stated for locales with open maps. The central difficulty is Proposition 5.16. An object of CSLEMS must be isomorphic, through point maps, to the Stone spectrum of its own measure algebra. In one direction this needs a lifting $M/N\to M$ that is a Boolean homomorphism, and that uses strict localizability through the von Neumann–Maharam theorem. In the other direction it needs a point map from the spectrum back to $X$, constructed from the compact class. The natural first idea, choosing representatives class by class, does not give a homomorphism: liftings exist only through a transfinite construction. A second difficulty is Lemma 5.11. A Boolean homomorphism induced by a measurable map preserves countable suprema, but in general it does not preserve arbitrary ones (Remark 5.12). Compactness and the measurable image of Proposition 4.65 are what rule this out.

Formalization scope

All five categories live in one universe, with objects in Type u. The encoding commits to these conventions:

• CSLEMS. Morphisms are partial premaps (X → Option Y) modulo weak equality almost everywhere. Theorem 1.1's bullet speaks of maps of sets, but with total maps the theorem is false: $(\mathrm{pt},2^{\mathrm{pt}},2^{\mathrm{pt}})$ has no map to $\varnothing$ (Remarks 4.9, 4.15). Strict localizability uses a small index family and isomorphism in PreEMS; the faithful finite measures of its σ-finite pieces are countably additive maps $M\to\mathbb C$ with absolutely convergent sums (Remark 4.29), because Definition 4.28's saturation clause alone would also admit merely finitely additive ones. Compactness quantifies over arbitrary subfamilies, not countable ones.
• MLoc. The full subcategory of Mathlib's Locale on localizable Boolean algebras.
• HStoneanLoc and HStonean. Morphisms are open frame maps (Definition 2.15) and open continuous maps. Hyperstonean spaces are sober spaces whose frame of opens is hyperstonean.
• CVNA. Commutative CStarAlgebras with WStarAlgebra. Normality is stated as "pulls normal functionals back to normal functionals", which is equivalent to Definition 3.3 by Sakai's uniqueness of the predual.
• No nontriviality. The empty space, the one-element Boolean algebra and the zero algebra are allowed.

The equivalence milestones assert an equivalence together with a description of its functor. They never take a functor as a hypothesis, so none of the statements reduces to rfl or to an instance argument.

Reusable parts:

• the CSLEMS category, with the category laws of Propositions 4.7 and 4.14 proved inline;
• the quotient $M/N$ and the pull-back;
• $\mathrm{TM}$ and the Stone spectrum;
• the projection Boolean algebra.

Contributions are welcome at every level: proofs of the milestones, Stone and Stonean duality for locales, and a lifting theorem.

Selected references

• D. Pavlov, Gelfand-type duality for commutative von Neumann algebras, J. Pure Appl. Algebra 226 (2022); arXiv:2005.05284v3. https://arxiv.org/abs/2005.05284
• J. Dixmier, Sur certains espaces considérés par M. H. Stone, Summa Brasil. Math. 2 (1951), 151–182.
• M. H. Stone, Algebraic characterizations of special Boolean rings, Fund. Math. 29 (1937), 223–303. https://eudml.org/doc/212943
• I. E. Segal, Equivalences of measure spaces, Amer. J. Math. 73 (1951), 275–313. https://doi.org/10.2307/2372178
• D. Maharam, On a theorem of von Neumann, Proc. Amer. Math. Soc. 9 (1958), 987–994. https://doi.org/10.1090/S0002-9939-1958-0105479-6
• D. H. Fremlin, Measure Theory, Vol. 3 (Measure algebras), Torres Fremlin, 2002.
• P. T. Johnstone, Stone Spaces, Cambridge University Press, 1982.
• S. Sakai, C*-algebras and W*-algebras, Springer, 1971.

Motivation

In fair division, a value may be assigned to each interval that a cut produces. If the value is continuous in the interval's endpoints, an equal-value partition is a natural target. Some valuations are nonnegative and additive, but a difference of competing measures or a signed utility need have neither property. Avvakumov and Karasev establish equal-value partitions even when the value changes sign and is not additive, provided it vanishes on degenerate intervals. Their result is used by Bogomolnaia and Moulin in work on guarantees for fair division. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The paper identifies earlier special cases: a nonnegative valuation follows from the Knaster–Kuratowski–Mazurkiewicz theorem; prime-power numbers of parts with a valuation of varying sign were known through degree-theoretic results; additive valuations admit an elementary argument. The remaining case permits a sign-changing, nonadditive valuation and an arbitrary positive number of parts. The authors distinguish this from an envy-free division problem with separate valuations for several players, which they state remains open outside prime-power cases. Avvakumov and Karasev, p. 2; Avvakumov and Karasev, Envy-free division using mapping degree; Meunier and Zerbib.

Setting

Write $\mathcal I$ for the set of all subsegments $I=[a,b]$ of $[0,1]$ with $0\le a\le b\le1$. An interval may be degenerate, meaning $a=b$. A real-valued function $f$ on $\mathcal I$ is continuous when its value varies continuously with the two endpoints. The required boundary condition is $f([a,a])=0$ for every $a\in[0,1]$. No sign, monotonicity, or additivity condition is imposed. A partition into $m$ parts is a sequence $0=x_0\le x_1\le\cdots\le x_m=1$, so its parts $[x_{j-1},x_j]$ may also be degenerate. Avvakumov and Karasev, Theorem 1.1, pp. 1–2.

The intermediate setting is a nice multivalued function. Its graph is a compact subset $Z$ of $\mathcal I\times(-1,1)$. The graph separates the bottom $\mathcal I\times\{-1\}$ from the top $\mathcal I\times\{1\}$ inside the cylinder $C=\mathcal I\times[-1,1]$: those two sides lie in different connected components of $C\setminus Z$. A representation of a nice graph is a continuous real function $\varphi$ on $C$ that is negative on the bottom, positive on the top, and whose zero set is the graph. The paper passes between graphs and representations in Lemma 2.2. Avvakumov and Karasev, Definition 2.1 and Lemma 2.2, p. 2.

For a prime $p$, a segment $I=[a,b]$, and a value $y$, a zero partition is a sequence $a=x_0\le\cdots\le x_p=b$ such that $\varphi([x_{j-1},x_j],y)=0$ for each $j=1,\ldots,p$. The set $Z_p(\varphi)$ contains exactly those pairs $(I,y)$ that admit a zero partition. This is the projection to the cylinder of the paper's simultaneous-solution set $S$ for labeled partitions. Avvakumov and Karasev, equation (4.1) and Claim 4.4, pp. 7–9.

Formalization targets

The goal is Theorem 1.1: for every positive integer $m$ and every continuous $f$ satisfying the degenerate-interval condition, there are possibly repeated cut points with a common value:

$$0=x_0\le x_1\le\cdots\le x_m=1,\qquad f([x_0,x_1])=\cdots=f([x_{m-1},x_m]).$$

The theorem is already posed as the Open platform statement FairGuarantees.DivideChoose.theorem_of_4; this mission references that exact statement as its goal. It supplies the paper's supporting statements, including Lemma 2.2 on graph representations, Claim 4.4 on separation by projected zero partitions, and the prime-step Lemma 2.3. The latter asserts that, when $\varphi([a,a],y)=y$, there is a represented nice graph with the same degenerate identity whose zeros each yield a zero partition for $\varphi$. The milestone list includes the fixed-segment and continuous-family statements used to characterize $Z_p(\varphi)$, and equation (4.2) describing its degenerate boundary. Avvakumov and Karasev, Lemmas 2.2–2.3, pp. 2–3; Claims 4.3–4.4 and equation (4.2), pp. 8–9.

Significance

The theorem guarantees equal values for any positive number of consecutive parts under only endpoint continuity and the zero-on-degenerates condition. It covers valuations for which nonnegative or additive special-case results give no conclusion. It also provides the theorem invoked in the fair-guarantee application cited by the authors. Avvakumov and Karasev, pp. 1–2; Bogomolnaia and Moulin.

The mathematical result was proved in the paper; the platform's theorem statement remains Open and lacks a machine-checked proof there. Formalizing the paper's intermediate claims makes its topological assumptions and its treatment of degenerate parts explicit. The definitions of a separating graph, its representation, and zero partitions can also be reused for related partition problems. The present mission states the paper's prime-step targets, leaving the proofs and the underlying equivariant topology as work for solvers.

Difficulty

For a fixed signed valuation, continuity alone does not select one common value that works across every piece of an arbitrary partition. The nonnegative case has a simplex-covering argument, but that argument does not directly control values of both signs. In the paper's general case, the difficult claim is that the projected simultaneous-zero set separates an entire cylinder, even as the segment varies. Its source proof requires a mod-$p$ statement for a space of labeled partitions and control of the resulting solution set. A further boundary issue arises on degenerate segments: a representation of the projected graph must satisfy $\psi([a,a],y)=y$, not merely have the right zeros. Avvakumov and Karasev, pp. 2, 7–10.

Formalization scope

Lean represents $I=[a,b]$ by the endpoint pair $(a,b)$ with $0\le a\le b\le1$. The cylinder uses the closed value range $[-1,1]$; a nice graph lies in its open interior $(-1,1)$. Functions are total Lean functions, but only their values on this cylinder enter the definitions and results. Continuity is required on the cylinder. Separation uses connected components of its complement, as in Definition 2.1, and explicitly requires the bottom and top to avoid the graph. This prevents a graph containing a boundary side from satisfying separation vacuously.

Every prime-step claim assumes $p$ prime, the representation's strict boundary signs, and the degenerate identity. Zero partitions have exactly $p$ consecutive parts whose endpoints are pinned to the original segment; repeated cuts are allowed. The goal reference likewise permits degenerate parts and assumes $m\ge1$. The projected set is defined through existence of an ordinary ordered partition, independent of how the paper labels partitions in its configuration space. The needed existing Lean notions include ContinuousOn, IsCompact, connectedComponentIn, finite index types, and Nat.Prime. A complete proof development also needs results about the paper's labeled-partition complex, equivariant cycles and transverse maps. Contributions establishing that reusable topology, as well as proofs of the stated milestones, are within scope. Avvakumov and Karasev, §§2–4.

Selected references

• Sergey Avvakumov and Roman Karasev, Equipartition of a Segment, Mathematics of Operations Research, 2023. arXiv:2009.09862v4.
• Anna Bogomolnaia and Hervé Moulin, Guarantees in Fair Division: General or Monotone Preferences, 2019. arXiv:1911.10009v3.
• Sergey Avvakumov and Roman Karasev, Envy-Free Division Using Mapping Degree, Mathematika 67, 2021. arXiv:1907.11183.
• Frédéric Meunier and Shira Zerbib, Envy-Free Cake Division Without Assuming the Players Prefer Nonempty Pieces, Israel Journal of Mathematics 234, 2019. arXiv:1804.00449.

Motivation

Traffic users choose routes for themselves, while a planner may choose routes that minimize everyone's combined travel cost. The price of anarchy measures the cost of the users' equilibrium relative to the planner's optimum. Travel demand and arc latency functions are estimated from data and change over time, so a ratio that changes abruptly under a small input change would be difficult to interpret or use. Wu and Möhring study this sensitivity for nonatomic congestion games, where each individual user has negligible influence on arc flows. Their preprint proves that the optimum cost, equilibrium cost, and their ratio vary continuously over the game space they define. This mission isolates that foundational continuity result. It supplies the qualitative starting point for the paper's later Hölder and Lipschitz estimates.

The cited artifact is arXiv:2007.13979v3, dated 2021. The article subsequently appeared in Mathematics of Operations Research in 2023, but theorem numbers and pages here refer to the preprint.

Setting

Fix finite sets $A$ of arcs, $S$ of routes, and $K$ of origin–destination pairs. Each route $s$ serves one pair $k$ and contains at least one arc. Every arc belongs to some route, and every pair has at least two routes. A game $\Gamma=(\tau,d)$ assigns each arc $a$ a nonnegative, nondecreasing, continuous latency function $\tau_a:[0,\infty)\to[0,\infty)$ and each pair $k$ a nonnegative demand $d_k$. The total demand is $T(d)=\sum_{k\in K}d_k$. These are the paper's basic model and standing combinatorial assumptions (pp. 10–11 and 14).

A feasible flow $f$ puts nonnegative traffic on routes so that the traffic for each pair sums to its demand. The induced arc flow is $f_a=\sum_{s\ni a}f_s$. Its total cost is

$$C(\Gamma,f)=\sum_{a\in A} f_a\tau_a(f_a).$$

A social optimum (SO) is a feasible flow minimizing total cost. A Wardrop equilibrium (WE) is a feasible flow in which every route carrying positive traffic has minimum cost among the routes serving the same pair. Write $C^*(\Gamma)$ for the SO cost and $\widetilde C(\Gamma)$ for the WE cost. The paper shows that all SO flows have the same cost and all WE flows have the same cost (pp. 11–12 and 18).

A generalized game has the stated nonnegative demands and regular latency functions. The game space $\mathcal G(G,K,S)$ further requires $T(d)>0$ and $\tau_a(x)>0$ for every arc and every $0<x\le T(d)$, the paper's Condition 2. On this space, the optimum cost is positive and the price of anarchy is defined by

$$\rho(\Gamma)=\frac{\widetilde C(\Gamma)}{C^*(\Gamma)}.$$

For $\Gamma=(\tau,d)$ and $\Gamma'=(\sigma,d')$, the paper's distance $\operatorname{Dist}(\Gamma,\Gamma')$ is the maximum of three discrepancies: the sup norm of $d-d'$, the largest $|\tau_a(x)-\sigma_a(x)|$ for $a\in A$ and $0\le x\le\min\{T(d),T(d')\}$, and the sup norm of $\tau(T(d))-\sigma(T(d'))$. The last term compares costs at the two games' respective demand endpoints. Games with equal demands and equal latency functions up to that demand are identified as equivalent (pp. 15–17, (3.1)–(3.3)).

Formalization targets

The supporting milestones establish a positive lower bound for $C^*$ and an upper bound for $\rho$ (Lemma 3), the distance properties of generalized games (Lemma 4), and behavior of feasible, SO, and WE flows under convergent game sequences (Lemma 5). The goal is the paper's Theorem 6, p. 19: for any sequence $\Gamma_n\in\mathcal G(G,K,S)$ with $\operatorname{Dist}(\Gamma_n,\Gamma)\to0$ and $\Gamma\in\mathcal G(G,K,S)$,

$$C^*(\Gamma_n)\to C^*(\Gamma),\qquad \widetilde C(\Gamma_n)\to\widetilde C(\Gamma),\qquad \rho(\Gamma_n)\to\rho(\Gamma).$$

Significance

The theorem establishes that sufficiently small changes in both demand and latency data produce small changes in the two total costs and their ratio. It allows the PoA to be treated as a stable observable of a game, including where the identity of an optimum or equilibrium flow changes. The result is qualitative: it does not supply a uniform rate of change. The same paper investigates sharper rates under additional assumptions (§4).

The mathematical result is proved in the paper. In this mission its statements and definitions are compiled Lean drafts, while proofs of Theorem 6 and its milestone lemmas remain open. A completed development would make the game-space metric, limit-of-flow statements, and cost continuity available for later sensitivity results on nonatomic routing.

Difficulty

Pointwise continuity of each $\tau_a$ does not by itself control an optimum or equilibrium when demands change: the feasible-flow sets change with $d$, and a flow for one game need not be feasible for another. A converging sequence of games can also have different optimal or equilibrium flows at every index. The distance compares functions only on demand-relevant intervals, so limits of costs must respect those varying intervals. Finally, continuity of the quotient requires a positive optimum cost throughout the game space; the paper's Condition 2 is what makes that denominator meaningful (pp. 15–19).

Formalization scope

Lean uses finite types for arcs, routes, and pairs; a route is a nonempty $0$–$1$ incidence column and is assigned to one pair. This admits arbitrary route collections rather than insisting on loop-free directed graph paths. The standing network predicate records the nonempty pair set, nonempty routes, every arc's membership in a route, and at least two routes per pair. Costs are total functions on the reals, with continuity, monotonicity, and nonnegativity required only on $[0,\infty)$. Flow feasibility, arc flow, the Wardrop condition, and the potential reuse the published KellyStochasticNetworks_Wardrop definition. The total cost uses the arc formula; $C^*$ is an infimum over feasible flows and $\widetilde C$ a supremum over WE flows. On valid games these recover the paper's common SO and WE costs.

The distance uses the sup norm on finite vectors and a real supremum over the bounded shared demand interval. Convergence is stated sequentially, following the paper, without imposing a metric-space instance on raw games that may be equivalent. Every theorem involving $\rho$ quantifies over the game space, so a zero denominator or an empty equilibrium set cannot supply a spurious value. The route-count and arc-count factors in Lemma 3 are the actual finite cardinalities. Contributions that establish existence and compactness of relevant flow sets, equivalence of the arc and path cost formulas, and the stated limit properties are useful beyond this theorem.

Selected references

• Z. Wu and R. H. Möhring, A sensitivity analysis of the PoA in non-atomic congestion games, arXiv:2007.13979v3, 2021. Preprint.
• Z. Wu and R. H. Möhring, A Sensitivity Analysis of the Price of Anarchy in Nonatomic Congestion Games, Mathematics of Operations Research 48(3), 2023. DOI.

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

1. Franks (1971). A $C^1$ structurally stable diffeomorphism has only hyperbolic periodic points.
2. Consequence of Pugh's closing lemma. For a $C^1$ structurally stable $f$, $\overline{\mathrm{Per}(f)}=\Omega(f)$.
3. Mañé (1988). The goal for $r=1$.
4. Palis (1988). A $C^1$ $\Omega$-stable diffeomorphism satisfies Axiom A.
5. 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.

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

1. 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$.
2. Pugh's $C^1$ closing lemma (1967) — the case $r=1$ (published platform statement).
3. 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

Why first passage times need a continuity theorem

Functional limit theorems in queueing and applied probability are rarely proved from scratch. A limit theorem is established once for a primitive process, such as a random walk, a cumulative input or a renewal-reward process, and then transferred to the quantities of interest through the continuous mapping theorem: if $X_n \Rightarrow X$ in a function space and $f$ is continuous at almost every path of $X$, then $f(X_n) \Rightarrow f(X)$. The method works only if the functions in use are known to be continuous, and in which topology.

Ward Whitt's 1980 paper supplies these facts for composition, addition, the supremum, the reflecting barrier, the inverse or first passage time, and time reversal. This mission covers §7, the first passage time. Its role in applications is direct: the counting process of a renewal process is the first passage time of the partial-sum process. A limit theorem for cumulative work can therefore yield one for the number of completed jobs, and a limit theorem for a cumulative input can yield one for the time it takes to reach a level, when the mapping theorem's hypotheses hold.

Timeline. Skorohod (1956) introduced the topologies $J_1$ and $M_1$ on the space $D$ of right-continuous paths with left limits. Vervaat (1972) studied functional central limit theorems for processes with positive drift and their inverses, and Whitt (1971) studied weak convergence of first passage time processes. Whitt's 1980 paper restates $M_1$ continuity (Theorem 7.1) and adds the $J_1$ result: the map is continuous at every strictly increasing path (Theorem 7.2), although it is not $J_1$-continuous on its whole domain.

Setting

A path is a function $x : [0,\infty) \to \mathbb R$. It belongs to $D = D([0,\infty),\mathbb R)$ when it is right-continuous and has a left limit at every $t > 0$.

• $J_1$ convergence. On a compact interval $[0,b]$, $x_n \to x$ in $J_1$ when there are increasing homeomorphisms $\lambda_n$ of $[0,b]$ with $\sup_t |\lambda_n(t) - t| \to 0$ and $\sup_t |x_n(t) - x(\lambda_n(t))| \to 0$. On $[0,\infty)$ this is required on $[0,b]$ for every $b$ at which $x$ is continuous.
• $U$ convergence. Uniform convergence on compact subintervals.
• $M_1$ convergence. The completed graph of $x$ on $[0,b]$ adds to the graph the vertical segment joining $x(t-)$ and $x(t)$ at each jump. $x_n \to x$ in $M_1$ when the completed graphs admit parametric representations (continuous, order-preserving maps from $[0,1]$ onto the completed graph) that are uniformly close in both time and space.
• The supremum. $x^{\uparrow}(t) = \sup_{0 \le s \le t} x(s)$.
• The domain $E$. The set of $x \in D$ that are unbounded above and have $x(0) \ge 0$.
• First passage time. For $x \in E$,

$$x^{-1}(t) = \inf\{s \ge 0 : x(s) > t\}, \qquad t \ge 0.$$

• $D_0$. The nondecreasing paths in $D$, and $C$ the continuous ones.

Formalization targets

Goal: Theorem 7.2, continuity clause

If $x_n, x \in E$, $x$ is strictly increasing, and $x_n \to x$ in $J_1$, then

$$x_n^{-1} \to x^{-1} \quad (J_1).$$

The theorem says that every strictly increasing path is a continuity point of the first passage time map for $J_1$. It fixes no constants, so a sharper variant of a milestone does not invalidate it.

Milestones

1. $J_1$ convergence implies $M_1$ convergence (§6, p. 80).
2. The supremum map is $M_1$-continuous on paths with $x(0) \ge 0$ (§6, p. 80, as used in the proof of Theorem 7.1).
3. $x \in E$ implies $x^{-1} \in E \cap D_0([0,\infty),[0,\infty))$ (§7, p. 82).
4. $x^{\uparrow} \in E$ and $(x^{\uparrow})^{-1} = x^{-1}$ (proof of Theorem 7.1).
5. Theorem 7.1. If $x_n, x \in E$ and $x_n \to x$ in $M_1$, then $x_n^{-1} \to x^{-1}$ in $M_1$.
6. For strictly increasing $x \in E$, $x^{-1}$ is continuous with $x^{-1}(0) = 0$.
7. $M_1$ convergence to a continuous limit starting at $0$ is $U$ convergence.
8. $U$ convergence implies $J_1$ convergence.
9. Theorem 7.4. If $c_n \to \infty$, $x_n \in E$, $c_n(x_n^{\uparrow} - e) \to x$ and $c_n(x_n^{-1} - e) \to -x$ in $J_1$, then $x \in C$.

Significance

The result. Theorem 7.2 lets $J_1$ functional limit theorems pass to first passage times when the limit has strictly increasing paths. The typical case is the fluid limit $x(t) = \mu t$ of a cumulative process, with $\mu>0$. Together with the composition results of §3, it supports Theorem 7.3's centered inverse limit: if $c_n \to \infty$, $x_n \in E$, $x(0)=0$, $x$ has no positive jumps, and $c_n(x_n-e) \to x$ in $J_1$, then $c_n(x_n^{-1}-e) \to -x$ in $J_1$. This is one step from a central limit theorem for partial sums to one for counting processes. Theorem 7.4 shows a limitation: convergence of both the centered supremum and the centered inverse in $J_1$ forces a continuous limit.

Formalizing it. The results are proved and classical, but none of them has a machine-checked proof. The mission produces the $M_1$ topology on $D([0,\infty),\mathbb R)$ in Lean, the first passage time map with its basic properties, and the comparison between $J_1$, $M_1$ and $U$. That infrastructure is reused by every later formalization that goes through counting processes or the $M_1$ topology, including the planned wave of §§3–7 corollaries in this series.

Difficulty

The first passage time map is not $J_1$-continuous. On p. 82 the paper gives paths $x_n \to x$ in $J_1$ whose inverses converge only in $M_1$: a flat stretch of the limit becomes a jump of $x^{-1}$, which the inverses of the approximating paths approach through two separate jumps. Inverting the time changes $\lambda_n$ of the $J_1$ convergence cannot handle that split, because $J_1$ matches jumps one to one. The hypothesis that $x$ is strictly increasing excludes flat stretches of the limit. The technical weight lies in completed graphs and their parametric representations, which Mathlib does not have, and in the restriction to compact intervals at continuity points of the limit.

Formalization scope

• Paths are total functions $\mathbb R \to \mathbb R$. Only $[0,\infty)$ matters, and every statement is on Ici 0. All convergences are sequential, which is equivalent because the spaces are metrizable (Theorem 2.6). Membership of every path in $D$ is part of each convergence.
• $J_1$ is the shared layer of the series: the metric (2.1) with $[0,\infty]$-valued distances, extended to $[0,\infty)$ through restrictions to $[a,b]$ whose endpoints are continuity points or endpoints.
• $M_1$ is not defined in the paper. The mission defines it with the convention $x(0-) := 0$ at the origin, so the completed graph on $[0,b]$ starts with the segment from $(0,0)$ to $(0,x(0))$. With the convention $x(0-) = x(0)$, Theorem 7.1 is false. For $x(s) = (s-1)^+$ and $x_n = x + 1/n$, $x_n^{-1}$ jumps from $0$ to $1$ at $t = 1/n$ while $x^{-1}(0) = 1$. The convention is Whitt's later $M_1'$. Two milestones carry a hypothesis that this convention forces, and each says so: the supremum milestone requires $x_n(0), x(0) \ge 0$ (as on $E$), and the $M_1 \Rightarrow U$ milestone requires $x(0) = 0$. The goal, which is stated in $J_1$, does not depend on the convention.
• $x^{-1}$ is a real infimum. Its set is nonempty because paths in $E$ are unbounded above, so every statement that uses $x^{-1}$ assumes membership in $E$. The inequality $x(s) > t$ is strict, as on the page.
• Omitted. The measurability clause of Theorem 7.2 refers to the Borel σ-field of $J_1$, which the series does not build, and it is not stated. Replacing it by measurability for the product σ-algebra would be a different statement. The second clause of the §6 sentence on $D_0$ is also not stated.
• Ruled out. A formalization in which $x^{-1}$ is applied outside $E$ (giving the junk value $0$), or in which $J_1$ convergence omits membership in $D$ (making the restriction clause vacuous), would trivialize the goal. Both are excluded.

Contributions welcome: the general theory of parametric representations (existence, and the $M_1$ comparison with $J_1$ and $U$), which is reusable for any $M_1$ result. Alternative proofs of Theorem 7.2 that avoid $M_1$ are also welcome.

Selected references

• W. Whitt, Some Useful Functions for Functional Limit Theorems, Mathematics of Operations Research 5(1), 1980, 67–85. https://doi.org/10.1287/moor.5.1.67
• A. V. Skorohod, Limit theorems for stochastic processes, Theory of Probability and Its Applications 1(3), 1956, 261–290. https://doi.org/10.1137/1101022
• W. Whitt, Weak convergence of first passage time processes, Journal of Applied Probability 8(2), 1971, 417–422. https://doi.org/10.2307/3211913
• W. Vervaat, Functional central limit theorems for processes with positive drift and their inverses, Zeitschrift für Wahrscheinlichkeitstheorie 23, 1972, 245–253. https://doi.org/10.1007/BF00532510
• W. Whitt, Stochastic-Process Limits, Springer, 2002, §13.6. https://doi.org/10.1007/b97479

Motivation

An arc can end at a point of a curve in several distinct directions. Menger's 1927 paper asks whether the number of arcs that can meet only at that point is determined by a local measurement: the smallest boundary size available around the point. This gives a concrete meaning to the order of a point in a regular curve. The question belongs to the early study of curves as compact metric spaces rather than as drawn or parametrized lines. A curve can wind near a point in ways that make the count of visible branches misleading; the local boundary definition is meant to survive such behavior. Menger, Zur allgemeinen Kurventheorie (1927), pp. 96–99.

The paper also states a topological version of the disjoint-path principle: if a small point set cannot separate two finite sets in a suitable compact space, the space contains a corresponding number of disjoint arcs between them. This principle connects the local order question to Menger's finite-graph result, treated separately in the first mission of this series. Here the central object remains a regular curve and one of its points. Menger (1927), Satz β and Satz δ, pp. 100–102.

Setting

A curve is a compact connected metric space in which each point has arbitrarily small open neighbourhoods with totally disconnected boundaries. A point is regular if arbitrarily small open neighbourhoods have finite boundaries. A regular curve is a curve all of whose points are regular. Because every finite set is totally disconnected, the Lean representation takes a compact connected metric space and requires every point to be regular; this already satisfies the paper's curve condition. Menger (1927), pp. 96–97.

For a point $p$, write $\partial U$ for the boundary of an open neighbourhood $U$. The point has order at most $n$ if every open neighbourhood of $p$ contains one with at most $n$ boundary points. It has order exactly $n$ if it has order at most $n$ and no smaller finite order. Thus an upper bound on order is not the same as exact order. An arc is a continuous injective map $\gamma:[0,1]\to R$. A topological $n$-leg at $p$ is a family of $n$ arcs with $\gamma_i(0)=p$ and with images intersecting exactly in $\{p\}$ for distinct indices. Injectivity makes each leg a real arc, including when the space has isolated or degenerate cases.

To express the intermediate results, a set $E$ separates $A$ and $B$ in a space $M$ if $M\setminus E$ is the union of two disjoint relatively closed parts, one containing $A\setminus E$ and the other containing $B\setminus E$. The space is $n$-point connected between $A$ and $B$ if no subset $E\subseteq M$ with fewer than $n$ points separates them. In the theorems using this notion, $A$ and $B$ are disjoint and closed in $M$, as stipulated before Menger's definition. A separator may itself meet either set. Menger (1927), pp. 99–100.

Formalization targets

Order and legs

The main target is the first and final assertions of Menger's Theorem on p. 98. For every point $p$ of exact finite order $n$ in a regular curve $R$,

$$\operatorname{HasNBein}(p,n)\quad\text{and}\quad \neg\operatorname{HasNBein}(p,n+1).$$

This states that $n$ is the greatest possible number of legs. The second assertion is the observation begun on p. 97 and completed on p. 98; it is included because the Theorem's concluding characterization depends on it. The paper's separate assertion for points of growing order is outside this finite-order target. Menger (1927), pp. 97–98.

Disjoint arcs between finite sets

The principal supporting target is Satz β. In a compact metric space $K$ whose points are all regular, let $P,Q$ be finite disjoint sets. If $K$ is $n$-point connected between them, there are $n$ pairwise disjoint arcs, each with one endpoint in $P$ and the other in $Q$. Satz δ is the finite union-of-arcs case, while Satz γ concerns decreasing intersections of closed separators. The milestone list also records the neighbourhood sequence, its annulus connectivity statement, and Satz α, which gives disjoint arcs crossing each annulus. Menger (1927), pp. 99–105.

Significance

The result turns a definition made from arbitrarily small neighbourhood boundaries into a geometric count of arcs. It permits local point order to be recognized through an embedded finite star, without choosing a drawing or a parametrization of the whole curve. Satz β supplies a reusable disjoint-arcs statement for compact regular spaces; Satz γ isolates the compactness and local-connectedness condition needed when separators are obtained as a limit. These are independent point-set topology statements as well as parts of the order theorem. Menger (1927), pp. 98–105.

The theorem is proved in the paper; the work here is to state its objects and assertions precisely in Lean and then supply checked proofs. Mathlib supplies boundaries, compactness, extended cardinality, unit intervals and connected components, but these Menger-specific definitions and topological disjoint-arcs theorems are not already represented by a matching published platform item in the local prior-art catalog. The first mission of this series treats the finite-graph form of Satz δ; its draft statement is distinct from the topological version here and cannot be imported as a published theorem.

Difficulty

A direct attempt to add one new arc to a chosen collection can fail. Menger gives a curve made from a line segment and a spiral winding toward its midpoint: the point has two available directions, but choosing the spiral as the first leg leaves no second leg disjoint from it away from the midpoint. The count of already selected arcs therefore does not by itself control whether another can be added. The paper also notes that an inverse-limit argument does not immediately apply, because the order of a point in a decreasing family of regular curves can drop in the intersection. These examples explain why the statement needs conditions on boundary sizes and separators rather than only a local picture of branches. Menger (1927), p. 99.

Formalization scope

The Lean development uses a metric space with CompactSpace and ConnectedSpace for the main regular curve. An open set containing $p$ is a neighbourhood. “Arbitrarily small” means that every such open set contains a smaller open set with the stated boundary property. Boundary size is measured by Set.encard, so infinite boundaries do not receive the spurious value zero. Exact order includes a minimality clause for every $m<n$, including $n=0$. Arc maps use the closed unit interval and are continuous and injective; the parameter value zero is the endpoint at $p$. Pairwise disjoint legs have image intersection exactly $\{p\}$, while arcs joining $P$ to $Q$ have disjoint images altogether.

For the neighbourhood milestone, “shrinking to $p$” is made quantitative by diameters tending to zero, with each neighbourhood bounded; compactness gives the latter. The paper's sequence starts at $k=1$, while Lean starts at $k=0$. The annulus is constructed as $\overline U\setminus U'$ from nested open neighbourhoods, and its endpoints are the two frontiers. Relative closedness in the definition of separation is imposed inside $M\setminus E$. Satz β is stated for a compact space of regular points without adding connectedness or an independent finite-components assumption. A compact subset can be represented by its subtype when this theorem is applied. The ordinary one-dimensional spaces of Satz δ are finite unions of injective arcs, with distinct arcs meeting only at common endpoints.

The development needs reusable lemmas on finite-boundary neighbourhoods, regularity of the relevant subspaces, closed separators, and the relation between point connectivity and disjoint arcs. Contributions to these foundations and to the seven stated milestones are in scope. Constant maps cannot count as legs, and order at most $n$ alone cannot be used to demand an $n$-leg; both would erase the theorem's content.

Selected references

• Karl Menger, Zur allgemeinen Kurventheorie, Fundamenta Mathematicae 10 (1927), 96–115. DOI: 10.4064/fm-10-1-96-115.

Motivation

The maximum flow problem asks how much of a commodity can be shipped from a source to a sink through a network whose arcs have limited capacities. L. R. Ford, Jr. and D. R. Fulkerson's 1956 paper Maximal Flow Through a Network proved the minimal cut theorem: the largest flow value equals the smallest total capacity of a set of arcs that separates source from sink. That theorem is formalized in the companion mission Maximal Flow Through a Network I.

The second section of the same paper treats a special class of networks, those that remain planar after an arc from source to sink is added. For these networks the paper shows that one particular source–sink chain crosses every minimal separating set exactly once. This structural fact turns the minimal cut theorem into a simple computing procedure: repeatedly push as much flow as possible along such a chain and delete the arcs it saturates. The paper notes that G. Dantzig had conjectured, before the minimal cut theorem was proved, that this procedure yields a maximal flow on planar networks. The same "uppermost path" idea underlies later algorithms for maximum flow in planar graphs with source and sink on a common face (Itai and Shiloach, 1979).

The statement is short and purely combinatorial in its conclusion, but its hypothesis is topological. This mission isolates that theorem.

Setting

A network $N$ has a finite set $V$ of vertices and a finite set $E$ of arcs. Each arc $e$ joins two distinct end vertices, written $\mathrm{tail}(e)$ and $\mathrm{head}(e)$; arcs carry no direction, and two arcs may join the same pair of vertices. Two distinct vertices are distinguished, the source $a$ and the sink $b$, and each arc carries a positive capacity (capacities play no role in the target below).

A chain joining $u$ and $w$ is a set $C$ of distinct arcs that can be arranged as $\alpha_1(v_0v_1), \alpha_2(v_1v_2), \dots, \alpha_k(v_{k-1}v_k)$ with $v_0 = u$, $v_k = w$, and the vertices $v_0, \dots, v_k$ pairwise distinct; each arc may be traversed in either direction. The empty set is the null chain from $u$ to $u$.

A set $D$ of arcs is a disconnecting set if every chain joining $a$ and $b$ contains an arc of $D$. A disconnecting set none of whose proper subsets is disconnecting is a cut.

The network is ab-planar if the graph of $N$, together with one additional arc joining $a$ and $b$, can be drawn in the plane without crossings: vertices go to distinct points of $\mathbb R^2$; each arc, including the added arc $ab$, goes to an injective continuous path between the points of its end vertices; no arc passes through a vertex other than its ends; and two distinct arcs meet only at endpoints of both. In Lean the drawing is the structure ABPlaneDrawing N, and $N$ is ab-planar when Nonempty (ABPlaneDrawing N). The section's standing assumption is that no arc of $N$ already joins $a$ and $b$.

Formalization targets

Goal: Theorem 2 (p. 403)

If $N$ is ab-planar, no arc of $N$ joins $a$ and $b$, and some chain joins $a$ and $b$, then

$$\exists\, T \text{ a chain joining } a \text{ and } b \ \text{ such that }\ |T \cap D| = 1 \ \text{ for every cut } D \text{ of } N.$$

This is FordFulkerson56.Planar.ab_planar_exists_chain_meeting_each_cut_once. "Precisely once" is exact cardinality one, neither "at least once" (true of every chain) nor "at most once".

Milestone: a chain meeting a cut in one prescribed arc (proof of Theorem 2, p. 403)

For every network $N$, every cut $D$ and every arc $\alpha \in D$, there is a chain $C$ joining $a$ and $b$ with $C \cap D = \{\alpha\}$. No planarity is involved; the statement is what the minimality of a cut provides to the proof.

Further item: the Fig. 2 example (p. 403)

In the "gas, water, electricity" graph $K_{3,3}$ with the arc $ab$ removed, every chain joining $a$ and $b$ meets some cut in three arcs. This network is not ab-planar, so the example shows that the planarity hypothesis of Theorem 2 cannot be dropped.

Significance

Theorem 2 and the minimal cut theorem together give the paper's procedure for planar networks: if $T$ meets every cut once, then imposing a flow $k$ on $T$ lowers the value of every cut by exactly $k$, so the minimal cut value, and hence the maximal flow value, drops by $k$. Saturated arcs can then be deleted and the step repeated. Without the "exactly once" property the reduction could overshoot the cut structure, and the greedy step would not be justified. The theorem is also one of the earliest instances of the link between planarity and cut structure that later underlies planar duality arguments for minimum cuts.

The result has been known since 1956 and is not open. No machine-checked version is recorded on the platform, and Mathlib, at the pinned revision, has neither planar graphs nor the Jordan curve theorem. A formal proof would be the first formalized statement about source–sink planar networks in this library, and the counterexample item records, as a checkable fact, that the hypothesis is necessary.

Difficulty

The conclusion is combinatorial while the hypothesis is a drawing in $\mathbb R^2$. The paper's proof normalises the drawing (the added arc $ab$ on the outer boundary, the graph in a vertical strip with $a$ on the left line and $b$ on the right), selects the "top-most" chain from $a$ to $b$, and argues that a chain meeting a cut below the top-most chain must cross another such chain. Each of these steps rests on plane topology: the existence of the outer region, the meaning of "top-most", and the fact that two chains with interleaved endpoints on a boundary must intersect, which is a form of the Jordan curve theorem.

The naive purely combinatorial route fails: the analogous statement for arbitrary networks is false (Fig. 2), so any argument has to use the drawing somewhere. Replacing the drawing by a combinatorial embedding (rotation systems, faces) is possible but then requires proving that the two notions agree, which is again Jordan-curve territory.

Formalization scope

Conventions committed to in the Lean statements:

• Vertices and arcs are finite types V, E with decidable equality. Arcs are undirected, may be parallel, and have two distinct end vertices. Source and sink are distinct, capacities are positive (structure Network).
• A chain is a Finset E that is the arc set of some arrangement as a simple path (IsChainWalk, IsChain); the null chain is allowed.
• IsDisconnecting and IsCut quantify over all chains joining source and sink; a cut is a disconnecting set no proper subset of which is disconnecting.
• ab-planarity is a plane drawing of the graph with the extra arc indexed by none : Option E, with injective Paths in ℝ × ℝ as arcs.

Hypotheses of the goal: hno_ab, the standing assumption of §2 (no arc joins $a$ and $b$, p. 403); hconn, that some chain joins $a$ and $b$. The second is not stated in the paper; its proof starts from "the chain joining a and b which is top-most", which presupposes one, and without it the statement is false (if $a$ and $b$ are disconnected, the empty set is a cut and no chain exists).

The drawing structure is satisfiable (a three-vertex path network has an explicit drawing), so the planarity hypothesis is not vacuous; and it covers the added arc $ab$ and all crossings, so $K_{3,3}$ minus $ab$ is not ab-planar and the goal is not refuted by the paper's own example. A formalization that dropped the arc $ab$ from the drawing, or quantified over disconnecting sets instead of cuts, would state a false theorem and is ruled out.

A complete development needs basic plane topology for paths in $\mathbb R^2$ (a Jordan-curve-type separation lemma for simple closed curves, or an equivalent statement about crossing paths in a strip), together with combinatorial lemmas about chains (concatenation and shortcutting of chains at a common vertex). The topological lemmas are reusable well beyond this mission. Proofs through a combinatorial embedding are welcome, provided the equivalence with ABPlaneDrawing is proved.

Selected references

• L. R. Ford, Jr. and D. R. Fulkerson, Maximal Flow Through a Network, Canadian Journal of Mathematics 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• H. Whitney, Non-separable and planar graphs, Transactions of the American Mathematical Society 34 (1932), 339–362. https://doi.org/10.1090/S0002-9947-1932-1501641-2
• A. Itai and Y. Shiloach, Maximum flow in planar networks, SIAM Journal on Computing 8 (1979), 135–150. https://doi.org/10.1137/0208012
• H. Whitney, Planar graphs, Fundamenta Mathematicae 21 (1933), 73–84. https://doi.org/10.4064/fm-21-1-73-84