Dynamical Systems

Motivation

A stochastic approximation algorithm updates an estimate by small noisy steps, $x_{n+1}-x_n=\gamma_{n+1}(F(x_n)+U_{n+1})$, with step sizes $\gamma_n\to0$ and noise $U_n$. Such recursions underlie stochastic gradient descent, adaptive control, reinforcement learning (Q-learning, temporal-difference methods) and learning in games (fictitious play, reinforcement models). The ODE method compares the long-run behaviour of the algorithm with that of the ordinary differential equation $\dot x=F(x)$. Classical versions of this comparison (Ljung 1977, Kushner and Clark 1978) assume the ODE has a globally asymptotically stable equilibrium, or a Lyapunov function, and cannot describe algorithms whose ODE has periodic orbits, heteroclinic cycles or chaotic sets.

Benaïm and Hirsch (1996) replaced these special assumptions by a single dynamical statement: the interpolated algorithm is an asymptotic pseudotrajectory of the flow of $F$, and the limit set of every precompact asymptotic pseudotrajectory is internally chain transitive. This mission formalizes that limit set theorem as it is presented in Michel Benaïm's lecture notes Dynamics of Stochastic Approximation Algorithms (Séminaire de Probabilités XXXIII, 1999).

Timeline. Bowen (1975) and Conley (1978) introduced $(\delta,T)$-pseudo-orbits and chain recurrence, and Conley proved that the chain recurrent set of a flow on a compact space is internally chain recurrent. Benaïm (1996, SIAM J. Control Optim.) related limit sets of stochastic approximation processes to the chain recurrence of the ODE; Benaïm and Hirsch (1996) introduced asymptotic pseudotrajectories for semiflows on metric spaces and proved the limit set theorem in the form formalized here. The 1999 notes give a self-contained proof through the translation semiflow on a space of curves.

Setting

Let $(M,d)$ be a metric space. A semiflow $\Phi$ on $M$ is a continuous map $\mathbb R_+\times M\to M$, $(t,x)\mapsto\Phi_t(x)$, with $\Phi_0=\mathrm{Id}$ and $\Phi_{t+s}=\Phi_t\circ\Phi_s$. A set $A$ is invariant if $\Phi_t(A)=A$ for every $t\ge0$; then $\Phi|A$ denotes the restricted semiflow on $A$.

A continuous curve $X:\mathbb R_+\to M$ is an asymptotic pseudotrajectory of $\Phi$ if

$$\lim_{t\to\infty}\sup_{0\le h\le T}d\big(X(t+h),\Phi_h(X(t))\big)=0\quad\text{for every }T>0,$$

and it is precompact if $X(\mathbb R_+)$ has compact closure. Its limit set is $L(X)=\bigcap_{t\ge0}\overline{X([t,\infty))}$.

For $\delta>0$, $T>0$, a $(\delta,T)$-pseudo-orbit from $a$ to $b$ consists of $k\ge1$ partial trajectories, given by points $y_0,\dots,y_{k-1}$ (and an endpoint $y_k$) and times $t_0,\dots,t_{k-1}\ge T$ with $d(y_0,a)<\delta$, $d(\Phi_{t_j}(y_j),y_{j+1})<\delta$ for $j<k$, and $y_k=b$. One writes $a\hookrightarrow b$ if such pseudo-orbits exist for all $\delta,T>0$. A nonempty compact invariant set $\Lambda$ is internally chain transitive if $a\hookrightarrow b$ for the restricted semiflow $\Phi|\Lambda$ for all $a,b\in\Lambda$, so that all $y_i$ lie in $\Lambda$; it is internally chain recurrent if $a\hookrightarrow a$ for $\Phi|\Lambda$ for every $a\in\Lambda$. An attractor is a nonempty compact invariant set $A$ with a neighbourhood $W$ such that $\operatorname{dist}(\Phi_tx,A)\to0$ uniformly in $x\in W$.

Formalization targets

Goal: Theorem 5.7 (i)

For every semiflow $\Phi$ on a metric space $M$ and every precompact asymptotic pseudotrajectory $X$ of $\Phi$,

$$L(X)\ \text{is internally chain transitive.}$$

Milestones (in the order of the proof)

• Lemma 3.1. $X$ is an asymptotic pseudotrajectory iff $d(\Theta^t(X),\hat\Phi\circ\Theta^t(X))\to0$, where $\Theta$ is the translation semiflow on $C^0(\mathbb R_+,M)$ and $\hat\Phi(Y)=\Phi^{Y(0)}$.
• Theorem 3.2. For precompact continuous $X$: $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of $\Theta^{t}(X)$, $t\to\infty$, is a trajectory of $\Phi$; and then $\{\Theta^t(X)\}_{t\ge0}$ is relatively compact.
• Lemma 5.2. A nonempty open $U$ with compact closure and $\Phi_T(\overline U)\subset U$ for some $T>0$ contains an attractor whose basin contains $\overline U$.
• Proposition 5.3. For nonempty $\Lambda$: internally chain transitive $\iff$ connected and internally chain recurrent $\iff$ compact, invariant and $\Phi|\Lambda$ has no proper attractor.
• Theorem 5.5. On a nonempty compact $M$, the chain recurrent set $R(\Phi)$ is internally chain recurrent.
• Corollary 5.6. If $\overline{\gamma^+(x)}$ is compact, then $\omega(x)$ is internally chain transitive.

Significance

The result. Theorem 5.7 (i) is the bridge between probability and dynamics in the ODE method. Once a stochastic approximation process is shown to be an asymptotic pseudotrajectory (missions 2 to 4 of this series do that under martingale-noise conditions), every statement about its limit points becomes a statement about internally chain transitive sets of the ODE: convergence to equilibria when a Lyapunov function exists (Proposition 6.4), convergence to attractors with positive probability (Theorem 7.3), and the analysis of learning dynamics in games. The theorem is sharp in the sense that every internally chain transitive set is a limit set of some asymptotic pseudotrajectory (Theorem 5.7 (ii), proved in Benaïm and Hirsch 1996 and not part of this mission).

Formalizing it. The result is proved in the literature; it is not formalized. Mathlib has semiflows (Flow), omega limit sets and the compact-open topology, but no pseudo-orbits, chain recurrence, Conley's theory of attractors, or asymptotic pseudotrajectories. This mission produces that layer for semiflows on general metric spaces, which is reusable for any later formalization of the ODE method, of Conley theory, or of learning in games.

Difficulty

The obvious approach follows $X$ from a point $a\in L(X)$ to a point $b\in L(X)$: $X$ returns near $a$ and near $b$ infinitely often, and on windows of length $T$ it is close to a trajectory, so concatenating windows gives a pseudo-orbit. The pseudo-orbit obtained this way has its points on the curve $X$, not in $L(X)$; this only shows that $L(X)$ is chain transitive for $\Phi$ on $M$, a strictly weaker property. Producing pseudo-orbits whose points lie in $L(X)$ itself is the central difficulty, and it is where precompactness of $X$ is used. Invariance $\Phi_t(L(X))=L(X)$, with equality, also needs a compactness argument, since a semiflow is not invertible.

Formalization scope

A semiflow is Mathlib's Flow ℝ≥0 M on a [MetricSpace M]; $M$ is arbitrary, with no compactness, completeness or local compactness. Time is ℝ≥0. Curves are functions ℝ≥0 → M; continuity is part of being an asymptotic pseudotrajectory, and precompactness is IsCompact (closure (Set.range X)). Invariance is equality $\Phi_t(A)=A$. Internally chain recurrent and internally chain transitive sets are nonempty by definition, and their pseudo-orbits are those of the restricted semiflow on the subtype $\Lambda$, so every point of the pseudo-orbit lies in $\Lambda$. Attractors converge uniformly on a neighbourhood. Lemma 3.1 and Theorem 3.2 are stated on $C^0(\mathbb R_+,M)$ (C(ℝ≥0, M), compact-open topology) with the half-line distance; the notes write $C^0(\mathbb R,M)$, but with the convention $\Phi^p(t)=p$ for $t<0$ that version fails for semiflows (a periodic trajectory is a counterexample), and the notes themselves describe asymptotic pseudotrajectories as points of $C^0(\mathbb R_+,M)$.

Ruled out: pseudo-orbits with no trajectory piece ($k=0$), pseudo-orbits allowed to leave $L(X)$, invariance as mere inclusion $\Phi_t(A)\subset A$, and any compactness assumption on $M$. Each of these makes the goal weaker than the theorem of the notes.

A complete development needs: elementary properties of pseudo-orbits (concatenation, continuity estimates), Arzelà–Ascoli on C(ℝ≥0, M), Conley's attractor construction, and the conjugacy between $\Phi$ and the translation semiflow on $S_\Phi$. Proofs of the milestones, alternative direct proofs of the goal (Benaïm 1996), and reusable lemmas about chain recurrence for Flow are all welcome.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Benaïm, A dynamical system approach to stochastic approximations, SIAM J. Control Optim. 34 (1996), 437–472. https://doi.org/10.1137/S0363012993253534
• C. Conley, Isolated Invariant Sets and the Morse Index, CBMS Regional Conference Series in Mathematics 38, AMS, 1978. https://doi.org/10.1090/cbms/038

Motivation

A stochastic approximation algorithm is a recursion

$$x_{n+1}-x_n=\gamma_{n+1}\big(F(x_n)+U_{n+1}\big)$$

in $\mathbb R^d$, driven by a vector field $F$, decreasing step sizes $\gamma_n$ and perturbations $U_n$. Robbins–Monro root finding, stochastic gradient descent, adaptive filters, learning dynamics in games (fictitious play, reinforcement learning) and urn models all have this form. The ODE method, introduced by Ljung (1977) and developed by Kushner and Clark (1978), Métivier and Priouret (1987) and Kushner and Yin (1997), studies such a recursion by comparing it with the differential equation $\dot x=F(x)$.

Benaïm and Hirsch (1996) gave the comparison a dynamical form: the continuous-time interpolation of $\{x_n\}$ is an asymptotic pseudotrajectory of the flow of $F$. Proposition 4.1 of Benaïm's lecture notes (Séminaire de Probabilités XXXIII, 1999) states that deterministic comparison theorem under two assumptions: a noise condition (A1) and either bounded iterates (A2) or a Lipschitz, bounded vector field near the iterates (A2′). The notes then verify A1 almost surely for martingale noise (Propositions 4.2 and 4.4) and use the asymptotic pseudotrajectory property to describe limit sets, attractors and nonconvergence.

Setting

Let $F:\mathbb R^d\to\mathbb R^d$ be continuous. It is globally integrable if through every point there is exactly one integral curve $y:\mathbb R\to\mathbb R^d$, $\dot y=F(y)$; the flow $\Phi_t(p)$ is the value at time $t$ of the integral curve through $p$.

The step sizes satisfy $\gamma_n\ge0$, $\sum_n\gamma_n=\infty$ and $\gamma_n\to0$. Set $\tau_0=0$, $\tau_n=\sum_{i=1}^n\gamma_i$, and $m(t)=\sup\{k\ge0:\tau_k\le t\}$. The affine interpolated process $X:\mathbb R_+\to\mathbb R^d$ and the piecewise constant processes $\overline X,\overline U,\bar\gamma$ are, for $0\le s<\gamma_{n+1}$,

$$X(\tau_n+s)=x_n+s\,\frac{x_{n+1}-x_n}{\gamma_{n+1}},\qquad \overline X(\tau_n+s)=x_n,\quad \overline U(\tau_n+s)=U_{n+1},\quad \bar\gamma(\tau_n+s)=\gamma_{n+1}.$$

The noise enters through

$$\Delta(t,T)=\sup_{0\le h\le T}\Big\|\int_t^{t+h}\overline U(s)\,ds\Big\| .$$

• A1: for every $T>0$, $\sup\{\|\sum_{i=n}^{k-1}\gamma_{i+1}U_{i+1}\|:n<k\le m(\tau_n+T)\}\to0$ as $n\to\infty$; equivalently $\Delta(t,T)\to0$ as $t\to\infty$.
• A2: $\sup_n\|x_n\|<\infty$.
• A2′: $F$ is Lipschitz and bounded on a neighbourhood of $\{x_n\}$.

A continuous $X:\mathbb R_+\to\mathbb R^d$ is an asymptotic pseudotrajectory of $\Phi$ if for every $T>0$

$$\lim_{t\to\infty}\sup_{0\le h\le T}\big\|X(t+h)-\Phi_h(X(t))\big\|=0 .$$

Formalization targets

Goal: Proposition 4.1

$$F\ \text{continuous, globally integrable},\quad \text{A1},\quad \text{A2 or A2}'\quad\Longrightarrow\quad X\ \text{is an asymptotic pseudotrajectory of}\ \Phi .$$

No rate and no constant appear; the statement holds under either alternative.

Milestones

1. Eq. (9): $X(t)-X(0)=\int_0^t[F(\overline X(s))+\overline U(s)]\,ds$.
2. A1: the discrete and the continuous forms of A1 are equivalent, for each $T>0$.
3. Theorem 3.2: for a flow on a metric space and a continuous $X$ with relatively compact image, $X$ is an asymptotic pseudotrajectory iff $X$ is uniformly continuous and every limit point of the translates $\Theta^t(X)$ in $C^0(\mathbb R,M)$ is a trajectory of the flow; both imply that $\{\Theta^t(X)\}$ is relatively compact.
4. Comparison of $X$ and $\overline X$ (p. 13): if $\|F(x_n)\|\le K$, then for $t$ large, $\sup_{t\le u\le t+T}\|X(u)-\overline X(u)\|\le2\Delta(t-1,T+1)+\sup_{t\le u\le t+T}K\bar\gamma(u)$.
5. Estimate (11): under A1 and A2′, for $t$ large,

$$\sup_{0\le h\le T}\|X(t+h)-\Phi_h(X(t))\|\le C(T)\Big[\Delta(t-1,T+1)+\sup_{t\le s\le t+T}\bar\gamma(s)\Big],$$

with $C(T)$ depending only on $T$ and on $F$ (through its Lipschitz constant and bound on the neighbourhood).

Significance

Proposition 4.1 separates the dynamics of a stochastic approximation algorithm from its noise. Any noise condition implying A1 almost surely (Propositions 4.2 and 4.4 of the notes for $L^q$-bounded and subgaussian martingale differences) combines with it to give: almost every sample path, after interpolation, is an asymptotic pseudotrajectory of $\dot x=F(x)$. The limit set theorem (Theorem 5.7: limit sets are internally chain transitive), the Lyapunov-function criterion (Proposition 6.4) and the attractor results (Section 7) then apply path by path. Estimate (11) gives the quantitative version used for rates.

The result is proved in the notes, building on Benaïm and Hirsch (1996). No machine-checked proof of it, or of the asymptotic pseudotrajectory framework, is known to exist. A formal proof would supply a checked bridge between discrete recursions with step sizes and flows of vector fields, which every ODE-method convergence proof crosses.

Difficulty

The obvious argument compares $X$ directly with the flow by Gronwall's inequality. It needs $F$ Lipschitz along both the interpolated path and the flow line, which holds under A2′ but not under A2, where $F$ is only continuous and solutions are unique without any Lipschitz bound. Under A2 the comparison must go through compactness instead: equicontinuity of the translates, identification of every limit point as an integral curve, and uniqueness of integral curves. The last step is where global integrability is used, and it cannot be replaced by a quantitative estimate.

Under A2′ the iterates may be unbounded, so no compactness is available, and the path and the flow line must be kept inside the region where $F$ is controlled for the whole window $[t,t+T]$.

Formalization scope

• Space $\mathbb R^d$ is EuclideanSpace ℝ (Fin d); time is ℝ≥0 for the pseudotrajectory and ℝ inside integrals. Sequences are ℕ → · with the paper's indices; $\gamma_0$ and $U_0$ are unused.
• $m(t)$ is the largest $k$ with $\tau_k\le t$, so the divisor $\gamma_{m(t)+1}$ is positive even when some steps vanish.
• Limits are written with $\varepsilon$; the suprema that remain ($\Delta$, $\sup\bar\gamma$) are over bounded nonempty sets, and $\overline U$ is a step function with finitely many pieces on bounded intervals, so no integral or supremum takes a default value.
• The flow of $F$ is a function satisfying the integral-curve property, together with global integrability (existence and uniqueness of integral curves on $\mathbb R$); continuity of the flow is not assumed.
• A2′ is read with a uniform neighbourhood: $F$ is Lipschitz and bounded on $\{y:\operatorname{dist}(y,\{x_n\})<r\}$ for some $r>0$. Under the reading "some open set containing $\{x_n\}$" the proposition fails for unbounded iterates.
• Theorem 3.2 is stated for flows on $C^0(\mathbb R,M)$ (compact-open topology); for semiflows with the convention $\Phi^p(t)=p$ for $t<0$, the implication (i)⇒(ii) is false as printed.

Trivializing formalizations are ruled out: the goal keeps both alternatives A2 and A2′ (neither a global Lipschitz condition nor bounded iterates is assumed in place of the disjunction), $X$ is the explicit piecewise affine interpolation rather than any curve with the desired property, and the constant in (11) is fixed before the sequences, so it cannot depend on the run.

A complete development needs Gronwall's inequality (in Mathlib), Arzelà–Ascoli on $C^0(\mathbb R,M)$, continuous dependence of solutions on initial data under uniqueness (Kamke's theorem, not in Mathlib), and interval integrals of step functions. The asymptotic pseudotrajectory definitions and Theorem 3.2 are reusable for the other missions on these notes. Proofs of individual milestones are welcome; Eq. (9) and the comparison of $X$ and $\overline X$ are the natural entry points.

Selected references

• M. Benaïm, Dynamics of stochastic approximation algorithms, Séminaire de Probabilités XXXIII, Lecture Notes in Math. 1709, Springer, 1999, pp. 1–68. https://doi.org/10.1007/BFb0096509
• M. Benaïm and M. W. Hirsch, Asymptotic pseudotrajectories and chain recurrent flows, with applications, J. Dynam. Differential Equations 8 (1996), 141–176. https://doi.org/10.1007/BF02218617
• M. Métivier and P. Priouret, Théorèmes de convergence presque sûre pour une classe d'algorithmes stochastiques à pas décroissant, Probab. Theory Related Fields 74 (1987), 403–428. https://doi.org/10.1007/BF00699098
• H. J. Kushner and G. G. Yin, Stochastic Approximation Algorithms and Applications, Springer, 1997. https://doi.org/10.1007/978-1-4899-2696-8
• L. Ljung, Analysis of recursive stochastic algorithms, IEEE Trans. Automat. Control 22 (1977), 551–575. https://doi.org/10.1109/TAC.1977.1101561

Motivation

In a Walrasian pure exchange economy, agents trade a fixed stock of $l$ commodities, and a price vector $p\in\mathbb R^l$ is a general equilibrium when aggregate excess demand vanishes. Existence of equilibrium (Arrow–Debreu, 1954) says nothing about how prices reach it. The classical tâtonnement model of Samuelson (1947), $dp_i/ds = c_i Z_i(p)$, is not derived from any optimization principle, and Scarf (1960) gave economies in which it is not globally stable; see also Smale's survey Dynamics in General Equilibrium Theory (JSTOR 1817235) and the chaotic tâtonnement examples of Bala–Majumdar (JSTOR 25054664).

Lindgren (doi:10.3390/analytics1010003) proposes instead that the economy as a whole chooses a price path by dynamic programming: it minimizes a running cost combining a quadratic transaction cost for price changes and the agents' aggregate minimal expenditure. From the resulting Hamilton–Jacobi–Bellman (HJB) equation the paper derives an evolution equation for the price velocity and a condition under which the value function acts as a Lyapunov function: the equilibrium is approached when price adjustments are large enough. This mission formalizes those derivations.

Setting

There are $l$ commodities and $n$ agents. Prices are vectors $p=(p_1,\dots,p_l)\in\mathbb R^l$, and the paper's implicit summation $x^iy_i=\sum_{i=1}^l x_iy_i$ is written $\langle x,y\rangle$. Agent $j$ has an expenditure function $e_j(p)$ (minimal cost of reaching a fixed utility level), and the market weighs agents with constants $\lambda_j>0$; the aggregate expenditure is

$$E(p)=\lambda^je_j(p)=\sum_{j=1}^n\lambda_je_j(p).$$

The economy controls the price velocity $v=dp/ds$ and minimizes the cost functional (eq. (7))

$$\int_t^T\Big(\tfrac12 m\langle v,v\rangle+E(p)\Big)\,ds,\qquad m>0,$$

whose value function is $J(t,p)$. The Hamiltonian (eq. (8)) is

$$H(v)=\tfrac12 m\langle v,v\rangle+E(p)+\langle\nabla J,v\rangle ,$$

the optimal policy (eq. (9)) is $v=-\tfrac1m\nabla J$, and the HJB equation (eq. (10)) reads

$$\frac{\partial J}{\partial t}=\frac1{2m}\langle\nabla J,\nabla J\rangle-E(p).$$

Here $\nabla$ always denotes the gradient with respect to prices. Shephard's lemma identifies the Hicksian demand of agent $j$ with $h^j=\nabla e_j$. For the stability analysis the paper runs time forward, which reverses the sign of the HJB equation: $\partial J/\partial s=-\frac1{2m}\langle\nabla J,\nabla J\rangle+E(p)$.

Formalization targets

Goal — Lyapunov stability condition (Section 3)

If $J$ is $C^1$ and solves the time-reversed HJB equation, and the price path follows the optimal policy $\dot p(s)=v(s)=-\frac1m\nabla J(s,p(s))$, then on any interval $[t,T]$ on which

$$E(p(s))<\tfrac32\,m\,\langle v(s),v(s)\rangle,$$

the function $s\mapsto J(s,p(s))$ is strictly decreasing; if moreover $J(T,p(T))=0$, it is strictly positive on $[t,T)$.

Milestones

1. Eq. (4): under the normalization $\langle p,p\rangle=1$, $\langle p,\dot p\rangle=0$.
2. Eq. (9): for $m>0$, $v$ minimizes $H$ if and only if $mv=-\nabla J$.
3. Eq. (10): the HJB equation $-\partial_tJ=\min_vH$ takes the explicit form above.
4. Eq. (12): for a $C^2$ solution of (10), $v=-\frac1m\nabla J$ satisfies

$$m\frac{\partial v_i}{\partial t}+\tfrac12 m\,\nabla_i\langle v,v\rangle=\nabla_iE .$$

5. Eq. (14): with Shephard's lemma, the right-hand side becomes $\sum_j\lambda_jh^j_i$.
6. Eq. (19): along the optimal path, $\dfrac{dJ}{ds}=E(p)-\tfrac32 m\langle v,v\rangle$.

Significance

The paper's contribution is the claim that price dynamics derived from an optimization principle are nonlinear and only conditionally stable, with stability requiring sufficiently fast price changes; the author connects this to volatility clustering in financial time series. The derivations in the paper are formal calculations with the regularity of $J$ left implicit. Formalizing them pins down exactly which smoothness assumptions each step needs (for instance, eq. (12) uses equality of mixed partial derivatives, hence a $C^2$ value function), and which facts are imported from outside (the HJB equation itself, Shephard's lemma). The resulting statements are reusable calculus facts about HJB equations with quadratic control cost.

Difficulty

Each step is a short computation on paper; the formal difficulty is in the calculus infrastructure: partial derivatives of functions on $\mathbb R\times\mathbb R^l$, symmetry of second derivatives, the chain rule along a curve, and turning a pointwise negative derivative into strict monotonicity on a closed interval. The HJB equation is taken as a hypothesis on $J$ rather than derived from the definition of the value function, because the paper asserts it without proof and a rigorous derivation would require viscosity-solution theory.

Formalization scope

All declarations live in the namespace LindgrenPriceDynamics. Prices are functions Fin l → ℝ; partial derivatives are Fréchet derivatives applied to standard basis vectors, and time derivatives are one-variable derivatives in the time argument. The value function is a function J : ℝ → (Fin l → ℝ) → ℝ whose joint regularity is stated for the uncurried map on ℝ × (Fin l → ℝ). The standing assumption $m>0$ is kept; positivity of $\lambda_j$ and $e_j$ is not needed by any stated conclusion and is not imposed. Prices are not restricted to the positive orthant. The goal's large-velocity hypothesis is satisfiable (e.g. $l=1$, $J=ap^2+cs$, $E=2a^2p^2/m+c$ with small $c>0$ on a bounded interval), so the goal is not vacuous.

Selected references

• J. Lindgren, General Equilibrium with Price Adjustments — A Dynamic Programming Approach, Analytics 1 (2022) 27–34. https://doi.org/10.3390/analytics1010003
• S. Smale, Dynamics in General Equilibrium Theory, American Economic Review 66 (1976) 288–294. https://www.jstor.org/stable/1817235
• H. Scarf, Some Examples of Global Instability of the Competitive Equilibrium, International Economic Review 1 (1960) 157–172.
• A. Mas-Colell, M. Whinston, J. Green, Microeconomic Theory, Oxford University Press, 1995.
• V. Bala, M. Majumdar, Chaotic Tatonnement, Economic Theory 2 (1992) 437–445. https://www.jstor.org/stable/25054664

Motivation

The cosmological constant $\Lambda$ entered physics in 1917, when Einstein added a term $\Lambda g_{\mu\nu}$ to his field equations in order to allow a spatially homogeneous universe that neither expands nor contracts (Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, 1917). The resulting Einstein static universe is the unique balance in which the attraction of pressureless matter, the repulsion carried by $\Lambda$, and a positive spatial curvature cancel exactly. Two facts about that balance shaped the next century of cosmology:

1. it is possible only for one specific relation between $\Lambda$, the matter density and the curvature, so the static model is fine-tuned by construction;
2. it is unstable: an arbitrarily small increase of the scale factor grows, and an arbitrarily small decrease collapses.

After Hubble's 1929 observations Einstein dropped the term; it returned in 1998, when the supernova measurements of the Supernova Cosmology Project and the High-$z$ Supernova Search Team required $\Lambda>0$. Interpreting $\Lambda$ as a vacuum energy density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ with equation of state $w=-1$ then produced the cosmological constant problem: the measured value, about $10^{-52}\,\mathrm{m}^{-2}$, is roughly $10^{-122}$ in Planck units, tens of orders of magnitude below the scale that effective quantum field theory suggests (Wikipedia, Cosmological constant problem).

This mission formalizes the classical ordinary-differential-equation content of that story: the static solution, its uniqueness, its instability, the vacuum-energy reading of $\Lambda$, the density-parameter bookkeeping, and the numerical size of the discrepancy.

Setting

A homogeneous isotropic universe is described by a positive scale factor $a:I\to\mathbb{R}$ on a set of times $I\subseteq\mathbb{R}$. Matter is pressureless dust, whose density dilutes with volume,

$$\rho(a)=\rho_0\left(\frac{a_0}{a}\right)^{3},$$

where $\rho_0>0$ and $a_0>0$ are reference values. Units are geometrized, $c=1$, so $\Lambda$ has dimension (length)$^{-2}$; $G>0$ is Newton's constant and $k\in\mathbb{R}$ the curvature constant.

The dynamics are the two Friedmann equations. The first Friedmann equation is the constraint

$$\dot a(t)^2=\frac{8\pi G}{3}\,\rho\big(a(t)\big)\,a(t)^2-k+\frac{\Lambda}{3}a(t)^2 ,\qquad t\in I,$$

and the acceleration equation for dust is

$$\ddot a(t)=F\big(a(t)\big),\qquad F(x):=-\frac{4\pi G}{3}\,\rho(x)\,x+\frac{\Lambda}{3}x=-\frac{4\pi G}{3}\frac{\rho_0a_0^3}{x^{2}}+\frac{\Lambda}{3}x .$$

The Hubble parameter is $H=\dot a/a$, the critical density is $\rho_c=3H^2/(8\pi G)$, and the density parameters are

$$\Omega_m=\frac{\rho}{\rho_c},\qquad \Omega_\Lambda=\frac{\Lambda}{3H^2},\qquad \Omega_k=-\frac{k}{a^2H^2}.$$

Formalization targets

Goal — the static universe exists for exactly one balance, and it is unstable

For $G,\rho_0,a_0,a_E>0$, the constant function $a\equiv a_E$ satisfies both Friedmann equations if and only if

$$\Lambda=4\pi G\,\rho(a_E)\qquad\text{and}\qquad k=\Lambda a_E^{2},$$

in which case $\Lambda>0$, $F(a_E)=0$, $F'(a_E)=\Lambda>0$, and the equilibrium is unstable in the following exact sense: every solution of $\ddot a=F(a)$ on $[0,\infty)$ with $a(0)>a_E$ and $\dot a(0)\ge 0$ is strictly increasing and satisfies $a(t)\to\infty$; and every positive solution on $[0,T]$ with $a(0)<a_E$ and $\dot a(0)\le 0$ is strictly decreasing.

Supporting targets

$\Lambda$ is exactly a perfect fluid of constant density $\rho_{\text{vac}}=\Lambda/(8\pi G)$ and pressure $p_{\text{vac}}=-\rho_{\text{vac}}$; the density parameters satisfy $\Omega_m+\Omega_k+\Omega_\Lambda=1$; the acceleration equation is a consequence of the first Friedmann equation along a solution with $\dot a\ne0$; and the observed $\Lambda$ is smaller than $10^{-120}$ in Planck units.

Significance

The static solution is the historical origin of $\Lambda$, and its instability is the reason the static model was never a viable cosmology even before the expansion was observed: the balance point is a local maximum of the effective potential, not a minimum, so the equilibrium cannot be maintained. The same function $F$ and the same linearization $\ddot\delta=\Lambda\,\delta$ govern the late-time behaviour of the standard $\Lambda$CDM model, where the growing mode becomes the de Sitter expansion $e^{\sqrt{\Lambda/3}\,t}$.

What the mission produces on top of the textbook statements: a machine-checked ODE treatment of a dust-plus-$\Lambda$ cosmology that does not stop at the linearized equation. The classical physics argument computes $F'(a_E)=\Lambda$ and calls the equilibrium unstable; the formal statements here ask for the nonlinear conclusion — monotone escape to infinity on one side and strict collapse on the other — which is what "unstable" has to mean for the exact equations. Mathlib contains neither the Friedmann equations nor a general instability criterion for second-order autonomous scalar ODEs, so both have to be built here.

Difficulty

The linearized step is routine calculus. The nonlinear instability is not: from $\ddot a=F(a)$ with $F(a_E)=0$ and $F$ strictly increasing on $(0,\infty)$, one must run a bootstrapping argument in which the sign of $\ddot a$ controls $\dot a$, which in turn controls whether $a$ stays in the region where the sign of $\ddot a$ was known. The obvious approach — solve the ODE explicitly — is not available: the dust-plus-$\Lambda$ equation with the static value of $k$ has no elementary closed-form solution through the static point, and the first Friedmann equation, which is the conserved energy of the second, degenerates exactly at $a=a_E$, where $\dot a=0$. Divergence $a(t)\to\infty$ additionally requires ruling out that $\dot a$ stalls, i.e. a quantitative lower bound on $\dot a$ once the solution has left a neighbourhood of $a_E$.

Formalization scope

Everything is stated for real-valued functions $a:\mathbb{R}\to\mathbb{R}$ of a real time variable; derivatives are the usual derivative of a real function, and each equation is asserted pointwise on an explicit set of times ($\mathbb{R}$, $[0,\infty)$, $[0,T]$, or a general open set), never globally by fiat. Dust density, the Friedmann equations, the acceleration function $F$, the Hubble parameter, the critical density and the three density parameters are all fixed in one definition file shared by every statement, so all items commit to the same conventions: $c=1$, curvature entering as $-k$ in the equation for $\dot a^2$, and $\rho_0,a_0$ as fixed reference constants rather than the value of the density at a particular time.

Two trivializing readings are ruled out explicitly. First, the contracting-side statement is posed on a bounded interval $[0,T]$ with positivity of $a$ assumed there, because a collapsing solution reaches $a=0$ in finite time; posing it on $[0,\infty)$ would make its hypotheses unsatisfiable and the statement vacuous. Second, the escape statement asks for $a(t)\to\infty$, not merely $\dot a\ge0$, so it cannot be satisfied by a solution that converges to a finite limit.

Useful contributions beyond the listed items: a reusable instability criterion for $\ddot x=F(x)$ at a zero of $F$ with $F'>0$, and the corresponding stability criterion, both of which are independent of cosmology.

Selected references

• Wikipedia, Cosmological constant. https://en.wikipedia.org/wiki/Cosmological_constant
• Wikipedia, Cosmological constant problem. https://en.wikipedia.org/wiki/Cosmological_constant_problem
• A. Einstein, Kosmologische Betrachtungen zur allgemeinen Relativitätstheorie, Sitzungsberichte der Preussischen Akademie der Wissenschaften, 1917.
• S. Weinberg, The cosmological constant problem, Reviews of Modern Physics 61 (1989) 1. https://doi.org/10.1103/RevModPhys.61.1
• J. Martin, Everything you always wanted to know about the cosmological constant problem (but were afraid to ask), Comptes Rendus Physique 13 (2012) 566. https://doi.org/10.1016/j.crhy.2012.04.008

Motivation

A coupling constant is the number that fixes the strength of an interaction: it is the coefficient that multiplies the interaction term of a Lagrangian relative to its kinetic term, and in a perturbative treatment it is the parameter the expansion is organised in. The central structural fact about such a coupling in a quantum field theory is that it is not constant: once quantum corrections are resummed, the coupling depends on the energy scale $\mu$ at which the theory is probed. This scale dependence — the running of the coupling — is what distinguishes quantum electrodynamics, whose coupling grows with energy until perturbation theory breaks down (the Landau pole), from quantum chromodynamics, whose coupling decreases logarithmically at high energy (asymptotic freedom, Gross–Politzer–Wilczek, Nobel Prize in Physics 2004).

This mission formalizes the elementary mathematics behind those statements: the one-loop renormalization-group equation, its exact solution, and the two qualitatively different behaviours it produces depending on the sign of the one-loop coefficient. The source is the Wikipedia article Coupling constant (sections Beta functions, QED and the Landau pole, QCD and asymptotic freedom), which states these facts in prose and in the single displayed formula for the running QCD coupling.

Setting

Write $g$ for a single real coupling and $t = \log \mu$ for the logarithm of the energy scale. The beta function is defined by

$$\frac{dg}{dt} \;=\; \mu \frac{dg}{d\mu} \;=\; \beta(g),$$

and at one loop $\beta$ is a cubic monomial,

$$\beta(g) \;=\; b\,g^{3},$$

with a scheme- and theory-dependent real coefficient $b$. Saying that $g$ runs at one loop on a set of scales $S$ means that $g$ is differentiable at every $t \in S$ with $g'(t) = b\,g(t)^{3}$.

For QCD the article records the one-loop form of the strong coupling directly in terms of the process energy $Q$ and the QCD scale $\Lambda$:

$$\alpha(Q) \;=\; \frac{1}{\beta_0 \,\log\!\big(Q^{2}/\Lambda^{2}\big)},\qquad \beta_0>0,\ \Lambda>0 .$$

Target

The goal theorem is the dichotomy governed by the sign of $b$, for an initial condition $g(0) = g_0 > 0$ at the reference scale $t = 0$:

1. Asymptotic freedom ($b < 0$). Every solution on $[0,\infty)$ satisfies

$$\lim_{t\to\infty} g(t) = 0, \qquad \lim_{t\to\infty} 2|b|\,t\,g(t)^{2} = 1,$$

i.e. $g(t)^{2} \sim 1/(2|b|\log\mu)$: the coupling dies off logarithmically in the energy.

2. Landau pole ($b > 0$). No solution exists on the whole closed interval

$$\Big[\,0,\ \frac{1}{2\,b\,g_0^{2}}\,\Big];$$

the flow cannot be continued up to the finite scale $t_\ast = 1/(2bg_0^{2})$, which is the Landau pole of the one-loop approximation.

Both follow from the exact one-loop solution, which is itself a milestone:

$$g(t)^{2}\,\big(1 - 2b\,g_0^{2}\,t\big) \;=\; g_0^{2}.$$

Significance

The dichotomy above is the mathematical content of the two headline claims made about running couplings: that a positive one-loop coefficient drives the coupling to infinity at a finite energy, and that a negative one makes it vanish logarithmically at high energy. The milestones also isolate the statement that a vanishing beta function means the coupling does not run at all (scale invariance), and record the elementary analytic properties of the explicit QCD formula $\alpha(Q) = 1/(\beta_0\log(Q^2/\Lambda^2))$: it is strictly decreasing above $\Lambda$, tends to $0$ as $Q\to\infty$, and satisfies the one-loop flow equation $d\alpha/dQ = -(2/Q)\,\beta_0\,\alpha^{2}$.

Nothing here is open mathematics: these are exercises in the theory of a separable scalar ODE. What the mission produces is a machine-checked, reusable Lean development of the one-loop renormalization-group flow — a small piece of formalized physics infrastructure that later missions on renormalization or dimensional transmutation can import.

Difficulty

The only real subtlety is that the exact solution is obtained by differentiating $t \mapsto g(t)^{-2}$, which requires knowing in advance that the solution never vanishes. Positivity is not assumed: it is a separate milestone, and must be derived from the initial condition together with the flow equation (if $g$ reached $0$ at a first time $t_1$, the identity $g(t)^{-2} = g_0^{-2} - 2bt$ on $[0,t_1)$ forces $g(t_1)^2$ to have a strictly positive limit). The Landau-pole statement is a non-existence claim and has no analytic content beyond this, but it does depend on the positivity step.

Formalization scope

Scales are parametrised logarithmically: the independent variable is $t = \log\mu \in \mathbb{R}$, the coupling is a function $g : \mathbb{R} \to \mathbb{R}$, and the flow hypothesis is imposed pointwise as a two-sided derivative at each point of the given set (at an endpoint of a closed interval this is slightly stronger than a one-sided derivative, which only strengthens the hypotheses of the positive results and weakens the non-existence claim — the Landau pole statement is therefore the conservative reading). No uniqueness or existence theory for ODEs is assumed; the statements quantify over arbitrary functions satisfying the flow equation. The QCD formula is taken with real arguments and no constraint tying $\beta_0$ or $\Lambda$ to a particular number of flavours; the numerical values quoted in the source ($\alpha_s(M_Z^2) = 0.1179 \pm 0.0010$, $\Lambda \approx 332$ MeV) are measurements and are deliberately not formalized.

Degenerate cases are visible in the statements rather than hidden: $b = 0$ appears as its own milestone (constant coupling), and the value of $\alpha(Q)$ for $Q \le \Lambda$, where the logarithm is non-positive or zero, is never asserted.

Selected references

• Coupling constant, Wikipedia, revision 1354339557, https://en.wikipedia.org/w/index.php?title=Coupling_constant&oldid=1354339557
• A. Deur, S. J. Brodsky, G. F. de Téramond, "The QCD running coupling", Progress in Particle and Nuclear Physics 90 (2016) 1–74, https://arxiv.org/abs/1604.08082
• Particle Data Group (P. A. Zyla et al.), "Review of Particle Physics — Quantum Chromodynamics", PTEP 2020 (8), https://doi.org/10.1093/ptep/ptaa104

Motivation

Roughly half of the stars in our galaxy belong to binary star systems: pairs of stars close enough to each other that their mutual gravitational attraction dominates every other influence, and far enough from every other star that the rest of the galaxy can be ignored. Such a pair is the cleanest physical realization of the Newtonian two-body problem, and it is the reason the two-body problem is not merely a textbook exercise: the masses of stars other than the Sun are known almost entirely because binaries can be observed, and the observation is converted into a mass by exactly the chain of reasoning formalized in this mission.

This mission formalizes Section 4.16, "Binary star systems", of Richard Fitzpatrick's Celestial Mechanics lecture notes (University of Texas at Austin), Eqs. (4.108)–(4.119). It is the first mission of a planned series on the same source; the whole series shares the Lean namespace CelestialMechanics.

Setting

Two point masses $m_1, m_2 > 0$ move in $\mathbb{R}^3$ under Newtonian gravity, with position vectors $\mathbf{r}_1(t)$ and $\mathbf{r}_2(t)$ defined for all times $t \in \mathbb{R}$. Write $\mathbf{r} = \mathbf{r}_2 - \mathbf{r}_1$ for the relative separation and $r = \lVert \mathbf{r} \rVert$ for the distance between the stars. The gravitational force the first star exerts on the second is Eq. (4.108),

$$\mathbf{f} = -\frac{G\,m_1 m_2}{r^{3}}\,\mathbf{r},$$

and Newton's second law for each star reads

$$m_1\,\ddot{\mathbf{r}}_1 = \frac{G\,m_1m_2}{r^{3}}\,\mathbf{r}, \qquad m_2\,\ddot{\mathbf{r}}_2 = -\frac{G\,m_1m_2}{r^{3}}\,\mathbf{r}.$$

A pair of twice continuously differentiable, never-colliding trajectories satisfying these two equations is what this mission calls a Newtonian gravitational two-body system.

Three derived objects organize the material. The center of mass is $\mathbf{R} = (m_1\mathbf{r}_1 + m_2\mathbf{r}_2)/(m_1+m_2)$. The relative Kepler problem with gravitational parameter $GM$, $M = m_1+m_2$, is the equation

$$\ddot{\mathbf{r}} = -\frac{G M}{r^{3}}\,\mathbf{r} \tag{4.110}$$

for a nowhere-vanishing curve $\mathbf{r}$. A Keplerian conic orbit with major radius $a$, eccentricity $e$ and angular momentum per unit reduced mass $h$ is a planar curve given in polar coordinates $(\rho, \theta)$ by

$$\mathbf{r} = (\rho\cos\theta,\ \rho\sin\theta,\ 0), \qquad \rho = \frac{a\,(1-e^{2})}{1+e\cos\theta}, \qquad \dot\theta = \frac{h}{\rho^{2}},$$

which are Eqs. (4.112)–(4.114); the elements are tied together by Eq. (4.115), $a = h^{2}/\bigl((1-e^{2})GM\bigr)$.

Target

The goal theorem is an existence-and-description statement: for every $G>0$, every pair of masses $m_1,m_2>0$ and every choice of orbital elements $a>0$, $0 \le e < 1$, there exist trajectories $\mathbf{r}_1, \mathbf{r}_2$, polar functions $\rho, \theta$ and a time $T>0$ such that

$$\text{(i) } \mathbf{r}_1, \mathbf{r}_2 \text{ solve the two-body equations above}; \qquad \text{(ii) } m_1\mathbf{r}_1 + m_2\mathbf{r}_2 = \mathbf{0};$$ $$\text{(iii) } \mathbf{r}_2 - \mathbf{r}_1 \text{ is the Keplerian conic with elements } (a, e, h), \quad h = \sqrt{(1-e^{2})\,G\,(m_1+m_2)\,a};$$ $$\text{(iv) } \mathbf{r}_1 = -\frac{m_2}{m_1+m_2}\,\mathbf{r}, \quad \mathbf{r}_2 = \frac{m_1}{m_1+m_2}\,\mathbf{r}; \qquad \text{(v) } T = \sqrt{\frac{4\pi^{2}a^{3}}{G(m_1+m_2)}} \text{ and both orbits are } T\text{-periodic}.$$

The milestones are the individual steps of Section 4.16, ordered as in the source: the reduction of the two-body system to the one-body problem (4.110)–(4.111); the uniform motion of the center of mass, which makes the center-of-mass frame inertial; the positions of the two stars in that frame (4.118)–(4.119); the verification that the conic (4.112)–(4.115) solves (4.110); the period of revolution (4.116)–(4.117); and the inversion of these relations that yields the two stellar masses from observation.

Significance

The result itself. The theorem is the complete qualitative and quantitative picture of a binary orbit: each star traverses an ellipse about the common center of mass, the two stars are diametrically opposite one another at every instant, the distances from the center of mass are in the fixed ratio $m_2 : m_1$, and the period depends only on the major radius and the total mass. The last two facts are what astronomers use: the measured pair $(a, T)$ gives the mass sum $m_1 + m_2 = 4\pi^{2}a^{3}/(GT^{2})$, the observed ratio of the two apparent orbits gives $m_1/m_2$, and sum plus ratio give the individual masses. The same reduction also supplies the finite-mass correction to one-body solar-system orbit theory, in which $G M_{\odot}$ is replaced by $G(M_{\odot} + m)$.

Formalizing it. The mathematics has been settled since Newton, so the contribution here is a machine-checked development rather than a new result. Mathlib currently has extensive analysis infrastructure — iterated derivatives, ContDiff, Euclidean spaces — but no development of the Kepler problem: neither the conic solution of the inverse-square equation of motion nor Kepler's laws. The reusable output of this mission is therefore a small, self-contained Kepler library: the two-body reduction, the conic solution, and the period law, stated for curves in $\mathbb{R}^3$ in a form that later missions in the series (perturbations, orbital elements, the restricted three-body problem) can import unchanged.

Difficulty

Two milestones carry essentially all of the analytic work.

The first is showing that the conic really solves (4.110). The obvious route — differentiate $\rho(t)$ twice and simplify — runs into the fact that $\rho$ is given as a function of $\theta(t)$ and $\theta$ is given only implicitly, through the angular-momentum law $\dot\theta = h/\rho^{2}$. Even the regularity in the conclusion has to be earned: the hypotheses supply only differentiability of $\theta$, and twice-continuous differentiability of the curve must be bootstrapped from the two polar equations. Getting the Cartesian second derivative into the form $-(GM/\rho^{3})\mathbf{r}$ requires the relation $h^{2} = (1-e^{2})GMa$ at exactly the right place, and this is where a sign or a factor typically goes wrong.

The second is the goal theorem, which is an existence statement and therefore needs the angular equation $\dot\theta = h/\rho(\theta)^{2}$ to be solved globally in time, on all of $\mathbb{R}$ and not merely on a small interval. The right-hand side is smooth and, for $0 \le e < 1$, bounded above and below by positive constants, so the solution exists for all time and advances by $2\pi$ in a fixed time $T$; but "exists for all time" is a real obligation in Lean, and a naive appeal to a local existence theorem does not discharge it.

Formalization scope

Space is EuclideanSpace ℝ (Fin 3), so the norm is the Euclidean one and the three Cartesian components are indexed $0, 1, 2$; the orbital plane is fixed to be the $x$-$y$ plane, exactly as in Eq. (4.112). Trajectories are total functions $\mathbb{R} \to \mathbb{R}^3$: all statements are global in time, and no restriction to an interval or to positive times is made. Derivatives are iteratedDeriv, and smoothness is ContDiff ℝ 2. Masses and $G$ are positive reals wherever the physics needs it, and this is stated explicitly rather than left implicit. Eccentricity is restricted to $0 \le e < 1$ throughout, so only bound (elliptical and circular) orbits are in scope; the parabolic and hyperbolic cases of Sections 4.13–4.15 are left to later missions.

Two trivializing formalizations are ruled out by construction. The definitions never allow the separation to vanish, so no statement is satisfied by a collision; and in the goal theorem the angular momentum $h$ and the period $T$ are not existentially quantified but pinned to their Keplerian values in terms of $(G, m_1+m_2, a, e)$, so the orbit cannot be rescaled to make the conditions easy to meet.

Contributions of independent interest are welcome: conservation of angular momentum and of energy for (4.110), the equal-areas law, the eccentricity (Laplace–Runge–Lenz) vector, and the Kepler equation relating mean and eccentric anomaly all sit naturally on top of this development.

Selected references

• Richard Fitzpatrick, Celestial Mechanics, University of Texas at Austin lecture notes, Chapter 4 "Keplerian orbits", Section 4.16 "Binary star systems", https://farside.ph.utexas.edu/teaching/celestial/Celestial/node38.html. The source of this mission; Eqs. (4.108)–(4.119).
• Isaac Newton, Philosophiæ Naturalis Principia Mathematica, 1687. Book I contains the original solution of the inverse-square two-body problem.

Motivation

In 1964 A. N. Sarkovskii proved a theorem about continuous maps of the real line that is remarkable both for how little it assumes — continuity, nothing more — and for how much it concludes: the set of periods of the periodic orbits of such a map is completely constrained by a single linear ordering of the positive integers. Its best-known corollary, rediscovered by Li and Yorke in 1975 under the slogan period three implies chaos, says that a continuous map of $\mathbb{R}$ with an orbit of period three has orbits of every period.

Devaney presents the theorem in §1.10 of An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003), calling it the chapter's first major theorem, and gives the elementary proof of Block, Guckenheimer, Misiurewicz and Young based on interval covering relations. This mission is the second in a series formalizing the book; it is independent of the first, sharing only the book-wide namespace.

Timeline: Sarkovskii (1964) proved the full ordering theorem, in Ukrainian, and it went largely unnoticed in the West; Li and Yorke (1975) independently proved the period-three case and gave the field the word "chaos"; Štefan (1977) and Block–Guckenheimer–Misiurewicz–Young (1980) gave the short interval-covering proofs, the latter being the one Devaney reproduces.

Setting

Let $f : \mathbb{R} \to \mathbb{R}$ be continuous. A point $x$ has prime period $n \ge 1$ if $f^{n}(x) = x$ and $f^{m}(x) \ne x$ for every $0 < m < n$.

The Sarkovskii ordering of the positive integers is

$$3 \,\triangleright\, 5 \,\triangleright\, 7 \,\triangleright\, \cdots \,\triangleright\, 2\cdot 3 \,\triangleright\, 2\cdot 5 \,\triangleright\, \cdots \,\triangleright\, 2^2\cdot 3 \,\triangleright\, 2^2 \cdot 5 \,\triangleright\, \cdots \,\triangleright\, 2^3 \,\triangleright\, 2^2 \,\triangleright\, 2 \,\triangleright\, 1 :$$

first the odd numbers greater than one in increasing order, then $2$ times the odds, then $2^2$ times the odds, and so on; the powers of two come last, in decreasing order. Writing $k = 2^{a}p$ and $\ell = 2^{b}q$ with $p, q$ odd, $k \triangleright \ell$ holds exactly when either $p, q > 1$ and $(a,p)$ precedes $(b,q)$ lexicographically, or $p > 1$ and $q = 1$, or $p = q = 1$ and $b < a$.

Two elementary facts drive the proof. If $I$ is a closed interval with $f(I) \supseteq I$, then $f$ has a fixed point in $I$; and if closed intervals satisfy $f(A_i) \supseteq A_{i+1}$ for $i < n$, then some point of $A_0$ has $f^{i}(x) \in A_i$ for all $i \le n$. One writes $I \to J$, "$f(I)$ covers $J$", for $J \subseteq f(I)$.

Target

The goal is Devaney's Theorem 10.2: for continuous $f : \mathbb{R} \to \mathbb{R}$,

$$\text{if } f \text{ has a point of prime period } k \text{ and } k \triangleright \ell, \text{ then } f \text{ has a point of prime period } \ell .$$

The milestones are the steps of the book's proof: the two covering observations, the period-three special case (Theorem 10.1), the odd case, the power-of-two case and the mixed case $p \cdot 2^m$ into which the general theorem is decomposed, the remark that a period which is not a power of two forces infinitely many periodic points, and the converse direction, witnessed by the piecewise-linear map with a period-five orbit and no period-three orbit.

Significance

Sarkovskii's theorem is the sharpest general statement known about the period structure of one-dimensional dynamics, and it is sharp in both directions: the ordering is realized, so no stronger implication holds. Its first consequence — only powers of two can occur as the set of periods of a map with finitely many periodic points — is what makes the period-doubling cascade the canonical route to chaos, a theme the book returns to in §1.17.

The theorem is emphatically one-dimensional: it fails on the circle, where a rotation by $120^\circ$ has every point of period three and no other period.

Formalizing it contributes a reusable Lean treatment of interval covering relations and of the Sarkovskii ordering itself; we are not aware of these in Mathlib at the pinned revision, and the covering machinery is exactly what §1.13 and §1.16 of the book reuse.

Difficulty

The period-three case is a short argument once the covering observations are available, and it is a reasonable first milestone. The general theorem is not: the odd case requires choosing the right interval $I_1 = [x_i, x_{i+1}]$ on the orbit, building the increasing family of unions $O_\ell$ of covered intervals, and showing that the shortest return loop has length exactly $n-1$ — a combinatorial argument on the cyclic order of the orbit that is easy to draw and tedious to formalize. Attempts to shortcut the ordering with a naive induction on $n$ fail: the statement for $n$ genuinely depends on the geometric arrangement of the orbit points.

Formalization scope

1. Periodicity is prime period throughout: $f^n(x) = x$ together with minimality of $n$. The statements would be false or trivial with "period" read as "fixed by $f^n$".
2. The Sarkovskii relation is defined arithmetically, in terms of the $2$-adic valuation and the odd part of an integer, rather than as a listed order; it is a strict relation, so $k \triangleright k$ is false and the goal theorem says nothing about $\ell = k$ (which holds by hypothesis anyway).
3. $0$ is outside the ordering: the relation is false whenever either argument is $0$.
4. Intervals in the covering lemmas are closed intervals $[a,b]$ with $a \le b$, given by their endpoints; "covers" means containment of the interval in the image, $J \subseteq f(I)$.
5. The converse milestone asserts the existence of a continuous map with a period-five point and no period-three point; the book's witness is piecewise linear on $[1,5]$, but the statement does not prescribe it.

Selected references

• Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd edition, Westview Press, 2003 (ISBN 0-8133-4085-3) — §1.10, pp. 60–68. The mission's primary source.
• T. Y. Li and J. A. Yorke, Period three implies chaos, American Mathematical Monthly 82 (1975), 985–992, DOI: 10.1080/00029890.1975.11994008.
• L. Block, J. Guckenheimer, M. Misiurewicz, L. S. Young, Periodic points and topological entropy of one-dimensional maps, in Global Theory of Dynamical Systems, Lecture Notes in Mathematics 819, Springer, 1980, 18–34, DOI: 10.1007/BFb0086977 — the proof Devaney follows.

Audit note (provenance of the read-backs)

The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.

Every definition and statement in this proposal was compiled locally against this mission's environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files elaborate with no errors, the only warnings being the expected sorry placeholders in the theorem bodies.

Motivation

The word chaos entered mathematics with a precise meaning, and Robert L. Devaney's An Introduction to Chaotic Dynamical Systems (2nd edition, Westview Press, 2003) is the text that fixed the meaning now used in most of the literature: a map is chaotic when it is unpredictable (sensitive dependence on initial conditions), indecomposable (topological transitivity), and nevertheless regular (dense periodic points). The book develops this definition on the simplest possible object — the real quadratic family $F_\mu(x) = \mu x(1-x)$ on the unit interval — and shows that for large $\mu$ the map is chaotic on an invariant Cantor set, by exhibiting an exact symbolic model for it.

This mission is the first of a planned series formalizing the book. It covers §1.5–§1.8: the invariant set of the quadratic family, symbolic dynamics on the sequence space $\Sigma_2$, topological conjugacy, and Devaney's definition of chaos. Everything later in the book — Sarkovskii's theorem, the horseshoe, hyperbolic toral automorphisms, Julia sets — is written in the vocabulary fixed here, so a faithful Lean version of this chapter fixes the vocabulary of the whole series.

Setting

Write $I = [0,1]$ and let $F_\mu(x) = \mu x(1-x)$ for a real parameter $\mu$. Iterates are written $F_\mu^n$, with $F_\mu^0$ the identity.

For $\mu > 4$ the maximum value $\mu/4$ of $F_\mu$ exceeds $1$, so some points of $I$ leave $I$ after one iteration. Let

$$A_0 = \{x \in I : F_\mu(x) > 1\}, \qquad A_n = \{x \in I : F_\mu^{\,n}(x) \in A_0\},$$

so that $A_n$ is the set of points escaping from $I$ at the $(n+1)$-st iteration. The set of points that never escape is

$$\Lambda = I \setminus \bigcup_{n \ge 0} A_n = \{x : F_\mu^{\,n}(x) \in I \text{ for all } n \ge 0\}.$$

The complement $I \setminus A_0$ consists of two closed intervals, $I_0$ to the left of the midpoint $1/2$ and $I_1$ to its right.

On the symbolic side, $\Sigma_2$ is the set of one-sided infinite sequences $s = (s_0 s_1 s_2 \dots)$ with $s_i \in \{0,1\}$, metrized by

$$d[s,t] = \sum_{i=0}^{\infty} \frac{|s_i - t_i|}{2^i},$$

and $\sigma : \Sigma_2 \to \Sigma_2$ is the shift map $\sigma(s_0 s_1 s_2 \dots) = (s_1 s_2 s_3 \dots)$. The itinerary of $x \in \Lambda$ is the sequence $S(x) = (s_0 s_1 s_2 \dots)$ with $s_j = 0$ when $F_\mu^{\,j}(x) \in I_0$ and $s_j = 1$ when $F_\mu^{\,j}(x) \in I_1$.

Following Devaney, $f : J \to J$ is topologically transitive if for every pair of open sets $U, V$ meeting $J$ there is $k > 0$ with $f^k(U \cap J) \cap V \neq \emptyset$; it has sensitive dependence on initial conditions if there is $\delta > 0$ such that every point of $J$ has points of $J$ arbitrarily near it whose orbit eventually separates from its own by more than $\delta$; and it is chaotic on $J$ when it has sensitive dependence, is topologically transitive, and has a dense set of periodic points in $J$.

Target

The goal is Devaney's Example 8.8: for $\mu > 2 + \sqrt 5$,

$$F_\mu \text{ is chaotic on } \Lambda .$$

The milestones are the results the book uses to get there, in the book's own order: the escape of orbits outside $I$ (Proposition 5.2), the tame regime $1 < \mu < 3$ (Proposition 5.3), the Cantor structure of $\Lambda$ (Theorem 5.6), the metric and dynamics of the shift (Propositions 6.3, 6.5, 6.6), the itinerary conjugacy (Theorems 7.2, 7.3), its dynamical consequences (Theorem 7.5), sensitive dependence (Example 8.3), and the chaos of $F_4$ on all of $I$ (Example 8.9).

Significance

The theorem is the prototype for every later "chaos via symbolic dynamics" argument: the horseshoe, hyperbolic toral automorphisms, and the quadratic Julia sets are all proved chaotic by producing a conjugacy with a shift. The conjugacy also gives quantitative information that is otherwise inaccessible — for example, that $F_\mu$ has exactly $2^n$ points fixed by $F_\mu^{\,n}$, which no direct computation with the degree-$2^n$ polynomial delivers.

Formalizing it produces reusable Lean infrastructure that Mathlib currently lacks: Devaney's three chaos conditions, the sequence space $\Sigma_2$ with its metric and shift, topological conjugacy of maps on subsets, and the notion of a Cantor subset of the interval. These are the foundation the rest of the book's series will import.

Difficulty

The obvious route to the goal — analyze $F_\mu$ on $\Lambda$ directly — fails, because $\Lambda$ has no explicit description: it is a nested intersection of $2^{n+1}$ intervals whose endpoints are not available in closed form. The whole argument therefore goes through the itinerary map, and its two hard steps are: (i) surjectivity of the itinerary map, which needs the nested-interval construction $I_{s_0 \dots s_n} = I_{s_0} \cap F_\mu^{-1}(I_{s_1}) \cap \dots \cap F_\mu^{-n}(I_{s_n})$ together with the fact that these intervals are nonempty and nested; and (ii) injectivity, which needs the hyperbolicity estimate $|F_\mu'| > \lambda > 1$ on $I_0 \cup I_1$, valid exactly because $\mu > 2 + \sqrt 5$, and the mean value theorem. The hypothesis $\mu > 2 + \sqrt 5$ is not cosmetic: Devaney notes the results hold for $\mu > 4$, but only with a more delicate argument.

Formalization scope

The Lean development fixes the following conventions.

1. $\Lambda$ is defined as $\{x : \forall n,\ F_\mu^{\,n}(x) \in [0,1]\}$ — the points whose whole forward orbit stays in $I$ — rather than as a complement of the sets $A_n$; the two descriptions agree, and the definitional form makes invariance immediate. The sets $A_0, A_n, I_0, I_1$ are nonetheless defined, since the book's arguments refer to them.
2. The itinerary is defined as a total function of a real argument, taking entry $0$ at step $n$ when $F_\mu^{\,n}(x) \le 1/2$ and $1$ otherwise. On $\Lambda$ this agrees with Devaney's $I_0/I_1$ test, since the midpoint $1/2$ lies in the gap $A_0$ when $\mu > 4$.
3. $\Sigma_2$ carries Devaney's metric $d$ literally, as a summable series, not merely a topology; the metric space instance is part of the definitional layer, so Proposition 6.2 is not a separate milestone.
4. Sensitive dependence, transitivity, chaos and periodicity are stated for a map $f : X \to X$ of a metric space together with an invariant subset $J$, using open sets of the ambient space intersected with $J$; this avoids subtype bookkeeping while keeping the relative formulation of the book.
5. Cardinality claims ("$\operatorname{Per}_n$ has $2^n$ elements") are stated with Set.ncard and are restricted to $n > 0$; for $n = 0$ every point is fixed by $F^0$ and the claim would be false.
6. Nothing here is vacuous: the hypothesis $\mu > 2+\sqrt 5$ is satisfiable, $\Lambda$ is nonempty (it contains $0$), and the chaos predicate is a conjunction of three nontrivial conditions rather than a definitional abbreviation.

Contributions of any kind are welcome: full proofs, reductions splitting a milestone into lemmas, and reusable lemmas about $\Sigma_2$ or about conjugacy that later missions in the series can import.

Selected references

• Robert L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd edition, Westview Press, 2003 (ISBN 0-8133-4085-3) — §1.5 (pp. 31–38), §1.6 (pp. 39–43), §1.7 (pp. 44–47), §1.8 (pp. 49–52). The mission's primary and authoritative source.
• J. Banks, J. Brooks, G. Cairns, G. Davis, P. Stacey, On Devaney's definition of chaos, American Mathematical Monthly 99 (1992), 332–334, DOI: 10.1080/00029890.1992.11995856 — proves that transitivity plus dense periodic points already imply sensitive dependence.

Audit note (provenance of the read-backs)

The read-backs attached to every draft item in this proposal are not independent. They were written by the same agent that drafted the Lean statements, not by a separate auditor working blind from the code alone. They are included because they are still useful as a line-by-line rendering of each statement, but they are not independent testimony: any misreading baked into a formalization is likely repeated in its read-back, and agreement between the two should not be taken as confirmation of faithfulness. Each read-back repeats this warning in its own first paragraph. Reviewers who want independent testimony should commission fresh, blind read-backs.

Every definition and statement in this proposal was compiled locally against this mission's environment (Lean 4.33.1, Mathlib 0df444a360eaa60ab8c11dca51a86af692955474): all files elaborate with no errors, the only warnings being the expected sorry placeholders in the theorem bodies.