Newton's fluxion notation, $\dot{x}$, names a rate. Leibniz's $dy/dx$ names a ratio of differentials, and that is the difference that matters here: written as a ratio, the chain rule $$\frac{dz}{dx} \;=\; \frac{dz}{dy}\cdot\frac{dy}{dx}$$ reads as cancellation and composes without bookkeeping. A notation that composes can be applied mechanically to an arbitrary composite, which is precisely what an automatic-differentiation engine does: it walks a composition graph and multiplies local derivatives. Reverse-mode is that walk taken from the output backwards, and reverse-mode on a scalar loss is backpropagation.
Nothing in that chain is new mathematics, and this volume claims none. What it claims is that the corpus already stands on it: G = U ∘ F ∘ K ∘ C is a composite map, its order-dependence is a statement about composition, and the derivative of that composite is the Leibniz rule. Book XVII ch 1 locates the standard statement at Deisenroth p. 146 and automatic differentiation at p. 164.
| ch | title | state |
|---|---|---|
| 1 | A Ratio, Not a Rate — Leibniz 1684 and Newton's Fluxions read side by side. The planned thesis failed: Newton's notation composes too (his Ex. 5). What differs is a clock, which maps onto forward versus reverse mode | written 2026-09-27 — ch01-verify.py, 0 FAIL |
| 2 | The Rule Itself — the chain rule for composite and vector-valued maps, Jacobians, and the corpus's operator chain as an instance | written 2026-09-27 — ch02-verify.py, 0 FAIL |
| 3 | Mechanising It — forward and reverse mode, why reverse mode wins on a scalar loss, and what backpropagation actually is | written 2026-09-27 — ch03-verify.py, 0 FAIL |
| 4 | Euler in the Middle — what the eighteenth century did with the notation before anyone could run it | written 2026-09-27 — ch04-verify.py, 0 FAIL |
| 5 | Off the Line — calculus in three dimensions: the divergence theorem, the expanding universe as a flux, and the visible universe's moving skin | written 2026-09-27 — ch05-verify.py, 0 FAIL |
| 6 | The Integral and the Fundamental Theorem — Riemann sums, the integral as Leibniz's sum of differentials, and the theorem that joins it to the derivative | planned |
| 7 | Sequences and Series — convergence, the geometric series, bounded monotone sequences, and the comparison test; the ratio test, the alternating series test and Abel’s lemma are in a second Lean file, Series2.lean (first compile: 7 of 8 theorems clean, one fix pending recompile); the root test, radius of convergence and Taylor’s theorem are still to come | written 2026-11-03; statements located in Lebl, Basic Analysis I (pp.55, 88, 92, 93) and Thomson–Bruckner–Bruckner (pp.68, 124, 132, 141) and Ross (pp.57, 96, 98) — ch07-verify.py, 0 FAIL; Lean core compiled (author run): Series.lean, series.axioms.txt |
| 8 | Several Variables — partial derivatives, the differential, the gradient, symmetry of mixed partials with a control, and the area scaling of a linear map; Fubini and the nonlinear change of variables are shown by example only, and line and surface integrals are not covered; Lean file untested | written 2026-11-04 |
| 9 | Foundations of Analysis — why the rationals have a hole, and three theorems that depend on completeness (Bolzano–Weierstrass, the intermediate value theorem, the extreme value theorem) with a control for each; pointwise versus uniform convergence; metric spaces and general compactness are not covered; Lean file untested | written 2026-11-04; statements located in Lebl, Basic Analysis I (pp.24, 78, 130, 133, 134, 229, 230, 235) — ch09-verify.py |
Scope extension, 2026-11-02. Chapters 6 to 9 turn this volume from a lineage into the single-variable and several-variable calculus sequence, finishing with analysis. They set out standard material and claim no new results. Each is meant to follow a named textbook page by page, as chapters 1 to 5 do; chapter 7 was written before a text was held, and says so. A chapter is marked written only when it has a verify script, as before, and a Lean file whose statements have been read against the textbook statement, because a Lean file that compiles may still not state the textbook result. None of this is machine-checked yet. The linear algebra that completes the sequence is in Book XXIV. Chapters 7 and 8 are prerequisites for Book XXI: the solutions of a linear system are a matrix exponential, which is a power series, and linearising a nonlinear system means taking its Jacobian.
Corrected the same day. An earlier pass reported no calculus textbook of any kind. Two arrived within the hour and the ledger was re-run: Loomis & Sternberg, Advanced Calculus (revised edition, 592 pp) and Knill, Introduction to Calculus (Harvard Math 1a, 311 pp). The earlier statement was true of its snapshot and false within sixty minutes — the standing hazard of quoting a ledger instead of re-running it.
What remains not held is Leibniz himself — not the 1684 Nova Methodus, not a collected works, not a secondary study. A narrower gap, and it binds one chapter.
Also held: Newton's Principia (594 pp), Bradley's Leonhard Euler (543 pp), and Deisenroth, where the rule is stated on p. 146 and mechanised on p. 164.
Chapters 2, 3 and 4 can now be written — the rule, its mechanisation and the eighteenth century all have founding texts with addresses. Chapter 1 still cannot. Its argument is about what Leibniz's notation does that Newton's does not, and that needs Leibniz, not a modern textbook restating him. [OPEN]
Closed 2026-09-27, and the thesis revised. Leibniz 1684 (Dunham's facsimile and a Stoudt reprint scan), Newton's Method of Fluxions (Colson 1736) and Rumelhart, Hinton & Williams (1986) arrived. Read against Newton's Example 5, the claim in §1 that Newton's notation does not compose is false: both compose. Chapter 1 records the failed thesis and what replaces it. Newton's derivative is a ratio of rates against a common clock, which is forward mode; Leibniz's is a ratio of changes with no clock, which is what a backward sweep needs. All four chapters are written, and a fifth, on calculus in three dimensions, was added the same day.