This record groups the data and proof fields needed for “primitive program refinement”. A proposition-valued field is a requirement until a constructor supplies it. Exact refinement for a primitive program, including its declared global phase.
structure PrimitiveProgramRefinement (qubits : Nat) where
program : PrimitiveProgram qubits
target : _root_.Matrix (PrimitiveBasis qubits) (PrimitiveBasis qubits) ℂ
exact : evalPrimitiveProgram program = target
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def PrimitiveProgramRefinement.resource {qubits : Nat}
(refinement : PrimitiveProgramRefinement qubits) : Resource :=
refinement.program.resource
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem PrimitiveProgramRefinement.oracleCalls_eq_zero {qubits : Nat}
(refinement : PrimitiveProgramRefinement qubits) :
refinement.resource.oracleCalls = 0 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def PrimitiveRefinement.resource {qubits : Nat}
(refinement : PrimitiveRefinement qubits) : Resource :=
refinement.circuit.resource
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem PrimitiveRefinement.oracleCalls_eq_zero {qubits : Nat}
(refinement : PrimitiveRefinement qubits) :
refinement.resource.oracleCalls = 0 := by
commit-pinned source · Verso Blueprint panel