A.9 Matrix transport and actual unitarity
On this page · Permalink · Source line 356
The semantics layer proves that coordinate matrix multiplication, adjoint, identity, and matrix-vector action have their ordinary complex meanings. The matrices \(F,P,D\) and the normalized states are then defined directly in that complex representation.
Literal source. SemanticBridge.lean, physical lines 65–91.
@[simp] theorem complexMatrix_mul (A B : KMatrix) :
complexMatrix (kMatMul A B) = complexMatrix A * complexMatrix B := by
ext i j
simp [complexMatrix, kMatMul, Matrix.mul_apply]
@[simp] theorem complexMatrix_adjoint (A : KMatrix) :
complexMatrix (kAdjoint A) = (complexMatrix A)ᴴ := by
ext i j
simp [complexMatrix, kAdjoint, Matrix.conjTranspose_apply]
@[simp] theorem complexMatrix_identity :
complexMatrix kIdentity = 1 := by
ext i j
by_cases h : i = j <;> simp [complexMatrix, kIdentity, h, Matrix.one_apply]
@[simp] theorem complexVector_mul (A : KMatrix) (v : KVector) :
complexVector (kMatVec A v) = (complexMatrix A).mulVec (complexVector v) := by
ext i
simp [complexVector, complexMatrix, kMatVec, Matrix.mulVec, dotProduct]
noncomputable def F : Matrix Index Index ℂ := complexMatrix exactFourier
noncomputable def P : Matrix Index Index ℂ := complexMatrix exactProjector
noncomputable def D : Matrix Index Index ℂ :=
Matrix.diagonal (fun i => if Nat.gcd i.val 12 = 1 then 1 else 0)
noncomputable def psi : Index → ℂ := complexVector exactPsi
noncomputable def chi : Index → ℂ := complexVector exactChi
noncomputable def unitState : Index → ℂ := complexVector exactUnitStateConsequently, the finite certificates produce actual complex unitarity and projector transport. The following excerpt contains the full proofs of both unitary identities, the cross-representation projector identity, and the two state-action identities.
Literal source. SemanticBridge.lean, physical lines 93–120.
/-- Actual complex unitarity, not an assertion only about the coordinate checker. -/
theorem fourier_unitary_left : Fᴴ * F = 1 := by
have h : kMatMul (kAdjoint exactFourier) exactFourier = kIdentity :=
funext (fun i => funext (normalized_fourier_left i))
simpa [F] using congrArg complexMatrix h
theorem fourier_unitary_right : F * Fᴴ = 1 := by
have h : kMatMul exactFourier (kAdjoint exactFourier) = kIdentity :=
funext (fun i => funext (normalized_fourier_right i))
simpa [F] using congrArg complexMatrix h
theorem projector_transport : F * D * Fᴴ = P := by
ext i j
have h := congrArg interpret (exact_projector_transport i j)
simp only [selectedKernel, interpret_kSum] at h
rw [Matrix.mul_apply]
simpa [D, P, F, complexMatrix, Matrix.mul_diagonal, Matrix.conjTranspose_apply,
apply_ite interpret, mul_ite] using h
theorem state_preparation : F.mulVec unitState = psi := by
have h : kMatVec exactFourier exactUnitState = exactPsi :=
funext exact_state_preparation
simpa [F, unitState, psi] using congrArg complexVector h
theorem state_recovery : Fᴴ.mulVec psi = unitState := by
have h : kMatVec (kAdjoint exactFourier) exactPsi = exactUnitState :=
funext exact_state_recovery
simpa [F, unitState, psi] using congrArg complexVector hThis is the key strengthening over the earlier checkpoint. The rational matrix, the exact coordinate kernel, and the complex matrix \(FDF^*\) are explicitly connected. State preparation and recovery are equalities of actual complex vectors. The theorem name state_preparation describes a matrix identity, not an efficient hardware preparation algorithm.