QuantumBlockEncoding/HermiteBinaryCutoff.lean

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

noncomputable def below (x : ℝ) : Run Bool :=
  charge .compare (decide (x < -1))

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

commit-pinned source · Verso Blueprint panel

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

noncomputable def search : (remaining start : ℕ) → (lower span : ℝ) → Run ℕ
  | 0, start, lower, _ => do
      let yes ← below lower
      pure (if yes then start + 1 else start)
  | remaining + 1, start, lower, span => do
      let half ← StoredGivens.div span 2
      let middle ← StoredGivens.add lower half
      let yes ← below middle
      if yes then search remaining (start + 2 ^ remaining) middle half
      else search remaining start lower half

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “search cost”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

noncomputable def compute (n : ℕ) (L : ℝ) : Run ℕ := do
  let width ← StoredGivens.mul Real.pi L
  let lower ← StoredGivens.sub 0 width
  search n 0 lower width

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compute value”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compute cost”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compute comparisons”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compute_comparisons (n : ℕ) (L : ℝ) :
    (compute n L).cost .compare = n + 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compute field operations”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem compute_field_operations (n : ℕ) (L : ℝ) :
    (compute n L).cost .field = 2 * n + 2 := by

commit-pinned source · Verso Blueprint panel