6.31. QuantumBlockEncoding/StoredDyadicSpans.lean🔗

17 explicit public declarations, in source order.

Definition6.31.1

uses 0used by 0✓L∃∀N

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

Why it is in this chapter. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. structure.

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

Lean code for Definition6.31.1●1 definition

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

complete

structure QuantumBlockEncoding.StoredDyadicSpans.SpanRun (α : Type) : Type

structure QuantumBlockEncoding.StoredDyadicSpans.SpanRun
  (α : Type) : Type

Fields

run : QuantumBlockEncoding.StoredGivens.Run α

integerDoublings : ℕ

Definition6.31.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “append”. Complete persistent copy, including the appended last value.

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. Complete persistent copy, including the appended last value.

Declaration kind. def.

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

Lean code for Definition6.31.2●1 definition

defdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

def QuantumBlockEncoding.StoredDyadicSpans.append {m : ℕ}
  (xs : Vector ℕ (m + 1)) (last : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℕ (m + 2))

def QuantumBlockEncoding.StoredDyadicSpans.append
  {m : ℕ} (xs : Vector ℕ (m + 1))
  (last : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℕ (m + 2))

Complete persistent copy, including the appended last value.

Theorem6.31.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.append_value {m : ℕ}
  (xs : Vector ℕ (m + 1)) (last : ℕ) (i : Fin (m + 2)) :
  (QuantumBlockEncoding.StoredDyadicSpans.append xs last).value[↑i] =
    if h : ↑i < m + 1 then xs[↑i] else last

theorem QuantumBlockEncoding.StoredDyadicSpans.append_value
  {m : ℕ} (xs : Vector ℕ (m + 1))
  (last : ℕ) (i : Fin (m + 2)) :
  (QuantumBlockEncoding.StoredDyadicSpans.append
          xs last).value[↑i] =
    if h : ↑i < m + 1 then xs[↑i]
    else last

Theorem6.31.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.append_cost {m : ℕ}
  (xs : Vector ℕ (m + 1)) (last : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.append xs last).cost op =
    (m + 2) *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.compare op +
        (3 * m + 5) *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read op +
      (2 * m + 4) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write op

theorem QuantumBlockEncoding.StoredDyadicSpans.append_cost
  {m : ℕ} (xs : Vector ℕ (m + 1))
  (last : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.append
          xs last).cost
      op =
    (m + 2) *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.compare
            op +
        (3 * m + 5) *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.read
            op +
      (2 * m + 4) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.write
          op

Definition6.31.5

uses 0used by 0✓L∃∀N

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

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/StoredDyadicSpans.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.31.5●1 definition

defdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

def QuantumBlockEncoding.StoredDyadicSpans.spans (n : ℕ) :
  QuantumBlockEncoding.StoredDyadicSpans.SpanRun (Vector ℕ (n + 1))

def QuantumBlockEncoding.StoredDyadicSpans.spans
  (n : ℕ) :
  QuantumBlockEncoding.StoredDyadicSpans.SpanRun
    (Vector ℕ (n + 1))

Theorem6.31.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_value (n : ℕ)
  (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.value[↑r] =
    2 ^ ↑r

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_value
  (n : ℕ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
            n).run.value[↑r] =
    2 ^ ↑r

Theorem6.31.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “spans vector value”; the hypotheses and conclusion in the code panel fix its exact scope. Exact table equality is a specification, not the data producer.

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

Technical source note. Exact table equality is a specification, not the data producer.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_vector_value (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.value =
    Vector.ofFn fun r => 2 ^ ↑r

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_vector_value
  (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
          n).run.value =
    Vector.ofFn fun r => 2 ^ ↑r

Exact table equality is a specification, not the data producer.

Theorem6.31.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_integerDoublings (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).integerDoublings = n

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_integerDoublings
  (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
        n).integerDoublings =
    n

Theorem6.31.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.append_total_cost {m : ℕ}
  (xs : Vector ℕ (m + 1)) (last : ℕ) :
  ∑ op,
      (QuantumBlockEncoding.StoredDyadicSpans.append xs last).cost op =
    6 * m + 11

theorem QuantumBlockEncoding.StoredDyadicSpans.append_total_cost
  {m : ℕ} (xs : Vector ℕ (m + 1))
  (last : ℕ) :
  ∑ op,
      (QuantumBlockEncoding.StoredDyadicSpans.append
            xs last).cost
        op =
    6 * m + 11

Theorem6.31.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “spans total cost”; the hypotheses and conclusion in the code panel fix its exact scope. Ordinary work is exactly quadratic; the n integer doublings are separate.

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

Technical source note. Ordinary work is exactly quadratic; the n integer doublings are separate.

Declaration kind. theorem.

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

Lean code for Theorem6.31.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_total_cost (n : ℕ) :
  ∑ op, (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.cost op =
    3 * n ^ 2 + 9 * n + 4

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_total_cost
  (n : ℕ) :
  ∑ op,
      (QuantumBlockEncoding.StoredDyadicSpans.spans
              n).run.cost
        op =
    3 * n ^ 2 + 9 * n + 4

Ordinary work is exactly quadratic; the n integer doublings are separate.

Theorem6.31.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_cost_le (n : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.cost op ≤
    3 * n ^ 2 + 9 * n + 4

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_cost_le
  (n : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
            n).run.cost
      op ≤
    3 * n ^ 2 + 9 * n + 4

Theorem6.31.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_field_cost (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    0

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_field_cost
  (n : ℕ) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
            n).run.cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    0

Theorem6.31.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “spans word bound”; the hypotheses and conclusion in the code panel fix its exact scope. All stored spans fit an unsigned word of n+1 bits.

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

Technical source note. All stored spans fit an unsigned word of n+1 bits.

Declaration kind. theorem.

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

Lean code for Theorem6.31.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_word_bound (n : ℕ)
  (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.value[↑r] ≤
      2 ^ n ∧
    (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.value[↑r] <
      2 ^ (n + 1)

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_word_bound
  (n : ℕ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.spans
              n).run.value[↑r] ≤
      2 ^ n ∧
    (QuantumBlockEncoding.StoredDyadicSpans.spans
              n).run.value[↑r] <
      2 ^ (n + 1)

All stored spans fit an unsigned word of n+1 bits.

Definition6.31.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “at stage”. This reads the existing ascending cache in chronological source order.

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. This reads the existing ascending cache in chronological source order.

Declaration kind. def.

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

Lean code for Definition6.31.14●1 definition

defdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

def QuantumBlockEncoding.StoredDyadicSpans.atStage {n : ℕ}
  (xs : Vector ℕ (n + 1)) (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℕ

def QuantumBlockEncoding.StoredDyadicSpans.atStage
  {n : ℕ} (xs : Vector ℕ (n + 1))
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℕ

This reads the existing ascending cache in chronological source order.

Theorem6.31.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.atStage_value (n : ℕ)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.atStage
        (QuantumBlockEncoding.StoredDyadicSpans.spans n).run.value
        t).value =
    2 ^ (n - ↑t)

theorem QuantumBlockEncoding.StoredDyadicSpans.atStage_value
  (n : ℕ) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredDyadicSpans.atStage
        (QuantumBlockEncoding.StoredDyadicSpans.spans
              n).run.value
        t).value =
    2 ^ (n - ↑t)

Theorem6.31.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.atStage_cost {n : ℕ}
  (xs : Vector ℕ (n + 1)) (t : Fin (n + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.atStage xs t).cost op =
    QuantumBlockEncoding.StoredGivens.tick
      QuantumBlockEncoding.StoredGivens.Op.read op

theorem QuantumBlockEncoding.StoredDyadicSpans.atStage_cost
  {n : ℕ} (xs : Vector ℕ (n + 1))
  (t : Fin (n + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredDyadicSpans.atStage
          xs t).cost
      op =
    QuantumBlockEncoding.StoredGivens.tick
      QuantumBlockEncoding.StoredGivens.Op.read
      op

Theorem6.31.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.31.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredDyadicSpans.lean

complete

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_certified (n : ℕ) :
  have result := QuantumBlockEncoding.StoredDyadicSpans.spans n;
  (∀ (r : Fin (n + 1)), result.run.value[↑r] = 2 ^ ↑r) ∧
    result.integerDoublings = n ∧
      ∑ op, result.run.cost op = 3 * n ^ 2 + 9 * n + 4 ∧
        ∀ (r : Fin (n + 1)),
          result.run.value[↑r] ≤ 2 ^ n ∧
            result.run.value[↑r] < 2 ^ (n + 1)

theorem QuantumBlockEncoding.StoredDyadicSpans.spans_certified
  (n : ℕ) :
  have result :=
    QuantumBlockEncoding.StoredDyadicSpans.spans
      n;
  (∀ (r : Fin (n + 1)),
      result.run.value[↑r] = 2 ^ ↑r) ∧
    result.integerDoublings = n ∧
      ∑ op, result.run.cost op =
          3 * n ^ 2 + 9 * n + 4 ∧
        ∀ (r : Fin (n + 1)),
          result.run.value[↑r] ≤ 2 ^ n ∧
            result.run.value[↑r] <
              2 ^ (n + 1)