Structured Preparation
Exercise SP-113
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
Let k,n be natural numbers and L>0. The actual real source target is f_k(p)=HermitePolynomial.smoothInitial(k,p): on the splice interval[-1,0] it equals the source Hermite bridge S_k, whose order-zero right endpoint identity is S_k(0)=(-1)^0=1. Thus f_k(0)=1. Its strict positivity at every real p is also known as a SEPARATE source fact.
Use the actual left-inclusive grid on an(n+1)-qubit register: M=2^(n+1), j=0,...,M-1, p_j=-pi L+j*(2 pi L/M). The integer index j is represented in little-endian order, j=sum_{i=0}^n bit_i*2^i. Define raw amplitudes a_j=f_k(p_j) and the unnormalized squared sample mass N=sum_{j=0}^{M-1}a_j^2. Prove N>=1 uniformly in k,n,L, explicitly locating and checking the unit sample. Deduce sqrt(N)>0 without using strict positivity of all samples.
Assess the predecessor's explanation that strict positivity is what makes this unit-grid anchor 'honest' or realizes it as an actual sample. Which exact facts actually realize the unit sample, and what role does strict positivity have in THIS inequality and its nonzero-normalizer consequence? Show by a strictly positive finite sample-table example that positivity alone need not give mass>=1 or a unit-valued sample. This example is a logical test of that proposed proof principle, not a claim about the actual source target. Discuss n=0 carefully: it means one qubit here, not a zero-qubit table. Do not infer preparation-circuit correctness or a success-probability bound from unnormalized mass alone.
Hint: mathematical route
The unit conditioning anchor comes from the actual central grid index and the exact endpoint value, not from strict positivity. One squared unit term proves mass>=1 and a nonzero normalizer; positivity is a separate structural theorem.
- The actual index2^n lies in the(n+1)-qubit grid and its physical point is0 by direct substitution; n=0 is a one-qubit case.
- The zeroth right endpoint identity gives f_k(0)=1 and therefore the actual central sample is1; positivity does not produce this equality.
- Nonnegative squares give N>=1 from the central unit term and hence a nonzero normalizer, without strict positivity. A separate positive-table counterexample shows positivity alone supplies no unit lower bound.
Reference solution
Let c=2^n. Since c>0 and M=2^(n+1)=2c, we have0<=c<M, so c is a genuine index in the specified register. In little-endian bits its only nonzero bit is bit_n; the proof then uses its actual natural integer value c. Substituting into the stated grid gives p_c=-pi L+2^n*(2 pi L/2^(n+1))=-pi L+pi L=0. This identity is independent of the function's signs and of k. For n=0 the register has M=2 points and c=1, so the same calculation holds on one qubit; this is not a claim about a zero-qubit single-point grid.
At that physical point the source middle branch applies. Its zeroth right endpoint jet is S_k(0)=(-1)^0=1, hence f_k(0)=1 and a_c=1. This endpoint identity and the explicit grid-index identity are the TWO facts that realize an actual unit sample. The source lemma smoothInitial_zero derives that value from sourceInterpolant_right_jet at order0; it is not deduced from positivity.
Every real square is nonnegative, regardless of the amplitude's sign. Therefore N=a_c^2+sum_{j!=c}a_j^2=1+sum_{j!=c}a_j^2>=1. In particular N>0 and sqrt(N)>=1>0, so this normalizer is well defined and nonzero. The inference uses only one unit sample and nonnegative squares; it never calls strict positivity of the other amplitudes. Width/order/scale uniformity comes from the same central point and endpoint value persisting for all stipulated k,n,L.
The old positivity-as-anchor explanation is incorrect. Positivity alone cannot locate a sample equal to1. For any fixed nonempty table size M, take every entry equal to eta=1/(2 sqrt(M)). All entries are strictly positive, yet the squared mass is M eta^2=1/4<1, and no entry equals1. This is a counterexample to the proposed implication from positivity alone, not to the actual Hermite sample table with its known unit term. Conversely a real table with a_c=1 and every other entry0 still has mass1, showing why strict positivity is unnecessary for this lower-bound argument. The actual target's positivity is a separate, stronger structural fact. It CAN independently prove a finite nonempty table's norm is positive, and the separate general sampleNorm_pos proof uses it; however it is neither what realizes the unit grid anchor nor needed once N>=1 has already proved the nonzero-normalizer consequence.
The existing sampled_mass_ge_one proof follows exactly the actual-grid/unit-value/single-square chain. It does not use sampledAmplitude_pos. Its Lean statement even permits every real L, but this candidate retains the original requested L>0 domain rather than adding a new generalization. Reading that theorem and its proof is static evidence, not a new compilation or a blanket state-preparation certificate. No phase, ancillary-space, circuit-resource or postselection-success conclusion is extracted from the unnormalized mass inequality itself.
Assessment rubric
- Proves c=2^n is an in-range actual LE integer index and substitutes it into the explicit grid to get p_c=0, independent of k,L; handles n=0 as one qubit. (1 weight)
- Uses the source zeroth right-endpoint value to obtain f_k(0)=1 and hence a_c=1, distinguishing that identity from amplitude positivity. (1 weight)
- Bounds the sum of nonnegative real squares by its unit central term, proves N>=1 uniformly and deduces sqrt(N)>0 without strict positivity. (1 weight)
- Refutes positivity-as-unit-anchor necessity with a strictly positive table of mass<1, identifies the actual grid/value dependencies and distinguishes positivity's separate norm-positivity role. Makes no circuit/success or new Lean-execution claim. (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/HermiteIntervalMass.lean
lines 162-195: smoothInitial_zero : smoothInitial k 0 = 1 (from sourceInterpolant_right_jet k 0); centralIndex n = <2^n, _> : Fin (gridSize (n+1)); gridPoint_central : gridPoint (n+1) L (centralIndex n) = 0; sampled_mass_ge_one : 1 <= sum_j (sampledAmplitude k (n+1) L j)^2 via Finset.single_le_sum at centralIndex
Source SHA-256:ff87cc69d0527cb1a7001a7bae4b916cf0a2c2b8bd1e6ba017511c3be27bc69f· MIT (repository LICENSE)
Contract: 84ba33c1266ca6bce4771fd68dc57cc64a084b96719cd7addab2896bcdd23973
Item digest: 525b8f123a38d56fcc3b95a970d0d7c293dddad13575bc075c874c6c6d614748
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-113", "predecessor_item_digest": "a7ff8025b9d3472242c418b45c7937ff94ad3774a512035a0a2895e785d55564", "predecessor_contract_hash": "3a69ad92920832681d43e5f54f6afcee5b54fa90202e271e585a405a0571ed06", "current_contract_hash": "84ba33c1266ca6bce4771fd68dc57cc64a084b96719cd7addab2896bcdd23973", "changed_contract_fields": [ "question" ], "repair_record": "shared/repairs/sp-113-unit-grid-anchor-state-successor.json", "repair_record_digest": "f5854401b05a07ca94c2aa833e7741057875f07f63a792481d4a17e041f23d72", "review_record": "reports/textbook-v1/repairs/sp-113-unit-grid-anchor-state-successor-review.json", "review_digest": "386f3429f9933063bbde17c5af33b5feb17577258efe17f38f14622f964f1a1b", "equivalence_to_predecessor_claimed": false, "additional_core_count": 0 }