6.4. QuantumBlockEncoding/ConstructiveIsometryCompletion.lean🔗

31 explicit public declarations, in source order.

Definition6.4.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prefix columns”. The first 'k' rectangular columns are their corresponding coordinate vectors.

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 first 'k' rectangular columns are their corresponding coordinate vectors.

Declaration kind. def.

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

Lean code for Definition6.4.1●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r ≤ N) (k : ℕ) : Prop

def QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r ≤ N) (k : ℕ) : Prop

The first `k` rectangular columns are their corresponding coordinate vectors.

Theorem6.4.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.2●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.rotateRows_isometry
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hV : V.transpose * V = 1)
  (i j : Fin N) (hij : i ≠ j) (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows V i j
          theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.rotateRows V i j theta =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.rotateRows_isometry
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hV : V.transpose * V = 1) (i j : Fin N)
  (hij : i ≠ j) (theta : ℝ) :
  (QuantumBlockEncoding.AdjacentGivens.rotateRows
          V i j theta).transpose *
      QuantumBlockEncoding.AdjacentGivens.rotateRows
        V i j theta =
    1

Theorem6.4.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.3●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_isometry
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hV : V.transpose * V = 1)
  (col : Fin r) (lo count : ℕ) (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep V col lo count
          bound).transpose *
      QuantumBlockEncoding.AdjacentGivens.columnSweep V col lo count
        bound =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_isometry
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hV : V.transpose * V = 1) (col : Fin r)
  (lo count : ℕ)
  (bound : lo + count < N) :
  (QuantumBlockEncoding.AdjacentGivens.columnSweep
          V col lo count
          bound).transpose *
      QuantumBlockEncoding.AdjacentGivens.columnSweep
        V col lo count bound =
    1

Theorem6.4.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.4●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.zero_of_fixed_column
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r ≤ N)
  (hV : V.transpose * V = 1) (old col : Fin r) (different : old ≠ col)
  (fixed :
    ∀ (row : Fin N),
      V row old = if row = Fin.castLE hr old then 1 else 0) :
  V (Fin.castLE hr old) col = 0

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.zero_of_fixed_column
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r ≤ N) (hV : V.transpose * V = 1)
  (old col : Fin r)
  (different : old ≠ col)
  (fixed :
    ∀ (row : Fin N),
      V row old =
        if row = Fin.castLE hr old then 1
        else 0) :
  V (Fin.castLE hr old) col = 0

Theorem6.4.5

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

Lean code for Theorem6.4.5●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r ≤ N) (col : Fin r)
  (count : ℕ) (bound : ↑col + count < N)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns V
      hr ↑col) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.AdjacentGivens.columnSweep V col (↑col) count
      bound)
    hr ↑col

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r ≤ N) (col : Fin r) (count : ℕ)
  (bound : ↑col + count < N)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
      V hr ↑col) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.AdjacentGivens.columnSweep
      V col (↑col) count bound)
    hr ↑col

Theorem6.4.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.6●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.supported_column_sq
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r ≤ N)
  (hV : V.transpose * V = 1) (col : Fin r)
  (support : ∀ (row : Fin N), row ≠ Fin.castLE hr col → V row col = 0) :
  V (Fin.castLE hr col) col ^ 2 = 1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.supported_column_sq
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r ≤ N) (hV : V.transpose * V = 1)
  (col : Fin r)
  (support :
    ∀ (row : Fin N),
      row ≠ Fin.castLE hr col →
        V row col = 0) :
  V (Fin.castLE hr col) col ^ 2 = 1

Theorem6.4.7

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. A nonfinal rectangular isometry column is swept to a positive unit pivot.

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

Technical source note. A nonfinal rectangular isometry column is swept to a positive unit pivot.

Declaration kind. theorem.

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

Lean code for Theorem6.4.7●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_prefix_succ
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r ≤ N)
  (hV : V.transpose * V = 1) (col : Fin r) (count : ℕ)
  (dimension : ↑col + count + 1 = N) (positive : 0 < count)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns V
      hr ↑col) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.AdjacentGivens.columnSweep V col (↑col) count
      ⋯)
    hr (↑col + 1)

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.columnSweep_prefix_succ
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r ≤ N) (hV : V.transpose * V = 1)
  (col : Fin r) (count : ℕ)
  (dimension : ↑col + count + 1 = N)
  (positive : 0 < count)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
      V hr ↑col) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.AdjacentGivens.columnSweep
      V col (↑col) count ⋯)
    hr (↑col + 1)

A nonfinal rectangular isometry column is swept to a positive unit pivot.

Theorem6.4.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sweep prefix”; the hypotheses and conclusion in the code panel fix its exact scope. The shared rectangular sweep fixes every processed isometry column.

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

Technical source note. The shared rectangular sweep fixes every processed isometry column.

Declaration kind. theorem.

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

Lean code for Theorem6.4.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.sweep_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r < N)
  (hV : V.transpose * V = 1) (k remaining : ℕ)
  (columns : k + remaining ≤ r)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns V
      ⋯ k) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.RectangularGivens.sweep V k remaining columns)
    ⋯ (k + remaining)

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.sweep_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r < N) (hV : V.transpose * V = 1)
  (k remaining : ℕ)
  (columns : k + remaining ≤ r)
  (fixed :
    QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
      V ⋯ k) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.RectangularGivens.sweep
      V k remaining columns)
    ⋯ (k + remaining)

The shared rectangular sweep fixes every processed isometry column.

Theorem6.4.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.9●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.reduced_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r < N)
  (hV : V.transpose * V = 1) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.RectangularGivens.reduced V) ⋯ r

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.reduced_prefix
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r < N)
  (hV : V.transpose * V = 1) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.PrefixColumns
    (QuantumBlockEncoding.RectangularGivens.reduced
      V)
    ⋯ r

Definition6.4.10

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “prefix completion”. Inverse of the explicitly computed row rotations; no matrix witness is chosen.

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. Inverse of the explicitly computed row rotations; no matrix witness is chosen.

Declaration kind. def.

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

Lean code for Definition6.4.10●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
  {N r : ℕ}
  (V : Matrix (Fin N) (Fin r) ℝ) :
  Matrix (Fin N) (Fin N) ℝ

Inverse of the explicitly computed row rotations; no matrix witness is chosen.

Theorem6.4.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.11●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_orthogonal
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
          V).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
        V =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_orthogonal
  {N r : ℕ}
  (V : Matrix (Fin N) (Fin r) ℝ) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
          V).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
        V =
    1

Theorem6.4.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.12●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_det
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
        V).det =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_det
  {N r : ℕ}
  (V : Matrix (Fin N) (Fin r) ℝ) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
        V).det =
    1

Theorem6.4.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.13●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_columns
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ) (hr : r < N)
  (hV : V.transpose * V = 1) (row : Fin N) (col : Fin r) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion V
      row (Fin.castLE ⋯ col) =
    V row col

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion_columns
  {N r : ℕ} (V : Matrix (Fin N) (Fin r) ℝ)
  (hr : r < N) (hV : V.transpose * V = 1)
  (row : Fin N) (col : Fin r) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.prefixCompletion
      V row (Fin.castLE ⋯ col) =
    V row col

Definition6.4.14

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “extend prefix”. Greedy swaps deterministically extend a finite prefix injection.

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. Greedy swaps deterministically extend a finite prefix injection.

Declaration kind. def.

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

Lean code for Definition6.4.14●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
  {N r : ℕ} (hr : r ≤ N) (e : Fin r ↪ Fin N) (k : ℕ) :
  k ≤ r → Equiv.Perm (Fin N)

def QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
  {N r : ℕ} (hr : r ≤ N)
  (e : Fin r ↪ Fin N) (k : ℕ) :
  k ≤ r → Equiv.Perm (Fin N)

Greedy swaps deterministically extend a finite prefix injection.

Theorem6.4.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.15●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix_agrees
  {N r : ℕ} (hr : r ≤ N) (e : Fin r ↪ Fin N) (k : ℕ) (hk : k ≤ r)
  (a : Fin r) (ha : ↑a < k) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix hr e
        k hk)
      (Fin.castLE hr a) =
    e a

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix_agrees
  {N r : ℕ} (hr : r ≤ N)
  (e : Fin r ↪ Fin N) (k : ℕ) (hk : k ≤ r)
  (a : Fin r) (ha : ↑a < k) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.extendPrefix
        hr e k hk)
      (Fin.castLE hr a) =
    e a

Definition6.4.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “unused position”. The first unused original coordinate is carried to an unused physical label.

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 first unused original coordinate is carried to an unused physical label.

Declaration kind. def.

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

Lean code for Definition6.4.16●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition
  {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N) : Fin N

def QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition
  {N r : ℕ} (hr : r < N)
  (e : Fin r ↪ Fin N) : Fin N

The first unused original coordinate is carried to an unused physical label.

Theorem6.4.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.17●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition_ne
  {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N) (a : Fin r) :
  e a ≠
    QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition
      hr e

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition_ne
  {N r : ℕ} (hr : r < N)
  (e : Fin r ↪ Fin N) (a : Fin r) :
  e a ≠
    QuantumBlockEncoding.ConstructiveIsometryCompletion.unusedPosition
      hr e

Definition6.4.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “permute columns”. Send original column 'a' to physical column 'p a'.

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. Send original column 'a' to physical column 'p a'.

Declaration kind. def.

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

Lean code for Definition6.4.18●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (p : Equiv.Perm (Fin N)) :
  Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (p : Equiv.Perm (Fin N)) :
  Matrix (Fin N) (Fin N) ℝ

Send original column `a` to physical column `p a`.

Theorem6.4.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “permute columns apply”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

Lean code for Theorem6.4.19●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_apply
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (p : Equiv.Perm (Fin N))
  (row col : Fin N) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns U p
      row (p col) =
    U row col

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_apply
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (p : Equiv.Perm (Fin N))
  (row col : Fin N) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
      U p row (p col) =
    U row col

Theorem6.4.20

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.20●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_orthogonal
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (hU : U.transpose * U = 1)
  (p : Equiv.Perm (Fin N)) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns U
          p).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
        U p =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_orthogonal
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (hU : U.transpose * U = 1)
  (p : Equiv.Perm (Fin N)) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
          U p).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
        U p =
    1

Theorem6.4.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.21●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_det
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (p : Equiv.Perm (Fin N)) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns U
        p).det =
    ↑↑(Equiv.Perm.sign p) * U.det

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns_det
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (p : Equiv.Perm (Fin N)) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.permuteColumns
        U p).det =
    ↑↑(Equiv.Perm.sign p) * U.det

Definition6.4.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “orient columns”. Correct only an unused column, using finite permutation parity, not a determinant test.

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. Correct only an unused column, using finite permutation parity, not a determinant test.

Declaration kind. def.

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

Lean code for Definition6.4.22●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (p : Equiv.Perm (Fin N))
  (unused : Fin N) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (p : Equiv.Perm (Fin N))
  (unused : Fin N) :
  Matrix (Fin N) (Fin N) ℝ

Correct only an unused column, using finite permutation parity, not a determinant test.

Theorem6.4.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.23●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_orthogonal
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (hU : U.transpose * U = 1)
  (p : Equiv.Perm (Fin N)) (unused : Fin N) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns U p
          unused).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
        U p unused =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_orthogonal
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (hU : U.transpose * U = 1)
  (p : Equiv.Perm (Fin N))
  (unused : Fin N) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
          U p unused).transpose *
      QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
        U p unused =
    1

Theorem6.4.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.24●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_det
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (hU : U.det = 1)
  (p : Equiv.Perm (Fin N)) (unused : Fin N) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns U p
        unused).det =
    1

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_det
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (hU : U.det = 1)
  (p : Equiv.Perm (Fin N))
  (unused : Fin N) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
        U p unused).det =
    1

Theorem6.4.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.25●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_preserves
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ) (p : Equiv.Perm (Fin N))
  (unused row col : Fin N) (hcol : p col ≠ unused) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns U p
      unused row (p col) =
    U row col

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns_preserves
  {N : ℕ} (U : Matrix (Fin N) (Fin N) ℝ)
  (p : Equiv.Perm (Fin N))
  (unused row col : Fin N)
  (hcol : p col ≠ unused) :
  QuantumBlockEncoding.ConstructiveIsometryCompletion.orientColumns
      U p unused row (p col) =
    U row col

Definition6.4.26

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “place columns”. Explicit physical-column placement of a prefix SO completion.

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. Explicit physical-column placement of a prefix SO completion.

Declaration kind. def.

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

Lean code for Definition6.4.26●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
  {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N)
  (U : Matrix (Fin N) (Fin N) ℝ) : Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
  {N r : ℕ} (hr : r < N)
  (e : Fin r ↪ Fin N)
  (U : Matrix (Fin N) (Fin N) ℝ) :
  Matrix (Fin N) (Fin N) ℝ

Explicit physical-column placement of a prefix SO completion.

Theorem6.4.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “place columns spec”; 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/ConstructiveIsometryCompletion.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.4.27●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns_spec
  {N r : ℕ} (hr : r < N) (e : Fin r ↪ Fin N)
  (U : Matrix (Fin N) (Fin N) ℝ) (hU : U.transpose * U = 1)
  (hd : U.det = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns hr e
            U).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
          hr e U =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns hr
            e U).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
            hr e U row (e a) =
          U row (Fin.castLE ⋯ a)

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns_spec
  {N r : ℕ} (hr : r < N)
  (e : Fin r ↪ Fin N)
  (U : Matrix (Fin N) (Fin N) ℝ)
  (hU : U.transpose * U = 1)
  (hd : U.det = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
            hr e U).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
          hr e U =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
            hr e U).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.placeColumns
            hr e U row (e a) =
          U row (Fin.castLE ⋯ a)

Definition6.4.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “complete”. Actual deterministic SO matrix with columns at the prescribed physical positions.

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. Actual deterministic SO matrix with columns at the prescribed physical positions.

Declaration kind. def.

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

Lean code for Definition6.4.28●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.complete {N r : ℕ}
  (hr : r < N) (V : Matrix (Fin N) (Fin r) ℝ) (e : Fin r ↪ Fin N) :
  Matrix (Fin N) (Fin N) ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
  {N r : ℕ} (hr : r < N)
  (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N) :
  Matrix (Fin N) (Fin N) ℝ

Actual deterministic SO matrix with columns at the prescribed physical positions.

Theorem6.4.29

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “complete spec”; the hypotheses and conclusion in the code panel fix its exact scope. The supplied hypothesis is only the input column isometry; the returned matrix is computed by the named producer, not supplied or selected existentially.

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

Technical source note. The supplied hypothesis is only the input column isometry; the returned matrix is computed by the named producer, not supplied or selected existentially.

Declaration kind. theorem.

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

Lean code for Theorem6.4.29●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.complete_spec
  {N r : ℕ} (hr : r < N) (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N) (hV : V.transpose * V = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr V
            e).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr
          V e =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr V
            e).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.complete hr
            V e row (e a) =
          V row a

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.complete_spec
  {N r : ℕ} (hr : r < N)
  (V : Matrix (Fin N) (Fin r) ℝ)
  (e : Fin r ↪ Fin N)
  (hV : V.transpose * V = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
            hr V e).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
          hr V e =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
            hr V e).det =
        1 ∧
      ∀ (row : Fin N) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.complete
            hr V e row (e a) =
          V row a

The supplied hypothesis is only the input column isometry; the returned
matrix is computed by the named producer, not supplied or selected existentially.

Definition6.4.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “complete named”. Transport using a supplied explicit coordinate equivalence, not an arbitrary enumeration chosen for the named basis.

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. Transport using a supplied explicit coordinate equivalence, not an arbitrary enumeration chosen for the named basis.

Declaration kind. def.

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

Lean code for Definition6.4.30●1 definition

defdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

def QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed.{u_1}
  {I : Type u_1} [Fintype I] [DecidableEq I] {N r : ℕ}
  (coordinates : I ≃ Fin N) (hr : r < N) (V : Matrix I (Fin r) ℝ)
  (e : Fin r ↪ I) : Matrix I I ℝ

def QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed.{u_1}
  {I : Type u_1} [Fintype I]
  [DecidableEq I] {N r : ℕ}
  (coordinates : I ≃ Fin N) (hr : r < N)
  (V : Matrix I (Fin r) ℝ)
  (e : Fin r ↪ I) : Matrix I I ℝ

Transport using a supplied explicit coordinate equivalence, not an arbitrary
enumeration chosen for the named basis.

Theorem6.4.31

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.4.31●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveIsometryCompletion.lean

complete

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed_spec.{u_1}
  {I : Type u_1} [Fintype I] [DecidableEq I] {N r : ℕ}
  (coordinates : I ≃ Fin N) (hr : r < N) (V : Matrix I (Fin r) ℝ)
  (e : Fin r ↪ I) (hV : V.transpose * V = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V e).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
          coordinates hr V e =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V e).det =
        1 ∧
      ∀ (row : I) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V e row (e a) =
          V row a

theorem QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed_spec.{u_1}
  {I : Type u_1} [Fintype I]
  [DecidableEq I] {N r : ℕ}
  (coordinates : I ≃ Fin N) (hr : r < N)
  (V : Matrix I (Fin r) ℝ) (e : Fin r ↪ I)
  (hV : V.transpose * V = 1) :
  (QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V
            e).transpose *
        QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
          coordinates hr V e =
      1 ∧
    (QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V e).det =
        1 ∧
      ∀ (row : I) (a : Fin r),
        QuantumBlockEncoding.ConstructiveIsometryCompletion.completeNamed
            coordinates hr V e row (e a) =
          V row a