6.32. QuantumBlockEncoding/StoredGivens.lean🔗

60 explicit public declarations, in source order.

Definition6.32.1

uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “op”; 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.

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

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

inductive(8 constructors)defined in QuantumBlockEncoding/StoredGivens.lean

complete

inductive QuantumBlockEncoding.StoredGivens.Op : Type

inductive QuantumBlockEncoding.StoredGivens.Op :
  Type

Constructors

field : QuantumBlockEncoding.StoredGivens.Op

sqrt : QuantumBlockEncoding.StoredGivens.Op

angle : QuantumBlockEncoding.StoredGivens.Op

trig : QuantumBlockEncoding.StoredGivens.Op

compare : QuantumBlockEncoding.StoredGivens.Op

read : QuantumBlockEncoding.StoredGivens.Op

write : QuantumBlockEncoding.StoredGivens.Op

emit : QuantumBlockEncoding.StoredGivens.Op

Definition6.32.2

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.32.2●1 definition

abbrevdefined in QuantumBlockEncoding/StoredGivens.lean

complete

abbrev QuantumBlockEncoding.StoredGivens.Cost : Type

abbrev QuantumBlockEncoding.StoredGivens.Cost :
  Type

Definition6.32.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.3●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.tick
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredGivens.tick
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredGivens.Cost

Definition6.32.4

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “run”. 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/StoredGivens.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.32.4●1 definition

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

complete

structure QuantumBlockEncoding.StoredGivens.Run (α : Type) : Type

structure QuantumBlockEncoding.StoredGivens.Run
  (α : Type) : Type

Fields

value : α

cost : QuantumBlockEncoding.StoredGivens.Cost

Definition6.32.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.5●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.Run.pure {α : Type} (x : α) :
  QuantumBlockEncoding.StoredGivens.Run α

def QuantumBlockEncoding.StoredGivens.Run.pure
  {α : Type} (x : α) :
  QuantumBlockEncoding.StoredGivens.Run α

Definition6.32.6

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.6●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.Run.bind {α β : Type}
  (x : QuantumBlockEncoding.StoredGivens.Run α)
  (f : α → QuantumBlockEncoding.StoredGivens.Run β) :
  QuantumBlockEncoding.StoredGivens.Run β

def QuantumBlockEncoding.StoredGivens.Run.bind
  {α β : Type}
  (x :
    QuantumBlockEncoding.StoredGivens.Run
      α)
  (f :
    α →
      QuantumBlockEncoding.StoredGivens.Run
        β) :
  QuantumBlockEncoding.StoredGivens.Run β

Definition6.32.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.7●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.charge {α : Type}
  (op : QuantumBlockEncoding.StoredGivens.Op) (x : α) :
  QuantumBlockEncoding.StoredGivens.Run α

def QuantumBlockEncoding.StoredGivens.charge
  {α : Type}
  (op :
    QuantumBlockEncoding.StoredGivens.Op)
  (x : α) :
  QuantumBlockEncoding.StoredGivens.Run α

Definition6.32.8

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.8●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.add (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.add
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.9

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.9●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.sub (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.sub
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.10●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.mul (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.mul
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.11

uses 0used by 0✓L∃∀N

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

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/StoredGivens.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.32.11●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.div (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.div
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.12

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.12●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.sqrt (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.sqrt
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.13

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.13●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.arccos (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.arccos
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.14

uses 0used by 0✓L∃∀N

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

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/StoredGivens.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.32.14●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.cos (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.cos
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.15

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.15●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.sin (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.sin
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition6.32.16

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.16●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.zeroTest (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run Bool

def QuantumBlockEncoding.StoredGivens.zeroTest
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    Bool

Definition6.32.17

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.17●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.signTest (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run Bool

def QuantumBlockEncoding.StoredGivens.signTest
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    Bool

Definition6.32.18

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.18●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.read {α : Type} {n : ℕ}
  (xs : Vector α n) (i : Fin n) :
  QuantumBlockEncoding.StoredGivens.Run α

def QuantumBlockEncoding.StoredGivens.read
  {α : Type} {n : ℕ} (xs : Vector α n)
  (i : Fin n) :
  QuantumBlockEncoding.StoredGivens.Run α

Definition6.32.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “collect”. Two materialized passes: write counted entries, read them for projection and summation, and write the projected output.

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. Two materialized passes: write counted entries, read them for projection and summation, and write the projected output. Counter words are metadata.

Declaration kind. def.

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

Lean code for Definition6.32.19●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.collect {α : Type} {n : ℕ}
  (f : Fin n → QuantumBlockEncoding.StoredGivens.Run α) :
  QuantumBlockEncoding.StoredGivens.Run (Vector α n)

def QuantumBlockEncoding.StoredGivens.collect
  {α : Type} {n : ℕ}
  (f :
    Fin n →
      QuantumBlockEncoding.StoredGivens.Run
        α) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector α n)

Two materialized passes: write counted entries, read them for projection
and summation, and write the projected output. Counter words are metadata.

Definition6.32.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “replace”. Persistent full-copy replacement; row references are stored words.

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. Persistent full-copy replacement; row references are stored words.

Declaration kind. def.

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

Lean code for Definition6.32.20●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.replace {α : Type} {n : ℕ}
  (xs : Vector α n) (i : Fin n) (x : α) :
  QuantumBlockEncoding.StoredGivens.Run (Vector α n)

def QuantumBlockEncoding.StoredGivens.replace
  {α : Type} {n : ℕ} (xs : Vector α n)
  (i : Fin n) (x : α) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector α n)

Persistent full-copy replacement; row references are stored words.

Definition6.32.21

uses 0used by 0✓L∃∀N

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

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

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

Lean code for Definition6.32.21●1 definition

abbrevdefined in QuantumBlockEncoding/StoredGivens.lean

complete

abbrev QuantumBlockEncoding.StoredGivens.StoredMatrix (N M : ℕ) : Type

abbrev QuantumBlockEncoding.StoredGivens.StoredMatrix
  (N M : ℕ) : Type

Definition6.32.22

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.22●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.denote {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) :
  Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.StoredGivens.denote
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M) :
  Matrix (Fin N) (Fin M) ℝ

Definition6.32.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “materialize”. Materializing an input callback is an explicit boundary: this constructor charges storage but does not certify the callback's scalar evaluation cost.

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. Materializing an input callback is an explicit boundary: this constructor charges storage but does not certify the callback's scalar evaluation cost.

Declaration kind. def.

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

Lean code for Definition6.32.23●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.materialize {N M : ℕ}
  (f : Fin N → Fin M → QuantumBlockEncoding.StoredGivens.Run ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N M)

def QuantumBlockEncoding.StoredGivens.materialize
  {N M : ℕ}
  (f :
    Fin N →
      Fin M →
        QuantumBlockEncoding.StoredGivens.Run
          ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)

Materializing an input callback is an explicit boundary: this constructor
charges storage but does not certify the callback's scalar evaluation cost.

Theorem6.32.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.collect_value {α : Type} {n : ℕ}
  (f : Fin n → QuantumBlockEncoding.StoredGivens.Run α) (i : Fin n) :
  (QuantumBlockEncoding.StoredGivens.collect f).value[↑i] = (f i).value

theorem QuantumBlockEncoding.StoredGivens.collect_value
  {α : Type} {n : ℕ}
  (f :
    Fin n →
      QuantumBlockEncoding.StoredGivens.Run
        α)
  (i : Fin n) :
  (QuantumBlockEncoding.StoredGivens.collect
          f).value[↑i] =
    (f i).value

Theorem6.32.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.collect_cost {α : Type} {n : ℕ}
  (f : Fin n → QuantumBlockEncoding.StoredGivens.Run α)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.collect f).cost op =
    ∑ i, (f i).cost op +
      n *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredGivens.collect_cost
  {α : Type} {n : ℕ}
  (f :
    Fin n →
      QuantumBlockEncoding.StoredGivens.Run
        α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.collect
          f).cost
      op =
    ∑ i, (f i).cost op +
      n *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

Definition6.32.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “angle”. Compute the norm once, then the exact signed angle once.

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. Compute the norm once, then the exact signed angle once.

Declaration kind. def.

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

Lean code for Definition6.32.26●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.angle (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredGivens.angle
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Compute the norm once, then the exact signed angle once.

Theorem6.32.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.angle_value (x y : ℝ) :
  (QuantumBlockEncoding.StoredGivens.angle x y).value =
    QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y

theorem QuantumBlockEncoding.StoredGivens.angle_value
  (x y : ℝ) :
  (QuantumBlockEncoding.StoredGivens.angle
        x y).value =
    QuantumBlockEncoding.AdjacentGivens.eliminationAngle
      x y

Definition6.32.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “coefficients”. One angle and one pair of trigonometric coefficients are shared by all entries of the two output rows.

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. One angle and one pair of trigonometric coefficients are shared by all entries of the two output rows.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.coefficients (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (ℝ × ℝ × ℝ)

def QuantumBlockEncoding.StoredGivens.coefficients
  (x y : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (ℝ × ℝ × ℝ)

One angle and one pair of trigonometric coefficients are shared by all
entries of the two output rows.

Theorem6.32.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.coefficients_value (x y : ℝ) :
  (QuantumBlockEncoding.StoredGivens.coefficients x y).value =
    (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y,
      Real.cos
        (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y / 2),
      Real.sin
        (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y / 2))

theorem QuantumBlockEncoding.StoredGivens.coefficients_value
  (x y : ℝ) :
  (QuantumBlockEncoding.StoredGivens.coefficients
        x y).value =
    (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
        x y,
      Real.cos
        (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
            x y /
          2),
      Real.sin
        (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
            x y /
          2))

Definition6.32.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “entry pair”. The six actual field operations for a pair of entries.

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 six actual field operations for a pair of entries.

Declaration kind. def.

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

Lean code for Definition6.32.30●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.entryPair (c s u v : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (ℝ × ℝ)

def QuantumBlockEncoding.StoredGivens.entryPair
  (c s u v : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (ℝ × ℝ)

The six actual field operations for a pair of entries.

Theorem6.32.31

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.31●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.entryPair_value (c s u v : ℝ) :
  (QuantumBlockEncoding.StoredGivens.entryPair c s u v).value =
    (c * u - s * v, s * u + c * v)

theorem QuantumBlockEncoding.StoredGivens.entryPair_value
  (c s u v : ℝ) :
  (QuantumBlockEncoding.StoredGivens.entryPair
        c s u v).value =
    (c * u - s * v, s * u + c * v)

Theorem6.32.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “entry pair 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/StoredGivens.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.32.32●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.entryPair_cost (c s u v : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.entryPair c s u v).cost op =
    6 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op

theorem QuantumBlockEncoding.StoredGivens.entryPair_cost
  (c s u v : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.entryPair
          c s u v).cost
      op =
    6 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op

Definition6.32.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “row pair”. Materialize both rows from a single stored vector of computed pairs.

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. Materialize both rows from a single stored vector of computed pairs.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.rowPair {M : ℕ} (u v : Vector ℝ M)
  (c s : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ M × Vector ℝ M)

def QuantumBlockEncoding.StoredGivens.rowPair
  {M : ℕ} (u v : Vector ℝ M) (c s : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ M × Vector ℝ M)

Materialize both rows from a single stored vector of computed pairs.

Theorem6.32.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.34●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.rowPair_value {M : ℕ}
  (u v : Vector ℝ M) (c s : ℝ) (j : Fin M) :
  (QuantumBlockEncoding.StoredGivens.rowPair u v c s).value.1[↑j] =
      c * u[↑j] - s * v[↑j] ∧
    (QuantumBlockEncoding.StoredGivens.rowPair u v c s).value.2[↑j] =
      s * u[↑j] + c * v[↑j]

theorem QuantumBlockEncoding.StoredGivens.rowPair_value
  {M : ℕ} (u v : Vector ℝ M) (c s : ℝ)
  (j : Fin M) :
  (QuantumBlockEncoding.StoredGivens.rowPair
              u v c s).value.1[↑j] =
      c * u[↑j] - s * v[↑j] ∧
    (QuantumBlockEncoding.StoredGivens.rowPair
              u v c s).value.2[↑j] =
      s * u[↑j] + c * v[↑j]

Definition6.32.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “rotate”. Cached input rows, materialized output rows, then two stored replacements.

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. Cached input rows, materialized output rows, then two stored replacements.

Declaration kind. def.

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

Lean code for Definition6.32.35●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.rotate {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (c s : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix N M)

def QuantumBlockEncoding.StoredGivens.rotate
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (c s : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)

Cached input rows, materialized output rows, then two stored replacements.

Theorem6.32.36

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.36●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.rotate_value {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (theta : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.rotate A i j
          (Real.cos (theta / 2)) (Real.sin (theta / 2))).value =
    QuantumBlockEncoding.AdjacentGivens.rotateRows
      (QuantumBlockEncoding.StoredGivens.denote A) i j theta

theorem QuantumBlockEncoding.StoredGivens.rotate_value
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (theta : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.rotate
          A i j (Real.cos (theta / 2))
          (Real.sin (theta / 2))).value =
    QuantumBlockEncoding.AdjacentGivens.rotateRows
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      i j theta

Definition6.32.37

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “elimination”. 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/StoredGivens.lean:188. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.32.37●1 definition

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

complete

structure QuantumBlockEncoding.StoredGivens.Elimination (N M : ℕ) : Type

structure QuantumBlockEncoding.StoredGivens.Elimination
  (N M : ℕ) : Type

Fields

matrix : QuantumBlockEncoding.StoredGivens.StoredMatrix N M

angle : ℝ

Definition6.32.38

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.32.38●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.eliminate {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (col : Fin M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.Elimination N M)

def QuantumBlockEncoding.StoredGivens.eliminate
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (col : Fin M) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredGivens.Elimination
      N M)

Theorem6.32.39

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.39●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.eliminate_angle {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (col : Fin M) :
  (QuantumBlockEncoding.StoredGivens.eliminate A i j col).value.angle =
    QuantumBlockEncoding.AdjacentGivens.eliminationAngle
      (QuantumBlockEncoding.StoredGivens.denote A i col)
      (QuantumBlockEncoding.StoredGivens.denote A j col)

theorem QuantumBlockEncoding.StoredGivens.eliminate_angle
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (col : Fin M) :
  (QuantumBlockEncoding.StoredGivens.eliminate
          A i j col).value.angle =
    QuantumBlockEncoding.AdjacentGivens.eliminationAngle
      (QuantumBlockEncoding.StoredGivens.denote
        A i col)
      (QuantumBlockEncoding.StoredGivens.denote
        A j col)

Theorem6.32.40

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.40●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.eliminate_matrix {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (col : Fin M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.eliminate A i j
            col).value.matrix =
    QuantumBlockEncoding.AdjacentGivens.eliminateEntry
      (QuantumBlockEncoding.StoredGivens.denote A) i j col

theorem QuantumBlockEncoding.StoredGivens.eliminate_matrix
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (col : Fin M) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.eliminate
            A i j col).value.matrix =
    QuantumBlockEncoding.AdjacentGivens.eliminateEntry
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      i j col

Definition6.32.41

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “sweep”. 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/StoredGivens.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.32.41●1 definition

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

complete

structure QuantumBlockEncoding.StoredGivens.Sweep (N M : ℕ) : Type

structure QuantumBlockEncoding.StoredGivens.Sweep
  (N M : ℕ) : Type

Fields

matrix : QuantumBlockEncoding.StoredGivens.StoredMatrix N M

steps : List (QuantumBlockEncoding.AdjacentGivens.Step N)

Definition6.32.42

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “column sweep”. One recursion returns both the residual and its actual chronological log.

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. One recursion returns both the residual and its actual chronological log. No separate rerun is used to generate angles or the next matrix.

Declaration kind. def.

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

Lean code for Definition6.32.42●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.columnSweep {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) :
  lo + count < N →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.Sweep N M)

def QuantumBlockEncoding.StoredGivens.columnSweep
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ) :
  lo + count < N →
    QuantumBlockEncoding.StoredGivens.Run
      (QuantumBlockEncoding.StoredGivens.Sweep
        N M)

One recursion returns both the residual and its actual chronological log.
No separate rerun is used to generate angles or the next matrix.

Theorem6.32.43

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.43●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_matrix {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
            bound).value.matrix =
    QuantumBlockEncoding.AdjacentGivens.columnSweep
      (QuantumBlockEncoding.StoredGivens.denote A) col lo count bound

theorem QuantumBlockEncoding.StoredGivens.columnSweep_matrix
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.columnSweep
            A col lo count
            bound).value.matrix =
    QuantumBlockEncoding.AdjacentGivens.columnSweep
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      col lo count bound

Theorem6.32.44

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.44●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_steps {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
          bound).value.steps =
    QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
      (QuantumBlockEncoding.StoredGivens.denote A) col lo count bound

theorem QuantumBlockEncoding.StoredGivens.columnSweep_steps
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep
          A col lo count
          bound).value.steps =
    QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
      (QuantumBlockEncoding.StoredGivens.denote
        A)
      col lo count bound

Definition6.32.45

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “angle budget”. Branch-independent upper bound; the zero pair uses fewer operations.

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. Branch-independent upper bound; the zero pair uses fewer operations.

Declaration kind. def.

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

Lean code for Definition6.32.45●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.angleBudget :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredGivens.angleBudget :
  QuantumBlockEncoding.StoredGivens.Cost

Branch-independent upper bound; the zero pair uses fewer operations.

Theorem6.32.46

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.46●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.angle_cost_le (x y : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.angle x y).cost op ≤
    QuantumBlockEncoding.StoredGivens.angleBudget op

theorem QuantumBlockEncoding.StoredGivens.angle_cost_le
  (x y : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.angle
          x y).cost
      op ≤
    QuantumBlockEncoding.StoredGivens.angleBudget
      op

Definition6.32.47

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.32.47●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.coefficientBudget :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredGivens.coefficientBudget :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.32.48

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.48●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.coefficients_cost_le (x y : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.coefficients x y).cost op ≤
    QuantumBlockEncoding.StoredGivens.coefficientBudget op

theorem QuantumBlockEncoding.StoredGivens.coefficients_cost_le
  (x y : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.coefficients
          x y).cost
      op ≤
    QuantumBlockEncoding.StoredGivens.coefficientBudget
      op

Theorem6.32.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “row pair 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/StoredGivens.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.32.49●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.rowPair_cost {M : ℕ}
  (u v : Vector ℝ M) (c s : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.rowPair u v c s).cost op =
    M *
      (6 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field op +
          10 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        6 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredGivens.rowPair_cost
  {M : ℕ} (u v : Vector ℝ M) (c s : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.rowPair
          u v c s).cost
      op =
    M *
      (6 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.field
              op +
          10 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        6 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)

Theorem6.32.50

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.50●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.rotate_cost {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (c s : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.rotate A i j c s).cost op =
    M *
          (6 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.field op +
              10 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.read op +
            6 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.write op) +
        2 * N *
          (QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op) +
      2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read op

theorem QuantumBlockEncoding.StoredGivens.rotate_cost
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (c s : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.rotate
          A i j c s).cost
      op =
    M *
          (6 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.field
                  op +
              10 *
                QuantumBlockEncoding.StoredGivens.tick
                  QuantumBlockEncoding.StoredGivens.Op.read
                  op +
            6 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.write
                op) +
        2 * N *
          (QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op) +
      2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read
          op

Definition6.32.51

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.32.51●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.eliminationBudget (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredGivens.eliminationBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.32.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate 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/StoredGivens.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.32.52●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.eliminate_cost_le {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (i j : Fin N)
  (col : Fin M) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.eliminate A i j col).cost op ≤
    QuantumBlockEncoding.StoredGivens.eliminationBudget N M op

theorem QuantumBlockEncoding.StoredGivens.eliminate_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (i j : Fin N) (col : Fin M)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.eliminate
          A i j col).cost
      op ≤
    QuantumBlockEncoding.StoredGivens.eliminationBudget
      N M op

Definition6.32.53

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.32.53●1 definition

defdefined in QuantumBlockEncoding/StoredGivens.lean

complete

def QuantumBlockEncoding.StoredGivens.stepBudget (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredGivens.stepBudget
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem6.32.54

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.54●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_cost_succ {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + (count + 1) < N)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.columnSweep A col lo (count + 1)
          bound).cost
      op =
    (QuantumBlockEncoding.StoredGivens.eliminate A ⟨lo + count, ⋯⟩
              ⟨lo + count + 1, bound⟩ col).cost
          op +
        (QuantumBlockEncoding.StoredGivens.columnSweep
              (QuantumBlockEncoding.StoredGivens.eliminate A
                    ⟨lo + count, ⋯⟩ ⟨lo + count + 1, bound⟩
                    col).value.matrix
              col lo count ⋯).cost
          op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.emit op

theorem QuantumBlockEncoding.StoredGivens.columnSweep_cost_succ
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + (count + 1) < N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.columnSweep
          A col lo (count + 1) bound).cost
      op =
    (QuantumBlockEncoding.StoredGivens.eliminate
              A ⟨lo + count, ⋯⟩
              ⟨lo + count + 1, bound⟩
              col).cost
          op +
        (QuantumBlockEncoding.StoredGivens.columnSweep
              (QuantumBlockEncoding.StoredGivens.eliminate
                    A ⟨lo + count, ⋯⟩
                    ⟨lo + count + 1,
                      bound⟩
                    col).value.matrix
              col lo count ⋯).cost
          op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.emit
        op

Theorem6.32.55

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Symbolic bound on the actual fused producer, not on just its log length.

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

Technical source note. Symbolic bound on the actual fused producer, not on just its log length.

Declaration kind. theorem.

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

Lean code for Theorem6.32.55●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_cost_le {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
          bound).cost
      op ≤
    count * QuantumBlockEncoding.StoredGivens.stepBudget N M op

theorem QuantumBlockEncoding.StoredGivens.columnSweep_cost_le
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.columnSweep
          A col lo count bound).cost
      op ≤
    count *
      QuantumBlockEncoding.StoredGivens.stepBudget
        N M op

Symbolic bound on the actual fused producer, not on just its log length.

Theorem6.32.56

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.56●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.stepBudget_fields (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.stepBudget N M
        QuantumBlockEncoding.StoredGivens.Op.field =
      6 * M + 8 ∧
    QuantumBlockEncoding.StoredGivens.stepBudget N M
          QuantumBlockEncoding.StoredGivens.Op.sqrt =
        1 ∧
      QuantumBlockEncoding.StoredGivens.stepBudget N M
            QuantumBlockEncoding.StoredGivens.Op.angle =
          1 ∧
        QuantumBlockEncoding.StoredGivens.stepBudget N M
              QuantumBlockEncoding.StoredGivens.Op.trig =
            2 ∧
          QuantumBlockEncoding.StoredGivens.stepBudget N M
                QuantumBlockEncoding.StoredGivens.Op.compare =
              2 ∧
            QuantumBlockEncoding.StoredGivens.stepBudget N M
                  QuantumBlockEncoding.StoredGivens.Op.read =
                10 * M + 2 * N + 6 ∧
              QuantumBlockEncoding.StoredGivens.stepBudget N M
                    QuantumBlockEncoding.StoredGivens.Op.write =
                  6 * M + 2 * N ∧
                QuantumBlockEncoding.StoredGivens.stepBudget N M
                    QuantumBlockEncoding.StoredGivens.Op.emit =
                  1

theorem QuantumBlockEncoding.StoredGivens.stepBudget_fields
  (N M : ℕ) :
  QuantumBlockEncoding.StoredGivens.stepBudget
        N M
        QuantumBlockEncoding.StoredGivens.Op.field =
      6 * M + 8 ∧
    QuantumBlockEncoding.StoredGivens.stepBudget
          N M
          QuantumBlockEncoding.StoredGivens.Op.sqrt =
        1 ∧
      QuantumBlockEncoding.StoredGivens.stepBudget
            N M
            QuantumBlockEncoding.StoredGivens.Op.angle =
          1 ∧
        QuantumBlockEncoding.StoredGivens.stepBudget
              N M
              QuantumBlockEncoding.StoredGivens.Op.trig =
            2 ∧
          QuantumBlockEncoding.StoredGivens.stepBudget
                N M
                QuantumBlockEncoding.StoredGivens.Op.compare =
              2 ∧
            QuantumBlockEncoding.StoredGivens.stepBudget
                  N M
                  QuantumBlockEncoding.StoredGivens.Op.read =
                10 * M + 2 * N + 6 ∧
              QuantumBlockEncoding.StoredGivens.stepBudget
                    N M
                    QuantumBlockEncoding.StoredGivens.Op.write =
                  6 * M + 2 * N ∧
                QuantumBlockEncoding.StoredGivens.stepBudget
                    N M
                    QuantumBlockEncoding.StoredGivens.Op.emit =
                  1

Theorem6.32.57

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep emit”; the hypotheses and conclusion in the code panel fix its exact scope. Each iteration emits exactly one record, including a harmless zero-pair rotation.

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

Technical source note. Each iteration emits exactly one record, including a harmless zero-pair rotation. This is a counter theorem for the producer in addition to its independent list-length refinement.

Declaration kind. theorem.

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

Lean code for Theorem6.32.57●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_emit {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
          bound).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    count

theorem QuantumBlockEncoding.StoredGivens.columnSweep_emit
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep
          A col lo count bound).cost
      QuantumBlockEncoding.StoredGivens.Op.emit =
    count

Each iteration emits exactly one record, including a harmless zero-pair
rotation. This is a counter theorem for the producer in addition to its
independent list-length refinement.

Theorem6.32.58

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.32.58●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_steps_length {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
            bound).value.steps.length =
    count

theorem QuantumBlockEncoding.StoredGivens.columnSweep_steps_length
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.StoredGivens.columnSweep
            A col lo count
            bound).value.steps.length =
    count

Theorem6.32.59

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep action”; the hypotheses and conclusion in the code panel fix its exact scope. The emitted list and materialized residual are a single coherent run.

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

Technical source note. The emitted list and materialized residual are a single coherent run.

Declaration kind. theorem.

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

Lean code for Theorem6.32.59●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.columnSweep_action {N M : ℕ}
  (A : QuantumBlockEncoding.StoredGivens.StoredMatrix N M) (col : Fin M)
  (lo count : ℕ) (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
            bound).value.steps
      (QuantumBlockEncoding.StoredGivens.denote A) =
    QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.columnSweep A col lo count
            bound).value.matrix

theorem QuantumBlockEncoding.StoredGivens.columnSweep_action
  {N M : ℕ}
  (A :
    QuantumBlockEncoding.StoredGivens.StoredMatrix
      N M)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.StoredGivens.columnSweep
            A col lo count
            bound).value.steps
      (QuantumBlockEncoding.StoredGivens.denote
        A) =
    QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredGivens.columnSweep
            A col lo count
            bound).value.matrix

The emitted list and materialized residual are a single coherent run.

Theorem6.32.60

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “materialize cost”; the hypotheses and conclusion in the code panel fix its exact scope. Input generation is charged once per materialized entry, and the specified callback must itself use the counted scalar interface.

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

Technical source note. Input generation is charged once per materialized entry, and the specified callback must itself use the counted scalar interface.

Declaration kind. theorem.

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

Lean code for Theorem6.32.60●1 theorem

theoremdefined in QuantumBlockEncoding/StoredGivens.lean

complete

theorem QuantumBlockEncoding.StoredGivens.materialize_cost {N M : ℕ}
  (f : Fin N → Fin M → QuantumBlockEncoding.StoredGivens.Run ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.materialize f).cost op =
    ∑ i, ∑ j, (f i j).cost op +
      (N * M + N) *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredGivens.materialize_cost
  {N M : ℕ}
  (f :
    Fin N →
      Fin M →
        QuantumBlockEncoding.StoredGivens.Run
          ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredGivens.materialize
          f).cost
      op =
    ∑ i, ∑ j, (f i j).cost op +
      (N * M + N) *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

Input generation is charged once per materialized entry, and the
specified callback must itself use the counted scalar interface.