ASPBE Lean Blueprint

10.30. QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean🔗

28 explicit public declarations, in source order.

Definition10.30.1
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.1●1 definition
Theorem10.30.2
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm slot)
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm
      slot)
Definition10.30.3
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.3●1 definition
Definition10.30.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry xor weight”.

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

Lean code for Definition10.30.4●1 definition
Definition10.30.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin symmetry xor amplitude”.

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

Lean code for Definition10.30.5●1 definition
Theorem10.30.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry xor amplitude bounded”; 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/SymmetryXorFourSlotLogicalUnitary.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.30.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorAmplitude_bounded
  (sector : Fin 2) (slot column : Fin 4) :
  |QuantumBlockEncoding.Robin.warmRobinSymmetryXorAmplitude sector slot
        column| ≤
    1
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorAmplitude_bounded
  (sector : Fin 2) (slot column : Fin 4) :
  |QuantumBlockEncoding.Robin.warmRobinSymmetryXorAmplitude
        sector slot column| ≤
    1
Theorem10.30.7
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin symmetry xor decomposition”; 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/SymmetryXorFourSlotLogicalUnitary.lean:43. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.30.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorDecomposition
  (sector : Fin 2) (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetrySectorBlock sector row
      column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm slot
              column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryXorWeight sector
          slot column
      else 0
    theorem QuantumBlockEncoding.Robin.warmRobinSymmetryXorDecomposition
  (sector : Fin 2) (row column : Fin 4) :
  QuantumBlockEncoding.Robin.warmRobinSymmetrySectorBlock
      sector row column =
    ∑ slot,
      if
          QuantumBlockEncoding.Robin.warmRobinSymmetryXorPerm
              slot column =
            row then
        QuantumBlockEncoding.Robin.warmRobinSymmetryXorWeight
          sector slot column
      else 0
Definition10.30.8
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.8●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm (slot : Fin 4)
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm
  (slot : Fin 4)
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
Theorem10.30.9
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm slot)
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm_bijective
  (slot : Fin 4) :
  Function.Bijective
    (QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm
      slot)
Definition10.30.10
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.10●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv
  (slot : Fin 4) :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv
  (slot : Fin 4) :
  QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ≃
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
Theorem10.30.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot 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/SymmetryXorFourSlotLogicalUnitary.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.30.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv_apply
  (slot : Fin 4)
  (index : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  (QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv slot)
      index =
    QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm slot index
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv_apply
  (slot : Fin 4)
  (index :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  (QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemEquiv
        slot)
      index =
    QuantumBlockEncoding.Robin.warmRobinXorFourSlotSystemPerm
      slot index
Definition10.30.12
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.12●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) : ℝ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  ℝ
Theorem10.30.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot 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/SymmetryXorFourSlotLogicalUnitary.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.30.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient_abs_le_one
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  |QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient slot
        column| ≤
    1
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient_abs_le_one
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  |QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient
        slot column| ≤
    1
Definition10.30.14
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.14●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  Matrix (Fin 2) (Fin 2) ℂ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  Matrix (Fin 2) (Fin 2) ℂ
Theorem10.30.15
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation_unitary
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation slot column ∈
    Matrix.unitaryGroup (Fin 2) ℂ
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation_unitary
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation
      slot column ∈
    Matrix.unitaryGroup (Fin 2) ℂ
Theorem10.30.16
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation_cleanEntry
  (slot : Fin 4)
  (column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation slot column 0
      0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient slot
        column)
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation_cleanEntry
  (slot : Fin 4)
  (column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotRotation
      slot column 0 0 =
    ↑(QuantumBlockEncoding.Robin.warmRobinXorFourSlotCoefficient
        slot column)
Definition10.30.17
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.17●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ
Theorem10.30.18
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot middle 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/SymmetryXorFourSlotLogicalUnitary.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.30.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ
Definition10.30.19
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin xor four slot sector clean formula”.

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

Lean code for Definition10.30.19●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula :
  Matrix QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem ℚ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula :
  Matrix
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem
    ℚ
Theorem10.30.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot clean formula eq target”; the hypotheses and conclusion in the code panel fix its exact scope.

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

Why it is in this chapter. 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/SymmetryXorFourSlotLogicalUnitary.lean:128. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.30.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotCleanFormula_eq_target
  (row column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula row
      column =
    QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTarget row column
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotCleanFormula_eq_target
  (row column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula
      row column =
    QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTarget
      row column
Theorem10.30.21
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_cleanEntry
  (row column : QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula
        row column)
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_cleanEntry
  (row column :
    QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary
      (0, 0, row) (0, 0, column) =
    ↑(QuantumBlockEncoding.Robin.warmRobinXorFourSlotSectorCleanFormula
        row column)
Theorem10.30.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot middle logical unitary clean system 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/SymmetryXorFourSlotLogicalUnitary.lean:178. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.30.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary
      0 0 =
    fun row column =>
    ↑(QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTarget row
        column)
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinXorFourSlotMiddleLogicalUnitary
      0 0 =
    fun row column =>
    ↑(QuantumBlockEncoding.Robin.warmRobinFourSlotSectorTarget
        row column)
Definition10.30.23
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.30.23●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      (Fin 2) (Fin 4)
      QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
    ℂ
Theorem10.30.24
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        (Fin 2) (Fin 4)
        QuantumBlockEncoding.Robin.WarmRobinSymmetrySystem)
      ℂ
Theorem10.30.25
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “warm robin xor four slot pair logical unitary clean system 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/SymmetryXorFourSlotLogicalUnitary.lean:202. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.30.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary
      0 0 =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary_cleanSystemBlock :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      QuantumBlockEncoding.Robin.warmRobinXorFourSlotPairLogicalUnitary
      0 0 =
    QuantumBlockEncoding.Robin.warmRobinPairNormalizedTargetComplex
Definition10.30.26
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “warm robin xor four slot 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/SymmetryXorFourSlotLogicalUnitary.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.30.26●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary :
  Matrix (Fin (QuantumBlockEncoding.gridSize 6))
    (Fin (QuantumBlockEncoding.gridSize 6)) ℂ
    def QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize 6))
    (Fin
      (QuantumBlockEncoding.gridSize 6))
    ℂ
Theorem10.30.27
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize 6)) ℂ
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary_unitary :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize 6))
      ℂ
Theorem10.30.28
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.30.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SymmetryXorFourSlotLogicalUnitary.lean
    complete
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)
    theorem QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary_cleanBlock
  (row column : Fin 8) :
  QuantumBlockEncoding.Robin.warmRobinXorFourSlotFlatUnitary
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
        row)
      (QuantumBlockEncoding.Robin.warmRobinFourSlotCleanIndex
        column) =
    ↑(QuantumBlockEncoding.RobinEvolution.warmRobinTarget
          row column /
        QuantumBlockEncoding.RobinEvolution.warmRobinNormalizer)