Lean checks the proposition indexed as “exists so named”; the hypotheses and conclusion in the code panel fix its exact scope. Coordinate adapter for special-orthogonal completion on any finite named basis, with prescribed columns at arbitrary physical labels.
theorem exists_SO_named {I : Type*} [Fintype I] [DecidableEq I] {r : ℕ}
(hr : r < Fintype.card I) (V : _root_.Matrix I (Fin r) ℝ) (e : Fin r ↪ I)
(hV : V.transpose * V = 1) :
∃ U : _root_.Matrix I I ℝ, U.transpose * U = 1 ∧ U.det = 1 ∧
∀ i a, U i (e a) = V i a := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “local index”. The bit is the highest local physical wire; the bond uses low wires.
def localIndex (q : ℕ) : PrimitiveBasis (q + 1) ≃ Fin 2 × Fin (2 ^ q) :=
(localBasisEquiv q).trans (Equiv.prodCongr (Equiv.refl _) (primitiveBasisLEEquiv q))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “local index snoc”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem localIndex_snoc (q : ℕ) (b : PrimitiveBasis q) (bit : Fin 2) :
localIndex q (Fin.snoc b bit) = (bit, primitiveBasisLEEquiv q b) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “padded at real”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem paddedAt_real {n l r B : ℕ} (C : Chain n l r) (t : ℕ)
(out : Fin 2 × Fin B) (a : Fin B) :
((paddedAt C t out a).re : ℂ) = paddedAt C t out a := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “padded at im zero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem paddedAt_im_zero {n l r B : ℕ} (C : Chain n l r) (t : ℕ)
(out : Fin 2 × Fin B) (a : Fin B) : (paddedAt C t out a).im = 0 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “active positions”.
def activePositions {q l : ℕ} (hl : l ≤ 2 ^ q) : Fin l ↪ PrimitiveBasis (q + 1) where
toFun a := (localIndex q).symm (0, Fin.castLE hl a)
inj' a b h := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “active columns”. The occupied real columns of a padded core, in physical named-wire order.
def activeColumns {n l r q : ℕ} (C : Chain n l r) (t : ℕ)
(hB : maxBond C ≤ 2 ^ q) :
_root_.Matrix (PrimitiveBasis (q + 1)) (Fin (rankAt C t)) ℝ :=
fun row a => (paddedAt C t (localIndex q row)
(Fin.castLE ((rankAt_le_maxBond C t).trans hB) a)).re
/-- Exact real orthonormality is extracted from the proved complex padded-core
semantics; no ambient matrix or desired circuit action is assumed. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “active columns isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Exact real orthonormality is extracted from the proved complex padded-core semantics; no ambient matrix or desired circuit action is assumed.
theorem activeColumns_isometry {n l r q : ℕ} (C : Chain n l r)
(hC : RightCanonical C) (hB : maxBond C ≤ 2 ^ q) (t : ℕ) (ht : t < n) :
(activeColumns C t hB).transpose * activeColumns C t hB = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists local circuit with resources”; the hypotheses and conclusion in the code panel fix its exact scope. Every actual canonical stage has an exact primitive implementation on the 'q' low bond wires and one highest output wire.
theorem exists_local_circuit_with_resources {n l r q : ℕ} (C : Chain n l r)
(hC : RightCanonical C) (hB : maxBond C ≤ 2 ^ q) (t : ℕ) (ht : t < n) :
∃ c : PrimitiveCircuit (q + 1),
c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧ c.resource.oracleCalls = 0 ∧
∀ (bit : Fin 2) (b a : PrimitiveBasis q),
(primitiveBasisLEEquiv q a).val < rankAt C t →
evalPrimitiveCircuit c (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
Lean checks the proposition indexed as “exists local circuit”; the hypotheses and conclusion in the code panel fix its exact scope. Minimal local-column interface for sequential tensor-train assembly.
theorem exists_local_circuit {n l r q : ℕ} (C : Chain n l r)
(hC : RightCanonical C) (hB : maxBond C ≤ 2 ^ q) (t : ℕ) (ht : t < n) :
∃ c : PrimitiveCircuit (q + 1), c.gateCount ≤ 6 * (2 ^ q) ^ 3 ∧
∀ (bit : Fin 2) (b a : PrimitiveBasis q),
(primitiveBasisLEEquiv q a).val < rankAt C t →
evalPrimitiveCircuit c (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