10.6. QuantumBlockEncoding/HermiteBinaryCutoff.lean🔗

9 explicit public declarations, in source order.

Definition10.6.1

uses 0used by 0✓L∃∀N

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

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. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Definition10.6.1●1 definition

defdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

def QuantumBlockEncoding.HermiteBinaryCutoff.below (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run Bool

def QuantumBlockEncoding.HermiteBinaryCutoff.below
  (x : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    Bool

Definition10.6.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “search”. Search an interval with '2^remaining' grid cells.

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. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Search an interval with '2^remaining' grid cells. 'lower' is its first grid point and 'span' its full real width. No grid-sized table is built.

Declaration kind. def.

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

Lean code for Definition10.6.2●1 definition

defdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

def QuantumBlockEncoding.HermiteBinaryCutoff.search (remaining start : ℕ)
  (lower span : ℝ) : QuantumBlockEncoding.StoredGivens.Run ℕ

def QuantumBlockEncoding.HermiteBinaryCutoff.search
  (remaining start : ℕ) (lower span : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℕ

Search an interval with `2^remaining` grid cells. `lower` is its first
grid point and `span` its full real width. No grid-sized table is built.

Theorem10.6.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “search 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.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Theorem10.6.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.search_cost
  (remaining start : ℕ) (lower span : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.search remaining start lower
          span).cost
      op =
    2 * remaining *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      (remaining + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.HermiteBinaryCutoff.search_cost
  (remaining start : ℕ) (lower span : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.search
          remaining start lower span).cost
      op =
    2 * remaining *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      (remaining + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op

Theorem10.6.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “search value”; the hypotheses and conclusion in the code panel fix its exact scope. A full interval invariant proves the actual returned index, including the cutoff at either endpoint and the one-cell case.

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

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. A full interval invariant proves the actual returned index, including the cutoff at either endpoint and the one-cell case.

Declaration kind. theorem.

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

Lean code for Theorem10.6.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.search_value
  (n remaining start : ℕ) (L : ℝ) (hL : 0 < L)
  (hlo :
    start ≤ QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
  (hhi :
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ≤
      start + 2 ^ remaining) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.search remaining start
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
          start)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
          2 ^ remaining)).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L

theorem QuantumBlockEncoding.HermiteBinaryCutoff.search_value
  (n remaining start : ℕ) (L : ℝ)
  (hL : 0 < L)
  (hlo :
    start ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L)
  (hhi :
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L ≤
      start + 2 ^ remaining) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.search
        remaining start
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L start)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
            n L *
          2 ^ remaining)).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
      n L

A full interval invariant proves the actual returned index, including
the cutoff at either endpoint and the one-cell case.

Definition10.6.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compute”. Source-level producer: one multiplication and negation initialize the interval from '-pi*L' to zero, then binary search finds its cutoff.

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. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Source-level producer: one multiplication and negation initialize the interval from '-pi*L' to zero, then binary search finds its cutoff.

Declaration kind. def.

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

Lean code for Definition10.6.5●1 definition

defdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

def QuantumBlockEncoding.HermiteBinaryCutoff.compute (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℕ

def QuantumBlockEncoding.HermiteBinaryCutoff.compute
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℕ

Source-level producer: one multiplication and negation initialize the
interval from `-pi*L` to zero, then binary search finds its cutoff.

Theorem10.6.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compute 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.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Theorem10.6.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_value (n : ℕ) (L : ℝ)
  (hL : 0 < L) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute n L).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_value
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute
        n L).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
      n L

Theorem10.6.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compute 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.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Theorem10.6.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_cost (n : ℕ) (L : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute n L).cost op =
    (2 * n + 2) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      (n + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_cost
  (n : ℕ) (L : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute
          n L).cost
      op =
    (2 * n + 2) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      (n + 1) *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op

Theorem10.6.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compute comparisons”; 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.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Theorem10.6.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_comparisons (n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute n L).cost
      QuantumBlockEncoding.StoredGivens.Op.compare =
    n + 1

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_comparisons
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute
          n L).cost
      QuantumBlockEncoding.StoredGivens.Op.compare =
    n + 1

Theorem10.6.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compute field operations”; 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.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

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

Lean code for Theorem10.6.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBinaryCutoff.lean

complete

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_field_operations
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute n L).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    2 * n + 2

theorem QuantumBlockEncoding.HermiteBinaryCutoff.compute_field_operations
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteBinaryCutoff.compute
          n L).cost
      QuantumBlockEncoding.StoredGivens.Op.field =
    2 * n + 2