QuantumBlockEncoding/StoredHermiteGeometry.lean

This record groups the data and proof fields needed for “tail level”. A proposition-valued field is a requirement until a constructor supplies it.

structure TailLevel where
  width : ℝ
  factor : ℝ

/-- Full-copy persistent extension; each copied record is a stored word. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “append level”. Full-copy persistent extension; each copied record is a stored word.

def appendLevel {m : ℕ} (xs : Vector TailLevel (m + 1)) (last : TailLevel) :
    Run (Vector TailLevel (m + 2)) :=
  collect fun i =>
    let result := if h : i.val < m + 1 then read xs ⟨i.val, h⟩ else pure last
    ⟨result.value, tick .compare + result.cost⟩

commit-pinned source · Verso Blueprint panel

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

theorem appendLevel_value {m : ℕ} (xs : Vector TailLevel (m + 1))
    (last : TailLevel) (i : Fin (m + 2)) :
    (appendLevel xs last).value[i.val] =
      if h : i.val < m + 1 then xs[i.val] else last := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “halve”. Repeated charged division, never an uncharged cast of 2^n.

noncomputable def halve : ℕ → ℝ → Run ℝ
  | 0, x => pure x
  | n + 1, x => do
      let y ← halve n x
      StoredGivens.div y 2

commit-pinned source · Verso Blueprint panel

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

theorem halve_value (n : ℕ) (x : ℝ) :
    (halve n x).value = x / (2 : ℝ)^n := by

commit-pinned source · Verso Blueprint panel

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

theorem halve_cost (n : ℕ) (x : ℝ) (op : Op) :
    (halve n x).cost op = n * tick .field op := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def step (n : ℕ) (L : ℝ) : Run ℝ := do
  let width ← StoredGivens.mul Real.pi L
  halve n width

commit-pinned source · Verso Blueprint panel

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

theorem step_value (n : ℕ) (L : ℝ) : (step n L).value = gridStep n L := by

commit-pinned source · Verso Blueprint panel

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

theorem step_cost (n : ℕ) (L : ℝ) (op : Op) :
    (step n L).cost op = (n + 1) * tick .field op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “root width”; the hypotheses and conclusion in the code panel fix its exact scope. Public root-width identity for geometry integration.

theorem root_width (n : ℕ) (L : ℝ) :
    gridStep n L * (2 : ℝ)^n = Real.pi * L := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tails”. One exponential is evaluated and stored per level.

noncomputable def tails (grid : ℝ) : (n : ℕ) → SourceRun (Vector TailLevel (n + 1))
  | 0 =>
      let result : Run (Vector TailLevel 1) := do
        let negative ← StoredGivens.sub 0 grid
        let factor ← (exponential negative).run
        collect fun _ => pure (⟨grid, factor⟩ : TailLevel)
      ⟨result, 1⟩
  | n + 1 =>
      let previous := tails grid n
      let result : Run (Vector TailLevel (n + 2)) := do
        let last ← read previous.run.value (Fin.last n)

commit-pinned source · Verso Blueprint panel

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

theorem tails_value (grid : ℝ) (n : ℕ) (r : Fin (n + 1)) :
    ((tails grid n).run.value[r.val]).width = grid * (2 : ℝ)^r.val ∧
    ((tails grid n).run.value[r.val]).factor = Real.exp (-grid * (2 : ℝ)^r.val) := by

commit-pinned source · Verso Blueprint panel

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

theorem tails_exponentialCalls (grid : ℝ) (n : ℕ) :
    (tails grid n).exponentialCalls = n + 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem appendLevel_cost_le {m : ℕ} (xs : Vector TailLevel (m + 1))
    (last : TailLevel) (op : Op) :
    (appendLevel xs last).cost op ≤ 6 * (m + 2) := by

commit-pinned source · Verso Blueprint panel

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

theorem tails_cost_le (grid : ℝ) (n : ℕ) (op : Op) :
    (tails grid n).run.cost op ≤ 12 * (n + 1)^2 := by

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “tail cache”. A proposition-valued field is a requirement until a constructor supplies it.

structure TailCache (n : ℕ) where
  cutoff : ℕ
  grid : ℝ
  levels : Vector TailLevel (n + 1)

/-- The actual binary-search cutoff and actual width cache are supplied in
the same run. No precomputed cutoff or coordinate callback is an input. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tail cache”. The actual binary-search cutoff and actual width cache are supplied in the same run.

noncomputable def tailCache (n : ℕ) (L : ℝ) : SourceRun (TailCache n) :=
  let cutoff := HermiteBinaryCutoff.compute n L
  let spacing := step n L
  let cached := tails spacing.value n
  ⟨⟨⟨cutoff.value, spacing.value, cached.run.value⟩,
    cutoff.cost + spacing.cost + cached.run.cost⟩, cached.exponentialCalls⟩

commit-pinned source · Verso Blueprint panel

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

theorem tailCache_value (n : ℕ) (L : ℝ) (hL : 0 < L) :
    (tailCache n L).run.value.cutoff = cutIndex n L ∧
    (tailCache n L).run.value.grid = gridStep n L ∧
    ∀ r : Fin (n + 1),
      ((tailCache n L).run.value.levels[r.val]).width = gridStep n L * (2 : ℝ)^r.val ∧
      ((tailCache n L).run.value.levels[r.val]).factor =
        Real.exp (-gridStep n L * (2 : ℝ)^r.val) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “tail cache exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem tailCache_exponentialCalls (n : ℕ) (L : ℝ) :
    (tailCache n L).exponentialCalls = n + 1 := tails_exponentialCalls _ _

commit-pinned source · Verso Blueprint panel

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

theorem tailCache_cost_le (n : ℕ) (L : ℝ) (op : Op) :
    (tailCache n L).run.cost op ≤ 16 * (n + 1)^2 := by

commit-pinned source · Verso Blueprint panel

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

theorem tailCache_total_cost_le (n : ℕ) (L : ℝ) :
    (∑ op : Op, (tailCache n L).run.cost op) ≤ 128 * (n + 1)^2 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “at stage”. The cache is physically indexed by r, but consumers use chronological source stage t=0,...,n and access r=n-t with a charged stored-word read.

def atStage {n : ℕ} (cache : TailCache n) (t : Fin (n + 1)) : Run TailLevel :=
  read cache.levels ⟨n - t.val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

theorem atStage_value (n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) :
    (atStage (tailCache n L).run.value t).value.width =
      gridStep n L * (2 : ℝ)^(n - t.val) ∧
    (atStage (tailCache n L).run.value t).value.factor =
      Real.exp (-gridStep n L * (2 : ℝ)^(n - t.val)) :=
  (tailCache_value n L hL).2.2 ⟨n - t.val, by omega⟩

commit-pinned source · Verso Blueprint panel

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

theorem atStage_cost {n : ℕ} (cache : TailCache n) (t : Fin (n + 1)) (op : Op) :
    (atStage cache t).cost op = tick .read op := rfl

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “at stage left free”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem atStage_leftFree (n : ℕ) (L : ℝ) (hL : 0 < L)
    (t : Fin (n + 1)) (bit : Bool) :
    (if bit then 1 else (atStage (tailCache n L).run.value t).value.factor) =
      leftFree (gridStep n L) (n - t.val) bit := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “at stage right free”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem atStage_rightFree (n : ℕ) (L : ℝ) (hL : 0 < L)
    (t : Fin (n + 1)) (bit : Bool) :
    (if bit then (atStage (tailCache n L).run.value t).value.factor else 1) =
      rightFree (gridStep n L) (n - t.val) bit := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “at stage right core”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem atStage_rightCore (n : ℕ) (L : ℝ) (hL : 0 < L)
    (t : Fin (n + 1)) (bit : Bool) :
    (if t.val = 0 then (if bit then 1 else 0) else
      (if bit then (atStage (tailCache n L).run.value t).value.factor else 1)) =
      rightCore n (gridStep n L) (n - t.val) bit := by

commit-pinned source · Verso Blueprint panel

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

theorem atStage_bounds (n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) :
    0 ≤ (atStage (tailCache n L).run.value t).value.factor ∧
      (atStage (tailCache n L).run.value t).value.factor ≤ 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “left injection”. A disabled injection performs no scalar arithmetic and no exponential.

noncomputable def leftInjection (enabled : Bool) (lower width grid : ℝ) : SourceRun ℝ :=
  if enabled then
    let result : Run ℝ := do
      let upper ← StoredGivens.add lower width
      let last ← StoredGivens.sub upper grid
      (exponential last).run
    ⟨⟨result.value, tick .compare + result.cost⟩, 1⟩
  else ⟨⟨0, tick .compare⟩, 0⟩

commit-pinned source · Verso Blueprint panel

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

theorem leftInjection_value (enabled : Bool) (origin grid lower width : ℝ)
    (first r : ℕ) (hl : lower = affinePoint origin grid first)
    (hw : width = grid * (2 : ℝ)^r) :
    (leftInjection enabled lower width grid).run.value =
      if enabled then leftInject origin grid first r else 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left injection last point”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftInjection_lastPoint (origin grid lower width : ℝ)
    (first r : ℕ) (hl : lower = affinePoint origin grid first)
    (hw : width = grid * (2 : ℝ)^r) :
    (leftInjection true lower width grid).run.value =
      Real.exp (affinePoint origin grid (first + 2^r - 1)) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “left injection exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem leftInjection_exponentialCalls (enabled : Bool) (lower width grid : ℝ) :
    (leftInjection enabled lower width grid).exponentialCalls = if enabled then 1 else 0 := by

commit-pinned source · Verso Blueprint panel

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

theorem leftInjection_cost (enabled : Bool) (lower width grid : ℝ) (op : Op) :
    (leftInjection enabled lower width grid).run.cost op = tick .compare op +
      (if enabled then 2 * tick .field op else 0) := by

commit-pinned source · Verso Blueprint panel

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

theorem leftInjection_bounds (n : ℕ) (L : ℝ) (hL : 0 < L)
    (enabled : Bool) (lower width : ℝ) (first r : ℕ)
    (hl : lower = affinePoint (-Real.pi * L) (gridStep n L) first)
    (hw : width = gridStep n L * (2 : ℝ)^r)
    (guard : enabled = true → Full 0 (cutIndex n L) first (2^r)) :
    0 ≤ (leftInjection enabled lower width (gridStep n L)).run.value ∧
      (leftInjection enabled lower width (gridStep n L)).run.value ≤ 1 := by

commit-pinned source · Verso Blueprint panel