Hadamard8Verified.lean🔗

16 explicit public declarations, in source order.

Definition10.15.1

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “warm robin hadamard bits”. Three binary selector wires before flattening to 'Fin 8'.

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. Three binary selector wires before flattening to 'Fin 8'.

Declaration kind. abbrev.

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

Lean code for Definition10.15.1●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

abbrev QuantumBlockEncoding.Robin.WarmRobinHadamardBits : Type

abbrev QuantumBlockEncoding.Robin.WarmRobinHadamardBits :
  Type

Three binary selector wires before flattening to `Fin 8`.

Definition10.15.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard bits equiv”. Signal-register order used by the eight-slot selector.

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. Signal-register order used by the eight-slot selector.

Declaration kind. def.

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

Lean code for Definition10.15.2●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamardBitsEquiv :
  QuantumBlockEncoding.Robin.WarmRobinHadamardBits ≃ Fin 8

def QuantumBlockEncoding.Robin.warmRobinHadamardBitsEquiv :
  QuantumBlockEncoding.Robin.WarmRobinHadamardBits ≃
    Fin 8

Signal-register order used by the eight-slot selector.

Definition10.15.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin uniform bit prepare”. One uniform binary PREPARE rotation.

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. One uniform binary PREPARE rotation.

Declaration kind. def.

Source: QuantumBlockEncoding/Robin/Hadamard8Verified.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.15.3●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare :
  Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare :
  Matrix (Fin 2) (Fin 2) ℂ

One uniform binary PREPARE rotation.

Theorem10.15.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin uniform bit prepare 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/Hadamard8Verified.lean:32. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.15.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Definition10.15.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard bits prepare”. Tensor product PREPARE on three binary selector wires.

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. Tensor product PREPARE on three binary selector wires.

Declaration kind. def.

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

Lean code for Definition10.15.5●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare :
  Matrix QuantumBlockEncoding.Robin.WarmRobinHadamardBits
    QuantumBlockEncoding.Robin.WarmRobinHadamardBits ℂ

def QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinHadamardBits
    QuantumBlockEncoding.Robin.WarmRobinHadamardBits
    ℂ

Tensor product PREPARE on three binary selector wires.

Theorem10.15.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard bits prepare 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/Hadamard8Verified.lean:46. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.15.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare ∈
    Matrix.unitaryGroup QuantumBlockEncoding.Robin.WarmRobinHadamardBits
      ℂ

theorem QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamardBitsPrepare ∈
    Matrix.unitaryGroup
      QuantumBlockEncoding.Robin.WarmRobinHadamardBits
      ℂ

Definition10.15.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 selector prepare”. The eight-dimensional selector PREPARE in the flattened selector 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 eight-dimensional selector PREPARE in the flattened selector basis.

Declaration kind. def.

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

Lean code for Definition10.15.7●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare :
  Matrix (Fin 8) (Fin 8) ℂ

def QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare :
  Matrix (Fin 8) (Fin 8) ℂ

The eight-dimensional selector PREPARE in the flattened selector basis.

Theorem10.15.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 selector prepare 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/Hadamard8Verified.lean:61. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.15.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare ∈
    Matrix.unitaryGroup (Fin 8) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8SelectorPrepare ∈
    Matrix.unitaryGroup (Fin 8) ℂ

Definition10.15.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 coefficient”. Real clean amplitude used by selector slot and system column.

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. Real clean amplitude used by selector slot and system column.

Declaration kind. def.

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

Lean code for Definition10.15.9●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient
  (slot column : Fin 8) : ℝ

def QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient
  (slot column : Fin 8) : ℝ

Real clean amplitude used by selector slot and system column.

Theorem10.15.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 coefficient abs le one”; 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/Hadamard8Verified.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.15.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient slot
        column| ≤
    1

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient
        slot column| ≤
    1

Definition10.15.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 rotation”. Controlled two-dimensional amplitude 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. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Controlled two-dimensional amplitude block.

Declaration kind. def.

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

Lean code for Definition10.15.11●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation
  (slot column : Fin 8) : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation
  (slot column : Fin 8) :
  Matrix (Fin 2) (Fin 2) ℂ

Controlled two-dimensional amplitude block.

Theorem10.15.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.15.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation_unitary
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation slot column ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation_unitary
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation
      slot column ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Theorem10.15.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.15.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation_cleanEntry
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation slot column 0
      0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient slot
        column)

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation_cleanEntry
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinHadamard8Rotation
      slot column 0 0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinHadamard8Coefficient
        slot column)

Definition10.15.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 system equiv”. Each certified system permutation is packaged as an equivalence.

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. Each certified system permutation is packaged as an equivalence.

Declaration kind. def.

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

Lean code for Definition10.15.14●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8SystemEquiv
  (slot : Fin 8) : Fin 8 ≃ Fin 8

def QuantumBlockEncoding.Robin.warmRobinHadamard8SystemEquiv
  (slot : Fin 8) : Fin 8 ≃ Fin 8

Each certified system permutation is packaged as an equivalence.

Definition10.15.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin hadamard 8 logical unitary”. Product-register matrix before flattening to seven qubits.

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. Product-register matrix before flattening to seven qubits.

Declaration kind. def.

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

Lean code for Definition10.15.15●1 definition

defdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

def QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      (Fin 8))
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
      (Fin 8))
    ℂ

def QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8) (Fin 8))
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 8) (Fin 8))
    ℂ

Product-register matrix before flattening to seven qubits.

Theorem10.15.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin hadamard 8 logical unitary unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete Hadamard-8 logical matrix is a standard complex unitary.

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 complete Hadamard-8 logical matrix is a standard complex unitary.

Declaration kind. theorem.

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

Lean code for Theorem10.15.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/Hadamard8Verified.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 8)
        (Fin 8))
      ℂ

theorem QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinHadamard8LogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        (Fin 2) (Fin 8) (Fin 8))
      ℂ

The complete Hadamard-8 logical matrix is a standard complex unitary.