This definition gives the library's named construction or computation for “word of basis”. Convert increasing-wire basis labels to the head-first chain word.
def wordOfBasis : {n : ℕ} → PrimitiveBasis n → Word n
| 0, _ => ()
| _ + 1, x => (x 0, wordOfBasis (Fin.tail x))
/-- Active rank before stage `t`; after the chain it is the terminal rank. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “rank at”. Active rank before stage 't'; after the chain it is the terminal rank.
def rankAt : {n l r : ℕ} → Chain n l r → ℕ → ℕ
| _, _, _, .nil r, _ => r
| _, l, _, .cons _ _, 0 => l
| _, _, _, .cons _ C, t + 1 => rankAt C t
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rank at zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem rankAt_zero {n l r : ℕ} (C : Chain n l r) : rankAt C 0 = l := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rank at length”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem rankAt_length {n l r : ℕ} (C : Chain n l r) : rankAt C n = r := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “padded at”. The finite schedule, zero after the final core.
def paddedAt {B : ℕ} : {n l r : ℕ} → Chain n l r → ℕ →
SequentialBondPreparation.Core (Fin B)
| _, _, _, .nil _, _ => 0
| _, _, _, .cons A _, 0 => paddedCore A
| _, _, _, .cons _ C, t + 1 => paddedAt C t
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rank at le max bond”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rankAt_le_maxBond {n l r : ℕ} (C : Chain n l r) (t : ℕ) :
rankAt C t ≤ maxBond C := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “padded at supported”; the hypotheses and conclusion in the code panel fix its exact scope. Zero amplitude outside the next actual rank, for the extracted schedule.
theorem paddedAt_supported {n l r B : ℕ} (C : Chain n l r) (t : ℕ)
(bit : Fin 2) (b a : Fin B) (hb : rankAt C (t + 1) ≤ b.val) :
paddedAt C t (bit, b) a = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transfer shift”; the hypotheses and conclusion in the code panel fix its exact scope. Rewrite chronological transfer in first-bit order, matching 'Chain.cons'.
theorem transfer_shift {B : Type*} [Fintype B] [DecidableEq B]
(K : ℕ → SequentialBondPreparation.Core B) (n : ℕ)
(x : PrimitiveBasis (n + 1)) :
transfer K (n + 1) x =
transfer (fun t => K (t + 1)) n (Fin.tail x) * coreSlice (K 0) (x 0) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “padded slice mul vec”; the hypotheses and conclusion in the code panel fix its exact scope. One extracted core slice acts as its exact real row-vector contraction, with zero padding on the old and new bond labels.
theorem paddedSlice_mulVec {l r B : ℕ} (hl : l ≤ B) (A : TensorTrainCanonical.Core l r)
(bit : Fin 2) (v : Fin l → ℝ) :
(coreSlice (paddedCore A : SequentialBondPreparation.Core (Fin B)) bit).mulVec
(padVector (fun a => (v a : ℂ))) =
padVector (fun b => ((_root_.Matrix.vecMul v (slice A bit)) b : ℂ)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “transfer padded”; the hypotheses and conclusion in the code panel fix its exact scope. All-length transfer equals the original chain contraction at every padded output label, not just after projection onto its active subspace.
theorem transfer_padded {n l r B : ℕ} (C : Chain n l r) (hB : maxBond C ≤ B)
(v : Fin l → ℝ) (x : PrimitiveBasis n) (b : Fin B) :
(transfer (paddedAt C) n x).mulVec (padVector (fun a => (v a : ℂ))) b =
padVector (fun c => ((_root_.Matrix.vecMul v (contract C (wordOfBasis x))) c : ℂ)) b := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “run eq transfer bounded”; the hypotheses and conclusion in the code panel fix its exact scope. A bounded version of the sequential local-column theorem: unused later stages need not implement the zero cores after the end of the schedule.
theorem run_eq_transfer_bounded {B : Type*} [Fintype B] [DecidableEq B]
(U : ℕ → Stage B) (K : ℕ → SequentialBondPreparation.Core B)
(active : ℕ → B → Prop) (boundary : B → ℂ)
(initialSupport : ∀ b, ¬ active 0 b → boundary b = 0)
(coreSupport : ∀ t bit b a, ¬ active (t + 1) b → K t (bit, b) a = 0)
(n : ℕ)
(columns : ∀ t, t < n → ∀ bit b a, active t a → U t (bit, b) (0, a) = K t (bit, b) a)
(x : PrimitiveBasis n) (b : B) :
run U boundary n (x, b) = (transfer K n x).mulVec boundary b := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “run padded”; the hypotheses and conclusion in the code panel fix its exact scope. Exact complete sequential action of the schedule extracted from an actual dependent train.
theorem run_padded {n l r B : ℕ} (C : Chain n l r) (hB : maxBond C ≤ B)
(U : ℕ → Stage (Fin B))
(columns : ∀ t, t < n → ∀ bit b a, a.val < rankAt C t →
U t (bit, b) (0, a) = paddedAt C t (bit, b) a)
(v : Fin l → ℝ) (x : PrimitiveBasis n) (b : Fin B) :
run U (padVector (fun a => (v a : ℂ))) n (x, b) =
padVector (fun c => ((_root_.Matrix.vecMul v (contract C (wordOfBasis x))) c : ℂ)) b := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “run terminal clean”; the hypotheses and conclusion in the code panel fix its exact scope. Terminal dimension one gives whole-state cleanup at physical label zero.
theorem run_terminal_clean {n l B : ℕ} (C : Chain n l 1) (hB : maxBond C ≤ B)
(U : ℕ → Stage (Fin B))
(columns : ∀ t, t < n → ∀ bit b a, a.val < rankAt C t →
U t (bit, b) (0, a) = paddedAt C t (bit, b) a)
(v : Fin l → ℝ) (x : PrimitiveBasis n) (b : Fin B) :
run U (padVector (fun a => (v a : ℂ))) n (x, b) =
if b.val = 0 then
((_root_.Matrix.vecMul v (contract C (wordOfBasis x))) 0 : ℂ) else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “padded at active isometry”; the hypotheses and conclusion in the code panel fix its exact scope. Every extracted stage of a canonical chain has orthonormal occupied columns in the one fixed physical register.
theorem paddedAt_active_isometry {n l r B : ℕ} (C : Chain n l r)
(hC : RightCanonical C) (hB : maxBond C ≤ B) (t : ℕ) (ht : t < n)
(a c : Fin (rankAt C t)) :
(∑ out : Fin 2 × Fin B,
star (paddedAt C t out (Fin.castLE ((rankAt_le_maxBond C t).trans hB) a)) *
paddedAt C t out (Fin.castLE ((rankAt_le_maxBond C t).trans hB) c)) =
if a = c then 1 else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exists normalized preparation schedule”; the hypotheses and conclusion in the code panel fix its exact scope. A normalized scalar-boundary source train has a bounded canonical schedule with exact whole-state source action whenever its *local occupied columns* are implemented.
theorem exists_normalized_preparation_schedule {n B : ℕ} (C : Chain n 1 1)
(hB : maxBond C ≤ B)
(hNorm : (∑ x : Word n, (contract C x 0 0) ^ 2) = 1) :
∃ (l' : ℕ) (u : Fin l' → ℝ) (D : Chain n l' 1),
RightCanonical D ∧ RankReduced C D ∧ mass u = 1 ∧ maxBond D ≤ B ∧
∀ (U : ℕ → Stage (Fin B)),
(∀ t, t < n → ∀ bit b a, a.val < rankAt D t →
U t (bit, b) (0, a) = paddedAt D t (bit, b) a) →
∀ (x : PrimitiveBasis n) (b : Fin B),
run U (padVector (fun a => (u a : ℂ))) n (x, b) =
if b.val = 0 then (contract C (wordOfBasis x) 0 0 : ℂ) else 0 := by
commit-pinned source · Verso Blueprint panel