QuantumBlockEncoding/ConcreteSemantics.lean

This abbreviation gives a shorter name to the type or expression used for “finite matrix”. A Mathlib finite matrix, definitionally compatible with ABEIS 'Matrix'.

abbrev FiniteMatrix (rows cols : Nat) (α : Type u) :=
  _root_.Matrix (Fin rows) (Fin cols) α

/-- A finite column vector. -/

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “state vector”. A finite column vector.

abbrev StateVector (dimension : Nat) (α : Type u) :=
  Fin dimension -> α

/-- A computational-basis ket in the concrete finite backend. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “basis ket”. A computational-basis ket in the concrete finite backend.

def basisKet (dimension : Nat) {α : Type u} [Zero α] [One α]
    (index : Fin dimension) : StateVector dimension α :=
  Pi.single index 1

/-- The all-zero computational-basis ket for an `n`-qubit register. -/

commit-pinned source · Verso Blueprint panel

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

def zeroKet (qubits : Nat) {α : Type u} [Zero α] [One α] :
    StateVector (gridSize qubits) α :=
  basisKet (gridSize qubits) (zeroBasisIndex qubits)

/-- Matrix-vector action using Mathlib's finite sum semantics. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “apply vec”. Matrix-vector action using Mathlib's finite sum semantics.

def applyVec {rows cols : Nat} {α : Type u} [NonUnitalNonAssocSemiring α]
    (operator : FiniteMatrix rows cols α) (state : StateVector cols α) :
    StateVector rows α :=
  operator.mulVec state

/--
A finite complex gate whose unitarity is the standard Mathlib unitary-group
predicate rather than an unconstrained proposition.
-/

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “complex unitary gate”. A proposition-valued field is a requirement until a constructor supplies it. A finite complex gate whose unitarity is the standard Mathlib unitary-group predicate rather than an unconstrained proposition.

structure ComplexUnitaryGate (qubits : Nat) where
  matrix : FiniteMatrix (gridSize qubits) (gridSize qubits) ℂ
  unitary :
    matrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize qubits)) ℂ

/-- Acting on a basis ket selects the corresponding matrix column. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “apply vec basis ket”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on a basis ket selects the corresponding matrix column.

@[simp] theorem applyVec_basisKet {rows cols : Nat} {α : Type u}
    [NonAssocSemiring α] (operator : FiniteMatrix rows cols α)
    (index : Fin cols) :
    applyVec operator (basisKet cols index) = operator.col index := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “apply vec zero ket”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on the all-zero ket selects column zero.

@[simp] theorem applyVec_zeroKet {α : Type u} [NonAssocSemiring α]
    {qubits : Nat}
    (operator : FiniteMatrix (gridSize qubits) (gridSize qubits) α) :
    applyVec operator (zeroKet qubits) =
      operator.col (zeroBasisIndex qubits) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “first column matches iff apply vec zero ket”; the hypotheses and conclusion in the code panel fix its exact scope. The ABEIS first-column contract is exactly the state-action equation 'U |0^n> = |psi>' in the concrete finite matrix backend.

theorem firstColumnMatches_iff_applyVec_zeroKet
    {α : Type u} [NonAssocSemiring α] {qubits : Nat}
    (operator : Matrix (gridSize qubits) (gridSize qubits) α)
    (target : StatePreparationTarget α qubits) :
    FirstColumnMatches operator target ↔
      applyVec operator (zeroKet qubits) = target.amplitudes := by

commit-pinned source · Verso Blueprint panel

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

structure ComplexStatePreparationCertificate (qubits : Nat) where
  target : StatePreparationTarget ℂ qubits
  gate : ComplexUnitaryGate qubits
  normalizationProof : target.normalization
  preparationProof :
    applyVec gate.matrix (zeroKet qubits) = target.amplitudes

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “candidate”. Repackage concrete semantics in the existing generic candidate interface.

def candidate (certificate : ComplexStatePreparationCertificate qubits)
    (circuit : Circuit) (schedule : LayeredCircuit) (resource : Resource)
    (auxiliaryQubits : Nat := 0) :
    StatePreparationCandidate ℂ qubits where
  target := certificate.target
  unitary := certificate.gate.matrix
  circuit := circuit
  schedule := schedule
  resource := resource
  auxiliaryQubits := auxiliaryQubits
  isUnitary :=

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “verified”. Promote a concrete certificate to the existing verified wrapper.

def verified (certificate : ComplexStatePreparationCertificate qubits)
    (circuit : Circuit) (schedule : LayeredCircuit) (resource : Resource)
    (auxiliaryQubits : Nat := 0) :
    VerifiedStatePreparation ℂ qubits where
  candidate :=
    certificate.candidate circuit schedule resource auxiliaryQubits
  normalizationProof := certificate.normalizationProof
  unitaryProof := certificate.gate.unitary
  preparationProof :=
    (firstColumnMatches_iff_applyVec_zeroKet
      certificate.gate.matrix certificate.target).mpr

commit-pinned source · Verso Blueprint panel

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

theorem preparesVector (certificate : ComplexStatePreparationCertificate qubits) :
    applyVec certificate.gate.matrix (zeroKet qubits) =
      certificate.target.amplitudes :=
  certificate.preparationProof

commit-pinned source · Verso Blueprint panel

This abbreviation gives a shorter name to the type or expression used for “product register matrix”. A matrix indexed by an explicit signal-register/system-register product.

abbrev ProductRegisterMatrix (signalDim rows cols : Nat) (α : Type u) :=
  (Fin signalDim × Fin rows) -> (Fin signalDim × Fin cols) -> α

/--
View a flattened signal-system matrix through explicit product-register
indices.  The signal register is high-order and the system register low-order.
-/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “flat to product register”. View a flattened signal-system matrix through explicit product-register indices.

def flatToProductRegister {signalDim rows cols : Nat} {α : Type u}
    (operator : Matrix (signalDim * rows) (signalDim * cols) α) :
    ProductRegisterMatrix signalDim rows cols α :=
  fun row col =>
    operator
      ⟨signalSystemBlockRowIndex rows row.1.val row.2.val,
        signalSystemBlockRowIndex_lt row.1 row.2⟩
      ⟨signalSystemBlockColIndex cols col.1.val col.2.val,
        signalSystemBlockColIndex_lt col.1 col.2⟩

/-- Project one signal branch from an explicit product-register matrix. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “product register block projection”. Project one signal branch from an explicit product-register matrix.

def productRegisterBlockProjection {signalDim rows cols : Nat} {α : Type u}
    (operator : ProductRegisterMatrix signalDim rows cols α)
    (signalIndex : Fin signalDim) : Matrix rows cols α :=
  fun row col => operator (signalIndex, row) (signalIndex, col)

/--
Product-register projection after viewing a flat matrix is definitionally the
existing ABEIS flattened block projection.
-/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “product register block projection flat to product register”; the hypotheses and conclusion in the code panel fix its exact scope. Product-register projection after viewing a flat matrix is definitionally the existing ABEIS flattened block projection.

theorem productRegisterBlockProjection_flatToProductRegister
    {signalDim rows cols : Nat} {α : Type u} [OfNat α 0]
    (operator : Matrix (signalDim * rows) (signalDim * cols) α)
    (signalIndex : Fin signalDim) :
    productRegisterBlockProjection
        (flatToProductRegister operator) signalIndex =
      signalSystemBlockProjection signalDim rows cols operator signalIndex := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “product index val eq signal system block row index”; the hypotheses and conclusion in the code panel fix its exact scope. The classic product index and circuit-semantics row index have the same value.

theorem productIndex_val_eq_signalSystemBlockRowIndex
    {signalDim systemDim : Nat}
    (signalIndex : Fin signalDim) (systemIndex : Fin systemDim) :
    (BlockEncodingClassics.productIndex signalIndex systemIndex).val =
      signalSystemBlockRowIndex
        systemDim signalIndex.val systemIndex.val := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “signal system block projection eq clean block product”; the hypotheses and conclusion in the code panel fix its exact scope. The classic rational clean block and the generic circuit-semantics projection are the same pointwise matrix under the shared register order.

theorem signalSystemBlockProjection_eq_cleanBlockProduct
    {signalDim systemDim : Nat}
    (operator : Matrix (signalDim * systemDim) (signalDim * systemDim) Rat)
    (signalIndex : Fin signalDim) :
    Matrix.PointwiseEq
      (signalSystemBlockProjection
        signalDim systemDim systemDim operator signalIndex)
      (BlockEncodingClassics.cleanBlockProduct signalIndex operator) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “clean basis action amplitude”. The clean output amplitude obtained by applying 'operator' to a clean signal-system basis input.

def cleanBasisActionAmplitude {signalDim systemDim : Nat} {α : Type u}
    [NonAssocSemiring α]
    (operator : FiniteMatrix (signalDim * systemDim) (signalDim * systemDim) α)
    (signalIndex : Fin signalDim) (output input : Fin systemDim) : α :=
  applyVec operator
    (basisKet (signalDim * systemDim)
      (BlockEncodingClassics.productIndex signalIndex input))
    (BlockEncodingClassics.productIndex signalIndex output)

/-- Acting on a clean basis input and reading a clean output is one projected-block entry. -/

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “clean basis action amplitude eq signal system block projection”; the hypotheses and conclusion in the code panel fix its exact scope. Acting on a clean basis input and reading a clean output is one projected-block entry.

theorem cleanBasisActionAmplitude_eq_signalSystemBlockProjection
    {signalDim systemDim : Nat} {α : Type u} [NonAssocSemiring α]
    (operator : FiniteMatrix (signalDim * systemDim) (signalDim * systemDim) α)
    (signalIndex : Fin signalDim) (output input : Fin systemDim) :
    cleanBasisActionAmplitude operator signalIndex output input =
      signalSystemBlockProjection signalDim systemDim systemDim
        operator signalIndex output input := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “pointwise projection iff clean basis action”; the hypotheses and conclusion in the code panel fix its exact scope. Finite-dimensional bridge between the projected-block definition and the clean-branch action proof.

theorem pointwiseProjection_iff_cleanBasisAction
    {signalDim systemDim : Nat} {α : Type u} [NonAssocSemiring α]
    (operator : FiniteMatrix (signalDim * systemDim) (signalDim * systemDim) α)
    (signalIndex : Fin signalDim) (target : Matrix systemDim systemDim α) :
    Matrix.PointwiseEq
        (signalSystemBlockProjection signalDim systemDim systemDim
          operator signalIndex)
        target ↔
      ∀ output input,
        cleanBasisActionAmplitude operator signalIndex output input =
          target output input := by

commit-pinned source · Verso Blueprint panel