6.30. QuantumBlockEncoding/StoredBinaryCoordinates.lean🔗

27 explicit public declarations, in source order.

Definition6.30.1

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.30.1●1 definition

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

complete

structure QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun (α : Type) :
  Type

structure QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
  (α : Type) : Type

Fields

run : QuantumBlockEncoding.StoredGivens.Run α

quotientCalls : ℕ

remainderCalls : ℕ

Definition6.30.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “binary real”. Read exactly 'width' low binary digits using quotient/remainder, then Horner arithmetic.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Technical source note. Read exactly 'width' low binary digits using quotient/remainder, then Horner arithmetic. The legal-input theorem requires the integer to fit.

Declaration kind. def.

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

Lean code for Definition6.30.2●1 definition

defdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

def QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal (width j : ℕ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun ℝ

def QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal
  (width j : ℕ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    ℝ

Read exactly `width` low binary digits using quotient/remainder, then
Horner arithmetic. The legal-input theorem requires the integer to fit.

Theorem6.30.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_value
  (width j : ℕ) (h : j < 2 ^ width) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal width
          j).run.value =
    ↑j

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_value
  (width j : ℕ) (h : j < 2 ^ width) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal
          width j).run.value =
    ↑j

Theorem6.30.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_cost
  (width j : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal width
            j).run.cost
      op =
    2 * width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_cost
  (width j : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal
            width j).run.cost
      op =
    2 * width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op

Theorem6.30.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_quotients
  (width j : ℕ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal width
        j).quotientCalls =
    width

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_quotients
  (width j : ℕ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal
        width j).quotientCalls =
    width

Theorem6.30.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_remainders
  (width j : ℕ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal width
        j).remainderCalls =
    width

theorem QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal_remainders
  (width j : ℕ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.binaryReal
        width j).remainderCalls =
    width

Definition6.30.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “coordinate”. Coordinate supplier from explicit real origin/step and a binary index.

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. Coordinate supplier from explicit real origin/step and a binary index. Origin and step are supplied values; their production is not charged here.

Declaration kind. def.

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

Lean code for Definition6.30.7●1 definition

defdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

def QuantumBlockEncoding.StoredBinaryCoordinates.coordinate (width j : ℕ)
  (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun ℝ

def QuantumBlockEncoding.StoredBinaryCoordinates.coordinate
  (width j : ℕ) (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    ℝ

Coordinate supplier from explicit real origin/step and a binary index.
Origin and step are supplied values; their production is not charged here.

Theorem6.30.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_value
  (width j : ℕ) (origin step : ℝ) (h : j < 2 ^ width) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate width j
          origin step).run.value =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
      step j

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_value
  (width j : ℕ) (origin step : ℝ)
  (h : j < 2 ^ width) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate
          width j origin step).run.value =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
      origin step j

Theorem6.30.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_cost
  (width j : ℕ) (origin step : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate width j
            origin step).run.cost
      op =
    (2 * width + 2) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_cost
  (width j : ℕ) (origin step : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate
            width j origin step).run.cost
      op =
    (2 * width + 2) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      width *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op

Theorem6.30.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “coordinate quotients”; 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/StoredBinaryCoordinates.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.30.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_quotients
  (width j : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate width j
        origin step).quotientCalls =
    width

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_quotients
  (width j : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate
        width j origin
        step).quotientCalls =
    width

Theorem6.30.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_remainders
  (width j : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate width j
        origin step).remainderCalls =
    width

theorem QuantumBlockEncoding.StoredBinaryCoordinates.coordinate_remainders
  (width j : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.coordinate
        width j origin
        step).remainderCalls =
    width

Definition6.30.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “collect indexed”. One materialized indexed pass, followed by value projection.

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 materialized indexed pass, followed by value projection. Scalar and index-call counters read stored results; callbacks are not rerun.

Declaration kind. def.

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

Lean code for Definition6.30.12●1 definition

defdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

def QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed {α : Type}
  {m : ℕ}
  (f :
    Fin m → QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun α) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun (Vector α m)

def QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
        α) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    (Vector α m)

One materialized indexed pass, followed by value projection. Scalar and
index-call counters read stored results; callbacks are not rerun.

Theorem6.30.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “collect indexed 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/StoredBinaryCoordinates.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.30.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed_value
  {α : Type} {m : ℕ}
  (f :
    Fin m → QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun α)
  (i : Fin m) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed
            f).run.value[↑i] =
    (f i).run.value

theorem QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed_value
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
        α)
  (i : Fin m) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed
            f).run.value[↑i] =
    (f i).run.value

Theorem6.30.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed_cost
  {α : Type} {m : ℕ}
  (f :
    Fin m → QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun α)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed
            f).run.cost
      op =
    ∑ i, (f i).run.cost op +
      m *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed_cost
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
        α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.collectIndexed
            f).run.cost
      op =
    ∑ i, (f i).run.cost op +
      m *
        (2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

Definition6.30.15

uses 0used by 0✓L∃∀N

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

Lean code for Definition6.30.15●1 definition

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

complete

structure QuantumBlockEncoding.StoredBinaryCoordinates.Point : Type

structure QuantumBlockEncoding.StoredBinaryCoordinates.Point :
  Type

Fields

first : ℕ

lower : ℝ

Definition6.30.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “parent”. The schedule uses one separately counted integer quotient.

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 schedule uses one separately counted integer quotient. Powers and integer address multiplication remain outside the two selected index counters. The real coordinate itself is built by charged binary arithmetic.

Declaration kind. def.

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

Lean code for Definition6.30.16●1 definition

defdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

def QuantumBlockEncoding.StoredBinaryCoordinates.parent (n cut r : ℕ)
  (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    QuantumBlockEncoding.StoredBinaryCoordinates.Point

def QuantumBlockEncoding.StoredBinaryCoordinates.parent
  (n cut r : ℕ) (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    QuantumBlockEncoding.StoredBinaryCoordinates.Point

The schedule uses one separately counted integer quotient. Powers and
integer address multiplication remain outside the two selected index counters.
The real coordinate itself is built by charged binary arithmetic.

Theorem6.30.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “parent first”; 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/StoredBinaryCoordinates.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.30.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_first (n cut r : ℕ)
  (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent n cut r origin
            step).run.value.first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule cut
      (r + 1)

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_first
  (n cut r : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent
            n cut r origin
            step).run.value.first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      cut (r + 1)

Theorem6.30.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_lower (n cut r : ℕ)
  (origin step : ℝ) (hc : cut ≤ 2 ^ n) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent n cut r origin
            step).run.value.lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
      step
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (r + 1))

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_lower
  (n cut r : ℕ) (origin step : ℝ)
  (hc : cut ≤ 2 ^ n) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent
            n cut r origin
            step).run.value.lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
      origin step
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (r + 1))

Theorem6.30.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_cost (n cut r : ℕ)
  (origin step : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent n cut r origin
            step).run.cost
      op =
    (2 * n + 4) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      (n + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_cost
  (n cut r : ℕ) (origin step : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent
            n cut r origin step).run.cost
      op =
    (2 * n + 4) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      (n + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op

Theorem6.30.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “parent quotients”; 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/StoredBinaryCoordinates.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.30.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_quotients
  (n cut r : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent n cut r origin
        step).quotientCalls =
    n + 2

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_quotients
  (n cut r : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent
        n cut r origin
        step).quotientCalls =
    n + 2

Theorem6.30.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_remainders
  (n cut r : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent n cut r origin
        step).remainderCalls =
    n + 1

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parent_remainders
  (n cut r : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parent
        n cut r origin
        step).remainderCalls =
    n + 1

Definition6.30.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “parents”. Chronological parent rows: index 't' corresponds to residual width 'n-t'.

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. Chronological parent rows: index 't' corresponds to residual width 'n-t'. Only 'n+1' coordinates are stored, not a grid-sized coordinate table.

Declaration kind. def.

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

Lean code for Definition6.30.22●1 definition

defdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

def QuantumBlockEncoding.StoredBinaryCoordinates.parents (n cut : ℕ)
  (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    (Vector QuantumBlockEncoding.StoredBinaryCoordinates.Point (n + 1))

def QuantumBlockEncoding.StoredBinaryCoordinates.parents
  (n cut : ℕ) (origin step : ℝ) :
  QuantumBlockEncoding.StoredBinaryCoordinates.IndexedRun
    (Vector
      QuantumBlockEncoding.StoredBinaryCoordinates.Point
      (n + 1))

Chronological parent rows: index `t` corresponds to residual width `n-t`.
Only `n+1` coordinates are stored, not a grid-sized coordinate table.

Theorem6.30.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_first (n cut : ℕ)
  (origin step : ℝ) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents n cut origin
              step).run.value[↑t].first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule cut
      (n - ↑t + 1)

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_first
  (n cut : ℕ) (origin step : ℝ)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents
              n cut origin
              step).run.value[↑t].first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      cut (n - ↑t + 1)

Theorem6.30.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_lower (n cut : ℕ)
  (origin step : ℝ) (hc : cut ≤ 2 ^ n) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents n cut origin
              step).run.value[↑t].lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
      step
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (n - ↑t + 1))

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_lower
  (n cut : ℕ) (origin step : ℝ)
  (hc : cut ≤ 2 ^ n) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents
              n cut origin
              step).run.value[↑t].lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
      origin step
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        cut (n - ↑t + 1))

Theorem6.30.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_cost (n cut : ℕ)
  (origin step : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents n cut origin
            step).run.cost
      op =
    (n + 1) *
      ((2 * n + 4) *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.field op +
            (n + 1) *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_cost
  (n cut : ℕ) (origin step : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents
            n cut origin step).run.cost
      op =
    (n + 1) *
      ((2 * n + 4) *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.field
                op +
            (n + 1) *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare
                op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)

Theorem6.30.26

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.26●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_quotients
  (n cut : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents n cut origin
        step).quotientCalls =
    (n + 1) * (n + 2)

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_quotients
  (n cut : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents
        n cut origin step).quotientCalls =
    (n + 1) * (n + 2)

Theorem6.30.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.30.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBinaryCoordinates.lean

complete

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_remainders
  (n cut : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents n cut origin
        step).remainderCalls =
    (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredBinaryCoordinates.parents_remainders
  (n cut : ℕ) (origin step : ℝ) :
  (QuantumBlockEncoding.StoredBinaryCoordinates.parents
        n cut origin
        step).remainderCalls =
    (n + 1) ^ 2