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

Quantum Scientific Computing / Hamiltonian Composition

Hamiltonian Composition

Exercise LA-019

intermediate · proof · train

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

  • Finite-dimensional complex matrices; ordinary conjugate transpose
  • All declared products have compatible dimensions
  • Tensor factors ordered as written; stencil offsets are ordinary integers, not modular wrapping
  • Original derivation from inspected local source; no fresh Lean verification

Question

Let S and T be Hermitian matrices on one finite system and X a Hermitian matrix on a second system. Prove that H=S tensor X+T tensor I is Hermitian without assuming that S and T commute. Give a counterexample showing that the same conclusion can fail if X is not Hermitian.

Hint: mathematical route

Let S and T be Hermitian matrices on one finite system and X a Hermitian matrix on a second system. Prove that H=S tensor X+T tensor I is Hermitian without assuming that S and T commute. Give a counterexample showing that the same conclusion can fail if X is not Hermitian.

  1. Check the tensor adjoint identity entry by entry and use both Hermitian premises.
  2. The identity factor and the sum preserve Hermiticity without a commutation assumption.
  3. A one-dimensional outer factor reduces to a non-Hermitian X, exposing the missing hypothesis.
Reference solution

The adjoint of a tensor product is the tensor product of the adjoints: entrywise, conjugating S(j,i)X(v,u) gives S(i,j)X(u,v) under Hermiticity of both factors. Hence (S tensor X) dagger=S tensor X. Similarly T tensor I is Hermitian because I dagger=I. Adjoint is additive, so H dagger=H. No product S T occurs anywhere in this argument, so S and T need not commute. The premise on X matters: take the first system one-dimensional with S=[1], T=[0], and X=[[0,1],[0,0]]. Then H=X, whereas X dagger=[[0,0],[1,0]] is different. This is an operator-algebra closure result, not a claim that implementing the factors or reading out a simulated evolution is free.

Assessment rubric
  1. Correct tensor and additive adjoint calculation (1 weight)
  2. Explicitly do not assume S and T commute (1 weight)
  3. Valid non-Hermitian counterexample when X premise removed (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
  • QuantumBlockEncoding/GHLHamiltonian.lean

    tensor367-369; tensor_isHermitian394-400; add_isHermitian402-408; oneDimHamiltonian_isHermitian410-417

    Source SHA-256: 2e453b72433b4031e29ba73e9e22c3be0f63e4640781b9c81219fdf908ee80c7 · MIT (repository LICENSE)

Contract: e578a5d6515ff90904424ad07813b130203478bf54a7f45b2d3aa8972feecb97

Item digest: 2608e997670f03f1d37ccd000716a0a0478826035c40e22316b4639af5704267

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

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