Orthonormality of the executable Gram–Schmidt Q factor (Qᵀ Q = 1)

This file closes the one finite-fold property left open by NN.Proofs.Tensor.Basic.FactorizationsReconstruction: the orthonormality of the Q factor produced by the executable classical Gram–Schmidt gramSchmidtFn.

The strategy is to unify the executable variant with Mathlib's gramSchmidt rather than re-derive the orthogonality induction by hand. Reading the columns of A as vectors of EuclideanSpace ℝ (Fin m), the j-th executable Q column equals Mathlib's gramSchmidtNormed ℝ of the column map (Qcol_bridge), so the orthonormality follows from Mathlib's gramSchmidtNormed_orthonormal'.

Main results

• Qcol_bridge: WithLp.toLp 2 (Qcol A k) = gramSchmidtNormed ℝ (gsCol A) k — the executable Q column is Mathlib's normalized Gram–Schmidt vector, proved by strong induction on k.
• Q_orthonormal: dotFn (Qcol A a) (Qcol A b) = if a = b then 1 else 0 under positive R pivots.
• QT_mul_Q_eq_one and isQR_of_pos: the matrix-level Qᵀ Q = 1 and the full Spec.Factorization.IsQR predicate for the executable factors (combining with the reconstruction A = Q · R and R upper-triangular from the companion file).
• qrSpec_orthonormal: the tensor-level corollary.

Method

The bridge rests on three connectors over ℝ: dotFn = ⟪·,·⟫ and normFn = ‖·‖ on EuclideanSpace ℝ (Fin m), and the projection identity proj_normalize showing the un-normalized Gram–Schmidt projection term equals the normalized one. The strong induction feeds the partial identification of the earlier Q columns into gramSchmidt_def'', term by term.

Connectors between the executable scalar ops and the Euclidean inner product

theorem Spec.Factorization.Reconstruction.dotFn_eq_sum {p : ℕ} (u v : Fin p → ℝ) : dotFn u v = ∑ i : Fin p, u i * v i

dotFn as a Finset sum.

theorem Spec.Factorization.Reconstruction.dotFn_eq_inner {p : ℕ} (u v : Fin p → ℝ) : dotFn u v = inner ℝ (WithLp.toLp 2 u) (WithLp.toLp 2 v)

The executable dot product is the Euclidean inner product over ℝ.

theorem Spec.Factorization.Reconstruction.normFn_eq_norm {p : ℕ} (v : Fin p → ℝ) : normFn v = ‖WithLp.toLp 2 v‖

The executable Euclidean norm is the EuclideanSpace norm over ℝ.

theorem Spec.Factorization.Reconstruction.proj_normalize {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (w x : F) : (inner ℝ w x / ‖w‖ ^ 2) • w = inner ℝ (‖w‖⁻¹ • w) x • ‖w‖⁻¹ • w

The Gram–Schmidt projection term, with the normalized vector pulled out. Holds with no non-degeneracy hypothesis (both sides vanish when gramSchmidt = 0).

theorem Spec.Factorization.Reconstruction.gn_eq {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [InnerProductSpace ℝ F] (f : Fin n → F) (i : Fin n) : InnerProductSpace.gramSchmidtNormed ℝ f i = ‖InnerProductSpace.gramSchmidt ℝ f i‖⁻¹ • InnerProductSpace.gramSchmidt ℝ f i

gramSchmidtNormed over ℝ, with the scalar coercion removed.

theorem Spec.Factorization.Reconstruction.sum_Iio_eq_mask {n : ℕ} (k : Fin n) (h : Fin n → ℝ) : ∑ i ∈ Finset.Iio k, h i = ∑ i : Fin n, if ↑i < ↑k then h i else 0

A masked full sum equals the sum over Iio.

The bridge to Mathlib's gramSchmidt

noncomputable def Spec.Factorization.Reconstruction.gsCol {m n : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : EuclideanSpace ℝ (Fin m)

Column j of A as a vector of EuclideanSpace ℝ (Fin m).

theorem Spec.Factorization.Reconstruction.gsCol_apply {m n : ℕ} (A : Fin m → Fin n → ℝ) (k : Fin n) (r : Fin m) : (gsCol A k).ofLp r = gsA A k r

gsCol A k reads as the executable column gsA A k.

theorem Spec.Factorization.Reconstruction.gsV_bridge {m n : ℕ} (A : Fin m → Fin n → ℝ) (k : Fin n) (ih : ∀ (i : Fin n), ↑i < ↑k → WithLp.toLp 2 (Qcol A i) = InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) i) : InnerProductSpace.gramSchmidt ℝ (gsCol A) k = WithLp.toLp 2 (gsV A (qsPrefix A k) k)

Orthogonalized-vector bridge. Given that the earlier Q columns coincide with Mathlib's normalized Gram–Schmidt vectors, the executable orthogonalized vector v at index k equals Mathlib's (un-normalized) gramSchmidt vector.

theorem Spec.Factorization.Reconstruction.Qcol_bridge {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (k : Fin n) : WithLp.toLp 2 (Qcol A k) = InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) k

Normalized-column bridge. The executable Q column at index k equals Mathlib's gramSchmidtNormed. Proved by strong induction on k, under positive R pivots (full column rank).

Orthonormality Qᵀ Q = 1

theorem Spec.Factorization.Reconstruction.gn_ne_zero {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (j : Fin n) : InnerProductSpace.gramSchmidtNormed ℝ (gsCol A) j ≠ 0

Each normalized Gram–Schmidt vector is non-zero (the pivot is positive).

theorem Spec.Factorization.Reconstruction.Q_orthonormal {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (a b : Fin n) : dotFn (Qcol A a) (Qcol A b) = if a = b then 1 else 0

Orthonormality of the executable Q columns. Under positive R pivots, qₐ · q_b = δₐᵦ.

theorem Spec.Factorization.Reconstruction.QT_mul_Q_eq_one {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) : ((Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k).transpose * Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k) = 1

Matrix-level orthonormality. Qᵀ Q = 1 for the executable Gram–Schmidt Q factor.

theorem Spec.Factorization.Reconstruction.isQR_of_pos {m n : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) : IsQR (Matrix.of A) (Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k) (Matrix.of fun (k j : Fin n) => Rmat A k j)

Full QR specification. For A with positive executable R-pivots (full column rank), the executable Gram–Schmidt factors satisfy Spec.Factorization.IsQR: Qᵀ Q = 1, R upper-triangular, and A = Q · R.

theorem Spec.Factorization.Reconstruction.qrSpec_orthonormal {m n : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (hrank : ∀ (j : Fin n), 0 < get2 (qrRSpec A) j j) (a b : Fin n) : ∑ i : Fin m, get2 (qrQSpec A) i a * get2 (qrQSpec A) i b = if a = b then 1 else 0

Tensor-level orthonormality. For a tensor A with positive qrRSpec pivots, the Q factor qrQSpec A has orthonormal columns: Σ_i Q[i,a]·Q[i,b] = δₐᵦ.