Motivation

Exact methods for the resource-constrained project scheduling problem — branch-and-bound over activity lists or over start-time assignments, and the lower-bound computations inside them — live or die by how much of the search space can be discarded before it is enumerated. The standard tool is constraint propagation: deducing, from the precedence, resource and time-window data, new precedence relations $i\to j$ that every feasible schedule must satisfy, and tighter time windows for the activities. Brucker and Knust's Section 3.6 (doi:10.1007/978-3-642-23929-8) presents the family of interval consistency tests — input, output, input-or-output and their negations — that constraint-programming schedulers apply at every node of the search, following Carlier and Pinson (An algorithm for solving the job-shop problem, Management Science 35, 1989, doi:10.1287/mnsc.35.2.164) and Baptiste, Le Pape and Nuijten (Constraint-Based Scheduling, Kluwer, 2001, doi:10.1007/978-1-4615-1479-4). Every test is an instance of one theorem, Theorem 3.7, and its cumulative-resource analogue, Theorem 3.8. Those two theorems, and the tests as their corollaries, are this mission.

Setting

The instance is the RCPSP of mission I: activities $0,\dots,n-1$ with integer processing times $p_i$, renewable resources $k$ with capacities $R_k$ and demands $r_{ik}$, and precedence arcs; a schedule is an integer start-time vector $S$, feasible when it meets the precedences and never exceeds a capacity. Section 3.6 adds three things.

Relations. A conjunction $i\to j$ holds in $S$ when $S_i+p_i\le S_j$. Two activities are parallel, $i\parallel j$, when they overlap for at least one time unit, and a disjunction $i-j$ is the negation of that: $i\to j$ or $j\to i$. The instance carries a set $C$ of conjunctions and a set $D$ of disjunctions that every feasible schedule must satisfy; initially $C_0$ is the precedence relation and $D_0$ the pairs whose combined demand exceeds some capacity, and propagation adds to them.

Disjunctive sets. A set $I$ of at least two activities is disjunctive when any two of its members are related by a disjunction or a conjunction, so no two are ever processed together: the activities of a unit-capacity resource, the jobs of a single machine, the operations of one job in a shop. Its total processing time is $P(I)=\sum_{i\in I}p_i$.

Time windows. Each activity has a head $r_i$ and a deadline $d_i$, and a feasible schedule has $r_i\le S_i$ and $S_i+p_i\le d_i$. An activity starts first in a set $J$ when no activity of $J$ starts earlier, and ends last when none completes later.

For a cumulative resource $k$ the work of activity $i$ is $w_i=r_{ik}p_i$ and $W(J)=\sum_{i\in J}w_i$.

Formalization targets

Goal — Theorem 3.7 (printed p. 169)

Let $I$ be a disjunctive set, $J\subseteq I$, and $J',J''$ proper subsets of $J$ with $J'\cup J''\ne\emptyset$. If

$$\max_{\substack{\nu\in J\setminus J',\ \mu\in J\setminus J''\\ \nu\ne\mu}}\bigl(d_\mu-r_\nu\bigr)<P(J),$$

then in every feasible schedule an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

The first infeasibility test (printed p. 169)

If some nonempty $J\subseteq I$ has $\max_{\mu\in J}d_\mu-\min_{\nu\in J}r_\nu<P(J)$, no feasible schedule exists.

The input test (3.123) and the output test (3.124) (printed p. 171)

For $\Omega\subseteq I$ nonempty and $i\in I\setminus\Omega$: if $\max_{\mu\in\Omega\cup\{i\}}d_\mu-\min_{\nu\in\Omega}r_\nu<P(\Omega)+p_i$ then $i\to j$ for all $j\in\Omega$; symmetrically, if $\max_{\mu\in\Omega}d_\mu-\min_{\nu\in\Omega\cup\{i\}}r_\nu<P(\Omega)+p_i$ then $j\to i$ for all $j\in\Omega$.

The input-or-output test (printed p. 170)

For $i,j\in J\subseteq I$, $|J|\ge 2$: if $\max_{\mu\in J\setminus\{j\}}d_\mu-\min_{\nu\in J\setminus\{i\}}r_\nu<P(J)$ then $i$ starts first in $J$ or $j$ ends last in $J$, and $i\to j$ when $i\ne j$.

Theorem 3.8 (printed p. 186)

For a cumulative resource $k$, $J\subseteq I_k$ and proper subsets $J',J''$ of $J$: if $R_k\bigl(\max_{\mu\in J\setminus J''}d_\mu-\min_{\nu\in J\setminus J'}r_\nu\bigr)<W(J)$ then an activity from $J'$ starts first in $J$ or an activity from $J''$ ends last in $J$.

Significance

Theorem 3.7 is the single statement behind a whole toolbox. Every interval consistency test in the literature — the input and output tests that fix a new conjunction, the input-or-output test, the negation tests that only shrink a window — is the theorem with a particular choice of $J'$ and $J''$, and the book's Section 3.6.4 derives them one by one. A propagation engine that applies these tests to a fixpoint is what makes branch-and-bound for the job shop and the RCPSP practical; Carlier and Pinson's solution of the 10×10 job-shop instance is the historical demonstration. Theorem 3.8 extends the same reasoning from disjunctive to cumulative resources by replacing "no overlap" with "at most $R_k$ units per time unit", the energetic-reasoning viewpoint that the rest of Section 3.6.5 develops.

The results are elementary and proved; formalizing them fixes, once, what "feasible" means in the presence of the relation sets $C$ and $D$ and time windows, on top of the RCPSP model of mission I. That layer is reusable: the start-start distance matrix of Section 3.6.2 and the symmetric-triple rules of Section 3.6.3 are statements about the same schedules and the same relations. Nothing here is on the platform or in Mathlib.

Difficulty

The obvious argument for Theorem 3.7 is the correct one, and its difficulty is in the bookkeeping. If no activity of $J'$ starts first and none of $J''$ ends last, the first starter is some $\nu\in J\setminus J'$ and the last finisher some $\mu\in J\setminus J''$, and every activity of $J$ is processed inside $[S_\nu,\,S_\mu+p_\mu]\subseteq[r_\nu,d_\mu]$. Since the activities of a disjunctive set are pairwise non-overlapping, their total length $P(J)$ fits in that interval, contradicting (3.121). The formal work is the packing lemma: pairwise disjoint integer intervals inside an interval of length $L$ have total length at most $L$, which requires ordering the activities by start time and an induction that Mathlib does not supply.

The subtle point is the restriction $\nu\ne\mu$ in (3.121). The book allows it because "an activity which starts first cannot complete also last" when there are at least two activities with positive durations. The formal statement reads "starts first" and "ends last" with $\le$, which makes the theorem true without a positivity hypothesis: when the restriction empties the index set, $J\setminus J'=J\setminus J''=\{x\}$, the conclusion holds because $x$ cannot be both the unique first starter and the unique last finisher of a disjunctive set with two or more members. A solver should expect to handle that corner separately.

For the tests the extra step is turning "starts first" into a conjunction $i\to j$, which uses the disjunction between $i$ and $j$ together with positive processing times: with $p_j=0$ an activity could start at the same instant as $i$ without violating the disjunction, so the tests carry the positivity hypothesis that Theorem 3.7 itself does not need. Theorem 3.8 replaces the packing lemma by a work-counting lemma: over an interval of length $L$ a resource of capacity $R_k$ supplies at most $R_kL$ units, and every activity of $J$ consumes $r_{ik}p_i$ of them.

Formalization scope

Schedules are integer start-time vectors on Fin n, as in missions I and II, and a feasible schedule of this mission is one that is FeasibleSchedule for the RCPSP instance (mission I), respects the arcs of $C$ (RespectsArcs, mission II), satisfies the disjunctions of $D$ and lies within the time windows; these four hypotheses are the book's "feasible schedule" in Section 3.6 and are carried on every statement, although the arguments use only the last two, or, for Theorem 3.8, the resource constraint and the windows. The sets $C$ and $D$ are parameters, not derived from the instance, since propagation enlarges them.

Every inequality "$\max(\cdot)-\min(\cdot)<P$" is stated as the family of inequalities $d_\mu<r_\nu+P$ over the same index pairs. This is equivalent, avoids natural-number subtraction, and gives an empty index set the value the convention $\max\emptyset=-\infty$ would: the hypothesis is then vacuous. "Starts first" and "ends last" use $\le$. Proper-subset hypotheses $J'\subset J$, $J''\subset J$ are the book's; the first infeasibility test needs $J$ nonempty, and the input-or-output test needs $|J|\ge 2$.

A trivializing reading is ruled out on the disjunctive side by the nonemptiness hypotheses (an empty $J$ would make the infeasibility test's family vacuous and its conclusion false) and on the cumulative side by the observation that Theorem 3.8 with $J'=J''=\emptyset$ asserts infeasibility, which is the book's intended reading. Welcome contributions beyond the milestones: the input-negation and output-negation tests, the window-tightening rules of Section 3.6.4, and the SSD-matrix results of Section 3.6.2.

Selected references

• Peter Brucker and Sigrid Knust, Complex Scheduling, 2nd ed., Springer, 2012, Section 3.6. doi:10.1007/978-3-642-23929-8
• Jacques Carlier and Eric Pinson, An algorithm for solving the job-shop problem, Management Science 35 (1989). doi:10.1287/mnsc.35.2.164
• Philippe Baptiste, Claude Le Pape and Wim Nuijten, Constraint-Based Scheduling, Kluwer, 2001. doi:10.1007/978-1-4615-1479-4
• Ulrich Dorndorf, Erwin Pesch and Toàn Phan-Huy, Constraint propagation techniques for the disjunctive scheduling problem, Artificial Intelligence 122 (2000). doi:10.1016/S0004-3702(00)00040-0

Motivation

When several processors share a workload, the first question is how long the workload takes if it is spread out as well as possible. If a job may be interrupted and resumed later, possibly on another processor — preemption, the setting of operating systems, of communication links and of any resource that can be time-shared — the answer is a closed formula, and it is one of the oldest results in scheduling: McNaughton's wrap-around rule of 1959 (Scheduling with deadlines and loss functions, Management Science 6, doi:10.1287/mnsc.6.1.1) shows that on identical machines the optimal makespan is the larger of the longest job and the average load. Horvath, Lam and Sethi (A level algorithm for preemptive scheduling, Journal of the ACM 24, 1977, doi:10.1145/321992.321995) extended this to machines of different speeds, and Gonzalez and Sahni (Preemptive scheduling of uniform processor systems, Journal of the ACM 25, 1978, doi:10.1145/322047.322055) gave the fast algorithm with few preemptions. Brucker's Chapter 5 (doi:10.1007/978-3-540-69516-5) presents the level-algorithm version, and this mission formalizes the statements it proves about schedules.

Setting

There are $n$ jobs with processing requirements $p_1,\dots,p_n>0$ and $m$ uniform machines with speeds $s_1,\dots,s_m>0$: running job $i$ on machine $j$ for a period of length $\ell$ performs $s_j\ell$ units of its requirement, so the whole job would take $p_i/s_j$ time units there. Identical machines are the case $s_1=\dots=s_m=1$.

A preemptive schedule is a finite list of pieces, each a job, a machine, a start time and a stop time. It is feasible for the data $(s,p)$ when every piece lies in $[0,\infty)$, no two pieces on the same machine overlap, no two pieces of the same job overlap (a job is on at most one machine at any instant), and every job $i$ receives total work exactly $p_i$ over its pieces. Its makespan $C_{\max}$ is the largest stop time; the completion time $C_i$ of job $i$ is the largest stop time of one of its pieces. A schedule is nonpreemptive when every job consists of a single piece.

Following Section 5.1.2 the data are sorted, $p_1\ge\dots\ge p_n$ and $s_1\ge\dots\ge s_m$, with $n\ge m$, and one writes $P_j=\sum_{i\le j}p_i$, $S_j=\sum_{i\le j}s_i$. For a set $A$ of jobs, $h(A)=S_{|A|}$ if $|A|\le m$ and $h(A)=S_m$ otherwise: the largest combined speed that $|A|$ jobs can use at one instant.

Formalization targets

Goal — Theorem 5.8 (printed p. 127)

The optimal makespan of $Q\mid pmtn\mid C_{\max}$ is the bound (5.5):

$$w \;=\; \max\Bigl\{\max_{j=1}^{m-1}\frac{P_j}{S_j},\ \frac{P_n}{S_m}\Bigr\} ,$$

in the sense that some feasible preemptive schedule has makespan exactly $w$ and no feasible preemptive schedule has a smaller makespan.

The lower bound (5.5) (printed p. 125)

Every feasible preemptive schedule has makespan at least $w$.

$P\mid pmtn\mid C_{\max}$ (printed p. 108)

On identical machines, $LB=\max\{\max_i p_i,\ \tfrac1m\sum_i p_i\}$ is a lower bound on the makespan and is attained by some feasible preemptive schedule.

Condition (5.8) (printed p. 129)

The jobs can be scheduled preemptively within $[0,T]$ if and only if $\sum_{i\in A}p_i\le T\,h(A)$ for every set $A$ of jobs.

Theorem 5.7 (printed p. 121)

For $P\mid pmtn\mid\sum w_iC_i$ with nonnegative weights there is an optimal schedule without preemption.

Significance

Theorem 5.8 turns an optimization over an infinite family of schedules into a formula in the data, and the formula is tight in both directions: each of its terms is a resource bound that some schedule meets exactly. That is what makes preemptive makespan minimization one of the few parallel-machine problems that is solvable at all — its nonpreemptive counterpart $P2\parallel C_{\max}$ is NP-hard (p. 124) — and it is why the preemptive relaxation appears as a bound inside branch-and-bound methods for the nonpreemptive problems.

Condition (5.8) is the form in which the result is reused. It is a Hall-type condition, one inequality per set of jobs, and it is exactly what Section 5.1.2 needs to prove Theorem 5.9, which decides $Q\mid pmtn; r_i\mid L_{\max}$ by a maximum flow in an expanded network. Theorem 5.7 is the complementary statement for the other classical objective: for total weighted completion time preemption buys nothing, so the nonpreemptive solutions of Section 5.1.1 are optimal in the larger class too.

On status: every statement here is classical and proved, and the formalization adds a checked model of preemptive schedules. Mathlib has no scheduling material, and the platform's SchedulingAlgorithms series so far models only single-machine sequences (missions I, II, IV) and two-machine permutation flow shops (mission III), none of which allow a job to be split. The piece-list model of this mission is the first reusable object for preemptive and parallel-machine problems, and the later sections of Chapter 5 — $Q\mid pmtn; r_i\mid L_{\max}$, $P\mid pmtn\mid L_{\max}$ — are stated in it.

Difficulty

The obvious first idea for the goal is to run McNaughton's rule with the speeds ignored. It fails on uniform machines: filling machines one after another does not respect the constraint that a long job on a slow machine is not done when a short job on a fast one is. The correct idea is the level algorithm — always process the jobs of highest remaining requirement on the fastest free machines, sharing machines among tied jobs — and the difficulty is in the analysis rather than the idea. The proof of Theorem 5.8 has to show that the schedule it produces ends exactly at one of the terms of $w$: either no machine idles before the end, giving $P_n/S_m$, or the machines finish in speed order with the first $j$ jobs busy from time $0$, giving $P_j/S_j$. Making that case analysis rigorous requires tracking that the order of remaining requirements is preserved over time (the invariant (5.6)) and that ties are broken consistently.

A second, formal difficulty is that the level algorithm's output is defined by continuous-time events (the next completion, the next time two levels coincide), so producing an explicit finite list of pieces with the required properties is itself a construction. Any proof must build a concrete schedule; "the infimum of makespans equals $w$" is not the goal.

For the lower bound the trap is the opposite: it is tempting to argue only with total capacity $S_mT$, which gives $P_n/S_m$ but not $P_j/S_j$. The latter needs the rule that a job is on at most one machine at a time, so that $j$ jobs run at combined speed at most $S_j$; a model that let a job be split across machines simultaneously would make the theorem false, and the definition of feasibility rules it out explicitly.

Formalization scope

A schedule is a List of Pieces over jobs Fin n and machines Fin m, with real start and stop times. Feasibility is the three-part condition of the Setting, disjointness of two pieces meaning one stops no later than the other starts. Work is measured with the machine's speed, so the same definitions cover identical machines as the constant speed $1$. Pieces of length zero and unsorted lists are allowed; both are harmless.

The sorted orders are hypotheses Antitone p and Antitone s, the speeds and requirements are positive, $m\ge 1$ and, where the book assumes it, $n\ge m$. The book's normalization $s_1=1$ is not assumed: every statement here is invariant under scaling all speeds, and the book uses the normalization only for a running-time estimate. The bound $w$ is defined as the maximum of an explicit nonempty finite set, so no supremum of an empty or unbounded set occurs; $LB$ takes a proof that $n\ge 1$ so that $\max_i p_i$ is meaningful.

Two things are deliberately not stated. The level algorithm itself is not transcribed: Theorem 5.8 is stated as the existence of an optimal schedule of makespan $w$, which is what its proof establishes. And Theorem 5.9, the flow characterization for $Q\mid pmtn; r_i\mid L_{\max}$, is left for a later mission, since it needs release times and the expanded network on top of this model.

A trivializing reading is excluded by the existential form of the goal and of Theorem 5.7: each asserts that an optimal schedule exists, not merely that any optimal schedule has a property. A proof of the goal has to construct a schedule; a proof of Theorem 5.7 has to construct a nonpreemptive one that beats every preemptive competitor. Contributions welcome beyond the milestones: a general lemma that a feasible schedule can be normalized to sorted, positive-length pieces, and a proof that (5.8) for the sets $\{1,\dots,j\}$ is equivalent to $w\le T$.

Selected references

• Peter Brucker, Scheduling Algorithms, 5th ed., Springer, 2007, Chapter 5. doi:10.1007/978-3-540-69516-5
• Robert McNaughton, Scheduling with deadlines and loss functions, Management Science 6 (1959). doi:10.1287/mnsc.6.1.1
• E. C. Horvath, S. Lam and R. Sethi, A level algorithm for preemptive scheduling, Journal of the ACM 24 (1977). doi:10.1145/321992.321995
• Teofilo Gonzalez and Sartaj Sahni, Preemptive scheduling of uniform processor systems, Journal of the ACM 25 (1978). doi:10.1145/322047.322055

Motivation

Cryptography before 1949 was a catalogue of ciphers and of the tricks that broke them. C. E. Shannon's Communication Theory of Secrecy Systems (Bell System Technical Journal 28(4):656–715, 1949) replaced the catalogue with a probabilistic model: a cipher is a family of invertible maps from messages to cryptograms, indexed by a key drawn from a known distribution, and the cryptanalyst's state of knowledge after an interception is the a posteriori distribution over messages. Part II of that paper asks when interception conveys nothing at all. The answer — perfect secrecy — is the origin of the one-time pad's security proof and of the modern habit of defining security as the indistinguishability of a posteriori from a priori beliefs.

This mission formalizes §10, Perfect Secrecy: the definition, the necessary and sufficient condition (Shannon's Theorem 6), the counting bound that the key set be at least as large as the message set, the cyclic system that attains the bound, the Latin-square description of the systems that attain it, and the entropy form of the constraint.

Setting

A finite secrecy system consists of three finite sets — the messages $M$, the keys $K$, the cryptograms $E$ — together with an enciphering map $T_k : M \to E$ for each key $k$. Each $T_k$ is non-singular, i.e. injective, so a receiver who knows the key deciphers unambiguously. The key is drawn from an a priori distribution $P(k) \ge 0$, $\sum_k P(k) = 1$, and the message from an a priori distribution $P(M) \ge 0$, $\sum_M P(M) = 1$, independently of the key.

Three derived quantities carry the theory. The key weight

$$P_M(E) \;=\; \sum_{k \,:\, T_k M = E} P(k)$$

is the probability that the cryptogram is $E$ given that the message is $M$. The cryptogram probability is $P(E) = \sum_M P(M) P_M(E)$, the probability of obtaining $E$ from any cause. The a posteriori probability of the message after interception is $P_E(M) = P(M) P_M(E) / P(E)$, defined for cryptograms with $P(E) \neq 0$.

A system has perfect secrecy when, for every a priori message distribution and every cryptogram that can occur, $P_E(M) = P(M)$ for all $M$: interception leaves the cryptanalyst's probabilities unchanged. Quantifying over all a priori message distributions is Shannon's requirement that the equality hold "independently of the values of $P(M)$".

Finally, $H(M) = -\sum_M P(M)\log P(M)$ and $H(K) = -\sum_K P(K)\log P(K)$ are the entropies of the message and key choices.

Formalization targets

Goal — Theorem 6

$$\text{perfect secrecy} \iff P_M(E) = P(E) \quad \text{for all } M, E .$$

Equivalently, $P_M(E)$ does not depend on $M$: the total probability of the keys carrying $M_i$ to a given $E$ is the same as that of the keys carrying $M_j$ to the same $E$. The goal fixes nothing about the sizes of the three sets, and no structure on the key distribution beyond normalization.

Milestone — the Bayes relation (p. 680)

$$P(E) = \sum_M P(M)P_M(E), \qquad P_E(M) = \frac{P(M)P_M(E)}{P(E)} .$$

Milestone — the key-counting bound (p. 681)

$$\text{perfect secrecy} \implies \#M \le \#K .$$

Milestone — attainability, the cyclic system of Fig. 5 (p. 681)

$$T_i M_j = E_s, \quad s = i + j \bmod n, \quad P(k) = \tfrac1n \;\Longrightarrow\; \text{perfect secrecy}.$$

Milestone — Latin-square characterization (p. 681)

$$\text{perfect secrecy} \ \wedge\ \#M = \#K = \#E \implies \big(\forall M, E\ \exists! k,\ T_k M = E\big) \ \wedge\ P \text{ is uniform}.$$

Milestone — the entropy constraint (p. 682)

$$\text{perfect secrecy} \implies H(M) \le H(K) .$$

Significance

Theorem 6 is the structural fact behind every later statement in the section: the counting bound, the Latin-square description, and the entropy constraint are all read off from the independence of $P_M(E)$ from $M$. The counting bound and the entropy constraint are the precise sense in which unconditional secrecy is expensive — the key must be at least as uncertain as the message — and they are the reason practical cryptography moved to computational assumptions. The cyclic system supplies the matching construction, so the bound is sharp.

These results are classical and have textbook proofs; what this mission produces is a machine-checked development of them from a single explicit model of a finite secrecy system, including the model itself. Mathlib has extensive measure-theoretic probability and some information theory, but no formalization of Shannon's secrecy systems, of perfect secrecy, or of the results of §10. The shared definition layer — ciphers with injective enciphering maps, key weights, a posteriori probabilities, the perfect-secrecy predicate, finite entropy — is reusable for the rest of the paper: the equivocation results of §11–§13, unicity distance, and the ideal-system theorems of §16 all rest on the same objects.

Difficulty

The two directions of Theorem 6 are not symmetric. Sufficiency is a computation. Necessity has to extract, from a statement about a posteriori probabilities that only constrains cryptograms of positive probability and only for one distribution at a time, a statement about key weights alone; the useful instantiation is a distribution giving every message positive mass, and the cryptograms of probability zero must be handled separately rather than ignored.

The counting and Latin-square milestones are finite combinatorics, but the obvious argument — "for each message and cryptogram pick the key joining them" — needs the keys picked to have positive probability, and the model permits keys of probability zero; this is exactly where an argument that looks complete on paper leaves a gap in Lean. The entropy milestone is the hardest of the five: $H(M) \le H(K)$ passes through the conditional entropies $H(M \mid E) \le H(K \mid E)$, and Mathlib's information-theoretic API is stated for measures rather than for finite weighted sums, so either a bridge or a self-contained development of finite conditional entropy is required.

Formalization scope

Messages, keys and cryptograms are arbitrary finite types with decidable equality on cryptograms; probabilities are real-valued functions with explicit non-negativity and normalization hypotheses rather than PMF, so that all sums are finite sums. A cipher bundles the enciphering maps, their injectivity, and the key distribution. The a posteriori probability is a real quotient, so it evaluates to zero when the cryptogram has probability zero; every statement that mentions it carries the hypothesis that the cryptogram has positive probability. Entropy uses the natural logarithm, with $x \mapsto -x\ln x$ vanishing at $0$; all inequalities are therefore in nats and are unaffected by the choice of base.

One trivializing formalization is ruled out explicitly: perfect secrecy is quantified over all a priori message distributions, not over one fixed distribution, and it is not vacuous — the cyclic milestone exhibits a family of ciphers satisfying it for every $n \ge 1$.

Contributions welcome beyond the milestones: finite conditional entropy and its chain rule as reusable lemmas, the equivalence of the present perfect-secrecy predicate with the statistical-independence formulation of message and cryptogram, and the extension of the model towards §11's equivocation $H_E(M)$, which is the next result of the paper to formalize.

Selected references

• C. E. Shannon, Communication Theory of Secrecy Systems, Bell System Technical Journal 28(4):656–715, 1949. https://doi.org/10.1002/j.1538-7305.1949.tb00928.x
• C. E. Shannon, A Mathematical Theory of Communication, Bell System Technical Journal 27(3):379–423, 1948. https://doi.org/10.1002/j.1538-7305.1948.tb01338.x

Motivation

Lagrangian mechanics is the standard reformulation of Newtonian dynamics used throughout physics: a mechanical system is described not by forces but by a single scalar function, the Lagrangian, and the equations of motion are the stationarity conditions of an integral of that function along a path. The organizing result of the theory is Noether's theorem: every continuous symmetry of the Lagrangian produces a quantity that is constant along every solution of the equations of motion. Conservation of momentum, of angular momentum, and of energy all arise this way, and the same statement — in field-theoretic form — underlies conservation laws in electrodynamics, general relativity, and the Standard Model.

This mission formalizes the Lagrangian chapter of David Tong's Classical Dynamics (University of Cambridge, Part II Mathematical Tripos), Section 2, in Lean 4. The finite-dimensional statement it targets is the one a physics student meets first, and it is the statement on which the field-theoretic versions are modelled.

Setting

The configuration space is $\mathbb{R}^n$; a path is a map $q : \mathbb{R} \to \mathbb{R}^n$, written $q(t) = (q_1(t), \dots, q_n(t))$, and its velocity is the coordinatewise time derivative $\dot q_i(t)$. A Lagrangian is a function

$$L : \mathbb{R} \times \mathbb{R}^n \times \mathbb{R}^n \to \mathbb{R}, \qquad (t, q, v) \mapsto L(t, q, v),$$

smooth in all arguments; Tong writes it $L(q_i, \dot q_i, t)$.

The action of a path over $[t_1, t_2]$ is

$$S[q] = \int_{t_1}^{t_2} L\big(t, q(t), \dot q(t)\big)\, dt .$$

A path is a motion (it solves Lagrange's equations, Tong eq. 2.43) when

$$\frac{d}{dt}\left(\frac{\partial L}{\partial \dot q_i}\right) = \frac{\partial L}{\partial q_i} \qquad \text{for every } i \text{ and every } t,$$

both partial derivatives being evaluated at $(t, q(t), \dot q(t))$. The quantity $p_i = \partial L/\partial \dot q_i$ is the generalised momentum conjugate to $q_i$ (eq. 2.44), and

$$H = \sum_j \dot q_j \frac{\partial L}{\partial \dot q_j} - L$$

is the Hamiltonian (eq. 2.47). A function of time is a constant of the motion when it takes the same value at all times (eq. 2.46).

A one-parameter family of paths is a map $Q : \mathbb{R} \times \mathbb{R} \to \mathbb{R}^n$, $(s, t) \mapsto Q(s, t)$, whose $s = 0$ member $Q(0, \cdot)$ is the path under study. It is a continuous symmetry of $L$ (eq. 2.52) when

$$\frac{\partial}{\partial s} L\big(t, Q(s,t), \dot Q(s,t)\big) = 0 \qquad \text{for all } s, t,$$

the dot denoting $\partial/\partial t$.

Formalization targets

Goal — Noether's theorem (Tong, eqs. 2.51–2.54)

If $Q$ is a continuous symmetry of $L$ and the path $Q(0, \cdot)$ solves Lagrange's equations, then

$$N(t) = \sum_{i=1}^{n} \frac{\partial L}{\partial \dot q_i}\Big(t, Q(0,t), \dot Q(0,t)\Big)\, \frac{\partial Q_i}{\partial s}(0, t)$$

takes the same value at every time $t$.

Supporting targets

$$\text{(2.8)} \quad \delta S = 0 \text{ for all fixed-endpoint variations} \iff \frac{d}{dt}\frac{\partial L}{\partial \dot q_i} = \frac{\partial L}{\partial q_i}$$ $$\text{(2.45)} \quad L \text{ and } L + \frac{df}{dt} \text{ have the same equations of motion}$$ $$\text{(2.47)} \quad \frac{\partial L}{\partial t} = 0 \implies H \text{ is a constant of the motion}$$ $$\text{(2.49)} \quad \frac{\partial L}{\partial q_j} \equiv 0 \implies p_j \text{ is a constant of the motion}$$

Significance

Noether's theorem is the statement that converts a structural property of a system — invariance under translations, rotations, or time shifts — into a number that does not change during the evolution. It is what licenses the use of conserved quantities as first integrals when solving mechanical problems, and it is the finite-dimensional prototype of the conservation laws that classify symmetries in field theory.

Formalizing it produces a small but reusable Lean development: a definition layer for Lagrangians and their partial derivatives on $\mathbb{R}^n$, Lagrange's equations as a predicate on paths, the action functional, and the notion of a constant of the motion. Mathlib currently has the calculus these statements need — deriv, fderiv, ContDiff, interval integrals and differentiation under the integral sign — but no Lagrangian-mechanics layer built on top of it, so the definition layer of this mission is itself a contribution. The results here are classical and completely proved in the mathematical literature; what is missing is machine-checked proofs.

Difficulty

The physics derivations are three lines each, and all three lines are the ones that Lean does not grant for free. Tong's proof of Noether's theorem differentiates $L(t, Q(s,t), \dot Q(s,t))$ with respect to $s$ by the chain rule, exchanges $\partial_s$ with $\partial_t$ on $Q$, and then substitutes Lagrange's equations; in Lean, each of these steps requires the corresponding differentiability side conditions to be produced from the smoothness hypotheses, and the exchange of the two partial derivatives requires a symmetry-of-second-derivatives argument. The principle-of-least-action target additionally needs differentiation under the integral sign and the fundamental lemma of the calculus of variations (a continuous function integrating to zero against every smooth bump supported in $(t_1, t_2)$ vanishes there), neither of which is available in the exact shape needed.

The naive route — defining everything through fderiv on the product space and hoping simp unfolds the chain rule — does not close these goals, because the partial derivatives are taken in single coordinate slots and must be reassembled into a total derivative along the path.

Formalization scope

Conventions fixed by the Lean development and worth knowing before starting:

• The configuration space is Fin n → ℝ for a fixed n : ℕ, and time is all of ℝ; no interval restriction is imposed except in the action functional.
• Partial derivatives are one-dimensional derivs taken in a single slot, using Function.update to vary one coordinate. Where a derivative fails to exist, deriv returns 0; the smoothness hypotheses on L, on paths, and on families are stated so that this junk value is never the content of a statement.
• Lagrange's equations are stated with HasDerivAt, so they assert the existence of d/dt (∂L/∂q̇ᵢ) as well as its value.
• "Constant of the motion" is ∀ t₁ t₂, F t₁ = F t₂, i.e. constancy on all of ℝ, not merely a vanishing derivative.
• The symmetry hypothesis is Tong's: the s-derivative vanishes for all s and t, not only at s = 0.
• The degenerate case n = 0 is included in every statement; there it is trivially true. It is not, however, a trivializing formalization of any target: for n ≥ 1 the hypotheses are satisfied by standard systems (a free particle, a particle in a central potential), so none of the statements is vacuous.

Contributions welcome: proofs of any supporting target, reusable lemmas relating the coordinate-slot derivs used here to fderiv on the product space, and worked instances (translation invariance giving momentum conservation, rotational invariance giving angular momentum) built on the same definition layer.

Selected references

• D. Tong, Classical Dynamics, University of Cambridge Part II Mathematical Tripos lecture notes, Michaelmas 2004/2005, Section 2. https://www.damtp.cam.ac.uk/user/tong/dynamics.html
• H. Goldstein, C. Poole, J. Safko, Classical Mechanics, 3rd ed., Addison-Wesley, 2001.
• V. I. Arnold, Mathematical Methods of Classical Mechanics, 2nd ed., Springer, 1989.
• E. Noether, Invariante Variationsprobleme, Nachr. d. König. Gesellsch. d. Wiss. zu Göttingen, Math-phys. Klasse (1918), 235–257.

Motivation

Periodic signals are the basic objects of audio processing, electrical engineering and the analytic study of partial differential equations, and the standard first-course tool for handling them is the Fourier series: a decomposition of a $T$-periodic signal into sinusoids of frequencies $\omega_n = 2\pi n / T$. The identity that makes the decomposition quantitatively useful is Parseval's theorem: the average power of the signal equals the sum of the squared moduli of its Fourier coefficients, so energy can be accounted for frequency by frequency.

This mission formalizes the chain of results leading to that identity exactly as it is presented in the open-access undergraduate textbook Análise de Fourier — Um Livro Colaborativo (Esequia Sauter and Fabio Souto de Azevedo, orgs., UFRGS/REAMAT, 2022): the orthogonality relations of the trigonometric system (Teorema 3.2.1), the coefficient formulas (Teorema 3.2.2), the passage to the exponential form (§4.2), and the Parseval identity itself (Teorema 5.1.1).

Setting

Fix a period $T > 0$ and write

$$\omega_n \;=\; \frac{2\pi n}{T}, \qquad n \in \mathbb{Z}.$$

For a real-valued $f$ integrable on $[0,T]$ the book defines the trigonometric Fourier coefficients (eq. 3.23)

$$a_n \;=\; \frac{2}{T}\int_0^T f(t)\cos(\omega_n t)\,dt, \qquad b_n \;=\; \frac{2}{T}\int_0^T f(t)\sin(\omega_n t)\,dt,$$

and for a complex-valued $f$ the exponential coefficients (§4.2, eq. 4.8)

$$C_n \;=\; \frac{1}{T}\int_0^T f(t)\,e^{-i\omega_n t}\,dt, \qquad n \in \mathbb{Z},$$

which for real $f$ satisfy $C_n = (a_n - i b_n)/2$. The average power of a $T$-periodic signal is (Definição 5.1.1)

$$P_f \;=\; \frac{1}{T}\int_0^T |f(t)|^2\,dt .$$

A trigonometric polynomial of degree $N$ (Definição 3.2.1) is

$$\frac{a_0}{2} + \sum_{n=1}^{N}\bigl[a_n\cos(\omega_n t) + b_n\sin(\omega_n t)\bigr].$$

Formalization targets

Goal — Teorema 5.1.1 (Teorema de Parseval)

For $T > 0$ and $f : \mathbb{R} \to \mathbb{C}$ continuous and $T$-periodic,

$$\frac{1}{T}\int_0^T |f(t)|^2\,dt \;=\; \sum_{n=-\infty}^{\infty} |C_n|^2 .$$

The book states the identity for a periodic function "representable by a Fourier series"; the mission fixes continuity as the concrete sufficient regularity hypothesis, which keeps the statement non-vacuous and true, and leaves the sum as an unordered sum over $\mathbb{Z}$ so that no summation order is smuggled in.

Supporting targets

1. Teorema 3.2.1 — the three orthogonality relations of $\{\cos(\omega_n t), \sin(\omega_n t)\}$ on $[0,T]$, including the degenerate index $n = m = 0$.
2. §4.2 — the orthogonality relation in exponential form, $\int_0^T e^{i\omega_n t}e^{-i\omega_m t}\,dt = T$ for $n = m$ and $0$ otherwise, $n, m \in \mathbb{Z}$.
3. Teorema 3.2.2 — recovery of the coefficients of a trigonometric polynomial by the integral formulas (3.23).
4. Eq. (4.8) — $C_n = (a_n - i b_n)/2$ for a real integrable $f$.
5. Bessel's inequality and summability — every finite partial sum of $|C_n|^2$ is at most $P_f$, and the family $(|C_n|^2)_{n \in \mathbb{Z}}$ is summable. Summability is what gives the goal's infinite sum a meaning independent of any ordering.

Significance

Parseval's identity converts an integral estimate into a coefficientwise one: it is the bridge between the time domain and the frequency domain, underlies the RMS computations of the book's own electrical-engineering examples (Exemplo 5.1.2), and yields closed-form evaluations of numerical series (the book's Exemplo 5.1.3 computes a series of reciprocal odd squares this way).

Mathlib already contains the abstract Hilbert-space form of the identity for the Fourier basis on the circle AddCircle T. What this mission adds is the concrete, classroom-level layer that an engineering or physics reader recognizes: coefficients written as interval integrals of a function on $\mathbb{R}$ with an explicit period $T$, the real $(a_n, b_n)$ form, the exponential $C_n$ form and the dictionary between them, and the orthogonality relations as free-standing computations. That layer is reusable by any later mission in this series (transformada de Fourier, equação do calor, equação da onda).

Difficulty

The obvious route — expand $|f|^2 = f\bar f$, substitute the Fourier series, and integrate term by term — is exactly the book's proof, and it is the step that a formal development cannot take for granted: interchanging the integral with an infinite sum requires a convergence theorem that the book explicitly places outside its scope (the remark after Definição 3.2.3), and pointwise convergence of the Fourier series of a merely continuous function is false in general. A complete proof must run through $L^2$ convergence rather than pointwise convergence, so the central task is to connect the interval-integral coefficients on $[0,T]$ with the Hilbert-space machinery for the circle, including the change of variables and the normalization of Haar measure.

Formalization scope

The development commits to the following conventions, all fixed in the definition bundle so that every statement shares them:

• The period is an explicit real parameter $T$ with the hypothesis $0 < T$ written into each statement; at $T = 0$ the definitions would divide by zero and nothing is claimed.
• Integrals are interval integrals over $[0,T]$ of functions defined on all of $\mathbb{R}$; the book's alternative window $[-T/2, T/2]$ is not used.
• Coefficient indices range over $\mathbb{Z}$; $a_n$ and $b_n$ are defined for negative $n$ as well, matching eq. (4.7) of the book.
• $a_n, b_n$ act on real-valued functions, $C_n$ and the average power on complex-valued ones; a real signal enters the complex statements through the coercion of its values.
• Sums over $\mathbb{Z}$ are unordered sums, so the goal asserts convergence of the family, not of a symmetric partial-sum limit.
• The sign convention is $e^{-i\omega_n t}$ in the coefficient and $e^{+i\omega_n t}$ in the synthesis, as in §4.2.

The goal is not trivializable: the hypotheses (a positive period, a continuous periodic function) are satisfiable, and both sides of the identity are non-degenerate already for $f(t) = \cos(2\pi t/T)$.

Useful infrastructure beyond the mission: the dictionary between the interval-integral coefficients on $[0,T]$ and Mathlib's fourierCoeff on AddCircle T, and the orthogonality relations as standalone integral computations.

Selected references

• Esequia Sauter, Fabio Souto de Azevedo (orgs.), Análise de Fourier — Um Livro Colaborativo, UFRGS/REAMAT, 26 July 2022. https://www.ufrgs.br/reamat/TransformadasIntegrais/livro-af/main.html

Motivation

Density functional theory (DFT) is the computational method behind a large fraction of present-day electronic-structure calculations in condensed-matter physics, quantum chemistry and materials science. Its appeal is a drastic reduction in dimension: instead of an $N$-electron wavefunction $\Psi(r_1,\dots,r_N)$ living on $\mathbb R^{3N}$, one works with the one-particle density $\rho(r)$ on $\mathbb R^{3}$. That reduction is not a modelling approximation; it is licensed by two theorems of Hohenberg and Kohn (1964), for which Walter Kohn shared the 1998 Nobel Prize in Chemistry. Every statement in this mission comes from the two Hohenberg–Kohn theorems and the identities the source text uses to set them up.

Timeline. The Thomas–Fermi model (1927) introduced density-only energy expressions but is known not to bind molecules (Teller, 1962). Hohenberg and Kohn (1964) proved that for non-degenerate ground states the external potential is fixed by the ground-state density, and that the exact energy functional is minimized at that density. Kohn and Sham (1965) turned this into a practical scheme by reproducing the density with non-interacting orbitals. Levy (1979) replaced the Hohenberg–Kohn functional, defined only on ground-state densities, by a constrained-search functional defined on all $N$-representable densities.

Setting

Fix an electron number. The objects are:

• a set of admissible normalized wavefunctions $\Psi$;
• a set of external potentials $v$ (in the physical model, multiplication by $\sum_i v(r_i)$);
• a set of one-particle densities; the density of $\Psi$ is written $\rho_\Psi$.

Two functionals act on these. The universal part $F(\Psi)$ is the expectation value of the kinetic-energy and electron–electron-interaction operators, which do not depend on the system. The external part is the expectation value of the external potential, and the identity that makes DFT possible is that it depends on $\Psi$ only through its density:

$$\langle \Psi \mid \textstyle\sum_i v(r_i) \mid \Psi\rangle \;=\; \int v(r)\,\rho_\Psi(r)\,dr \;=:\; \operatorname{ext}(v,\rho_\Psi).$$

The total energy is $E_v(\Psi) = F(\Psi) + \operatorname{ext}(v,\rho_\Psi)$. A state $\Psi$ is a ground state of $v$ when it minimizes $E_v$, and a nondegenerate ground state when it is the strict minimizer. A density is $v$-representable when it is the density of a nondegenerate ground state of some potential.

Formalization targets

Goal — the two Hohenberg–Kohn theorems

$$\text{(1)}\quad \forall\,O,\ \exists\,\mathcal O:\ O(\Psi)=\mathcal O(\rho_\Psi) \ \text{ for every nondegenerate ground state } \Psi;$$ $$\text{(2)}\quad F[\rho_0]+\operatorname{ext}(v,\rho_0)\;\le\;F[\rho]+\operatorname{ext}(v,\rho) \quad\text{for every } v\text{-representable } \rho,$$

with equality exactly when $\rho=\rho_0$, the ground-state density of $v$. Part (1) is the source's Corollary 1 — the density determines every ground-state property; part (2) is its Theorem 2.

Milestone level

The supporting statements are the density-determines-the-state half of Theorem 1, the potential-is-determined-up-to-a-constant half of Theorem 1, the well-definedness of the universal functional $F[\rho]$, the variational principle, the Levy constrained-search identity, the identity $\langle\Psi|\sum_i v(r_i)|\Psi\rangle=\int v\rho_\Psi$ on $L^2(\mathbb R^{3N})$, and the normalization $\int \sum_i |\varphi_i|^2 = N$ of a Kohn–Sham density built from orthonormal orbitals.

Significance

The Hohenberg–Kohn theorems are what justifies computing with $\rho$ rather than $\Psi$: without Theorem 1 the density would not carry enough information to determine the system, and without Theorem 2 there would be no variational principle to minimize. They are also the reason the exchange–correlation functional is a well-posed object of study: it is the unknown part of a functional that the theorems guarantee exists.

Formalizing them contributes a reusable variational core — ground states, universal functionals, $v$-representability, constrained search — plus two genuinely analytic statements about $L^2(\mathbb R^{3N})$: the density-pairing identity for the external energy and the "a.e. nonvanishing eigenfunction forces the potential difference to be constant" lemma. The latter two are where the mathematical work lies, and both are stated here over the concrete configuration space $(\mathbb R^3)^N$, not in the abstract model.

Difficulty

The reductio that proves Theorem 1 is short, and it is short in Lean too. The difficulty of DFT as mathematics sits elsewhere, and this mission isolates it:

• Going from "the two potentials share a ground state" to "they differ by a constant" requires knowing the ground state does not vanish on a set of positive measure — for Schrödinger operators this is unique continuation, and here it is placed in the hypotheses of the milestone that consumes it, not assumed away in the conclusion.
• Turning $\langle\Psi|\sum_i v(r_i)|\Psi\rangle$ into $\int v \rho_\Psi$ is a Fubini argument over $(\mathbb R^3)^{N}$ with one coordinate singled out, and needs the measure-preserving identification of $(\mathbb R^3)^{N}$ with $\mathbb R^3\times(\mathbb R^3)^{N-1}$ together with integrability bookkeeping.
• The constrained-search identity is an interchange of two infima where the inner one is over a fibre that may be empty, so the junk value of sInf has to be handled.

Formalization scope

The variational layer is stated over an abstract model carrying the data actually used by the Hohenberg–Kohn argument: wavefunctions, potentials, densities, a universal functional $F$, a density map, and an external-energy pairing. No Hilbert-space structure is assumed there, because the argument uses none; what it uses is that $F$ does not depend on $v$ and that the external energy sees $\Psi$ only through $\rho_\Psi$. The two analytic milestones are stated concretely instead, on $L^2$ over $(\mathbb R^3)^{N}$, with $\rho_\Psi(r)=\sum_i\int|\Psi(\dots,r,\dots)|^2$.

Conventions fixed in Lean: energies are real; "nondegenerate ground state" means strict minimizer, so degenerate ground states are outside the scope of every statement that mentions it, exactly as in the source's caveat that the original theorems hold for non-degenerate ground states; $v$-representability quantifies over nondegenerate ground states only; the Hohenberg–Kohn functional takes the junk value $0$ off the $v$-representable set, so statements about it always carry the representability hypothesis; the Levy functional is an sInf, which is $0$ on an empty fibre.

The statements are not trivially satisfiable: the model has no hypothesis forcing the wavefunction set to be empty or the ground states to be unique, part (1) of the goal quantifies over every real-valued observable, and part (2) asserts an equality case, not merely an inequality. Contributions of the two analytic milestones are the most valuable: they need marginal-density machinery over product spaces that is reusable for any many-body formalization.

Selected references

• P. Hohenberg, W. Kohn, Inhomogeneous electron gas, Phys. Rev. 136 (1964) B864. https://doi.org/10.1103/PhysRev.136.B864
• W. Kohn, L. J. Sham, Self-consistent equations including exchange and correlation effects, Phys. Rev. 140 (1965) A1133. https://doi.org/10.1103/PhysRev.140.A1133
• M. Levy, Universal variational functionals of electron densities, first-order density matrices, and natural spin-orbitals and solution of the v-representability problem, Proc. Natl. Acad. Sci. USA 76 (1979) 6062. https://doi.org/10.1073/pnas.76.12.6062
• E. H. Lieb, Density functionals for Coulomb systems, Int. J. Quantum Chem. 24 (1983) 243. https://doi.org/10.1002/qua.560240302
• Wikipedia, Density functional theory. https://en.wikipedia.org/wiki/Density_functional_theory

Motivation

The discrete Fourier transform (DFT) is the basic spectral tool of digital signal processing, numerical analysis and computational number theory: it turns a finite sample of a signal into its frequency content, converts convolution into pointwise multiplication, and underlies fast integer and polynomial multiplication. Computed straight from its defining sum, a transform of length $n$ costs $\Theta(n^2)$ arithmetic operations. The fast Fourier transform (FFT) is any method that computes the same values in $O(n \log n)$ operations, and the radix-2 Cooley–Tukey algorithm is the most widely used of them.

The history is long and worth stating precisely. Gauss used an equivalent divide-and-conquer scheme in unpublished work of 1805 on the orbits of Pallas and Juno, without any complexity analysis. Danielson and Lanczos (1942) published the doubling step — the even/odd splitting identity that the recursion rests on — for x-ray crystallography. Good (1958) gave the prime-factor algorithm for coprime factorizations. Cooley and Tukey (1965) published the general composite-size algorithm together with the $O(n \log n)$ analysis that made the method famous. What is not known is a matching lower bound: whether a DFT of length $n$ can be computed in $o(n \log n)$ arithmetic operations is open.

Setting

Fix a length $n \in \mathbb{N}$ and a sequence of complex samples $x_0, x_1, x_2, \dots$, modelled as a function $x : \mathbb{N} \to \mathbb{C}$. The DFT of length $n$ evaluated at frequency index $k$ is

$$\mathrm{dft}(n, x)(k) \;=\; \sum_{m=0}^{n-1} x_m \, e^{-2\pi i\, m k / n},$$

and the inverse transform of a spectrum $X$ is

$$\mathrm{idft}(n, X)(m) \;=\; \frac{1}{n} \sum_{k=0}^{n-1} X_k \, e^{+2\pi i\, m k / n}.$$

Only the first $n$ samples $x_0, \dots, x_{n-1}$ enter the sum; the frequency index $k$ is an arbitrary natural number, and the transform is $n$-periodic in it.

The radix-2 Cooley–Tukey algorithm is the recursion on the exponent $p$, with $n = 2^p$:

$$\mathrm{fft}(0, x)(k) = x_0, \qquad \mathrm{fft}(p+1, x)(k) = E\!\left(k \bmod 2^p\right) + e^{-2\pi i k / 2^{p+1}} \cdot O\!\left(k \bmod 2^p\right),$$

where $E = \mathrm{fft}(p, m \mapsto x_{2m})$ is the transform of the even-indexed subsequence and $O = \mathrm{fft}(p, m \mapsto x_{2m+1})$ that of the odd-indexed one. The factor $e^{-2\pi i k/2^{p+1}}$ is the twiddle factor of the merge stage.

The arithmetic cost of that recursion is modelled by two counters. At the merge stage of a transform of $2^{p+1}$ points there are $2^p$ butterflies; each butterfly performs one twiddle-factor multiplication and two complex additions, and the two recursive calls are on $2^p$ points each:

$$M(0) = 0, \quad M(p+1) = 2M(p) + 2^p, \qquad A(0) = 0, \quad A(p+1) = 2A(p) + 2^{p+1}.$$

Formalization targets

Goal

$$\forall\, p \in \mathbb{N},\ \forall\, x : \mathbb{N} \to \mathbb{C},\ \forall\, k \in \mathbb{N}: \quad \mathrm{fft}(p, x)(k) \;=\; \mathrm{dft}(2^p, x)(k).$$

The goal fixes no operation count and no rate: it asserts only that the recursion computes exactly the transform it is supposed to compute, at every frequency index, for every input. That is the statement an implementation's correctness rests on, and it stays true whatever the cost analysis of the algorithm turns out to be.

Supporting targets

The milestones are the intermediate statements the source separates out: $n$-periodicity of the transform in the frequency index; the Danielson–Lanczos even/odd splitting

$$\mathrm{dft}(2N, x)(k) = \mathrm{dft}(N, m \mapsto x_{2m})(k) + e^{-2\pi i k/(2N)} \cdot \mathrm{dft}(N, m \mapsto x_{2m+1})(k) \qquad (N \ge 1);$$

Fourier inversion $\mathrm{idft}(n, \mathrm{dft}(n, x))(m) = x_m$ for $m < n$; the conjugate symmetry $X_{n-k} = \overline{X_k}$ of the spectrum of a real input; and the closed forms $M(p) = \tfrac{n}{2}\log_2 n$ and $A(p) = n\log_2 n$ of the two cost recursions, with $n = 2^p$.

Significance

Fourier inversion and the splitting identity are the two facts that make the transform usable at all: the first says no information is lost, the second is the single algebraic step from which every Cooley–Tukey variant — mixed radix, split radix, iterative bit-reversed implementations — is assembled. The operation counts are what justify the claim that the algorithm is $O(n\log n)$ rather than $\Theta(n^2)$: for $n = 2^{20}$ they are the difference between roughly $10^{12}$ and roughly $2 \times 10^7$ complex multiplications.

None of this is open mathematics; all of it is classical. What this mission produces is a self-contained machine-checked development of the radix-2 algorithm against an explicit definition of the DFT: a recursive algorithm, a proof that it agrees with the defining sum at every index, and a proof of its arithmetic cost. Mathlib carries Fourier theory for characters of finite abelian groups and for $\mathbb{Z}/n\mathbb{Z}$, but the mission is stated against the elementary sum above so that the statements can be read, and audited, without that background.

Difficulty

The obvious induction on $p$ does not close by itself. Unfolding the recursion gives the even and odd sub-transforms evaluated at the reduced index $k \bmod 2^p$, while the splitting identity produces them at $k$. Closing the gap needs periodicity of the length-$N$ transform in its frequency index — which is why periodicity is a milestone rather than a step inside the main proof. The second recurring obstacle is bookkeeping with the exponential: $e^{-2\pi i (2m)k/(2N)} = e^{-2\pi i mk/N}$ and $e^{-2\pi i m} = 1$ are the only analytic inputs, but they must be applied under a finite sum with natural-number casts, where $\mathbb{N}$-subtraction and division by a cast $n$ that may be zero are easy to get wrong.

Formalization scope

Sequences are total functions $\mathbb{N} \to \mathbb{C}$, not vectors of a fixed length: the length $n$ appears only as the range of the defining sum, so the transform of length $n$ ignores $x_m$ for $m \ge n$. The frequency index ranges over all of $\mathbb{N}$, and the goal is asserted for every such index, not only for $k < 2^p$ — the periodicity of both sides makes this the stronger, and cleaner, statement.

Degenerate inputs are inside the statements, not excluded by hypothesis. The length-$0$ transform is the empty sum $0$; division by the cast $(n : \mathbb{C}) = 0$ follows Lean's convention $z/0 = 0$, which is why inversion carries the hypothesis $0 < n$ and the splitting identity carries $0 < N$. The real-input symmetry is stated for $k \le n$, with $\mathbb{N}$-subtraction in $n - k$.

There is no trivializing reading: the FFT recursion is defined without ever mentioning the DFT, the cost counters are defined by their own recursions, and every hypothesis in the list above is satisfiable.

A complete development needs: the geometric-sum evaluation of $\sum_{k<n} \zeta^k$ for an $n$-th root of unity $\zeta \ne 1$ (for inversion), the even/odd reindexing of a sum over $\{0,\dots,2N-1\}$, and the periodicity computations above. All of these are reusable beyond this mission; the splitting identity in particular is the entry point for a mixed-radix or split-radix sequel.

Selected references

• J. W. Cooley and J. W. Tukey, An algorithm for the machine calculation of complex Fourier series, Mathematics of Computation 19 (1965), 297–301. https://doi.org/10.1090/S0025-5718-1965-0178586-1
• G. C. Danielson and C. Lanczos, Some improvements in practical Fourier analysis and their application to x-ray scattering from liquids, Journal of the Franklin Institute 233 (1942), 365–380 and 435–452. https://doi.org/10.1016/S0016-0032(42)90767-1
• M. T. Heideman, D. H. Johnson and C. S. Burrus, Gauss and the history of the fast Fourier transform, Archive for History of Exact Sciences 34 (1985), 265–277. https://doi.org/10.1007/BF00348431
• Fast Fourier transform, Wikipedia. https://en.wikipedia.org/wiki/Fast_Fourier_transform

Motivation

The NRL Plasma Formulary is a standard desk reference of the plasma-physics community: a compilation of the formulas, constants and unit conversions used in daily practice. Its opening section, "Numerical and Algebraic" (p. 3 of the 2013 edition), collects the few purely mathematical identities the rest of the handbook leans on. Two of them are exact summation formulas rather than approximations, and the first is the Rothe–Hagen identity, quoted there as valid "for all complex $x$, $y$, $z$ except when singular" and attributed to H. W. Gould's work on binomial coefficient summations.

Unlike the handbook's numerical entries, this identity is a theorem with a precise hypothesis set, and it is exactly the kind of entry a reader takes on trust. It generalizes the Vandermonde convolution, it is the coefficient identity underlying the generalized binomial series, and it specializes to Abel's binomial theorem. Formalizing it turns one line of a reference handbook into a machine-checked statement and produces, as a by-product, a reusable Lean development of binomial coefficients with an arbitrary complex upper index.

Setting

For a complex number $w$ and a natural number $k$, the generalized binomial coefficient is the falling factorial divided by a factorial,

$$\binom{w}{k} \;=\; \frac{w(w-1)\cdots(w-k+1)}{k!} \;=\; \frac{1}{k!}\prod_{j=0}^{k-1}(w-j),$$

with the empty-product convention $\binom{w}{0} = 1$. It is a polynomial in $w$ of degree $k$, and it agrees with the usual binomial coefficient when $w$ is a natural number.

Fix complex parameters $x$, $y$, $z$ and, for $k \in \mathbb{N}$, consider the Rothe factor

$$A_k(x,z) \;=\; \frac{x}{x+kz}\binom{x+kz}{k},$$

which is defined whenever $x + kz \neq 0$. The factor $x+kz$ in the denominator cancels against the leading factor of the falling factorial, so $A_k(x,z)$ extends to a polynomial in $x$ and $z$: $A_0(x,z) = 1$ and, for $k \ge 1$,

$$A_k(x,z) \;=\; \frac{x\,(x+kz-1)(x+kz-2)\cdots(x+kz-k+1)}{k!}.$$

Both forms occur in the literature; the mission carries both and asks for the comparison between them, because the quotient form is the one printed in the handbook while the polynomial form is the one that carries no side condition.

Formalization targets

Goal — the Rothe–Hagen identity, as printed

For complex $x,y,z$ and $n \in \mathbb{N}$, provided $x+kz \neq 0$ and $y+kz \neq 0$ for every $0 \le k \le n$, and $x+y+nz \neq 0$,

$$\sum_{k=0}^{n} \frac{x}{x+kz}\binom{x+kz}{k}\;\frac{y}{y+(n-k)z}\binom{y+(n-k)z}{n-k} \;=\; \frac{x+y}{x+y+nz}\binom{x+y+nz}{n}.$$

This is the handbook's line, with its "except when singular" proviso made explicit as the three non-vanishing hypotheses.

Stronger — the identity with no side condition

$$\sum_{k=0}^{n} A_k(x,z)\,A_{n-k}(y,z) \;=\; A_n(x+y,z),$$

in terms of the polynomial form $A_k$ above. This version holds for all complex $x,y,z$, with no exceptional locus, and implies the printed form wherever the latter's denominators are non-zero.

Supporting targets

$$\binom{w+1}{k+1} = \binom{w}{k} + \binom{w}{k+1}, \qquad \sum_{k=0}^{n}\binom{x}{k}\binom{y}{n-k} = \binom{x+y}{n}.$$

The first is Pascal's rule for a complex upper index; the second is the Vandermonde convolution over $\mathbb{C}$, which is the case $z = 0$ of the goal.

Significance

The identity is the convolution law of the generalized binomial series: the formal power series $\mathcal{B}_z(t)$ solving $\mathcal{B} = 1 + t\,\mathcal{B}^{z}$ satisfies $\mathcal{B}_z(t)^x = \sum_{n \ge 0} A_n(x,z)\,t^n$, so the goal is the statement $\mathcal{B}_z^x \cdot \mathcal{B}_z^y = \mathcal{B}_z^{x+y}$ read off coefficientwise (Graham–Knuth–Patashnik, Concrete Mathematics, §5.4). Consequences include Abel's binomial theorem, the Lagrange-inversion count of $z$-ary trees, and ballot-type identities in lattice-path enumeration.

Mathlib provides the Vandermonde convolution for natural-number arguments (Nat.add_choose_eq), the ascending and descending Pochhammer polynomials, and Ring.choose for binomial rings; it does not contain the Rothe–Hagen identity in any form. The four statements of this mission are therefore new formal content, and the complex-upper-index binomial API they force is reusable well beyond the mission.

The identity is classical and has been proved many times since Rothe (1793) and Hagen (1891), with the modern treatment in Gould's papers; nothing here is open mathematics. What is missing is a machine-checked proof.

Difficulty

The obvious attack — induction on $n$ using Pascal's rule — does not close as stated: the summand $A_k(x,z)$ is not Pascal-stable, since shifting $x$ by $1$ moves $x+kz$ for every $k$ at once, and the induction hypothesis is about a different family. The standard proofs instead treat both sides as polynomials in $x$ and $y$ for fixed $z$ and $n$, verify the identity on an infinite set of points where a combinatorial reading is available, and conclude by the identity theorem for polynomials; or they extract coefficients from the generalized binomial series via Lagrange inversion. Either route needs infrastructure: a two-variable polynomial-identity argument over $\mathbb{C}$, or a formal-power-series compositional inverse.

A second, more prosaic difficulty is the singular locus. The printed identity divides by $x+kz$ for every $k \le n$, and in Lean division by zero returns zero rather than failing, so a formalization that drops the non-vanishing hypotheses states a different — and in general false — claim.

Formalization scope

All statements are over $\mathbb{C}$. The generalized binomial coefficient is defined as an explicit product over Finset.range k divided by (k ! : ℂ), so $\binom{w}{0} = 1$ holds definitionally and no Nat.choose coercion enters. Sums run over Finset.range (n+1), with the complementary index written as the truncated natural subtraction n - k; inside that range this is the ordinary $n-k$, so the truncation convention is never exercised.

The proviso "except when singular" is formalized as three explicit hypotheses — $x+kz \ne 0$ for all $k \le n$, $y+kz \ne 0$ for all $k \le n$, and $x+y+nz \ne 0$ — rather than by relying on Lean's junk value for division by zero. These hypotheses are satisfiable (for instance $z = 0$, $x = y = 1$), so the goal is not vacuous, and they constrain only denominators, so they do not trivialize the sum.

The singularity-free milestone commits to a total function rotheA defined by cases on $k$, with value $1$ at $k = 0$; the comparison milestone pins that function to the quotient form under the non-vanishing hypothesis, so the mission cannot be satisfied by proving facts about a differently normalized object.

Contributions welcome beyond the milestones: complex-upper-index binomial API (symmetry, negation $\binom{-w}{k} = (-1)^k\binom{w+k-1}{k}$, polynomiality in the upper index), and any formal-power-series development supporting Lagrange inversion.

Selected references

• J. D. Huba, NRL Plasma Formulary, Naval Research Laboratory, 2013, p. 3, "Numerical and Algebraic" (Rothe–Hagen identity). https://www.nrl.navy.mil/News-Media/Publications/NRL-Plasma-Formulary/
• H. W. Gould, "Note on Some Binomial Coefficient Identities of Rosenbaum", Journal of Mathematical Physics 10, 49 (1969). https://doi.org/10.1063/1.1664760
• H. W. Gould and J. Kaucky, "Evaluation of a Class of Binomial Coefficient Summations", Journal of Combinatorial Theory 1, 233–247 (1966). https://doi.org/10.1016/S0021-9800(66)80051-9
• R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics, 2nd ed., Addison-Wesley, 1994, §5.4 (generalized binomial series).

Motivation

This mission formalizes the group theory of J. A. Wolf's Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968) 421–446 (doi:10.4310/jdg/1214428658), namely its §3 and §4. Wolf opens with the object of study: "If a group $\Gamma$ is generated by a finite subset $S$, then one has the 'growth function' $g_S$, where $g_S(m)$ is the number of distinct elements of $\Gamma$ expressible as words of length $\le m$ on $S$" (p. 421). Section 3 proves that a group with a finitely generated nilpotent subgroup of finite index "is of polynomial growth, and in fact $c_1m^{E_1(\Delta)} \le g_S(m) \le c_2m^{E_2(\Delta)}$"; section 4 proves that "a polycyclic group, either has a finitely generated nilpotent subgroup of finite index and thus is of polynomial growth, or has no such subgroup and is of exponential growth" (p. 421).

Applying Milnor's companion note, which is the complete mission Milnor: growth of finitely generated solvable groups on this platform, Wolf concludes "that a finitely generated solvable group, either is polycyclic and has a nilpotent subgroup of finite index and is thus of polynomial growth, or has no nilpotent subgroup of finite index and is of exponential growth" (p. 421). That is the Milnor–Wolf theorem, the goal here, and Wolf's Theorem 4.8. It prompted the question Wolf asks on p. 422, "whether every finitely generated group $\Gamma$, which is not of exponential growth, necessarily has a nilpotent subgroup of finite index"; Grigorchuk's groups of intermediate growth (1984) answered it in the negative, and Gromov (1981) proved that polynomial growth alone does force a nilpotent subgroup of finite index.

Setting

Growth. For a finite subset $S$ of a group $\Gamma$, the growth function $g_S(m)$ counts the elements expressible as words of length $\le m$ on $S$, a word $s_1^{a_1} \cdots s_r^{a_r}$ having length $|a_1| + \cdots + |a_r|$ (p. 426). The published MilnorWolf.growthFunction S m takes this as the size of the ball Chou.wordBall S m, the set of products of at most $m$ factors from $S \cup S^{-1}$. Wolf's two kinds of bound (p. 421) are polynomial growth of degree $\le E$, $g_S(m) \le c \cdot m^E$, and exponential growth, $u \cdot v^m \le g_S(m)$ with $v > 1$; the published predicates are MilnorWolf.HasPolynomialGrowthOfDegreeLE and Chou.HasExponentialGrowth, the latter with $u = 1$, which is what Theorem 4.3 actually produces. Both quantify over some finite generating set, and Wolf shows (p. 427, p. 434) that neither depends on which one.

Growth exponents. For a finitely generated nilpotent $\Delta$ with lower central series $\Delta = \Delta_0 \supseteq \Delta_1 \supseteq \cdots \supseteq \Delta_{s+1} = \{1\}$, each factor $\Delta_k/\Delta_{k+1}$ is finitely generated abelian with free part of rank $n_k$; Wolf's (3.3) sets $E_1(\Delta) = \sum_k (k+1)n_k$ and $E_2(\Delta) = \sum_k 2^kn_k$. These are MilnorWolf.growthExponentOne and MilnorWolf.growthExponentTwo.

Polycyclic groups. A solvable group is polycyclic if it satisfies condition (1) of Proposition 4.1: "There is a normal series $\Gamma = A_0 \supset A_1 \supset \cdots \supset A_t = \{1\}$ with every quotient $A_i/A_{i+1}$ finite or infinite cyclic" (p. 433), where a normal series, as in Kurosh, has each term normal in the preceding one. This is MilnorWolf.IsPolycyclic. Solvable is Mathlib's Group.IsSolvable.

Formalization targets

The goal is Wolf's Theorem 4.8 (p. 438): "Let $\Gamma$ be a finitely generated solvable group. If $\Gamma$ has a nilpotent subgroup $\Delta$ of finite index, then $\Gamma$ is polycyclic and of polynomial growth of degree $\le E_2(\Delta)$. If $\Gamma$ does not have a nilpotent subgroup of finite index, then $\Gamma$ is of exponential growth."

The milestones are the results it rests on, in the paper's order. Section 3 climbs from two rescaling lemmas (3.4, 3.5) and the growth function of a free abelian group (3.6) through generating sets adapted to the lower central series (3.7) to the polynomial bounds for a finitely generated nilpotent group (3.2), then passes them to a group with a finite-index subgroup (3.11). Section 4 characterises polycyclic groups (4.1, whose one hard input is Hirsch's theorem, a milestone of its own) and proves the polycyclic dichotomy (4.3). Milnor's Theorem, already proved on this platform, appears as a reference milestone: it is what carries 4.3 from polycyclic to solvable, and Wolf notes on p. 437 that "J. Milnor extended the scope of Theorem 4.3 by proving [10] that a finitely generated nonpolycyclic solvable group must be of exponential growth."

Significance

Theorem 4.8 is the first growth dichotomy: within finitely generated solvable groups there is nothing between polynomial and exponential, and the polynomial side is exactly the almost nilpotent one. It is the result Gromov's theorem generalises in one direction and Grigorchuk's groups bound in the other, and the reason a group of intermediate growth can be neither solvable nor elementary amenable, which is how those groups were first placed outside both classes. Chou's Theorem 3.2, in the mission Chou: elementary amenable groups, extends exactly this statement to elementary amenable groups and cites both halves.

Section 3 also has independent value. The polynomial bounds with the explicit exponents $E_1$ and $E_2$ from the lower central series are sharper than the usual textbook statement that a finitely generated nilpotent group has polynomial growth, and the pieces along the way are reusable: the growth function of $\mathbb Z^n$ in closed form, and the fact that polynomial growth of a given degree is inherited from a finite-index subgroup.

Difficulty

The hard milestone is the second half of Theorem 4.3, that a polycyclic group with no nilpotent subgroup of finite index has exponential growth. Wolf proves it through Proposition 4.4, which passes to a Malcev completion and reads the eigenvalues of the induced Lie algebra automorphisms; that machinery is not in Mathlib and is not part of this mission. A route that avoids it: a polycyclic group acts on a free abelian factor of its chain by integer matrices, so either some element has an eigenvalue off the unit circle, and then the separation argument of Wolf's p. 437 applies verbatim with that factor in place of the Lie algebra, or every eigenvalue of every element lies on the unit circle, and then Kronecker's theorem, which Mathlib has, makes them all roots of unity, so a finite-index subgroup acts unipotently and is nilpotent. Wolf records in the "Added in Proof" (p. 445) that "B. Hartley recently sent me a manuscript consisting of an alternate proof that a polycyclic group without nilpotent subgroups of finite index is of exponential growth."

Theorem 3.2 is long rather than deep: the lower bound (3.8) and the upper bound (3.9), (3.10) are two inductions along the lower central series, each carrying explicit word-length bookkeeping, and both need the adapted generating sets of Lemma 3.7, in the corrected form stated here: as printed, the lemma fails when a lower-central factor has torsion. Mathlib has no polycyclic groups, so Proposition 4.1 starts from nothing; it also lacks Hirsch's theorem and P. Hall's finite presentability results, which is why Hirsch is stated here as its own milestone rather than assumed.

Formalization scope

No new definitions: every notion is taken from the published bundles Chou_Growth and MilnorWolf_Growth, so the statements here are directly comparable with those of the Chou and Milnor missions. Growth is measured on closed balls, Chou.wordBall S m being the products of at most $m$ letters from $S \cup S^{-1}$ and $g_S(m)$ its cardinality, finite because $S$ is a Finset. "Not of exponential growth" is the negation of an existential, so it is a statement about every finite generating set.

Conditions (8) to (11) of Proposition 4.1, Proposition 4.4 and the Lie-theoretic apparatus of §4, and the Riemannian geometry of §2, §5 and §6, are outside this mission; Proposition 4.1 is stated here with its first seven conditions, which are the ones §4 uses. Hirsch's theorem is cited, not proved, by Wolf, and appears as a milestone under its own source (Proc. London Math. Soc. 44 (1938) 53–60) rather than as an omission. Cheeger's and Hartley's sharpenings, recorded in Wolf's "Added in Proof", are not included.

No hypothesis is vacuous: the free abelian groups witness Proposition 3.6 and Theorem 3.2, a polycyclic group with no nilpotent subgroup of finite index exists (the semidirect product $\mathbb Z^2 \rtimes_A \mathbb Z$ for a hyperbolic $A \in SL_2(\mathbb Z)$, which is Wolf's own example of the exponential case), and the lamplighter group $\mathbb Z/2 \wr \mathbb Z$ is finitely generated solvable and not polycyclic, so Theorem 4.8's second alternative is not empty either. Contributions welcome: proofs of any milestone, and the general library results they need, such as polycyclic groups and Hirsch's theorem.

Selected references

• J. A. Wolf, Growth of finitely generated solvable groups and curvature of Riemannian manifolds, J. Differential Geometry 2 (1968), 421–446. doi:10.4310/jdg/1214428658
• J. Milnor, Growth of finitely generated solvable groups, J. Differential Geometry 2 (1968), 447–449. doi:10.4310/jdg/1214428659
• J. Milnor, Problem 5603, Amer. Math. Monthly 75 (1968), 685–686. The identifier is for the Advanced Problems section 5600–5609 that contains it: doi:10.2307/2313822
• K. A. Hirsch, On infinite soluble groups. I, Proc. London Math. Soc. 44 (1938), 53–60. doi:10.1112/plms/s2-44.1.53
• A. G. Kurosh, Theory of groups, vol. II, 2nd ed., translated by K. A. Hirsch, Chelsea, 1955. Scanned at archive.org/details/a.-g.-kurosh-the-theory-of-groups-volume-2-1960.
• A. I. Mal'cev, On certain classes of infinite solvable groups, Amer. Math. Soc. Transl. (2) 2 (1956), 1–21. doi:10.1090/trans2/002/01
• R. G. Swan, Representations of polycyclic groups, Proc. Amer. Math. Soc. 18 (1967), 573–574. doi:10.1090/S0002-9939-1967-0213442-5
• M. Gromov, Groups of polynomial growth and expanding maps, Publ. Math. IHÉS 53 (1981), 53–78. doi:10.1007/BF02698687
• R. I. Grigorchuk, Degrees of growth of finitely generated groups, and the theory of invariant means, Math. USSR-Izv. 25 (1985), 259–300 (Russian original 1984). doi:10.1070/IM1985v025n02ABEH001281
• C. Chou, Elementary amenable groups, Illinois J. Math. 24 (1980), 396–407. doi:10.1215/ijm/1256047608