5.5. QuantumBlockEncoding/StatePreparation.lean🔗

11 explicit public declarations, in source order.

Definition5.5.1

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The computational all-zero basis index in an 'n'-qubit register.

Declaration kind. def.

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

Lean code for Definition5.5.1●1 definition

defdefined in QuantumBlockEncoding/StatePreparation.lean

complete

def QuantumBlockEncoding.zeroBasisIndex (n : ℕ) :
  Fin (QuantumBlockEncoding.gridSize n)

def QuantumBlockEncoding.zeroBasisIndex
  (n : ℕ) :
  Fin (QuantumBlockEncoding.gridSize n)

The computational all-zero basis index in an `n`-qubit register.

Definition5.5.2

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A normalized state requested by the user.

Declaration kind. structure.

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

Lean code for Definition5.5.2●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StatePreparation.lean

complete

structure QuantumBlockEncoding.StatePreparationTarget.{u} (α : Type u)
  (qubits : ℕ) : Type u

structure QuantumBlockEncoding.StatePreparationTarget.{u}
  (α : Type u) (qubits : ℕ) : Type u

A normalized state requested by the user.

Fields

amplitudes : Fin (QuantumBlockEncoding.gridSize qubits) → α

normalization : Prop

source : String

Definition5.5.3

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The matrix-level first-column acceptance predicate.

Declaration kind. def.

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

Lean code for Definition5.5.3●1 definition

defdefined in QuantumBlockEncoding/StatePreparation.lean

complete

def QuantumBlockEncoding.FirstColumnMatches.{u} {α : Type u} {qubits : ℕ}
  (unitary :
    QuantumBlockEncoding.Matrix (QuantumBlockEncoding.gridSize qubits)
      (QuantumBlockEncoding.gridSize qubits) α)
  (target : QuantumBlockEncoding.StatePreparationTarget α qubits) : Prop

def QuantumBlockEncoding.FirstColumnMatches.{u}
  {α : Type u} {qubits : ℕ}
  (unitary :
    QuantumBlockEncoding.Matrix
      (QuantumBlockEncoding.gridSize
        qubits)
      (QuantumBlockEncoding.gridSize
        qubits)
      α)
  (target :
    QuantumBlockEncoding.StatePreparationTarget
      α qubits) :
  Prop

The matrix-level first-column acceptance predicate.

Definition5.5.4

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A state-preparation candidate before semantic proofs are attached.

Declaration kind. structure.

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

Lean code for Definition5.5.4●1 definition

structure(7 fields)defined in QuantumBlockEncoding/StatePreparation.lean

complete

structure QuantumBlockEncoding.StatePreparationCandidate.{u} (α : Type u)
  (qubits : ℕ) : Type u

structure QuantumBlockEncoding.StatePreparationCandidate.{u}
  (α : Type u) (qubits : ℕ) : Type u

A state-preparation candidate before semantic proofs are attached.

Fields

target : QuantumBlockEncoding.StatePreparationTarget α qubits

unitary : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.gridSize qubits) (QuantumBlockEncoding.gridSize qubits) α

circuit : QuantumBlockEncoding.Circuit

schedule : QuantumBlockEncoding.LayeredCircuit

resource : QuantumBlockEncoding.Resource

auxiliaryQubits : ℕ

isUnitary : Prop

Definition5.5.5

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. The candidate's fixed semantic target; callers cannot replace it by a flag.

Declaration kind. def.

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

Lean code for Definition5.5.5●1 definition

defdefined in QuantumBlockEncoding/StatePreparation.lean

complete

def QuantumBlockEncoding.StatePreparationCandidate.preparesTarget.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate α qubits) :
  Prop

def QuantumBlockEncoding.StatePreparationCandidate.preparesTarget.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits) :
  Prop

The candidate's fixed semantic target; callers cannot replace it by a flag.

Definition5.5.6

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. Reuse the block-encoding resource order for state-preparation candidates.

Declaration kind. def.

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

Lean code for Definition5.5.6●1 definition

defdefined in QuantumBlockEncoding/StatePreparation.lean

complete

def QuantumBlockEncoding.StatePreparationCandidate.cost.{u_1} {α : Type u_1}
  {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate α qubits) :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.StatePreparationCandidate.cost.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits) :
  QuantumBlockEncoding.BlockEncodingCost

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

Definition5.5.7

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A candidate promoted by proofs of normalization, unitarity, and state action.

Declaration kind. structure.

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

Lean code for Definition5.5.7●1 definition

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

complete

structure QuantumBlockEncoding.VerifiedStatePreparation.{u} (α : Type u)
  (qubits : ℕ) : Type u

structure QuantumBlockEncoding.VerifiedStatePreparation.{u}
  (α : Type u) (qubits : ℕ) : Type u

A candidate promoted by proofs of normalization, unitarity, and state action.

Fields

candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits

normalizationProof : self.candidate.target.normalization

unitaryProof : self.candidate.isUnitary

preparationProof : self.candidate.preparesTarget

Definition5.5.8

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. An approximate candidate with a backend-specific state-error predicate.

Declaration kind. structure.

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

Lean code for Definition5.5.8●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StatePreparation.lean

complete

structure QuantumBlockEncoding.ApproximateStatePreparationCandidate.{u}
  (α : Type u) (qubits : ℕ) : Type u

structure QuantumBlockEncoding.ApproximateStatePreparationCandidate.{u}
  (α : Type u) (qubits : ℕ) : Type u

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

Fields

candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits

epsilon : α

approximationBound : Prop

Definition5.5.9

uses 0used by 0✓L∃∀N

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

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

Why it is in this chapter. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. A verified approximate state-preparation certificate.

Declaration kind. structure.

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

Lean code for Definition5.5.9●1 definition

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

complete

structure QuantumBlockEncoding.VerifiedApproximateStatePreparation.{u}
  (α : Type u) (qubits : ℕ) : Type u

structure QuantumBlockEncoding.VerifiedApproximateStatePreparation.{u}
  (α : Type u) (qubits : ℕ) : Type u

A verified approximate state-preparation certificate.

Fields

approxCandidate : QuantumBlockEncoding.ApproximateStatePreparationCandidate α qubits

normalizationProof : self.approxCandidate.candidate.target.normalization

unitaryProof : self.approxCandidate.candidate.isUnitary

approximationProof : self.approxCandidate.approximationBound

Definition5.5.10

uses 0used by 0✓L∃∀N

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

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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

Technical source note. 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.

Declaration kind. def.

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

Lean code for Definition5.5.10●1 definition

defdefined in QuantumBlockEncoding/StatePreparation.lean

complete

def QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox.{u_1}
  {α : Type u_1} {qubits : ℕ} [OfNat α 0]
  (verified : QuantumBlockEncoding.VerifiedStatePreparation α qubits) :
  QuantumBlockEncoding.VerifiedApproximateStatePreparation α qubits

def QuantumBlockEncoding.VerifiedStatePreparation.asZeroErrorApprox.{u_1}
  {α : Type u_1} {qubits : ℕ} [OfNat α 0]
  (verified :
    QuantumBlockEncoding.VerifiedStatePreparation
      α qubits) :
  QuantumBlockEncoding.VerifiedApproximateStatePreparation
    α qubits

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.

Theorem5.5.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “first column”; 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. Core finite matrices, task contracts, resource records, circuit syntax, and certificate data structures.

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/StatePreparation.lean:98. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.5.11●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparation.lean

complete

theorem QuantumBlockEncoding.VerifiedStatePreparation.firstColumn.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (verified : QuantumBlockEncoding.VerifiedStatePreparation α qubits) :
  verified.candidate.preparesTarget

theorem QuantumBlockEncoding.VerifiedStatePreparation.firstColumn.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (verified :
    QuantumBlockEncoding.VerifiedStatePreparation
      α qubits) :
  verified.candidate.preparesTarget