ComplexLCU.lean🔗

29 explicit public declarations, in source order.

Definition10.4.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “real orthogonal rotation”. A real planar rotation with explicit cosine and sine entries, embedded in 'ℂ'.

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. A real planar rotation with explicit cosine and sine entries, embedded in 'ℂ'.

Declaration kind. def.

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

Lean code for Definition10.4.1●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
  (cosine sine : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
  (cosine sine : ℝ) :
  Matrix (Fin 2) (Fin 2) ℂ

A real planar rotation with explicit cosine and sine entries, embedded in `ℂ`.

Theorem10.4.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real orthogonal rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A real planar rotation is unitary whenever its two entries lie on the unit circle.

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. A real planar rotation is unitary whenever its two entries lie on the unit circle.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/ComplexLCU.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.4.2●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation_unitary
  (cosine sine : ℝ)
  (normalization : cosine * cosine + sine * sine = 1) :
  QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation cosine
      sine ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation_unitary
  (cosine sine : ℝ)
  (normalization :
    cosine * cosine + sine * sine = 1) :
  QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
      cosine sine ∈
    Matrix.unitaryGroup (Fin 2) ℂ

A real planar rotation is unitary whenever its two entries lie on the unit circle.

Definition10.4.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “real rotation”. A real planar rotation, parameterized by an angle.

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. A real planar rotation, parameterized by an angle.

Declaration kind. def.

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

Lean code for Definition10.4.3●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.realRotation (angle : ℝ) :
  Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.realRotation
  (angle : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

A real planar rotation, parameterized by an angle.

Theorem10.4.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real rotation zero zero”; 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/ComplexLCU.lean:64. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.4.4●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_zero_zero
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation angle 0 0 =
    ↑(Real.cos angle)

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_zero_zero
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation
      angle 0 0 =
    ↑(Real.cos angle)

Theorem10.4.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real rotation zero 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/ComplexLCU.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.4.5●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_zero_one
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation angle 0 1 =
    -↑(Real.sin angle)

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_zero_one
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation
      angle 0 1 =
    -↑(Real.sin angle)

Theorem10.4.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real rotation one zero”; 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/ComplexLCU.lean:72. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.4.6●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_one_zero
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation angle 1 0 =
    ↑(Real.sin angle)

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_one_zero
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation
      angle 1 0 =
    ↑(Real.sin angle)

Theorem10.4.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real rotation one 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/ComplexLCU.lean:76. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.4.7●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_one_one (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation angle 1 1 =
    ↑(Real.cos angle)

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_one_one
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation
      angle 1 1 =
    ↑(Real.cos angle)

Theorem10.4.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “real rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Every real planar rotation is unitary over 'ℂ'.

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

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

Technical source note. Every real planar rotation is unitary over 'ℂ'.

Declaration kind. theorem.

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

Lean code for Theorem10.4.8●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_unitary (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation angle ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.realRotation_unitary
  (angle : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.realRotation
      angle ∈
    Matrix.unitaryGroup (Fin 2) ℂ

Every real planar rotation is unitary over `ℂ`.

Definition10.4.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “amplitude rotation”. Rotation whose clean entry is intended to encode '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. Rotation whose clean entry is intended to encode 'coefficient'.

Declaration kind. def.

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

Lean code for Definition10.4.9●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
  (coefficient : ℝ) : Matrix (Fin 2) (Fin 2) ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
  (coefficient : ℝ) :
  Matrix (Fin 2) (Fin 2) ℂ

Rotation whose clean entry is intended to encode `coefficient`.

Theorem10.4.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude rotation unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The amplitude rotation is unitary without any domain hypothesis.

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 amplitude rotation is unitary without any domain hypothesis.

Declaration kind. theorem.

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

Lean code for Theorem10.4.10●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation_unitary
  (coefficient : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation coefficient ∈
    Matrix.unitaryGroup (Fin 2) ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation_unitary
  (coefficient : ℝ) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
      coefficient ∈
    Matrix.unitaryGroup (Fin 2) ℂ

The amplitude rotation is unitary without any domain hypothesis.

Theorem10.4.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude rotation clean entry”; the hypotheses and conclusion in the code panel fix its exact scope. Under the standard arccos domain, the clean entry is exactly the coefficient.

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. Under the standard arccos domain, the clean entry is exactly the coefficient.

Declaration kind. theorem.

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

Lean code for Theorem10.4.11●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation_cleanEntry
  (coefficient : ℝ) (lower : -1 ≤ coefficient)
  (upper : coefficient ≤ 1) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation coefficient 0
      0 =
    ↑coefficient

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation_cleanEntry
  (coefficient : ℝ)
  (lower : -1 ≤ coefficient)
  (upper : coefficient ≤ 1) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeRotation
      coefficient 0 0 =
    ↑coefficient

Under the standard arccos domain, the clean entry is exactly the coefficient.

Theorem10.4.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “reindex unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Reindexing rows and columns by the same equivalence 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 and concrete Robin-boundary example artifacts.

Technical source note. Reindexing rows and columns by the same equivalence preserves unitarity.

Declaration kind. theorem.

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

Lean code for Theorem10.4.12●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.reindex_unitary.{u_1, u_2}
  {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ] (equiv : ι ≃ κ) (operator : Matrix ι ι ℂ)
  (unitary : operator ∈ Matrix.unitaryGroup ι ℂ) :
  (Matrix.reindexAlgEquiv ℂ ℂ equiv) operator ∈ Matrix.unitaryGroup κ ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.reindex_unitary.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ] (equiv : ι ≃ κ)
  (operator : Matrix ι ι ℂ)
  (unitary :
    operator ∈ Matrix.unitaryGroup ι ℂ) :
  (Matrix.reindexAlgEquiv ℂ ℂ equiv)
      operator ∈
    Matrix.unitaryGroup κ ℂ

Reindexing rows and columns by the same equivalence preserves unitarity.

Theorem10.4.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “block diagonal unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A finite family of unitary blocks is unitary when placed block-diagonally.

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. A finite family of unitary blocks is unitary when placed block-diagonally.

Declaration kind. theorem.

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

Lean code for Theorem10.4.13●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.blockDiagonal_unitary.{u_1, u_2}
  {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ] (blocks : κ → Matrix ι ι ℂ)
  (unitary : ∀ (k : κ), blocks k ∈ Matrix.unitaryGroup ι ℂ) :
  Matrix.blockDiagonal blocks ∈ Matrix.unitaryGroup (ι × κ) ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.blockDiagonal_unitary.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ]
  (blocks : κ → Matrix ι ι ℂ)
  (unitary :
    ∀ (k : κ),
      blocks k ∈
        Matrix.unitaryGroup ι ℂ) :
  Matrix.blockDiagonal blocks ∈
    Matrix.unitaryGroup (ι × κ) ℂ

A finite family of unitary blocks is unitary when placed block-diagonally.

Definition10.4.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “equiv permutation matrix”. Matrix of a finite basis permutation.

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. Matrix of a finite basis permutation.

Declaration kind. def.

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

Lean code for Definition10.4.14●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix.{u_1}
  {ι : Type u_1} [DecidableEq ι] (equiv : ι ≃ ι) : Matrix ι ι ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (equiv : ι ≃ ι) : Matrix ι ι ℂ

Matrix of a finite basis permutation.

Theorem10.4.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “equiv permutation matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope. Every equivalence induces a unitary permutation matrix.

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

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

Technical source note. Every equivalence induces a unitary permutation matrix.

Declaration kind. theorem.

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

Lean code for Theorem10.4.15●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_unitary.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] (equiv : ι ≃ ι) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix equiv ∈
    Matrix.unitaryGroup ι ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_unitary.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (equiv : ι ≃ ι) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      equiv ∈
    Matrix.unitaryGroup ι ℂ

Every equivalence induces a unitary permutation matrix.

Theorem10.4.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “equiv permutation matrix mul apply”; the hypotheses and conclusion in the code panel fix its exact scope. Multiplication by a permutation matrix applies the inverse permutation to rows.

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. Multiplication by a permutation matrix applies the inverse permutation to rows.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/ComplexLCU.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.4.16●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul_apply.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι]
  (equiv : ι ≃ ι) (operator : Matrix ι κ ℂ) (row : ι) (column : κ) :
  (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix equiv *
        operator)
      row column =
    operator (equiv.symm row) column

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul_apply.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  [Fintype ι] [DecidableEq ι]
  (equiv : ι ≃ ι)
  (operator : Matrix ι κ ℂ) (row : ι)
  (column : κ) :
  (QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          equiv *
        operator)
      row column =
    operator (equiv.symm row) column

Multiplication by a permutation matrix applies the inverse permutation to rows.

Theorem10.4.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mul equiv permutation matrix apply”; the hypotheses and conclusion in the code panel fix its exact scope. Multiplication on the right by a permutation matrix applies the permutation to columns.

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. Multiplication on the right by a permutation matrix applies the permutation to columns.

Declaration kind. theorem.

Source: QuantumBlockEncoding/Robin/ComplexLCU.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.4.17●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.mul_equivPermutationMatrix_apply.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2} [Fintype κ] [DecidableEq κ]
  (operator : Matrix ι κ ℂ) (equiv : κ ≃ κ) (row : ι) (column : κ) :
  (operator *
        QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          equiv)
      row column =
    operator row (equiv column)

theorem QuantumBlockEncoding.Robin.ComplexLCU.mul_equivPermutationMatrix_apply.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  [Fintype κ] [DecidableEq κ]
  (operator : Matrix ι κ ℂ)
  (equiv : κ ≃ κ) (row : ι) (column : κ) :
  (operator *
        QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          equiv)
      row column =
    operator row (equiv column)

Multiplication on the right by a permutation matrix applies the
permutation to columns.

Theorem10.4.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “equiv permutation matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope. Chronological composition of finite basis permutations.

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. Chronological composition of finite basis permutations.

Declaration kind. theorem.

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

Lean code for Theorem10.4.18●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul.{u_1}
  {ι : Type u_1} [Fintype ι] [DecidableEq ι] (first second : ι ≃ ι) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix second *
      QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        first =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (first.trans second)

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_mul.{u_1}
  {ι : Type u_1} [Fintype ι]
  [DecidableEq ι] (first second : ι ≃ ι) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        second *
      QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        first =
    QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
      (first.trans second)

Chronological composition of finite basis permutations.

Theorem10.4.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “equiv permutation matrix conjugates reindex”; the hypotheses and conclusion in the code panel fix its exact scope. Conjugating a reindexed operator by an involutive basis permutation is the same as composing that permutation into the indexing equivalence.

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. Conjugating a reindexed operator by an involutive basis permutation is the same as composing that permutation into the indexing equivalence.

Declaration kind. theorem.

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

Lean code for Theorem10.4.19●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_conjugates_reindex.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ] (basis : ι ≃ ι) (logical : ι ≃ κ)
  (operator : Matrix κ κ ℂ) (involutive : Function.Involutive ⇑basis) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix basis *
        (Matrix.reindexAlgEquiv ℂ ℂ logical.symm) operator *
      QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        basis =
    (Matrix.reindexAlgEquiv ℂ ℂ (basis.trans logical).symm) operator

theorem QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix_conjugates_reindex.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  [Fintype ι] [DecidableEq ι] [Fintype κ]
  [DecidableEq κ] (basis : ι ≃ ι)
  (logical : ι ≃ κ)
  (operator : Matrix κ κ ℂ)
  (involutive :
    Function.Involutive ⇑basis) :
  QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
          basis *
        (Matrix.reindexAlgEquiv ℂ ℂ
            logical.symm)
          operator *
      QuantumBlockEncoding.Robin.ComplexLCU.equivPermutationMatrix
        basis =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (basis.trans logical).symm)
      operator

Conjugating a reindexed operator by an involutive basis permutation is
the same as composing that permutation into the indexing equivalence.

Definition10.4.20

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “lcu index”. Product-register index for coefficient, selector, and system registers.

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

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

Technical source note. Product-register index for coefficient, selector, and system registers.

Declaration kind. abbrev.

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

Lean code for Definition10.4.20●1 definition

abbrevdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

abbrev QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex.{u_1, u_2, u_3}
  (coefficient : Type u_1) (selector : Type u_2) (system : Type u_3) :
  Type (max u_1 u_3 u_2)

abbrev QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex.{u_1,
    u_2, u_3}
  (coefficient : Type u_1)
  (selector : Type u_2)
  (system : Type u_3) :
  Type (max u_1 u_3 u_2)

Product-register index for coefficient, selector, and system registers.

Definition10.4.21

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selector lift”. Lift selector PREPARE to coefficient × selector × system.

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. Lift selector PREPARE to coefficient × selector × system.

Declaration kind. def.

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

Lean code for Definition10.4.21●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.selectorLift.{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]
  (prepare : Matrix selector selector ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.selectorLift.{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]
  (prepare : Matrix selector selector ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ

Lift selector PREPARE to coefficient × selector × system.

Theorem10.4.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “selector lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A unitary selector PREPARE remains unitary after tensoring with identities.

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. A unitary selector PREPARE remains unitary after tensoring with identities.

Declaration kind. theorem.

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

Lean code for Theorem10.4.22●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectorLift_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]
  (prepare : Matrix selector selector ℂ)
  (unitary : prepare ∈ Matrix.unitaryGroup selector ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectorLift prepare ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectorLift_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]
  (prepare : Matrix selector selector ℂ)
  (unitary :
    prepare ∈
      Matrix.unitaryGroup selector ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectorLift
      prepare ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ

A unitary selector PREPARE remains unitary after tensoring with identities.

Definition10.4.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “amplitude lift”. Lift a coefficient-unitary family controlled by selector and system.

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. Lift a coefficient-unitary family controlled by selector and system.

Declaration kind. def.

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

Lean code for Definition10.4.23●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift.{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]
  (rotation : selector → system → Matrix coefficient coefficient ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift.{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]
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient
          ℂ) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ

Lift a coefficient-unitary family controlled by selector and system.

Theorem10.4.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “amplitude lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. A controlled family of unitary amplitude blocks is unitary.

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

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

Technical source note. A controlled family of unitary amplitude blocks is unitary.

Declaration kind. theorem.

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

Lean code for Theorem10.4.24●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_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]
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (unitary :
    ∀ (selector : selector) (system : system),
      rotation selector system ∈ Matrix.unitaryGroup coefficient ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift rotation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift_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]
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (unitary :
    ∀ (selector : selector)
      (system : system),
      rotation selector system ∈
        Matrix.unitaryGroup coefficient
          ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.amplitudeLift
      rotation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ

A controlled family of unitary amplitude blocks is unitary.

Definition10.4.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “controlled system equiv”. SELECT equivalence preserving coefficient and selector and permuting the system.

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. SELECT equivalence preserving coefficient and selector and permuting the system.

Declaration kind. def.

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

Lean code for Definition10.4.25●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.controlledSystemEquiv.{u_1, u_2,
    u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  (permutation : selector → system ≃ system) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system

def QuantumBlockEncoding.Robin.ComplexLCU.controlledSystemEquiv.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  (permutation :
    selector → system ≃ system) :
  QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system ≃
    QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system

SELECT equivalence preserving coefficient and selector and permuting the system.

Definition10.4.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “select lift”. Logical SELECT matrix for a family of system permutations.

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

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

Technical source note. Logical SELECT matrix for a family of system permutations.

Declaration kind. def.

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

Lean code for Definition10.4.26●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.selectLift.{u_1, u_2, u_3}
  {coefficient : Type u_1} {selector : Type u_2} {system : Type u_3}
  [DecidableEq coefficient] [DecidableEq selector] [DecidableEq system]
  (permutation : selector → system ≃ system) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.selectLift.{u_1,
    u_2, u_3}
  {coefficient : Type u_1}
  {selector : Type u_2}
  {system : Type u_3}
  [DecidableEq coefficient]
  [DecidableEq selector]
  [DecidableEq system]
  (permutation :
    selector → system ≃ system) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ

Logical SELECT matrix for a family of system permutations.

Theorem10.4.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “select lift unitary”; the hypotheses and conclusion in the code panel fix its exact scope. SELECT is unitary because it is a basis permutation.

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. SELECT is unitary because it is a basis permutation.

Declaration kind. theorem.

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

Lean code for Theorem10.4.27●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_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]
  (permutation : selector → system ≃ system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectLift permutation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.selectLift_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]
  (permutation :
    selector → system ≃ system) :
  QuantumBlockEncoding.Robin.ComplexLCU.selectLift
      permutation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ

SELECT is unitary because it is a basis permutation.

Definition10.4.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prepare amplitude select unprepare”. PREPARE → amplitude → SELECT → unprepare logical matrix.

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

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

Technical source note. PREPARE → amplitude → SELECT → unprepare logical matrix.

Declaration kind. def.

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

Lean code for Definition10.4.28●1 definition

defdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

def QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare.{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]
  (prepare : Matrix selector selector ℂ)
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (permutation : selector → system ≃ system) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient selector
      system)
    ℂ

def QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare.{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]
  (prepare : Matrix selector selector ℂ)
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (permutation :
    selector → system ≃ system) :
  Matrix
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
      coefficient selector system)
    ℂ

PREPARE → amplitude → SELECT → unprepare logical matrix.

Theorem10.4.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “prepare amplitude select unprepare unitary”; the hypotheses and conclusion in the code panel fix its exact scope. The complete logical LCU composition is unitary from its local certificates.

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

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

Technical source note. The complete logical LCU composition is unitary from its local certificates.

Declaration kind. theorem.

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

Lean code for Theorem10.4.29●1 theorem

theoremdefined in QuantumBlockEncoding/Robin/ComplexLCU.lean

complete

theorem QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_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]
  (prepare : Matrix selector selector ℂ)
  (rotation : selector → system → Matrix coefficient coefficient ℂ)
  (permutation : selector → system ≃ system)
  (prepareUnitary : prepare ∈ Matrix.unitaryGroup selector ℂ)
  (rotationUnitary :
    ∀ (selector : selector) (system : system),
      rotation selector system ∈ Matrix.unitaryGroup coefficient ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare
      prepare rotation permutation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex coefficient
        selector system)
      ℂ

theorem QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare_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]
  (prepare : Matrix selector selector ℂ)
  (rotation :
    selector →
      system →
        Matrix coefficient coefficient ℂ)
  (permutation :
    selector → system ≃ system)
  (prepareUnitary :
    prepare ∈
      Matrix.unitaryGroup selector ℂ)
  (rotationUnitary :
    ∀ (selector : selector)
      (system : system),
      rotation selector system ∈
        Matrix.unitaryGroup coefficient
          ℂ) :
  QuantumBlockEncoding.Robin.ComplexLCU.prepareAmplitudeSelectUnprepare
      prepare rotation permutation ∈
    Matrix.unitaryGroup
      (QuantumBlockEncoding.Robin.ComplexLCU.LCUIndex
        coefficient selector system)
      ℂ

The complete logical LCU composition is unitary from its local certificates.