QuantumComputinglib learn · inspect · formalize
Checked on this commit 4,524 public declarations commit 4e2c5b2c0be5 Build record

Shared mathematical foundations / Matrix Constructions

Matrix Constructions

Exercise LA-109

intermediate · proof · train

local source supported. Current content-bound mathematical second pass accepted. No new Lean verification is claimed for this NL view.

Assumptions and conventions

  • Fixed-width real cores; left boundary vector of length D; terminal bond 1
  • Amplitudes are finite chronological matrix contractions
  • Closing the left boundary absorbs the vector into the first core only
  • Original derivation from inspected local source; no fresh Lean verification

Question

A finite matrix-product chain of width-D cores produces an amplitude for a bit string by chronological matrix contraction, with a fixed left boundary vector of length D. Contracting that left boundary into the first core yields a chain with left bond 1. Prove that the single scalar amplitude of this closed chain equals the sum over a of left[a] times the open chain's amplitude indexed by a.

Hint: mathematical route

Folding a left boundary vector into the first core of a matrix-product chain gives a scalar amplitude equal to the left-weighted sum of open-chain amplitudes, via a finite double-sum exchange.

  1. Expand the closed-chain amplitude using the folded first core.
  2. Rewrite it as a double sum over the first bond and the output index.
  3. Express the left-weighted open amplitudes as the same double sum.
  4. Conclude equality by exchanging the finite summation order.
Reference solution

Write the first core as a function A[a,out] of an incoming bond a and an output index out, and let the rest of the chain contract to a vector indexed by its own incoming bond. Closing the left boundary replaces the first core by the single-row core whose entry at out is sum over a of left[a]*A[a,out]. The amplitude of the closed chain for a string x is then sum over out of (sum over a of left[a]*A[a,out]) * (tail amplitude at bond out). Expanding the inner definition this is a double sum over a and out of left[a]*A[a,out]*(tail amplitude at out). The open chain's amplitude indexed by a is sum over out of A[a,out]*(tail amplitude at out). So the target expression sum over a of left[a]*(open amplitude at a) is sum over a of left[a]* sum over out of A[a,out]*(tail at out), which is the same double sum with the two finite summations exchanged. Exchanging the order of a finite double sum is valid, so the two expressions are equal. This is an exact contraction identity about absorbing a boundary vector, not a claim about contraction runtime.

Assessment rubric
  1. Express the closed-chain amplitude as a double sum over the first bond and output (1 weight)
  2. Express the target as left-weighted open amplitudes, also a double sum (1 weight)
  3. Equate the two by exchanging the finite summation order (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

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

Sources and provenance

Contract: 3a4b07627c4804b35b0209114e8b987dde911a8907425c5fd445793279dd9344

Item digest: 1fd3017d71601c3fa4b81db41b1b04a8d4a9fd00e609a2ba2b87f5082ddbb14b

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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