ASPBE Lean Blueprint

10.49. QuantumBlockEncoding/Robin/SystemConjugation.lean🔗

10 explicit public declarations, in source order.

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

Plain-English reading. This definition gives the library's named construction or computation for “system lift”. Lift a system-register matrix through coefficient and selector identities.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Lift a system-register matrix through coefficient and selector identities.

Declaration kind. def.

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

Lean code for Definition10.49.1●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    def QuantumBlockEncoding.Robin.ComplexLCU.systemLift.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (operator : Matrix system system ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ
    def QuantumBlockEncoding.Robin.ComplexLCU.systemLift.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (operator : Matrix system system ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ
    Lift a system-register matrix through coefficient and selector identities.
Theorem10.49.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “system lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary system operation remains unitary after the identity lifts.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. A unitary system operation remains unitary after the identity lifts.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SystemConjugation.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.49.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_unitary.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (operator : Matrix system system ℂ)
  (unitary : operator ∈ Matrix.unitaryGroup system ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.systemLift operator ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_unitary.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (operator : Matrix system system ℂ)
  (unitary :
    operator ∈
      Matrix.unitaryGroup system ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.systemLift
      operator ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ
    A unitary system operation remains unitary after the identity lifts.
Theorem10.49.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “system lift apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula: coefficient and selector are Kronecker deltas.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Entry formula: coefficient and selector are Kronecker deltas.

Declaration kind. theorem.

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

Lean code for Theorem10.49.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_apply.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (operator : Matrix system system ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  QuantumBlockEncoding.Robin.ComplexLCU.systemLift operator row column =
    if row.1 = column.1 ∧ row.2.1 = column.2.1 then
      operator row.2.2 column.2.2
    else 0
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (operator : Matrix system system ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  QuantumBlockEncoding.Robin.ComplexLCU.systemLift
      operator row column =
    if
        row.1 = column.1 ∧
          row.2.1 = column.2.1 then
      operator row.2.2 column.2.2
    else 0
    Entry formula: coefficient and selector are Kronecker deltas.
Theorem10.49.4
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “star system lift apply”; the hypotheses and conclusion in the code panel fix its exact scope. Entry formula for the adjoint system lift.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Entry formula for the adjoint system lift.

Declaration kind. theorem.

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

Lean code for Theorem10.49.4●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.star_systemLift_apply.{u_1, u_2,
    u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (operator : Matrix system system ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system) :
  star (QuantumBlockEncoding.Robin.ComplexLCU.systemLift operator) row
      column =
    if row.1 = column.1 ∧ row.2.1 = column.2.1 then
      star (operator column.2.2 row.2.2)
    else 0
    theorem QuantumBlockEncoding.Robin.ComplexLCU.star_systemLift_apply.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (operator : Matrix system system ℂ)
  (row column :
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system) :
  star
      (QuantumBlockEncoding.Robin.ComplexLCU.systemLift
        operator)
      row column =
    if
        row.1 = column.1 ∧
          row.2.1 = column.2.1 then
      star (operator column.2.2 row.2.2)
    else 0
    Entry formula for the adjoint system lift.
Theorem10.49.5
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “system lift mul clean row”; the hypotheses and conclusion in the code panel fix its exact scope. Left multiplication by a lifted system matrix on a clean row.

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

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Left multiplication by a lifted system matrix on a clean row.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/SystemConjugation.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.49.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_mul_cleanRow.{u_1, u_2,
    u_3, u_4}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  {columnType : Type u_4} [Fintype coefficient]
  [DecidableEq coefficient] [Fintype selector] [DecidableEq selector]
  [Fintype system] [DecidableEq system] [Fintype columnType]
  (systemOperator : Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      columnType ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemRow : system) (column : columnType) :
  (QuantumBlockEncoding.Robin.ComplexLCU.systemLift systemOperator *
        operator)
      (cleanCoefficient, cleanSelector, systemRow) column =
    ∑ intermediate,
      systemOperator systemRow intermediate *
        operator (cleanCoefficient, cleanSelector, intermediate) column
    theorem QuantumBlockEncoding.Robin.ComplexLCU.systemLift_mul_cleanRow.{u_1,
    u_2, u_3, u_4}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  {columnType : Type u_4}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  [Fintype columnType]
  (systemOperator :
    Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      columnType ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemRow : system)
  (column : columnType) :
  (QuantumBlockEncoding.Robin.ComplexLCU.systemLift
          systemOperator *
        operator)
      (cleanCoefficient, cleanSelector,
        systemRow)
      column =
    ∑ intermediate,
      systemOperator systemRow
          intermediate *
        operator
          (cleanCoefficient,
            cleanSelector, intermediate)
          column
    Left multiplication by a lifted system matrix on a clean row.
Theorem10.49.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mul star system lift clean column”; the hypotheses and conclusion in the code panel fix its exact scope. Right multiplication by the adjoint lift on a clean column.

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

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Right multiplication by the adjoint lift on a clean column.

Declaration kind. theorem.

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

Lean code for Theorem10.49.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.mul_star_systemLift_cleanColumn.{u_1,
    u_2, u_3, u_4}
  {rowType : Type u_1} {coefficient : Type u_2} {selector : Type u_3}
  {system : Type u_4} [Fintype rowType] [Fintype coefficient]
  [DecidableEq coefficient] [Fintype selector] [DecidableEq selector]
  [Fintype system] [DecidableEq system]
  (operator :
    Matrix rowType
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ)
  (systemOperator : Matrix system system ℂ) (row : rowType)
  (cleanCoefficient : coefficient) (cleanSelector : selector)
  (systemColumn : system) :
  (operator *
        star
          (QuantumBlockEncoding.Robin.ComplexLCU.systemLift
            systemOperator))
      row (cleanCoefficient, cleanSelector, systemColumn) =
    ∑ intermediate,
      operator row (cleanCoefficient, cleanSelector, intermediate) *
        star (systemOperator systemColumn intermediate)
    theorem QuantumBlockEncoding.Robin.ComplexLCU.mul_star_systemLift_cleanColumn.{u_1,
    u_2, u_3, u_4}
  {rowType : Type u_1}
  {coefficient : Type u_2}
  {selector : Type u_3}
  {system : Type u_4} [Fintype rowType]
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (operator :
    Matrix rowType
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ)
  (systemOperator :
    Matrix system system ℂ)
  (row : rowType)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector)
  (systemColumn : system) :
  (operator *
        star
          (QuantumBlockEncoding.Robin.ComplexLCU.systemLift
            systemOperator))
      row
      (cleanCoefficient, cleanSelector,
        systemColumn) =
    ∑ intermediate,
      operator row
          (cleanCoefficient,
            cleanSelector, intermediate) *
        star
          (systemOperator systemColumn
            intermediate)
    Right multiplication by the adjoint lift on a clean column.
Definition10.49.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “clean system block”. Extract the coefficient/selector clean block as a system matrix.

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

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Extract the coefficient/selector clean block as a system matrix.

Declaration kind. def.

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

Lean code for Definition10.49.7●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    def QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector) :
  Matrix system system ℂ
    def QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector) :
  Matrix system system ℂ
    Extract the coefficient/selector clean block as a system matrix.
Definition10.49.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “conjugate system”. Conjugate a full logical matrix only on its system register.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Conjugate a full logical matrix only on its system register.

Declaration kind. def.

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

Lean code for Definition10.49.8●1 definition
  • defdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    def QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (systemOperator : Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ
    def QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (systemOperator :
    Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ
    Conjugate a full logical matrix only on its system register.
Theorem10.49.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “conjugate system unitary”; the hypotheses and conclusion in the code panel fix its exact scope. System conjugation preserves unitarity.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. System conjugation preserves unitarity.

Declaration kind. theorem.

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

Lean code for Theorem10.49.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem_unitary.{u_1, u_2,
    u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (systemOperator : Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ)
  (systemUnitary : systemOperator ∈ Matrix.unitaryGroup system ℂ)
  (operatorUnitary :
    operator ∈
      Matrix.unitaryGroup
        (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
          selector system)
        ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem systemOperator
      operator ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ
    theorem QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem_unitary.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (systemOperator :
    Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ)
  (systemUnitary :
    systemOperator ∈
      Matrix.unitaryGroup system ℂ)
  (operatorUnitary :
    operator ∈
      Matrix.unitaryGroup
        (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
          coefficient selector system)
        ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem
      systemOperator operator ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ
    System conjugation preserves unitarity.
Theorem10.49.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “clean system block conjugate system”; the hypotheses and conclusion in the code panel fix its exact scope. Conjugating the full logical matrix conjugates exactly its clean system block.

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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Conjugating the full logical matrix conjugates exactly its clean system block.

Declaration kind. theorem.

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

Lean code for Theorem10.49.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/Robin/SystemConjugation.lean
    complete
    theorem QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock_conjugateSystem.{u_1,
    u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [Fintype coefficient] [DecidableEq coefficient] [Fintype selector]
  [DecidableEq selector] [Fintype system] [DecidableEq system]
  (systemOperator : Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ)
  (cleanCoefficient : coefficient) (cleanSelector : selector) :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      (QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem
        systemOperator operator)
      cleanCoefficient cleanSelector =
    systemOperator *
      (QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock operator
          cleanCoefficient cleanSelector *
        star systemOperator)
    theorem QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock_conjugateSystem.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [Fintype coefficient]
  [DecidableEq coefficient]
  [Fintype selector]
  [DecidableEq selector] [Fintype system]
  [DecidableEq system]
  (systemOperator :
    Matrix system system ℂ)
  (operator :
    Matrix
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ)
  (cleanCoefficient : coefficient)
  (cleanSelector : selector) :
  QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
      (QuantumBlockEncoding.Robin.ComplexLCU.conjugateSystem
        systemOperator operator)
      cleanCoefficient cleanSelector =
    systemOperator *
      (QuantumBlockEncoding.Robin.ComplexLCU.cleanSystemBlock
          operator cleanCoefficient
          cleanSelector *
        star systemOperator)
    Conjugating the full logical matrix conjugates exactly its clean system block.