All missions

Motivation

The $(s, S)$ policy is the standard ordering rule for a single stocked item with a fixed charge per order: when the stock position falls below a reorder point $s$, order up to a level $S$; otherwise order nothing. Scarf (1960) proved that when the expected one-period cost is convex, some $(s, S)$ policy is optimal in every period of a finite-horizon model with set-up cost. Iglehart (1963) extended this to the infinite horizon. These results establish existence only. They give no procedure for finding the optimal pair.

Veinott and Wagner (1965) gave such a procedure. Its first step is to bound the optimal $s$ and $S$ by four integers $\underline{s} \le \bar{s} \le \underline{S} \le \bar{S}$ computed from the one-period cost alone. This reduces the search for an optimal policy to a finite box. Their Theorem 4(a) proves that the bounds hold for the first-period parameters of an optimal $(s, S)$ policy in every $n$-period model. This mission formalizes that theorem and the four comparison lemmas (Lemmas 2–5 of the paper's Appendix §2) from which the paper derives it.

Setting

Demands $\xi_1, \xi_2, \dots$ in periods $1, 2, \dots$ are independent, non-negative integer random variables with common distribution $\varphi(k) = \Pr(\xi_t = k)$ and finite mean. Unfilled demand is backlogged, so stock levels are arbitrary integers. In period $t$, $X_t$ is the stock on hand plus on order before ordering and $Y_t \ge X_t$ the level after ordering. Then $X_1 = x$ and $X_{t+1} = Y_t - \xi_t$.

A policy chooses $Y_t$ as any integer function of the information available at the start of period $t$. Given $X_1 = x$, that information is determined by $x$ and $\xi_1, \dots, \xi_{t-1}$. Policies may therefore depend on the whole history; they are not required to be Markov.

Costs are summarized by a set-up cost $K \ge 0$, a discount factor $0 \le \alpha \le 1$ and a one-period cost $G_\alpha : \mathbb Z \to \mathbb R$. The paper reduces the model with purchase cost $c$, lead time $\lambda$ and holding–penalty cost $L$ to these data by its Eq. (2), with $G_\alpha(y) = (1 - \alpha) c y + L(y)$. The $n$-period cost of a policy $Y$ from $X_1 = x$ is

$$f_n(x \mid Y) = \sum_{t=1}^{n} \alpha^{t-1}\bigl[K\,E\,\delta(Y_t - X_t) + E\,G_\alpha(Y_t)\bigr],$$

where $\delta(0) = 0$ and $\delta(z) = 1$ for $z > 0$. A policy is optimal if it minimizes $f_n(x \mid \cdot)$ for every $x$ simultaneously. The standing assumptions are that $G_\alpha$ is convex on the integers (non-decreasing forward differences) and $G_\alpha(y) \to \infty$ as $|y| \to \infty$.

The bounds (p. 537) are defined as follows. $\underline{S}$ is the smallest minimizer of $G_\alpha$. $\bar S$ is the smallest integer $\ge \underline{S}$ with $G_\alpha(\bar S + 1) \ge G_\alpha(\underline S) + \alpha K$ (21). $\underline s$ is the smallest integer with $G_\alpha(\underline s) \le G_\alpha(\underline S) + K$ (22). $\bar s$ is the smallest integer with $G_\alpha(\bar s) \le G_\alpha(\underline S) + (1 - \alpha)K$ (23).

Formalization targets

Goal: Theorem 4(a)

For every $n \ge 2$ there is an optimal $(s, S)$ policy for the $n$-period model whose first-period rule $(s_n, S_n)$ satisfies

$$\underline{s} \le s_n \le \bar{s} \le \underline{S} \le S_n \le \bar{S}.$$

Optimality is against all history-dependent policies and for every starting level. The existence of an optimal $(s, S)$ policy is part of the conclusion.

Milestones

1. The characterization of $\underline S$ by $\Delta G_\alpha(\underline S - 1) < 0 \le \Delta G_\alpha(\underline S)$, and the existence of the parameters of (21)–(23).
2. Lemma 2: $\underline{S} \le S_n$ for any optimal policy using $(s_n, S_n)$ in period 1.
3. Lemma 3: if $\bar s < s_n$, some policy using $(\bar s, S_n)$ in period 1 costs no more, from every $x$.
4. Lemma 4: if $\bar S < S_n$ (and $s_n \le \bar s$), some policy using $(s_n, \underline S)$ in period 1 costs no more, from every $x$.
5. Lemma 5: $\underline{s} \le s_n$ for any optimal policy using $(s_n, S_n)$ in period 1.

Significance

The theorem turns the optimization over $(s, S)$ policies into a search over a finite box that depends only on $G_\alpha$, $K$ and $\alpha$. The paper's Section 4 procedure for the infinite-horizon problem (Theorem 4(b), Step i) is built on this box, and the bounds also give an interpretation of $s$ and $S$: $\underline S$ is the single-period optimum, and $\bar s$, $\underline s$, $\bar S$ mark where the one-period cost exceeds that optimum by the fractions $(1 - \alpha)K$, $K$ and $\alpha K$ of the set-up cost.

The results are proved in the paper. None of them has a machine-checked proof as far as is known; no discrete-state finite-horizon inventory model with set-up cost is on the platform. A formal proof would provide a reusable finite-horizon dynamic-programming model with history-dependent policies and extended-real expected costs, and a machine-checked version of the existence of optimal $(s, S)$ policies in the discrete setting, which Theorem 4(a) contains.

Difficulty

The four lemmas compare an optimal policy with an explicit modification of it. The modification in Lemmas 2 and 5 raises the stock in period 1 and then orders $\max(X'_t, Y^n_t)$, where $Y^n_t$ is the original policy's decision along the original demand path. This comparison policy is history-dependent even when the original policy is not, so the argument cannot be carried out inside the class of Markov or $(s, S)$ policies. Expectations must be handled over finite demand histories, and costs can be infinite for general policies.

The goal also contains the existence of an optimal $(s, S)$ policy for the $n$-period model. The paper cites this from Scarf and Zabel rather than proving it. Applying Lemma 3 or 4 yields an optimal policy whose later periods are no longer of $(s, S)$ form. Restoring the $(s, S)$ form requires the dynamic-programming principle of optimality together with the $K$-convexity argument.

Formalization scope

The Lean model (VeinottWagnerSS.Bounds.Model) uses the reduced model of Eq. (2): G : ℤ → ℝ is a primitive, and $c$, $\lambda$ and $L$ do not appear. Stock levels are integers and demands are natural numbers; the demand law is a PMF ℕ with finite mean. A policy is Y : (t : ℕ) → ℤ → (Fin t → ℕ) → ℤ: period $t + 1$'s level as a function of $x$ and the first $t$ demands, so it cannot see current or future demand. Periods are numbered from $0$ in Lean. Expectations are sums over demand histories weighted by $\prod_i \varphi(\xi_i)$. $E\,G_\alpha(Y_t)$ is the difference of the expectations of the positive and negative parts, and $f_n$ is valued in EReal. Under the standing assumptions $G_\alpha$ is bounded below, so the negative part is finite and no $\infty - \infty$ arises. Both $\alpha = 1$ and $\alpha = 0$ are allowed.

The bounds SLow, SHigh, sLow, sHigh are infima of the sets in (21)–(23); a milestone proves they are the least elements. A trivializing formalization is ruled out as follows. Optimality is over all admissible policies and for every $x$. The bounds are the least integers of (21)–(23). The goal requires an optimal policy, not only a bounded pair. Existence of an optimal policy is proved, not assumed.

Printed statements corrected. Lemma 4 as printed has no hypothesis on $s_n$. Its proof begins "By lemma 3 we may assume that $s_n \le \bar s$", and without that assumption $(s_n, \underline S)$ need not be an $(s, S)$ rule. The Lean statement adds $s_n \le \bar s$. The last display of the proof of Lemma 5 reads $G_\alpha(\underline s + 1)$ where $G_\alpha(\underline s - 1)$ is meant; this affects only the proof. The milestone texts are verbatim.

Useful contributions include lemmas on convex functions on $\mathbb Z$ (monotonicity on either side of a minimizer), expectation lemmas for sums over Fin t → ℕ, and the finite-horizon principle of optimality for this model.

Selected references

• A. F. Veinott, Jr. and H. M. Wagner, Computing Optimal (s, S) Inventory Policies, Management Science 11(5), 525–552, 1965. https://doi.org/10.1287/mnsc.11.5.525
• H. Scarf, The Optimality of (S, s) Policies in the Dynamic Inventory Problem, in Mathematical Methods in the Social Sciences, Stanford University Press, 1960.
• E. Zabel, A Note on the Optimality of (S, s) Policies in Inventory Theory, Management Science 9(1), 123–125, 1962. https://doi.org/10.1287/mnsc.9.1.123
• D. L. Iglehart, Optimality of (s, S) Policies in the Infinite Horizon Dynamic Inventory Problem, Management Science 9(2), 259–267, 1963. https://doi.org/10.1287/mnsc.9.2.259

Motivation

How many times can $n$ points and $t$ lines in the plane meet? The question is the prototype of incidence geometry, and the answer controls a long list of problems in discrete and computational geometry: the number of lines rich in points, the number of distinct distances or unit distances among $n$ points, the complexity of arrangements, and sum–product estimates in additive combinatorics. Erdős asked for the order of magnitude when $t = n$ and conjectured that the answer is $n^{4/3}$; Erdős and Purdy asked for the matching bound on the number of lines containing at least $k$ of the points.

Szemerédi and Trotter settled both questions in Extremal Problems in Discrete Geometry (Combinatorica 3 (1983) 381–392, doi:10.1007/BF02579194). Their principal theorem bounds the number of point–line incidences by $c_1 n^{2/3} t^{2/3}$ over the whole range $\sqrt n \le t \le \binom n2$, and the same paper derives from it the Erdős–Purdy bound on $k$-rich lines, a version of Dirac's conjecture (proved independently by Beck, Combinatorica 3 (1983)), and a bound on the number of sequences of line densities.

Timeline.

• Erdős conjectures $O(n^{4/3})$ incidences for $n$ points and $n$ lines, and shows by a grid construction that this order would be sharp.
• 1983: Szemerédi and Trotter prove the bound $c_1 n^{2/3} t^{2/3}$ for $\sqrt n \le t \le \binom n2$, with $c_1 = 10^{60}$, by a minimal-counterexample argument and a covering lemma for squares from their earlier paper.
• 1990: Clarkson, Edelsbrunner, Guibas, Sharir and Welzl give a second proof by cuttings, with a far smaller constant (Discrete Comput. Geom. 5 (1990) 99–160).
• 1997: Székely derives the bound in a few lines from the crossing lemma (Combin. Probab. Comput. 6 (1997) 353–358).

Setting

Work in the Euclidean plane $\mathbb R^2$, written Plane in the Lean development. A line is an affine subspace $l \subseteq \mathbb R^2$ whose direction space has dimension one (IsLine l). Let $\mathcal P$ be a finite set of $n$ points and $\mathcal L$ a finite family of $t$ distinct lines. The number of incidences is

$$I(\mathcal P, \mathcal L) = \#\{(p, l) \in \mathcal P \times \mathcal L : p \in l\},$$

written incidences P L. The degree $d_i$ of a point $p_i$ is the number of lines of $\mathcal L$ through it (degree L p), and the density $y_j$ of a line $l_j$ is the number of points of $\mathcal P$ on it (density P l); so $I = \sum_i d_i = \sum_j y_j$.

For the covering lemma, coordinate axes are fixed and a square is a closed axis-parallel square $Q(a,b,s) = [a, a+s] \times [b, b+s]$ with side $s > 0$ (closedSquare (a, b, s)); its interior is the open square $(a, a+s) \times (b, b+s)$ (openSquare). A square contains the points of $\mathcal P$ in the closed square, and a family of squares covers the points lying in at least one of them.

Formalization targets

Goal: Theorem 1 (p. 381, restated and proved on p. 383)

There is an absolute constant $c_1$ such that for every finite point set $\mathcal P$ with $|\mathcal P| = n$ and every finite family $\mathcal L$ of $t$ distinct lines,

$$\sqrt n \le t \le \binom n2 \quad\Longrightarrow\quad I(\mathcal P, \mathcal L) \le c_1\, n^{2/3}\, t^{2/3}.$$

The goal leaves $c_1$ unspecified. The paper's proof gives $c_1 = 10^{60}$, and later proofs give much smaller values; any improvement of the constant still proves this statement.

Milestones, in the order the proof uses them

1. Section 3, display on p. 383. Two distinct lines meet in at most one point, so the number of good intersections is at most the number of pairs of lines:

$$\sum_{i} \binom{d_i}{2} \le \binom t2, \qquad \frac{I^2}{2n} - \frac I2 \le \frac{t^2}{2}.$$

2. Section 3, inequality (1), p. 384. $0.6\,x + (1-x)^{2/3} \le 1$ for $0 < x \le 1/2$.
3. Section 3, inequality (5), p. 385. $x^{2/3} + (1-x)/100 + 2^{-1/3}(1-x)^{2/3} \le 1$ for $0 < x \le 0.1$, and the reverse strict inequality holds somewhere in $(0.1, 0.2)$.
4. Section 3, display on p. 387. With $M = 10^{10}$, $2^{i/3}(1 - 2/M)^{4i/3} \ge 200/((0.1)^{1/3} 2^{2/3})$ for every integer $i \ge 30$.
5. Section 2, Lemma (covering lemma), p. 382. For integers $1 \le r_1 \le n$ and $r_2 \ge 256 r_1$, every set of $n$ points is covered, to at least $n/16$ of its points, by a family of squares with pairwise disjoint interiors, each containing between $r_1$ and $r_2$ of the points.

Significance

The result. The bound $n^{2/3} t^{2/3}$ is sharp up to the constant throughout the range $\sqrt n \le t \le \binom n2$, as integer-grid configurations show. Outside that range the trivial bounds $n + t^2$ and $t + n^2$ take over. Theorem 1 is the source of the $O(n^2/k^3)$ bound on $k$-rich lines (the paper's Theorem 2), of Beck's theorem (Theorem 3), and, through them, of the unit-distance bound $O(n^{4/3})$, of the Elekes sum–product estimate and of many algorithmic bounds on arrangements. It is the first nontrivial case of the polynomial-partitioning incidence theory developed since 2010.

Formalizing it. The theorem has been proved, and reproved in several ways, for four decades. To the best of the mission's knowledge Mathlib has no statement of it, of the crossing lemma, or of any point–line incidence bound in the Euclidean plane. This mission produces a checked statement of the theorem with lines as genuine one-dimensional affine subspaces and an absolute constant. It also produces checked statements of the auxiliary facts the 1983 proof uses. A complete proof may follow the original argument, the cutting argument or Székely's crossing-lemma argument; any of them closes the goal.

Difficulty

Counting pairs of lines through common points (milestone 1) gives only $I \lesssim n^{1/2} t + n$, and its dual gives $I \lesssim t^{1/2} n + t$. These Cauchy–Schwarz bounds use only the fact that two lines meet at most once, a property shared by lines in finite projective planes, where the incidence count genuinely reaches order $n^{3/2}$. Any proof of the $n^{2/3} t^{2/3}$ bound must therefore use a property of the real plane that the finite geometries lack: order, continuity, or the planarity of drawings. Szemerédi and Trotter use it through a covering lemma for axis-parallel squares, whose proof is only cited in the paper ([7]). The remaining difficulty is keeping the constants of a multi-stage minimal-counterexample argument under control.

Formalization scope

The plane is EuclideanSpace ℝ (Fin 2). A line is an AffineSubspace ℝ Plane whose direction has Module.finrank equal to $1$. Every statement requires IsLine of each member of $\mathcal L$, so neither the whole plane nor a single point counts as a line. The points form a Finset Plane and the lines a Finset (AffineSubspace ℝ Plane), which makes the $t$ lines distinct. Incidences, degrees and densities are Finset.filter cardinalities under classical decidability. Powers $n^{2/3}$, $t^{2/3}$ are Real.rpow of the counts cast to $\mathbb R$, and $\binom n2$ is Nat.choose.

In the goal, the constant $c_1$ is quantified before the points and the lines. The form "for every configuration there is a $c_1$" is trivially true (take $c_1 = I + 1$) and is not this theorem. Both ends of the range $\sqrt n \le t \le \binom n2$ are kept exactly: without the lower end, a single line through $n$ collinear points has $n$ incidences, more than $c_1 n^{2/3}$ for large $n$.

The goal follows the wording of p. 381 ("at most"). The restatement on p. 383 says "less than", which fails at $n = t = 0$ and is equivalent for $n \ge 1$ after doubling $c_1$. The covering lemma is stated with the added non-degeneracy hypotheses $1 \le r_1 \le n$. As printed it fails when $0 < n < r_1$ (no square can hold $r_1$ points), and when $r_1 = r_2 = 0$ with $n > 0$.

A full development needs a real-plane incidence toolkit: a crossing lemma or a cutting lemma, or the covering lemma with its quadtree proof. That toolkit is reusable for $k$-rich lines, Beck's theorem, unit distances and sum–product bounds, and contributions of such infrastructure as separate theorems are welcome. The three numerical milestones are self-contained real-analysis exercises.

Selected references

• E. Szemerédi, W. T. Trotter, Jr., Extremal problems in discrete geometry, Combinatorica 3 (1983) 381–392. https://doi.org/10.1007/BF02579194
• E. Szemerédi, W. T. Trotter, Jr., A combinatorial distinction between the Euclidean and projective planes, European J. Combin. 4 (1983) 385–394. https://doi.org/10.1016/S0195-6698(83)80036-5
• J. Beck, On the lattice property of the plane and some problems of Dirac, Motzkin and Erdős in combinatorial geometry, Combinatorica 3 (1983) 281–297. https://doi.org/10.1007/BF02579184
• K. L. Clarkson, H. Edelsbrunner, L. J. Guibas, M. Sharir, E. Welzl, Combinatorial complexity bounds for arrangements of curves and spheres, Discrete Comput. Geom. 5 (1990) 99–160. https://doi.org/10.1007/BF02187783
• L. A. Székely, Crossing numbers and hard Erdős problems in discrete geometry, Combin. Probab. Comput. 6 (1997) 353–358. https://doi.org/10.1017/S0963548397002976

Motivation

The security of the RSA cryptosystem rests on the assumed difficulty of factoring large integers, and the best known classical algorithms for factoring run in super-polynomial time. In 1994 Peter Shor showed that a quantum computer can factor an $n$-digit integer in time polynomial in $n$ (Shor, SIAM J. Comput. 1997; conference version FOCS 1994). The algorithm has two parts. A classical reduction, due to Miller (1976), turns factoring into order finding: given $x$ coprime to $n$, find the least $r \ge 1$ with $x^r \equiv 1 \pmod n$. The quantum part solves order finding.

This mission formalizes the quantum part as Shor analyzes it in §5 of the journal paper: the construction of the quantum state, the probability of each measurement outcome, and the classical post-processing that reads $r$ off the measured value. The paper's claim is that one run of this procedure returns $r$ with probability at least $\varphi(r)/3r$.

Timeline:

• 1976: Miller reduces factoring to order finding (with randomization).
• 1985–1994: Deutsch, Bernstein–Vazirani and Simon give the quantum Fourier sampling ideas the algorithm builds on.
• 1994: Shor's FOCS paper introduces the factoring and discrete logarithm algorithms.
• 1997: the SIAM J. Comput. version gives the analysis formalized here, with $q$ the power of $2$ in $[n^2, 2n^2)$.

Setting

Fix an integer $n \ge 2$ and an integer $x$ coprime to $n$. Its order $r$ is the least $r \ge 1$ with $x^r \equiv 1 \pmod n$; since $x$ is a unit, $r \le \varphi(n) < n$. Let $q = 2^l$ be the power of $2$ with $n^2 \le q < 2n^2$.

A quantum state on two registers, the first holding $0 \le a < q$ and the second a residue $y \in \mathbb{Z}/n$, is a complex vector $\psi(a, y)$ indexed by the basis states $|a, y\rangle$. Measuring it returns $|a, y\rangle$ with probability $|\psi(a, y)|^2$.

The Fourier matrix $A_q$ is the $q \times q$ matrix with entries $(A_q)_{a,c} = q^{-1/2}\exp(2\pi i a c/q)$, with rows indexing inputs and columns outputs. The algorithm

1. prepares $\frac{1}{q^{1/2}}\sum_{a=0}^{q-1}|a\rangle|x^a \bmod n\rangle$ (eq. (5.2)),
2. applies $A_q$ to the first register, obtaining $\frac1q\sum_{a,c}\exp(2\pi iac/q)|c\rangle|x^a \bmod n\rangle$ (eq. (5.4)),
3. measures, obtaining some $|c, y\rangle$,
4. rounds $c/q$ to the nearest fraction with denominator smaller than $n$.

The observed $c$ gives us $r$ if some fraction with lowest-terms denominator below $n$ is within $1/2q$ of $c/q$, and every such fraction has lowest-terms denominator exactly $r$. In the Lean development these objects are preFourierState, finalState, outcomeProb and yieldsOrder, in the namespace ShorAlgorithms.OrderFinding, and the shared definition ShorAlgorithms.Shared.fourierMatrix.

Formalization targets

Goal: success probability at least $\varphi(r)/3r$

For all sufficiently large $n$, with $x$, $r$ and $q$ as above,

$$\Pr\bigl[\text{the observed } c \text{ gives us } r\bigr] \;=\; \sum_{c\ \text{gives}\ r}\ \sum_{y \in \mathbb{Z}/n} |\Psi(c, y)|^2 \;\ge\; \frac{\varphi(r)}{3r},$$

where $\Psi$ is the state (5.4). The threshold on $n$ is uniform in $x$ and $q$; it is the paper's "for sufficiently large $n$" from the per-state bound.

Milestones

1. Eqs. (5.5)–(5.6). For $0 \le k < r$, the probability of $|c, x^k\rangle$ equals $\left|\frac1q\sum_{b=0}^{\lfloor (q-k-1)/r\rfloor}\exp(2\pi i(br+k)c/q)\right|^2$.
2. Eq. (5.11). For $n$ past a threshold, every $|c, x^k\rangle$ with $-r/2 \le rc - dq \le r/2$ for some integer $d$ has probability at least $1/3r^2$.
3. Eq. (5.13). If $n^2 \le q$, at most one fraction with denominator below $n$ lies within $1/2q$ of $c/q$.
4. p. 1500. Such a fraction is a convergent of the continued fraction of $c/q$.
5. p. 1501. At least $\varphi(r)$ values of $c$ are within $1/2q$ of some $d/r$ with $\gcd(d, r) = 1$; with the $r$ distinct values of $x^k$ this gives at least $r\varphi(r)$ states $|c, x^k\rangle$, and each such $c$ gives us $r$.

Significance

The goal is the quantitative statement behind "order finding is in bounded-error quantum polynomial time": since $\varphi(r)/r \ge \delta/\log\log r$ for a constant $\delta$ (Hardy and Wright, Thm. 328), $O(\log\log r)$ repetitions find $r$ with high probability, and Miller's reduction then factors $n$. Without the bound, the algorithm is a procedure with no guarantee.

The result is proved, in the paper and in textbooks (Nielsen and Chuang, 2000, §5.3), usually with a phase-estimation analysis rather than Shor's direct count. What this mission adds is a machine-checked proof of Shor's own argument, with his choice of $q$ and his constants, starting from the state built by applying $A_q$ to (5.2). Formal proofs of idealized versions exist elsewhere, for instance in the exact-period model where $r$ divides $q$ and the output is uniform on $r$ peaks, but that model removes the approximation that the $1/3r^2$ bound is about. Legendre's theorem on continued fractions is already on the platform (FamousTheorems.legendre_continued_fraction_theorem) and is included as a reference item.

Difficulty

The obvious route is to compute the output distribution in closed form. That works only when $r$ divides $q$; here $q$ is a power of $2$ and $r$ is arbitrary, so the amplitudes are geometric sums of $\lfloor (q-k-1)/r\rfloor + 1$ terms whose phases do not cancel exactly. The per-state bound $1/3r^2$ requires a lower bound on such a sum that is uniform in $r$, $c$ and $k$, with error terms of order $1/q$ controlled against a main term of order $1/r^2$. The constant $1/3$ leaves only a small margin below the limiting value $4/\pi^2 \approx 0.405$, so the errors must be bounded explicitly, not merely shown to vanish.

The second difficulty is the counting: distinct coprime numerators $d$ must give distinct outcomes $c$ in $[0, q)$, and each good $c$ must determine $r$ uniquely, which uses $r < n$ and $n^2 \le q$.

Formalization scope

Conventions the statements commit to:

• States are functions Fin q × ZMod n → ℂ; the matrix convention is row = input, so applying $A_q$ to the first register gives the amplitude $\sum_a \psi(a, y)(A_q)_{a,c}$ at $(c, y)$.
• The final state is built by applying $A_q$ to the state (5.2); the closed forms (5.5) and (5.6) are theorems, not definitions. No normalization hypothesis is assumed.
• Probabilities are squared moduli; the probability of the event "$c$ gives us $r$" sums over all $y \in \mathbb{Z}/n$, which is exact because $y$ that are not powers of $x$ have probability zero.
• $x$ is a natural number with $\gcd(x, n) = 1$; $r$ is orderOf (x : ZMod n). $q$ enters through the three hypotheses $q = 2^l$, $n^2 \le q$, $q < 2n^2$, not through a function of $n$.
• Fractions are rationals, and "in lowest terms" is Rat.den.
• Thresholds "for sufficiently large $n$" are $\exists N,\ \forall n \ge N$, with $N$ quantified before $x$, $q$, $c$ and $k$.
• Condition (5.11) is stated in its equivalent form (5.12), with an integer $d$.
• Printed slip. Eq. (5.13)'s justification says "Because $q > n^2$", but $q$ was chosen with $n^2 \le q$, and $q = n^2$ when $n$ is a power of $2$. The uniqueness claim holds under $n^2 \le q$, and that is what is stated.

Typing the closed form (5.4)–(5.6) in as the definition of the final state would make milestone 1 trivial and hide whether the probability model is the paper's; the definitions exclude this by construction.

Not stated: the polynomial running time of any step, the $O(\log\log r)$ repetition count (no explicit constant), the reversible modular exponentiation of §3, and the post-processing heuristics on p. 1501. Needed infrastructure: bounds on geometric exponential sums, Euler's totient, Diophantine approximation by fractions with bounded denominator, and Mathlib's continued fractions. Lemmas on geometric sums of roots of unity and on the order of units mod $n$ are reusable in the companion discrete logarithm mission.

Selected references

• P. W. Shor, Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer, SIAM J. Comput. 26(5):1484–1509, 1997. https://doi.org/10.1137/S0097539795293172
• P. W. Shor, Algorithms for quantum computation: discrete logarithms and factoring, Proc. 35th FOCS, 1994. https://doi.org/10.1109/SFCS.1994.365700
• G. L. Miller, Riemann's hypothesis and tests for primality, J. Comput. System Sci. 13(3):300–317, 1976. https://doi.org/10.1016/S0022-0000(76)80043-8
• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 5th ed., Oxford, 1979 (Ch. X, continued fractions; Thm. 328).
• M. A. Nielsen and I. L. Chuang, Quantum Computation and Quantum Information, Cambridge, 2000. https://doi.org/10.1017/CBO9780511976667

Motivation

In quantum mechanics the state of a system at time $t$ is $\psi(t) = \mathrm e^{-\mathrm itA}\psi$, where the Hamiltonian $A$ is a self-adjoint operator. The spectral theorem splits the Hilbert space into subspaces according to the type of the spectral measure of a vector (absolutely continuous, singularly continuous, pure point). That splitting is defined through measure theory, and it is not evident what it has to do with the motion of the system. The RAGE theorem, named after Ruelle (1969), Amrein and Georgescu (1973) and Enß (1978), answers this. Vectors in the continuous subspace are exactly the states that, on time average, leave every bounded region: the scattering states. Vectors in the pure point subspace are exactly the states that stay in a bounded region uniformly in time: the bound states. This dynamical characterization is the starting point of the geometric approach to scattering theory and of the modern theory of quantum dynamics and transport.

This mission formalizes Chapter 5 of Teschl's Mathematical Methods in Quantum Mechanics (AMS GSM 99, 2009). The chapter covers the time evolution $\mathrm e^{-\mathrm itA}$ as a unitary group, Wiener's theorem on Fourier transforms of measures, and the abstract RAGE theorem with its Heisenberg-picture corollaries.

Setting

Let $\mathfrak H$ be a complex Hilbert space with inner product $\langle\cdot,\cdot\rangle$, conjugate linear in the first argument. An operator $A$ is a linear map defined on a subspace $\mathfrak D(A)$, its domain. $A$ is self-adjoint if $\mathfrak D(A)$ is dense and $A = A^*$. $\mathfrak L(\mathfrak H)$ denotes the bounded, everywhere defined operators.

A projection-valued measure $P$ assigns to each Borel set $\Omega \subseteq \mathbb R$ an orthogonal projection $P(\Omega)$, with $P(\mathbb R) = \mathbb I$ and $P(\bigcup_n \Omega_n)\psi = \sum_n P(\Omega_n)\psi$ for disjoint $\Omega_n$. The spectral measure of $\psi$ is the finite Borel measure $\mu_\psi(\Omega) = \langle\psi, P(\Omega)\psi\rangle$. The spectral theorem says that every self-adjoint $A$ is $A = \int \lambda\, dP(\lambda)$ for a unique $P = P_A$. Then $\mathfrak D(A) = \{\psi \mid \int\lambda^2\, d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\, d\mu_\psi(\lambda)$. For a bounded Borel function $f$, $f(A)$ is the bounded operator with $\langle\psi, f(A)\psi\rangle = \int f\, d\mu_\psi$. The time evolution is $U(t) = \mathrm e^{-\mathrm itA}$, the case $f(\lambda) = \mathrm e^{-\mathrm it\lambda}$.

The spectral subspaces are

$$\mathfrak H_{ac} = \{\psi \mid \mu_\psi \ll \text{Lebesgue}\},\quad \mathfrak H_{sc} = \{\psi \mid \mu_\psi \text{ singular, without atoms}\},\quad \mathfrak H_{pp} = \{\psi \mid \mu_\psi \text{ supported on a countable set}\},$$

and the continuous subspace is $\mathfrak H_c = \mathfrak H_{ac} \oplus \mathfrak H_{sc}$. The projectors $P^{ac}, P^c, P^{pp}$ are the orthogonal projections onto these subspaces. $\sigma_p(A)$ is the set of eigenvalues of $A$.

A finite rank operator is a $K \in \mathfrak L(\mathfrak H)$ with finite dimensional range. The compact operators $\mathfrak C(\mathfrak H)$ are the norm closure of the finite rank operators. For $z$ in the resolvent set $\rho(A)$, $R_A(z) = (A - z)^{-1} \in \mathfrak L(\mathfrak H)$. An operator $K$ is relatively compact with respect to $A$ if $K R_A(z) \in \mathfrak C(\mathfrak H)$ for one $z \in \rho(A)$; in particular $\mathfrak D(A) \subseteq \mathfrak D(K)$. The Fourier transform of a finite complex Borel measure $\mu$ on $\mathbb R$ is $\hat\mu(t) = \int_{\mathbb R} \mathrm e^{-\mathrm it\lambda}\, d\mu(\lambda)$.

Formalization targets

Goal: the RAGE theorem (Theorem 5.7)

Let $A$ be self-adjoint and let $K_n \in \mathfrak L(\mathfrak H)$ be relatively compact operators converging strongly to $\mathbb I$. Then

$$\mathfrak H_c = \Big\{\psi \;\Big|\; \lim_{n\to\infty}\lim_{T\to\infty} \frac1T\int_0^T \|K_n\mathrm e^{-\mathrm itA}\psi\|\, dt = 0\Big\},\qquad \mathfrak H_{pp} = \Big\{\psi \;\Big|\; \lim_{n\to\infty}\sup_{t\ge0} \|(\mathbb I - K_n)\mathrm e^{-\mathrm itA}\psi\| = 0\Big\}.$$

Milestones

• Theorem 5.1. $U(t) = \mathrm e^{-\mathrm itA}$ is a strongly continuous one-parameter unitary group. $\lim_{t\to0}\frac1t(U(t)\psi - \psi)$ exists iff $\psi \in \mathfrak D(A)$, and then it equals $-\mathrm iA\psi$. $U(t)\mathfrak D(A) = \mathfrak D(A)$ and $AU(t) = U(t)A$.
• Theorem 5.4 (Wiener). $\displaystyle\lim_{T\to\infty}\frac1T\int_0^T|\hat\mu(t)|^2\,dt = \sum_{\lambda\in\mathbb R}|\mu(\{\lambda\})|^2$, and the sum is finite.
• Lemma 5.5. $\mathfrak C(\mathfrak H)$ is a closed $*$-ideal in $\mathfrak L(\mathfrak H)$.
• Theorem 5.6. For relatively compact $K$ and $\psi \in \mathfrak D(A)$: $\frac1T\int_0^T\|K\mathrm e^{-\mathrm itA}P^c\psi\|^2dt \to 0$ and $\|K\mathrm e^{-\mathrm itA}P^{ac}\psi\| \to 0$. For bounded $K$ this holds for all $\psi$.
• Theorem 5.8. $\displaystyle\lim_{T\to\infty}\frac1T\int_0^T \mathrm e^{\mathrm itA}K\mathrm e^{-\mathrm itA}\psi\,dt = \sum_{\lambda\in\sigma_p(A)}P_A(\{\lambda\})KP_A(\{\lambda\})\psi$ for $\psi \in \mathfrak D(A)$, and for all $\psi$ if $K$ is bounded.
• Corollary 5.9. Under the RAGE assumptions, the iterated time averages of $\mathrm e^{\mathrm itA}K_n\mathrm e^{-\mathrm itA}\psi$ and of $\mathrm e^{\mathrm itA}(\mathbb I - K_n)\mathrm e^{-\mathrm itA}\psi$ converge to $P^{pp}\psi$ and to $P^c\psi$.

Significance

The RAGE theorem connects the spectral types of the Hamiltonian with observable long-time behaviour. For Schrödinger operators $-\Delta + V$ on $L^2(\mathbb R^n)$, taking $K_n$ to be multiplication by the indicator of the ball of radius $n$ gives a sequence of relatively compact operators. The theorem then says that states in $\mathfrak H_c$ spend, on time average, a vanishing fraction of time in every ball, while states in $\mathfrak H_{pp}$ stay uniformly localized. Enß's proof of asymptotic completeness for short-range potentials rests on this characterization. The same argument, through Wiener's theorem, is used to relate the fractal dimensions of spectral measures to rates of quantum transport. Theorem 5.8 and Corollary 5.9 describe the asymptotic observables of the Heisenberg picture.

These results are classical and proved in the literature. They are not formalized. Mathlib has neither a spectral theorem nor a functional calculus for unbounded self-adjoint operators, and no decomposition of a Hilbert space by spectral type. What the platform has are Stone's theorem in the separate BookProof development (for weakly measurable groups, with its own structure of unbounded self-adjoint operators) and the discrete-time von Neumann mean ergodic theorem for contractions. The mean ergodic theorem is related to Theorem 5.8 with $K = \mathbb I$ but is a different statement. This mission formalizes the continuous-time, spectral-type-resolved statements.

Difficulty

The two sides of the RAGE characterization are defined in unrelated terms. $\mathfrak H_c$ and $\mathfrak H_{pp}$ are defined by properties of the scalar measures $\mu_\psi$, while the conditions in (5.14) concern norms of vectors moving under a unitary group and seen through operators that are only relatively compact. Wiener's theorem controls scalar quantities $\langle\varphi, \mathrm e^{-\mathrm itA}\psi\rangle$. Passing to norms $\|K\mathrm e^{-\mathrm itA}\psi\|$ needs compactness, and relative compactness only gives compactness after composing with a resolvent, which is where the restriction to $\mathfrak D(A)$ in Theorems 5.6 and 5.8 comes from. The pure point characterization needs control that is uniform in $t \ge 0$, so a limit over $n$ has to be exchanged with a supremum over all times. The limits in (5.14) and (5.19)–(5.20) are iterated, not joint, and a naive exchange of the two limits is not justified. Summing over $\sigma_p(A)$ in (5.18) needs an unconditionally convergent sum over a possibly uncountable index set. Wiener's theorem itself needs a Fubini argument for a complex measure against its conjugate.

Formalization scope

The formalization uses Lean 4 with Mathlib. Operators are partially defined linear maps (LinearPMap, H →ₗ.[ℂ] H) on a complex Hilbert space. Self-adjointness is Mathlib's IsSelfAdjoint, which includes density of the domain. The Hilbert space is not assumed separable.

The spectral theorem is not part of this mission. Every statement about $A$ takes a projection-valued measure $P$ on the Borel sets of $\mathbb R$ as data, together with the hypothesis that $A = \int\lambda\, dP(\lambda)$: $\mathfrak D(A) = \{\psi \mid \int\lambda^2 d\mu_\psi < \infty\}$ and $\langle\psi, A\psi\rangle = \int\lambda\,d\mu_\psi$ there. This is the form the spectral theorem guarantees, and it makes $P_A = P$. The time evolution $\mathrm e^{-\mathrm itA}$ is the bounded operator $P(\lambda \mapsto \mathrm e^{-\mathrm it\lambda})$, determined by its quadratic form, and $\mathrm e^{\mathrm itA}$ is its value at $-t$. Nothing else the book derives is assumed.

The spectral subspaces are sets of vectors defined only from the spectral measures, as above, and $\mathfrak H_c$ is the set of sums of a vector of $\mathfrak H_{ac}$ and a vector of $\mathfrak H_{sc}$. A formalization that defined $\mathfrak H_c$ or $\mathfrak H_{pp}$ by the dynamical conditions of (5.14) would make the goal a tautology; that is ruled out here. $P^c$, $P^{ac}$, $P^{pp}$ are the orthogonal projections onto the closed linear spans of these sets. Compact operators are the norm closure of the finite rank operators (the book's definition), not Mathlib's IsCompactOperator. Relative compactness asks for one $z \in \rho(A)$, its resolvent $R$, and a compact $C$ with $\operatorname{Ran} R \subseteq \mathfrak D(K)$ and $KR = C$. "$K$ bounded" means an everywhere defined $K \in \mathfrak L(\mathfrak H)$.

Iterated limits $\lim_n\lim_T$ are stated as: for every $n$ the inner limit exists, and the sequence of inner limits converges. The supremum over $t \ge 0$ is taken in $[0,\infty]$. Time averages use interval integrals, with Bochner integrals for vector-valued integrands; all integrands are continuous in $t$. Wiener's theorem uses Mathlib's ComplexMeasure ℝ and its vector-measure integral. The sum over $\lambda \in \mathbb R$ is an unconditional sum whose summability is part of the conclusion, and the sum over $\sigma_p(A)$ is an unconditional sum in $\mathfrak H$. The Fourier transform has the book's normalization.

A complete development needs a functional calculus for projection-valued measures (multiplicativity, strong continuity in the function argument), the reduction of $A$ by the spectral subspaces (Lemma 3.19), the Riemann–Lebesgue lemma for absolutely continuous measures, and the approximation of compact operators by finite rank ones. These pieces are reusable across the rest of the book, notably for scattering theory. Proofs of any milestone, and of such supporting lemmas, are welcome.

Selected references

• G. Teschl, Mathematical Methods in Quantum Mechanics, With Applications to Schrödinger Operators, Graduate Studies in Mathematics 99, American Mathematical Society, 2009. doi:10.1090/gsm/099. Chapter 5, pp. 123–132.
• D. Ruelle, A remark on bound states in potential-scattering theory, Il Nuovo Cimento A 61 (1969), 655–662. doi:10.1007/BF02819607.
• W. O. Amrein and V. Georgescu, On the characterization of bound states and scattering states in quantum mechanics, Helvetica Physica Acta 46 (1973), 635–658 (archive: e-periodica.ch).
• V. Enss, Asymptotic completeness for quantum mechanical potential scattering. I. Short range potentials, Communications in Mathematical Physics 61 (1978), 285–291. doi:10.1007/BF01940771.
• M. H. Stone, On one-parameter unitary groups in Hilbert space, Annals of Mathematics 33 (1932), 643–648. doi:10.2307/1968538.

Why the horseshoe

The Smale horseshoe is the standard example of a smooth invertible map of the plane with chaotic dynamics. Smale introduced it in the 1960s as the mechanism behind the complicated orbits near a transverse homoclinic point, and it became the basic model of hyperbolic invariant sets (Smale 1967). Its importance for differential equations is the Smale–Birkhoff theorem: whenever the stable and unstable manifolds of a hyperbolic fixed point intersect transversally, some iterate of the map contains a horseshoe. Melnikov's method then turns this into a checkable criterion for chaos in periodically forced planar systems such as Duffing's equation.

This mission formalizes the horseshoe as it is treated in Chapter 13 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (author's preliminary version of AMS GSM 140, 2012). It takes along the one-dimensional results from §§11.4–11.5 that the chapter's argument reuses: the tent map's Cantor set, the one-sided shift, and the metric on two-sided sequences.

Setting

Fix parameters $\lambda$ and $\mu$ and let $D = [0,1]^2$. The two horizontal strips

$$J_0 = [0,1] \times [0, 1/\mu], \qquad J_1 = [0,1] \times [1 - 1/\mu, 1]$$

are mapped by

$$F(x,y) = (\lambda x, \mu y) \text{ on } J_0, \qquad F(x,y) = (1 - \lambda x, \mu(1-y)) \text{ on } J_1 .$$

Each strip is contracted horizontally by $\lambda$ and stretched vertically by $\mu$ into a vertical strip crossing $D$. The book specifies $F$ only on $J_0 \cup J_1$ and leaves the fold between them to a picture. A horseshoe map here is any $F : \mathbb{R}^2 \to \mathbb{R}^2$ given by these formulas on $J_0 \cup J_1$. On $K_0 = F(J_0) = [0, \lambda] \times [0,1]$ and $K_1 = F(J_1) = [1-\lambda, 1] \times [0,1]$ the inverse $g$ is given by explicit formulas.

The tent map $T_\nu(x) = \frac{\nu}{2}(1 - |2x-1|)$ on $\mathbb{R}$ has the invariant set

$$\Lambda(T_\nu) = \{x \in \mathbb{R} : T_\nu^n(x) \in [0,1] \text{ for all } n \ge 0\}.$$

The second coordinate of $F$ is $T_\mu(y)$ and the first coordinate of $g$ is $T_{1/\lambda}(x)$. The horseshoe's invariant set is

$$\Lambda = \Lambda(T_{1/\lambda}) \times \Lambda(T_\mu).$$

The two-sided shift space is $\Sigma_2 = \{0,1\}^{\mathbb{Z}}$. It carries the metric

$$d(s,t) = \tfrac12 \sum_{n \ge 0} \frac{|s_n - t_n| + |s_{-n} - t_{-n}|}{2^n}$$

and the shift $\sigma(s)_n = s_{n+1}$. The itinerary $\varphi(x,y) \in \Sigma_2$ of a point of $\Lambda$ records, for $n \ge 0$, which strip $J_{y_n}$ contains $F^n(x,y)$. For $n < 0$ it records which strip $K_{x_{-n-1}}$ contains $g^{-n-1}(x,y)$.

A system $(M, f)$ is chaotic in the book's sense (p. 296) under four conditions: $f$ is continuous, $M$ is infinite, $f$ is topologically transitive (for nonempty open $U, V$ some $f^n(U)$ meets $V$), and the periodic points are dense. A Cantor set is a compact, perfect, totally disconnected set.

Formalization targets

Goal: Theorem 13.1 (p. 333)

For $0 < \lambda < \tfrac12$, $\mu > 2$ and every horseshoe map $F$:

$$\Lambda \text{ is a Cantor set}, \quad F(\Lambda) = \Lambda, \quad \varphi : \Lambda \to \Sigma_2 \text{ is a homeomorphism with } \sigma \circ \varphi = \varphi \circ F \text{ on } \Lambda,$$ $$\text{and } (\Lambda, F|_\Lambda) \text{ is chaotic.}$$

The book's sentence is: "The Smale horseshoe map has an invariant Cantor set $\Lambda$ on which the dynamics is equivalent to the double sided shift on two symbols. In particular it is chaotic."

Milestones, in attack order

• Lemma 11.15 (p. 306). On two-sided sequences, $d(s,t) \le N^{-n}$ when $s, t$ agree on $|j| \le n$, and $d(s,t)$ is bounded below by a multiple of $N^{-n}$ when they differ at some $|j| \le n$.
• Lemma 11.8 (p. 303). The one-sided shift on $\Sigma_N = \{0, \dots, N-1\}^{\mathbb{N}_0}$ has countably many periodic points, and they are dense.
• Lemma 11.9 (p. 303). The one-sided shift has a dense forward orbit.
• Lemma 11.4 (p. 299). For $\nu > 2$, $\Lambda(T_\nu)$ is a Cantor set.
• Theorem 11.5 (p. 301). For $\nu > 2$, the itinerary map conjugates $(\Lambda(T_\nu), T_\nu)$ to the one-sided shift on $\{0,1\}^{\mathbb{N}_0}$ by a homeomorphism.

Significance

Theorem 13.1 exhibits a two-dimensional invertible system with an explicit invariant set on which the dynamics is exactly the two-sided shift. Every property of the shift is then inherited:

• infinitely many periodic orbits of every period;
• a dense orbit;
• sensitive dependence (Lemma 11.3);
• orbits with any prescribed forward and backward itinerary.

Theorem 13.1 is the model to which the Smale–Birkhoff theorem (13.2) reduces the dynamics near a transverse homoclinic point. It is therefore the terminal object of the book's route from Melnikov integrals to chaos in forced oscillators.

The results are classical and fully proved in the literature. Their proofs have not been formalized. Mathlib has Cantor-type sets (the middle-thirds set), totally disconnected and perfect sets, and product topologies. It has no tent-map invariant set, no two-sided symbolic dynamics with the book's metric, and no conjugacy theorem of this kind. A formal proof would supply a machine-checked conjugacy between a concrete planar map and a full shift, together with the symbolic-dynamics layer it rests on.

Difficulty

The book's own argument for Theorem 13.1 has two gaps that a formal proof must fill. First, it asserts that a product of two Cantor sets is again a Cantor set and leaves this as an exercise. Second, it treats continuity of the itinerary map and of its inverse as an exercise. It also leans on "all other results hold with no further modifications" to transfer the one-sided lemmas (11.7–11.9) to the two-sided shift.

The two-sided transfer is not literally a restatement. The metric (11.35) weights each off-centre index by $\tfrac12$, and so the one-sided closeness estimate does not carry over verbatim; see the correction to Lemma 11.15 below.

The inverse $g$ must also be tracked alongside $F$. The negative half of the itinerary is defined through $g$ rather than through $F$, so the conjugacy at index $-1$ couples the two halves.

Finally, the parameter endpoints need care. The book allows $\lambda = \tfrac12$ and $\mu = 2$. At $\mu = 2$ the defining formulas are inconsistent on $y = \tfrac12$, and at either endpoint one factor of $\Lambda$ is the whole interval $[0,1]$.

Formalization scope

• Parameters. The goal is stated for $0 < \lambda < \tfrac12$ and $\mu > 2$, a correction of the book's closed endpoints recorded in the statement.
• Lemma 11.15 is stated with the lower bound $\tfrac12 N^{-n}$ instead of the printed $N^{-n}$. The printed bound fails for the metric (11.35): for $N = 2$, $n = 1$ and sequences differing only at index $1$, $d = \tfrac14$. The first clause is as printed.
• The map. IsHorseshoeMap λ μ F is a predicate fixing $F$ only on $J_0 \cup J_1$, and the goal quantifies over all such $F$. Its conclusion therefore cannot depend on how the fold is drawn. The inverse horseshoeInv is the explicit formula (13.5)–(13.6).
• Spaces. $\mathbb{R}^2$ is ℝ × ℝ; its max-distance has the Euclidean topology. Sequence spaces are ℕ → Fin N and ℤ → Fin N. The metrics (11.28) and (11.35) are functions symDist and symDistZ, not type-class instances. Density and continuity are stated in $\varepsilon$–$\delta$ form against them, so no unmentioned product topology enters.
• Topological equivalence is spelled out: $F$ maps $\Lambda$ onto $\Lambda$, $\varphi$ is a bijection $\Lambda \to \Sigma_2$, $\sigma \circ \varphi = \varphi \circ F$ on $\Lambda$, and $\varphi$, $\varphi^{-1}$ are continuous.
• Chaos is the book's definition (continuous, infinite, transitive, dense periodic points), applied to $F$ restricted to the subtype $\Lambda$. It is not the three-axiom definition with sensitive dependence.
• Cantor set means compact, Preperfect and IsTotallySeparated, the last being the book's definition of total disconnectedness on p. 302.

$\Lambda$ is constructed as in (13.8) and $\varphi$ as in (13.9), not quantified over. The goal asserts the full conjunction, so it cannot be discharged by exhibiting some other invariant set or some other conjugacy. For $\mu > 2$ maps satisfying IsHorseshoeMap exist, so the hypothesis is not vacuous.

A complete development needs:

• the product of Cantor sets in a product of metric spaces;
• the tent-map coding (Theorem 11.5) for both $T_\mu$ and $T_{1/\lambda}$;
• the two-sided shift's Cantor, periodic-point and transitivity properties;
• transport of chaos along a conjugacy.

The tent-map and one-sided shift lemmas duplicate those of the interval-maps mission of this series and are reusable there. Contributions proving the two-sided analogues of Lemmas 11.7–11.9 as auxiliary lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. Author's preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf
• S. Smale, Differentiable dynamical systems, Bull. Amer. Math. Soc. 73 (1967), 747–817. https://doi.org/10.1090/S0002-9904-1967-11798-1
• R. L. Devaney, An Introduction to Chaotic Dynamical Systems, 2nd ed., Addison-Wesley, 1989.
• C. Robinson, Dynamical Systems: Stability, Symbolic Dynamics, and Chaos, 2nd ed., CRC Press, 1999.

Motivation

Periodic solutions are the simplest non-stationary long-time behaviour of an autonomous system $\dot x = f(x)$: limit cycles in oscillators and population models, closed orbits of conservative systems. The first question about a periodic orbit is whether it is stable. Poincaré introduced the first-return map on a transversal section, which turns this question into a question about a fixed point of a map in one dimension less. Floquet theory attacks the same question through the linear periodic system obtained by linearizing along the orbit. This mission formalizes Chapter 12, §§12.1–12.2 of G. Teschl, Ordinary Differential Equations and Dynamical Systems (AMS Graduate Studies in Mathematics 140, 2012; author's preliminary version, DOI of the published book). That chapter proves the two approaches agree and derives the standard stability and persistence criteria from this.

Setting

Let $M \subseteq \mathbb{R}^n$ be open, $f \in C^k(M, \mathbb{R}^n)$ with $k \ge 1$, and let $\Phi(t, x)$ be the flow of $\dot x = f(x)$ with maximal intervals $I_x$: $t \mapsto \Phi(t,x)$ is the unique maximal solution with $\Phi(0,x) = x$. A point $x_0 \in M$ is periodic with period $T > 0$ if $\Phi(T, x_0) = x_0$ and $\Phi(t, x_0) \neq x_0$ for $0 < t < T$. Its orbit $\gamma(x_0) = \{\Phi(t, x_0)\}$ is then a closed curve.

Linearization along the orbit. Put $A(t) = df_{\Phi(t, x_0)}$, a $T$-periodic matrix. The first variational equation is $\dot y = A(t) y$, and $\Pi_{x_0}(t, t_0)$ denotes its principal matrix solution: $\partial_t \Pi = A(t)\Pi$, $\Pi(t_0, t_0) = \mathbb{I}$. The monodromy matrix based at $\Phi(t_0,x_0)$ is

$$M_{x_0}(t_0) = \frac{\partial \Phi_T}{\partial x}\big(\Phi(t_0, x_0)\big).$$

The Poincaré map. A transversal section is $\Sigma = \{x \in U \mid S(x) = 0\}$ with $U$ open, $S \in C^k(U)$, $\partial S/\partial x \ne 0$ and $(\partial S/\partial x)\, f \neq 0$ on $\Sigma$. If $x_0 \in \Sigma$ there is a $C^k$ return time $\tau$ near $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y), y) \in \Sigma$. The Poincaré map is

$$P_\Sigma(y) = \Phi(\tau(y), y).$$

Its derivative $dP_\Sigma(x_0)$ is a linear map of the $(n-1)$-dimensional tangent space $T_{x_0}\Sigma = \ker \frac{\partial S}{\partial x}(x_0)$ into itself.

Stability. The orbit $\gamma$ is stable if every neighborhood $U$ of $\gamma$ contains a neighborhood $V$ of $\gamma$ from which solutions stay in $U$ for all $t \ge 0$. It is asymptotically stable if moreover $d(\Phi(t,x), \gamma) \to 0$ for all $x$ in some neighborhood of $\gamma$. A periodic orbit is hyperbolic if $dP_\Sigma(x_0)$ has no eigenvalue on the unit circle.

Formalization targets

Goal: Theorem 12.4

For every $t_0 \in \mathbb{R}$,

$$\chi_{M_{x_0}(t_0)}(X) = (X - 1)\,\chi_{dP_\Sigma(x_0)}(X),$$

where $\chi$ is the characteristic polynomial. So the eigenvalues of $dP_\Sigma(x_0)$ together with the single value $1$ are exactly the eigenvalues of the monodromy matrix, with multiplicities. In particular they depend neither on the section $\Sigma$ nor on the base point on the orbit.

Milestones

• Lemma 12.1. $\Pi_{x_0}(t,t_0) = \frac{\partial\Phi_{t-t_0}}{\partial x}(\Phi(t_0,x_0))$, and $f(\Phi(t,x_0)) = \Pi_{x_0}(t,t_0) f(\Phi(t_0,x_0))$.
• Corollary 12.3. If every eigenvalue of $dP_\Sigma(x_0)$ has modulus $< 1$, then $\gamma(x_0)$ is asymptotically stable.
• Corollary 12.5. $\det dP_\Sigma(x_0) = \det M_{x_0}(t_0) \neq 0$, and $P_\Sigma$ is a local $C^k$ diffeomorphism of $\Sigma$ at $x_0$.
• Lemma 12.6. For $n = 2$, $\gamma(x_0)$ is asymptotically stable if $\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt < 0$ and unstable if the integral is positive.
• Lemma 12.7. If $f(x,0)$ has a hyperbolic periodic orbit through $x_0$ and $f(x,\mu)$ is $C^k$, then on a neighborhood of $\mu = 0$ there is a $C^k$ family $x_0(\mu)$ with $x_0(0) = x_0$ and each $x_0(\mu)$ periodic for $f(\cdot,\mu)$.

Significance

The result. Theorem 12.4 is the bridge between the two standard tools for periodic orbits. The Floquet multipliers of $\dot y = A(t)y$ can often be computed or estimated, for instance through Liouville's formula $\det M_{x_0}(t_0) = \exp\int_0^T \operatorname{div} f(\Phi(t,x_0))\,dt$. The Poincaré map is where the dynamics is decided, for instance through the fixed-point stability theory of maps. Corollaries 12.3 and 12.5 and Lemma 12.6 are the resulting stability tests. Lemma 12.7 is the structural-stability statement for hyperbolic orbits that bifurcation theory starts from. Theorems 12.8–12.10 (stable manifolds of periodic orbits) build on the same objects.

Formalizing it. All results are classical and proved in the book. None has a machine-checked proof on the platform or, as far as is known, in Mathlib, which has neither Poincaré maps nor the linearization of flows along orbits. The work is a formalization of the known proofs. It needs differentiability of the flow with respect to initial conditions, and that part is reusable across the whole of qualitative ODE theory.

Difficulty

The algebra of Theorem 12.4 is short. The two linear maps act on different spaces: $M_{x_0}(0)$ on $\mathbb{R}^n$, and $dP_\Sigma(x_0)$ on the hyperplane $T_{x_0}\Sigma$. That hyperplane is in general not orthogonal to $f(x_0)$, not a coordinate hyperplane, and not invariant under $M_{x_0}(0)$. Any comparison has to go through the derivative of $y \mapsto \Phi(\tau(y), y)$, which involves the derivative of the implicitly defined return time. Behind all this sits the differentiability of $\Phi$ in $x$ and the variational equation it satisfies, which Mathlib does not provide for local flows. For the stability milestones, the delicate step is passing from the discrete iterates of $P_\Sigma$ on $\Sigma$ back to the continuous flow near the whole orbit. That requires uniform control over one period.

Formalization scope

The state space is Fin n → ℝ. Norm-dependent notions (distance to the orbit, neighborhoods) do not depend on the choice of norm. The flow is local: IsMaximalFlow f M I Φ characterizes $\Phi$ and $I_x$ by maximality and uniqueness, and $\Phi$'s values outside its domain are never used. Derivatives are Mathlib's fderiv. The section $\Sigma$ is the book's general $\{S = 0\}$ with $(\partial S/\partial x)f \neq 0$, not a hyperplane chosen orthogonal to $f(x_0)$. The return time $\tau$ is any $C^k$ function on a neighborhood of $x_0$ with $\tau(x_0) = T$ and $\Phi(\tau(y),y) \in \Sigma$; such a function agrees with the book's $\tau$ near $x_0$. $dP_\Sigma(x_0)$ is an endomorphism L of LinearMap.ker (fderiv ℝ S x₀) that agrees with the derivative of $y \mapsto \Phi(\tau(y), y)$ there (IsPoincareDerivative). Theorems 12.4 and 12.5 assert that it exists. Eigenvalues are complex roots of characteristic polynomials.

Conventions and readings:

• The goal compares characteristic polynomials, so multiplicities count. Equality of eigenvalue sets, a statement at a single convenient $t_0$, or a hyperplane section would each be weaker than the book's theorem and do not count as solving the goal.
• The monodromy matrix is $\frac{\partial\Phi_T}{\partial x}(\Phi(t_0,x_0))$. The book prints $\Phi_{T-t_0}$ on p. 316, a typo inconsistent with (12.5) and (12.8).
• "Periodic orbit" means positive least period. Fixed points are excluded, since there is no transversal section through them. In dimension $n \le 1$ no such orbit exists, and the statements are vacuous there as in the book.
• "Hyperbolic periodic orbit" is not defined in the preliminary version. The definition used is the one the proof of Lemma 12.7 uses: no eigenvalue of $dP_\Sigma(x_0)$ on the unit circle, for some transversal section.
• Lemma 12.7: "in a sufficiently small neighborhood of $0$" is read as: there exists an open $W \ni 0$ inside the parameter set on which $x_0(\cdot)$ is $C^k$. The parameter lies in $\mathbb{R}^p$.
• Corollary 12.5: "local diffeomorphism at $x_0$" is read as: $P_\Sigma$ maps $W \cap \Sigma$ bijectively onto $W' \cap \Sigma$ for open $W, W' \ni x_0$, with an inverse that is the restriction of a $C^k$ map on $W'$.
• (12.1) is stated for all $x$ in a neighborhood of the orbit. The book writes $U(x_0)$ right after introducing $U(\gamma(x_0))$.

Needed infrastructure: existence, uniqueness and $C^k$ dependence on initial conditions for local flows; the implicit function theorem (Mathlib); characteristic polynomials and determinants of endomorphisms of finite-dimensional subspaces (Mathlib); Liouville's formula; stability of fixed points of $C^1$ maps with contracting linearization. Contributions of any of these as standalone lemmas are welcome.

Selected references

• G. Teschl, Ordinary Differential Equations and Dynamical Systems, Graduate Studies in Mathematics 140, AMS, 2012. https://doi.org/10.1090/gsm/140 (preliminary version: https://www.mat.univie.ac.at/~gerald/ftp/book-ode/ode.pdf)
• H. Poincaré, Mémoire sur les courbes définies par une équation différentielle, J. Math. Pures Appl. (3) 7 (1881) 375–422. http://www.numdam.org/item/JMPA_1881_3_7__375_0/
• G. Floquet, Sur les équations différentielles linéaires à coefficients périodiques, Ann. Sci. ÉNS (2) 12 (1883) 47–88. https://doi.org/10.24033/asens.220
• P. Hartman, Ordinary Differential Equations, 2nd ed., SIAM Classics in Applied Mathematics 38, 2002. https://doi.org/10.1137/1.9780898719222