6.39. QuantumBlockEncoding/StoredThinLQ.lean🔗

28 explicit public declarations, in source order.

Definition6.39.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “factors”. 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.

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

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

Lean code for Definition6.39.1●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredThinLQ.lean

complete

structure QuantumBlockEncoding.StoredThinLQ.Factors (m n k : ℕ) : Type

structure QuantumBlockEncoding.StoredThinLQ.Factors
  (m n k : ℕ) : Type

Fields

R : QuantumBlockEncoding.StoredGivens.StoredMatrix m k

Q : QuantumBlockEncoding.StoredGivens.StoredMatrix k n

Definition6.39.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “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. 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/StoredThinLQ.lean:20. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.39.2●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.entry {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i : Fin N)
  (j : Fin M) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredThinLQ.entry
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i : Fin N) (j : Fin M) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Theorem6.39.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.entry_value {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i : Fin N)
  (j : Fin M) :
  (QuantumBlockEncoding.StoredThinLQ.entry A i j).value =
    QuantumBlockEncoding.StoredGivens.denote A i j

theorem QuantumBlockEncoding.StoredThinLQ.entry_value
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i : Fin N) (j : Fin M) :
  (QuantumBlockEncoding.StoredThinLQ.entry
        A i j).value =
    QuantumBlockEncoding.StoredGivens.denote
      A i j

Theorem6.39.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.entry_cost {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i : Fin N)
  (j : Fin M) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.entry A i j).cost op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read op

theorem QuantumBlockEncoding.StoredThinLQ.entry_cost
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i : Fin N) (j : Fin M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.entry
          A i j).cost
      op =
    2 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read
        op

Definition6.39.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.39.5●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.transpose {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix n m)

def QuantumBlockEncoding.StoredThinLQ.transpose
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      n m)

Theorem6.39.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.transpose_value {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.transpose A).value =
    (QuantumBlockEncoding.StoredGivens.denote A).transpose

theorem QuantumBlockEncoding.StoredThinLQ.transpose_value
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.transpose
          A).value =
    (QuantumBlockEncoding.StoredGivens.denote
        A).transpose

Definition6.39.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “extraction 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/StoredThinLQ.lean:40. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.39.7●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.extractionBudget (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredThinLQ.extractionBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.39.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.transpose_cost {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.transpose A).cost op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget n m op

theorem QuantumBlockEncoding.StoredThinLQ.transpose_cost
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.transpose
          A).cost
      op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget
      n m op

Definition6.39.9

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.39.9●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.extractR {m n : ℕ} (h : m ≤ n)
  (C : QuantumBlockEncoding.StoredGivens.StoredMatrix n m) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix m m)

def QuantumBlockEncoding.StoredThinLQ.extractR
  {m n : ℕ} (h : m ≤ n)
  (C :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n m) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      m m)

Definition6.39.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.39.10●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.extractQ {m n : ℕ} (h : m ≤ n)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix n n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix m n)

def QuantumBlockEncoding.StoredThinLQ.extractQ
  {m n : ℕ} (h : m ≤ n)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n)

Theorem6.39.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.extractR_value {m n : ℕ} (h : m ≤ n)
  (C : QuantumBlockEncoding.StoredGivens.StoredMatrix n m) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.extractR h C).value =
    fun i j =>
    QuantumBlockEncoding.StoredGivens.denote C (Fin.castLE h j) i

theorem QuantumBlockEncoding.StoredThinLQ.extractR_value
  {m n : ℕ} (h : m ≤ n)
  (C :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n m) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.extractR
          h C).value =
    fun i j =>
    QuantumBlockEncoding.StoredGivens.denote
      C (Fin.castLE h j) i

Theorem6.39.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.extractQ_value {m n : ℕ} (h : m ≤ n)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix n n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.extractQ h E).value =
    fun i j =>
    QuantumBlockEncoding.StoredGivens.denote E (Fin.castLE h i) j

theorem QuantumBlockEncoding.StoredThinLQ.extractQ_value
  {m n : ℕ} (h : m ≤ n)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.extractQ
          h E).value =
    fun i j =>
    QuantumBlockEncoding.StoredGivens.denote
      E (Fin.castLE h i) j

Theorem6.39.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “extract r cost”; 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/StoredThinLQ.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.39.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.extractR_cost {m n : ℕ} (h : m ≤ n)
  (C : QuantumBlockEncoding.StoredGivens.StoredMatrix n m)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.extractR h C).cost op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget m m op

theorem QuantumBlockEncoding.StoredThinLQ.extractR_cost
  {m n : ℕ} (h : m ≤ n)
  (C :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n m)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.extractR
          h C).cost
      op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget
      m m op

Theorem6.39.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “extract q cost”; 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/StoredThinLQ.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.39.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.extractQ_cost {m n : ℕ} (h : m ≤ n)
  (E : QuantumBlockEncoding.StoredGivens.StoredMatrix n n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.extractQ h E).cost op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget m n op

theorem QuantumBlockEncoding.StoredThinLQ.extractQ_cost
  {m n : ℕ} (h : m ≤ n)
  (E :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      n n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.extractQ
          h E).cost
      op =
    QuantumBlockEncoding.StoredThinLQ.extractionBudget
      m n op

Definition6.39.15

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.39.15●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.wide {m n : ℕ} (h : m ≤ n)
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors m n m)

def QuantumBlockEncoding.StoredThinLQ.wide
  {m n : ℕ} (h : m ≤ n)
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors
      m n m)

Theorem6.39.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.wide_R {m n : ℕ} (h : m ≤ n)
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.wide h A).value.R =
    QuantumBlockEncoding.ConstructiveThinLQ.wideR h
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredThinLQ.wide_R
  {m n : ℕ} (h : m ≤ n)
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.wide
            h A).value.R =
    QuantumBlockEncoding.ConstructiveThinLQ.wideR
      h
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Theorem6.39.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.wide_Q {m n : ℕ} (h : m ≤ n)
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.wide h A).value.Q =
    QuantumBlockEncoding.ConstructiveThinLQ.wideQ h
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredThinLQ.wide_Q
  {m n : ℕ} (h : m ≤ n)
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.wide
            h A).value.Q =
    QuantumBlockEncoding.ConstructiveThinLQ.wideQ
      h
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Theorem6.39.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.wide_correct {m n : ℕ} (h : m ≤ n)
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote A =
      QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide h A).value.R *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide h A).value.Q ∧
    QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide h A).value.Q *
        (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredThinLQ.wide h
                  A).value.Q).transpose =
      1

theorem QuantumBlockEncoding.StoredThinLQ.wide_correct
  {m n : ℕ} (h : m ≤ n)
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
        A =
      QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide
                h A).value.R *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide
                h A).value.Q ∧
    QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.wide
                h A).value.Q *
        (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredThinLQ.wide
                  h
                  A).value.Q).transpose =
      1

Definition6.39.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “wide 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/StoredThinLQ.lean:100. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.39.19●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.wideBudget (m n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredThinLQ.wideBudget
  (m n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.39.20

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.wide_cost_le {m n : ℕ} (h : m ≤ n)
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.wide h A).cost op ≤
    QuantumBlockEncoding.StoredThinLQ.wideBudget m n op

theorem QuantumBlockEncoding.StoredThinLQ.wide_cost_le
  {m n : ℕ} (h : m ≤ n)
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.wide
          h A).cost
      op ≤
    QuantumBlockEncoding.StoredThinLQ.wideBudget
      m n op

Definition6.39.21

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.39.21●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.compileBody {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors m n (min m n))

def QuantumBlockEncoding.StoredThinLQ.compileBody
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors
      m n (min m n))

Definition6.39.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. The all-shape dispatcher additionally charges its dimension comparison.

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 all-shape dispatcher additionally charges its dimension comparison.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.compile {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors m n (min m n))

def QuantumBlockEncoding.StoredThinLQ.compile
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredThinLQ.Factors
      m n (min m n))

The all-shape dispatcher additionally charges its dimension comparison.

Theorem6.39.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.compile_R {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.compile A).value.R =
    (QuantumBlockEncoding.ConstructiveThinLQ.factor
        (QuantumBlockEncoding.StoredGivens.denote A)).R

theorem QuantumBlockEncoding.StoredThinLQ.compile_R
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.compile
            A).value.R =
    (QuantumBlockEncoding.ConstructiveThinLQ.factor
        (QuantumBlockEncoding.StoredGivens.denote
          A)).R

Theorem6.39.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.compile_Q {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.compile A).value.Q =
    (QuantumBlockEncoding.ConstructiveThinLQ.factor
        (QuantumBlockEncoding.StoredGivens.denote A)).Q

theorem QuantumBlockEncoding.StoredThinLQ.compile_Q
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredThinLQ.compile
            A).value.Q =
    (QuantumBlockEncoding.ConstructiveThinLQ.factor
        (QuantumBlockEncoding.StoredGivens.denote
          A)).Q

Theorem6.39.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.compile_correct {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredGivens.denote A =
      QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile A).value.R *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile A).value.Q ∧
    QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile A).value.Q *
        (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredThinLQ.compile
                  A).value.Q).transpose =
      1

theorem QuantumBlockEncoding.StoredThinLQ.compile_correct
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredGivens.denote
        A =
      QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile
                A).value.R *
        QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile
                A).value.Q ∧
    QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredThinLQ.compile
                A).value.Q *
        (QuantumBlockEncoding.StoredGivens.denote
            (QuantumBlockEncoding.StoredThinLQ.compile
                  A).value.Q).transpose =
      1

Definition6.39.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile 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/StoredThinLQ.lean:174. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.39.26●1 definition

defdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

def QuantumBlockEncoding.StoredThinLQ.compileBudget (m n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredThinLQ.compileBudget
  (m n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.39.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.39.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.compile_cost_le {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.compile A).cost op ≤
    QuantumBlockEncoding.StoredThinLQ.compileBudget m n op

theorem QuantumBlockEncoding.StoredThinLQ.compile_cost_le
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredThinLQ.compile
          A).cost
      op ≤
    QuantumBlockEncoding.StoredThinLQ.compileBudget
      m n op

Theorem6.39.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Uniform cubic polynomial, including transpose/extraction and dispatch.

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

Technical source note. Uniform cubic polynomial, including transpose/extraction and dispatch.

Declaration kind. theorem.

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

Lean code for Theorem6.39.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredThinLQ.lean

complete

theorem QuantumBlockEncoding.StoredThinLQ.compile_total_cost_le {m n : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix m n) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredThinLQ.compile A).cost ≤
    n * m * (22 * m + 30 * n + 41) + 5 * n * n + 6 * m * m + 8 * n +
        9 * m +
      2

theorem QuantumBlockEncoding.StoredThinLQ.compile_total_cost_le
  {m n : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      m n) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredThinLQ.compile
          A).cost ≤
    n * m * (22 * m + 30 * n + 41) +
              5 * n * n +
            6 * m * m +
          8 * n +
        9 * m +
      2

Uniform cubic polynomial, including transpose/extraction and dispatch.