6.11. QuantumBlockEncoding/TeachingRouteClosures.lean🔗

35 explicit public declarations, in source order.

Definition6.11.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “executable resource certificate”. A proposition-valued field is a requirement until a constructor supplies it. Backend-neutral cost evidence computed from the canonical primitive IR.

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. Backend-neutral cost evidence computed from the canonical primitive IR.

Declaration kind. structure.

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

Lean code for Definition6.11.1●1 definition

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

complete

structure QuantumBlockEncoding.ExecutableResourceCertificate (qubits : ℕ) : Type

structure QuantumBlockEncoding.ExecutableResourceCertificate
  (qubits : ℕ) : Type

Backend-neutral cost evidence computed from the canonical primitive IR.

Fields

program : QuantumBlockEncoding.PrimitiveProgram qubits

auxiliaryQubits : ℕ

Definition6.11.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “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. 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. def.

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

Lean code for Definition6.11.2●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.ExecutableResourceCertificate.resource {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.ExecutableResourceCertificate.resource
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  QuantumBlockEncoding.Resource

Definition6.11.3

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

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

Lean code for Definition6.11.3●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.ExecutableResourceCertificate.cost {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  QuantumBlockEncoding.BlockEncodingCost

def QuantumBlockEncoding.ExecutableResourceCertificate.cost
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  QuantumBlockEncoding.BlockEncodingCost

Theorem6.11.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.4●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ExecutableResourceCertificate.resource_eq_program_resource
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  certificate.resource = certificate.program.resource

theorem QuantumBlockEncoding.ExecutableResourceCertificate.resource_eq_program_resource
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  certificate.resource =
    certificate.program.resource

Theorem6.11.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.5●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_auxiliaryQubits
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  certificate.cost.auxiliaryQubits = certificate.auxiliaryQubits

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_auxiliaryQubits
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  certificate.cost.auxiliaryQubits =
    certificate.auxiliaryQubits

Theorem6.11.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.6●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_gateCount
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  certificate.cost.gateCount = certificate.program.resource.gates

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_gateCount
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  certificate.cost.gateCount =
    certificate.program.resource.gates

Theorem6.11.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.7●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_depth
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  certificate.cost.depth = certificate.program.resource.depth

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_depth
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  certificate.cost.depth =
    certificate.program.resource.depth

Theorem6.11.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.8●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_oracleCalls
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate qubits) :
  certificate.cost.oracleCalls =
    certificate.program.resource.oracleCalls

theorem QuantumBlockEncoding.ExecutableResourceCertificate.cost_oracleCalls
  {qubits : ℕ}
  (certificate :
    QuantumBlockEncoding.ExecutableResourceCertificate
      qubits) :
  certificate.cost.oracleCalls =
    certificate.program.resource.oracleCalls

Definition6.11.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “certify”. Promote a candidate only after all three state-preparation obligations are supplied.

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 candidate only after all three state-preparation obligations are supplied.

Declaration kind. def.

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

Lean code for Definition6.11.9●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.StatePreparationCandidate.certify.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits)
  (normalizationProof : candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof : candidate.preparesTarget) :
  QuantumBlockEncoding.VerifiedStatePreparation α qubits

def QuantumBlockEncoding.StatePreparationCandidate.certify.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits)
  (normalizationProof :
    candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof :
    candidate.preparesTarget) :
  QuantumBlockEncoding.VerifiedStatePreparation
    α qubits

Promote a candidate only after all three state-preparation obligations are supplied.

Theorem6.11.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.10●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_firstColumn.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits)
  (normalizationProof : candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof : candidate.preparesTarget) :
  (candidate.certify normalizationProof unitaryProof
        preparationProof).candidate.preparesTarget

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_firstColumn.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits)
  (normalizationProof :
    candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof :
    candidate.preparesTarget) :
  (candidate.certify normalizationProof
        unitaryProof
        preparationProof).candidate.preparesTarget

Theorem6.11.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.11●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_unitary.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits)
  (normalizationProof : candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof : candidate.preparesTarget) :
  (candidate.certify normalizationProof unitaryProof
        preparationProof).candidate.isUnitary

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_unitary.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits)
  (normalizationProof :
    candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof :
    candidate.preparesTarget) :
  (candidate.certify normalizationProof
        unitaryProof
        preparationProof).candidate.isUnitary

Theorem6.11.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.12●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_normalization.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate : QuantumBlockEncoding.StatePreparationCandidate α qubits)
  (normalizationProof : candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof : candidate.preparesTarget) :
  (candidate.certify normalizationProof unitaryProof
          preparationProof).candidate.target.normalization

theorem QuantumBlockEncoding.StatePreparationCandidate.certify_normalization.{u_1}
  {α : Type u_1} {qubits : ℕ}
  (candidate :
    QuantumBlockEncoding.StatePreparationCandidate
      α qubits)
  (normalizationProof :
    candidate.target.normalization)
  (unitaryProof : candidate.isUnitary)
  (preparationProof :
    candidate.preparesTarget) :
  (candidate.certify normalizationProof
          unitaryProof
          preparationProof).candidate.target.normalization

Definition6.11.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “of first column”. Build concrete state-preparation evidence from the equivalent first-column statement.

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. Build concrete state-preparation evidence from the equivalent first-column statement.

Declaration kind. def.

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

Lean code for Definition6.11.13●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.ofFirstColumn
  {qubits : ℕ}
  (target : QuantumBlockEncoding.StatePreparationTarget ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate qubits)
  (normalizationProof : target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches gate.matrix target) :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    qubits

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.ofFirstColumn
  {qubits : ℕ}
  (target :
    QuantumBlockEncoding.StatePreparationTarget
      ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
      qubits)
  (normalizationProof :
    target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches
      gate.matrix target) :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    qubits

Build concrete state-preparation evidence from the equivalent first-column statement.

Definition6.11.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “verified of first column”. Promote first-column evidence through the concrete finite-matrix 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. Promote first-column evidence through the concrete finite-matrix backend.

Declaration kind. def.

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

Lean code for Definition6.11.14●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
  {qubits : ℕ}
  (target : QuantumBlockEncoding.StatePreparationTarget ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate qubits)
  (normalizationProof : target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches gate.matrix target)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule : QuantumBlockEncoding.LayeredCircuit)
  (resource : QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.VerifiedStatePreparation ℂ qubits

def QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
  {qubits : ℕ}
  (target :
    QuantumBlockEncoding.StatePreparationTarget
      ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
      qubits)
  (normalizationProof :
    target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches
      gate.matrix target)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule :
    QuantumBlockEncoding.LayeredCircuit)
  (resource :
    QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  QuantumBlockEncoding.VerifiedStatePreparation
    ℂ qubits

Promote first-column evidence through the concrete finite-matrix backend.

Theorem6.11.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “verified of first column prepares target”; 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/TeachingRouteClosures.lean:116. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.15●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn_preparesTarget
  {qubits : ℕ}
  (target : QuantumBlockEncoding.StatePreparationTarget ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate qubits)
  (normalizationProof : target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches gate.matrix target)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule : QuantumBlockEncoding.LayeredCircuit)
  (resource : QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  (QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
        target gate normalizationProof firstColumnProof circuit schedule
        resource auxiliaryQubits).candidate.preparesTarget

theorem QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn_preparesTarget
  {qubits : ℕ}
  (target :
    QuantumBlockEncoding.StatePreparationTarget
      ℂ qubits)
  (gate :
    QuantumBlockEncoding.ConcreteSemantics.ComplexUnitaryGate
      qubits)
  (normalizationProof :
    target.normalization)
  (firstColumnProof :
    QuantumBlockEncoding.FirstColumnMatches
      gate.matrix target)
  (circuit : QuantumBlockEncoding.Circuit)
  (schedule :
    QuantumBlockEncoding.LayeredCircuit)
  (resource :
    QuantumBlockEncoding.Resource)
  (auxiliaryQubits : ℕ := 0) :
  (QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate.verifiedOfFirstColumn
        target gate normalizationProof
        firstColumnProof circuit schedule
        resource
        auxiliaryQubits).candidate.preparesTarget

Definition6.11.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “textbook pauli x verified of first column”. Finite witness that the generic first-column route reuses the Pauli-X proof.

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. Finite witness that the generic first-column route reuses the Pauli-X proof.

Declaration kind. def.

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

Lean code for Definition6.11.16●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn :
  QuantumBlockEncoding.VerifiedStatePreparation ℂ 1

def QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn :
  QuantumBlockEncoding.VerifiedStatePreparation
    ℂ 1

Finite witness that the generic first-column route reuses the Pauli-X proof.

Theorem6.11.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “textbook pauli x verified of first column prepares target”; 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/TeachingRouteClosures.lean:141. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.17●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn_preparesTarget :
  QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn.candidate.preparesTarget

theorem QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn_preparesTarget :
  QuantumBlockEncoding.textbookPauliXVerifiedOfFirstColumn.candidate.preparesTarget

Definition6.11.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “exact clean block of signal projection”. Convert a signal-register projection proof into an exact clean-block certificate.

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. Convert a signal-register projection proof into an exact clean-block certificate.

Declaration kind. def.

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

Lean code for Definition6.11.18●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim)
  (target : QuantumBlockEncoding.Matrix systemDim systemDim ℚ)
  (projectionProof :
    (QuantumBlockEncoding.signalSystemBlockProjection signalDim
          systemDim systemDim operator signalIndex).PointwiseEq
      target) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock systemDim
    (signalDim * systemDim)

def QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix
      (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim)
  (target :
    QuantumBlockEncoding.Matrix systemDim
      systemDim ℚ)
  (projectionProof :
    (QuantumBlockEncoding.signalSystemBlockProjection
          signalDim systemDim systemDim
          operator
          signalIndex).PointwiseEq
      target) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
    systemDim (signalDim * systemDim)

Convert a signal-register projection proof into an exact clean-block certificate.

Theorem6.11.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exact clean block of signal projection 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. 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/TeachingRouteClosures.lean:166. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.19●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection_correct
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim)
  (target : QuantumBlockEncoding.Matrix systemDim systemDim ℚ)
  (projectionProof :
    (QuantumBlockEncoding.signalSystemBlockProjection signalDim
          systemDim systemDim operator signalIndex).PointwiseEq
      target) :
  (QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection
          operator signalIndex target projectionProof).clean.PointwiseEq
    target

theorem QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection_correct
  {signalDim systemDim : ℕ}
  (operator :
    QuantumBlockEncoding.Matrix
      (signalDim * systemDim)
      (signalDim * systemDim) ℚ)
  (signalIndex : Fin signalDim)
  (target :
    QuantumBlockEncoding.Matrix systemDim
      systemDim ℚ)
  (projectionProof :
    (QuantumBlockEncoding.signalSystemBlockProjection
          signalDim systemDim systemDim
          operator
          signalIndex).PointwiseEq
      target) :
  (QuantumBlockEncoding.ConcreteSemantics.exactCleanBlockOfSignalProjection
          operator signalIndex target
          projectionProof).clean.PointwiseEq
    target

Definition6.11.20

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “certified circuit block extraction”. A proposition-valued field is a requirement until a constructor supplies it. A circuit block extraction whose selected block equality is carried as a proof.

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 circuit block extraction whose selected block equality is carried as a proof.

Declaration kind. structure.

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

Lean code for Definition6.11.20●1 definition

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

complete

structure QuantumBlockEncoding.CertifiedCircuitBlockExtraction
  (qubits dim signalDim : ℕ) : Type

structure QuantumBlockEncoding.CertifiedCircuitBlockExtraction
  (qubits dim signalDim : ℕ) : Type

A circuit block extraction whose selected block equality is carried as a proof.

Fields

semantics : QuantumBlockEncoding.CircuitMatrixSemantics ℚ qubits

dimCompat : QuantumBlockEncoding.qubitDim qubits = signalDim * dim

targetMatrix : QuantumBlockEncoding.Matrix dim dim ℚ

normalizer : ℚ

normalizer_ne_zero : self.normalizer ≠ 0

signalIndex : Fin signalDim

blockProof : ∀ (row column : Fin dim),
  QuantumBlockEncoding.signalSystemBlockProjection signalDim dim dim (cast ⋯ self.semantics.matrix) self.signalIndex row
      column =
    self.targetMatrix row column / self.normalizer

Definition6.11.21

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.11.21●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  QuantumBlockEncoding.BlockExtractionTarget ℚ dim dim signalDim

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  QuantumBlockEncoding.BlockExtractionTarget
    ℚ dim dim signalDim

Definition6.11.22

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.11.22●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.normalizedTarget
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  QuantumBlockEncoding.Matrix dim dim ℚ

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.normalizedTarget
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  QuantumBlockEncoding.Matrix dim dim ℚ

Definition6.11.23

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.11.23●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock dim
    (signalDim * dim)

def QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
    dim (signalDim * dim)

Theorem6.11.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.24●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget_blockProjection_proved
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  certificate.extractionTarget.blockProjection.proved = true

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget_blockProjection_proved
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  certificate.extractionTarget.blockProjection.proved =
    true

Theorem6.11.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.25●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget_blockCorrect_proved
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  certificate.extractionTarget.blockCorrect.proved = true

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.extractionTarget_blockCorrect_proved
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  certificate.extractionTarget.blockCorrect.proved =
    true

Theorem6.11.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exact clean block 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. 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/TeachingRouteClosures.lean:238. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.26●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock_correct
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction qubits dim
      signalDim) :
  certificate.exactCleanBlock.clean.PointwiseEq
    certificate.normalizedTarget

theorem QuantumBlockEncoding.CertifiedCircuitBlockExtraction.exactCleanBlock_correct
  {qubits dim signalDim : ℕ}
  (certificate :
    QuantumBlockEncoding.CertifiedCircuitBlockExtraction
      qubits dim signalDim) :
  certificate.exactCleanBlock.clean.PointwiseEq
    certificate.normalizedTarget

Definition6.11.27

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “teaching identity circuit semantics”. Empty-circuit semantics on the one-dimensional zero-qubit space.

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. Empty-circuit semantics on the one-dimensional zero-qubit space.

Declaration kind. def.

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

Lean code for Definition6.11.27●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.teachingIdentityCircuitSemantics :
  QuantumBlockEncoding.CircuitMatrixSemantics ℚ 0

def QuantumBlockEncoding.teachingIdentityCircuitSemantics :
  QuantumBlockEncoding.CircuitMatrixSemantics
    ℚ 0

Empty-circuit semantics on the one-dimensional zero-qubit space.

Definition6.11.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “teaching identity block extraction”. Finite witness for certified circuit block extraction.

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. Finite witness for certified circuit block extraction.

Declaration kind. def.

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

Lean code for Definition6.11.28●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.teachingIdentityBlockExtraction :
  QuantumBlockEncoding.CertifiedCircuitBlockExtraction 0 1 1

def QuantumBlockEncoding.teachingIdentityBlockExtraction :
  QuantumBlockEncoding.CertifiedCircuitBlockExtraction
    0 1 1

Finite witness for certified circuit block extraction.

Theorem6.11.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “teaching identity block extraction 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. 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/TeachingRouteClosures.lean:263. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.11.29●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.teachingIdentityBlockExtraction_correct :
  QuantumBlockEncoding.teachingIdentityBlockExtraction.exactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.teachingIdentityBlockExtraction.normalizedTarget

theorem QuantumBlockEncoding.teachingIdentityBlockExtraction_correct :
  QuantumBlockEncoding.teachingIdentityBlockExtraction.exactCleanBlock.clean.PointwiseEq
    QuantumBlockEncoding.teachingIdentityBlockExtraction.normalizedTarget

Definition6.11.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “certify”. Promote an operator candidate only after its unitary and block proofs are supplied.

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 an operator candidate only after its unitary and block proofs are supplied.

Declaration kind. def.

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

Lean code for Definition6.11.30●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.OperatorBlockEncodingCandidate.certify.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate α systemQubits)
  (unitaryProof : candidate.isUnitary)
  (blockProof : candidate.blockContainsTarget) :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding α systemQubits

def QuantumBlockEncoding.OperatorBlockEncodingCandidate.certify.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate
      α systemQubits)
  (unitaryProof : candidate.isUnitary)
  (blockProof :
    candidate.blockContainsTarget) :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    α systemQubits

Promote an operator candidate only after its unitary and block proofs are supplied.

Theorem6.11.31

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.31●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost_eq_fromLayoutAndResource.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate α
      systemQubits) :
  candidate.cost =
    QuantumBlockEncoding.BlockEncodingCost.fromLayoutAndResource
      candidate.layout candidate.resource

theorem QuantumBlockEncoding.OperatorBlockEncodingCandidate.cost_eq_fromLayoutAndResource.{u_1}
  {α : Type u_1} {systemQubits : ℕ}
  (candidate :
    QuantumBlockEncoding.OperatorBlockEncodingCandidate
      α systemQubits) :
  candidate.cost =
    QuantumBlockEncoding.BlockEncodingCost.fromLayoutAndResource
      candidate.layout candidate.resource

Definition6.11.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “identity”. Degree-one identity consumer: a proved clean block is returned unchanged.

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. Degree-one identity consumer: a proved clean block is returned unchanged.

Declaration kind. def.

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

Lean code for Definition6.11.32●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract system
    total

def QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
    system total

Degree-one identity consumer: a proved clean block is returned unchanged.

Theorem6.11.33

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.33●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity_sideConditions
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  (QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
      input).sideConditions

theorem QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity_sideConditions
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  (QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
      input).sideConditions

Theorem6.11.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.11.34●1 theorem

theoremdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

theorem QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity_output
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock system
      total) :
  (QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
      input).outputStatement

theorem QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity_output
  {system total : ℕ}
  (input :
    QuantumBlockEncoding.BlockEncodingClassics.ExactCleanBlock
      system total) :
  (QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract.identity
      input).outputStatement

Definition6.11.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “teaching identity qsvt consumer”. Finite witness that a certified clean block crosses the typed QSVT boundary.

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. Finite witness that a certified clean block crosses the typed QSVT boundary.

Declaration kind. def.

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

Lean code for Definition6.11.35●1 definition

defdefined in QuantumBlockEncoding/TeachingRouteClosures.lean

complete

def QuantumBlockEncoding.teachingIdentityQSVTConsumer :
  QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract 1 1

def QuantumBlockEncoding.teachingIdentityQSVTConsumer :
  QuantumBlockEncoding.BlockEncodingClassics.QSVTConsumerContract
    1 1

Finite witness that a certified clean block crosses the typed QSVT boundary.