Exercise SP-111

Squared affine sampling has natural degree at most2*natDegree(q), with zero-step collapse explicitly allowed; any retained coefficient bound at least that value yields the exact Faulhaber discrete squared-mass formula for every sample count.

1. The predecessor's unconditional exact-degree equality fails at zero step. The squared affine sample instead has natDegree at most2*natDegree(q), with exact nonzero-step and constant/zero cases distinguished, so every sample is captured by a bound D>=2*natDegree(q).
2. Expanding the actual squared affine polynomial with trailing-zero coefficients and exchanging two finite sums gives M=sum_r g_r*sum_j j^r, valid for every exact real grid and natural count.
3. Substitution of the exact Faulhaber power-sum polynomial yields the degree-bounded expression, including zero count/step/polynomial and constants; expression size is not a finite-bit or coherent-oracle cost certificate.

The unconditional exact-degree assertion is false. For q(X)=X, start=1 and step=0, we have d=1 but g(X)=1, whose ordinary and natural degree are0, not2. With start=0 the same choice yields g=0, with natDegree(g)=0 and ordinary degree undefined or minus infinity according to the extended-degree convention. An affine substitution does not raise degree, but that inequality alone cannot justify an equality.

For every q, the affine polynomial start+step*X has natDegree at most1. Composition therefore has natDegree at most d, and squaring gives natDegree(g)<=2*d. The zero polynomial is covered using natDegree(0)=0. More explicitly, if step=0 then g is the constant polynomial q(start)^2: its natural degree is0, its ordinary degree is0 if q(start)!=0, and it is the zero polynomial otherwise. If step!=0 and q!=0 has leading coefficient a_d, the affine composite has nonzero leading coefficient a_d*step^d and exact degree d. Squaring gives leading coefficient a_d^2*step^(2*d), still nonzero, and exact degree2*d. If q=0 then g=0 regardless of step. A nonzero constant q=c gives g=c^2 and degree0 for every step. Thus the natural-degree equality holds for all q when step!=0, and at step=0 exactly when d=0; a positive-degree polynomial may collapse even if its sampled value is nonzero. No division by step is needed for the universal bound or the mass formula.

Since natDegree(g)<=2*d<=D, all coefficients above D vanish and for every real x the exact monomial expansion is g(x)=sum_{r=0}^{D} g_r*x^r. Substituting each integer sample index gives q(start+step*j)^2=g(j)=sum_{r=0}^{D} g_r*j^r. Hence M=sum_{j=0}^{count-1} sum_{r=0}^{D} g_r*j^r =sum_{r=0}^{D} g_r*sum_{j=0}^{count-1} j^r =sum_{r=0}^{D} g_r*P_r(count). The exchange is between two finite sums, and the last substitution is the exact Faulhaber identity. The upper bound D need not equal the actual degree of g; zero trailing coefficients are permitted. In particular choosing D=2*d always gives at most2*d+1 weighted power sums. This is an exact real/rational algebraic expression with a number of coefficient slots controlled by degree, not a continuum integral, asymptotic expansion or quadrature approximation.

For count=0 the original sum is empty and P_r(0)=0 for every r, so both sides are0. In particular P_0(N)=N, since the zeroth power is1 in polynomial evaluation, including j=0. For step=0, g_0=q(start)^2 and g_r=0 for r>=1, so the result reduces to M=count*q(start)^2, valid also when q(start)=0. For q=0 every coefficient and both sides are0. For a nonzero constant q=c it reduces to count*c^2; the same formula includes c=0. Negative or zero step and repeated sample locations do not invalidate any finite-sum identity.

The D+1 statement counts weighted power-sum slots, not unit-cost implementation steps in a bit model. If each P_r is expanded separately by a degree-r+1 Bernoulli formula, it has its own degree-dependent terms; powers of count and rational arithmetic still must be evaluated. The representation/precision costs of arbitrary real coefficients, the bit length of count and growth of exact integers/rationals are not bounded away by this identity. The source is an algebraic mass-evaluation leaf, not a free coherent oracle or state-preparation circuit. Static inspection of its degree-bound and sum-exchange proofs is not a new kernel certificate for this candidate.

1. Refutes the unconditional exact-degree claim with an allowed zero-step example; proves natDegree(g)<=2*d and correctly distinguishes step=0, step!=0, zero q, constant q and zero sampled-value cases, without adding step!=0 as a standing assumption. (1 weight)
2. Uses an upper coefficient bound D>=2*d, not a false exact-degree equality, expands g including trailing zeros and identifies g(j)=q(start+step*j)^2 for every sampled index. (1 weight)
3. Exchanges the two finite sums and substitutes the exact power-sum identity to obtain M=sum_{r=0}^{D} g_r*P_r(count), uniformly in all natural counts. (1 weight)
4. Checks count=0, P_0(N)=N, zero step, zero polynomial and constants; distinguishes exact algebraic expression size from quadrature, finite-bit runtime and any circuit/oracle certificate. (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/HermiteIntervalMass.lean

  lines 20-57: powerSumClosed count degree = sum_{i in range (degree+1)} bernoulli i * C(degree+1,i) * count^(degree+1-i)/(degree+1); powerSumClosed_eq : (powerSumClosed count degree : R) = sum_{j in range count} j^degree (via sum_range_pow); affineSquared p start step = (p.comp (C start + C step*X))^2; polynomialMassClosed_eq (h : affineSquared.natDegree <= bound) : polynomialMassClosed = sum_{j in range count} (p.eval (start+step*j))^2

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

Contract: 43fa4e5865634e668b2600393484ad6e44df32e9c848ead8e01b986715794b7f

Item digest: ad9afb52217bd9d006bb331601450ccf04dd24abd44b86ee895c6b4fe2fdc311

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-111", "predecessor_item_digest": "bd9b2d2da101f1db87e218c7ec51012ef6c990243065faefa15cd99c4985d4eb", "predecessor_contract_hash": "1c89646531e5e6897c0e8bc9ebaf2840d58c260824ce3d40d7ff57427cb09bc1", "current_contract_hash": "43fa4e5865634e668b2600393484ad6e44df32e9c848ead8e01b986715794b7f", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-111-question-degree-successor.json", "repair_record_digest": "470f9a8189d5265b0b901236ee73547481f404a08a5f0e443102e0a81252a436", "review_record": "reports/textbook-v1/repairs/sp-111-question-degree-successor-migration-revalidation-review.json", "review_digest": "58e87a7c9091ae4d2d8872d40c1667b8d559ed315223a20d165886b9e85c2988", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }