This definition gives the library's named construction or computation for “selected ry angles”. One nonzero entry in a multiplexed angle table; all other branches are identity.
def selectedRyAngles {controls : Nat} (chosen : PrimitiveBasis controls)
(angle : ExactAngle) : PrimitiveBasis controls → ExactAngle :=
fun bits => if bits = chosen then angle else .rational 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile selected ry”.
def compileSelectedRy {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(chosen : PrimitiveBasis controls) (angle : ExactAngle) :
PrimitiveCircuit qubits :=
compileUniformlyControlledRy controls wires target distinct
(selectedRyAngles chosen angle)
/-- General block version, allowing unused passive wires. -/
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry eval block”; the hypotheses and conclusion in the code panel fix its exact scope. General block version, allowing unused passive wires.
theorem compileSelectedRy_eval_block {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(chosen : PrimitiveBasis controls) (angle : ExactAngle) :
evalPrimitiveCircuit (compileSelectedRy wires target distinct chosen angle) =
controlledRyBlockMatrix wires target distinct (selectedRyAngles chosen angle) :=
compileUniformlyControlledRy_eval_controlledRyBlockMatrix _ _ _ _
/-- The real matrix underlying the standard half-angle RY convention. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “real ry plane block”. The real matrix underlying the standard half-angle RY convention.
noncomputable def realRyPlaneBlock (theta : ℝ) :
_root_.Matrix (Fin 2) (Fin 2) ℝ :=
!![Real.cos (theta / 2), -Real.sin (theta / 2);
Real.sin (theta / 2), Real.cos (theta / 2)]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “standard ry matrix eq real ry plane block”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem standardRyMatrix_eq_realRyPlaneBlock (theta : ℝ) (row column : Fin 2) :
standardRyMatrix theta row column = (realRyPlaneBlock theta row column : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “real ry plane block zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem realRyPlaneBlock_zero : realRyPlaneBlock 0 = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “selected ry plane matrix”. A real two-level plane: the chosen pair is ordered by target bit 0, then 1.
noncomputable def selectedRyPlaneMatrix {qubits : Nat} (target : Fin qubits)
(chosen : OtherPrimitiveWires target → Fin 2) (theta : ℝ) :
_root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℝ :=
fun row column =>
if (splitPrimitiveWire target row).2 = chosen ∧
(splitPrimitiveWire target column).2 = chosen then
realRyPlaneBlock theta (row target) (column target)
else if row = column then 1 else 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive control assignment eq iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem primitiveControlAssignment_eq_iff {qubits controls : Nat}
(target : Fin qubits) (wires : Fin controls ≃ OtherPrimitiveWires target)
(rowContext chosen : OtherPrimitiveWires target → Fin 2) :
primitiveControlAssignment (fun index => (wires index).1) target
(fun index => (wires index).2) rowContext =
(fun index => chosen (wires index)) ↔ rowContext = chosen := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry eval plane”; the hypotheses and conclusion in the code panel fix its exact scope. Full-control specialization: an actual finite RY/CX circuit equals the complex embedding of the explicitly real two-level plane.
theorem compileSelectedRy_eval_plane {qubits controls : Nat}
(target : Fin qubits) (wires : Fin controls ≃ OtherPrimitiveWires target)
(chosen : OtherPrimitiveWires target → Fin 2) (angle : ExactAngle) :
evalPrimitiveCircuit
(compileSelectedRy (fun index => (wires index).1) target
(fun index => (wires index).2) (fun index => chosen (wires index)) angle) =
(selectedRyPlaneMatrix target chosen angle.eval).map Complex.ofReal := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “selected ry plane matrix fixed column”; the hypotheses and conclusion in the code panel fix its exact scope. Entry-level complement statement: no amplitude or phase is changed outside the selected pair.
theorem selectedRyPlaneMatrix_fixed_column {qubits : Nat} (target : Fin qubits)
(chosen : OtherPrimitiveWires target → Fin 2) (theta : ℝ)
(column : PrimitiveBasis qubits)
(outside : (splitPrimitiveWire target column).2 ≠ chosen)
(row : PrimitiveBasis qubits) :
selectedRyPlaneMatrix target chosen theta row column =
(1 : _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℝ) row column := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “selected ry plane matrix selected entry”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem selectedRyPlaneMatrix_selected_entry {qubits : Nat} (target : Fin qubits)
(chosen : OtherPrimitiveWires target → Fin 2) (theta : ℝ)
(rowBit columnBit : Fin 2) :
selectedRyPlaneMatrix target chosen theta
((splitPrimitiveWire target).symm (rowBit, chosen))
((splitPrimitiveWire target).symm (columnBit, chosen)) =
realRyPlaneBlock theta rowBit columnBit := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry ry count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRy_ryCount {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(chosen : PrimitiveBasis controls) (angle : ExactAngle) :
(compileSelectedRy wires target distinct chosen angle).ryCount = 2 ^ controls :=
compileUniformlyControlledRy_ryCount _ _ _ _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry cx count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRy_cxCount {qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(chosen : PrimitiveBasis controls) (angle : ExactAngle) :
(compileSelectedRy wires target distinct chosen angle).cxCount =
2 * (2 ^ controls - 1) :=
compileUniformlyControlledRy_cxCount _ _ _ _
/-- A concrete selected-rotation instruction, not an assumed target operator. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “selected ry step”. A proposition-valued field is a requirement until a constructor supplies it. A concrete selected-rotation instruction, not an assumed target operator.
structure SelectedRyStep (qubits controls : Nat) where
wires : Fin controls → Fin qubits
target : Fin qubits
distinct : ∀ control, wires control ≠ target
chosen : PrimitiveBasis controls
angle : ExactAngle
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile”.
def SelectedRyStep.compile {qubits controls : Nat}
(step : SelectedRyStep qubits controls) : PrimitiveCircuit qubits :=
compileSelectedRy step.wires step.target step.distinct step.chosen step.angle
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “matrix”.
noncomputable def SelectedRyStep.matrix {qubits controls : Nat}
(step : SelectedRyStep qubits controls) :
_root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ :=
controlledRyBlockMatrix step.wires step.target step.distinct
(selectedRyAngles step.chosen step.angle)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile selected ry steps”.
def compileSelectedRySteps {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) : PrimitiveCircuit qubits :=
steps.flatMap SelectedRyStep.compile
/-- Chronological product: the last listed stage multiplies on the left. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “selected ry steps matrix”. Chronological product: the last listed stage multiplies on the left.
noncomputable def selectedRyStepsMatrix {qubits controls : Nat} :
List (SelectedRyStep qubits controls) →
_root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
| [] => 1
| step :: rest => selectedRyStepsMatrix rest * step.matrix
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRySteps_eval {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) :
evalPrimitiveCircuit (compileSelectedRySteps steps) = selectedRyStepsMatrix steps := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps ry count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRySteps_ryCount {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) :
(compileSelectedRySteps steps).ryCount = steps.length * 2 ^ controls := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps cx count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRySteps_cxCount {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) :
(compileSelectedRySteps steps).cxCount = steps.length * (2 * (2 ^ controls - 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps no oracle”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRySteps_noOracle {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) :
(compileSelectedRySteps steps).resource.oracleCalls = 0 := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile uniformly controlled ry gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileUniformlyControlledRy_gateCount {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).gateCount =
2 ^ controls + 2 * (2 ^ controls - 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compileSelectedRySteps_gateCount {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) :
(compileSelectedRySteps steps).gateCount =
steps.length * (2 ^ controls + 2 * (2 ^ controls - 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile selected ry steps cubic bound”; the hypotheses and conclusion in the code panel fix its exact scope. Concrete cubic bound for a supplied finite list.
theorem compileSelectedRySteps_cubic_bound {qubits controls : Nat}
(steps : List (SelectedRyStep qubits controls)) (stages : Nat)
(lengthBound : steps.length ≤
stages * ((2 * 2 ^ controls) * (2 * 2 ^ controls - 1) / 2)) :
(compileSelectedRySteps steps).gateCount ≤ 6 * stages * (2 ^ controls) ^ 3 ∧
(compileSelectedRySteps steps).resource.oracleCalls = 0 := by
commit-pinned source · Verso Blueprint panel