Exercise SP-008

Unitary sequential stages from a basis boundary keep total probability one at every length, a coherent success with mass-neutral fresh-zero padding and no postselection.

1. One step factors as fresh-zero padding followed by the lifted stage action and a label regrouping; the lifted stage is unitary because a Kronecker product of unitaries is unitary.
2. Fresh-zero padding preserves mass and a full unitary action preserves mass, so a single step preserves amplitude mass.
3. Induction on n propagates mass preservation to the whole run; the basis-boundary mass equals one, giving total probability one at every length with no postselection.

Define amplitudeMass v = sum over labels i of star(v_i) * v_i (a complex scalar equal to the total squared modulus). Two facts drive the proof. First, a single step preserves amplitude mass whenever its stage is unitary: the step is the composition of (a) appending a fresh zero bit, which preserves mass because it only adjoins zero components, and (b) applying the stage tensored with the identity on all passive emitted wires. A Kronecker product of unitaries is unitary, so the lifted stage is unitary, and a full unitary matrix-vector action preserves amplitude mass since star(Mv) dot (Mv) = star(v) (M^dagger M) v = star(v) dot v. A final basis regrouping is a bijection of labels and does not change the sum. Hence amplitudeMass(step U v) = amplitudeMass(v). Second, by induction on n the full run preserves mass: at length 0 the run is the boundary and the inductive step applies the one-step invariant, so amplitudeMass(run U boundary n) = amplitudeMass(boundary). Finally, for a basis boundary the mass is sum over labels of the indicator squared = 1. Therefore the emitted state has total probability one at every length. This is a coherent success statement because the entire register is retained: no amplitude is projected out and no renormalization is performed. The fresh-zero padding is essential and benign: it enlarges the register by a provably mass-neutral embedding, so unitarity of each stage is enough to carry total probability one through every emission.

1. Defines amplitude mass as the sum of star times value and shows a single step factors as fresh-zero padding then a lifted (Kronecker-with-identity) unitary action. (1 weight)
2. Shows fresh-zero padding is mass-preserving and that a full unitary action preserves mass via star(Mv).(Mv) = star(v).v, hence one step preserves mass. (1 weight)
3. Inducts on n to conclude the run preserves mass, then evaluates the basis-boundary mass to 1. (1 weight)
4. Explains this is coherent success with no postselection/renormalization and that fresh-zero padding is a mass-neutral register enlargement. (1 weight)

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.

Read the Lean track and existing diagnostic warmups

• QuantumBlockEncoding/SequentialBondPreparation.lean

  lines 288-340: noncomputable def amplitudeMass v := sum i, star (v i) * v i; theorem amplitudeMass_step (hU : U in unitaryGroup) : amplitudeMass (step U v) = amplitudeMass v; theorem amplitudeMass_run (unitary : for all t, U t in unitaryGroup) : amplitudeMass (run U boundary n) = amplitudeMass boundary; theorem amplitudeMass_run_basisBoundary : amplitudeMass (run U (basisBoundary initial) n) = 1

  Source SHA-256: ad4542b108d44f196f2a02f78e59b58f43d45b1e890709cf4c22e1222805d5c5 · MIT (repository LICENSE)

Contract: b292fd14d37907ff3e7aba598779c0fd83b21c819fa4be460397ff0fc38cfa02

Item digest: d403cce404da75f2931579b020692a9cf08143dfd7b2a59eeec69fce4c59f771

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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