Hadamard8BlockEncoding.lean🔗

24 explicit public declarations, in source order.

Definition10.14.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 index equiv”. Flatten coefficient × selector × system into the seven-qubit basis.

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. Flatten coefficient × selector × system into the seven-qubit basis.

Declaration kind. def.

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

Lean code for Definition10.14.1●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      (Fin 8) ≃
    Fin (QuantumBlockEncoding.gridSize 7)

def QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8) (Fin 8) ≃
    Fin (QuantumBlockEncoding.gridSize 7)

Flatten coefficient × selector × system into the seven-qubit basis.

Definition10.14.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 clean index”. The clean coefficient/selector branch embedded in the flat seven-qubit basis.

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 clean coefficient/selector branch embedded in the flat seven-qubit basis.

Declaration kind. def.

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

Lean code for Definition10.14.2●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex
  (system : Fin 8) : Fin (QuantumBlockEncoding.gridSize 7)

def QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex
  (system : Fin 8) :
  Fin (QuantumBlockEncoding.gridSize 7)

The clean coefficient/selector branch embedded in the flat seven-qubit basis.

Theorem10.14.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 clean index value”; 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/Hadamard8BlockEncoding.lean:31. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.14.3●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex_value
  (system : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex system) =
    ↑system

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex_value
  (system : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex
        system) =
    ↑system

Definition10.14.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 flat unitary”. The product-register logical unitary reindexed as a seven-qubit matrix.

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

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

Technical source note. The product-register logical unitary reindexed as a seven-qubit matrix.

Declaration kind. def.

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

Lean code for Definition10.14.4●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 7))
    (Fin (QuantumBlockEncoding.gridSize 7)) ℂ

def QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 7))
    (Fin
      (QuantumBlockEncoding.gridSize 7))
    ℂ

The product-register logical unitary reindexed as a seven-qubit matrix.

Theorem10.14.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing preserves the exact Mathlib unitary-group certificate.

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. Reindexing preserves the exact Mathlib unitary-group certificate.

Declaration kind. theorem.

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

Lean code for Theorem10.14.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 7)) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 7))
      ℂ

Reindexing preserves the exact Mathlib unitary-group certificate.

Theorem10.14.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Applying the reindexed matrix at reindexed indices recovers the product entry.

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

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

Technical source note. Applying the reindexed matrix at reindexed indices recovers the product entry.

Declaration kind. theorem.

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

Lean code for Theorem10.14.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_reindex
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      (Fin 8)) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv row)
      (QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv column) =
    QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary row
      column

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_reindex
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8) (Fin 8)) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv
        row)
      (QuantumBlockEncoding.Robin.warmRobinHadamard8IndexEquiv
        column) =
    QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary
      row column

Applying the reindexed matrix at reindexed indices recovers the product entry.

Theorem10.14.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform bit prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Every row of the one-bit PREPARE has the same clean-column amplitude.

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. Every row of the one-bit PREPARE has the same clean-column amplitude.

Declaration kind. theorem.

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

Lean code for Theorem10.14.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare_cleanColumn
  (bit : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare bit 0 =
    ↑(√2 / 2)

theorem QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare_cleanColumn
  (bit : Fin 2) :
  QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare
      bit 0 =
    ↑(√2 / 2)

Every row of the one-bit PREPARE has the same clean-column amplitude.

Theorem10.14.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard bits prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. The three-bit tensor PREPARE has a uniform clean column.

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

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

Technical source note. The three-bit tensor PREPARE has a uniform clean column.

Declaration kind. theorem.

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

Lean code for Theorem10.14.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare_cleanColumn
  (bits : QuantumBlockEncoding.Robin.WarmRobinHadamardBits) :
  QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare bits
      (0, 0, 0) =
    ↑(√2 / 2) * ↑(√2 / 2) * ↑(√2 / 2)

theorem QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare_cleanColumn
  (bits :
    QuantumBlockEncoding.Robin.WarmRobinHadamardBits) :
  QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare
      bits (0, 0, 0) =
    ↑(√2 / 2) * ↑(√2 / 2) * ↑(√2 / 2)

The three-bit tensor PREPARE has a uniform clean column.

Theorem10.14.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 selector prepare clean column”; the hypotheses and conclusion in the code panel fix its exact scope. The flattened selector PREPARE still has a uniform clean column.

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

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

Technical source note. The flattened selector PREPARE still has a uniform clean column.

Declaration kind. theorem.

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

Lean code for Theorem10.14.9●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_cleanColumn
  (slot : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare slot 0 =
    ↑(√2 / 2) * ↑(√2 / 2) * ↑(√2 / 2)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_cleanColumn
  (slot : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare
      slot 0 =
    ↑(√2 / 2) * ↑(√2 / 2) * ↑(√2 / 2)

The flattened selector PREPARE still has a uniform clean column.

Theorem10.14.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 selector prepare probability”; the hypotheses and conclusion in the code panel fix its exact scope. Squared magnitude of each selector amplitude is exactly '1/8'.

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. Squared magnitude of each selector amplitude is exactly '1/8'.

Declaration kind. theorem.

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

Lean code for Theorem10.14.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_probability
  (slot : Fin 8) :
  star
        (QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare
          slot 0) *
      QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare slot
        0 =
    1 / 8

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_probability
  (slot : Fin 8) :
  star
        (QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare
          slot 0) *
      QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare
        slot 0 =
    1 / 8

Squared magnitude of each selector amplitude is exactly `1/8`.

Theorem10.14.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 coefficient complex”; the hypotheses and conclusion in the code panel fix its exact scope. Rational and real-complex views of a slot coefficient agree.

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. Rational and real-complex views of a slot coefficient agree.

Declaration kind. theorem.

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

Lean code for Theorem10.14.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient_complex
  (slot column : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient slot
        column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude slot
        column)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient_complex
  (slot column : Fin 8) :
  ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient
        slot column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinEightSlotAmplitude
        slot column)

Rational and real-complex views of a slot coefficient agree.

Theorem10.14.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. The reusable clean-entry expansion specializes to the Robin eight-slot formula.

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 reusable clean-entry expansion specializes to the Robin eight-slot formula.

Declaration kind. theorem.

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

Lean code for Theorem10.14.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8CleanFormula row
        column)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8CleanFormula
        row column)

The reusable clean-entry expansion specializes to the Robin eight-slot formula.

Theorem10.14.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary clean entry eq target”; the hypotheses and conclusion in the code panel fix its exact scope. The product-register clean entry is the normalized fixed Robin target.

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 product-register clean entry is the normalized fixed Robin target.

Declaration kind. theorem.

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

Lean code for Theorem10.14.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_cleanEntry_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_cleanEntry_eq_target
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

The product-register clean entry is the normalized fixed Robin target.

Theorem10.14.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 flat unitary clean block”; the hypotheses and conclusion in the code panel fix its exact scope. The flat seven-qubit clean block is the normalized fixed Robin operator.

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 flat seven-qubit clean block is the normalized fixed Robin operator.

Declaration kind. theorem.

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

Lean code for Theorem10.14.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex row)
      (QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8FlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinHadamard8CleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

The flat seven-qubit clean block is the normalized fixed Robin operator.

Definition10.14.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin complex target”. Complex view of the fixed Robin target used by the operator-first 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. Complex view of the fixed Robin target used by the operator-first API.

Declaration kind. def.

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

Lean code for Definition10.14.15●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinComplexTarget :
  QuantumBlockEncoding.Matrix 8 8 ℂ

def QuantumBlockEncoding.Robin.warmRobinComplexTarget :
  QuantumBlockEncoding.Matrix 8 8 ℂ

Complex view of the fixed Robin target used by the operator-first API.

Definition10.14.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin query target”. Operator-first target contract for the fixed homogeneous Robin benchmark.

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. Operator-first target contract for the fixed homogeneous Robin benchmark.

Declaration kind. def.

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

Lean code for Definition10.14.16●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget ℂ 8 8

def QuantumBlockEncoding.Robin.warmRobinQueryTarget :
  QuantumBlockEncoding.QueryOperatorTarget
    ℂ 8 8

Operator-first target contract for the fixed homogeneous Robin benchmark.

Definition10.14.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 schedule”. Four logical stages with the three selector Hadamards made explicit.

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. Four logical stages with the three selector Hadamards made explicit.

Declaration kind. def.

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

Lean code for Definition10.14.17●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Schedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Schedule :
  QuantumBlockEncoding.LayeredCircuit

Four logical stages with the three selector Hadamards made explicit.

Definition10.14.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 circuit”. Logical gate list associated with the fair T2 schedule.

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. Logical gate list associated with the fair T2 schedule.

Declaration kind. def.

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

Lean code for Definition10.14.18●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Circuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Circuit :
  QuantumBlockEncoding.Circuit

Logical gate list associated with the fair T2 schedule.

Definition10.14.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 t 2 resource”. Resource record under the logical-stage convention, not a T3 primitive count.

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. Resource record under the logical-stage convention, not a T3 primitive count.

Declaration kind. def.

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

Lean code for Definition10.14.19●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Resource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Robin.warmRobinHadamard8T2Resource :
  QuantumBlockEncoding.Resource

Resource record under the logical-stage convention, not a T3 primitive count.

Definition10.14.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 block contains target”. The exact block predicate attached to the 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 exact block predicate attached to the operator candidate.

Declaration kind. def.

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

Lean code for Definition10.14.20●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget : Prop

def QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget :
  Prop

The exact block predicate attached to the operator candidate.

Theorem10.14.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 block contains target proof”; the hypotheses and conclusion in the code panel fix its exact scope. The clean-block predicate follows from the specialized clean-entry theorem.

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 clean-block predicate follows from the specialized clean-entry theorem.

Declaration kind. theorem.

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

Lean code for Theorem10.14.21●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinHadamard8BlockContainsTarget

The clean-block predicate follows from the specialized clean-entry theorem.

Definition10.14.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 operator candidate”. Fixed 'N=8' Hadamard-8 candidate at the exact logical-unitary tier.

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. Fixed 'N=8' Hadamard-8 candidate at the exact logical-unitary tier.

Declaration kind. def.

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

Lean code for Definition10.14.22●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

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

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

Fixed `N=8` Hadamard-8 candidate at the exact logical-unitary tier.

Definition10.14.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 verified block encoding”. Fully verified T2 block encoding of the fixed Robin matrix.

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

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

Technical source note. Fully verified T2 block encoding of the fixed Robin matrix.

Declaration kind. def.

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

Lean code for Definition10.14.23●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

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

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

Fully verified T2 block encoding of the fixed Robin matrix.

Definition10.14.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 t 3 blocked leaf”. Honest boundary: primitive synthesis/refinement is still a separate T3 theorem.

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. Honest boundary: primitive synthesis/refinement is still a separate T3 theorem.

Declaration kind. def.

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

Lean code for Definition10.14.24●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8BlockEncoding.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8T3BlockedLeaf : String

def QuantumBlockEncoding.Robin.warmRobinHadamard8T3BlockedLeaf :
  String

Honest boundary: primitive synthesis/refinement is still a separate T3 theorem.