6.1. QuantumBlockEncoding/AdjacentGivens.lean🔗

62 explicit public declarations, in source order.

Definition6.1.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “rotate rows”.

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. Circuit and register semantics, reusable tensor-train and matrix constructions, and explicit exact-real storage-cost refinements. Each declaration's hypotheses and conclusion fix its certified scope.

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

Lean code for Definition6.1.1●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.rotateRows {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (theta : ℝ) :
  Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.AdjacentGivens.rotateRows
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (theta : ℝ) :
  Matrix (Fin N) (Fin M) ℝ

Definition6.1.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “plane matrix”.

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

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

Lean code for Definition6.1.2●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.planeMatrix {N : ℕ} (i j : Fin N)
  (theta : ℝ) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.AdjacentGivens.planeMatrix
  {N : ℕ} (i j : Fin N) (theta : ℝ) :
  Matrix (Fin N) (Fin N) ℝ

Theorem6.1.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix mul”; 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.

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

Lean code for Theorem6.1.3●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_mul {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta * A =
    QuantumBlockEncoding.AdjacentGivens.rotateRows A i j theta

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_mul
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j theta *
      A =
    QuantumBlockEncoding.AdjacentGivens.rotateRows
      A i j theta

Theorem6.1.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “rotate rows inverse”; 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.

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

Lean code for Theorem6.1.4●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_inverse {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.rotateRows
      (QuantumBlockEncoding.AdjacentGivens.rotateRows A i j theta) i j
      (-theta) =
    A

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_inverse
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.rotateRows
      (QuantumBlockEncoding.AdjacentGivens.rotateRows
        A i j theta)
      i j (-theta) =
    A

Theorem6.1.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix inverse”; 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.

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

Lean code for Theorem6.1.5●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_inverse {N : ℕ}
  (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix i j (-theta) *
      QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta =
    1

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_inverse
  {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j (-theta) *
      QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j theta =
    1

Theorem6.1.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix transpose”; 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.

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

Lean code for Theorem6.1.6●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_transpose {N : ℕ}
  (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix i j
        theta).transpose =
    QuantumBlockEncoding.AdjacentGivens.planeMatrix i j (-theta)

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_transpose
  {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j theta).transpose =
    QuantumBlockEncoding.AdjacentGivens.planeMatrix
      i j (-theta)

Theorem6.1.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix orthogonal”; 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.

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

Lean code for Theorem6.1.7●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_orthogonal {N : ℕ}
  (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix i j
          theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta =
    1

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_orthogonal
  {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix
          i j theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j theta =
    1

Theorem6.1.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “rotate rows preserves orthogonal”; 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.

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

Lean code for Theorem6.1.8●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1) (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows A i j
          theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.rotateRows A i j theta =
    1

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows
          A i j theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.rotateRows
        A i j theta =
    1

Theorem6.1.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “split angle real first column”; 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.

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

Lean code for Theorem6.1.9●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.splitAngle_real_firstColumn
  (x y : ℝ) :
  Real.cos
          ((QuantumBlockEncoding.RealAmplitudePreparation.splitAngle x
                y).eval /
            2) *
        QuantumBlockEncoding.RealAmplitudePreparation.pairNorm x y =
      x ∧
    Real.sin
          ((QuantumBlockEncoding.RealAmplitudePreparation.splitAngle x
                y).eval /
            2) *
        QuantumBlockEncoding.RealAmplitudePreparation.pairNorm x y =
      y

theorem QuantumBlockEncoding.AdjacentGivens.splitAngle_real_firstColumn
  (x y : ℝ) :
  Real.cos
          ((QuantumBlockEncoding.RealAmplitudePreparation.splitAngle
                x y).eval /
            2) *
        QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
          x y =
      x ∧
    Real.sin
          ((QuantumBlockEncoding.RealAmplitudePreparation.splitAngle
                x y).eval /
            2) *
        QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
          x y =
      y

Definition6.1.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “elimination angle”.

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

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

Lean code for Definition6.1.10●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.eliminationAngle (x y : ℝ) : ℝ

def QuantumBlockEncoding.AdjacentGivens.eliminationAngle
  (x y : ℝ) : ℝ

Theorem6.1.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “elimination angle 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.

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

Lean code for Theorem6.1.11●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminationAngle_zero :
  QuantumBlockEncoding.AdjacentGivens.eliminationAngle 0 0 = 0

theorem QuantumBlockEncoding.AdjacentGivens.eliminationAngle_zero :
  QuantumBlockEncoding.AdjacentGivens.eliminationAngle
      0 0 =
    0

Theorem6.1.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate pair”; 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.

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

Lean code for Theorem6.1.12●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminate_pair (x y : ℝ) :
  Real.cos
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y /
              2) *
          x -
        Real.sin
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y /
              2) *
          y =
      QuantumBlockEncoding.RealAmplitudePreparation.pairNorm x y ∧
    Real.sin
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y /
              2) *
          x +
        Real.cos
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle x y /
              2) *
          y =
      0

theorem QuantumBlockEncoding.AdjacentGivens.eliminate_pair
  (x y : ℝ) :
  Real.cos
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
                x y /
              2) *
          x -
        Real.sin
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
                x y /
              2) *
          y =
      QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
        x y ∧
    Real.sin
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
                x y /
              2) *
          x +
        Real.cos
            (QuantumBlockEncoding.AdjacentGivens.eliminationAngle
                x y /
              2) *
          y =
      0

Theorem6.1.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pair norm eq zero iff”; 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.

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

Lean code for Theorem6.1.13●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.pairNorm_eq_zero_iff (x y : ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.pairNorm x y = 0 ↔
    x = 0 ∧ y = 0

theorem QuantumBlockEncoding.AdjacentGivens.pairNorm_eq_zero_iff
  (x y : ℝ) :
  QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
        x y =
      0 ↔
    x = 0 ∧ y = 0

Theorem6.1.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pair norm pos of nonzero”; 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.

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

Lean code for Theorem6.1.14●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.pairNorm_pos_of_nonzero (x y : ℝ)
  (nonzero : x ≠ 0 ∨ y ≠ 0) :
  0 < QuantumBlockEncoding.RealAmplitudePreparation.pairNorm x y

theorem QuantumBlockEncoding.AdjacentGivens.pairNorm_pos_of_nonzero
  (x y : ℝ) (nonzero : x ≠ 0 ∨ y ≠ 0) :
  0 <
    QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
      x y

Definition6.1.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eliminate entry”.

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

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

Lean code for Definition6.1.15●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.eliminateEntry {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (col : Fin M) :
  Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.AdjacentGivens.eliminateEntry
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (col : Fin M) :
  Matrix (Fin N) (Fin M) ℝ

Theorem6.1.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate entry pivot”; 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.

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

Lean code for Theorem6.1.16●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_pivot {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (distinct : i ≠ j)
  (col : Fin M) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col i col =
      QuantumBlockEncoding.RealAmplitudePreparation.pairNorm (A i col)
        (A j col) ∧
    QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col j col =
      0

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_pivot
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (distinct : i ≠ j)
  (col : Fin M) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry
        A i j col i col =
      QuantumBlockEncoding.RealAmplitudePreparation.pairNorm
        (A i col) (A j col) ∧
    QuantumBlockEncoding.AdjacentGivens.eliminateEntry
        A i j col j col =
      0

Theorem6.1.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate entry unchanged”; 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.

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

Lean code for Theorem6.1.17●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_unchanged {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j row : Fin N)
  (col otherCol : Fin M) (hi : row ≠ i) (hj : row ≠ j) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col row
      otherCol =
    A row otherCol

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_unchanged
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j row : Fin N) (col otherCol : Fin M)
  (hi : row ≠ i) (hj : row ≠ j) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry
      A i j col row otherCol =
    A row otherCol

Theorem6.1.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate entry preserves zero column”; 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.

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

Lean code for Theorem6.1.18●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_preserves_zero_column
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N)
  (col oldCol : Fin M) (hi : A i oldCol = 0) (hj : A j oldCol = 0)
  (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col row
      oldCol =
    A row oldCol

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_preserves_zero_column
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (col oldCol : Fin M)
  (hi : A i oldCol = 0)
  (hj : A j oldCol = 0) (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry
      A i j col row oldCol =
    A row oldCol

Theorem6.1.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate entry preserves orthogonal”; 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.

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

Lean code for Theorem6.1.19●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1) (i j : Fin N) (distinct : i ≠ j)
  (col : Fin N) :
  (QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j
          col).transpose *
      QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col =
    1

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (i j : Fin N) (distinct : i ≠ j)
  (col : Fin N) :
  (QuantumBlockEncoding.AdjacentGivens.eliminateEntry
          A i j col).transpose *
      QuantumBlockEncoding.AdjacentGivens.eliminateEntry
        A i j col =
    1

Theorem6.1.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eliminate entry zero pair”; the hypotheses and conclusion in the code panel fix its exact scope. A zero pair produces an actual identity step, without division by zero.

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

Technical source note. A zero pair produces an actual identity step, without division by zero.

Declaration kind. theorem.

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

Lean code for Theorem6.1.20●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_zero_pair {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (i j : Fin N) (col : Fin M)
  (firstZero : A i col = 0) (secondZero : A j col = 0) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry A i j col = A

theorem QuantumBlockEncoding.AdjacentGivens.eliminateEntry_zero_pair
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (i j : Fin N) (col : Fin M)
  (firstZero : A i col = 0)
  (secondZero : A j col = 0) :
  QuantumBlockEncoding.AdjacentGivens.eliminateEntry
      A i j col =
    A

A zero pair produces an actual identity step, without division by zero.

Definition6.1.21

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “step”. A proposition-valued field is a requirement until a constructor supplies it. An actual adjacent-row rotation, carrying the precise ordered support.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

Technical source note. An actual adjacent-row rotation, carrying the precise ordered support.

Declaration kind. structure.

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

Lean code for Definition6.1.21●1 definition

structure(4 fields)defined in QuantumBlockEncoding/AdjacentGivens.lean

complete

structure QuantumBlockEncoding.AdjacentGivens.Step (N : ℕ) : Type

structure QuantumBlockEncoding.AdjacentGivens.Step
  (N : ℕ) : Type

An actual adjacent-row rotation, carrying the precise ordered support.

Fields

first : Fin N

second : Fin N

adjacent : ↑self.first + 1 = ↑self.second

angle : ℝ

Theorem6.1.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “distinct”; 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.

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

Lean code for Theorem6.1.22●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.Step.distinct {N : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step N) :
  step.first ≠ step.second

theorem QuantumBlockEncoding.AdjacentGivens.Step.distinct
  {N : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      N) :
  step.first ≠ step.second

Definition6.1.23

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “matrix”.

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

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

Lean code for Definition6.1.23●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.Step.matrix {N : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step N) :
  Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.AdjacentGivens.Step.matrix
  {N : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      N) :
  Matrix (Fin N) (Fin N) ℝ

Definition6.1.24

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “apply steps”. Chronological action: the first listed matrix acts first.

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

Technical source note. Chronological action: the first listed matrix acts first.

Declaration kind. def.

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

Lean code for Definition6.1.24●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.applySteps {N M : ℕ} :
  List (QuantumBlockEncoding.AdjacentGivens.Step N) →
    Matrix (Fin N) (Fin M) ℝ → Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.AdjacentGivens.applySteps
  {N M : ℕ} :
  List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N) →
    Matrix (Fin N) (Fin M) ℝ →
      Matrix (Fin N) (Fin M) ℝ

Chronological action: the first listed matrix acts first.

Definition6.1.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “inverse”.

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

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

Lean code for Definition6.1.25●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.Step.inverse {N : ℕ}
  (step : QuantumBlockEncoding.AdjacentGivens.Step N) :
  QuantumBlockEncoding.AdjacentGivens.Step N

def QuantumBlockEncoding.AdjacentGivens.Step.inverse
  {N : ℕ}
  (step :
    QuantumBlockEncoding.AdjacentGivens.Step
      N) :
  QuantumBlockEncoding.AdjacentGivens.Step
    N

Theorem6.1.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “apply steps append”; 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.

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

Lean code for Theorem6.1.26●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_append {N M : ℕ}
  (left right : List (QuantumBlockEncoding.AdjacentGivens.Step N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps (left ++ right) A =
    QuantumBlockEncoding.AdjacentGivens.applySteps right
      (QuantumBlockEncoding.AdjacentGivens.applySteps left A)

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_append
  {N M : ℕ}
  (left right :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (left ++ right) A =
    QuantumBlockEncoding.AdjacentGivens.applySteps
      right
      (QuantumBlockEncoding.AdjacentGivens.applySteps
        left A)

Theorem6.1.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “apply steps reverse inverse”; the hypotheses and conclusion in the code panel fix its exact scope. Reversing the chronological list and negating every angle exactly undoes it.

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

Technical source note. Reversing the chronological list and negating every angle exactly undoes it.

Declaration kind. theorem.

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

Lean code for Theorem6.1.27●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_reverse_inverse {N M : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (List.map QuantumBlockEncoding.AdjacentGivens.Step.inverse
        steps.reverse)
      (QuantumBlockEncoding.AdjacentGivens.applySteps steps A) =
    A

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_reverse_inverse
  {N M : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (List.map
        QuantumBlockEncoding.AdjacentGivens.Step.inverse
        steps.reverse)
      (QuantumBlockEncoding.AdjacentGivens.applySteps
        steps A) =
    A

Reversing the chronological list and negating every angle exactly undoes it.

Definition6.1.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “column sweep”.

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

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

Lean code for Definition6.1.28●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.columnSweep {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ) :
  lo + count < N → Matrix (Fin N) (Fin M) ℝ

def QuantumBlockEncoding.AdjacentGivens.columnSweep
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ) :
  lo + count < N →
    Matrix (Fin N) (Fin M) ℝ

Definition6.1.29

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “column sweep steps”. The list is computed from the changing matrix, not supplied as a certificate.

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

Technical source note. The list is computed from the changing matrix, not supplied as a certificate.

Declaration kind. def.

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

Lean code for Definition6.1.29●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.columnSweepSteps {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ) :
  lo + count < N → List (QuantumBlockEncoding.AdjacentGivens.Step N)

def QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ) :
  lo + count < N →
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N)

The list is computed from the changing matrix, not supplied as a certificate.

Theorem6.1.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep steps length”; 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.

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

Lean code for Theorem6.1.30●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweepSteps_length {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps A col lo count
        bound).length =
    count

theorem QuantumBlockEncoding.AdjacentGivens.columnSweepSteps_length
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
        A col lo count bound).length =
    count

Theorem6.1.31

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep steps action”; 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.

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

Lean code for Theorem6.1.31●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweepSteps_action {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps A col lo
        count bound)
      A =
    QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count bound

theorem QuantumBlockEncoding.AdjacentGivens.columnSweepSteps_action
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
        A col lo count bound)
      A =
    QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col lo count bound

Theorem6.1.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep exact recovery”; the hypotheses and conclusion in the code panel fix its exact scope. The original matrix is recovered from the computed residual.

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

Technical source note. The original matrix is recovered from the computed residual. No identity or full-decomposition assumption is hidden in this statement.

Declaration kind. theorem.

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

Lean code for Theorem6.1.32●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_exact_recovery {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (List.map QuantumBlockEncoding.AdjacentGivens.Step.inverse
        (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps A col lo
            count bound).reverse)
      (QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count
        bound) =
    A

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_exact_recovery
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (List.map
        QuantumBlockEncoding.AdjacentGivens.Step.inverse
        (QuantumBlockEncoding.AdjacentGivens.columnSweepSteps
            A col lo count bound).reverse)
      (QuantumBlockEncoding.AdjacentGivens.columnSweep
        A col lo count bound) =
    A

The original matrix is recovered from the computed residual. No identity
or full-decomposition assumption is hidden in this statement.

Theorem6.1.33

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep outside”; 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.

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

Lean code for Theorem6.1.33●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_outside {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) (row : Fin N) (otherCol : Fin M)
  (outside : ↑row < lo ∨ lo + count < ↑row) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count bound
      row otherCol =
    A row otherCol

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_outside
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) (row : Fin N)
  (otherCol : Fin M)
  (outside :
    ↑row < lo ∨ lo + count < ↑row) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col lo count bound row otherCol =
    A row otherCol

Theorem6.1.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep zeroed”; 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.

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

Lean code for Theorem6.1.34●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_zeroed {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) (row : Fin N) (lower : lo < ↑row)
  (upper : ↑row ≤ lo + count) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count bound
      row col =
    0

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_zeroed
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) (row : Fin N)
  (lower : lo < ↑row)
  (upper : ↑row ≤ lo + count) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col lo count bound row col =
    0

Theorem6.1.35

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep preserves zero column”; 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.

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

Lean code for Theorem6.1.35●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_zero_column
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ) (col oldCol : Fin M)
  (lo count : ℕ) (bound : lo + count < N)
  (zeros :
    ∀ (row : Fin N), lo ≤ ↑row → ↑row ≤ lo + count → A row oldCol = 0)
  (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count bound
      row oldCol =
    A row oldCol

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_zero_column
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col oldCol : Fin M) (lo count : ℕ)
  (bound : lo + count < N)
  (zeros :
    ∀ (row : Fin N),
      lo ≤ ↑row →
        ↑row ≤ lo + count →
          A row oldCol = 0)
  (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col lo count bound row oldCol =
    A row oldCol

Theorem6.1.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep preserves orthogonal”; 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.

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

Lean code for Theorem6.1.36●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1) (col : Fin N) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count
          bound).transpose *
      QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count
        bound =
    1

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_orthogonal
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (col : Fin N) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep
          A col lo count
          bound).transpose *
      QuantumBlockEncoding.AdjacentGivens.columnSweep
        A col lo count bound =
    1

Theorem6.1.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “det two row mix”; 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.

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

Lean code for Theorem6.1.37●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.det_two_row_mix {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (i j : Fin N) (distinct : i ≠ j)
  (a b c d : ℝ) :
  ((A.updateRow i (a • A i + b • A j)).updateRow j
        (c • A i + d • A j)).det =
    (a * d - b * c) * A.det

theorem QuantumBlockEncoding.AdjacentGivens.det_two_row_mix
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (i j : Fin N) (distinct : i ≠ j)
  (a b c d : ℝ) :
  ((A.updateRow i
            (a • A i + b • A j)).updateRow
        j (c • A i + d • A j)).det =
    (a * d - b * c) * A.det

Theorem6.1.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “rotate rows det”; 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.

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

Lean code for Theorem6.1.38●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_det {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows A i j theta).det =
    A.det

theorem QuantumBlockEncoding.AdjacentGivens.rotateRows_det
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows
        A i j theta).det =
    A.det

Theorem6.1.39

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix det”; 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.

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

Lean code for Theorem6.1.39●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_det {N : ℕ}
  (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta).det = 1

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_det
  {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.planeMatrix
        i j theta).det =
    1

Theorem6.1.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep preserves det”; 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.

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

Lean code for Theorem6.1.40●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_det {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (col : Fin N) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count
        bound).det =
    A.det

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_preserves_det
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (col : Fin N) (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep
        A col lo count bound).det =
    A.det

Definition6.1.41

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prefix identity”.

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

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

Lean code for Definition6.1.41●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.PrefixIdentity {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k : ℕ) : Prop

def QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k : ℕ) : Prop

Theorem6.1.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “orthogonal zero of fixed column”; 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.

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

Lean code for Theorem6.1.42●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.orthogonal_zero_of_fixed_column
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1) (old col : Fin N)
  (distinct : old ≠ col)
  (fixed : ∀ (row : Fin N), A row old = if row = old then 1 else 0) :
  A old col = 0

theorem QuantumBlockEncoding.AdjacentGivens.orthogonal_zero_of_fixed_column
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (old col : Fin N) (distinct : old ≠ col)
  (fixed :
    ∀ (row : Fin N),
      A row old =
        if row = old then 1 else 0) :
  A old col = 0

Theorem6.1.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep prefix”; 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.

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

Lean code for Theorem6.1.43●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_prefix {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (col : Fin N) (count : ℕ)
  (bound : ↑col + count < N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity A ↑col) :
  QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
    (QuantumBlockEncoding.AdjacentGivens.columnSweep A col (↑col) count
      bound)
    ↑col

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_prefix
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (col : Fin N) (count : ℕ)
  (bound : ↑col + count < N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
      A ↑col) :
  QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
    (QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col (↑col) count bound)
    ↑col

Theorem6.1.44

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep pivot nonneg”; 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.

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

Lean code for Theorem6.1.44●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_pivot_nonneg {N M : ℕ}
  (A : Matrix (Fin N) (Fin M) ℝ) (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N) (positive : 0 < count) :
  0 ≤
    QuantumBlockEncoding.AdjacentGivens.columnSweep A col lo count bound
      ⟨lo, ⋯⟩ col

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_pivot_nonneg
  {N M : ℕ} (A : Matrix (Fin N) (Fin M) ℝ)
  (col : Fin M) (lo count : ℕ)
  (bound : lo + count < N)
  (positive : 0 < count) :
  0 ≤
    QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col lo count bound ⟨lo, ⋯⟩ col

Theorem6.1.45

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “orthogonal supported column sq”; 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.

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

Lean code for Theorem6.1.45●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.orthogonal_supported_column_sq
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1) (col : Fin N)
  (support : ∀ (row : Fin N), row ≠ col → A row col = 0) :
  A col col ^ 2 = 1

theorem QuantumBlockEncoding.AdjacentGivens.orthogonal_supported_column_sq
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (col : Fin N)
  (support :
    ∀ (row : Fin N),
      row ≠ col → A row col = 0) :
  A col col ^ 2 = 1

Theorem6.1.46

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “column sweep prefix succ”; 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.

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

Lean code for Theorem6.1.46●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_prefix_succ {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
  (col : Fin N) (count : ℕ) (dimension : ↑col + count + 1 = N)
  (positive : 0 < count)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity A ↑col) :
  QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
    (QuantumBlockEncoding.AdjacentGivens.columnSweep A col (↑col) count
      ⋯)
    (↑col + 1)

theorem QuantumBlockEncoding.AdjacentGivens.columnSweep_prefix_succ
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (col : Fin N) (count : ℕ)
  (dimension : ↑col + count + 1 = N)
  (positive : 0 < count)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
      A ↑col) :
  QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
    (QuantumBlockEncoding.AdjacentGivens.columnSweep
      A col (↑col) count ⋯)
    (↑col + 1)

Theorem6.1.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “matrix eq one of full prefix”; 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.

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

Lean code for Theorem6.1.47●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.matrix_eq_one_of_full_prefix {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity A N) :
  A = 1

theorem QuantumBlockEncoding.AdjacentGivens.matrix_eq_one_of_full_prefix
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
      A N) :
  A = 1

Theorem6.1.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “matrix eq one of last prefix”; 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.

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

Lean code for Theorem6.1.48●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.matrix_eq_one_of_last_prefix {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) (k : ℕ) (dimension : k + 1 = N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity A k) :
  A = 1

theorem QuantumBlockEncoding.AdjacentGivens.matrix_eq_one_of_last_prefix
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) (k : ℕ)
  (dimension : k + 1 = N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
      A k) :
  A = 1

Definition6.1.49

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “full sweep”.

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

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

Lean code for Definition6.1.49●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.fullSweep {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k remaining : ℕ) :
  k + remaining = N → Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.AdjacentGivens.fullSweep
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k remaining : ℕ) :
  k + remaining = N →
    Matrix (Fin N) (Fin N) ℝ

Definition6.1.50

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “full sweep steps”.

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

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

Lean code for Definition6.1.50●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.fullSweepSteps {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k remaining : ℕ) :
  k + remaining = N → List (QuantumBlockEncoding.AdjacentGivens.Step N)

def QuantumBlockEncoding.AdjacentGivens.fullSweepSteps
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k remaining : ℕ) :
  k + remaining = N →
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N)

Theorem6.1.51

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “full sweep steps action”; 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.

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

Lean code for Theorem6.1.51●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_action {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k remaining : ℕ)
  (dimension : k + remaining = N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps A k remaining
        dimension)
      A =
    QuantumBlockEncoding.AdjacentGivens.fullSweep A k remaining
      dimension

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_action
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k remaining : ℕ)
  (dimension : k + remaining = N) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps
        A k remaining dimension)
      A =
    QuantumBlockEncoding.AdjacentGivens.fullSweep
      A k remaining dimension

Theorem6.1.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “full sweep steps length twice”; 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.

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

Lean code for Theorem6.1.52●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_length_twice {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k remaining : ℕ)
  (dimension : k + remaining = N) :
  (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps A k remaining
          dimension).length *
      2 =
    remaining * (remaining - 1)

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_length_twice
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k remaining : ℕ)
  (dimension : k + remaining = N) :
  (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps
          A k remaining
          dimension).length *
      2 =
    remaining * (remaining - 1)

Theorem6.1.53

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “full sweep steps length”; 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.

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

Lean code for Theorem6.1.53●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_length {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (k remaining : ℕ)
  (dimension : k + remaining = N) :
  (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps A k remaining
        dimension).length =
    remaining * (remaining - 1) / 2

theorem QuantumBlockEncoding.AdjacentGivens.fullSweepSteps_length
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (k remaining : ℕ)
  (dimension : k + remaining = N) :
  (QuantumBlockEncoding.AdjacentGivens.fullSweepSteps
        A k remaining dimension).length =
    remaining * (remaining - 1) / 2

Theorem6.1.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “full sweep eq 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.

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

Lean code for Theorem6.1.54●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.fullSweep_eq_one {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) (k remaining : ℕ)
  (dimension : k + remaining = N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity A k) :
  QuantumBlockEncoding.AdjacentGivens.fullSweep A k remaining
      dimension =
    1

theorem QuantumBlockEncoding.AdjacentGivens.fullSweep_eq_one
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1)
  (k remaining : ℕ)
  (dimension : k + remaining = N)
  (fixedPrefix :
    QuantumBlockEncoding.AdjacentGivens.PrefixIdentity
      A k) :
  QuantumBlockEncoding.AdjacentGivens.fullSweep
      A k remaining dimension =
    1

Definition6.1.55

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “decompose so”. A computed finite list of adjacent RY planes in chronological circuit order.

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

Technical source note. A computed finite list of adjacent RY planes in chronological circuit order.

Declaration kind. def.

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

Lean code for Definition6.1.55●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.decomposeSO {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) :
  List (QuantumBlockEncoding.AdjacentGivens.Step N)

def QuantumBlockEncoding.AdjacentGivens.decomposeSO
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) :
  List
    (QuantumBlockEncoding.AdjacentGivens.Step
      N)

A computed finite list of adjacent RY planes in chronological circuit order.

Theorem6.1.56

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “decompose so action”; the hypotheses and conclusion in the code panel fix its exact scope. Every real determinant-one orthogonal matrix is exactly the action of the constructed adjacent-plane list.

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

Technical source note. Every real determinant-one orthogonal matrix is exactly the action of the constructed adjacent-plane list. The final identity is proved, not supplied.

Declaration kind. theorem.

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

Lean code for Theorem6.1.56●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_action {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.decomposeSO A) 1 =
    A

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_action
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      (QuantumBlockEncoding.AdjacentGivens.decomposeSO
        A)
      1 =
    A

Every real determinant-one orthogonal matrix is exactly the action of the
constructed adjacent-plane list. The final identity is proved, not supplied.

Theorem6.1.57

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “decompose so length”; the hypotheses and conclusion in the code panel fix its exact scope. Including harmless identity rotations at zero pivots gives an exact count.

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

Technical source note. Including harmless identity rotations at zero pivots gives an exact count.

Declaration kind. theorem.

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

Lean code for Theorem6.1.57●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_length {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.decomposeSO A).length =
    N * (N - 1) / 2

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_length
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.decomposeSO
        A).length =
    N * (N - 1) / 2

Including harmless identity rotations at zero pivots gives an exact count.

Theorem6.1.58

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix selected entry”; the hypotheses and conclusion in the code panel fix its exact scope. The ordered two-dimensional block uses exactly the selected-RY convention.

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

Technical source note. The ordered two-dimensional block uses exactly the selected-RY convention.

Declaration kind. theorem.

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

Lean code for Theorem6.1.58●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_selected_entry {N : ℕ}
  (i j : Fin N) (distinct : i ≠ j) (theta : ℝ) (rowBit colBit : Fin 2) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta
      (if rowBit = 0 then i else j) (if colBit = 0 then i else j) =
    QuantumBlockEncoding.realRyPlaneBlock theta rowBit colBit

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_selected_entry
  {N : ℕ} (i j : Fin N) (distinct : i ≠ j)
  (theta : ℝ) (rowBit colBit : Fin 2) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix
      i j theta
      (if rowBit = 0 then i else j)
      (if colBit = 0 then i else j) =
    QuantumBlockEncoding.realRyPlaneBlock
      theta rowBit colBit

The ordered two-dimensional block uses exactly the selected-RY convention.

Theorem6.1.59

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “plane matrix fixed column”; the hypotheses and conclusion in the code panel fix its exact scope. Every basis vector outside the selected pair is fixed, including its sign.

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

Technical source note. Every basis vector outside the selected pair is fixed, including its sign.

Declaration kind. theorem.

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

Lean code for Theorem6.1.59●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_fixed_column {N : ℕ}
  (i j col : Fin N) (theta : ℝ) (outsideFirst : col ≠ i)
  (outsideSecond : col ≠ j) (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix i j theta row col =
    1 row col

theorem QuantumBlockEncoding.AdjacentGivens.planeMatrix_fixed_column
  {N : ℕ} (i j col : Fin N) (theta : ℝ)
  (outsideFirst : col ≠ i)
  (outsideSecond : col ≠ j)
  (row : Fin N) :
  QuantumBlockEncoding.AdjacentGivens.planeMatrix
      i j theta row col =
    1 row col

Every basis vector outside the selected pair is fixed, including its sign.

Definition6.1.60

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “steps matrix”. Chronological matrix product, matching the circuit list convention.

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

Technical source note. Chronological matrix product, matching the circuit list convention.

Declaration kind. def.

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

Lean code for Definition6.1.60●1 definition

defdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

def QuantumBlockEncoding.AdjacentGivens.stepsMatrix {N : ℕ} :
  List (QuantumBlockEncoding.AdjacentGivens.Step N) →
    Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.AdjacentGivens.stepsMatrix
  {N : ℕ} :
  List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N) →
    Matrix (Fin N) (Fin N) ℝ

Chronological matrix product, matching the circuit list convention.

Theorem6.1.61

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “apply steps eq matrix mul”; 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.

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

Lean code for Theorem6.1.61●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_eq_matrix_mul {N M : ℕ}
  (steps : List (QuantumBlockEncoding.AdjacentGivens.Step N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps steps A =
    QuantumBlockEncoding.AdjacentGivens.stepsMatrix steps * A

theorem QuantumBlockEncoding.AdjacentGivens.applySteps_eq_matrix_mul
  {N M : ℕ}
  (steps :
    List
      (QuantumBlockEncoding.AdjacentGivens.Step
        N))
  (A : Matrix (Fin N) (Fin M) ℝ) :
  QuantumBlockEncoding.AdjacentGivens.applySteps
      steps A =
    QuantumBlockEncoding.AdjacentGivens.stepsMatrix
        steps *
      A

Theorem6.1.62

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “decompose so matrix”; 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.

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

Lean code for Theorem6.1.62●1 theorem

theoremdefined in QuantumBlockEncoding/AdjacentGivens.lean

complete

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_matrix {N : ℕ}
  (A : Matrix (Fin N) (Fin N) ℝ) (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.AdjacentGivens.stepsMatrix
      (QuantumBlockEncoding.AdjacentGivens.decomposeSO A) =
    A

theorem QuantumBlockEncoding.AdjacentGivens.decomposeSO_matrix
  {N : ℕ} (A : Matrix (Fin N) (Fin N) ℝ)
  (orthogonal : A.transpose * A = 1)
  (determinant : A.det = 1) :
  QuantumBlockEncoding.AdjacentGivens.stepsMatrix
      (QuantumBlockEncoding.AdjacentGivens.decomposeSO
        A) =
    A