Exercise SP-108

The endpoint-factor term has exact degree i+k+1, not generally k+1; its exact representation in degree2k+1 Bernstein coordinates yields nonnegative coefficients for the same weighted source interpolant.

1. The nonzero leading term has degree i+k+1, refuting the predecessor's universal k+1 description; on each allowed index, positive binomial cancellation gives the exact single-term elevation factorization.
2. The finite binomial sum equals (t+(1-t))^(k-i)=1, so the ambient-degree2k+1 Bernstein expansion holds for every real t, including the endpoint and k=0 cases.
3. Collecting nonnegative source coefficients and weights, then forming exp(-1)L_r+L_{2k+1-r}, gives the source coefficient vector; its nonnegativity and nonnegative basis values imply the source polynomial is nonnegative on [0,1].

The predecessor's universal degree description is false. The factor (1-t)^(k+1) has leading term (-1)^(k+1)*t^(k+1); multiplying by t^i gives the nonzero leading coefficient (-1)^(k+1) at degree i+k+1. This equals k+1 exactly when i=0. For k=i=1 the term is t*(1-t)^2=t-2*t^2+t^3, of degree3 rather than2. Since i<=k, its actual degree is at most d=2*k+1, reaching d when i=k. The degree-d Bernstein basis is an ambient representation choice, not an assertion that every term has exact degree d. These terms are never zero or constant polynomials, since k+1>=1 and their leading coefficients are nonzero.

For 0<=j<=k-i we have 0<=i+j<=k<=d, hence C(d,i+j)>0 and its real reciprocal is defined. Multiplication cancels that binomial factor in w*B. The exponent relation d-(i+j)=(k+1)+(k-i-j) then gives w(k,i,j)*B_{d,i+j}(t)=t^i*(1-t)^(k+1)*C(k-i,j)*t^j*(1-t)^(k-i-j). Summing over j yields the fixed endpoint term multiplied by (t+(1-t))^(k-i)=1, by the binomial theorem. This proves the polynomial identity, hence its evaluation at every real t; no division by t or 1-t occurs. For i=k the sum has only j=0 and gives w=1/C(d,k), with no increase in actual degree. For i=0 it is the usual expansion of (1-t)^(k+1) into this ambient basis. For k=0 necessarily i=j=0 and the identity is B_{1,0}(t)=1-t. At t=0 or1 the same polynomial evaluations remain valid, using the standard constant-polynomial convention t^0=1, including 0^0=1 in such evaluations.

Each a_{k,i} is nonnegative, because every binomial numerator is nonnegative and m! is a positive real number. For r=0,...,d define L_{k,r}=sum_{i=0}^{k} sum_{j=0}^{k-i} [r=i+j]*a_{k,i}*w(k,i,j), where the bracket is1 when the index equality holds and0 otherwise. Finite collection of the exact single-term identities gives F_k(t)=sum_{r=0}^{d} L_{k,r}*B_{d,r}(t). All L_{k,r} are nonnegative, and L_{k,r}=0 for r>k. The reflection identity B_{d,r}(1-t)=B_{d,d-r}(t) gives F_k(1-t)=sum_{r=0}^{d} L_{k,d-r}*B_{d,r}(t). Therefore H_k(t)=sum_{r=0}^{d} c_{k,r}*B_{d,r}(t), with c_{k,r}=exp(-1)*L_{k,r}+L_{k,d-r}>=0. The positive exponential weight multiplies the unreflected F_k, exactly as in the source formula; it is not moved to the other endpoint. This is the degree-d coefficient vector for the same H_k. Its nonnegativity is a statement about real coefficients, independent of t. On [0,1] the powers in every B_{d,r} are nonnegative, so the displayed sum implies H_k(t)>=0. The coefficient positivity alone makes no claim about signs of the basis outside that interval. At k=0 the coefficients are exp(-1) and1 and H_0(t)=exp(-1)*(1-t)+t, consistent with all formulas.

This answer reconstructs the source mathematics statically. The inspected elevation and coefficient lemmas support the identities/nonnegativity; no exact-degree lemma or new native formal proof is asserted merely because the source module exists.

1. Explicitly refutes the universal exact-degree k+1 description, derives nonzero leading coefficient (-1)^(k+1) and exact degree i+k+1, gives a valid allowed counterexample, and distinguishes actual term degree from ambient Bernstein degree2k+1. (1 weight)
2. Checks C(2k+1,i+j)>0 on the full summation range, cancels it, splits the exponent correctly and sums by the binomial theorem to prove the identity for all real t, including endpoint evaluations and i=0/i=k/k=0. (1 weight)
3. Uses the actual nonnegative source coefficients a_{k,i}, collects them into L_{k,r}, and reflects indices to give c_{k,r}=exp(-1)L_{k,r}+L_{k,2k+1-r}, preserving the source coordinate/weight orientation. (1 weight)
4. Proves coefficient nonnegativity independently of t and only then uses basis nonnegativity on [0,1] to conclude H_k>=0; does not claim an exact degree for every represented polynomial or a fresh formal admission. (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/HermiteBernstein.lean

  lines 50-84: elevationWeight k i j = C(k-i,j)/C(2k+1,i+j); elevation_term : weight * basis (2k+1) (i+j) t = t^i (1-t)^(k+1) * C(k-i,j) * t^j * (1-t)^(k-i-j); elevation_sum : sum_{j in range (k-i+1)} weight*basis = t^i (1-t)^(k+1) via add_pow. lines 166-173: sourceBernsteinCoefficient_nonneg

  Source SHA-256: 661618d9c10826491ee293c7c411ac2d55056426739f4bbfd3e7c410c05e4bff · MIT (repository LICENSE)

Contract: cadcbadd693451e8bdb77013bce1d01119d42dd0ea6083150acda0c8b2969f50

Item digest: 7ac3b4a42b4938b05810a34d1f1499f78762790a5aeed2b602759e1476caaaee

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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

{ "question_version": 2, "predecessor_key": "qcb-core-sp-108", "predecessor_item_digest": "f857c429fedee80ac422ff286d3c82d03a902fb323bfeb8787effb1826e5a490", "predecessor_contract_hash": "0c40b3818a787101bd8d762d33210b70f3847eb30289dc997d15279634febffa", "current_contract_hash": "cadcbadd693451e8bdb77013bce1d01119d42dd0ea6083150acda0c8b2969f50", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-108-question-degree-successor.json", "repair_record_digest": "124f75cdf35d89a6bbf0df3c9aa618e59138f2c132663078bbc6e2ce0807383f", "review_record": "reports/textbook-v1/repairs/sp-108-question-degree-successor-migration-revalidation-review.json", "review_digest": "3e48012ae399699e5b2ce38eda393a00930cce32789b1396bb0588ca1ce1171b", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }