QuantumBlockEncoding/StatePreparation.lean

This definition gives the library's named construction or computation for “zero basis index”. The computational all-zero basis index in an 'n'-qubit register.

def zeroBasisIndex (n : Nat) : Fin (gridSize n) :=
  ⟨0, Nat.pow_pos (by decide)⟩

/-- A normalized state requested by the user. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “state preparation target”. A proposition-valued field is a requirement until a constructor supplies it. A normalized state requested by the user.

structure StatePreparationTarget (α : Type u) (qubits : Nat) where
  amplitudes : Fin (gridSize qubits) → α
  normalization : Prop
  source : String := ""

/-- The matrix-level first-column acceptance predicate. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “first column matches”. The matrix-level first-column acceptance predicate.

def FirstColumnMatches {α : Type u} {qubits : Nat}
    (unitary : Matrix (gridSize qubits) (gridSize qubits) α)
    (target : StatePreparationTarget α qubits) : Prop :=
  ∀ row, unitary row (zeroBasisIndex qubits) = target.amplitudes row

/-- A state-preparation candidate before semantic proofs are attached. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “state preparation candidate”. A proposition-valued field is a requirement until a constructor supplies it. A state-preparation candidate before semantic proofs are attached.

structure StatePreparationCandidate (α : Type u) (qubits : Nat) where
  target : StatePreparationTarget α qubits
  unitary : Matrix (gridSize qubits) (gridSize qubits) α
  circuit : Circuit
  schedule : LayeredCircuit := []
  resource : Resource
  auxiliaryQubits : Nat := 0
  isUnitary : Prop

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “prepares target”. The candidate's fixed semantic target; callers cannot replace it by a flag.

def preparesTarget (candidate : StatePreparationCandidate α qubits) : Prop :=
  FirstColumnMatches candidate.unitary candidate.target

/-- Reuse the block-encoding resource order for state-preparation candidates. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “cost”. Reuse the block-encoding resource order for state-preparation candidates.

def cost (candidate : StatePreparationCandidate α qubits) : BlockEncodingCost :=
  {
    auxiliaryQubits := candidate.auxiliaryQubits
    gateCount := candidate.resource.gates
    depth := candidate.resource.depth
    oracleCalls := candidate.resource.oracleCalls
  }

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “verified state preparation”. A proposition-valued field is a requirement until a constructor supplies it. A candidate promoted by proofs of normalization, unitarity, and state action.

structure VerifiedStatePreparation (α : Type u) (qubits : Nat) where
  candidate : StatePreparationCandidate α qubits
  normalizationProof : candidate.target.normalization
  unitaryProof : candidate.isUnitary
  preparationProof : candidate.preparesTarget

/-- An approximate candidate with a backend-specific state-error predicate. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “approximate state preparation candidate”. A proposition-valued field is a requirement until a constructor supplies it. An approximate candidate with a backend-specific state-error predicate.

structure ApproximateStatePreparationCandidate
    (α : Type u) (qubits : Nat) where
  candidate : StatePreparationCandidate α qubits
  epsilon : α
  approximationBound : Prop

/-- A verified approximate state-preparation certificate. -/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “verified approximate state preparation”. A proposition-valued field is a requirement until a constructor supplies it. A verified approximate state-preparation certificate.

structure VerifiedApproximateStatePreparation
    (α : Type u) (qubits : Nat) where
  approxCandidate : ApproximateStatePreparationCandidate α qubits
  normalizationProof : approxCandidate.candidate.target.normalization
  unitaryProof : approxCandidate.candidate.isUnitary
  approximationProof : approxCandidate.approximationBound

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “as zero error approx”. Package an exact state-preparation certificate as a zero-error approximate certificate when the backend uses the exact first-column predicate as its zero-error proposition.

def asZeroErrorApprox [OfNat α 0]
    (verified : VerifiedStatePreparation α qubits) :
    VerifiedApproximateStatePreparation α qubits where
  approxCandidate := {
    candidate := verified.candidate
    epsilon := 0
    approximationBound := verified.candidate.preparesTarget
  }
  normalizationProof := verified.normalizationProof
  unitaryProof := verified.unitaryProof
  approximationProof := verified.preparationProof

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “first column”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem firstColumn
    (verified : VerifiedStatePreparation α qubits) :
    verified.candidate.preparesTarget :=
  verified.preparationProof

commit-pinned source · Verso Blueprint panel