QuantumBlockEncoding/StoredSelectedRyTrace.lean

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

abbrev Coefficients (controls : Nat) := Vector Rat (2 ^ controls)

/-- The first recursive control selects the high half of the stored array. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “basis index”. The first recursive control selects the high half of the stored array.

def basisIndex : (controls : Nat) → PrimitiveBasis controls → Fin (2 ^ controls)
  | 0, _ => 0
  | q + 1, bits =>
    let rest := basisIndex q (fun i => bits i.succ)
    ⟨(bits 0).val * 2 ^ q + rest.val, by
      have hb := (bits 0).isLt
      have hr := rest.isLt
      simp only [pow_succ]
      nlinarith⟩

commit-pinned source · Verso Blueprint panel

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

def denote {q : Nat} (coefficients : Coefficients q) : PrimitiveBasis q → Rat :=
  fun bits => coefficients[(basisIndex q bits).val]

commit-pinned source · Verso Blueprint panel

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

def denoteBits {q : Nat} (bits : Vector (Fin 2) q) : PrimitiveBasis q :=
  fun i => bits[i.val]

commit-pinned source · Verso Blueprint panel

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

theorem basisIndex_injective (q : Nat) : Function.Injective (basisIndex q) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “tail”. Materialize a tail; persistent storage is not treated as a free view.

def tail {q : Nat} (xs : Vector α (q + 1)) : Run (Vector α q) :=
  collect fun i => read xs i.succ

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem tail_value {q : Nat} (xs : Vector α (q + 1)) (i : Fin q) :
    (tail xs).value[i.val] = xs[i.succ.val] := by

commit-pinned source · Verso Blueprint panel

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

theorem tail_cost {q : Nat} (xs : Vector α (q + 1)) (op : Op) :
    (tail xs).cost op = q * (3 * 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 “half add”.

def halfAdd (a b : Rat) : Run Rat := do
  let sum ← charge .field (a + b)
  charge .field (sum / 2)

commit-pinned source · Verso Blueprint panel

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

def halfSub (a b : Rat) : Run Rat := do
  let difference ← charge .field (a - b)
  charge .field (difference / 2)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem halfAdd_value (a b : Rat) : (halfAdd a b).value = (a + b) / 2 := rfl

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem halfSub_value (a b : Rat) : (halfSub a b).value = (a - b) / 2 := rfl

commit-pinned source · Verso Blueprint panel

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

theorem halfAdd_cost (a b : Rat) (op : Op) :
    (halfAdd a b).cost op = 2 * tick .field op := by

commit-pinned source · Verso Blueprint panel

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

theorem halfSub_cost (a b : Rat) (op : Op) :
    (halfSub a b).cost op = 2 * tick .field op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “split”. One read of each input coefficient feeds both charged half operations.

def split {q : Nat} (xs : Coefficients (q + 1)) :
    Run (Coefficients q × Coefficients q) := do
  let pairs ← collect fun i : Fin (2 ^ q) => do
    let a ← read xs ⟨i.val, by have := i.isLt; simp only [pow_succ]; omega⟩
    let b ← read xs ⟨2 ^ q + i.val, by have := i.isLt; simp only [pow_succ]; omega⟩
    let plus ← halfAdd a b
    let minus ← halfSub a b
    pure (plus, minus)
  let plus ← collect fun i => do
    let pair ← read pairs i
    pure pair.1

commit-pinned source · Verso Blueprint panel

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

theorem split_value {q : Nat} (xs : Coefficients (q + 1)) :
    denote (split xs).value.1 =
        (fun bits => (denote xs (Fin.cons 0 bits) + denote xs (Fin.cons 1 bits)) / 2) ∧
    denote (split xs).value.2 =
        (fun bits => (denote xs (Fin.cons 0 bits) - denote xs (Fin.cons 1 bits)) / 2) := by

commit-pinned source · Verso Blueprint panel

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

theorem split_cost {q : Nat} (xs : Coefficients (q + 1)) (op : Op) :
    (split xs).cost op =
      2 ^ q * (4 * tick .field op + 10 * tick .read op + 6 * tick .write op) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “append”. A real recursive persistent append: inspect each node and copy each nonempty prefix node.

def append : List α → List α → Run (List α)
  | [], ys => charge .read ys
  | x :: xs, ys =>
    let rest := append xs ys
    ⟨x :: rest.value, tick .read + rest.cost + tick .write⟩

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.

@[simp] theorem append_value (xs ys : List α) : (append xs ys).value = xs ++ ys := 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 (xs ys : List α) (op : Op) :
    (append xs ys).cost op =
      (xs.length + 1) * tick .read op + xs.length * tick .write op := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “emit”. Emission and the list-cell write are both charged.

def emit {qubits : Nat} (gate : SelectedRyTrace.Gate qubits)
    (rest : List (SelectedRyTrace.Gate qubits)) : Run (List (SelectedRyTrace.Gate qubits)) := do
  let gate ← charge .emit gate
  charge .write (gate :: rest)

commit-pinned source · Verso Blueprint panel

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

@[simp] theorem emit_value {qubits : Nat} (gate : SelectedRyTrace.Gate qubits) (rest) :
    (emit gate rest).value = gate :: rest := rfl

commit-pinned source · Verso Blueprint panel

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

theorem emit_cost {qubits : Nat} (gate : SelectedRyTrace.Gate qubits) (rest) (op : Op) :
    (emit gate rest).cost op = tick .emit op + tick .write op := rfl

/-- The actual recursive stored producer. The two append traversals copy
only the two recursively emitted prefixes, not an already assembled trace. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile”. The actual recursive stored producer.

def compile {qubits : Nat} : (q : Nat) →
    (wires : Vector (Fin qubits) q) → (target : Fin qubits) →
    (∀ i : Fin q, wires[i.val] ≠ target) → Coefficients q →
    Run (List (SelectedRyTrace.Gate qubits))
  | 0, _, target, _, xs => do
    let coefficient ← read xs 0
    emit (.ry target coefficient) []
  | q + 1, wires, target, distinct, xs =>
    let halves := split xs
    let tailWires := tail wires
    let control := StoredGivens.read wires 0

commit-pinned source · Verso Blueprint panel

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

theorem compile_value {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) :
    (compile q wires target distinct xs).value =
      SelectedRyTrace.compile q (fun i => wires[i.val]) target distinct (denote xs) := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_length {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) :
    (compile q wires target distinct xs).value.length =
      2 ^ q + 2 * (2 ^ q - 1) := by

commit-pinned source · Verso Blueprint panel

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

theorem compile_refines {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) (angle : ExactAngle) :
    evalPrimitiveCircuit (SelectedRyTrace.instantiate angle (compile q wires target distinct xs).value) =
      evalPrimitiveCircuit (compileUniformlyControlledRy q (fun i => wires[i.val]) target distinct
        (fun bits => .scale (denote xs bits) angle)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “trace cost”. This recurrence describes the charged algorithm, including both append traversals and materialization of the control-wire tail at every node.

def traceCost : Nat → Cost
  | 0 => tick .read + tick .write + tick .emit
  | q + 1 => fun op =>
    2 * traceCost q op +
    2 ^ q * (4 * tick .field op + 10 * tick .read op + 6 * tick .write op) +
    q * (3 * tick .read op + 2 * tick .write op) + tick .read op +
    2 * (tick .emit op + tick .write op) +
    2 * ((2 ^ q + 2 * (2 ^ q - 1) + 1) * tick .read op +
      (2 ^ q + 2 * (2 ^ q - 1)) * tick .write op)

commit-pinned source · Verso Blueprint panel

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

theorem compile_cost {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) (op : Op) :
    (compile q wires target distinct xs).cost op = traceCost q op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “trace cost fields”; the hypotheses and conclusion in the code panel fix its exact scope. Exact component counts, written additively to avoid truncated subtraction.

theorem traceCost_fields (q : Nat) :
    traceCost q .field = 2 * q * 2 ^ q ∧
    traceCost q .read + 3 * q + 2 = (8 * q + 3) * 2 ^ q ∧
    traceCost q .write + 2 * q = (6 * q + 1) * 2 ^ q ∧
    traceCost q .emit + 2 = 3 * 2 ^ q := by

commit-pinned source · Verso Blueprint panel

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

theorem traceCost_unused (q : Nat) :
    traceCost q .sqrt = 0 ∧ traceCost q .angle = 0 ∧
    traceCost q .trig = 0 ∧ traceCost q .compare = 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “compile emit”; the hypotheses and conclusion in the code panel fix its exact scope. All instructions, including zero-coefficient rotations, are emitted.

theorem compile_emit {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) :
    (compile q wires target distinct xs).cost .emit =
      (compile q wires target distinct xs).value.length := by

commit-pinned source · Verso Blueprint panel

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

theorem traceCost_total (q : Nat) :
    StoredRectangularGivens.total (traceCost q) + 5 * q + 4 = (16 * q + 7) * 2 ^ q := by

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. Polynomial in the local table size 'S = 2^q' and control count 'q'.

theorem compile_total_cost_le {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (xs : Coefficients q) :
    StoredRectangularGivens.total (compile q wires target distinct xs).cost ≤
      (16 * q + 7) * 2 ^ q := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “join index”. Two explicit index-word operations, locally charged under the field tag.

def joinIndex {q : Nat} (bit : Fin 2) (rest : Fin (2 ^ q)) : Run (Fin (2 ^ (q + 1))) :=
  let offset := charge .field (bit.val * 2 ^ q)
  let joined := charge .field (offset.value + rest.val)
  ⟨⟨joined.value, by
    have hb := bit.isLt
    have hr := rest.isLt
    dsimp [joined, offset, charge]
    simp only [pow_succ]
    nlinarith⟩, offset.cost + joined.cost⟩

/-- Convert a stored bit pattern to its array address, with charged tail copies. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “encode”. Convert a stored bit pattern to its array address, with charged tail copies.

def encode : (q : Nat) → Vector (Fin 2) q → Run (Fin (2 ^ q))
  | 0, _ => pure 0
  | q + 1, bits =>
    let first := StoredGivens.read bits 0
    let rest := tail bits
    let address := encode q rest.value
    let joined := joinIndex first.value address.value
    ⟨joined.value, first.cost + rest.cost + address.cost + joined.cost⟩

commit-pinned source · Verso Blueprint panel

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

theorem encode_value {q : Nat} (bits : Vector (Fin 2) q) :
    (encode q bits).value = basisIndex q (denoteBits bits) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “encoding index operations”. Independent index-operation count; these are the extra local field-tag charges and do not change any existing real/rational field-cost theorem.

def encodingIndexOperations (q : Nat) : Nat := 2 * q

commit-pinned source · Verso Blueprint panel

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

def encodingCost : Nat → Cost
  | 0 => 0
  | q + 1 => fun op => encodingCost q op + 2 * tick .field op +
    (3 * q + 1) * tick .read op + 2 * q * tick .write op

commit-pinned source · Verso Blueprint panel

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

theorem encode_cost {q : Nat} (bits : Vector (Fin 2) q) (op : Op) :
    (encode q bits).cost op = encodingCost q op := by

commit-pinned source · Verso Blueprint panel

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

theorem encode_index_operations {q : Nat} (bits : Vector (Fin 2) q) :
    (encode q bits).cost .field = encodingIndexOperations q := by

commit-pinned source · Verso Blueprint panel

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

theorem encodingCost_bound (q : Nat) (op : Op) :
    encodingCost q op ≤ q * (2 * tick .field op +
      (3 * q + 1) * tick .read op + 2 * q * tick .write op) := by

commit-pinned source · Verso Blueprint panel

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

def oneHot {q : Nat} (chosen : Fin (2 ^ q)) : Run (Coefficients q) :=
  collect fun i => charge .compare (if i = chosen then 1 else 0)

commit-pinned source · Verso Blueprint panel

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

theorem oneHot_value {q : Nat} (chosen : Fin (2 ^ q)) :
    denote (oneHot chosen).value = (fun bits => if basisIndex q bits = chosen then 1 else 0) := by

commit-pinned source · Verso Blueprint panel

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

theorem oneHot_cost {q : Nat} (chosen : Fin (2 ^ q)) (op : Op) :
    (oneHot chosen).cost op =
      2 ^ q * (tick .compare op + 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 “selected coefficients”.

def selectedCoefficients {q : Nat} (chosen : Vector (Fin 2) q) : Run (Coefficients q) := do
  let address ← encode q chosen
  oneHot address

commit-pinned source · Verso Blueprint panel

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

theorem selectedCoefficients_value {q : Nat} (chosen : Vector (Fin 2) q) :
    denote (selectedCoefficients chosen).value =
      (fun bits => if bits = denoteBits chosen then 1 else 0) := by

commit-pinned source · Verso Blueprint panel

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

def selected {qubits q : Nat} (wires : Vector (Fin qubits) q) (target : Fin qubits)
    (distinct : ∀ i : Fin q, wires[i.val] ≠ target) (chosen : Vector (Fin 2) q) :
    Run (List (SelectedRyTrace.Gate qubits)) := do
  let coefficients ← selectedCoefficients chosen
  compile q wires target distinct coefficients

commit-pinned source · Verso Blueprint panel

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

theorem selected_value {qubits q : Nat} (wires : Vector (Fin qubits) q) (target : Fin qubits)
    (distinct : ∀ i : Fin q, wires[i.val] ≠ target) (chosen : Vector (Fin 2) q) :
    (selected wires target distinct chosen).value =
      SelectedRyTrace.selected (fun i => wires[i.val]) target distinct (denoteBits chosen) := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_refines {qubits q : Nat} (wires : Vector (Fin qubits) q) (target : Fin qubits)
    (distinct : ∀ i : Fin q, wires[i.val] ≠ target) (chosen : Vector (Fin 2) q) (angle : ExactAngle) :
    evalPrimitiveCircuit (SelectedRyTrace.instantiate angle (selected wires target distinct chosen).value) =
      evalPrimitiveCircuit (compileSelectedRy (fun i => wires[i.val]) target distinct
        (denoteBits chosen) angle) := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_cost {qubits q : Nat} (wires : Vector (Fin qubits) q) (target : Fin qubits)
    (distinct : ∀ i : Fin q, wires[i.val] ≠ target) (chosen : Vector (Fin 2) q) (op : Op) :
    (selected wires target distinct chosen).cost op = encodingCost q op +
      2 ^ q * (tick .compare op + 2 * tick .read op + 2 * tick .write op) + traceCost q op := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “selected field tag split”; the hypotheses and conclusion in the code panel fix its exact scope. The local field-tag overcount is exposed separately from rational work.

theorem selected_field_tag_split {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (chosen : Vector (Fin 2) q) :
    (selected wires target distinct chosen).cost .field =
      2 * q * 2 ^ q + encodingIndexOperations q := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_length {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (chosen : Vector (Fin 2) q) :
    (selected wires target distinct chosen).value.length =
      2 ^ q + 2 * (2 ^ q - 1) := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_emit {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (chosen : Vector (Fin 2) q) :
    (selected wires target distinct chosen).cost .emit =
      (selected wires target distinct chosen).value.length := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_total_cost_le {qubits q : Nat} (wires : Vector (Fin qubits) q)
    (target : Fin qubits) (distinct : ∀ i : Fin q, wires[i.val] ≠ target)
    (chosen : Vector (Fin 2) q) :
    StoredRectangularGivens.total (selected wires target distinct chosen).cost ≤
      (16 * q + 12) * 2 ^ q + 5 * q ^ 2 + 3 * q := by

commit-pinned source · Verso Blueprint panel