Structured Preparation
Exercise SP-102
local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
Let p and q be real polynomials and a a real point. Suppose (x-a)^{k+1} divides the difference p-q. Prove that for every order j with 0 <= j <= k, the j-th derivatives of p and q agree at a: (d^j p/dx^j)(a) = (d^j q/dx^j)(a). Explain precisely why the hypothesis forces agreement of all jets strictly below the multiplicity k+1, and why it says nothing about the j = k+1 derivative in general.
Hint: mathematical route
A zero of multiplicity k+1 in p-q forces all derivatives through order k to agree at the point, with the bound sharp at order k+1.
- A zero of order k+1 differentiated j<=k times retains a zero of order k+1-j >= 1.
- Divisibility by (x-a) forces vanishing at a, so the j-th derivative of p-q is 0 at a.
- Linearity transfers this to equality of the individual jets of p and q for all j<=k, and the bound is sharp at k+1.
Reference solution
Set r = p - q, so (x-a)^{k+1} | r. Step 1 (differentiation lowers the zero order by at most j): differentiating a function with a zero of order m at a exactly j times leaves a zero of order at least m-j; formally, (x-a)^{m-j} divides the j-th derivative of r whenever (x-a)^m | r. With m = k+1 and j <= k we get m-j = k+1-j >= 1. Step 2: therefore (x-a)^{k+1-j} divides (d^j r/dx^j); since k+1-j >= 1, in particular (x-a)^1 = (x-a) divides the j-th derivative of r. Step 3: a polynomial divisible by (x-a) vanishes at a; evaluating (d^j r/dx^j) at a gives 0. Step 4: derivatives are linear, so (d^j r/dx^j)(a) = (d^j p/dx^j)(a) - (d^j q/dx^j)(a) = 0, i.e. the jets agree. Why only below the multiplicity: at j = k+1 we have m-j = 0, so the argument only yields (x-a)^0 = 1 dividing the derivative, a vacuous statement; the (k+1)-th derivatives need not agree. Concretely p - q = (x-a)^{k+1} has k-th derivative 0 at a but nonzero (k+1)-th derivative (k+1)!, witnessing that the bound is sharp.
Assessment rubric
- States that dividing by (x-a)^{k+1} and differentiating j<=k times leaves divisibility by (x-a)^{k+1-j} with exponent >= 1. (1 weight)
- Concludes (x-a) divides the j-th derivative of p-q, hence it vanishes at a. (1 weight)
- Uses linearity of the derivative to transfer vanishing of the difference's jet into equality of the jets of p and q. (1 weight)
- Explains sharpness: at order k+1 the exponent drops to 0, and p-q=(x-a)^{k+1} shows the (k+1)-th derivatives can differ. (1 weight)
Graph-grounded prerequisites
These are support/source anchors, not an automatically extracted theorem-dependency proof.
Lean view and evidence boundary
No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.
Sources and provenance
- QuantumBlockEncoding/HermitePolynomial.lean
lines 51-62: theorem jet_eq_of_pow_dvd_sub (p q : R[X]) (a : R) (k j : N) (hj : j <= k) (h : (X - C a)^(k+1) | p - q) : (derivative^[j] p).eval a = (derivative^[j] q).eval a; proof uses pow_sub_dvd_iterate_derivative_of_pow_dvd and X - C a | derivative^[j] (p-q)
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: 72a750b6a3fecacff3cef3a4a6404cb1b0796ff56e3ff9c2819e95a97b1432c9
Item digest: 68c0514f0b9677c677caf2ac29f4872c3571042ec82a12426c71df57763e6c00
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.