Gram–Schmidt Coordinates in the Coefficient Field

Abstract

The trace Hankel inner product preserves the coefficient field during Gram–Schmidt.

Theorem 1.1 (Every orthogonalized coordinate belongs to the coefficient-generated subfield).

$$\begin{array}{r}F=\mathrm{subfieldClosure}\left(\mathrm{range}\left(\mathrm{coeff}\left(q\right)\right)\right)\\ m\left(n\right)=\frac{\mathrm{trace}\left(\mathrm{coefficientMultiplicationMatrix}{\left(q\right)}^n\right)}{\mathrm{natDegree}\left(q\right)}\\ (\forall x,y\in E,\mathrm{inner}\left(x,y\right)=\mathrm{coefficientHankelValue}\left(power,m,x,y\right))\Rightarrow \\ \forall i,j\in \mathrm{Fin}\left(\mathrm{natDegree}\left(q\right)\right),\mathrm{repr}\left(power,\mathrm{gramSchmidtBasis}\left(power\right)\left(i\right),j\right)\in F.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Constants/Moments/GramSchmidtCoefficientField.gram_schmidt_coordinates_mem_coefficient_field (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let q be a real polynomial, d its natural degree, and power a real basis of an inner product space E indexed by Fin d. Set S to the canonical coefficientMultiplicationMatrix of q and m(n) to trace(S^n)/d. Assume that the inner product equals coefficientHankelValue power m for every pair of vectors. Let F be the subfield of the reals generated by all coefficients of q.

Every entry of S belongs to F. Induction on matrix powers, finite sums, and division by the natural number d place all moments in F. The finite Hankel sum therefore pairs vectors with F-valued coordinates to an element of F.

Induction on the Gram–Schmidt index now preserves coordinate membership. A basis vector starts with zero-one coordinates. Each projection subtracts a previous orthogonalized vector multiplied by the ratio of its inner product with the input vector to its inner product with itself. Both inner products and all previous coordinates belong to F, which is closed under these field operations.

The basis is unnormalized. No square-root closure is asserted. Monicity and positive degree are unnecessary for this invariant. The theorem assumes the trace Hankel identity; it neither constructs that inner product nor identifies traces with an enumeration of roots. Membership of later Jacobi parameters and chain weights is not part of this declaration.

References

• Truth anchor: D5/S3/Constants/Moments/GramSchmidtCoefficientField.gram_schmidt_coordinates_mem_coefficient_field
• Dependency: D5/S3/Constants/Moments/CoefficientDrivenJacobiCharacteristicPolynomial