This definition gives the library's named construction or computation for “primitive control assignment”.
def primitiveControlAssignment {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(context : OtherPrimitiveWires target → Fin 2) : PrimitiveBasis controls :=
fun control => context ⟨wires control, distinct control⟩
/-- Backend-independent specification: each fixed assignment of the non-target
wires owns one exact two-dimensional RY block selected by the control bits. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “controlled ry block matrix”. Backend-independent specification: each fixed assignment of the non-target wires owns one exact two-dimensional RY block selected by the control bits.
noncomputable def controlledRyBlockMatrix {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
_root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (splitPrimitiveWire target).symm
(_root_.Matrix.blockDiagonal fun context =>
standardRyMatrix (angles (primitiveControlAssignment wires target distinct context)).eval)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “controlled ry block matrix apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem controlledRyBlockMatrix_apply {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle)
(row column : PrimitiveBasis qubits) :
controlledRyBlockMatrix wires target distinct angles row column =
if (splitPrimitiveWire target row).2 =
(splitPrimitiveWire target column).2 then
standardRyMatrix
(angles (primitiveControlAssignment wires target distinct
(splitPrimitiveWire target row).2)).eval
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile uniformly controlled ry”. Reference recursive compiler.
def compileUniformlyControlledRy {qubits : Nat} :
(controls : Nat) →
(wires : Fin controls → Fin qubits) →
(target : Fin qubits) →
(∀ control, wires control ≠ target) →
(PrimitiveBasis controls → ExactAngle) →
PrimitiveCircuit qubits
| 0, _, target, _, angles =>
[.ry target (angles fun index => Fin.elim0 index)]
| controls + 1, wires, target, distinct, angles =>
let head := wires 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “uniformly controlled ry matrix”. Recursive matrix specification corresponding to the standard multiplexor identity.
noncomputable def uniformlyControlledRyMatrix {qubits : Nat} :
(controls : Nat) →
(wires : Fin controls → Fin qubits) →
(target : Fin qubits) →
(∀ control, wires control ≠ target) →
(PrimitiveBasis controls → ExactAngle) →
_root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
| 0, _, target, _, angles =>
evalPrimitiveGate (.ry target (angles fun index => Fin.elim0 index))
| controls + 1, wires, target, distinct, angles =>
let head := wires 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileUniformlyControlledRy_eval {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
evalPrimitiveCircuit
(compileUniformlyControlledRy controls wires target distinct angles) =
uniformlyControlledRyMatrix controls wires target distinct angles := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry eval controlled ry block matrix”; the hypotheses and conclusion in the code panel fix its exact scope. The recursive compiler satisfies the independent block-diagonal specification selected by the computational-basis controls.
theorem compileUniformlyControlledRy_eval_controlledRyBlockMatrix
{qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
evalPrimitiveCircuit
(compileUniformlyControlledRy controls wires target distinct angles) =
controlledRyBlockMatrix wires target distinct angles := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry ry count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileUniformlyControlledRy_ryCount {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
(compileUniformlyControlledRy controls wires target distinct angles).ryCount =
2 ^ controls := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry cx count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileUniformlyControlledRy_cxCount {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
(compileUniformlyControlledRy controls wires target distinct angles).cxCount =
2 * (2 ^ controls - 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileUniformlyControlledRy_oracleCalls_eq_zero
{qubits controls : Nat} (wires : Fin controls → Fin qubits)
(target : Fin qubits) (distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle) :
(compileUniformlyControlledRy controls wires target distinct angles).resource.oracleCalls = 0 :=
PrimitiveCircuit.resource_oracleCalls_eq_zero _
/-- Frozen Robin reference count: five controls require 32 RY and 62 CX. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry five control counts”; the hypotheses and conclusion in the code panel fix its exact scope. Frozen Robin reference count: five controls require 32 RY and 62 CX.
theorem compileUniformlyControlledRy_five_control_counts
{qubits : Nat} (wires : Fin 5 → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis 5 → ExactAngle) :
(compileUniformlyControlledRy 5 wires target distinct angles).ryCount = 32 ∧
(compileUniformlyControlledRy 5 wires target distinct angles).cxCount = 62 := by
commit-pinned source · Verso Blueprint panel