6.37. QuantumBlockEncoding/StoredTensorTrain.lean🔗

30 explicit public declarations, in source order.

Definition6.37.1

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “stored core”.

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 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. abbrev.

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

Lean code for Definition6.37.1●1 definition

abbrevdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

abbrev QuantumBlockEncoding.StoredTensorTrain.StoredCore (l r : ℕ) : Type

abbrev QuantumBlockEncoding.StoredTensorTrain.StoredCore
  (l r : ℕ) : Type

Definition6.37.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “denote core”.

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 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. def.

Source: QuantumBlockEncoding/StoredTensorTrain.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.37.2●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.denoteCore {l r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r) :
  QuantumBlockEncoding.TensorTrainCanonical.Core l r

def QuantumBlockEncoding.StoredTensorTrain.denoteCore
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r) :
  QuantumBlockEncoding.TensorTrainCanonical.Core
    l r

Definition6.37.3

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “stored chain”; its constructors are the cases that downstream code must handle.

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 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. inductive.

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

Lean code for Definition6.37.3●1 definition

inductive(2 constructors, 3 parameters)defined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

inductive QuantumBlockEncoding.StoredTensorTrain.StoredChain : ℕ → ℕ → ℕ → Type

inductive QuantumBlockEncoding.StoredTensorTrain.StoredChain :
  ℕ → ℕ → ℕ → Type

Constructors

nil (r : ℕ) :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain 0 r r

cons {n l m r : ℕ}
  (head :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (tail :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain n m
      r) :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain (n + 1)
    l r

Definition6.37.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “denote chain”.

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 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. def.

Source: QuantumBlockEncoding/StoredTensorTrain.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.37.4●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.denoteChain {n l r : ℕ} :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain n l r

def QuantumBlockEncoding.StoredTensorTrain.denoteChain
  {n l r : ℕ} :
  QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r →
    QuantumBlockEncoding.TensorTrainCanonical.Chain
      n l r

Definition6.37.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sum entries”. Each callback is invoked once; its arithmetic cost remains charged.

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. Each callback is invoked once; its arithmetic cost remains charged.

Declaration kind. def.

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

Lean code for Definition6.37.5●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.sumEntries {k : ℕ} :
  (Fin k → QuantumBlockEncoding.StoredGivens.Run ℝ) →
    QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredTensorTrain.sumEntries
  {k : ℕ} :
  (Fin k →
      QuantumBlockEncoding.StoredGivens.Run
        ℝ) →
    QuantumBlockEncoding.StoredGivens.Run
      ℝ

Each callback is invoked once; its arithmetic cost remains charged.

Theorem6.37.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sum entries value”; 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/StoredTensorTrain.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.sumEntries_value {k : ℕ}
  (f : Fin k → QuantumBlockEncoding.StoredGivens.Run ℝ) :
  (QuantumBlockEncoding.StoredTensorTrain.sumEntries f).value =
    ∑ i, (f i).value

theorem QuantumBlockEncoding.StoredTensorTrain.sumEntries_value
  {k : ℕ}
  (f :
    Fin k →
      QuantumBlockEncoding.StoredGivens.Run
        ℝ) :
  (QuantumBlockEncoding.StoredTensorTrain.sumEntries
        f).value =
    ∑ i, (f i).value

Theorem6.37.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sum entries cost 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/StoredTensorTrain.lean:49. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.sumEntries_cost_le {k : ℕ}
  (f : Fin k → QuantumBlockEncoding.StoredGivens.Run ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) (B : ℕ)
  (bound : ∀ (i : Fin k), (f i).cost op ≤ B) :
  (QuantumBlockEncoding.StoredTensorTrain.sumEntries f).cost op ≤
    k *
      (B +
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op)

theorem QuantumBlockEncoding.StoredTensorTrain.sumEntries_cost_le
  {k : ℕ}
  (f :
    Fin k →
      QuantumBlockEncoding.StoredGivens.Run
        ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op)
  (B : ℕ)
  (bound :
    ∀ (i : Fin k), (f i).cost op ≤ B) :
  (QuantumBlockEncoding.StoredTensorTrain.sumEntries
          f).cost
      op ≤
    k *
      (B +
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op)

Definition6.37.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “absorption entry”. Multiply the residual into a single bit-preserving output entry.

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. Multiply the residual into a single bit-preserving output entry.

Declaration kind. def.

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

Lean code for Definition6.37.8●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.absorptionEntry {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) (a : Fin l)
  (out : Fin 2 × Fin r) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredTensorTrain.absorptionEntry
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r)
  (a : Fin l) (out : Fin 2 × Fin r) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Multiply the residual into a single bit-preserving output entry.

Theorem6.37.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorption entry value”; 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/StoredTensorTrain.lean:69. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.absorptionEntry_value {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) (a : Fin l)
  (out : Fin 2 × Fin r) :
  (QuantumBlockEncoding.StoredTensorTrain.absorptionEntry A R a
        out).value =
    QuantumBlockEncoding.TensorTrainCanonical.absorb
      (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)
      (QuantumBlockEncoding.StoredGivens.denote R) a out

theorem QuantumBlockEncoding.StoredTensorTrain.absorptionEntry_value
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r)
  (a : Fin l) (out : Fin 2 × Fin r) :
  (QuantumBlockEncoding.StoredTensorTrain.absorptionEntry
        A R a out).value =
    QuantumBlockEncoding.TensorTrainCanonical.absorb
      (QuantumBlockEncoding.StoredTensorTrain.denoteCore
        A)
      (QuantumBlockEncoding.StoredGivens.denote
        R)
      a out

Theorem6.37.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorption entry cost 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/StoredTensorTrain.lean:75. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.absorptionEntry_cost_le
  {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) (a : Fin l)
  (out : Fin 2 × Fin r) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrain.absorptionEntry A R a
          out).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op)

theorem QuantumBlockEncoding.StoredTensorTrain.absorptionEntry_cost_le
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r)
  (a : Fin l) (out : Fin 2 × Fin r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrain.absorptionEntry
          A R a out).cost
      op ≤
    m *
      (4 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op)

Definition6.37.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “absorption”.

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 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. def.

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

Lean code for Definition6.37.11●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.absorption {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore l r)

def QuantumBlockEncoding.StoredTensorTrain.absorption
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r)

Theorem6.37.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorption value”; 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/StoredTensorTrain.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.37.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_value {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredTensorTrain.absorption A R).value =
    QuantumBlockEncoding.TensorTrainCanonical.absorb
      (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)
      (QuantumBlockEncoding.StoredGivens.denote R)

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_value
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredTensorTrain.absorption
          A R).value =
    QuantumBlockEncoding.TensorTrainCanonical.absorb
      (QuantumBlockEncoding.StoredTensorTrain.denoteCore
        A)
      (QuantumBlockEncoding.StoredGivens.denote
        R)

Definition6.37.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “absorption budget”.

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 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. def.

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

Lean code for Definition6.37.13●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.absorptionBudget (l m r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredTensorTrain.absorptionBudget
  (l m r : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.37.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorption cost 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/StoredTensorTrain.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.37.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_cost_le {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrain.absorption A R).cost op ≤
    QuantumBlockEncoding.StoredTensorTrain.absorptionBudget l m r op

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_cost_le
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredTensorTrain.absorption
          A R).cost
      op ≤
    QuantumBlockEncoding.StoredTensorTrain.absorptionBudget
      l m r op

Definition6.37.15

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “core result”. A proposition-valued field is a requirement until a constructor supplies it.

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

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. structure.

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

Lean code for Definition6.37.15●1 definition

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

complete

structure QuantumBlockEncoding.StoredTensorTrain.CoreResult {l r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r) : Type

structure QuantumBlockEncoding.StoredTensorTrain.CoreResult
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r) :
  Type

Fields

R : QuantumBlockEncoding.StoredGivens.StoredMatrix l (min l (2 * r))

Q : QuantumBlockEncoding.StoredTensorTrain.StoredCore (min l (2 * r)) r

factorization : QuantumBlockEncoding.StoredTensorTrain.denoteCore A =
  QuantumBlockEncoding.StoredGivens.denote self.R * QuantumBlockEncoding.StoredTensorTrain.denoteCore self.Q

orthogonal : QuantumBlockEncoding.StoredTensorTrain.denoteCore self.Q *
    Matrix.transpose (QuantumBlockEncoding.StoredTensorTrain.denoteCore self.Q) =
  1

Definition6.37.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factor core”.

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 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. def.

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

Lean code for Definition6.37.16●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.factorCore {l r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.CoreResult A)

def QuantumBlockEncoding.StoredTensorTrain.factorCore
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.CoreResult
      A)

Definition6.37.17

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.

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

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. structure.

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

Lean code for Definition6.37.17●1 definition

structure(7 fields)defined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

structure QuantumBlockEncoding.StoredTensorTrain.Result {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) : Type

structure QuantumBlockEncoding.StoredTensorTrain.Result
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r) :
  Type

Fields

rank : ℕ

residual : QuantumBlockEncoding.StoredGivens.StoredMatrix l self.rank

canonical : QuantumBlockEncoding.StoredTensorTrain.StoredChain n self.rank r

rightCanonical : QuantumBlockEncoding.TensorTrainCanonical.RightCanonical
  (QuantumBlockEncoding.StoredTensorTrain.denoteChain self.canonical)

rankReduced : QuantumBlockEncoding.TensorTrainCanonical.RankReduced (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)
  (QuantumBlockEncoding.StoredTensorTrain.denoteChain self.canonical)

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

rank_le : self.rank ≤ l

Definition6.37.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “node budget”. Read the input tag/payload and allocate the output chain node.

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. Read the input tag/payload and allocate the output chain node.

Declaration kind. def.

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

Lean code for Definition6.37.18●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.nodeBudget :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredTensorTrain.nodeBudget :
  QuantumBlockEncoding.StoredGivens.Cost

Read the input tag/payload and allocate the output chain node.

Definition6.37.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “canonicalize”.

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 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. def.

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

Lean code for Definition6.37.19●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.canonicalize {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.Result C)

def QuantumBlockEncoding.StoredTensorTrain.canonicalize
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.Result
      C)

Theorem6.37.20

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

Lean code for Theorem6.37.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_maxBond_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredTensorTrain.canonicalize
              C).value.canonical) ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_maxBond_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        (QuantumBlockEncoding.StoredTensorTrain.canonicalize
              C).value.canonical) ≤
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        C)

Theorem6.37.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “absorption total cost 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/StoredTensorTrain.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.37.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_total_cost_le
  {l m r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l m)
  (R : QuantumBlockEncoding.StoredGivens.StoredMatrix m r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.absorption A R).cost ≤
    12 * l * m * r + 8 * l * r + 4 * l

theorem QuantumBlockEncoding.StoredTensorTrain.absorption_total_cost_le
  {l m r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l m)
  (R :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m r) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.absorption
          A R).cost ≤
    12 * l * m * r + 8 * l * r + 4 * l

Theorem6.37.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “factor core total cost 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/StoredTensorTrain.lean:210. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_total_cost_le
  {l r : ℕ} (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r)
  (D : ℕ) (hl : l ≤ D) (hr : r ≤ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.factorCore A).cost ≤
    164 * D ^ 3 + 108 * D ^ 2 + 25 * D + 2

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_total_cost_le
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r)
  (D : ℕ) (hl : l ≤ D) (hr : r ≤ D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.factorCore
          A).cost ≤
    164 * D ^ 3 + 108 * D ^ 2 + 25 * D + 2

Theorem6.37.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. The actual stored producer uses linear-in-length, cubic-in-bond work in the declared exact-real model, including absorption, storage, and node costs.

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

Technical source note. The actual stored producer uses linear-in-length, cubic-in-bond work in the declared exact-real model, including absorption, storage, and node costs.

Declaration kind. theorem.

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

Lean code for Theorem6.37.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_total_cost_le
  {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.canonicalize C).cost ≤
    n * (176 * D ^ 3 + 116 * D ^ 2 + 29 * D + 8) + 5 * D ^ 2 + 4 * D + 6

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_total_cost_le
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r)
  (D : ℕ)
  (bound :
    QuantumBlockEncoding.TensorTrainCanonical.maxBond
        (QuantumBlockEncoding.StoredTensorTrain.denoteChain
          C) ≤
      D) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredTensorTrain.canonicalize
          C).cost ≤
    n *
            (176 * D ^ 3 + 116 * D ^ 2 +
                29 * D +
              8) +
          5 * D ^ 2 +
        4 * D +
      6

The actual stored producer uses linear-in-length, cubic-in-bond work in
the declared exact-real model, including absorption, storage, and node costs.

Definition6.37.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “boundary”. The output's semantic boundary is obtained from its stored residual.

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 output's semantic boundary is obtained from its stored residual.

Declaration kind. def.

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

Lean code for Definition6.37.24●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.boundary {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r)
  (v : Fin l → ℝ) :
  Fin
      (QuantumBlockEncoding.StoredTensorTrain.canonicalize
            C).value.rank →
    ℝ

def QuantumBlockEncoding.StoredTensorTrain.boundary
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r)
  (v : Fin l → ℝ) :
  Fin
      (QuantumBlockEncoding.StoredTensorTrain.canonicalize
            C).value.rank →
    ℝ

The output's semantic boundary is obtained from its stored residual.

Theorem6.37.25

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.

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/StoredTensorTrain.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.37.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

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

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

Theorem6.37.26

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

Lean code for Theorem6.37.26●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

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

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

Definition6.37.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “to semantic”. Forget storage, retaining the actual concrete canonicalization data.

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. Forget storage, retaining the actual concrete canonicalization data.

Declaration kind. def.

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

Lean code for Definition6.37.27●1 definition

defdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

def QuantumBlockEncoding.StoredTensorTrain.Result.toSemantic {n l r : ℕ}
  {C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r}
  (result : QuantumBlockEncoding.StoredTensorTrain.Result C) :
  QuantumBlockEncoding.ConstructiveTensorTrain.Result
    (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)

def QuantumBlockEncoding.StoredTensorTrain.Result.toSemantic
  {n l r : ℕ}
  {C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r}
  (result :
    QuantumBlockEncoding.StoredTensorTrain.Result
      C) :
  QuantumBlockEncoding.ConstructiveTensorTrain.Result
    (QuantumBlockEncoding.StoredTensorTrain.denoteChain
      C)

Forget storage, retaining the actual concrete canonicalization data.

Theorem6.37.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “factor core r”; 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/StoredTensorTrain.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.37.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_R {l r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrain.factorCore A).value.R =
    (QuantumBlockEncoding.ConstructiveTensorTrain.factorCore
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)).R

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_R
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredTensorTrain.factorCore
            A).value.R =
    (QuantumBlockEncoding.ConstructiveTensorTrain.factorCore
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore
          A)).R

Theorem6.37.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “factor core q”; 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/StoredTensorTrain.lean:303. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.37.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_Q {l r : ℕ}
  (A : QuantumBlockEncoding.StoredTensorTrain.StoredCore l r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredTensorTrain.factorCore A).value.Q =
    (QuantumBlockEncoding.ConstructiveTensorTrain.factorCore
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore A)).Q

theorem QuantumBlockEncoding.StoredTensorTrain.factorCore_Q
  {l r : ℕ}
  (A :
    QuantumBlockEncoding.StoredTensorTrain.StoredCore
      l r) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredTensorTrain.factorCore
            A).value.Q =
    (QuantumBlockEncoding.ConstructiveTensorTrain.factorCore
        (QuantumBlockEncoding.StoredTensorTrain.denoteCore
          A)).Q

Theorem6.37.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “canonicalize refines”; the hypotheses and conclusion in the code panel fix its exact scope. Exact data refinement, not just another witness of the same contract.

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

Technical source note. Exact data refinement, not just another witness of the same contract.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredTensorTrain.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.37.30●1 theorem

theoremdefined in QuantumBlockEncoding/StoredTensorTrain.lean

complete

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_refines {n l r : ℕ}
  (C : QuantumBlockEncoding.StoredTensorTrain.StoredChain n l r) :
  (QuantumBlockEncoding.StoredTensorTrain.canonicalize
          C).value.toSemantic =
    QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain C)

theorem QuantumBlockEncoding.StoredTensorTrain.canonicalize_refines
  {n l r : ℕ}
  (C :
    QuantumBlockEncoding.StoredTensorTrain.StoredChain
      n l r) :
  (QuantumBlockEncoding.StoredTensorTrain.canonicalize
          C).value.toSemantic =
    QuantumBlockEncoding.ConstructiveTensorTrain.canonicalize
      (QuantumBlockEncoding.StoredTensorTrain.denoteChain
        C)

Exact data refinement, not just another witness of the same contract.