This definition gives the library's named construction or computation for “eval primitive circuit le”.
noncomputable def evalPrimitiveCircuitLE {qubits : Nat}
(circuit : PrimitiveCircuit qubits) :
FiniteMatrix (gridSize qubits) (gridSize qubits) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv qubits)
(evalPrimitiveCircuit circuit)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval primitive circuit le unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem evalPrimitiveCircuitLE_unitary {qubits : Nat}
(circuit : PrimitiveCircuit qubits) :
evalPrimitiveCircuitLE circuit ∈
_root_.Matrix.unitaryGroup (Fin (gridSize qubits)) ℂ := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “exact primitive state preparation route”. A proposition-valued field is a requirement until a constructor supplies it.
structure ExactPrimitiveStatePreparationRoute (qubits : Nat) where
target : StatePreparationTarget ℂ qubits
circuit : PrimitiveCircuit qubits
normalizationProof : target.normalization
preparationProof :
applyVec (evalPrimitiveCircuitLE circuit) (zeroKet qubits) =
target.amplitudes
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “cost”.
def cost (route : ExactPrimitiveStatePreparationRoute qubits) :
BlockEncodingCost where
auxiliaryQubits := 0
gateCount := route.circuit.resource.gates
depth := route.circuit.resource.depth
oracleCalls := route.circuit.resource.oracleCalls
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem unitary (route : ExactPrimitiveStatePreparationRoute qubits) :
evalPrimitiveCircuitLE route.circuit ∈
_root_.Matrix.unitaryGroup (Fin (gridSize qubits)) ℂ :=
evalPrimitiveCircuitLE_unitary route.circuit
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ry angle 35”.
noncomputable def ryAngle35 : ExactAngle :=
.twiceArccosRational cosine35 (by
norm_num [cosine35, abs_of_nonneg])
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ry angle 513”.
noncomputable def ryAngle513 : ExactAngle :=
.twiceArccosRational cosine513 (by
norm_num [cosine513, abs_of_nonneg])
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ry angle zero”.
def ryAngleZero : ExactAngle := .rational 0
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “standard ry matrix ry angle 35”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem standardRyMatrix_ryAngle35 :
standardRyMatrix ryAngle35.eval =
realOrthogonalRotation (cosine35 : Real) (sine35 : Real) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “standard ry matrix ry angle 513”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem standardRyMatrix_ryAngle513 :
standardRyMatrix ryAngle513.eval =
realOrthogonalRotation (cosine513 : Real) (sine513 : Real) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “standard ry matrix ry angle zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem standardRyMatrix_ryAngleZero :
standardRyMatrix ryAngleZero.eval = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “primitive le bits”.
def primitiveLEBits (qubits : Nat) (index : Fin (gridSize qubits)) :
PrimitiveBasis qubits :=
(primitiveBasisLEEquiv qubits).symm index
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval primitive circuit le append”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem evalPrimitiveCircuitLE_append {qubits : Nat}
(left right : PrimitiveCircuit qubits) :
evalPrimitiveCircuitLE (left ++ right) =
evalPrimitiveCircuitLE right * evalPrimitiveCircuitLE left := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval primitive circuit le singleton ry apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem evalPrimitiveCircuitLE_singleton_ry_apply {qubits : Nat}
(target : Fin qubits) (angle : ExactAngle)
(row column : Fin (gridSize qubits)) :
evalPrimitiveCircuitLE ([PrimitiveGate.ry target angle]) row column =
if (splitPrimitiveWire target (primitiveLEBits qubits row)).2 =
(splitPrimitiveWire target (primitiveLEBits qubits column)).2 then
standardRyMatrix angle.eval
((primitiveLEBits qubits row) target)
((primitiveLEBits qubits column) target)
else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval primitive circuit le compile uniformly controlled ry apply”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem evalPrimitiveCircuitLE_compileUniformlyControlledRy_apply
{qubits controls : Nat}
(wires : Fin controls → Fin qubits) (target : Fin qubits)
(distinct : ∀ control, wires control ≠ target)
(angles : PrimitiveBasis controls → ExactAngle)
(row column : Fin (gridSize qubits)) :
evalPrimitiveCircuitLE
(compileUniformlyControlledRy controls wires target distinct angles)
row column =
if (splitPrimitiveWire target (primitiveLEBits qubits row)).2 =
(splitPrimitiveWire target (primitiveLEBits qubits column)).2 then
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph control wire”.
def groverRudolphControlWire : Fin 1 → Fin 2 := fun _ => 1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph control wire ne target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphControlWire_ne_target :
∀ control, groverRudolphControlWire control ≠ (0 : Fin 2) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph constant angles”.
noncomputable def groverRudolphConstantAngles (_ : PrimitiveBasis 1) : ExactAngle :=
ryAngle35
/-- Generic binary-tree route: a root split followed by a one-control UCRY. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph tree circuit”. Generic binary-tree route: a root split followed by a one-control UCRY.
noncomputable def groverRudolphTreeCircuit : PrimitiveCircuit 2 :=
[PrimitiveGate.ry (1 : Fin 2) ryAngle35] ++
compileUniformlyControlledRy 1 groverRudolphControlWire (0 : Fin 2)
groverRudolphControlWire_ne_target groverRudolphConstantAngles
/-- Product-aware route: the two independent rotations can occupy one layer. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph factorized circuit”. Product-aware route: the two independent rotations can occupy one layer.
noncomputable def groverRudolphFactorizedCircuit : PrimitiveCircuit 2 :=
[PrimitiveGate.ry (1 : Fin 2) ryAngle35] ++
[PrimitiveGate.ry (0 : Fin 2) ryAngle35]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph constant ucry eval”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphConstantUcry_eval :
evalPrimitiveCircuit
(compileUniformlyControlledRy 1 groverRudolphControlWire (0 : Fin 2)
groverRudolphControlWire_ne_target groverRudolphConstantAngles) =
evalPrimitiveGate (PrimitiveGate.ry (0 : Fin 2) ryAngle35) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph tree eval eq factorized”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphTree_eval_eq_factorized :
evalPrimitiveCircuit groverRudolphTreeCircuit =
evalPrimitiveCircuit groverRudolphFactorizedCircuit := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph tree eval le eq factorized”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphTree_evalLE_eq_factorized :
evalPrimitiveCircuitLE groverRudolphTreeCircuit =
evalPrimitiveCircuitLE groverRudolphFactorizedCircuit := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph factorized eval le eq matrix”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphFactorized_evalLE_eq_matrix :
evalPrimitiveCircuitLE groverRudolphFactorizedCircuit =
groverRudolphProductMatrix := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph factorized prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphFactorized_prepares_target :
applyVec (evalPrimitiveCircuitLE groverRudolphFactorizedCircuit) (zeroKet 2) =
groverRudolphProductTarget.amplitudes := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph tree prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphTree_prepares_target :
applyVec (evalPrimitiveCircuitLE groverRudolphTreeCircuit) (zeroKet 2) =
groverRudolphProductTarget.amplitudes := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph factorized route”.
noncomputable def groverRudolphFactorizedRoute :
ExactPrimitiveStatePreparationRoute 2 where
target := groverRudolphProductTarget
circuit := groverRudolphFactorizedCircuit
normalizationProof := groverRudolphProductTarget_normalized
preparationProof := groverRudolphFactorized_prepares_target
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “grover rudolph tree route”.
noncomputable def groverRudolphTreeRoute :
ExactPrimitiveStatePreparationRoute 2 where
target := groverRudolphProductTarget
circuit := groverRudolphTreeCircuit
normalizationProof := groverRudolphProductTarget_normalized
preparationProof := groverRudolphTree_prepares_target
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph factorized verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphFactorizedVerified_cost :
groverRudolphFactorizedRoute.cost =
{ auxiliaryQubits := 0, gateCount := 2, depth := 1, oracleCalls := 0 } := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph tree verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphTreeVerified_cost :
groverRudolphTreeRoute.cost =
{ auxiliaryQubits := 0, gateCount := 5, depth := 4, oracleCalls := 0 } := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “grover rudolph factorized better than tree”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem groverRudolphFactorized_betterThan_tree :
groverRudolphFactorizedRoute.cost.betterThan groverRudolphTreeRoute.cost := by
commit-pinned source · Verso Blueprint panel