PaperSevenLogicalUnitary.lean🔗

27 explicit public declarations, in source order.

Definition10.17.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 system perm”.

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/PaperSevenLogicalUnitary.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.17.1●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm
  (slot column : Fin 8) : Fin 8

def QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm
  (slot column : Fin 8) : Fin 8

Theorem10.17.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven system perm bijective”; 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/PaperSevenLogicalUnitary.lean:23. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm slot)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm_bijective
  (slot : Fin 8) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemPerm
      slot)

Definition10.17.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 system equiv”.

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

Lean code for Definition10.17.3●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven system equiv apply”; 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/PaperSevenLogicalUnitary.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.17.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemEquiv_apply
  (slot column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemEquiv slot)
      column =
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow slot column

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemEquiv_apply
  (slot column : Fin 8) :
  (QuantumBlockEncoding.Robin.warmRobinPaperSevenSystemEquiv
        slot)
      column =
    QuantumBlockEncoding.Robin.warmRobinSourceDTRow
      slot column

Definition10.17.5

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.17.5●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat
  (slot column : Fin 8) : ℚ

def QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat
  (slot column : Fin 8) : ℚ

Theorem10.17.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven coefficient rat 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/PaperSevenLogicalUnitary.lean:40. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat slot
        column| ≤
    1

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficientRat
        slot column| ≤
    1

Definition10.17.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.17.7●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.17.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient slot
        column| ≤
    1

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient_abs_le_one
  (slot column : Fin 8) :
  |QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient
        slot column| ≤
    1

Definition10.17.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven 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. 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/PaperSevenLogicalUnitary.lean:57. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.17.9●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven 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/PaperSevenLogicalUnitary.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.17.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.17.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation_cleanEntry
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation slot column 0
      0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient slot
        column)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation_cleanEntry
  (slot column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenRotation
      slot column 0 0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinPaperSevenCoefficient
        slot column)

Definition10.17.12

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.17.12●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.17.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven logical unitary 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/PaperSevenLogicalUnitary.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.17.14●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula row
        column)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary_cleanEntry
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinSourceSevenCleanFormula
        row column)

Theorem10.17.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven logical unitary clean block”; 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/PaperSevenLogicalUnitary.lean:135. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary_cleanBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary 0 0 =
    fun row column =>
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary_cleanBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinPaperSevenLogicalUnitary
      0 0 =
    fun row column =>
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

Definition10.17.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven index equiv”. Flatten coefficient, selector, and system registers 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. Flatten coefficient, selector, and system registers to seven qubits.

Declaration kind. def.

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

Lean code for Definition10.17.16●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Flatten coefficient, selector, and system registers to seven qubits.

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

Lean code for Definition10.17.17●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Definition10.17.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 flat unitary”.

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

Lean code for Definition10.17.18●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Theorem10.17.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.17.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 7)) ℂ

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 7))
      ℂ

Theorem10.17.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin paper seven flat unitary clean block”; 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/PaperSevenLogicalUnitary.lean:167. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.17.20●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenCleanIndex row)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinPaperSevenCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)

Definition10.17.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven 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/PaperSevenLogicalUnitary.lean:183. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.17.21●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget : Prop

def QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget :
  Prop

Theorem10.17.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.17.22●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget

theorem QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget_proof :
  QuantumBlockEncoding.Robin.warmRobinPaperSevenBlockContainsTarget

Definition10.17.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven t 2 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. 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/PaperSevenLogicalUnitary.lean:197. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.17.23●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Schedule :
  QuantumBlockEncoding.LayeredCircuit

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Schedule :
  QuantumBlockEncoding.LayeredCircuit

Definition10.17.24

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.17.24●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Circuit :
  QuantumBlockEncoding.Circuit

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Circuit :
  QuantumBlockEncoding.Circuit

Definition10.17.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven t 2 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/PaperSevenLogicalUnitary.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.17.25●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Resource :
  QuantumBlockEncoding.Resource

def QuantumBlockEncoding.Robin.warmRobinPaperSevenT2Resource :
  QuantumBlockEncoding.Resource

Definition10.17.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin paper seven 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/PaperSevenLogicalUnitary.lean:209. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.17.26●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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

Definition10.17.27

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.17.27●1 definition

defdefined in QuantumBlockEncoding/Robin/PaperSevenLogicalUnitary.lean

complete

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

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