Exercise SP-104

Two degree-<=2k+1 polynomials with matching k-jets at both endpoints coincide, by coprime endpoint moduli and a degree-count against the combined multiplicity 2k+2.

1. Jet agreement through order k at a node is equivalent to divisibility by (x-node)^{k+1}, applied at -1 and 0.
2. The two endpoint moduli are coprime, so their product divides p-q.
3. The product has degree 2k+2 while deg(p-q) <= 2k+1, forcing p-q = 0.

Step 1 (each endpoint gives a divisibility): since p and q share all jets through order k at -1, the difference p-q has a zero of order at least k+1 at -1, i.e. (x+1)^{k+1} divides p-q. The equivalence used is: agreement of all derivatives through order k at a point a is equivalent to (x-a)^{k+1} dividing the difference (one direction is the high-multiplicity-zero fact; the converse is proved by reading Taylor coefficients, all of which through degree k vanish). The same at 0 gives x^{k+1} divides p-q. Step 2 (coprimality combines the two): (x+1)^{k+1} and x^{k+1} are coprime because their bases x+1 and x differ by a unit (their difference is 1), and coprimality is preserved under taking powers. For coprime factors each dividing the same element, their product divides it; hence (x+1)^{k+1} * x^{k+1} divides p-q. Step 3 (degree accounting forces zero difference): the product has degree (k+1)+(k+1) = 2k+2. If p-q were nonzero, a nonzero multiple of a degree-(2k+2) polynomial would have degree at least 2k+2. But deg(p-q) <= max(deg p, deg q) <= 2k+1 < 2k+2, a contradiction. Therefore p-q = 0, i.e. p = q. The degree budget 2k+1 is exactly one below the combined multiplicity 2k+2, which is what makes the only common solution the zero difference; coprimality is what lets the two separate divisibilities multiply.

1. Translates jet agreement at each node into divisibility of p-q by (x+1)^{k+1} and by x^{k+1} respectively (both directions of the equivalence). (1 weight)
2. Establishes coprimality of the two endpoint moduli (bases differ by a unit, preserved under powers) to multiply the divisibilities. (1 weight)
3. Computes the product degree 2k+2 and compares with the degree budget 2k+1 on p-q. (1 weight)
4. Concludes p-q=0 since a nonzero multiple of the degree-(2k+2) product cannot have degree <= 2k+1, and identifies 2k+1 as the sharp budget. (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/HermitePolynomial.lean

  lines 119-127: leftModulus k = (X - C(-1))^(k+1); rightModulus k = (X - C 0)^(k+1); endpointModuli_coprime k : IsCoprime. lines 380-417: pow_dvd_sub_of_jet_eq (p q a k) (h : forall j<=k, jets equal) : (X-C a)^(k+1) | p - q; sourceInterpolant_unique (k p) (hp : natDegree <= 2k+1) (hl hr : endpoint jets) : p = sourceInterpolant k

  Source SHA-256: f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e · MIT (repository LICENSE)

Contract: 7bbea63cce5e0f098f5b8294acda383c03cffca10fc69df2ddc12d1d2c8f4741

Item digest: 10130b96d45745bf1b25df4c137ef2168b7368cb7eef7fb384197c1df6db6fc7

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.