ASPBE Lean Blueprint

5.1. QuantumBlockEncoding/BlockEncoding.lean🔗

22 explicit public declarations, in source order.

Definition5.1.1
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “register layout”. A proposition-valued field is a requirement until a constructor supplies it.

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. 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. structure.

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

Lean code for Definition5.1.1●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.RegisterLayout : Type
    structure QuantumBlockEncoding.RegisterLayout : Type

    Fields

    systemQubits : ℕ
    signalQubits : ℕ
    pureAncillas : ℕ
Definition5.1.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “auxiliary qubits”. The auxiliary qubit count used by the block-encoding score.

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 auxiliary qubit count used by the block-encoding score. This combines the signal qubits selecting the block with pure ancillas that must be returned to a clean state.

Declaration kind. def.

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

Lean code for Definition5.1.2●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.RegisterLayout.auxiliaryQubits
  (layout : QuantumBlockEncoding.RegisterLayout) : ℕ
    def QuantumBlockEncoding.RegisterLayout.auxiliaryQubits
  (layout :
    QuantumBlockEncoding.RegisterLayout) :
  ℕ
    The auxiliary qubit count used by the block-encoding score.  This combines the
signal qubits selecting the block with pure ancillas that must be returned to a
clean state.
Definition5.1.3
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “block encoding spec”. A proposition-valued field is a requirement until a constructor supplies it. A block-encoding 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 block-encoding candidate before semantic proofs are attached.

Declaration kind. structure.

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

Lean code for Definition5.1.3●1 definition
  • structure(6 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.BlockEncodingSpec.{u} (α : Type u)
  (rows cols : ℕ) : Type u
    structure QuantumBlockEncoding.BlockEncodingSpec.{u}
  (α : Type u) (rows cols : ℕ) : Type u
    A block-encoding candidate before semantic proofs are attached.

    Fields

    matrix : QuantumBlockEncoding.Matrix rows cols α
    normalizer : α
    error : α
    layout : QuantumBlockEncoding.RegisterLayout
    circuit : QuantumBlockEncoding.Circuit
    resource : QuantumBlockEncoding.Resource
Definition5.1.4
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “block encoding cost”. A proposition-valued field is a requirement until a constructor supplies it. Resource score for comparing two candidate block encodings of the same operator.

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. Resource score for comparing two candidate block encodings of the same operator. The search order is deliberately domain-specific: 1. fewer gates, 2. smaller circuit depth, 3. fewer auxiliary qubits, 4. fewer unresolved oracle calls.

Declaration kind. structure.

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

Lean code for Definition5.1.4●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.BlockEncodingCost : Type
    structure QuantumBlockEncoding.BlockEncodingCost :
  Type
    Resource score for comparing two candidate block encodings of the same
operator.  The search order is deliberately domain-specific:

1. fewer gates,
2. smaller circuit depth,
3. fewer auxiliary qubits,
4. fewer unresolved oracle calls.

    Fields

    auxiliaryQubits : ℕ
    gateCount : ℕ
    depth : ℕ
    oracleCalls : ℕ
Definition5.1.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “from layout and resource”.

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 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. def.

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

Lean code for Definition5.1.5●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.BlockEncodingCost.fromLayoutAndResource
  (layout : QuantumBlockEncoding.RegisterLayout)
  (resource : QuantumBlockEncoding.Resource) :
  QuantumBlockEncoding.BlockEncodingCost
    def QuantumBlockEncoding.BlockEncodingCost.fromLayoutAndResource
  (layout :
    QuantumBlockEncoding.RegisterLayout)
  (resource :
    QuantumBlockEncoding.Resource) :
  QuantumBlockEncoding.BlockEncodingCost
Definition5.1.6
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “from spec”.

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 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. def.

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

Lean code for Definition5.1.6●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.BlockEncodingCost.fromSpec.{u_1} {α : Type u_1}
  {rows cols : ℕ}
  (spec : QuantumBlockEncoding.BlockEncodingSpec α rows cols) :
  QuantumBlockEncoding.BlockEncodingCost
    def QuantumBlockEncoding.BlockEncodingCost.fromSpec.{u_1}
  {α : Type u_1} {rows cols : ℕ}
  (spec :
    QuantumBlockEncoding.BlockEncodingSpec
      α rows cols) :
  QuantumBlockEncoding.BlockEncodingCost
Definition5.1.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “better than”. Strict lexicographic improvement used by candidate-population selection.

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. Strict lexicographic improvement used by candidate-population selection.

Declaration kind. def.

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

Lean code for Definition5.1.7●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.BlockEncodingCost.betterThan
  (x y : QuantumBlockEncoding.BlockEncodingCost) : Prop
    def QuantumBlockEncoding.BlockEncodingCost.betterThan
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  Prop
    Strict lexicographic improvement used by candidate-population selection.
Definition5.1.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “no worse than”. Non-strict version for accepting a candidate as no worse than a baseline.

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. Non-strict version for accepting a candidate as no worse than a baseline.

Declaration kind. def.

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

Lean code for Definition5.1.8●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.BlockEncodingCost.noWorseThan
  (x y : QuantumBlockEncoding.BlockEncodingCost) : Prop
    def QuantumBlockEncoding.BlockEncodingCost.noWorseThan
  (x y :
    QuantumBlockEncoding.BlockEncodingCost) :
  Prop
    Non-strict version for accepting a candidate as no worse than a baseline.
Definition5.1.9
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “query operator target”. A proposition-valued field is a requirement until a constructor supplies it. The concrete input ABEIS is meant to solve: a user gives an operator/query oracle target, usually as a finite matrix together with a normalization contract and optional free parameters.

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. The concrete input ABEIS is meant to solve: a user gives an operator/query oracle target, usually as a finite matrix together with a normalization contract and optional free parameters.

Declaration kind. structure.

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

Lean code for Definition5.1.9●1 definition
  • structure(5 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.QueryOperatorTarget.{u} (α : Type u)
  (rows cols : ℕ) : Type u
    structure QuantumBlockEncoding.QueryOperatorTarget.{u}
  (α : Type u) (rows cols : ℕ) : Type u
    The concrete input ABEIS is meant to solve: a user gives an operator/query
oracle target, usually as a finite matrix together with a normalization
contract and optional free parameters.

    Fields

    operator : QuantumBlockEncoding.Matrix rows cols α
    normalizer : α
    source : String
    semanticContract : String
    freeParameters : List String
Definition5.1.10
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. A candidate unitary for an 'n'-qubit square operator.

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 unitary for an 'n'-qubit square operator. The size of the unitary is fixed by the chosen number of auxiliary qubits: if the target acts on 'N = 2^n' dimensions and the candidate uses 'a' auxiliary qubits, then the unitary acts on '2^(n+a)' dimensions.

Declaration kind. structure.

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

Lean code for Definition5.1.10●1 definition
  • structure(10 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.OperatorBlockEncodingCandidate.{u} (α : Type u)
  (systemQubits : ℕ) : Type u
    structure QuantumBlockEncoding.OperatorBlockEncodingCandidate.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    A candidate unitary for an `n`-qubit square operator.  The size of the unitary
is fixed by the chosen number of auxiliary qubits: if the target acts on
`N = 2^n` dimensions and the candidate uses `a` auxiliary qubits, then the
unitary acts on `2^(n+a)` dimensions.

    Fields

    auxiliaryQubits : ℕ
    target : QuantumBlockEncoding.QueryOperatorTarget α (QuantumBlockEncoding.gridSize systemQubits)
  (QuantumBlockEncoding.gridSize systemQubits)
    unitary : QuantumBlockEncoding.Matrix (QuantumBlockEncoding.gridSize (systemQubits + self.auxiliaryQubits))
  (QuantumBlockEncoding.gridSize (systemQubits + self.auxiliaryQubits)) α
    layout : QuantumBlockEncoding.RegisterLayout
    circuit : QuantumBlockEncoding.Circuit
    schedule : QuantumBlockEncoding.LayeredCircuit
    resource : QuantumBlockEncoding.Resource
    layoutMatches : self.layout.auxiliaryQubits = self.auxiliaryQubits
    isUnitary : Prop
    blockContainsTarget : Prop
Definition5.1.11
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cost”.

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 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. def.

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

Lean code for Definition5.1.11●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate α
      systemQubits) :
  QuantumBlockEncoding.BlockEncodingCost
    def QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate
      α systemQubits) :
  QuantumBlockEncoding.BlockEncodingCost
Definition5.1.12
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “verified operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified candidate with explicit proofs of unitarity and block containment.

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 candidate with explicit proofs of unitarity and block containment.

Declaration kind. structure.

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

Lean code for Definition5.1.12●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.VerifiedOperatorBlockEncoding.{u} (α : Type u)
  (systemQubits : ℕ) : Type u
    structure QuantumBlockEncoding.VerifiedOperatorBlockEncoding.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    A verified candidate with explicit proofs of unitarity and block containment.

    Fields

    candidate : QuantumBlockEncoding.OperatorBlockEncodingCandidate α systemQubits
    unitaryProof : self.candidate.isUnitary
    blockProof : self.candidate.blockContainsTarget
Definition5.1.13
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “approximate operator block encoding candidate”. A proposition-valued field is a requirement until a constructor supplies it. An approximate block-encoding candidate for the same operator-first interface.

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 block-encoding candidate for the same operator-first interface. The mathematical backend should instantiate 'approximationBound' with the norm inequality '‖A - α * ((⟨0^a| ⊗ I) U (|0^a⟩ ⊗ I))‖ ≤ ε'. The field is deliberately a proposition, because different finite backends may start with different norms or exact-rational surrogate checks before connecting to a full analytic norm library.

Declaration kind. structure.

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

Lean code for Definition5.1.13●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.ApproximateOperatorBlockEncodingCandidate.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    structure QuantumBlockEncoding.ApproximateOperatorBlockEncodingCandidate.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    An approximate block-encoding candidate for the same operator-first interface.

The mathematical backend should instantiate `approximationBound` with the
norm inequality

`‖A - α * ((⟨0^a| ⊗ I) U (|0^a⟩ ⊗ I))‖ ≤ ε`.

The field is deliberately a proposition, because different finite backends may
start with different norms or exact-rational surrogate checks before connecting
to a full analytic norm library.

    Fields

    candidate : QuantumBlockEncoding.OperatorBlockEncodingCandidate α systemQubits
    epsilon : α
    approximationBound : Prop
Definition5.1.14
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “verified approximate operator block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified approximate block encoding.

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 block encoding. Exact block encodings are the special case 'epsilon = 0' when the backend proves that exact equality implies the chosen norm bound.

Declaration kind. structure.

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

Lean code for Definition5.1.14●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    structure QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding.{u}
  (α : Type u) (systemQubits : ℕ) : Type u
    A verified approximate block encoding.  Exact block encodings are the special
case `epsilon = 0` when the backend proves that exact equality implies the
chosen norm bound.

    Fields

    approxCandidate : QuantumBlockEncoding.ApproximateOperatorBlockEncodingCandidate α systemQubits
    unitaryProof : self.approxCandidate.candidate.isUnitary
    approximationProof : self.approxCandidate.approximationBound
Definition5.1.15
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 certificate as a zero-error approximate certificate when the chosen approximate proposition is the same exact block 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. Package an exact certificate as a zero-error approximate certificate when the chosen approximate proposition is the same exact block predicate. Analytic backends can later replace this with a theorem connecting exact block equality to a concrete operator-norm inequality.

Declaration kind. def.

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

Lean code for Definition5.1.15●1 definition
  • defdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    def QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox.{u_1}
  {α : Type u_1} {systemQubits : ℕ} [OfNat α 0]
  (v :
    QuantumBlockEncoding.VerifiedOperatorBlockEncoding α systemQubits) :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding α
    systemQubits
    def QuantumBlockEncoding.VerifiedOperatorBlockEncoding.asZeroErrorApprox.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  [OfNat α 0]
  (v :
    QuantumBlockEncoding.VerifiedOperatorBlockEncoding
      α systemQubits) :
  QuantumBlockEncoding.VerifiedApproximateOperatorBlockEncoding
    α systemQubits
    Package an exact certificate as a zero-error approximate certificate when the
chosen approximate proposition is the same exact block predicate.  Analytic
backends can later replace this with a theorem connecting exact block equality
to a concrete operator-norm inequality.
Definition5.1.16
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “adaptive block encoding policy”. A proposition-valued field is a requirement until a constructor supplies it. User-level stopping and relaxation policy for operator block-encoding search.

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. User-level stopping and relaxation policy for operator block-encoding search. The harness first searches for exact block encodings. If a certified exact candidate meeting 'requiredCost' appears before 'maxExactIterations', it may enter a post-convergence approximate-improvement phase for the user's requested epsilon. If the exact search stalls, the upper layer may switch to approximate search and, if allowed, relax beyond the requested epsilon.

Declaration kind. structure.

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

Lean code for Definition5.1.16●1 definition
  • structure(8 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.AdaptiveBlockEncodingPolicy.{u} (α : Type u) :
  Type u
    structure QuantumBlockEncoding.AdaptiveBlockEncodingPolicy.{u}
  (α : Type u) : Type u
    User-level stopping and relaxation policy for operator block-encoding search.

The harness first searches for exact block encodings.  If a certified exact
candidate meeting `requiredCost` appears before `maxExactIterations`, it may
enter a post-convergence approximate-improvement phase for the user's requested
epsilon.  If the exact search stalls, the upper layer may switch to approximate
search and, if allowed, relax beyond the requested epsilon.

    Fields

    maxExactIterations : ℕ
    exactStallIterations : ℕ
    requiredCost : QuantumBlockEncoding.BlockEncodingCost
    requestedEpsilon : α
    allowRelaxedEpsilon : Bool
    maxUpperAgents : ℕ
    maxMiddleAgents : ℕ
    maxLowerAgents : ℕ
Definition5.1.17
uses 0used by 0✓L∃∀N

Plain-English reading. This type lists the allowed alternatives for “block encoding search phase”; its constructors are the cases that downstream code must handle. High-level phase labels used by the candidate-population ledger.

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. High-level phase labels used by the candidate-population ledger.

Declaration kind. inductive.

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

Lean code for Definition5.1.17●1 definition
  • inductive(4 constructors)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    inductive QuantumBlockEncoding.BlockEncodingSearchPhase : Type
    inductive QuantumBlockEncoding.BlockEncodingSearchPhase :
  Type
    High-level phase labels used by the candidate-population ledger.

    Constructors

    exactSearch : QuantumBlockEncoding.BlockEncodingSearchPhase
    exactConvergedApproxSearch :
  QuantumBlockEncoding.BlockEncodingSearchPhase
    relaxedApproxSearch :
  QuantumBlockEncoding.BlockEncodingSearchPhase
    stopped : QuantumBlockEncoding.BlockEncodingSearchPhase
Definition5.1.18
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “verified block encoding”. A proposition-valued field is a requirement until a constructor supplies it. A verified block encoding.

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 block encoding. The three proposition fields are intentionally parameters of the certificate so that early project files can state workflows without committing to a specific matrix norm or unitary semantics. A mathlib backend should instantiate these propositions with concrete definitions.

Declaration kind. structure.

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

Lean code for Definition5.1.18●1 definition
  • structure(7 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.VerifiedBlockEncoding.{u} (α : Type u)
  (rows cols : ℕ) : Type u
    structure QuantumBlockEncoding.VerifiedBlockEncoding.{u}
  (α : Type u) (rows cols : ℕ) : Type u
    A verified block encoding.  The three proposition fields are intentionally
parameters of the certificate so that early project files can state workflows
without committing to a specific matrix norm or unitary semantics.  A mathlib
backend should instantiate these propositions with concrete definitions.

    Fields

    spec : QuantumBlockEncoding.BlockEncodingSpec α rows cols
    isUnitary : Prop
    blockCorrect : Prop
    resourceBound : Prop
    unitaryProof : self.isUnitary
    blockProof : self.blockCorrect
    resourceProof : self.resourceBound
Theorem5.1.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “unitary”; 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/BlockEncoding.lean:231. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.1.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.unitary.{u} {α : Type u}
  {rows cols : ℕ}
  (v : QuantumBlockEncoding.VerifiedBlockEncoding α rows cols) :
  v.isUnitary
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.unitary.{u}
  {α : Type u} {rows cols : ℕ}
  (v :
    QuantumBlockEncoding.VerifiedBlockEncoding
      α rows cols) :
  v.isUnitary
Theorem5.1.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “correct”; 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/BlockEncoding.lean:235. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.1.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.correct.{u} {α : Type u}
  {rows cols : ℕ}
  (v : QuantumBlockEncoding.VerifiedBlockEncoding α rows cols) :
  v.blockCorrect
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.correct.{u}
  {α : Type u} {rows cols : ℕ}
  (v :
    QuantumBlockEncoding.VerifiedBlockEncoding
      α rows cols) :
  v.blockCorrect
Theorem5.1.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “resource ok”; 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/BlockEncoding.lean:239. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem5.1.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.resource_ok.{u} {α : Type u}
  {rows cols : ℕ}
  (v : QuantumBlockEncoding.VerifiedBlockEncoding α rows cols) :
  v.resourceBound
    theorem QuantumBlockEncoding.VerifiedBlockEncoding.resource_ok.{u}
  {α : Type u} {rows cols : ℕ}
  (v :
    QuantumBlockEncoding.VerifiedBlockEncoding
      α rows cols) :
  v.resourceBound
Definition5.1.22
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “construction claim”. A proposition-valued field is a requirement until a constructor supplies it. A high-level construction claim imported from a paper or generated by AI.

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 high-level construction claim imported from a paper or generated by AI.

Declaration kind. structure.

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

Lean code for Definition5.1.22●1 definition
  • structure(6 fields)defined in QuantumBlockEncoding/BlockEncoding.lean
    complete
    structure QuantumBlockEncoding.ConstructionClaim : Type
    structure QuantumBlockEncoding.ConstructionClaim :
  Type
    A high-level construction claim imported from a paper or generated by AI.

    Fields

    name : String
    source : String
    target : String
    normalization : String
    layout : String
    resource : QuantumBlockEncoding.AsymptoticResource