This record groups the data and proof fields needed for “executable resource certificate”. A proposition-valued field is a requirement until a constructor supplies it. Backend-neutral cost evidence computed from the canonical primitive IR.
structure ExecutableResourceCertificate (qubits : Nat) where
program : PrimitiveProgram qubits
auxiliaryQubits : Nat
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource (certificate : ExecutableResourceCertificate qubits) : Resource :=
certificate.program.resource
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “cost”.
def cost (certificate : ExecutableResourceCertificate qubits) : BlockEncodingCost where
auxiliaryQubits := certificate.auxiliaryQubits
gateCount := certificate.resource.gates
depth := certificate.resource.depth
oracleCalls := certificate.resource.oracleCalls
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “resource eq program resource”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem resource_eq_program_resource
(certificate : ExecutableResourceCertificate qubits) :
certificate.resource = certificate.program.resource := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cost auxiliary qubits”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cost_auxiliaryQubits
(certificate : ExecutableResourceCertificate qubits) :
certificate.cost.auxiliaryQubits = certificate.auxiliaryQubits := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cost gate count”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cost_gateCount
(certificate : ExecutableResourceCertificate qubits) :
certificate.cost.gateCount = certificate.program.resource.gates := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cost depth”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cost_depth
(certificate : ExecutableResourceCertificate qubits) :
certificate.cost.depth = certificate.program.resource.depth := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cost oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cost_oracleCalls
(certificate : ExecutableResourceCertificate qubits) :
certificate.cost.oracleCalls = certificate.program.resource.oracleCalls := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “certify”. Promote a candidate only after all three state-preparation obligations are supplied.
def certify (candidate : StatePreparationCandidate α qubits)
(normalizationProof : candidate.target.normalization)
(unitaryProof : candidate.isUnitary)
(preparationProof : candidate.preparesTarget) :
VerifiedStatePreparation α qubits where
candidate := candidate
normalizationProof := normalizationProof
unitaryProof := unitaryProof
preparationProof := preparationProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “certify first column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem certify_firstColumn (candidate : StatePreparationCandidate α qubits)
(normalizationProof : candidate.target.normalization)
(unitaryProof : candidate.isUnitary)
(preparationProof : candidate.preparesTarget) :
(candidate.certify normalizationProof unitaryProof preparationProof).candidate.preparesTarget :=
preparationProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “certify unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem certify_unitary (candidate : StatePreparationCandidate α qubits)
(normalizationProof : candidate.target.normalization)
(unitaryProof : candidate.isUnitary)
(preparationProof : candidate.preparesTarget) :
(candidate.certify normalizationProof unitaryProof preparationProof).candidate.isUnitary :=
unitaryProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “certify normalization”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem certify_normalization (candidate : StatePreparationCandidate α qubits)
(normalizationProof : candidate.target.normalization)
(unitaryProof : candidate.isUnitary)
(preparationProof : candidate.preparesTarget) :
(candidate.certify normalizationProof unitaryProof preparationProof).candidate.target.normalization :=
normalizationProof
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “of first column”. Build concrete state-preparation evidence from the equivalent first-column statement.
def ofFirstColumn (target : StatePreparationTarget ℂ qubits)
(gate : ComplexUnitaryGate qubits)
(normalizationProof : target.normalization)
(firstColumnProof : FirstColumnMatches gate.matrix target) :
ComplexStatePreparationCertificate qubits where
target := target
gate := gate
normalizationProof := normalizationProof
preparationProof :=
(ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet gate.matrix target).mp
firstColumnProof
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “verified of first column”. Promote first-column evidence through the concrete finite-matrix backend.
def verifiedOfFirstColumn (target : StatePreparationTarget ℂ qubits)
(gate : ComplexUnitaryGate qubits)
(normalizationProof : target.normalization)
(firstColumnProof : FirstColumnMatches gate.matrix target)
(circuit : Circuit) (schedule : LayeredCircuit) (resource : Resource)
(auxiliaryQubits : Nat := 0) : VerifiedStatePreparation ℂ qubits :=
(ofFirstColumn target gate normalizationProof firstColumnProof).verified
circuit schedule resource auxiliaryQubits
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “verified of first column prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem verifiedOfFirstColumn_preparesTarget
(target : StatePreparationTarget ℂ qubits)
(gate : ComplexUnitaryGate qubits)
(normalizationProof : target.normalization)
(firstColumnProof : FirstColumnMatches gate.matrix target)
(circuit : Circuit) (schedule : LayeredCircuit) (resource : Resource)
(auxiliaryQubits : Nat := 0) :
(verifiedOfFirstColumn target gate normalizationProof firstColumnProof
circuit schedule resource auxiliaryQubits).candidate.preparesTarget :=
(verifiedOfFirstColumn target gate normalizationProof firstColumnProof
circuit schedule resource auxiliaryQubits).preparationProof
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “textbook pauli x verified of first column”. Finite witness that the generic first-column route reuses the Pauli-X proof.
def textbookPauliXVerifiedOfFirstColumn : VerifiedStatePreparation ℂ 1 :=
ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
TextbookStatePreparation.oneTarget TextbookStatePreparation.pauliXGate
TextbookStatePreparation.oneTarget_normalized
((ConcreteSemantics.firstColumnMatches_iff_applyVec_zeroKet
TextbookStatePreparation.pauliX TextbookStatePreparation.oneTarget).mpr
TextbookStatePreparation.pauliX_prepares_one)
TextbookStatePreparation.pauliXCircuit
[[Gate.oneQubit "X" 0]] TextbookStatePreparation.pauliXCircuit.resource
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “textbook pauli x verified of first column prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem textbookPauliXVerifiedOfFirstColumn_preparesTarget :
textbookPauliXVerifiedOfFirstColumn.candidate.preparesTarget :=
textbookPauliXVerifiedOfFirstColumn.preparationProof
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “exact clean block of signal projection”. Convert a signal-register projection proof into an exact clean-block certificate.
def exactCleanBlockOfSignalProjection {signalDim systemDim : Nat}
(operator : Matrix (signalDim * systemDim) (signalDim * systemDim) Rat)
(signalIndex : Fin signalDim)
(target : Matrix systemDim systemDim Rat)
(projectionProof :
Matrix.PointwiseEq
(signalSystemBlockProjection
signalDim systemDim systemDim operator signalIndex)
target) :
BlockEncodingClassics.ExactCleanBlock systemDim (signalDim * systemDim) where
U := operator
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “exact clean block of signal projection correct”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem exactCleanBlockOfSignalProjection_correct {signalDim systemDim : Nat}
(operator : Matrix (signalDim * systemDim) (signalDim * systemDim) Rat)
(signalIndex : Fin signalDim)
(target : Matrix systemDim systemDim Rat)
(projectionProof :
Matrix.PointwiseEq
(signalSystemBlockProjection
signalDim systemDim systemDim operator signalIndex)
target) :
Matrix.PointwiseEq
(exactCleanBlockOfSignalProjection operator signalIndex target projectionProof).clean
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “teaching identity circuit semantics”. Empty-circuit semantics on the one-dimensional zero-qubit space.
def teachingIdentityCircuitSemantics : CircuitMatrixSemantics Rat 0 :=
CircuitMatrixSemantics.ofGateMatrices [] [] rfl
/-- Finite witness for certified circuit block extraction. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “certify”. Promote an operator candidate only after its unitary and block proofs are supplied.
def certify (candidate : OperatorBlockEncodingCandidate α systemQubits)
(unitaryProof : candidate.isUnitary)
(blockProof : candidate.blockContainsTarget) :
VerifiedOperatorBlockEncoding α systemQubits where
candidate := candidate
unitaryProof := unitaryProof
blockProof := blockProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cost eq from layout and resource”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem cost_eq_fromLayoutAndResource
(candidate : OperatorBlockEncodingCandidate α systemQubits) :
candidate.cost =
BlockEncodingCost.fromLayoutAndResource candidate.layout candidate.resource := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “identity”. Degree-one identity consumer: a proved clean block is returned unchanged.
def identity (input : ExactCleanBlock system total) :
QSVTConsumerContract system total where
input := input
polynomialDescription := "p(x)=x; degree-one identity consumer"
sideConditions := True
outputStatement := Matrix.PointwiseEq input.clean input.A
sideConditionProof := trivial
outputProof := input.blockProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “identity side conditions”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem identity_sideConditions (input : ExactCleanBlock system total) :
(identity input).sideConditions :=
(identity input).sideConditionProof
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “identity output”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem identity_output (input : ExactCleanBlock system total) :
(identity input).outputStatement :=
(identity input).outputProof
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “teaching identity qsvt consumer”. Finite witness that a certified clean block crosses the typed QSVT boundary.
def teachingIdentityQSVTConsumer :
BlockEncodingClassics.QSVTConsumerContract 1 1 :=
BlockEncodingClassics.QSVTConsumerContract.identity
teachingIdentityBlockExtraction.exactCleanBlock
commit-pinned source · Verso Blueprint panel