6.6. QuantumBlockEncoding/ConstructiveTensorTrain.lean🔗

15 explicit public declarations, in source order.

Definition6.6.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “core factorization”. A proposition-valued field is a requirement until a constructor supplies it. The physical bit/right-bond indexing is retained in the returned core.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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 physical bit/right-bond indexing is retained in the returned core.

Declaration kind. structure.

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

Lean code for Definition6.6.1●1 definition

structure(4 fields)defined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

structure QuantumBlockEncoding.ConstructiveTensorTrain.CoreFactorization {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r) : Type

structure QuantumBlockEncoding.ConstructiveTensorTrain.CoreFactorization
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r) :
  Type

The physical bit/right-bond indexing is retained in the returned core.

Fields

R : Matrix (Fin l) (Fin (min l (2 * r))) ℝ

Q : QuantumBlockEncoding.TensorTrainCanonical.Core (min l (2 * r)) r

factorization : A = self.R * self.Q

orthogonal : self.Q * Matrix.transpose self.Q = 1

Definition6.6.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factor core”. Relabel the deterministic matrix factors by the explicit product index.

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

Technical source note. Relabel the deterministic matrix factors by the explicit product index.

Declaration kind. def.

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

Lean code for Definition6.6.2●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrain.factorCore {l r : ℕ}
  (A : QuantumBlockEncoding.TensorTrainCanonical.Core l r) :
  QuantumBlockEncoding.ConstructiveTensorTrain.CoreFactorization A

def QuantumBlockEncoding.ConstructiveTensorTrain.factorCore
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.TensorTrainCanonical.Core
      l r) :
  QuantumBlockEncoding.ConstructiveTensorTrain.CoreFactorization
    A

Relabel the deterministic matrix factors by the explicit product index.

Definition6.6.3

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “result”. A proposition-valued field is a requirement until a constructor supplies it. Concrete canonical data, indexed by the precise original chain.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Technical source note. Concrete canonical data, indexed by the precise original chain.

Declaration kind. structure.

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

Lean code for Definition6.6.3●1 definition

structure(6 fields)defined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

structure QuantumBlockEncoding.ConstructiveTensorTrain.Result {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) : Type

structure QuantumBlockEncoding.ConstructiveTensorTrain.Result
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  Type

Concrete canonical data, indexed by the precise original chain.

Fields

rank : ℕ

residual : Matrix (Fin l) (Fin self.rank) ℝ

canonical : QuantumBlockEncoding.TensorTrainCanonical.Chain n self.rank r

rightCanonical : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical self.canonical

rankReduced : QuantumBlockEncoding.TensorTrainCanonical.RankReduced C self.canonical

action : ∀ (x : QuantumBlockEncoding.TensorTrainCanonical.Word n),
  QuantumBlockEncoding.TensorTrainCanonical.contract C x =
    self.residual * QuantumBlockEncoding.TensorTrainCanonical.contract self.canonical x

Definition6.6.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “canonicalize”. Structural recursion on the source chain; no factor or basis selection.

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

Technical source note. Structural recursion on the source chain; no factor or basis selection.

Declaration kind. def.

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

Lean code for Definition6.6.4●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.ConstructiveTensorTrain.Result C

def QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.ConstructiveTensorTrain.Result
    C

Structural recursion on the source chain; no factor or basis selection.

Theorem6.6.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize right canonical”; 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.

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/ConstructiveTensorTrain.lean:73. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.5●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_rightCanonical
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
        C).canonical

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_rightCanonical
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
        C).canonical

Theorem6.6.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize rank reduced”; 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.

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/ConstructiveTensorTrain.lean:76. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.6●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_rankReduced
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.RankReduced C
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
        C).canonical

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_rankReduced
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.RankReduced
    C
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
        C).canonical

Theorem6.6.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize action”; 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.

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/ConstructiveTensorTrain.lean:79. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.7●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_action
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word n) :
  QuantumBlockEncoding.TensorTrainCanonical.contract C x =
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).residual *
      QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
            C).canonical
        x

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_action
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      n) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      C x =
    (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).residual *
      QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
            C).canonical
        x

Theorem6.6.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize max bond le”; 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.

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/ConstructiveTensorTrain.lean:83. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_maxBond_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).canonical ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond C

theorem QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize_maxBond_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).canonical ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      C

Definition6.6.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “boundary”. The returned residual converts an original boundary into its new boundary.

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

Technical source note. The returned residual converts an original boundary into its new boundary.

Declaration kind. def.

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

Lean code for Definition6.6.9●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrain.boundary {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (v : Fin l → ℝ) :
  Fin
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).rank →
    ℝ

def QuantumBlockEncoding.ConstructiveTensorTrain.boundary
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (v : Fin l → ℝ) :
  Fin
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).rank →
    ℝ

The returned residual converts an original boundary into its new boundary.

Theorem6.6.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary action”; 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.

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/ConstructiveTensorTrain.lean:91. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.10●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_action {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (v : Fin l → ℝ)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word n) :
  Matrix.vecMul v
      (QuantumBlockEncoding.TensorTrainCanonical.contract C x) =
    Matrix.vecMul
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary C v)
      (QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
            C).canonical
        x)

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_action
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (v : Fin l → ℝ)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      n) :
  Matrix.vecMul v
      (QuantumBlockEncoding.TensorTrainCanonical.contract
        C x) =
    Matrix.vecMul
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary
        C v)
      (QuantumBlockEncoding.TensorTrainCanonical.contract
        (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
            C).canonical
        x)

Theorem6.6.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary mass”; the hypotheses and conclusion in the code panel fix its exact scope. Total source mass is obtained from the small returned residual boundary.

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

Technical source note. Total source mass is obtained from the small returned residual boundary.

Declaration kind. theorem.

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

Lean code for Theorem6.6.11●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_mass {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary C v)

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_mass
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (v : Fin l → ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.chainMass
      C v =
    QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary
        C v)

Total source mass is obtained from the small returned residual boundary.

Theorem6.6.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary normalized”; 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.

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/ConstructiveTensorTrain.lean:103. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.12●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_normalized
  {n l r : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n l r)
  (v : Fin l → ℝ)
  (normalized :
    QuantumBlockEncoding.TensorTrainCanonical.chainMass C v = 1) :
  QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary C v) =
    1

theorem QuantumBlockEncoding.ConstructiveTensorTrain.boundary_normalized
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r)
  (v : Fin l → ℝ)
  (normalized :
    QuantumBlockEncoding.TensorTrainCanonical.chainMass
        C v =
      1) :
  QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.boundary
        C v) =
    1

Definition6.6.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “state boundary”. Concrete scalar-boundary state data, without requiring normalization.

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

Technical source note. Concrete scalar-boundary state data, without requiring normalization.

Declaration kind. def.

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

Lean code for Definition6.6.13●1 definition

defdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

def QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary {n : ℕ}
  (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1) :
  Fin
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).rank →
    ℝ

def QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1) :
  Fin
      (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
          C).rank →
    ℝ

Concrete scalar-boundary state data, without requiring normalization.

Theorem6.6.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “state boundary action”; 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.

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/ConstructiveTensorTrain.lean:111. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.14●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary_action
  {n : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word n) :
  QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 =
    ∑ a,
      QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary C a *
        QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
              C).canonical
          x a 0

theorem QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary_action
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      n) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      C x 0 0 =
    ∑ a,
      QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary
          C a *
        QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
              C).canonical
          x a 0

Theorem6.6.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “state boundary normalized”; 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.

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/ConstructiveTensorTrain.lean:117. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.6.15●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveTensorTrain.lean

complete

theorem QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary_normalized
  {n : ℕ} (C : QuantumBlockEncoding.TensorTrainCanonical.Chain n 1 1)
  (normalized :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract C x 0 0 ^ 2 =
      1) :
  QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary C) =
    1

theorem QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary_normalized
  {n : ℕ}
  (C :
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n 1 1)
  (normalized :
    ∑ x,
        QuantumBlockEncoding.TensorTrainCanonical.contract
            C x 0 0 ^
          2 =
      1) :
  QuantumBlockEncoding.TensorTrainCanonical.mass
      (QuantumBlockEncoding.ConstructiveTensorTrain.stateBoundary
        C) =
    1