QuantumBlockEncoding/StoredIsometryCompletion.lean

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

structure Positions (N r : ℕ) where
  values : Vector (Fin N) r
  injective : Function.Injective (fun i : Fin r => values[i.val])

commit-pinned source · Verso Blueprint panel

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

def Positions.embedding {N r : ℕ} (e : Positions N r) : Fin r ↪ Fin N :=
  ⟨fun i => e.values[i.val], e.injective⟩

/-- Materialize a counted physical-label generator. Injectivity is an input
contract, not a charged search for a proof or a freely evaluated embedding. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “materialize”. Materialize a counted physical-label generator.

def Positions.materialize {N r : ℕ} (f : Fin r → Run (Fin N))
    (injective : Function.Injective (fun i => (f i).value)) : Run (Positions N r) :=
  let entries := collect f
  ⟨⟨entries.value, by
      intro a b equal
      apply injective
      simpa [entries] using equal⟩, entries.cost⟩

commit-pinned source · Verso Blueprint panel

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

theorem Positions.materialize_value {N r : ℕ} (f : Fin r → Run (Fin N))
    (injective : Function.Injective (fun i => (f i).value)) (i : Fin r) :
    (Positions.materialize f injective).value.embedding i = (f i).value := 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.

theorem Positions.materialize_cost {N r : ℕ} (f : Fin r → Run (Fin N))
    (injective : Function.Injective (fun i => (f i).value)) (op : Op) :
    (Positions.materialize f injective).cost op = (∑ i : Fin r, (f i).cost op) +
      r * (2 * tick .read op + 2 * tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

def transpose {N M : ℕ} (A : StoredMatrix N M) : Run (StoredMatrix M N) :=
  materialize fun i j => do
    let row ← read A j
    read row i

commit-pinned source · Verso Blueprint panel

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

theorem transpose_value {N M : ℕ} (A : StoredMatrix N M) :
    denote (transpose A).value = (denote A).transpose := by

commit-pinned source · Verso Blueprint panel

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

def transposeBudget (N M : ℕ) : Cost := fun op =>
  (4 * N * M + 2 * M) * tick .read op + (2 * N * M + 2 * M) * tick .write op

commit-pinned source · Verso Blueprint panel

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

theorem transpose_cost {N M : ℕ} (A : StoredMatrix N M) (op : Op) :
    (transpose A).cost op = transposeBudget N M op := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def prefixCompletion {N r : ℕ} (V : StoredMatrix N r) :
    Run (StoredMatrix N N) := do
  let result ← StoredRectangularGivens.compile V
  transpose result.transform

commit-pinned source · Verso Blueprint panel

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

theorem prefixCompletion_value {N r : ℕ} (V : StoredMatrix N r) :
    denote (prefixCompletion V).value =
      ConstructiveIsometryCompletion.prefixCompletion (denote V) := by

commit-pinned source · Verso Blueprint panel

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

def prefixBudget (N r : ℕ) : Cost :=
  StoredRectangularGivens.polynomialBudget N r + transposeBudget N N

commit-pinned source · Verso Blueprint panel

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

theorem prefixCompletion_cost_le {N r : ℕ} (V : StoredMatrix N r) (op : Op) :
    (prefixCompletion V).cost op ≤ prefixBudget N r op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “swap index”. Both equality decisions are actual charged operations; the second is skipped if the first comparison succeeds.

def swapIndex {N : ℕ} (x y z : Fin N) : Run (Fin N) := do
  let first ← charge .compare (decide (z = x))
  if first then pure y else do
    let second ← charge .compare (decide (z = y))
    if second then pure x else pure z

commit-pinned source · Verso Blueprint panel

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

theorem swapIndex_value {N : ℕ} (x y z : Fin N) :
    (swapIndex x y z).value = Equiv.swap x y z := by

commit-pinned source · Verso Blueprint panel

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

theorem swapIndex_cost_le {N : ℕ} (x y z : Fin N) (op : Op) :
    (swapIndex x y z).cost op ≤ 2 * tick .compare op := by

commit-pinned source · Verso Blueprint panel

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

structure PermutationTable (N : ℕ) where
  forward : Vector (Fin N) N
  inverse : Vector (Fin N) N
  polarity : ℝ

commit-pinned source · Verso Blueprint panel

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

def identityPermutation (N : ℕ) : Run (PermutationTable N) := do
  let forward ← collect (fun i : Fin N => pure i)
  let inverse ← collect (fun i : Fin N => pure i)
  pure ⟨forward, inverse, 1⟩

commit-pinned source · Verso Blueprint panel

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

noncomputable def swapPermutation {N : ℕ} (p : PermutationTable N) (x y : Fin N) :
    Run (PermutationTable N) := do
  let forward ← collect fun i => do
    let old ← read p.forward i
    swapIndex x y old
  let inverse ← collect fun i => do
    let oldIndex ← swapIndex x y i
    read p.inverse oldIndex
  let same ← charge .compare (decide (x = y))
  let polarity ← if same then pure p.polarity else StoredGivens.sub 0 p.polarity
  pure ⟨forward, inverse, polarity⟩

commit-pinned source · Verso Blueprint panel

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

theorem swapPermutation_forward {N : ℕ} (p : PermutationTable N) (x y i : Fin N) :
    (swapPermutation p x y).value.forward[i.val] = Equiv.swap x y p.forward[i.val] := by

commit-pinned source · Verso Blueprint panel

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

theorem swapPermutation_inverse {N : ℕ} (p : PermutationTable N) (x y i : Fin N) :
    (swapPermutation p x y).value.inverse[i.val] = p.inverse[(Equiv.swap x y i).val] := by

commit-pinned source · Verso Blueprint panel

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

theorem swapPermutation_polarity {N : ℕ} (p : PermutationTable N) (x y : Fin N) :
    (swapPermutation p x y).value.polarity = if x = y then p.polarity else -p.polarity := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “real sign”. A proof-only interpretation of permutation orientation.

def realSign {N : ℕ} (p : Equiv.Perm (Fin N)) : ℝ := (Equiv.Perm.sign p : ℤ)

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “real sign swap trans”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem realSign_swap_trans {N : ℕ} (p : Equiv.Perm (Fin N)) (x y : Fin N) :
    realSign (p.trans (Equiv.swap x y)) = if x = y then realSign p else -realSign p := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “real sign one iff”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem realSign_one_iff {N : ℕ} (p : Equiv.Perm (Fin N)) :
    realSign p = 1 ↔ Equiv.Perm.sign p = 1 := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def permutation {N r : ℕ} (hr : r ≤ N) (e : Positions N r) :
    (k : ℕ) → k ≤ r → Run (PermutationTable N)
  | 0, _ => identityPermutation N
  | k + 1, hk => do
      let p ← permutation hr e k (by omega)
      let x ← read p.forward ⟨k, by omega⟩
      let y ← read e.values ⟨k, by omega⟩
      swapPermutation p x y

commit-pinned source · Verso Blueprint panel

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

theorem permutation_forward {N r : ℕ} (hr : r ≤ N) (e : Positions N r)
    (k : ℕ) (hk : k ≤ r) (i : Fin N) :
    (permutation hr e k hk).value.forward[i.val] =
      ConstructiveIsometryCompletion.extendPrefix hr e.embedding k hk i := by

commit-pinned source · Verso Blueprint panel

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

theorem permutation_inverse {N r : ℕ} (hr : r ≤ N) (e : Positions N r)
    (k : ℕ) (hk : k ≤ r) (i : Fin N) :
    (permutation hr e k hk).value.inverse[i.val] =
      (ConstructiveIsometryCompletion.extendPrefix hr e.embedding k hk).symm i := by

commit-pinned source · Verso Blueprint panel

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

theorem permutation_polarity {N r : ℕ} (hr : r ≤ N) (e : Positions N r)
    (k : ℕ) (hk : k ≤ r) :
    (permutation hr e k hk).value.polarity =
      realSign (ConstructiveIsometryCompletion.extendPrefix hr e.embedding k hk) := by

commit-pinned source · Verso Blueprint panel

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

theorem collect_cost_le {n : ℕ} (f : Fin n → Run α) (op : Op) (cap : ℕ)
    (bounded : ∀ i, (f i).cost op ≤ cap) :
    (collect f).cost op ≤ n * (cap + 2 * tick .read op + 2 * tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

def swapBudget (N : ℕ) : Cost := fun op =>
  tick .field op + (4 * N + 1) * tick .compare op +
    6 * N * tick .read op + 4 * N * tick .write op

commit-pinned source · Verso Blueprint panel

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

theorem swapPermutation_cost_le {N : ℕ} (p : PermutationTable N) (x y : Fin N) (op : Op) :
    (swapPermutation p x y).cost op ≤ swapBudget N op := by

commit-pinned source · Verso Blueprint panel

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

def permutationBudget (N k : ℕ) : Cost := fun op =>
  4 * N * (tick .read op + tick .write op) + k * (swapBudget N op + 2 * tick .read op)

commit-pinned source · Verso Blueprint panel

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

theorem identityPermutation_cost (N : ℕ) (op : Op) :
    (identityPermutation N).cost op = 4 * N * (tick .read op + tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

theorem permutation_cost_le {N r : ℕ} (hr : r ≤ N) (e : Positions N r)
    (k : ℕ) (hk : k ≤ r) (op : Op) :
    (permutation hr e k hk).cost op ≤ permutationBudget N k op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “permute columns”. Every matrix entry reads its old column from the stored inverse table.

def permuteColumns {N : ℕ} (U : StoredMatrix N N) (inverse : Vector (Fin N) N) :
    Run (StoredMatrix N N) :=
  materialize fun row col => do
    let old ← StoredGivens.read inverse col
    let values ← StoredGivens.read U row
    StoredGivens.read values old

commit-pinned source · Verso Blueprint panel

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

theorem permuteColumns_value {N : ℕ} (U : StoredMatrix N N) (inverse : Vector (Fin N) N)
    (row col : Fin N) :
    denote (permuteColumns U inverse).value row col = denote U row inverse[col.val] := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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

theorem permuteColumns_cost {N : ℕ} (U : StoredMatrix N N) (inverse : Vector (Fin N) N)
    (op : Op) : (permuteColumns U inverse).cost op = permuteBudget N op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sign column”. Negate exactly the spare entry of each stored row.

noncomputable def signColumn {N : ℕ} (U : StoredMatrix N N) (spare : Fin N) :
    Run (StoredMatrix N N) :=
  collect fun row => do
    let values ← StoredGivens.read U row
    let old ← StoredGivens.read values spare
    let flipped ← StoredGivens.sub 0 old
    replace values spare flipped

commit-pinned source · Verso Blueprint panel

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

theorem signColumn_value {N : ℕ} (U : StoredMatrix N N) (spare : Fin N) :
    denote (signColumn U spare).value = denote U * RealIsometryCompletion.signFlip spare := by

commit-pinned source · Verso Blueprint panel

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

def signBudget (N : ℕ) : Cost := fun op =>
  N * tick .field op + (N * N + 4 * N) * tick .read op +
    (N * N + 2 * N) * tick .write op

commit-pinned source · Verso Blueprint panel

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

theorem signColumn_cost {N : ℕ} (U : StoredMatrix N N) (spare : Fin N) (op : Op) :
    (signColumn U spare).cost op = signBudget N op := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def placeColumns {N r : ℕ} (hr : r < N) (e : Positions N r)
    (U : StoredMatrix N N) : Run (StoredMatrix N N) := do
  let p ← permutation hr.le e r le_rfl
  let spare ← StoredGivens.read p.forward ⟨r, hr⟩
  let moved ← permuteColumns U p.inverse
  let positive ← charge .compare (decide (p.polarity = 1))
  if positive then pure moved else signColumn moved spare

commit-pinned source · Verso Blueprint panel

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

theorem placeColumns_value {N r : ℕ} (hr : r < N) (e : Positions N r)
    (U : StoredMatrix N N) :
    denote (placeColumns hr e U).value =
      ConstructiveIsometryCompletion.placeColumns hr e.embedding (denote U) := by

commit-pinned source · Verso Blueprint panel

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

def placeBudget (N r : ℕ) : Cost :=
  permutationBudget N r + tick .read + permuteBudget N + tick .compare + signBudget N

commit-pinned source · Verso Blueprint panel

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

theorem placeColumns_cost_le {N r : ℕ} (hr : r < N) (e : Positions N r)
    (U : StoredMatrix N N) (op : Op) :
    (placeColumns hr e U).cost op ≤ placeBudget N r op := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def complete {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) : Run (StoredMatrix N N) := do
  let base ← prefixCompletion V
  placeColumns hr e base

commit-pinned source · Verso Blueprint panel

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

theorem complete_value {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) :
    denote (complete hr V e).value =
      ConstructiveIsometryCompletion.complete hr (denote V) e.embedding := by

commit-pinned source · Verso Blueprint panel

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

def completeBudget (N r : ℕ) : Cost := prefixBudget N r + placeBudget N r

commit-pinned source · Verso Blueprint panel

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

theorem complete_cost_le {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) (op : Op) :
    (complete hr V e).cost op ≤ completeBudget N r op := by

commit-pinned source · Verso Blueprint panel

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

theorem complete_spec {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) (hV : (denote V).transpose * denote V = 1) :
    (denote (complete hr V e).value).transpose * denote (complete hr V e).value = 1 ∧
    (denote (complete hr V e).value).det = 1 ∧
    ∀ row a, denote (complete hr V e).value row (e.embedding a) = denote V row a := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “polynomial budget”. Expanded bound including the stored prefix matrix, both permutation tables, orientation tracking, column placement, and spare-column correction.

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

commit-pinned source · Verso Blueprint panel

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

theorem completeBudget_eq (N r : ℕ) : completeBudget N r = polynomialBudget N r := by

commit-pinned source · Verso Blueprint panel

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

theorem complete_polynomial_cost_le {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) (op : Op) :
    (complete hr V e).cost op ≤ polynomialBudget N r op := by

commit-pinned source · Verso Blueprint panel

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

theorem complete_total_cost_le {N r : ℕ} (hr : r < N) (V : StoredMatrix N r)
    (e : Positions N r) :
    StoredRectangularGivens.total (complete hr V e).cost ≤
      N * r * (22 * r + 30 * N + 43) + 20 * N * N + 27 * N + 5 * r + 3 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “complete from”. Source construction is composed as counted input producers, never an unpriced callback hidden inside the completion.

noncomputable def completeFrom {N r : ℕ} (hr : r < N)
    (active : Run (StoredMatrix N r)) (positions : Run (Positions N r)) :
    Run (StoredMatrix N N) := do
  let V ← active
  let e ← positions
  complete hr V e

commit-pinned source · Verso Blueprint panel

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

theorem completeFrom_value {N r : ℕ} (hr : r < N)
    (active : Run (StoredMatrix N r)) (positions : Run (Positions N r)) :
    denote (completeFrom hr active positions).value =
      ConstructiveIsometryCompletion.complete hr (denote active.value) positions.value.embedding := by

commit-pinned source · Verso Blueprint panel

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

theorem completeFrom_cost_le {N r : ℕ} (hr : r < N)
    (active : Run (StoredMatrix N r)) (positions : Run (Positions N r)) (op : Op) :
    (completeFrom hr active positions).cost op ≤
      active.cost op + positions.cost op + polynomialBudget N r op := by

commit-pinned source · Verso Blueprint panel