Structured Preparation
Exercise SP-105
nl bridge from inspected source. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
Question
A colleague claims that the two-point jet data 'all derivatives through order k agree at -1 and at 0' pins down a real polynomial uniquely, with no restriction on its degree. Show this is false by exhibiting an explicit nonzero polynomial of degree 2k+2 all of whose derivatives through order k vanish at both -1 and 0. Conclude that the degree bound 2k+1 in the uniqueness statement cannot be dropped, and state the exact dimension of the space of polynomials sharing a fixed set of such endpoint jets.
Hint: mathematical route
The vanishing-jet kernel is E*R[x] for E=(x+1)^(k+1)*x^(k+1). Fixed endpoint jets form a nonempty affine coset of countably infinite real dimension; the degree-2k+1 slice is one point and the next degree already defeats uniqueness.
- The nonzero monic E of degree 2k+2 has multiplicity k+1 at both endpoints, so it carries all-zero endpoint k-jets.
- A difference preserves all fixed jets exactly when it is a multiple of E; adding E gives a distinct solution while the degree-2k+1 slice remains unique.
- The full nonempty affine coset p0+E*R[x] has translation-space basis E*x^m and countably infinite real affine dimension. The degree-at-most-2k+1+d slice instead has affine dimension d for d>=0; this dimension reasoning is an NL extension, not a new compiled Lean theorem.
Reference solution
Let k be a nonnegative integer and set E(x)=(x+1)^(k+1)*x^(k+1). This is monic of degree 2k+2, hence nonzero. Its zero of multiplicity k+1 at each endpoint makes every derivative of order 0 through k vanish at -1 and at 0. Thus if p is any solution to given endpoint data, p+E is a distinct solution with the same data: uniqueness fails without a degree restriction.
For the exact solution space, first choose the degree-at-most-2k+1 Hermite interpolant p0 of the fixed data. Such a p0 exists for arbitrary real endpoint jets: use the Taylor coefficients v_j/j! at the two distinct nodes and the Chinese remainder theorem for the coprime moduli (x+1)^(k+1) and x^(k+1). A polynomial p has those same jets exactly when p-p0 is divisible by both moduli, equivalently by their product E. Therefore the complete solution set is the affine coset p0+E*R[x]. Its translation space E*R[x] has the countably infinite real basis {E*x^m : m=0,1,2,...}: it spans because every polynomial multiplier has finitely many monomials, and it is linearly independent because E is nonzero and R[x] is an integral domain. The unrestricted real affine dimension is consequently countably infinite, not a finite number and not the cardinality of the set of real coefficients. In general the solution set is affine rather than a vector subspace; it is a vector subspace precisely for all-zero prescribed jets.
For comparison, if the degree is capped at 2k+1+d with an integer d>=0, then the possible multipliers of E have degree <d, so the affine dimension is d. At d=0 only p0 remains; at d=1 the new direction is E. Nonzero differences divisible by E cannot have degree below 2k+2, proving uniqueness at degree at most 2k+1 and its sharp failure at the next degree. The countably infinite affine-dimension argument is natural-language linear algebra over the inspected source interfaces, not a claim that a new Lean dimension theorem was compiled.
Assessment rubric
- Exhibits monic nonzero E=(x+1)^(k+1)*x^(k+1) of degree 2k+2 and uses multiplicity k+1 to prove all endpoint derivatives through order k vanish. (1 weight)
- Adds E to a solution to refute unrestricted uniqueness and explains why degree at most 2k+1 rules out a nonzero E-divisible difference. (1 weight)
- Identifies all solutions as the nonempty affine coset p0+E*R[x], using the two coprime endpoint moduli and existence of the degree-bounded Hermite interpolant. (1 weight)
- Explicitly gives countably infinite real affine dimension in the unrestricted case, with translation-space basis {E*x^m}. Does not substitute only a finite degree-capped dimension or confuse affine dimension with the cardinality of the solution set. (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 119-166: leftModulus k = (X-C(-1))^(k+1), rightModulus k = (X-C 0)^(k+1); interpolant degree <= 2k+1; product (leftModulus*rightModulus).natDegree = 2k+2 used in uniqueness degree count. lines 394-417: sourceInterpolant_unique requires hp : natDegree <= 2k+1
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: e239c4f961247b71d53bc63f03b5731eac7660e8dd9d5a253d3a45ba183fd15c
Item digest: 7a9a04f7d42afb7e8df78d995ac2f8c887d0e54dd1ce5d16e5bf558014d278c4
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "fd8583539b598362720ad73856121d268dbc99230408318a2d7a311621b422dc", "predecessor_key": "qcb-core-sp-105", "repair_record": "shared/repairs/sp-105-affine-dimension-repair.json", "repair_record_digest": "3e6bc43d7c1c1f10a8a83c16b1fa833dcdb3f8a55662ec5273d302f520b1063f", "review_record": "reports/textbook-v1/repairs/sp-105-affine-dimension-repair-review.json", "review_digest": "4819b114fed21a7058e879f3f5bda48c3efd08126aefc3edb1b45c633d772a8e" }