6.8. QuantumBlockEncoding/ConstructiveThinLQ.lean🔗

8 explicit public declarations, in source order.

Definition6.8.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “factorization”. A proposition-valued field is a requirement until a constructor supplies it. Actual factors together with the same two equations as 'ThinLQ'.

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

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. Actual factors together with the same two equations as 'ThinLQ'.

Declaration kind. structure.

Source: QuantumBlockEncoding/ConstructiveThinLQ.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.8.1●1 definition

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

complete

structure QuantumBlockEncoding.ConstructiveThinLQ.Factorization {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) (r : ℕ) : Type

structure QuantumBlockEncoding.ConstructiveThinLQ.Factorization
  {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ)
  (r : ℕ) : Type

Actual factors together with the same two equations as `ThinLQ`.

Fields

R : Matrix (Fin m) (Fin r) ℝ

Q : Matrix (Fin r) (Fin n) ℝ

factorization : A = self.R * self.Q

orthogonal : self.Q * self.Q.transpose = 1

Definition6.8.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.2●1 definition

defdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

def QuantumBlockEncoding.ConstructiveThinLQ.wideR {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) : Matrix (Fin m) (Fin m) ℝ

def QuantumBlockEncoding.ConstructiveThinLQ.wideR
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  Matrix (Fin m) (Fin m) ℝ

Definition6.8.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition6.8.3●1 definition

defdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

def QuantumBlockEncoding.ConstructiveThinLQ.wideQ {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) : Matrix (Fin m) (Fin n) ℝ

def QuantumBlockEncoding.ConstructiveThinLQ.wideQ
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  Matrix (Fin m) (Fin n) ℝ

Theorem6.8.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.4●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

theorem QuantumBlockEncoding.ConstructiveThinLQ.wide_factorization {m n : ℕ}
  (hmn : m ≤ n) (A : Matrix (Fin m) (Fin n) ℝ) :
  A =
    QuantumBlockEncoding.ConstructiveThinLQ.wideR hmn A *
      QuantumBlockEncoding.ConstructiveThinLQ.wideQ hmn A

theorem QuantumBlockEncoding.ConstructiveThinLQ.wide_factorization
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  A =
    QuantumBlockEncoding.ConstructiveThinLQ.wideR
        hmn A *
      QuantumBlockEncoding.ConstructiveThinLQ.wideQ
        hmn A

Theorem6.8.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem6.8.5●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

theorem QuantumBlockEncoding.ConstructiveThinLQ.wide_orthogonal {m n : ℕ}
  (hmn : m ≤ n) (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.wideQ hmn A *
      (QuantumBlockEncoding.ConstructiveThinLQ.wideQ hmn A).transpose =
    1

theorem QuantumBlockEncoding.ConstructiveThinLQ.wide_orthogonal
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.wideQ
        hmn A *
      (QuantumBlockEncoding.ConstructiveThinLQ.wideQ
          hmn A).transpose =
    1

Definition6.8.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factor of le”. A deterministic wide-matrix supplier, including zero and repeated rows.

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 deterministic wide-matrix supplier, including zero and repeated rows.

Declaration kind. def.

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

Lean code for Definition6.8.6●1 definition

defdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

def QuantumBlockEncoding.ConstructiveThinLQ.factorOfLE {m n : ℕ}
  (hmn : m ≤ n) (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.Factorization A m

def QuantumBlockEncoding.ConstructiveThinLQ.factorOfLE
  {m n : ℕ} (hmn : m ≤ n)
  (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.Factorization
    A m

A deterministic wide-matrix supplier, including zero and repeated rows.

Definition6.8.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factor”. All shapes are handled by an explicit dimension comparison and recursion.

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. All shapes are handled by an explicit dimension comparison and recursion.

Declaration kind. def.

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

Lean code for Definition6.8.7●1 definition

defdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

def QuantumBlockEncoding.ConstructiveThinLQ.factor {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.Factorization A (min m n)

def QuantumBlockEncoding.ConstructiveThinLQ.factor
  {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  QuantumBlockEncoding.ConstructiveThinLQ.Factorization
    A (min m n)

All shapes are handled by an explicit dimension comparison and recursion.

Theorem6.8.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “factor correct”; the hypotheses and conclusion in the code panel fix its exact scope. The concrete output satisfies the existing all-shape thin-LQ contract.

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

Technical source note. The concrete output satisfies the existing all-shape thin-LQ contract.

Declaration kind. theorem.

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

Lean code for Theorem6.8.8●1 theorem

theoremdefined in QuantumBlockEncoding/ConstructiveThinLQ.lean

complete

theorem QuantumBlockEncoding.ConstructiveThinLQ.factor_correct {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  A =
      (QuantumBlockEncoding.ConstructiveThinLQ.factor A).R *
        (QuantumBlockEncoding.ConstructiveThinLQ.factor A).Q ∧
    (QuantumBlockEncoding.ConstructiveThinLQ.factor A).Q *
        (QuantumBlockEncoding.ConstructiveThinLQ.factor A).Q.transpose =
      1

theorem QuantumBlockEncoding.ConstructiveThinLQ.factor_correct
  {m n : ℕ}
  (A : Matrix (Fin m) (Fin n) ℝ) :
  A =
      (QuantumBlockEncoding.ConstructiveThinLQ.factor
            A).R *
        (QuantumBlockEncoding.ConstructiveThinLQ.factor
            A).Q ∧
    (QuantumBlockEncoding.ConstructiveThinLQ.factor
            A).Q *
        (QuantumBlockEncoding.ConstructiveThinLQ.factor
              A).Q.transpose =
      1

The concrete output satisfies the existing all-shape thin-LQ contract.