State Preparation

Exercise SP-005

intermediate · proof · test_public

nl bridge from inspected source. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

f is an arbitrary real table on n+1 wires; no positivity or normalization is assumed
the marginal is defined by the sibling-pair Euclidean length as in the source

normSq g is the sum of squared entries; wires are little-endian with the last bit split off by snoc
pairNorm is the nonnegative Euclidean length of a pair

Question

For a finite real amplitude table f on n+1 wires, define its low-wire marginal by taking, at each prefix word b, the Euclidean length of the sibling pair (f at b-with-last-bit-0, f at b-with-last-bit-1). Prove that the total squared Euclidean norm of the marginal equals the total squared Euclidean norm of f. Explain why this makes the recursive marginal pass norm-faithful.

Hint: mathematical route

The low-wire marginal has the same total squared norm as the full table, via the per-pair Pythagorean identity and a last-bit reindexing.

pairNorm(a,b)^2 = a^2 + b^2, so each marginal entry squared equals the sum of its two children squared.
The map (prefix word, last bit) to full word via snoc is a bijection partitioning full words by their last bit.
Reindexing the full squared-norm sum along this bijection and splitting the last bit into 0 and 1 reproduces the marginal sum, giving normSq(marginal f) = normSq f.

Reference solution

Write normSq g = sum over basis words of g^2, and for a prefix word b let m(b) = pairNorm(f(snoc b 0), f(snoc b 1)) with pairNorm(a,b) = sqrt(a^2+b^2). First, pairNorm squares cleanly: pairNorm(a,b)^2 = a^2 + b^2, because pairNorm is the square root of the nonnegative quantity a^2+b^2 and squaring a square root of a nonnegative real returns the radicand. Hence m(b)^2 = f(snoc b 0)^2 + f(snoc b 1)^2 for every prefix b. Summing over all prefix words b: normSq(marginal f) = sum_b m(b)^2 = sum_b [ f(snoc b 0)^2 + f(snoc b 1)^2 ]. Now use the bijection between words on n+1 wires and (prefix word b, last bit v) given by w = snoc b v, which partitions every full word uniquely by its last bit. Reindexing the full sum normSq f = sum over w of f(w)^2 along this bijection and splitting the last bit into the two cases v=0 and v=1 gives exactly sum_b [ f(snoc b 0)^2 + f(snoc b 1)^2 ]. The two expressions coincide, so normSq(marginal f) = normSq f. Norm-faithfulness follows: the recursive loader first prepares the marginal on the lower wires and then splits each marginal entry with one rotation; because each marginal step reproduces the exact squared norm, the induction hypothesis about the normalized lower state transfers without any loss or rescaling, which is precisely the invariant the first-column proof consumes.

Assessment rubric

Establishes pairNorm(a,b)^2 = a^2 + b^2 (square of a square root of a nonnegative radicand), hence m(b)^2 = f(snoc b 0)^2 + f(snoc b 1)^2. (1 weight)
Uses the (prefix word, last bit) bijection w = snoc b v to reindex the full squared-norm sum. (1 weight)
Splits the last-bit sum into v=0 and v=1 to match the marginal sum, concluding normSq(marginal f) = normSq f. (1 weight)
Explains that exact squared-norm preservation per level is what carries the normalization invariant through the recursion. (1 weight)

Graph-grounded prerequisites

These are support/source anchors, not an automatically extracted theorem-dependency proof.

Download the shared core registry

Lean view and evidence boundary

Exact formal conclusion: independently decoded and compared with this question, then checked with the fixed reference in Lean. This is a library-lemma application, not a deep proof-search result. The kernel does not certify every sentence of the natural-language explanation.

{
  "imports": [
    "QuantumBlockEncoding.RealAmplitudePreparation"
  ],
  "target": "∀ {n : ℕ} (f : QuantumBlockEncoding.PrimitiveBasis (n + 1) → ℝ), QuantumBlockEncoding.RealAmplitudePreparation.normSq (QuantumBlockEncoding.RealAmplitudePreparation.marginal f) = QuantumBlockEncoding.RealAmplitudePreparation.normSq f"
}

Fixed reference proof

by exact QuantumBlockEncoding.RealAmplitudePreparation.normSq_marginal

No positivity or normalization premise. This is a norm identity, not a signed-state loading, circuit-cost or finite-precision theorem.

Execution class: trusted local reference; not isolated model-output evaluation. The same core, family and split apply to both views.

Source-blind reconstruction, distinct comparison and actual reference receipts: inspect the evidence records.

Read the Lean track and existing diagnostic warmups

Sources and provenance

QuantumBlockEncoding/RealAmplitudePreparation.lean
lines 142-222: theorem pairNorm_sq (a b : R) : pairNorm a b ^ 2 = a ^ 2 + b ^ 2; noncomputable def marginal f := fun b => pairNorm (f (Fin.snoc b 0)) (f (Fin.snoc b 1)); noncomputable def normSq f := sum b, f b ^ 2; theorem normSq_marginal (f : PrimitiveBasis (n+1) -> R) : normSq (marginal f) = normSq f
Source SHA-256: a6ded7e65a7e42d5724529befb48eefc9505814136206dd96248fb59b3c45efa · MIT (repository LICENSE)

Contract: 0821f527326022b9972f0d4083b8a2a99c179263e36e5d27112f6cb5c1c98865

Item digest: 4748bf7c81283496b115e778c1f365bd503d4384829e85ceb0959f348a5a97d4

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 3. This is not measured graph distance or model difficulty.