State Preparation
Exercise SP-006
nl bridge from inspected source. Additive answer successor with distinct content-bound review; historical rejected answer retained only for audit. No new Lean verification is claimed for this NL view.
Assumptions and conventions
- the total squared norm S is strictly positive
- entries are real; normalization is by division by sqrt(S)
- normSq is the sum of squared entries; sqrt is the real nonnegative square root
Question
Let f be a finite real amplitude table whose total squared Euclidean norm S = sum_b f(b)^2 is strictly positive. Prove that dividing every entry by sqrt(S) yields an exactly normalized state, i.e. sum_b (f(b)/sqrt(S))^2 = 1, and identify exactly where strict positivity of S is used.
Hint: mathematical route
Dividing a real table by the square root of its strictly positive total squared norm yields an exactly unit state, with nonvanishing of the norm the single load-bearing hypothesis.
- Factoring the common squared denominator out of the finite sum gives S/(sqrt(S))^2.
- The square-root identity for nonnegative S reduces this expression to S/S.
- Strict positivity makes S nonzero, hence S/S = 1, for arbitrary real entries. This algebraic conclusion does not remove the separate nonnegative-entry premise of prepareCircuit_firstColumn.
Reference solution
Let S = sum_b f(b)^2 > 0. The common denominator is independent of b, so sum_b (f(b)/sqrt(S))^2 = (sum_b f(b)^2)/(sqrt(S))^2 = S/S = 1. The square-root identity (sqrt(S))^2 = S uses nonnegativity of S, which already follows from its being a finite sum of real squares. Strict positivity is needed for nonvanishing: sqrt(S) is nonzero and cancellation S/S = 1 is justified. It does not require the individual f(b) to be nonnegative. At S=0 every entry is zero, so there is no normalized state proportional to that table. Ordinary division by zero is undefined; in Lean's total real division, 0/0 is defined as zero, and the corresponding sum is zero rather than one. This norm identity alone is not a first-column correctness theorem for a particular preparation circuit. The library's prepareCircuit_firstColumn additionally requires every f(b) to be nonnegative. For example, the zero-qubit table with its sole entry -1 has positive S and normalizes to -1, while the empty preparation circuit has first column +1. Thus one must not transfer the circuit theorem to arbitrary signed real tables under the assumptions of this question.
Assessment rubric
- Factors the constant squared denominator out of the finite sum to obtain S/(sqrt(S))^2. (1 weight)
- Uses (sqrt(S))^2 = S from S >= 0, independently of signs of individual entries. (1 weight)
- Uses S > 0 to ensure the nonzero denominator and S/S = 1; identifies nonvanishing as the load-bearing condition. (1 weight)
- Keeps the claim at normalization of the real table, without requiring or asserting arbitrary-signed circuit loading. If discussing S=0, distinguishes absence of a normalized proportional state from Lean's total division. No circuit discussion is required for full credit. (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/RealAmplitudePreparation.lean
lines 310-317: theorem normalized_sum_sq (f : PrimitiveBasis n -> R) (positive : 0 < normSq f) : (sum b, (f b / Real.sqrt (normSq f)) ^ 2) = 1, proved by simp_rw [div_pow]; rw [Finset.sum_div]; Real.sq_sqrt (normSq_nonneg f); div_self (ne_of_gt positive)
Source SHA-256:a6ded7e65a7e42d5724529befb48eefc9505814136206dd96248fb59b3c45efa· MIT (repository LICENSE)
Contract: 707c3d1e73346e5b7db45aef51792362cdd94974cd01199fac9eff41413a842d
Item digest: 80d8cf9a6ab1179417909a57f88236985358dda61923d365c37edbbe5f4df69d
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.
Answer revision lineage
{ "predecessor_item_digest": "44c37085b4bd6ee2044b283002c7cb3d2067205bc96c3b84b5cb04a60a4002a6", "predecessor_key": "qcb-core-sp-006", "repair_record": "shared/repairs/sp-006-normalization-boundary-repair.json", "repair_record_digest": "fafbf96e8efc8d116beffec203eb79caf60dc5d551b63df44e3baca73cb3b5a3", "review_record": "reports/textbook-v1/repairs/sp-006-normalization-boundary-repair-review.json", "review_digest": "ee93b57c7dea37159597a7c3f2d5ac86f81f09019452d70a62da62acad058f6f" }