QuantumBlockEncoding/SelectedRyTrace.lean

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

inductive Gate (qubits : Nat) where
  | ry (target : Fin qubits) (coefficient : Rat)
  | cx (control target : Fin qubits) (distinct : control ≠ target)
  deriving Repr

commit-pinned source · Verso Blueprint panel

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

def Gate.instantiate {qubits : Nat} (angle : ExactAngle) : Gate qubits → PrimitiveGate qubits
  | .ry target coefficient => .ry target (.scale coefficient angle)
  | .cx control target distinct => .cx control target distinct

commit-pinned source · Verso Blueprint panel

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

def instantiate {qubits : Nat} (angle : ExactAngle) (trace : List (Gate qubits)) :
    PrimitiveCircuit qubits := trace.map (Gate.instantiate angle)

/-- The supplied tuple order is the recursive control order. No dense data-state
amplitude table is needed: these coefficients concern only the local controls. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “compile”. The supplied tuple order is the recursive control order.

def compile {qubits : Nat} : (controls : Nat) →
    (wires : Fin controls → Fin qubits) → (target : Fin qubits) →
    (∀ control, wires control ≠ target) → (PrimitiveBasis controls → Rat) → List (Gate qubits)
  | 0, _, target, _, coefficients => [.ry target (coefficients fun i => Fin.elim0 i)]
  | controls + 1, wires, target, distinct, coefficients =>
      let tailWires := fun i : Fin controls => wires i.succ
      let tailDistinct := fun i : Fin controls => distinct i.succ
      let controlled := Gate.cx (wires 0) target (distinct 0)
      compile controls tailWires target tailDistinct
          (fun bits => (coefficients (Fin.cons 0 bits) + coefficients (Fin.cons 1 bits)) / 2) ++
        [controlled] ++

commit-pinned source · Verso Blueprint panel

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

theorem eval_congr {qubits controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (a b : PrimitiveBasis controls → ExactAngle) (h : ∀ bits, (a bits).eval = (b bits).eval) :
    evalPrimitiveCircuit (compileUniformlyControlledRy controls wires target distinct a) =
      evalPrimitiveCircuit (compileUniformlyControlledRy controls wires target distinct b) := 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 controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (coefficients : PrimitiveBasis controls → Rat) (angle : ExactAngle) :
    evalPrimitiveCircuit (instantiate angle (compile controls wires target distinct coefficients)) =
      evalPrimitiveCircuit (compileUniformlyControlledRy controls wires target distinct
        (fun bits => .scale (coefficients bits) angle)) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “selected”. A selected plane has one coefficient equal to one; all other controls select zero.

def selected {qubits controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (chosen : PrimitiveBasis controls) : List (Gate qubits) :=
  compile controls wires target distinct (fun bits => if bits = chosen then 1 else 0)

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 controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (chosen : PrimitiveBasis controls) (angle : ExactAngle) :
    evalPrimitiveCircuit (instantiate angle (selected wires target distinct chosen)) =
      evalPrimitiveCircuit (compileSelectedRy wires target distinct chosen angle) := 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 controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (coefficients : PrimitiveBasis controls → Rat) :
    (compile controls wires target distinct coefficients).length =
      2 ^ controls + 2 * (2 ^ controls - 1) := by

commit-pinned source · Verso Blueprint panel

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

theorem selected_gateCount {qubits controls : Nat} (wires : Fin controls → Fin qubits)
    (target : Fin qubits) (distinct : ∀ c, wires c ≠ target)
    (chosen : PrimitiveBasis controls) (angle : ExactAngle) :
    (instantiate angle (selected wires target distinct chosen)).gateCount =
      2 ^ controls + 2 * (2 ^ controls - 1) := by

commit-pinned source · Verso Blueprint panel