Structured Preparation
Exercise SP-119
local source supported. Explicit question version 2 with distinct contract-change review; the predecessor question is not equivalent current gold. Core, family and split are retained. No new Lean verification is claimed for this NL view.
Assumptions and conventions
This question explicitly revises its historical contract. A Lean companion must bind the current contract hash, not the predecessor hash. This is one reserved core, not two exercises.
Question
For each natural smoothing order k, let S_k(p) be the actual polynomial (HermitePolynomial.sourceInterpolant k).eval p. To fix this family unambiguously, put t=p+1, a_{k,r}=sum_{m=0}^r binom(k+r-m,k)/m!, A_k(t)=sum_{r=0}^k a_{k,r}t^r, and S_k(p)=exp(-1)(1-t)^(k+1)A_k(t)+t^(k+1)A_k(1-t). Define f_k(p)=exp(p) for p<-1, S_k(p) for -1<=p<=0, and exp(-p) for p>0. Thus both S_k and f_k depend on k.
As in the predecessor, you may use the established endpoint jets: for every integer order 0<=j<=k, S_k^(j)(-1)=exp(-1) and S_k^(j)(0)=(-1)^j. No reproof of the coefficient or endpoint-jet construction is requested. Use the reusable finite-order gluing theorem: if real functions u,v are globally C^k and have equal derivatives through order k at c, then splice_c(u,v)(p), defined as u(p) for p<c and v(p) for p>=c, is globally C^k.
Fix k and prove f_k is globally C^k by applying this SAME theorem first at 0 and then at -1. Justify equality of all needed jets of the inner splice with S_k near -1 by local eventual equality, not merely equality at the single point. Prove that the nested right-valued splices equal the literal middle-inclusive f_k at every point, checking p=-1 and p=0 explicitly. State the conclusion with its quantifiers as forall k in N, f_k belongs to C^k(R).
Does this conclusion say that one fixed member f_{k0} is C^r for every r, or that one fixed polynomial splice is C-infinity? Assess that stronger reading using the actual k=0 member: derive S_0 and compute the one-sided derivatives of f_0 at p=0. Keep this finite-order family result separate from any circuit, normalizer, resource or finite-bit assertion.
Hint: mathematical route
Each finite-order source bridge S_k yields its own f_k, globally C^k by two finite-order gluings and exact boundary-convention reconciliation. This indexed-family theorem is not infinite smoothness of a fixed member; the canonical f_0 is continuous but not differentiable at0.
- For a fixed smoothing order k, the polynomial S_k and right exponential glue C^k at0 using their matching analytic jets through k.
- Near -1 the inner right splice equals S_k on an open neighborhood, so its jets agree there; the left exponential glues to it C^k at -1 using the same finite-order theorem.
- The nested right-valued splices equal the middle-inclusive f_k, including both junctions, hence forall k,C^k(f_k). The explicit source k=0 member has unequal derivatives at0 and refutes C-infinity of one fixed target.
Reference solution
Fix one natural k throughout the two gluing applications. Write R_k=splice_0(S_k,exp(-.)) and D_k=splice_{-1}(exp,R_k). The polynomial S_k and both exponentials are globally C^k. Their analytic derivatives at zero are S_k^(j)(0)=(-1)^j and (d^j/dp^j)exp(-p)|_0=(-1)^j exp(0)=(-1)^j for all j<=k. The first application of the finite-order gluing theorem therefore gives R_k in C^k(R). These are analytic jets: for a real polynomial, ordinary iterated derivatives of its evaluation agree with evaluation of iterated formal derivatives, as the source adapter proves.
For the second application, choose any open neighborhood of -1 lying strictly below0, for example(-3/2,-1/2). On every point of that neighborhood R_k(p)=S_k(p), since the inner splice takes its polynomial branch for p<0. Consequently R_k and S_k have the same derivatives of every order at -1 (germs/local eventual equality, not an inference from a single function value). In particular for j<=k, R_k^(j)(-1)=S_k^(j)(-1)=exp(-1). The j-th derivative of exp(p) at -1 is also exp(-1). Both exp and R_k are already C^k, so the second use of the same theorem yields D_k in C^k(R).
The gluing theorem includes its cut point. Its proof can be understood by induction on the finite order: for k=0, equal values and continuity of both branches give continuity across the cut; for a successor, equal values and first derivatives give a common difference-quotient limit at the cut, while neighborhoods away from it select one branch. The derivative is the splice of the branch derivatives, whose remaining jets agree through the lower order, so induction applies. This explains why the full jets, not merely the endpoint values, are consumed; no infinite-order premise has been added.
Identify D_k with the exact f_k. For p<-1, both equal exp(p). At p=-1, the OUTER splice takes R_k(-1), and -1<0 forces R_k(-1)=S_k(-1), just as f_k does. For -1<p<0, both equal S_k(p). At p=0, D_k takes the RIGHT exponential value exp(0)=1, whereas f_k takes the middle polynomial value S_k(0)=(-1)^0=1; this zeroth jet reconciles their different branch conventions. For p>0, both equal exp(-p). Thus D_k=f_k pointwise, including both junctions, and f_k is globally C^k.
Now quantify over the order used to CONSTRUCT the family: for every k in N, C^k(f_k). This is not forall r,C^r(f_{k0}) for a fixed k0, nor C-infinity of one fixed target. For k=0, a_{0,0}=1 and A_0=1, so the exact formula becomes S_0(p)=exp(-1)(1-(p+1))+(p+1)=1+(1-exp(-1))p. The literal f_0 has f_0(0)=1, is this linear polynomial immediately to the left of0, and is exp(-p) immediately to its right. Therefore its left derivative at0 is1-exp(-1)>0, whereas its right derivative is-1. They differ, so f_0 is not differentiable at0 and in particular is not C^1, despite being globally C^0 by the proved k=0 case. This canonical member refutes the stronger unindexed all-orders reading. It does not claim an exact maximal regularity formula for every other k.
All parameters and the two cuts are unchanged from the source target; strict positivity, grid sampling, normalization, ancillas and resource costs are not needed for this regularity proof. Static inspection of the existing full proofs is not a new Lean execution, external-paper seal or admitted formal companion.
Assessment rubric
- Fixes one smoothing order k, defines the inner right splice and outer left splice in the correct order, and applies finite-order gluing at0 using polynomial/exponential C^k regularity and matching jets through k. (1 weight)
- Justifies local eventual equality R_k=S_k on a neighborhood strictly below0 around -1, transports derivatives through k, and applies the SAME gluing theorem again at -1 using exp's jets. (1 weight)
- Proves exact equality of the double splice with f_k in all regions, explicitly checking the middle value at -1 and the p=0 branch mismatch via S_k(0)=exp(0)=1. (1 weight)
- States forall k,C^k(f_k), not C-infinity of a fixed member. Derives S_0=1+(1-exp(-1))p and unequal one-sided derivatives1-exp(-1) and-1 at0, so f_0 is not C^1. Does not overclaim maximal regularity, circuit or computational consequences. (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/HermiteSmoothness.lean
lines 99-147: contDiff_right_splice k : ContDiff k (splice 0 (S) (exp(-.))) via sourceInterpolant_right_iteratedDeriv and iteratedDeriv_exp_neg; right_splice_eventuallyEq : the right splice =f near -1 equals S; contDiff_double_splice k uses iteratedDeriv_exp and sourceInterpolant_left_iteratedDeriv; smoothInitial_eq_double_splice; smoothInitial_contDiff k : ContDiff k (smoothInitial k)
Source SHA-256:da47568584b8435a07431a7ebae29836796018f76d02b4d8b0c4169830ec68bc· MIT (repository LICENSE)
Contract: 5139594d8e003d84aa5ff57197bb73cd7cf709141dcf6e8c5872c139912e3c68
Item digest: 58d06db209ab05bc1f263c33a9bf0275e53a0d2f57e4850f8dd28f5a6143bb8b
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Question revision lineage
{ "question_version": 2, "predecessor_key": "qcb-core-sp-119", "predecessor_item_digest": "040f53d31ca55c21c402b682f39e82941f9decafb2374dbed92e8d3d8bc47194", "predecessor_contract_hash": "3cca256fbe1e92a6a60deb68dd6a466510b411317f18ebd99ddc3fb3875e292a", "current_contract_hash": "5139594d8e003d84aa5ff57197bb73cd7cf709141dcf6e8c5872c139912e3c68", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-119-indexed-smoothness-state-successor.json", "repair_record_digest": "f2a3ae41db0d0615af7123de249e67f5598a0a130b68630cf1640482de672172", "review_record": "reports/textbook-v1/repairs/sp-119-indexed-smoothness-state-successor-review.json", "review_digest": "c5812711a6557b4fbef0d669092570a7b5cbd1851a0a23951f4dbbb0c92180af", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }