Every calculus course teaches the chain rule as a cancellation, dz/dx = dz/dy · dy/dx, and every rigorous text then adds that the cancellation is not what is really happening. This chapter follows the rule through three held texts, from the fraction to the linear map. It then applies the rule to this corpus's own operator chain and finds something the corpus had not said.
Oliver Knill's Harvard course introduces the rule in Unit 10 with sin(x7): take the derivative of the inside, multiply by the derivative of the outside evaluated at the inside, and get 7x6 cos(x7). He adds that avoiding the rule by expanding a power by hand “is called the pain rule”. His justification is the one most people remember: write the difference quotient of f(g(x)) as a product of two quotients, the second over h and the first over H = g(x+h) − g(x), and let both go to zero CITED.
That is Leibniz's notation doing the thinking. Written as fractions, the dy's cancel, and the rule looks like arithmetic. Chapter 1 of this volume will argue from Leibniz's own text why that property mattered historically. It is waiting for the 1684 paper to be held. This chapter is about what the property is worth mathematically.
The cancellation argument divides by H, and H can be zero. Take g(x) = x² sin(1/x) with g(0) = 0. It is differentiable at 0 with g′(0) = 0, yet g(h) = 0 exactly at every h = 1/(kπ), points that crowd in on zero. At each of them H = 0 and the “first quotient” is 0/0 COMPUTED. The rule itself is still true there. The derivative of exp(g(x)) at 0 is exp(0) · 0 = 0, and the script's difference quotients go to zero with it. What fails is the proof.
Deisenroth, Faisal and Ong say the same thing in a margin note beside their statement of the rule (p. 148): the fraction reading “is only an intuition, but not mathematically correct since the partial derivative is not a fraction.” Their own gloss is more useful than the cancellation. The factors behave like matrices whose inner dimensions must match, and “∂f cancels” is what matching dimensions look like CITED.
Loomis and Sternberg state the version that needs no fractions (Theorem 6.2, p. 143). If F is differentiable at a and G is differentiable at F(a), then G ∘ F is differentiable at a, and
The differential of a composite is the composite of the differentials. Each d is a linear map, the best linear approximation at a point, and the proof on p. 144 is a chain of equalities that never divides by anything. In coordinates the linear maps are Jacobian matrices and composition is matrix multiplication. That is Deisenroth's “neighbouring dimensions have to match”, now as a theorem.
Two things follow, and the script checks both on a pair of maps of the plane. The rule holds in both orders: d(f∘g) = dfg(x)·dgx and d(g∘f) = dgf(x)·dfx, to six decimal places. And the two orders give different derivatives, differing by 0.99 in their largest entry COMPUTED. Matrix products do not commute, so composition order shows up in the derivative. That is the bridge to the next section.
This series composes four operators and calls the result the generator, G = U ∘ F ∘ K ∘ C. In AMonster/dm3_operators.lean they are written out as explicit maps of (r, θ, z):
| operator | map | Jacobian |
|---|---|---|
| C₃ constraint | z ↦ r²θ | identity except the z-row, which is (2rθ, r², 0) |
| K₃ kinetics | z ↦ z + 1 | the identity |
| F₃ fold | r ↦ r below κ, 2κ − r above | radial slope +1 or −1 |
| U₃ unfold | r ↦ r₀ + (r − r₀)e−1 | radial slope e−1 |
At two sample states, one on each side of the fold, the Jacobian of G₃ equals the product dU₃·dF₃·dK₃·dC₃, each evaluated where the chain passes COMPUTED. The corpus's generator is a composite map, and its derivative is Leibniz's rule. That is the thesis of this volume, checked on the corpus's own definitions.
The Lean file's first theorem is that constraint and kinetics do not commute: C₃(K₃(1,1,0)) = (1,1,1) while K₃(C₃(1,1,0)) = (1,1,2). That is true, and the script reproduces it. But their derivatives are identical everywhere the script looks. dK₃ is the identity, and C₃ ignores the incoming z, so d(C₃∘K₃) = d(K₃∘C₃) COMPUTED. The two orders differ by a constant shift, and a derivative cannot see a constant. The corpus's showcase non-commutation is invisible to first order.
Other pairs are different. Constraint and unfold do not commute, and neither do their derivatives: d(C₃∘U₃) and d(U₃∘C₃) differ by 1.26 in their largest entry at (1,1,0), because C₃'s Jacobian depends on r and U₃ moves it. If the series wants an order effect that survives linearisation, which is what every gradient-based method sees, this is the pair to cite, not the first theorem. MODEL — computed at sample points from the definitions; no derivative is stated or proved in the Lean file.
The fold has slope +1 just below κ and −1 just above. At r = κ it has a corner and no derivative, so the rule has nothing to say there COMPUTED. That point is exactly where the series locates its transition. A method that differentiates through G, such as Chapter 3's backpropagation, works on either side of the threshold and is blind at it. OPEN — whether the corpus's other definitions of F are smooth at the fold is not checked here.