PaperSevenT3.lean🔗

19 explicit public declarations, in source order.

Definition10.21.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven selector prepare program”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

Theorem10.21.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven selector prepare program eval”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram_eval :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepareProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      (QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
        QuantumBlockEncoding.Robin.warmRobinPaperSevenSelectorPrepare)

Definition10.21.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive program”. Chronological exact primitive source program.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Chronological exact primitive source program.

Declaration kind. def.

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

Lean code for Definition10.21.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram :
  QuantumBlockEncoding.PrimitiveProgram 8

Chronological exact primitive source program.

Theorem10.21.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive eval eq logical”; the hypotheses and conclusion in the code panel fix its exact scope. Required T3 semantic root.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Required T3 semantic root. Equality includes the exact accumulated global phase and uses the actual reversible extension on dirty 'q7'.

Declaration kind. theorem.

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

Lean code for Theorem10.21.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_eval_eq_logical :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_eval_eq_logical :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram =
    (Matrix.reindexAlgEquiv ℂ ℂ
        QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv.symm)
      QuantumBlockEncoding.Robin.warmRobinPaperSevenWorkspaceLogicalUnitary

Required T3 semantic root.  Equality includes the exact accumulated global
phase and uses the actual reversible extension on dirty `q7`.

Theorem10.21.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven bits equiv encode”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv_encode
  (coefficient : Fin 2) (selector : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenEncodeBits
        coefficient selector system) =
    (coefficient, selector, system)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv_encode
  (coefficient : Fin 2) (selector : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBitsEquiv
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenEncodeBits
        coefficient selector system) =
    (coefficient, selector, system)

Definition10.21.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive flat unitary”. Flat eight-qubit unitary used by the operator-first block-encoding API.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Flat eight-qubit unitary used by the operator-first block-encoding API.

Declaration kind. def.

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

Lean code for Definition10.21.6●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 8))
    (Fin (QuantumBlockEncoding.gridSize 8)) ℂ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 8))
    (Fin
      (QuantumBlockEncoding.gridSize 8))
    ℂ

Flat eight-qubit unitary used by the operator-first block-encoding API.

Theorem10.21.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive flat unitary 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 8)) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 8))
      ℂ

Definition10.21.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive clean index”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.8●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
  (system : Fin 8) : Fin (QuantumBlockEncoding.gridSize 8)

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
  (system : Fin 8) :
  Fin (QuantumBlockEncoding.gridSize 8)

Theorem10.21.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The physical primitive program has the exact 'M/224 = A/(56/3)' clean block; no numerical matrix comparison is used.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. The physical primitive program has the exact 'M/224 = A/(56/3)' clean block; no numerical matrix comparison is used.

Declaration kind. theorem.

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

Lean code for Theorem10.21.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

The physical primitive program has the exact `M/224 = A/(56/3)` clean
block; no numerical matrix comparison is used.

Definition10.21.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive block contains 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.10●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget :
  Prop

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget :
  Prop

Theorem10.21.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive block contains target proof”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveBlockContainsTarget

Theorem10.21.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven full system equiv workspace”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_workspace
  (slot : Fin 8)
  (system : QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  ((QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv slot)
        system).2 =
    system.2

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv_workspace
  (slot : Fin 8)
  (system :
    QuantumBlockEncoding.Robin.WarmRobinPaperSevenFullSystem) :
  ((QuantumBlockEncoding.Robin.warmRobinPaperSevenFullSystemEquiv
          slot)
        system).2 =
    system.2

Theorem10.21.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive workspace clean”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix-level workspace restoration: a clean input column has no amplitude on a dirty workspace output row.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Matrix-level workspace restoration: a clean input column has no amplitude on a dirty workspace output row.

Declaration kind. theorem.

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

Lean code for Theorem10.21.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_workspaceClean
  (row column : QuantumBlockEncoding.PrimitiveBasis 8)
  (columnClean : column 7 = 0) (rowDirty : row 7 ≠ 0) :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram row
      column =
    0

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_workspaceClean
  (row column :
    QuantumBlockEncoding.PrimitiveBasis 8)
  (columnClean : column 7 = 0)
  (rowDirty : row 7 ≠ 0) :
  QuantumBlockEncoding.evalPrimitiveProgram
      QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram
      row column =
    0

Matrix-level workspace restoration: a clean input column has no amplitude
on a dirty workspace output row.

Definition10.21.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive presentation”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.14●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitivePresentation :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitivePresentation :
  QuantumBlockEncoding.Circuit

Definition10.21.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.15●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource :
  QuantumBlockEncoding.Resource

Theorem10.21.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven primitive resource faithful”; 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Theorem10.21.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_resource_faithful :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram.circuit.resource

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitive_resource_faithful :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveResource =
    QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveProgram.circuit.resource

Definition10.21.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive operator candidate”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.17●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate ℂ 3

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveOperatorCandidate :
  QuantumBlockEncoding.OperatorBlockEncodingCandidate
    ℂ 3

Definition10.21.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive refinement”.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

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

Lean code for Definition10.21.18●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveRefinement :
  QuantumBlockEncoding.PrimitiveProgramRefinement 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveRefinement :
  QuantumBlockEncoding.PrimitiveProgramRefinement
    8

Definition10.21.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven primitive verified block encoding”. Exact primitive verified block encoding for the paper-seven source route.

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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Exact primitive verified block encoding for the paper-seven source route.

Declaration kind. def.

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

Lean code for Definition10.21.19●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenT3.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding ℂ 3

def QuantumBlockEncoding.Robin.warmRobinPaperSevenPrimitiveVerifiedBlockEncoding :
  QuantumBlockEncoding.VerifiedOperatorBlockEncoding
    ℂ 3

Exact primitive verified block encoding for the paper-seven source route.