QuantumBlockEncoding/StoredDyadicSpans.lean

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

structure SpanRun (α : Type) where
  run : Run α
  integerDoublings : ℕ

/-- Complete persistent copy, including the appended last value. -/

commit-pinned source · Verso Blueprint panel

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

def append {m : ℕ} (xs : Vector ℕ (m + 1)) (last : ℕ) : Run (Vector ℕ (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 value”; the hypotheses and conclusion in the code panel fix its exact scope.

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

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

def spans : (n : ℕ) → SpanRun (Vector ℕ (n + 1))
  | 0 => ⟨collect (fun _ => pure 1), 0⟩
  | n + 1 =>
      let previous := spans n
      let result : Run (Vector ℕ (n + 2)) := do
        let last ← read previous.run.value (Fin.last n)
        append previous.run.value (last * 2)
      ⟨⟨result.value, previous.run.cost + result.cost⟩,
        previous.integerDoublings + 1⟩

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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.

theorem spans_vector_value (n : ℕ) :
    (spans n).run.value = Vector.ofFn (fun r : Fin (n + 1) => 2^r.val) := by

commit-pinned source · Verso Blueprint panel

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

theorem spans_integerDoublings (n : ℕ) : (spans n).integerDoublings = n := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

theorem spans_field_cost (n : ℕ) : (spans n).run.cost .field = 0 := by

commit-pinned source · Verso Blueprint panel

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.

theorem spans_word_bound (n : ℕ) (r : Fin (n + 1)) :
    (spans n).run.value[r.val] ≤ 2^n ∧ (spans n).run.value[r.val] < 2^(n + 1) := by

commit-pinned source · Verso Blueprint panel

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

def atStage {n : ℕ} (xs : Vector ℕ (n + 1)) (t : Fin (n + 1)) : Run ℕ :=
  read xs ⟨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 : ℕ) (t : Fin (n + 1)) :
    (atStage (spans n).run.value t).value = 2^(n - t.val) :=
  spans_value n ⟨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 : ℕ} (xs : Vector ℕ (n + 1)) (t : Fin (n + 1)) (op : Op) :
    (atStage xs t).cost op = tick .read op := rfl

commit-pinned source · Verso Blueprint panel

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

theorem spans_certified (n : ℕ) :
    let result := spans n
    (∀ r : Fin (n + 1), result.run.value[r.val] = 2^r.val) ∧
    result.integerDoublings = n ∧
    (∑ op : Op, result.run.cost op) = 3 * n^2 + 9 * n + 4 ∧
    (∀ r : Fin (n + 1), result.run.value[r.val] ≤ 2^n ∧ result.run.value[r.val] < 2^(n + 1)) :=
  ⟨spans_value n, spans_integerDoublings n, spans_total_cost n, spans_word_bound n⟩

commit-pinned source · Verso Blueprint panel