QuantumBlockEncoding/StoredGivens.lean

This type lists the allowed alternatives for “op”; its constructors are the cases that downstream code must handle.

inductive Op where
  | field | sqrt | angle | trig | compare | read | write | emit
  deriving DecidableEq, Fintype

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “cost”.

abbrev Cost := Op → ℕ

commit-pinned source · Verso Blueprint panel

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

def tick (op : Op) : Cost := fun q => if q = op then 1 else 0

commit-pinned source · Verso Blueprint panel

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

structure Run (α : Type) where
  value : α
  cost : Cost

commit-pinned source · Verso Blueprint panel

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

def Run.pure (x : α) : Run α := ⟨x, 0⟩

commit-pinned source · Verso Blueprint panel

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

def Run.bind (x : Run α) (f : α → Run β) : Run β :=
  let y := f x.value
  ⟨y.value, x.cost + y.cost⟩

instance : Monad Run where
  pure := Run.pure
  bind := Run.bind

commit-pinned source · Verso Blueprint panel

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

def charge (op : Op) (x : α) : Run α := ⟨x, tick op⟩

commit-pinned source · Verso Blueprint panel

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

noncomputable def add (x y : ℝ) : Run ℝ := charge .field (x + y)

commit-pinned source · Verso Blueprint panel

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

noncomputable def sub (x y : ℝ) : Run ℝ := charge .field (x - y)

commit-pinned source · Verso Blueprint panel

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

noncomputable def mul (x y : ℝ) : Run ℝ := charge .field (x * y)

commit-pinned source · Verso Blueprint panel

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

noncomputable def div (x y : ℝ) : Run ℝ := charge .field (x / y)

commit-pinned source · Verso Blueprint panel

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

noncomputable def sqrt (x : ℝ) : Run ℝ := charge .sqrt (Real.sqrt x)

commit-pinned source · Verso Blueprint panel

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

noncomputable def arccos (x : ℝ) : Run ℝ := charge .angle (Real.arccos x)

commit-pinned source · Verso Blueprint panel

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

noncomputable def cos (x : ℝ) : Run ℝ := charge .trig (Real.cos x)

commit-pinned source · Verso Blueprint panel

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

noncomputable def sin (x : ℝ) : Run ℝ := charge .trig (Real.sin x)

commit-pinned source · Verso Blueprint panel

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

noncomputable def zeroTest (x : ℝ) : Run Bool := charge .compare (decide (x = 0))

commit-pinned source · Verso Blueprint panel

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

noncomputable def signTest (x : ℝ) : Run Bool := charge .compare (decide (x < 0))

commit-pinned source · Verso Blueprint panel

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

def read {n : ℕ} (xs : Vector α n) (i : Fin n) : Run α := charge .read xs[i.val]

/-- Two materialized passes: write counted entries, read them for projection
and summation, and write the projected output. Counter words are metadata. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “collect”. Two materialized passes: write counted entries, read them for projection and summation, and write the projected output.

def collect {n : ℕ} (f : Fin n → Run α) : Run (Vector α n) :=
  let entries : Vector (Run α) n := Vector.ofFn f
  ⟨entries.map Run.value,
    (fun op => ∑ i : Fin n, entries[i.val].cost op) +
      n • (2 • tick .read + 2 • tick .write)⟩

/-- Persistent full-copy replacement; row references are stored words. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “replace”. Persistent full-copy replacement; row references are stored words.

def replace {n : ℕ} (xs : Vector α n) (i : Fin n) (x : α) : Run (Vector α n) :=
  ⟨xs.set i.val x, n • (tick .read + tick .write)⟩

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “stored matrix”.

abbrev StoredMatrix (N M : ℕ) := Vector (Vector ℝ M) N

commit-pinned source · Verso Blueprint panel

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

def denote {N M : ℕ} (A : StoredMatrix N M) : _root_.Matrix (Fin N) (Fin M) ℝ :=
  fun i j => A[i.val][j.val]

/-- Materializing an input callback is an explicit boundary: this constructor
charges storage but does not certify the callback's scalar evaluation cost. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “materialize”. Materializing an input callback is an explicit boundary: this constructor charges storage but does not certify the callback's scalar evaluation cost.

def materialize {N M : ℕ} (f : Fin N → Fin M → Run ℝ) : Run (StoredMatrix N M) :=
  collect (fun i => collect (f i))

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem collect_value {n : ℕ} (f : Fin n → Run α) (i : Fin n) :
    (collect f).value[i.val] = (f i).value := by simp [collect]

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem collect_cost {n : ℕ} (f : Fin n → Run α) (op : Op) :
    (collect f).cost op = (∑ i : Fin n, (f i).cost op) +
      n * (2 * tick .read op + 2 * tick .write op) := by simp [collect]; ring

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “angle”. Compute the norm once, then the exact signed angle once.

noncomputable def angle (x y : ℝ) : Run ℝ := do
  let xx ← mul x x
  let yy ← mul y y
  let ss ← add xx yy
  let r ← sqrt ss
  let zero ← zeroTest r
  if zero then pure 0 else do
    let ratio ← div x r
    let a ← arccos ratio
    let negative ← signTest y
    let signed ← if negative then sub 0 a else pure a

commit-pinned source · Verso Blueprint panel

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

theorem angle_value (x y : ℝ) : (angle x y).value = eliminationAngle x y := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “coefficients”. One angle and one pair of trigonometric coefficients are shared by all entries of the two output rows.

noncomputable def coefficients (x y : ℝ) : Run (ℝ × ℝ × ℝ) := do
  let theta ← angle x y
  let half ← div theta 2
  let c ← cos half
  let s ← sin half
  pure (theta, c, s)

commit-pinned source · Verso Blueprint panel

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

theorem coefficients_value (x y : ℝ) : (coefficients x y).value =
    (eliminationAngle x y, Real.cos (eliminationAngle x y / 2),
      Real.sin (eliminationAngle x y / 2)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “entry pair”. The six actual field operations for a pair of entries.

noncomputable def entryPair (c s : ℝ) (u v : ℝ) : Run (ℝ × ℝ) := do
  let cu ← mul c u
  let sv ← mul s v
  let su ← mul s u
  let cv ← mul c v
  let first ← sub cu sv
  let second ← add su cv
  pure (first, second)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem entryPair_value (c s u v : ℝ) :
    (entryPair c s u v).value = (c * u - s * v, s * u + c * v) := rfl

commit-pinned source · Verso Blueprint panel

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

theorem entryPair_cost (c s u v : ℝ) (op : Op) :
    (entryPair c s u v).cost op = 6 * tick .field op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “row pair”. Materialize both rows from a single stored vector of computed pairs.

noncomputable def rowPair {M : ℕ} (u v : Vector ℝ M) (c s : ℝ) :
    Run (Vector ℝ M × Vector ℝ M) := do
  let pairs ← collect fun j => do
    let x ← read u j
    let y ← read v j
    entryPair c s x y
  let first ← collect fun j => do
    let pair ← read pairs j
    pure pair.1
  let second ← collect fun j => do
    let pair ← read pairs j

commit-pinned source · Verso Blueprint panel

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

theorem rowPair_value {M : ℕ} (u v : Vector ℝ M) (c s : ℝ) (j : Fin M) :
    (rowPair u v c s).value.1[j.val] = c * u[j.val] - s * v[j.val] ∧
    (rowPair u v c s).value.2[j.val] = s * u[j.val] + c * v[j.val] := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “rotate”. Cached input rows, materialized output rows, then two stored replacements.

noncomputable def rotate {N M : ℕ} (A : StoredMatrix N M) (i j : Fin N)
    (c s : ℝ) : Run (StoredMatrix N M) := do
  let u ← read A i
  let v ← read A j
  let rows ← rowPair u v c s
  let B ← replace A j rows.2
  replace B i rows.1

commit-pinned source · Verso Blueprint panel

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

theorem rotate_value {N M : ℕ} (A : StoredMatrix N M) (i j : Fin N)
    (theta : ℝ) :
    denote (rotate A i j (Real.cos (theta / 2)) (Real.sin (theta / 2))).value =
      rotateRows (denote A) i j theta := by

commit-pinned source · Verso Blueprint panel

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

structure Elimination (N M : ℕ) where
  matrix : StoredMatrix N M
  angle : ℝ

commit-pinned source · Verso Blueprint panel

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

noncomputable def eliminate {N M : ℕ} (A : StoredMatrix N M)
    (i j : Fin N) (col : Fin M) : Run (Elimination N M) := do
  let u ← read A i
  let v ← read A j
  let x ← read u col
  let y ← read v col
  let cs ← coefficients x y
  let B ← rotate A i j cs.2.1 cs.2.2
  pure ⟨B, cs.1⟩

commit-pinned source · Verso Blueprint panel

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

theorem eliminate_angle {N M : ℕ} (A : StoredMatrix N M)
    (i j : Fin N) (col : Fin M) :
    (eliminate A i j col).value.angle = eliminationAngle (denote A i col) (denote A j col) := by

commit-pinned source · Verso Blueprint panel

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

theorem eliminate_matrix {N M : ℕ} (A : StoredMatrix N M)
    (i j : Fin N) (col : Fin M) :
    denote (eliminate A i j col).value.matrix = eliminateEntry (denote A) i j col := by

commit-pinned source · Verso Blueprint panel

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

structure Sweep (N M : ℕ) where
  matrix : StoredMatrix N M
  steps : List (Step N)

/-- One recursion returns both the residual and its actual chronological log.
No separate rerun is used to generate angles or the next matrix. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “column sweep”. One recursion returns both the residual and its actual chronological log.

noncomputable def columnSweep {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo : ℕ) : (count : ℕ) → lo + count < N → Run (Sweep N M)
  | 0, _ => pure ⟨A, []⟩
  | count + 1, bound => do
      let first : Fin N := ⟨lo + count, by omega⟩
      let second : Fin N := ⟨lo + count + 1, by omega⟩
      let next ← eliminate A first second col
      let tail ← columnSweep next.matrix col lo count (by omega)
      let steps ← charge .emit
        ({ first := first, second := second, adjacent := rfl, angle := next.angle } :: tail.steps)
      pure ⟨tail.matrix, steps⟩

commit-pinned source · Verso Blueprint panel

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

theorem columnSweep_matrix {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
    denote (columnSweep A col lo count bound).value.matrix =
      AdjacentGivens.columnSweep (denote A) col lo count bound := by

commit-pinned source · Verso Blueprint panel

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

theorem columnSweep_steps {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
    (columnSweep A col lo count bound).value.steps =
      columnSweepSteps (denote A) col lo count bound := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “angle budget”. Branch-independent upper bound; the zero pair uses fewer operations.

def angleBudget : Cost :=
  7 • tick .field + tick .sqrt + tick .angle + 2 • tick .compare

commit-pinned source · Verso Blueprint panel

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

theorem angle_cost_le (x y : ℝ) (op : Op) : (angle x y).cost op ≤ angleBudget op := by

commit-pinned source · Verso Blueprint panel

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

def coefficientBudget : Cost := angleBudget + tick .field + 2 • tick .trig

commit-pinned source · Verso Blueprint panel

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

theorem coefficients_cost_le (x y : ℝ) (op : Op) :
    (coefficients x y).cost op ≤ coefficientBudget op := by

commit-pinned source · Verso Blueprint panel

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

theorem rowPair_cost {M : ℕ} (u v : Vector ℝ M) (c s : ℝ) (op : Op) :
    (rowPair u v c s).cost op =
      M * (6 * tick .field op + 10 * tick .read op + 6 * tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

theorem rotate_cost {N M : ℕ} (A : StoredMatrix N M) (i j : Fin N)
    (c s : ℝ) (op : Op) :
    (rotate A i j c s).cost op =
      M * (6 * tick .field op + 10 * tick .read op + 6 * tick .write op) +
      2 * N * (tick .read op + tick .write op) + 2 * tick .read op := by

commit-pinned source · Verso Blueprint panel

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

def eliminationBudget (N M : ℕ) : Cost := fun op =>
  coefficientBudget op +
    M * (6 * tick .field op + 10 * tick .read op + 6 * tick .write op) +
    2 * N * (tick .read op + tick .write op) + 6 * tick .read op

commit-pinned source · Verso Blueprint panel

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

theorem eliminate_cost_le {N M : ℕ} (A : StoredMatrix N M)
    (i j : Fin N) (col : Fin M) (op : Op) :
    (eliminate A i j col).cost op ≤ eliminationBudget N M op := by

commit-pinned source · Verso Blueprint panel

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

def stepBudget (N M : ℕ) : Cost := eliminationBudget N M + tick .emit

commit-pinned source · Verso Blueprint panel

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

theorem columnSweep_cost_succ {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + (count + 1) < N) (op : Op) :
    (columnSweep A col lo (count + 1) bound).cost op =
      (eliminate A ⟨lo + count, by omega⟩ ⟨lo + count + 1, by omega⟩ col).cost op +
      (columnSweep
        (eliminate A ⟨lo + count, by omega⟩ ⟨lo + count + 1, by omega⟩ col).value.matrix
        col lo count (by omega)).cost op + tick .emit op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “column sweep cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Symbolic bound on the actual fused producer, not on just its log length.

theorem columnSweep_cost_le {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) (op : Op) :
    (columnSweep A col lo count bound).cost op ≤ count * stepBudget N M op := by

commit-pinned source · Verso Blueprint panel

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

theorem stepBudget_fields (N M : ℕ) :
    stepBudget N M .field = 6 * M + 8 ∧
    stepBudget N M .sqrt = 1 ∧
    stepBudget N M .angle = 1 ∧
    stepBudget N M .trig = 2 ∧
    stepBudget N M .compare = 2 ∧
    stepBudget N M .read = 10 * M + 2 * N + 6 ∧
    stepBudget N M .write = 6 * M + 2 * N ∧
    stepBudget N M .emit = 1 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “column sweep emit”; the hypotheses and conclusion in the code panel fix its exact scope. Each iteration emits exactly one record, including a harmless zero-pair rotation.

theorem columnSweep_emit {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
    (columnSweep A col lo count bound).cost .emit = count := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “column sweep steps length”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem columnSweep_steps_length {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
    (columnSweep A col lo count bound).value.steps.length = count := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “column sweep action”; the hypotheses and conclusion in the code panel fix its exact scope. The emitted list and materialized residual are a single coherent run.

theorem columnSweep_action {N M : ℕ} (A : StoredMatrix N M)
    (col : Fin M) (lo count : ℕ) (bound : lo + count < N) :
    applySteps (columnSweep A col lo count bound).value.steps (denote A) =
      denote (columnSweep A col lo count bound).value.matrix := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “materialize cost”; the hypotheses and conclusion in the code panel fix its exact scope. Input generation is charged once per materialized entry, and the specified callback must itself use the counted scalar interface.

theorem materialize_cost {N M : ℕ} (f : Fin N → Fin M → Run ℝ) (op : Op) :
    (materialize f).cost op =
      (∑ i : Fin N, ∑ j : Fin M, (f i j).cost op) +
      (N * M + N) * (2 * tick .read op + 2 * tick .write op) := by

commit-pinned source · Verso Blueprint panel