6.23. QuantumBlockEncoding/RealIsometryCompletion.lean🔗

7 explicit public declarations, in source order.

Theorem6.23.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists orthogonal completion”; the hypotheses and conclusion in the code panel fix its exact scope. An arbitrary injection specifies the physical positions of the active columns, so no assumption that they form a prefix is needed.

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

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. An arbitrary injection specifies the physical positions of the active columns, so no assumption that they form a prefix is needed.

Declaration kind. theorem.

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

Lean code for Theorem6.23.1●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_orthogonal_completion
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧ ∀ (i : Fin N) (a : Fin r), U i (e a) = V i a

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_orthogonal_completion
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧
      ∀ (i : Fin N) (a : Fin r),
        U i (e a) = V i a

An arbitrary injection specifies the physical positions of the active
columns, so no assumption that they form a prefix is needed.

Definition6.23.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sign flip”. Change the sign of one chosen column; every other column is unchanged.

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. Change the sign of one chosen column; every other column is unchanged.

Declaration kind. def.

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

Lean code for Definition6.23.2●1 definition

defdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

def QuantumBlockEncoding.RealIsometryCompletion.signFlip {N : ℕ}
  (j : Fin N) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.RealIsometryCompletion.signFlip
  {N : ℕ} (j : Fin N) :
  Matrix (Fin N) (Fin N) ℝ

Change the sign of one chosen column; every other column is unchanged.

Theorem6.23.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.23.3●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.signFlip_orthogonal {N : ℕ}
  (j : Fin N) :
  (QuantumBlockEncoding.RealIsometryCompletion.signFlip j).transpose *
      QuantumBlockEncoding.RealIsometryCompletion.signFlip j =
    1

theorem QuantumBlockEncoding.RealIsometryCompletion.signFlip_orthogonal
  {N : ℕ} (j : Fin N) :
  (QuantumBlockEncoding.RealIsometryCompletion.signFlip
          j).transpose *
      QuantumBlockEncoding.RealIsometryCompletion.signFlip
        j =
    1

Theorem6.23.4

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sign flip 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/RealIsometryCompletion.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.23.4●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.signFlip_det {N : ℕ}
  (j : Fin N) :
  (QuantumBlockEncoding.RealIsometryCompletion.signFlip j).det = -1

theorem QuantumBlockEncoding.RealIsometryCompletion.signFlip_det
  {N : ℕ} (j : Fin N) :
  (QuantumBlockEncoding.RealIsometryCompletion.signFlip
        j).det =
    -1

Theorem6.23.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mul sign flip preserves”; 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/RealIsometryCompletion.lean:77. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem6.23.5●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.mul_signFlip_preserves
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (j i a : Fin N) (ha : a ≠ j) :
  (U * QuantumBlockEncoding.RealIsometryCompletion.signFlip j) i a =
    U i a

theorem QuantumBlockEncoding.RealIsometryCompletion.mul_signFlip_preserves
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (j i a : Fin N) (ha : a ≠ j) :
  (U *
        QuantumBlockEncoding.RealIsometryCompletion.signFlip
          j)
      i a =
    U i a

Theorem6.23.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists special orthogonal completion of unused”; the hypotheses and conclusion in the code panel fix its exact scope. Correct a negative determinant using a known unused column.

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

Technical source note. Correct a negative determinant using a known unused column. All active columns remain exact, and the result lies in SO(N), not merely O(N).

Declaration kind. theorem.

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

Lean code for Theorem6.23.6●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_specialOrthogonal_completion_of_unused
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1) (unused : Fin N)
  (hu : ∀ (a : Fin r), e a ≠ unused) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧ ∀ (i : Fin N) (a : Fin r), U i (e a) = V i a

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_specialOrthogonal_completion_of_unused
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1)
  (unused : Fin N)
  (hu : ∀ (a : Fin r), e a ≠ unused) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧
        ∀ (i : Fin N) (a : Fin r),
          U i (e a) = V i a

Correct a negative determinant using a known unused column. All active
columns remain exact, and the result lies in SO(N), not merely O(N).

Theorem6.23.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “exists special orthogonal completion”; the hypotheses and conclusion in the code panel fix its exact scope. A strict active-dimension bound guarantees a spare orientation column.

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

Technical source note. A strict active-dimension bound guarantees a spare orientation column.

Declaration kind. theorem.

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

Lean code for Theorem6.23.7●1 theorem

theoremdefined in QuantumBlockEncoding/RealIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_specialOrthogonal_completion
  {N r : ℕ} (hr : r < N) (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N) (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧ ∀ (i : Fin N) (a : Fin r), U i (e a) = V i a

theorem QuantumBlockEncoding.RealIsometryCompletion.exists_specialOrthogonal_completion
  {N r : ℕ} (hr : r < N)
  (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1) :
  ∃ U,
    U.transpose * U = 1 ∧
      U.det = 1 ∧
        ∀ (i : Fin N) (a : Fin r),
          U i (e a) = V i a

A strict active-dimension bound guarantees a spare orientation column.