Exercise SP-009

Orthonormal real core rows become orthonormal complex input-bond columns under the output-row/input-column orientation, because realness makes conjugation trivial.

1. The (a,c) entry of the Gram product is a sum over outputs of conj(entry at a) times entry at c.
2. Realness makes conjugation trivial, reducing the sum to the real sum A_{a,out} A_{c,out} = (A * A^T)_{a,c}.
3. A * A^T = 1 gives the Kronecker delta; the real part matches it and the imaginary part is zero, so the complex Gram matrix is the identity.

Let A be a real core with A * A^T = 1 (orthonormal rows). The complex embedding places (bit, new bond) as the output row index and the old bond a as the input column, with entry the real number A_{a,(bit,newbond)} viewed as a complex number. The isometry claim is (complexCore A)^dagger * (complexCore A) = 1 on the old-bond index. Fix input columns a and c; the (a,c) entry of the product is sum over all outputs (bit, newbond) of conj(entry at output,(a)) times entry at output,(c). Because every entry is a real number embedded in the complex field, its conjugate is itself, so this equals the real sum over outputs of A_{a,out} * A_{c,out}, which is precisely the (a,c) entry of A * A^T. By hypothesis A * A^T = 1, so the sum is 1 when a = c and 0 otherwise. Splitting the complex equality into real and imaginary parts: the real part reproduces the (a,c) entry of A * A^T (equal to the Kronecker delta), and the imaginary part vanishes because every summand is a product of reals and hence has zero imaginary component. Therefore (complexCore A)^dagger (complexCore A) is the identity. The conceptual point: the row-canonical condition on the real core, summation over the physical bit together with the new bond, is literally the Gram matrix of the complex input-bond columns under this output-row/input-column orientation; realness makes conjugation trivial so the real orthonormality transfers verbatim to complex column orthonormality.

1. States the isometry target (complexCore A)^dagger (complexCore A) = 1 and expands the (a,c) entry as a sum over outputs (bit, new bond) of conj times entry. (1 weight)
2. Uses realness of the entries (conjugate = itself) to reduce the sum to the real sum A_{a,out} A_{c,out}, i.e. the (a,c) entry of A * A^T. (1 weight)
3. Invokes A * A^T = 1 to get the Kronecker delta, splitting the complex identity into a real part (= delta) and a vanishing imaginary part. (1 weight)
4. Explains the orientation point: real orthonormal rows are exactly the Gram matrix of complex input-bond columns, so orthonormality transfers verbatim. (1 weight)

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.TensorTrainCanonical"
  ],
  "target": "∀ {l r : ℕ} (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r), A * A.transpose = 1 → (QuantumBlockEncoding.TensorTrainCanonical.complexCore A).conjTranspose * QuantumBlockEncoding.TensorTrainCanonical.complexCore A = 1"
}

by exact QuantumBlockEncoding.TensorTrainCanonical.complexCore_isometry

Real row-canonical core, complex output-row/input-column embedding. No efficient completion/compiler/resource claim; the legacy API exercise is the same mathematical target and adds no core.

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

• QuantumBlockEncoding/TensorTrainCanonical.lean

  lines 209-226: def complexCore A := fun out a => (A a out : C); theorem complexCore_isometry (A : Core l r) (hA : A * A.transpose = 1) : (complexCore A).conjTranspose * complexCore A = 1, proved via congrFun hA, Complex.ext on real and imaginary parts of the mul_apply / conjTranspose_apply / one_apply expansion

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

Contract: 108977edccc1cb916d3614d5b4d2927d1a82e337f901ff73421320ef956448b0

Item digest: 3f133557d4caeab060a7631ee2641d0019434fd496c4f8fa413895aaf318e981

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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