QuantumBlockEncoding/StoredRectangularGivens.lean

This definition gives the library's named construction or computation for “append”. Copy the left list spine, sharing the right list.

def append (xs ys : List α) : Run (List α) :=
  ⟨xs ++ ys, xs.length • (tick .read + tick .write)⟩

commit-pinned source · Verso Blueprint panel

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

noncomputable def sweep {N M : ℕ} (A : StoredMatrix N M)
    (k : ℕ) : (remaining : ℕ) → k + remaining ≤ M → Run (Sweep N M)
  | 0, _ => pure ⟨A, []⟩
  | remaining + 1, columns =>
      let result := if h : k < N then do
        let first ← StoredGivens.columnSweep A ⟨k, by omega⟩ k (N - 1 - k) (by omega)
        let rest ← sweep first.matrix (k + 1) remaining (by omega)
        let steps ← append first.steps rest.steps
        pure ⟨rest.matrix, steps⟩
      else sweep A (k + 1) remaining (by omega)
      ⟨result.value, tick .compare + result.cost⟩

commit-pinned source · Verso Blueprint panel

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

theorem sweep_matrix {N M : ℕ} (A : StoredMatrix N M)
    (k remaining : ℕ) (columns : k + remaining ≤ M) :
    denote (sweep A k remaining columns).value.matrix =
      RectangularGivens.sweep (denote A) k remaining columns := by

commit-pinned source · Verso Blueprint panel

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

theorem sweep_steps {N M : ℕ} (A : StoredMatrix N M)
    (k remaining : ℕ) (columns : k + remaining ≤ M) :
    (sweep A k remaining columns).value.steps =
      RectangularGivens.sweepSteps (denote A) k remaining columns := by

commit-pinned source · Verso Blueprint panel

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

def columnBudget (N M : ℕ) : Cost := fun op =>
  N * stepBudget N M op + N * (tick .read op + tick .write op) + tick .compare op

commit-pinned source · Verso Blueprint panel

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

theorem sweep_cost_le {N M : ℕ} (A : StoredMatrix N M)
    (k remaining : ℕ) (columns : k + remaining ≤ M) (op : Op) :
    (sweep A k remaining columns).cost op ≤ remaining * columnBudget N M op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “identity”. Materialized identity, including its finite-index equality decisions.

def identity (N : ℕ) : Run (StoredMatrix N N) :=
  materialize (fun i j => charge .compare (if i = j then 1 else 0))

commit-pinned source · Verso Blueprint panel

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

theorem identity_value (N : ℕ) : denote (identity N).value = 1 := by

commit-pinned source · Verso Blueprint panel

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

def identityBudget (N : ℕ) : Cost := fun op =>
  N * N * tick .compare op + (N * N + N) * (2 * tick .read op + 2 * tick .write op)

commit-pinned source · Verso Blueprint panel

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

theorem identity_cost (N : ℕ) (op : Op) :
    (identity N).cost op = identityBudget N op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “replay”. Replay uses only a pair of stored row updates.

noncomputable def replay {N M : ℕ} : List (Step N) → StoredMatrix N M → Run (StoredMatrix N M)
  | [], A => charge .read A
  | step :: rest, A => do
      let current ← charge .read step
      let half ← StoredGivens.div current.angle 2
      let c ← StoredGivens.cos half
      let s ← StoredGivens.sin half
      let B ← rotate A current.first current.second c s
      replay rest B

commit-pinned source · Verso Blueprint panel

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

theorem replay_value {N M : ℕ} (steps : List (Step N)) (A : StoredMatrix N M) :
    denote (replay steps A).value = applySteps steps (denote A) := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

theorem replay_cost {N M : ℕ} (steps : List (Step N)) (A : StoredMatrix N M) (op : Op) :
    (replay steps A).cost op = steps.length * replayStepBudget N M op + tick .read op := by

commit-pinned source · Verso Blueprint panel

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

structure Result (N M : ℕ) where
  reduced : StoredMatrix N M
  transform : StoredMatrix N N
  steps : List (Step N)

commit-pinned source · Verso Blueprint panel

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

noncomputable def compile {N M : ℕ} (A : StoredMatrix N M) : Run (Result N M) := do
  let result ← sweep A 0 M (by omega)
  let initial ← identity N
  let E ← replay result.steps initial
  pure ⟨result.matrix, E, result.steps⟩

commit-pinned source · Verso Blueprint panel

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

theorem compile_reduced {N M : ℕ} (A : StoredMatrix N M) :
    denote (compile A).value.reduced = RectangularGivens.reduced (denote A) := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_steps {N M : ℕ} (A : StoredMatrix N M) :
    (compile A).value.steps = RectangularGivens.decompose (denote A) := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_transform {N M : ℕ} (A : StoredMatrix N M) :
    denote (compile A).value.transform = RectangularGivens.transform (denote A) := by

commit-pinned source · Verso Blueprint panel

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

def compileBudget (N M : ℕ) : Cost := fun op =>
  M * columnBudget N M op + identityBudget N op +
    (N * M) * replayStepBudget N N op + tick .read op

/-- A componentwise polynomial operation bound for residual, log, and the
fully stored accumulated transform produced by this actual algorithm. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile cost le”; the hypotheses and conclusion in the code panel fix its exact scope. A componentwise polynomial operation bound for residual, log, and the fully stored accumulated transform produced by this actual algorithm.

theorem compile_cost_le {N M : ℕ} (A : StoredMatrix N M) (op : Op) :
    (compile A).cost op ≤ compileBudget N M op := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_exact_recovery {N M : ℕ} (A : StoredMatrix N M) :
    (denote (compile A).value.transform).transpose * denote (compile A).value.reduced =
      denote A := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_transform_orthogonal {N M : ℕ} (A : StoredMatrix N M) :
    (denote (compile A).value.transform).transpose * denote (compile A).value.transform = 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_transform_det {N M : ℕ} (A : StoredMatrix N M) :
    (denote (compile A).value.transform).det = 1 := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_zero_below {N M : ℕ} (A : StoredMatrix N M)
    (row : Fin N) (col : Fin M) (below : col.val < row.val) :
    denote (compile A).value.reduced row col = 0 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “polynomial budget”. Expanded polynomial form of every operation category.

def polynomialBudget (N M : ℕ) : Cost
  | .field => N * M * (6 * M + 6 * N + 9)
  | .sqrt => N * M
  | .angle => N * M
  | .trig => 4 * N * M
  | .compare => 2 * N * M + M + N * N
  | .read => N * M * (10 * M + 14 * N + 10) + 2 * N * N + 2 * N + 1
  | .write => N * M * (6 * M + 10 * N + 1) + 2 * N * N + 2 * N
  | .emit => N * M

commit-pinned source · Verso Blueprint panel

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

theorem compileBudget_eq (N M : ℕ) : compileBudget N M = polynomialBudget N M := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_polynomial_cost_le {N M : ℕ} (A : StoredMatrix N M) (op : Op) :
    (compile A).cost op ≤ polynomialBudget N M op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “total”. Sum of the eight explicitly separated operation counters.

def total (cost : Cost) : ℕ :=
  cost .field + cost .sqrt + cost .angle + cost .trig +
    cost .compare + cost .read + cost .write + cost .emit

commit-pinned source · Verso Blueprint panel

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

theorem compile_total_cost_le {N M : ℕ} (A : StoredMatrix N M) :
    total (compile A).cost ≤
      N * M * (22 * M + 30 * N + 29) + 5 * N * N + 4 * N + M + 1 := by

commit-pinned source · Verso Blueprint panel