6.35. QuantumBlockEncoding/StoredRectangularGivens.lean🔗

30 explicit public declarations, in source order.

Definition6.35.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “append”. Copy the left list spine, sharing the right list.

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. Copy the left list spine, sharing the right list. Cost-counter traversal is bookkeeping; the data append's reads and writes are charged here.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.append {α : Type}
  (xs ys : List α) : QuantumBlockEncoding.StoredGivens.Run (List α)

def QuantumBlockEncoding.StoredRectangularGivens.append
  {α : Type} (xs ys : List α) :
  QuantumBlockEncoding.StoredGivens.Run
    (List α)

Copy the left list spine, sharing the right list. Cost-counter traversal
is bookkeeping; the data append's reads and writes are charged here.

Definition6.35.2

uses 0used by 0✓L∃∀N

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

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/StoredRectangularGivens.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.35.2●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.sweep {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (k remaining : ℕ) :
  k + remaining ≤ M →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.Sweep N M)

def QuantumBlockEncoding.StoredRectangularGivens.sweep
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (k remaining : ℕ) :
  k + remaining ≤ M →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.Sweep
        N M)

Theorem6.35.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_matrix {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (k remaining : ℕ) (columns : k + remaining ≤ M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.sweep A k remaining
            columns).value.matrix =
    QuantumBlockEncoding.RectangularGivens.sweep
      (QuantumBlockEncoding.StoredGivens.denote A) k remaining columns

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_matrix
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.sweep
            A k remaining
            columns).value.matrix =
    QuantumBlockEncoding.RectangularGivens.sweep
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      k remaining columns

Theorem6.35.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_steps {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (k remaining : ℕ) (columns : k + remaining ≤ M) :
  (QuantumBlockEncoding.StoredRectangularGivens.sweep A k remaining
          columns).value.steps =
    QuantumBlockEncoding.RectangularGivens.sweepSteps
      (QuantumBlockEncoding.StoredGivens.denote A) k remaining columns

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_steps
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M) :
  (QuantumBlockEncoding.StoredRectangularGivens.sweep
          A k remaining
          columns).value.steps =
    QuantumBlockEncoding.RectangularGivens.sweepSteps
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      k remaining columns

Definition6.35.5

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.35.5●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.columnBudget (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredRectangularGivens.columnBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.35.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_cost_le {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (k remaining : ℕ) (columns : k + remaining ≤ M)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.sweep A k remaining
          columns).cost
      op ≤
    remaining *
      QuantumBlockEncoding.StoredRectangularGivens.columnBudget N M op

theorem QuantumBlockEncoding.StoredRectangularGivens.sweep_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (k remaining : ℕ)
  (columns : k + remaining ≤ M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.sweep
          A k remaining columns).cost
      op ≤
    remaining *
      QuantumBlockEncoding.StoredRectangularGivens.columnBudget
        N M op

Definition6.35.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “identity”. Materialized identity, including its finite-index equality decisions.

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. Materialized identity, including its finite-index equality decisions.

Declaration kind. def.

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

Lean code for Definition6.35.7●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.identity (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N N)

def QuantumBlockEncoding.StoredRectangularGivens.identity
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N N)

Materialized identity, including its finite-index equality decisions.

Theorem6.35.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.identity_value (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.identity N).value =
    1

theorem QuantumBlockEncoding.StoredRectangularGivens.identity_value
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.identity
          N).value =
    1

Definition6.35.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “identity 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/StoredRectangularGivens.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.35.9●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.identityBudget (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredRectangularGivens.identityBudget
  (N : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.35.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “identity 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/StoredRectangularGivens.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.35.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.identity_cost (N : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.identity N).cost op =
    QuantumBlockEncoding.StoredRectangularGivens.identityBudget N op

theorem QuantumBlockEncoding.StoredRectangularGivens.identity_cost
  (N : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.identity
          N).cost
      op =
    QuantumBlockEncoding.StoredRectangularGivens.identityBudget
      N op

Definition6.35.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “replay”. Replay uses only a pair of stored row updates.

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. Replay uses only a pair of stored row updates. Reading the end marker is charged in the empty case; each cons record is charged in the nonempty case.

Declaration kind. def.

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

Lean code for Definition6.35.11●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.replay {N M : ℕ} :
  List (QuantumBlockEncoding.AdjacentGivens.Step N) →
    QuantumBlockEncoding.StoredGivens.StoredMatrix N M →
      QuantumBlockEncoding.StoredGivens.Run
        (QuantumBlockEncoding.StoredGivens.StoredMatrix N M)

def QuantumBlockEncoding.StoredRectangularGivens.replay
  {N M : ℕ} :
  List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N) →
    QuantumBlockEncoding.StoredGivens.StoredMatrix
        N M →
      QuantumBlockEncoding.StoredGivens.Run
        (QuantumBlockEncoding.StoredGivens.StoredMatrix
          N M)

Replay uses only a pair of stored row updates. Reading the end marker is
charged in the empty case; each cons record is charged in the nonempty case.

Theorem6.35.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.replay_value {N M : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N))
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.replay steps
          A).value =
    QuantumBlockEncoding.AdjacentGivens.applySteps steps
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredRectangularGivens.replay_value
  {N M : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N))
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.replay
          steps A).value =
    QuantumBlockEncoding.AdjacentGivens.applySteps
      steps
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Definition6.35.13

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.35.13●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.replayStepBudget
  (N M : ℕ) : QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredRectangularGivens.replayStepBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.35.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.replay_cost {N M : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N))
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.replay steps A).cost
      op =
    steps.length *
        QuantumBlockEncoding.StoredRectangularGivens.replayStepBudget N
          M op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read op

theorem QuantumBlockEncoding.StoredRectangularGivens.replay_cost
  {N M : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N))
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.replay
          steps A).cost
      op =
    steps.length *
        QuantumBlockEncoding.StoredRectangularGivens.replayStepBudget
          N M op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read
        op

Definition6.35.15

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

Lean code for Definition6.35.15●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

structure QuantumBlockEncoding.StoredRectangularGivens.Result (N M : ℕ) : Type

structure QuantumBlockEncoding.StoredRectangularGivens.Result
  (N M : ℕ) : Type

Fields

reduced : QuantumBlockEncoding.StoredGivens.StoredMatrix N M

transform : QuantumBlockEncoding.StoredGivens.StoredMatrix N N

steps : List (QuantumBlockEncoding.AdjacentGivens.Step N)

Definition6.35.16

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.35.16●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.compile {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredRectangularGivens.Result N M)

def QuantumBlockEncoding.StoredRectangularGivens.compile
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredRectangularGivens.Result
      N M)

Theorem6.35.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_reduced {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.reduced =
    QuantumBlockEncoding.RectangularGivens.reduced
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_reduced
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.reduced =
    QuantumBlockEncoding.RectangularGivens.reduced
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Theorem6.35.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_steps {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile A).value.steps =
    QuantumBlockEncoding.RectangularGivens.decompose
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_steps
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile
          A).value.steps =
    QuantumBlockEncoding.RectangularGivens.decompose
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Theorem6.35.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.transform =
    QuantumBlockEncoding.RectangularGivens.transform
      (QuantumBlockEncoding.StoredGivens.denote A)

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.transform =
    QuantumBlockEncoding.RectangularGivens.transform
      (QuantumBlockEncoding.StoredGivens.denote
        A)

Definition6.35.20

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

Lean code for Definition6.35.20●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.compileBudget (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredRectangularGivens.compileBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.35.21

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. A componentwise polynomial operation bound for residual, log, and the fully stored accumulated transform produced by this actual algorithm.

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

Technical source note. A componentwise polynomial operation bound for residual, log, and the fully stored accumulated transform produced by this actual algorithm.

Declaration kind. theorem.

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

Lean code for Theorem6.35.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_cost_le {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile A).cost op ≤
    QuantumBlockEncoding.StoredRectangularGivens.compileBudget N M op

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile
          A).cost
      op ≤
    QuantumBlockEncoding.StoredRectangularGivens.compileBudget
      N M op

A componentwise polynomial operation bound for residual, log, and the
fully stored accumulated transform produced by this actual algorithm.

Theorem6.35.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile exact recovery”; 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/StoredRectangularGivens.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.35.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_exact_recovery
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  (QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredRectangularGivens.compile
                A).value.transform).transpose *
      QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.reduced =
    QuantumBlockEncoding.StoredGivens.denote A

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_exact_recovery
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  (QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredRectangularGivens.compile
                A).value.transform).transpose *
      QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.reduced =
    QuantumBlockEncoding.StoredGivens.denote
      A

Theorem6.35.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform_orthogonal
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  (QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredRectangularGivens.compile
                A).value.transform).transpose *
      QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.transform =
    1

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform_orthogonal
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  (QuantumBlockEncoding.StoredGivens.denote
          (QuantumBlockEncoding.StoredRectangularGivens.compile
                A).value.transform).transpose *
      QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.transform =
    1

Theorem6.35.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform_det
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  (QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.transform).det =
    1

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_transform_det
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  (QuantumBlockEncoding.StoredGivens.denote
        (QuantumBlockEncoding.StoredRectangularGivens.compile
              A).value.transform).det =
    1

Theorem6.35.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_zero_below
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (row : Fin N) (col : Fin M) (below : ↑col < ↑row) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.reduced
      row col =
    0

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_zero_below
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (row : Fin N) (col : Fin M)
  (below : ↑col < ↑row) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredRectangularGivens.compile
            A).value.reduced
      row col =
    0

Definition6.35.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “polynomial budget”. Expanded polynomial form of every operation category.

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. Expanded polynomial form of every operation category.

Declaration kind. def.

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

Lean code for Definition6.35.26●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget
  (N M : ℕ) : QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Expanded polynomial form of every operation category.

Theorem6.35.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compileBudget_eq
  (N M : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.compileBudget N M =
    QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget N M

theorem QuantumBlockEncoding.StoredRectangularGivens.compileBudget_eq
  (N M : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.compileBudget
      N M =
    QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget
      N M

Theorem6.35.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.35.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_polynomial_cost_le
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile A).cost op ≤
    QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget N M op

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_polynomial_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredRectangularGivens.compile
          A).cost
      op ≤
    QuantumBlockEncoding.StoredRectangularGivens.polynomialBudget
      N M op

Definition6.35.29

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “total”. Sum of the eight explicitly separated operation counters.

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. Sum of the eight explicitly separated operation counters.

Declaration kind. def.

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

Lean code for Definition6.35.29●1 definition

defdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

def QuantumBlockEncoding.StoredRectangularGivens.total
  (cost : QuantumBlockEncoding.StoredGivens.Cost) : ℕ

def QuantumBlockEncoding.StoredRectangularGivens.total
  (cost :
    QuantumBlockEncoding.StoredGivens.Cost) :
  ℕ

Sum of the eight explicitly separated operation counters.

Theorem6.35.30

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.

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

Lean code for Theorem6.35.30●1 theorem

theoremdefined in QuantumBlockEncoding/StoredRectangularGivens.lean

complete

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_total_cost_le
  {N M : ℕ} (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredRectangularGivens.compile A).cost ≤
    N * M * (22 * M + 30 * N + 29) + 5 * N * N + 4 * N + M + 1

theorem QuantumBlockEncoding.StoredRectangularGivens.compile_total_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredRectangularGivens.compile
          A).cost ≤
    N * M * (22 * M + 30 * N + 29) +
            5 * N * N +
          4 * N +
        M +
      1