QuantumBlockEncoding/TensorTrainPrimitivePreparation.lean

This definition gives the library's named construction or computation for “boundary row”.

def boundaryRow {l : ℕ} (u : Fin l → ℝ) : _root_.Matrix (Fin 1) (Fin l) ℝ := fun _ a => u a

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary row isometry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryRow_isometry {l : ℕ} (u : Fin l → ℝ) (hu : mass u = 1) :
    boundaryRow u * (boundaryRow u).transpose = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary core isometry”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryCore_isometry {l r : ℕ} (u : Fin l → ℝ) (hu : mass u = 1)
    (A : TensorTrainCanonical.Core l r) (hA : A * A.transpose = 1) :
    (boundaryRow u * A) * (boundaryRow u * A).transpose = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “boundary core contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem boundaryCore_contract {n l m r : ℕ} (u : Fin l → ℝ)
    (A : TensorTrainCanonical.Core l m) (C : Chain n m r) (x : Word (n + 1)) :
    contract (.cons (boundaryRow u * A) C) x = boundaryRow u * contract (.cons A C) x := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists unit boundary canonical”; the hypotheses and conclusion in the code panel fix its exact scope. Eliminate the signed initial residual by absorbing it into the first row-isometric core.

theorem exists_unitBoundary_canonical {n B : ℕ} (C : Chain (n + 1) 1 1)
    (hB : maxBond C ≤ B)
    (hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
    ∃ D : Chain (n + 1) 1 1, RightCanonical D ∧ maxBond D ≤ B ∧
      ∀ x, contract D x 0 0 = contract C x 0 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “transport stage”. Reindex only the finite bond labels of a local stage.

def transportStage {B C : Type*} (e : B ≃ C) (U : Stage C) : Stage B :=
  fun row col => U (row.1, e row.2) (col.1, e col.2)

commit-pinned source · Verso Blueprint panel

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

theorem run_transport {B C : Type*} [Fintype B] [Fintype C] [DecidableEq B] [DecidableEq C]
    (e : B ≃ C) (U : ℕ → Stage C) (boundary : B → ℂ)
    (n : ℕ) (x : PrimitiveBasis n) (b : C) :
    run U (fun c => boundary (e.symm c)) n (x, b) =
      run (fun t => transportStage e (U t)) boundary n (x, e.symm b) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bond index zero”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bondIndex_zero (q : ℕ) : (primitiveBasisLEEquiv q (fun _ => 0)).val = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bond index zero iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bondIndex_zero_iff {q : ℕ} (b : PrimitiveBasis q) :
    (primitiveBasisLEEquiv q b).val = 0 ↔ b = (fun _ => 0) := by

commit-pinned source · Verso Blueprint panel

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

theorem initial_padding {q : ℕ} (b : PrimitiveBasis q) :
    padVector (fun _ : Fin 1 => (1 : ℂ)) (primitiveBasisLEEquiv q b) =
      evalPrimitiveCircuit ([] : PrimitiveCircuit q) b (fun _ => 0) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “run circuits clean”; the hypotheses and conclusion in the code panel fix its exact scope. Actual local circuit columns imply the complete sequential source state from an empty initial circuit, including terminal cleanup.

theorem run_circuits_clean {n q : ℕ} (D : Chain n 1 1) (hB : maxBond D ≤ 2 ^ q)
    (stages : ℕ → PrimitiveCircuit (q + 1))
    (columns : ∀ t, t < n → ∀ bit (b a : PrimitiveBasis q),
      (primitiveBasisLEEquiv q a).val < rankAt D t →
      evalPrimitiveCircuit (stages t) (Fin.snoc b bit) (Fin.snoc a 0) =
        paddedAt D t (bit, primitiveBasisLEEquiv q b) (primitiveBasisLEEquiv q a))
    (x : PrimitiveBasis n) (b : PrimitiveBasis q) :
    run (fun t => circuitStage (stages t))
      (fun c => evalPrimitiveCircuit ([] : PrimitiveCircuit q) c (fun _ => 0)) n (x, b) =
      if b = (fun _ => 0) then (contract D (wordOfBasis x) 0 0 : ℂ) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “public circuit clean”; the hypotheses and conclusion in the code panel fix its exact scope. The published data-low/bond-high circuit realizes the chain in the corresponding most-significant-bit-first word order.

theorem publicCircuit_clean {n q : ℕ} (D : Chain n 1 1) (hB : maxBond D ≤ 2 ^ q)
    (stages : ℕ → PrimitiveCircuit (q + 1))
    (columns : ∀ t, t < n → ∀ bit (b a : PrimitiveBasis q),
      (primitiveBasisLEEquiv q a).val < rankAt D t →
      evalPrimitiveCircuit (stages t) (Fin.snoc b bit) (Fin.snoc a 0) =
        paddedAt D t (bit, primitiveBasisLEEquiv q b) (primitiveBasisLEEquiv q a))
    (x : PrimitiveBasis n) (b : PrimitiveBasis q) :
    evalPrimitiveCircuit (SequentialPrimitiveAssembly.publicCircuit [] stages n)
      (Fin.append x b) (fun _ => 0) = if b = (fun _ => 0) then
        (contract D (wordOfBasis (fun i => x i.rev)) 0 0 : ℂ) else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “assemble gate count”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem assemble_gateCount (q : ℕ) (stages : ℕ → PrimitiveCircuit (q + 1)) (n : ℕ) :
    (SequentialPrimitiveAssembly.assemble q stages n).gateCount =
      ∑ t ∈ Finset.range n, (stages t).gateCount := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “public circuit gate count bound”; the hypotheses and conclusion in the code panel fix its exact scope. Gate-list length, not only an arithmetic count proxy, is bounded.

theorem publicCircuit_gateCount_bound {q : ℕ} (stages : ℕ → PrimitiveCircuit (q + 1))
    (n bound : ℕ) (h : ∀ t, t < n → (stages t).gateCount ≤ bound) :
    (SequentialPrimitiveAssembly.publicCircuit [] stages n).gateCount ≤ n * bound := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “exists primitive preparation”; the hypotheses and conclusion in the code panel fix its exact scope. Any bounded normalized nonempty real scalar-boundary tensor train has an actual clean primitive preparation.

theorem exists_primitive_preparation {n q : ℕ} (C : Chain (n + 1) 1 1)
    (hB : maxBond C ≤ 2 ^ q)
    (hNorm : (∑ x : Word (n + 1), (contract C x 0 0) ^ 2) = 1) :
    ∃ circuit : PrimitiveCircuit ((n + 1) + q),
      circuit.gateCount ≤ (n + 1) * (6 * (2 ^ q) ^ 3) ∧ circuit.resource.oracleCalls = 0 ∧
      evalPrimitiveCircuit circuit ∈ _root_.Matrix.unitaryGroup (PrimitiveBasis ((n + 1) + q)) ℂ ∧
      ∀ (x : PrimitiveBasis (n + 1)) (b : PrimitiveBasis q),
        evalPrimitiveCircuit circuit (Fin.append x b) (fun _ => 0) =
          if b = (fun _ => 0) then
            (contract C (wordOfBasis (fun i => x i.rev)) 0 0 : ℂ) else 0 := by

commit-pinned source · Verso Blueprint panel