6.2. QuantumBlockEncoding/ConcreteSemantics.lean🔗

22 explicit public declarations, in source order.

Definition6.2.1

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. A Mathlib finite matrix, definitionally compatible with ABEIS 'Matrix'.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:25. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.1●1 definition

abbrevdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

abbrev QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix.{u} (rows cols : ℕ)
  (α : Type u) : Type u

abbrev QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix.{u}
  (rows cols : ℕ) (α : Type u) : Type u

A Mathlib finite matrix, definitionally compatible with ABEIS `Matrix`.

Definition6.2.2

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. A finite column vector.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:29. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.2●1 definition

abbrevdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

abbrev QuantumBlockEncoding.ConcreteSemantics.StateVector.{u} (dimension : ℕ)
  (α : Type u) : Type u

abbrev QuantumBlockEncoding.ConcreteSemantics.StateVector.{u}
  (dimension : ℕ) (α : Type u) : Type u

A finite column vector.

Definition6.2.3

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. A computational-basis ket in the concrete finite backend.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.3●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.basisKet.{u} (dimension : ℕ)
  {α : Type u} [Zero α] [One α] (index : Fin dimension) :
  QuantumBlockEncoding.ConcreteSemantics.StateVector dimension α

def QuantumBlockEncoding.ConcreteSemantics.basisKet.{u}
  (dimension : ℕ) {α : Type u} [Zero α]
  [One α] (index : Fin dimension) :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    dimension α

A computational-basis ket in the concrete finite backend.

Definition6.2.4

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The all-zero computational-basis ket for an 'n'-qubit register.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.4●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.zeroKet.{u} (qubits : ℕ)
  {α : Type u} [Zero α] [One α] :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize qubits) α

def QuantumBlockEncoding.ConcreteSemantics.zeroKet.{u}
  (qubits : ℕ) {α : Type u} [Zero α]
  [One α] :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize qubits)
    α

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

Definition6.2.5

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Matrix-vector action using Mathlib's finite sum semantics.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:43. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.5●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.applyVec.{u} {rows cols : ℕ}
  {α : Type u} [NonUnitalNonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix rows cols α)
  (state : QuantumBlockEncoding.ConcreteSemantics.StateVector cols α) :
  QuantumBlockEncoding.ConcreteSemantics.StateVector rows α

def QuantumBlockEncoding.ConcreteSemantics.applyVec.{u}
  {rows cols : ℕ} {α : Type u}
  [NonUnitalNonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      rows cols α)
  (state :
    QuantumBlockEncoding.ConcreteSemantics.StateVector
      cols α) :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    rows α

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

Definition6.2.6

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Declaration kind. structure.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:52. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.6●1 definition

structure(2 fields)defined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

structure QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate (qubits : ℕ) :
  Type

structure QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
  (qubits : ℕ) : Type

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

Fields

matrix : QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix (QuantumBlockEncoding.gridSize qubits)
  (QuantumBlockEncoding.gridSize qubits) ℂ

unitary : self.matrix ∈ Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize qubits)) ℂ

Theorem6.2.7

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Acting on a basis ket selects the corresponding matrix column.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:58. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.7●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.applyVec_basisKet.{u}
  {rows cols : ℕ} {α : Type u} [NonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix rows cols α)
  (index : Fin cols) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec operator
      (QuantumBlockEncoding.ConcreteSemantics.basisKet cols index) =
    Matrix.col operator index

theorem QuantumBlockEncoding.ConcreteSemantics.applyVec_basisKet.{u}
  {rows cols : ℕ} {α : Type u}
  [NonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      rows cols α)
  (index : Fin cols) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      operator
      (QuantumBlockEncoding.ConcreteSemantics.basisKet
        cols index) =
    Matrix.col operator index

Acting on a basis ket selects the corresponding matrix column.

Theorem6.2.8

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Acting on the all-zero ket selects column zero.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:65. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.applyVec_zeroKet.{u} {α : Type u}
  [NonAssocSemiring α] {qubits : ℕ}
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      (QuantumBlockEncoding.gridSize qubits)
      (QuantumBlockEncoding.gridSize qubits) α) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec operator
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet qubits) =
    Matrix.col operator (QuantumBlockEncoding.zeroBasisIndex qubits)

theorem QuantumBlockEncoding.ConcreteSemantics.applyVec_zeroKet.{u}
  {α : Type u} [NonAssocSemiring α]
  {qubits : ℕ}
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      (QuantumBlockEncoding.gridSize
        qubits)
      (QuantumBlockEncoding.gridSize
        qubits)
      α) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      operator
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        qubits) =
    Matrix.col operator
      (QuantumBlockEncoding.zeroBasisIndex
        qubits)

Acting on the all-zero ket selects column zero.

Theorem6.2.9

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The ABEIS first-column contract is exactly the state-action equation 'U |0^n> = |psi>' in the concrete finite matrix backend.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:76. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.9●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

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

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

The ABEIS first-column contract is exactly the state-action equation
`U |0^n> = |psi>` in the concrete finite matrix backend.

Definition6.2.10

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Concrete state-preparation evidence. This is an optional final semantic layer: existing symbolic and rational candidates do not need to use it, but a complex candidate cannot enter this record without standard unitarity and state action.

Declaration kind. structure.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:95. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.10●1 definition

structure(4 fields)defined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

structure QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
  (qubits : ℕ) : Type

structure QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
  (qubits : ℕ) : Type

Concrete state-preparation evidence.  This is an optional final semantic layer:
existing symbolic and rational candidates do not need to use it, but a complex
candidate cannot enter this record without standard unitarity and state action.

Fields

target : QuantumBlockEncoding.StatePreparationTarget ℂ qubits

gate : QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate qubits

normalizationProof : self.target.normalization

preparationProof : QuantumBlockEncoding.ConcreteSemantics.applyVec self.gate.matrix
    (QuantumBlockEncoding.ConcreteSemantics.zeroKet qubits) =
  self.target.amplitudes

Definition6.2.11

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Repackage concrete semantics in the existing generic candidate interface.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:105. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.11●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.candidate
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule : QuantumBlockEncoding.LayeredCircuit)
  (resource : QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.StatePreparationCandidate ℂ qubits

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.candidate
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule :
    QuantumBlockEncoding.LayeredCircuit)
  (resource :
    QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.StatePreparationCandidate
    ℂ qubits

Repackage concrete semantics in the existing generic candidate interface.

Definition6.2.12

uses 0used by 0✓L∃∀N

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Promote a concrete certificate to the existing verified wrapper. The generic 'isUnitary' field is instantiated by, rather than substituted for, the Mathlib unitary-group predicate.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:124. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.12●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verified
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule : QuantumBlockEncoding.LayeredCircuit)
  (resource : QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.VerifiedStatePreparation ℂ qubits

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verified
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule :
    QuantumBlockEncoding.LayeredCircuit)
  (resource :
    QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.VerifiedStatePreparation
    ℂ qubits

Promote a concrete certificate to the existing verified wrapper.  The generic
`isUnitary` field is instantiated by, rather than substituted for, the
Mathlib unitary-group predicate.

Theorem6.2.13

uses 0used by 0✓L∃∀N

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

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:137. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.13●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.preparesVector
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      certificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet qubits) =
    certificate.target.amplitudes

theorem QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.preparesVector
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
      qubits) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      certificate.gate.matrix
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        qubits) =
    certificate.target.amplitudes

Definition6.2.14

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. A matrix indexed by an explicit signal-register/system-register product.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:145. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.14●1 definition

abbrevdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

abbrev QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix.{u}
  (signalDim rows cols : ℕ) (α : Type u) : Type u

abbrev QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix.{u}
  (signalDim rows cols : ℕ) (α : Type u) :
  Type u

A matrix indexed by an explicit signal-register/system-register product.

Definition6.2.15

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:152. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.15●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.flatToProductRegister.{u}
  {signalDim rows cols : ℕ} {α : Type u}
  (operator :
    QuantumBlockEncoding.Matrix (signalDim * rows) (signalDim * cols)
      α) :
  QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix signalDim
    rows cols α

def QuantumBlockEncoding.ConcreteSemantics.flatToProductRegister.{u}
  {signalDim rows cols : ℕ} {α : Type u}
  (operator :
    QuantumBlockEncoding.Matrix
      (signalDim * rows)
      (signalDim * cols) α) :
  QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix
    signalDim rows cols α

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

Definition6.2.16

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Project one signal branch from an explicit product-register matrix.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:163. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.16●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.productRegisterBlockProjection.{u}
  {signalDim rows cols : ℕ} {α : Type u}
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix
      signalDim rows cols α)
  (signalIndex : Fin signalDim) :
  QuantumBlockEncoding.Matrix rows cols α

def QuantumBlockEncoding.ConcreteSemantics.productRegisterBlockProjection.{u}
  {signalDim rows cols : ℕ} {α : Type u}
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.ProductRegisterMatrix
      signalDim rows cols α)
  (signalIndex : Fin signalDim) :
  QuantumBlockEncoding.Matrix rows cols α

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

Theorem6.2.17

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:172. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.17●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

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

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

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

Theorem6.2.18

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The classic product index and circuit-semantics row index have the same value.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:182. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.18●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.productIndex_val_eq_signalSystemBlockRowIndex
  {signalDim systemDim : ℕ} (signalIndex : Fin signalDim)
  (systemIndex : Fin systemDim) :
  ↑(QuantumBlockEncoding.BlockEncodingClassics.productIndex signalIndex
        systemIndex) =
    QuantumBlockEncoding.signalSystemBlockRowIndex systemDim
      ↑signalIndex ↑systemIndex

theorem QuantumBlockEncoding.ConcreteSemantics.productIndex_val_eq_signalSystemBlockRowIndex
  {signalDim systemDim : ℕ}
  (signalIndex : Fin signalDim)
  (systemIndex : Fin systemDim) :
  ↑(QuantumBlockEncoding.BlockEncodingClassics.productIndex
        signalIndex systemIndex) =
    QuantumBlockEncoding.signalSystemBlockRowIndex
      systemDim ↑signalIndex ↑systemIndex

The classic product index and circuit-semantics row index have the same value.

Theorem6.2.19

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The classic rational clean block and the generic circuit-semantics projection are the same pointwise matrix under the shared register order.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:194. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.19●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim) :
  (QuantumBlockEncoding.signalSystemBlockProjection signalDim systemDim
        systemDim operator signalIndex).PointwiseEq
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
      signalIndex operator)

theorem QuantumBlockEncoding.ConcreteSemantics.signalSystemBlockProjection_eq_cleanBlockProduct
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix
      (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim) :
  (QuantumBlockEncoding.signalSystemBlockProjection
        signalDim systemDim systemDim
        operator signalIndex).PointwiseEq
    (QuantumBlockEncoding.BlockEncodingClassics.cleanBlockProduct
      signalIndex operator)

The classic rational clean block and the generic circuit-semantics projection
are the same pointwise matrix under the shared register order.

Definition6.2.20

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. The clean output amplitude obtained by applying 'operator' to a clean signal-system basis input. Naming this quantity makes the two common block-encoding proof styles explicit: prove the projected matrix block, or prove the clean branch of the action on every basis input.

Declaration kind. def.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:211. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition6.2.20●1 definition

defdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude.{u}
  {signalDim systemDim : ℕ} {α : Type u} [NonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      (signalDim * systemDim) (signalDim * systemDim) α)
  (signalIndex : Fin signalDim) (output input : Fin systemDim) : α

def QuantumBlockEncoding.ConcreteSemantics.cleanBasisActionAmplitude.{u}
  {signalDim systemDim : ℕ} {α : Type u}
  [NonAssocSemiring α]
  (operator :
    QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
      (signalDim * systemDim)
      (signalDim * systemDim) α)
  (signalIndex : Fin signalDim)
  (output input : Fin systemDim) : α

The clean output amplitude obtained by applying `operator` to a clean
signal-system basis input.  Naming this quantity makes the two common
block-encoding proof styles explicit: prove the projected matrix block, or
prove the clean branch of the action on every basis input.

Theorem6.2.21

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

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

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:221. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.21●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

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

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

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

Theorem6.2.22

uses 0used by 0✓L∃∀N

Plain-English reading. 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.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

Why it is in this chapter. Definitions and lemmas that connect circuit syntax to evaluated matrix semantics, finite state action, and explicit product-register projection.

Technical source note. Finite-dimensional bridge between the projected-block definition and the clean-branch action proof. Linearity then extends the basis statement to an arbitrary system state; any normalized orthogonal failure branch is additional unitarity evidence, not a different block-encoding contract.

Declaration kind. theorem.

Source: QuantumBlockEncoding/ConcreteSemantics.lean:239. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.2.22●1 theorem

theoremdefined in QuantumBlockEncoding/ConcreteSemantics.lean

complete

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

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

Finite-dimensional bridge between the projected-block definition and the
clean-branch action proof.  Linearity then extends the basis statement to an
arbitrary system state; any normalized orthogonal failure branch is additional
unitarity evidence, not a different block-encoding contract.