Linear Algebra
Exercise LA-008
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
- a fixed clean signal value is chosen
- finite matrices over a semiring backend
- signal-system flattening with signal high-order
- pointwise matrix equality quantifies over all entries
Question
Two proof styles are commonly used to certify that a flattened signal-system unitary block-encodes a target operator on the system register at a fixed 'clean' signal value. Style A proves a pointwise equality: the matrix block obtained by projecting the unitary onto that clean signal branch equals the target matrix entry by entry. Style B proves an action statement: for every clean-signal basis input and every clean-signal output row, the amplitude the unitary produces equals the corresponding target matrix entry. Prove that these two styles are logically equivalent, by first showing the single bridging identity that the clean-input/clean-output amplitude of the unitary equals exactly one entry of the projected block.
Hint: mathematical route
Projected-block pointwise equality to the target is equivalent to the clean-basis action equality, bridged by cleanBasisActionAmplitude = signalSystemBlockProjection entry.
- The clean-input/clean-output amplitude equals one entry of the signal-branch projected block.
- Pointwise block equality implies the clean-basis action statement for all outputs/inputs.
- The clean-basis action statement for all outputs/inputs implies pointwise block equality.
Reference solution
The bridge is: for a fixed clean signal value and any output and input system indices, the amplitude obtained by feeding the clean-signal basis input into the unitary and reading the clean-signal output row equals exactly the (output, input) entry of the projected block of the unitary at that signal value. This holds because acting on a basis ket selects a column (the basis-column fact), and selecting the clean-output coordinate of that column is by definition the same entry that the signal-branch projection reads off; so the amplitude and the projected-block entry are literally the same number for every output and input. Now prove the equivalence. (Style A implies Style B) Assume the projected block equals the target entrywise. Fix any output and input. By the bridge the clean-input/clean-output amplitude equals the projected-block (output,input) entry, which by assumption equals the target (output,input) entry; so the action statement holds for every output and input. (Style B implies Style A) Assume the action statement holds for all outputs and inputs. Fix any output and input; the projected-block (output,input) entry equals, by the bridge, the clean-input/clean-output amplitude, which by assumption equals the target (output,input) entry; so the projected block equals the target entrywise. Since each direction follows from the single bridging identity applied at an arbitrary (output, input) pair, the two certification styles are equivalent. (Linearity further extends the basis action to arbitrary system inputs, and any orthogonal failure branch is separate unitarity evidence rather than a competing block contract.)
Assessment rubric
- States and justifies the bridge: clean-input/clean-output amplitude = projected-block entry (via basis-ket selects a column). (1 weight)
- Proves Style A => Style B by applying the bridge at an arbitrary (output,input). (1 weight)
- Proves Style B => Style A symmetrically. (1 weight)
- Notes the universal quantification over all (output,input) pairs is what delivers full equivalence (and linearity extends to arbitrary inputs). (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/ConcreteSemantics.lean
complete declarations cleanBasisActionAmplitude (lines 249-256), cleanBasisActionAmplitude_eq_signalSystemBlockProjection (lines 259-269), pointwiseProjection_iff_cleanBasisAction (lines 277-294)
Source SHA-256:454c0c5e215ca197c5883bedf74882f392d259c7afeadc63912230437698ebe5· MIT (repository LICENSE)
Contract: 713df377e45237947cc505da3883231cdc9e2105d18e8eab77e7cdbc987289a8
Item digest: ffed957ea2517808e052738941799ab1478ba9bade87b7bf84f0987ffc74cd0d
Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a
Authored support steps: 3. This is not measured graph distance or model difficulty.