QuantumBlockEncoding/ConstructiveIsometryLocal.lean

This definition gives the library's named construction or computation for “coordinates”. Low bond wires, highest emitted bit, with an explicit finite coordinate map.

def coordinates (q : ℕ) : PrimitiveBasis (q + 1) ≃ Fin (2 * 2 ^ q) :=
  (localIndex q).trans finProdFinEquiv

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “local completion”.

noncomputable def localCompletion {q r : ℕ} (hr : r ≤ 2 ^ q)
    (V : _root_.Matrix (PrimitiveBasis (q + 1)) (Fin r) ℝ) :
    _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ :=
  completeNamed (coordinates q) (by
    have : 0 < 2 ^ q := by positivity

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “local completion spec”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem localCompletion_spec {q r : ℕ} (hr : r ≤ 2 ^ q)
    (V : _root_.Matrix (PrimitiveBasis (q + 1)) (Fin r) ℝ) (hV : V.transpose * V = 1) :
    (localCompletion hr V).transpose * localCompletion hr V = 1 ∧
    (localCompletion hr V).det = 1 ∧
    ∀ row a, localCompletion hr V row (activePositions hr a) = V row a :=
  completeNamed_spec (coordinates q) _ V (activePositions hr) hV

/-- Actual stage matrix derived from the chain's real occupied columns. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “complete stage”. Actual stage matrix derived from the chain's real occupied columns.

noncomputable def completeStage {n l r q : ℕ} (C : Chain n l r)
    (hB : maxBond C ≤ 2 ^ q) (t : ℕ) :
    _root_.Matrix (PrimitiveBasis (q + 1)) (PrimitiveBasis (q + 1)) ℝ :=
  localCompletion ((rankAt_le_maxBond C t).trans hB) (activeColumns C t hB)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “complete stage spec”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem completeStage_spec {n l r q : ℕ} (C : Chain n l r)
    (hC : RightCanonical C) (hB : maxBond C ≤ 2 ^ q) (t : ℕ) (ht : t < n) :
    (completeStage C hB t).transpose * completeStage C hB t = 1 ∧
    (completeStage C hB t).det = 1 ∧
    ∀ (bit : Fin 2) (b a : PrimitiveBasis q),
      (primitiveBasisLEEquiv q a).val < rankAt C t →
      (completeStage C hB t (Fin.snoc b bit) (Fin.snoc a 0) : ℂ) =
        paddedAt C t (bit, primitiveBasisLEEquiv q b) (primitiveBasisLEEquiv q a) := by

commit-pinned source · Verso Blueprint panel