Structured Preparation
Exercise SP-107
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 natural k define the canonical real source coefficient polynomial by a_{k,r}=sum_{m=0}^r C(k+r-m,k)/m! for0<=r<=k and A_k(t)=sum_{r=0}^k a_{k,r}t^r. Equivalently it is the degree-k truncation of the formal series exp(t)/(1-t)^(k+1). Let F_k(t)=(1-t)^(k+1)A_k(t), H_k(t)=exp(-1)F_k(t)+F_k(1-t), and S_k(p)=H_k(p+1).
The predecessor specified only that A_k had degree<=k and asked why the endpoint values were exp(-1) and1. Explain why that degree condition alone cannot determine those values, using k=0 and a suitable constant-polynomial example. For the actual coefficient definition above, derive A_k(0)=1 rather than assuming it.
Explain why t=p+1 sends p=-1,0 to t=0,1 with no derivative scaling. Show how the two endpoint factors make each contribution and its derivatives of orders0,...,k vanish at the OPPOSITE endpoint, and then compute S_k(-1) and S_k(0). Distinguish this opposite-endpoint decoupling from specifying every derivative at the contribution's own endpoint; a full higher-jet derivation is not requested here.
Finally write the exact reflected expression H_k(1-t). State precisely what it means for reflection to exchange the two endpoint SHAPES and their assigned weights. Is H_k literally reflection invariant, or does H_k(1-t)=c H_k(t) hold for some fixed scalar c for all t? Decide this by its endpoint values. Include k=0 and preserve which shape carries exp(-1); do not move that weight to the other endpoint in the definition of the unreflected source.
Hint: mathematical route
The canonical source coefficients give A_k(0)=1, which a degree bound alone cannot supply. The shifted endpoint factors decouple opposite k-jets, and reflection exchanges shapes with their weights rather than leaving the unequal-weight source invariant.
- The source coefficient definition supplies its constant normalization, and t=p+1 sends physical nodes-1,0 to0,1 without derivative scaling.
- The factors(1-t)^(k+1) and t^(k+1) kill the opposite endpoint derivatives through k; this decoupling does not by itself prescribe every own-node jet.
- A_k(0)=1 gives the exact endpoint values with exp(-1) on F_k; reflection swaps the endpoint shapes/weights, not the fixed polynomial or a scalar multiple of it.
Reference solution
A degree bound alone says nothing about the constant coefficient. If k=0 and A_0=2, then the displayed generic weighted endpoint form is2exp(-1)(1-t)+2t; its endpoint values are2exp(-1) and2, not the requested values. This does not refute the actual canonical source polynomial; it shows why the predecessor's standalone description omitted load-bearing normalization. In the canonical definition, a_{k,0}=C(k,k)/0!=1, and evaluating A_k at0 retains exactly that constant coefficient. Thus A_k(0)=1 for every k. This follows from the supplied finite source coefficients, not from degree<=k or a new normalization hypothesis.
Set t=p+1. Then p=-1 gives t=0, p=0 gives t=1 and dt/dp=1, so ordinary differentiation in p adds no scale factor. F_k(t) has the factor(1-t)^(k+1); by repeated product differentiation, every derivative of order j<=k still vanishes at t=1. Its reflection F_k(1-t)=t^(k+1)A_k(1-t) and its derivatives through order k vanish at t=0. Therefore the unreflected exp(-1)F_k term contributes no k-jet at the right node, while the reflected F_k(1-t) term contributes no k-jet at the left node. Those opposite-node zeros decouple the two contributions. They alone would not determine all derivatives at the responsible node; the actual coefficient identities supply further own-node information, outside this question's requested proof.
For the endpoint values, F_k(0)=A_k(0)=1 and F_k(1)=0 because k+1>=1. Thus H_k(0)=exp(-1),H_k(1)=1 and S_k(-1)=exp(-1),S_k(0)=1, with the exponential weight on the UNREFLECTED F_k term. No interior or nonzero-k assumption is needed. At k=0,A_0=1,F_0(t)=1-t and H_0(t)=exp(-1)(1-t)+t.
The exact reflected expression is H_k(1-t)=exp(-1)F_k(1-t)+F_k(t). Reflection exchanges the ordered shape pair(F_k(t),F_k(1-t)). Expressed again against the unreflected ordered pair, the weights change from(exp(-1),1) to(1,exp(-1)). More generally H_{a,b}(t)=aF_k(t)+bF_k(1-t) obeys H_{a,b}(1-t)=H_{b,a}(t). This is weighted SHAPE exchange, not invariance of the fixed-weight polynomial. Literal invariance already fails because H_k(0)!=H_k(1). If H_k(1-t)=c H_k(t) held for all t, t=0 would give c=exp(1), while t=1 would give c=exp(-1); these are unequal. Thus no such fixed scalar exists. The k=0 linear example shows the same failure directly.
This is the same canonical endpoint decomposition in the production definitions. The corrected question makes its coefficient normalization explicit and replaces ambiguous 'symmetry up to a constant' by an exact weighted-reflection identity. Static inspection of the local source/theorem proofs is not new Lean execution, a new circuit/resource theorem or an external-paper fidelity seal.
Assessment rubric
- Explains degree alone does not force the required endpoint normalization, gives a valid k=0 constant counterexample, and derives A_k(0)=1 from the actual finite coefficient definition. (1 weight)
- Uses t=p+1 with correct endpoint/order and no derivative scale, and proves opposite-node derivatives through k vanish from the(k+1) factors without conflating decoupling with all own-node jet values. (1 weight)
- Computes F_k(0)=1,F_k(1)=0 and hence S_k(-1)=exp(-1),S_k(0)=1, including k=0 and the correct source weight orientation. (1 weight)
- Writes the exact reflected shape/weight exchange and refutes literal invariance or fixed scalar covariance using endpoint values; does not call the unequal-weight polynomial symmetric in the invariant sense. (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 176-182,288-308: endpointFactor k = (1-X)^(k+1) * coefficientPolynomial k; sourceInterpolant k = taylor 1 (C(exp(-1))*endpointFactor k + (endpointFactor k).comp(1-X)); sourceInterpolant_eval (k p) : eval p = exp(-1)*(1-(p+1))^(k+1)*A_k(p+1) + (p+1)^(k+1)*A_k(1-(p+1))
Source SHA-256:f8a3e1d5f29aed1228b6ede3577a9af1e76301559172ee67a266fcb0d56fee1e· MIT (repository LICENSE)
Contract: 9109484ddca89403a139199617fb30ffe7e0cb7862778d9cf38f0e09223dcbc3
Item digest: 57ed32498781ddea98e9e57375e919b798bb2f47c40f922e7ad4595a6a50750b
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-107", "predecessor_item_digest": "3edb854fbc6b1caef98b17e0be51e11cfabd70712e0a0852d776b4a990fc7075", "predecessor_contract_hash": "74f67ca96f4d2d3fddf5b38276976be1291002a448bf81f9447f09e0bbf392e6", "current_contract_hash": "9109484ddca89403a139199617fb30ffe7e0cb7862778d9cf38f0e09223dcbc3", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-107-coefficient-reflection-state-successor.json", "repair_record_digest": "067930875932fba4ea81c92628ca8db49352fd1a4bd6689877842e844954e138", "review_record": "reports/textbook-v1/repairs/sp-107-coefficient-reflection-state-successor-review.json", "review_digest": "465cec2834a13cf54e6c928500fdedf7584327bcdad99e6384a6e76dcacb3e19", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }