ASPBE Lean Blueprint

6.28. QuantumBlockEncoding/SequentialBondPreparation.lean🔗

35 explicit public declarations, in source order.

Definition6.28.1
uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “core”. A core emits one bit and changes the bond.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A core emits one bit and changes the bond.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.1●1 definition
  • abbrevdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    abbrev QuantumBlockEncoding.SequentialBondPreparation.Core.{u_2}
  (B : Type u_2) : Type u_2
    abbrev QuantumBlockEncoding.SequentialBondPreparation.Core.{u_2}
  (B : Type u_2) : Type u_2
    A core emits one bit and changes the bond.
Definition6.28.2
uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “stage”. The square, full local matrix; its nonzero-bit input columns are not specified by a tensor core and must be supplied by an actual completion.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The square, full local matrix; its nonzero-bit input columns are not specified by a tensor core and must be supplied by an actual completion.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.2●1 definition
  • abbrevdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    abbrev QuantumBlockEncoding.SequentialBondPreparation.Stage.{u_2}
  (B : Type u_2) : Type u_2
    abbrev QuantumBlockEncoding.SequentialBondPreparation.Stage.{u_2}
  (B : Type u_2) : Type u_2
    The square, full local matrix; its nonzero-bit input columns are not
specified by a tensor core and must be supplied by an actual completion.
Definition6.28.3
uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “bond state”. State amplitudes after exactly 'n' output bits have been emitted.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. State amplitudes after exactly 'n' output bits have been emitted.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:36. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.3●1 definition
  • abbrevdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    abbrev QuantumBlockEncoding.SequentialBondPreparation.BondState.{u_2} (n : ℕ)
  (B : Type u_2) : Type u_2
    abbrev QuantumBlockEncoding.SequentialBondPreparation.BondState.{u_2}
  (n : ℕ) (B : Type u_2) : Type u_2
    State amplitudes after exactly `n` output bits have been emitted.
Definition6.28.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “fresh zero”. Add the next output bit in zero, without changing any existing amplitude.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Add the next output bit in zero, without changing any existing amplitude.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:39. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.4●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.freshZero.{u_1}
  {B : Type u_1} {n : ℕ}
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B) :
  QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B → ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.freshZero.{u_1}
  {B : Type u_1} {n : ℕ}
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B) :
  QuantumBlockEncoding.PrimitiveBasis n ×
      Fin 2 × B →
    ℂ
    Add the next output bit in zero, without changing any existing amplitude.
Definition6.28.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “lift stage”. Local stage tensored with the identity on all already emitted bits.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Local stage tensored with the identity on all already emitted bits.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.5●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.liftStage.{u_1}
  {B : Type u_1} (n : ℕ)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B) :
  Matrix (QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B)
    (QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B) ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.liftStage.{u_1}
  {B : Type u_1} (n : ℕ)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B) :
  Matrix
    (QuantumBlockEncoding.PrimitiveBasis
        n ×
      Fin 2 × B)
    (QuantumBlockEncoding.PrimitiveBasis
        n ×
      Fin 2 × B)
    ℂ
    Local stage tensored with the identity on all already emitted bits.
Theorem6.28.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift stage apply”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:50. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.liftStage_apply.{u_1}
  {B : Type u_1} (n : ℕ)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (r c : QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B) :
  QuantumBlockEncoding.SequentialBondPreparation.liftStage n U r c =
    if r.1 = c.1 then U r.2 c.2 else 0
    theorem QuantumBlockEncoding.SequentialBondPreparation.liftStage_apply.{u_1}
  {B : Type u_1} (n : ℕ)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (r c :
    QuantumBlockEncoding.PrimitiveBasis
        n ×
      Fin 2 × B) :
  QuantumBlockEncoding.SequentialBondPreparation.liftStage
      n U r c =
    if r.1 = c.1 then U r.2 c.2 else 0
Definition6.28.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “step”. A genuine matrix-vector action followed only by a basis regrouping.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A genuine matrix-vector action followed only by a basis regrouping.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:56. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.7●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.step.{u_1} {B : Type u_1}
  [Fintype B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B) :
  QuantumBlockEncoding.SequentialBondPreparation.BondState (n + 1) B
    def QuantumBlockEncoding.SequentialBondPreparation.step.{u_1}
  {B : Type u_1} [Fintype B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B) :
  QuantumBlockEncoding.SequentialBondPreparation.BondState
    (n + 1) B
    A genuine matrix-vector action followed only by a basis regrouping.
Theorem6.28.8
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “step apply”; the hypotheses and conclusion in the code panel fix its exact scope. Only the clean-input columns of a local stage affect an emitted state.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Only the clean-input columns of a local stage affect an emitted state. The sum over passive prefixes and fresh-bit inputs collapses exactly.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:64. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_apply.{u_1}
  {B : Type u_1} [Fintype B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step U v (x, b) =
    ∑ a, U (x (Fin.last n), b) (0, a) * v (Fin.init x, a)
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_apply.{u_1}
  {B : Type u_1} [Fintype B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U v (x, b) =
    ∑ a,
      U (x (Fin.last n), b) (0, a) *
        v (Fin.init x, a)
    Only the clean-input columns of a local stage affect an emitted state.
The sum over passive prefixes and fresh-bit inputs collapses exactly.
Theorem6.28.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “lift stage unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Unitarity of the full local completion gives unitarity after adding arbitrarily many passive emitted wires.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Unitarity of the full local completion gives unitarity after adding arbitrarily many passive emitted wires.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:72. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.liftStage_unitary.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B] (n : ℕ)
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (hU : U ∈ Matrix.unitaryGroup (Fin 2 × B) ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.liftStage n U ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B) ℂ
    theorem QuantumBlockEncoding.SequentialBondPreparation.liftStage_unitary.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B] (n : ℕ)
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (hU :
    U ∈
      Matrix.unitaryGroup (Fin 2 × B) ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.liftStage
      n U ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.PrimitiveBasis
          n ×
        Fin 2 × B)
      ℂ
    Unitarity of the full local completion gives unitarity after adding
arbitrarily many passive emitted wires.
Definition6.28.10
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “core slice”. Fixing an emitted bit leaves a bond-to-bond transfer matrix.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Fixing an emitted bit leaves a bond-to-bond transfer matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.10●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.coreSlice.{u_1}
  {B : Type u_1}
  (K : QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (bit : Fin 2) : Matrix B B ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.coreSlice.{u_1}
  {B : Type u_1}
  (K :
    QuantumBlockEncoding.SequentialBondPreparation.Core
      B)
  (bit : Fin 2) : Matrix B B ℂ
    Fixing an emitted bit leaves a bond-to-bond transfer matrix.
Definition6.28.11
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “transfer”. Chronological tensor contraction.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Chronological tensor contraction. The last emitted core multiplies on the left, in the same convention as 'evalPrimitiveCircuit'.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:86. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.11●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.transfer.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (n : ℕ) : QuantumBlockEncoding.PrimitiveBasis n → Matrix B B ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.transfer.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (n : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis n →
    Matrix B B ℂ
    Chronological tensor contraction. The last emitted core multiplies on
the left, in the same convention as `evalPrimitiveCircuit`.
Definition6.28.12
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “run”. Explicit initial boundary, followed by sequential matrix actions.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Explicit initial boundary, followed by sequential matrix actions. At stage zero there are no output bits and the bond amplitude is 'boundary'.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:93. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.12●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.run.{u_1} {B : Type u_1}
  [Fintype B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (boundary : B → ℂ) (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.BondState n B
    def QuantumBlockEncoding.SequentialBondPreparation.run.{u_1}
  {B : Type u_1} [Fintype B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (boundary : B → ℂ) (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.BondState
    n B
    Explicit initial boundary, followed by sequential matrix actions.
At stage zero there are no output bits and the bond amplitude is `boundary`.
Theorem6.28.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run eq transfer”; the hypotheses and conclusion in the code panel fix its exact scope. Local clean-column equalities suffice to identify the complete state with the tensor contraction at every length; no global state action is assumed.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Local clean-column equalities suffice to identify the complete state with the tensor contraction at every length; no global state action is assumed.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:100. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_eq_transfer.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      U t (bit, b) (0, a) = K t (bit, b) a)
  (boundary : B → ℂ) (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U boundary n
      (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer K n
          x).mulVec
      boundary b
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_eq_transfer.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      U t (bit, b) (0, a) =
        K t (bit, b) a)
  (boundary : B → ℂ) (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U boundary n (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer
          K n x).mulVec
      boundary b
    Local clean-column equalities suffice to identify the complete state
with the tensor contraction at every length; no global state action is assumed.
Definition6.28.14
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “basis boundary”. Initial computational-basis boundary for the bond.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Initial computational-basis boundary for the bond.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:113. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.14●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.basisBoundary.{u_1}
  {B : Type u_1} [DecidableEq B] (initial : B) : B → ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.basisBoundary.{u_1}
  {B : Type u_1} [DecidableEq B]
  (initial : B) : B → ℂ
    Initial computational-basis boundary for the bond.
Theorem6.28.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run basis boundary”; the hypotheses and conclusion in the code panel fix its exact scope. Starting from a basis boundary extracts the corresponding transfer column.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Starting from a basis boundary extracts the corresponding transfer column.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:116. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_basisBoundary.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      U t (bit, b) (0, a) = K t (bit, b) a)
  (initial : B) (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
        initial)
      n (x, b) =
    QuantumBlockEncoding.SequentialBondPreparation.transfer K n x b
      initial
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_basisBoundary.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      U t (bit, b) (0, a) =
        K t (bit, b) a)
  (initial : B) (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U
      (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
        initial)
      n (x, b) =
    QuantumBlockEncoding.SequentialBondPreparation.transfer
      K n x b initial
    Starting from a basis boundary extracts the corresponding transfer column.
Theorem6.28.16
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “transfer boundary supported”; the hypotheses and conclusion in the code panel fix its exact scope. If every core is zero outside the next active bond set, its contracted state has that support.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. If every core is zero outside the next active bond set, its contracted state has that support. This allows ranks to shrink inside a fixed register.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.transfer_boundary_supported.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (active : ℕ → B → Prop) (boundary : B → ℂ)
  (initialSupport : ∀ (b : B), ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n) (b : B)
  (inactive : ¬active n b) :
  (QuantumBlockEncoding.SequentialBondPreparation.transfer K n x).mulVec
      boundary b =
    0
    theorem QuantumBlockEncoding.SequentialBondPreparation.transfer_boundary_supported.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (active : ℕ → B → Prop)
  (boundary : B → ℂ)
  (initialSupport :
    ∀ (b : B),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) (inactive : ¬active n b) :
  (QuantumBlockEncoding.SequentialBondPreparation.transfer
          K n x).mulVec
      boundary b =
    0
    If every core is zero outside the next active bond set, its contracted
state has that support. This allows ranks to shrink inside a fixed register.
Theorem6.28.17
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run eq transfer of supported”; the hypotheses and conclusion in the code panel fix its exact scope. Rank-changing version of 'run_eq_transfer': only columns for occupied input bond labels must agree.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Rank-changing version of 'run_eq_transfer': only columns for occupied input bond labels must agree. Unused completion columns may be arbitrary. The support invariant is proved from the cores, not assumed of the full run.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:140. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_eq_transfer_of_supported.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (active : ℕ → B → Prop) (boundary : B → ℂ)
  (initialSupport : ∀ (b : B), ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a → U t (bit, b) (0, a) = K t (bit, b) a)
  (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run U boundary n
      (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer K n
          x).mulVec
      boundary b
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_eq_transfer_of_supported.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (active : ℕ → B → Prop)
  (boundary : B → ℂ)
  (initialSupport :
    ∀ (b : B),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a →
        U t (bit, b) (0, a) =
          K t (bit, b) a)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U boundary n (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer
          K n x).mulVec
      boundary b
    Rank-changing version of `run_eq_transfer`: only columns for occupied
input bond labels must agree. Unused completion columns may be arbitrary.
The support invariant is proved from the cores, not assumed of the full run.
Theorem6.28.18
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run supported”; the hypotheses and conclusion in the code panel fix its exact scope. No leakage to inactive labels at any intermediate stage.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. No leakage to inactive labels at any intermediate stage.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:166. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_supported.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (active : ℕ → B → Prop) (boundary : B → ℂ)
  (initialSupport : ∀ (b : B), ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a → U t (bit, b) (0, a) = K t (bit, b) a)
  (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n) (b : B)
  (inactive : ¬active n b) :
  QuantumBlockEncoding.SequentialBondPreparation.run U boundary n
      (x, b) =
    0
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_supported.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (active : ℕ → B → Prop)
  (boundary : B → ℂ)
  (initialSupport :
    ∀ (b : B),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a →
        U t (bit, b) (0, a) =
          K t (bit, b) a)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b : B) (inactive : ¬active n b) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      U boundary n (x, b) =
    0
    No leakage to inactive labels at any intermediate stage.
Definition6.28.19
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “terminal core”. A terminal bond of dimension one, embedded at a chosen padded label.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A terminal bond of dimension one, embedded at a chosen padded label.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:177. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.19●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.terminalCore.{u_1}
  {B : Type u_1} [DecidableEq B] (clean : B) (T : Matrix (Fin 2) B ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.Core B
    def QuantumBlockEncoding.SequentialBondPreparation.terminalCore.{u_1}
  {B : Type u_1} [DecidableEq B]
  (clean : B) (T : Matrix (Fin 2) B ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.Core
    B
    A terminal bond of dimension one, embedded at a chosen padded label.
Theorem6.28.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “step terminal core”; the hypotheses and conclusion in the code panel fix its exact scope. Appending a rank-one terminal bond factors the *whole* state as a clean bond times the contracted output amplitude; this is not a projection theorem.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Appending a rank-one terminal bond factors the *whole* state as a clean bond times the contracted output amplitude; this is not a projection theorem.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:182. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.SequentialBondPreparation.terminalCore
          clean T (bit, b) a)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step U v (x, b) =
    if b = clean then ∑ a, T (x (Fin.last n)) a * v (Fin.init x, a)
    else 0
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.SequentialBondPreparation.terminalCore
          clean T (bit, b) a)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U v (x, b) =
    if b = clean then
      ∑ a,
        T (x (Fin.last n)) a *
          v (Fin.init x, a)
    else 0
    Appending a rank-one terminal bond factors the *whole* state as a clean
bond times the contracted output amplitude; this is not a projection theorem.
Theorem6.28.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “step terminal core no leakage”; the hypotheses and conclusion in the code panel fix its exact scope. Zero leakage to every non-clean bond label, with no measurement or postselection.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Zero leakage to every non-clean bond label, with no measurement or postselection. Local terminal-column synthesis is the explicit prerequisite.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:194. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore_no_leakage.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.SequentialBondPreparation.terminalCore
          clean T (bit, b) a)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : B)
  (h : b ≠ clean) :
  QuantumBlockEncoding.SequentialBondPreparation.step U v (x, b) = 0
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore_no_leakage.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      U (bit, b) (0, a) =
        QuantumBlockEncoding.SequentialBondPreparation.terminalCore
          clean T (bit, b) a)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : B) (h : b ≠ clean) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U v (x, b) =
    0
    Zero leakage to every non-clean bond label, with no measurement or
postselection. Local terminal-column synthesis is the explicit prerequisite.
Theorem6.28.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “step terminal core of supported”; the hypotheses and conclusion in the code panel fix its exact scope. Padded-register terminal cleanup on the occupied input subspace only.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Padded-register terminal cleanup on the occupied input subspace only. Requiring this terminal action on *all* padded input columns would be incompatible with unitarity for bond dimension greater than two.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:204. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore_of_supported.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B)
  (active : B → Prop) (clean : B) (T : Matrix (Fin 2) B ℂ)
  (support :
    ∀ (p : QuantumBlockEncoding.PrimitiveBasis n) (a : B),
      ¬active a → v (p, a) = 0)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      active a →
        U (bit, b) (0, a) =
          QuantumBlockEncoding.SequentialBondPreparation.terminalCore
            clean T (bit, b) a)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step U v (x, b) =
    if b = clean then ∑ a, T (x (Fin.last n)) a * v (Fin.init x, a)
    else 0
    theorem QuantumBlockEncoding.SequentialBondPreparation.step_terminalCore_of_supported.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B)
  (active : B → Prop) (clean : B)
  (T : Matrix (Fin 2) B ℂ)
  (support :
    ∀
      (p :
        QuantumBlockEncoding.PrimitiveBasis
          n)
      (a : B), ¬active a → v (p, a) = 0)
  (cleanColumns :
    ∀ (bit : Fin 2) (b a : B),
      active a →
        U (bit, b) (0, a) =
          QuantumBlockEncoding.SequentialBondPreparation.terminalCore
            clean T (bit, b) a)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      U v (x, b) =
    if b = clean then
      ∑ a,
        T (x (Fin.last n)) a *
          v (Fin.init x, a)
    else 0
    Padded-register terminal cleanup on the occupied input subspace only.
Requiring this terminal action on *all* padded input columns would be
incompatible with unitarity for bond dimension greater than two.
Theorem6.28.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run terminal clean”; the hypotheses and conclusion in the code panel fix its exact scope. Complete state action after a supported sequential run and one terminal stage.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Complete state action after a supported sequential run and one terminal stage. The target is the explicit transfer contraction, and every non-clean bond amplitude is zero. No postselection, target-state oracle, or global state-action equality is among the hypotheses.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:228. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_terminal_clean.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (K : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Core B)
  (active : ℕ → B → Prop) (boundary : B → ℂ)
  (initialSupport : ∀ (b : B), ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a → U t (bit, b) (0, a) = K t (bit, b) a)
  (n : ℕ)
  (lastU : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (lastColumns :
    ∀ (bit : Fin 2) (b a : B),
      active n a →
        lastU (bit, b) (0, a) =
          QuantumBlockEncoding.SequentialBondPreparation.terminalCore
            clean T (bit, b) a)
  (x : QuantumBlockEncoding.PrimitiveBasis (n + 1)) (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step lastU
      (QuantumBlockEncoding.SequentialBondPreparation.run U boundary n)
      (x, b) =
    if b = clean then
      ∑ a,
        T (x (Fin.last n)) a *
          (QuantumBlockEncoding.SequentialBondPreparation.transfer K n
                (Fin.init x)).mulVec
            boundary a
    else 0
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_terminal_clean.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        B)
  (active : ℕ → B → Prop)
  (boundary : B → ℂ)
  (initialSupport :
    ∀ (b : B),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (cleanColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b a : B),
      active t a →
        U t (bit, b) (0, a) =
          K t (bit, b) a)
  (n : ℕ)
  (lastU :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (clean : B) (T : Matrix (Fin 2) B ℂ)
  (lastColumns :
    ∀ (bit : Fin 2) (b a : B),
      active n a →
        lastU (bit, b) (0, a) =
          QuantumBlockEncoding.SequentialBondPreparation.terminalCore
            clean T (bit, b) a)
  (x :
    QuantumBlockEncoding.PrimitiveBasis
      (n + 1))
  (b : B) :
  QuantumBlockEncoding.SequentialBondPreparation.step
      lastU
      (QuantumBlockEncoding.SequentialBondPreparation.run
        U boundary n)
      (x, b) =
    if b = clean then
      ∑ a,
        T (x (Fin.last n)) a *
          (QuantumBlockEncoding.SequentialBondPreparation.transfer
                K n (Fin.init x)).mulVec
            boundary a
    else 0
    Complete state action after a supported sequential run and one terminal
stage. The target is the explicit transfer contraction, and every non-clean
bond amplitude is zero. No postselection, target-state oracle, or global
state-action equality is among the hypotheses.
Definition6.28.24
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “local basis equiv”. The local primitive circuit uses the low 'q' wires for the bond and its highest wire for the fresh emitted bit.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The local primitive circuit uses the low 'q' wires for the bond and its highest wire for the fresh emitted bit. This equivalence makes that order explicit.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:248. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.24●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.localBasisEquiv (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis (q + 1) ≃
    Fin 2 × QuantumBlockEncoding.PrimitiveBasis q
    def QuantumBlockEncoding.SequentialBondPreparation.localBasisEquiv
  (q : ℕ) :
  QuantumBlockEncoding.PrimitiveBasis
      (q + 1) ≃
    Fin 2 ×
      QuantumBlockEncoding.PrimitiveBasis
        q
    The local primitive circuit uses the low `q` wires for the bond and its
highest wire for the fresh emitted bit. This equivalence makes that order explicit.
Definition6.28.25
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “circuit stage”. Exact local stage supplied by a primitive circuit, not an opaque oracle.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Exact local stage supplied by a primitive circuit, not an opaque oracle.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:252. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.25●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.circuitStage {q : ℕ}
  (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.Stage
    (QuantumBlockEncoding.PrimitiveBasis q)
    def QuantumBlockEncoding.SequentialBondPreparation.circuitStage
  {q : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.Stage
    (QuantumBlockEncoding.PrimitiveBasis
      q)
    Exact local stage supplied by a primitive circuit, not an opaque oracle.
Theorem6.28.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “circuit stage apply”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:256. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.circuitStage_apply
  {q : ℕ} (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (bit bit' : Fin 2) (b a : QuantumBlockEncoding.PrimitiveBasis q) :
  QuantumBlockEncoding.SequentialBondPreparation.circuitStage c (bit, b)
      (bit', a) =
    QuantumBlockEncoding.evalPrimitiveCircuit c (Fin.snoc b bit)
      (Fin.snoc a bit')
    theorem QuantumBlockEncoding.SequentialBondPreparation.circuitStage_apply
  {q : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1))
  (bit bit' : Fin 2)
  (b a :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  QuantumBlockEncoding.SequentialBondPreparation.circuitStage
      c (bit, b) (bit', a) =
    QuantumBlockEncoding.evalPrimitiveCircuit
      c (Fin.snoc b bit) (Fin.snoc a bit')
Theorem6.28.27
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “circuit stage unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Primitive stages have checked full unitarity, independently of whether their active columns implement the intended tensor cores.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Primitive stages have checked full unitarity, independently of whether their active columns implement the intended tensor cores.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:264. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.circuitStage_unitary
  {q : ℕ} (c : QuantumBlockEncoding.PrimitiveCircuit (q + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.circuitStage c ∈
    Matrix.unitaryGroup (Fin 2 × QuantumBlockEncoding.PrimitiveBasis q)
      ℂ
    theorem QuantumBlockEncoding.SequentialBondPreparation.circuitStage_unitary
  {q : ℕ}
  (c :
    QuantumBlockEncoding.PrimitiveCircuit
      (q + 1)) :
  QuantumBlockEncoding.SequentialBondPreparation.circuitStage
      c ∈
    Matrix.unitaryGroup
      (Fin 2 ×
        QuantumBlockEncoding.PrimitiveBasis
          q)
      ℂ
    Primitive stages have checked full unitarity, independently of whether
their active columns implement the intended tensor cores.
Theorem6.28.28
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “run circuit stages eq transfer”; the hypotheses and conclusion in the code panel fix its exact scope. Direct instantiation with primitive-circuit stages.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Direct instantiation with primitive-circuit stages. The sole compiler alignment premise is stated on active clean-input columns, in actual 'evalPrimitiveCircuit' semantics. This does not synthesize these circuits or prove a gate-count bound.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:272. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_circuitStages_eq_transfer
  {q : ℕ} (circuits : ℕ → QuantumBlockEncoding.PrimitiveCircuit (q + 1))
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        (QuantumBlockEncoding.PrimitiveBasis q))
  (active : ℕ → QuantumBlockEncoding.PrimitiveBasis q → Prop)
  (boundary : QuantumBlockEncoding.PrimitiveBasis q → ℂ)
  (initialSupport :
    ∀ (b : QuantumBlockEncoding.PrimitiveBasis q),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2)
      (b a : QuantumBlockEncoding.PrimitiveBasis q),
      ¬active (t + 1) b → K t (bit, b) a = 0)
  (compilerColumns :
    ∀ (t : ℕ) (bit : Fin 2) (b : Fin q → Fin 2)
      (a : QuantumBlockEncoding.PrimitiveBasis q),
      active t a →
        QuantumBlockEncoding.evalPrimitiveCircuit (circuits t)
            (Fin.snoc b bit) (Fin.snoc a 0) =
          K t (bit, b) a)
  (n : ℕ) (x : QuantumBlockEncoding.PrimitiveBasis n)
  (b : QuantumBlockEncoding.PrimitiveBasis q) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (circuits t))
      boundary n (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer K n
          x).mulVec
      boundary b
    theorem QuantumBlockEncoding.SequentialBondPreparation.run_circuitStages_eq_transfer
  {q : ℕ}
  (circuits :
    ℕ →
      QuantumBlockEncoding.PrimitiveCircuit
        (q + 1))
  (K :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Core
        (QuantumBlockEncoding.PrimitiveBasis
          q))
  (active :
    ℕ →
      QuantumBlockEncoding.PrimitiveBasis
          q →
        Prop)
  (boundary :
    QuantumBlockEncoding.PrimitiveBasis
        q →
      ℂ)
  (initialSupport :
    ∀
      (b :
        QuantumBlockEncoding.PrimitiveBasis
          q),
      ¬active 0 b → boundary b = 0)
  (coreSupport :
    ∀ (t : ℕ) (bit : Fin 2)
      (b a :
        QuantumBlockEncoding.PrimitiveBasis
          q),
      ¬active (t + 1) b →
        K t (bit, b) a = 0)
  (compilerColumns :
    ∀ (t : ℕ) (bit : Fin 2)
      (b : Fin q → Fin 2)
      (a :
        QuantumBlockEncoding.PrimitiveBasis
          q),
      active t a →
        QuantumBlockEncoding.evalPrimitiveCircuit
            (circuits t) (Fin.snoc b bit)
            (Fin.snoc a 0) =
          K t (bit, b) a)
  (n : ℕ)
  (x :
    QuantumBlockEncoding.PrimitiveBasis n)
  (b :
    QuantumBlockEncoding.PrimitiveBasis
      q) :
  QuantumBlockEncoding.SequentialBondPreparation.run
      (fun t =>
        QuantumBlockEncoding.SequentialBondPreparation.circuitStage
          (circuits t))
      boundary n (x, b) =
    (QuantumBlockEncoding.SequentialBondPreparation.transfer
          K n x).mulVec
      boundary b
    Direct instantiation with primitive-circuit stages. The sole compiler
alignment premise is stated on active clean-input columns, in actual
`evalPrimitiveCircuit` semantics. This does not synthesize these circuits or
prove a gate-count bound.
Definition6.28.29
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “amplitude mass”. Sum of amplitude squared moduli, represented as a complex scalar with zero imaginary part.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Sum of amplitude squared moduli, represented as a complex scalar with zero imaginary part. Keeping the star-product form avoids norm rewrites.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:288. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.29●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass.{u_2}
  {I : Type u_2} [Fintype I] (v : I → ℂ) : ℂ
    def QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass.{u_2}
  {I : Type u_2} [Fintype I] (v : I → ℂ) :
  ℂ
    Sum of amplitude squared moduli, represented as a complex scalar with
zero imaginary part. Keeping the star-product form avoids norm rewrites.
Theorem6.28.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude mass mul vec”; the hypotheses and conclusion in the code panel fix its exact scope. Full unitary matrix action preserves total amplitude mass.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Full unitary matrix action preserves total amplitude mass.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:292. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_mulVec.{u_2}
  {I : Type u_2} [Fintype I] [DecidableEq I] (M : Matrix I I ℂ)
  (v : I → ℂ) (hM : M ∈ Matrix.unitaryGroup I ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (M.mulVec v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass v
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_mulVec.{u_2}
  {I : Type u_2} [Fintype I]
  [DecidableEq I] (M : Matrix I I ℂ)
  (v : I → ℂ)
  (hM : M ∈ Matrix.unitaryGroup I ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (M.mulVec v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      v
    Full unitary matrix action preserves total amplitude mass.
Theorem6.28.31
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude mass fresh zero”; the hypotheses and conclusion in the code panel fix its exact scope. Introducing a zero bit is norm-preserving, not a postselection.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Introducing a zero bit is norm-preserving, not a postselection.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:304. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_freshZero.{u_1}
  {B : Type u_1} [Fintype B] {n : ℕ}
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.freshZero v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass v
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_freshZero.{u_1}
  {B : Type u_1} [Fintype B] {n : ℕ}
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.freshZero
        v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      v
    Introducing a zero bit is norm-preserving, not a postselection.
Definition6.28.32
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “step basis equiv”. The regrouping of passive prefix, newly emitted bit, and bond labels.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The regrouping of passive prefix, newly emitted bit, and bond labels.

Declaration kind. def.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:309. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.28.32●1 definition
  • defdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    def QuantumBlockEncoding.SequentialBondPreparation.stepBasisEquiv.{u_2}
  (n : ℕ) (B : Type u_2) :
  QuantumBlockEncoding.PrimitiveBasis (n + 1) × B ≃
    QuantumBlockEncoding.PrimitiveBasis n × Fin 2 × B
    def QuantumBlockEncoding.SequentialBondPreparation.stepBasisEquiv.{u_2}
  (n : ℕ) (B : Type u_2) :
  QuantumBlockEncoding.PrimitiveBasis
        (n + 1) ×
      B ≃
    QuantumBlockEncoding.PrimitiveBasis
        n ×
      Fin 2 × B
    The regrouping of passive prefix, newly emitted bit, and bond labels.
Theorem6.28.33
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude mass step”; the hypotheses and conclusion in the code panel fix its exact scope. Sequential stages preserve total mass even when their occupied bond subspaces have different dimensions.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Sequential stages preserve total mass even when their occupied bond subspaces have different dimensions.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:316. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_step.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B] {n : ℕ}
  (U : QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (v : QuantumBlockEncoding.SequentialBondPreparation.BondState n B)
  (hU : U ∈ Matrix.unitaryGroup (Fin 2 × B) ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.step U v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass v
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_step.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B] {n : ℕ}
  (U :
    QuantumBlockEncoding.SequentialBondPreparation.Stage
      B)
  (v :
    QuantumBlockEncoding.SequentialBondPreparation.BondState
      n B)
  (hU :
    U ∈
      Matrix.unitaryGroup (Fin 2 × B) ℂ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.step
        U v) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      v
    Sequential stages preserve total mass even when their occupied bond
subspaces have different dimensions.
Theorem6.28.34
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude mass run”; the hypotheses and conclusion in the code panel fix its exact scope. Full sequential action is norm-preserving for every length.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. Full sequential action is norm-preserving for every length.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:327. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.34●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_run.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (boundary : B → ℂ)
  (unitary : ∀ (t : ℕ), U t ∈ Matrix.unitaryGroup (Fin 2 × B) ℂ)
  (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.run U boundary
        n) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      boundary
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_run.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (boundary : B → ℂ)
  (unitary :
    ∀ (t : ℕ),
      U t ∈
        Matrix.unitaryGroup (Fin 2 × B) ℂ)
  (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.run
        U boundary n) =
    QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      boundary
    Full sequential action is norm-preserving for every length.
Theorem6.28.35
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude mass run basis boundary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary sequential run starting at one bond basis label has total probability one at every stage.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. A unitary sequential run starting at one bond basis label has total probability one at every stage.

Declaration kind. theorem.

Source: QuantumBlockEncoding/SequentialBondPreparation.lean:336. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.28.35●1 theorem
  • theoremdefined in QuantumBlockEncoding/SequentialBondPreparation.lean
    complete
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_run_basisBoundary.{u_1}
  {B : Type u_1} [Fintype B] [DecidableEq B]
  (U : ℕ → QuantumBlockEncoding.SequentialBondPreparation.Stage B)
  (initial : B)
  (unitary : ∀ (t : ℕ), U t ∈ Matrix.unitaryGroup (Fin 2 × B) ℂ)
  (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.run U
        (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
          initial)
        n) =
    1
    theorem QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass_run_basisBoundary.{u_1}
  {B : Type u_1} [Fintype B]
  [DecidableEq B]
  (U :
    ℕ →
      QuantumBlockEncoding.SequentialBondPreparation.Stage
        B)
  (initial : B)
  (unitary :
    ∀ (t : ℕ),
      U t ∈
        Matrix.unitaryGroup (Fin 2 × B) ℂ)
  (n : ℕ) :
  QuantumBlockEncoding.SequentialBondPreparation.amplitudeMass
      (QuantumBlockEncoding.SequentialBondPreparation.run
        U
        (QuantumBlockEncoding.SequentialBondPreparation.basisBoundary
          initial)
        n) =
    1
    A unitary sequential run starting at one bond basis label has total
probability one at every stage.