Common-Denominator Polynomial Basis

Abstract

Distinct finite Cayley scales give a common-denominator polynomial basis.

Theorem 1.1 (The common-denominator family is a basis).

$$\begin{array}{r}\forall m:\mathbb{N},r:\mathrm{Fin}(m)\to \mathbb{C},depth:\mathrm{Fin}(m)\to \mathbb{N},\\ referenceDepth:\mathbb{N},\\ rNonzero:\forall i\in \mathrm{Fin}(m),r(i)\ne 0,rInjective:\mathrm{Injective}(r),\\ rInDisk:\forall i\in \mathrm{Fin}(m),\mathrm{norm}(r(i))<1,\\ \mathrm{let}(multiplicity:\mathrm{Fin}(m)\to \mathbb{N},\forall i:\mathrm{Fin}(m),multiplicity(i)=depth(i)+1q:\mathbb{N}=\mathrm{sum}(\mathrm{Fin}(m),(i:\mathrm{Fin}(m)\mapsto multiplicity(i)))factor:\mathrm{Fin}(m)\to \mathrm{Polynomial}(\mathbb{C}),\forall i:\mathrm{Fin}(m),factor(i)=1+C(r(i))\cdot XD:\mathrm{Polynomial}(\mathbb{C})=\mathrm{prod}(\mathrm{Fin}(m),(i:\mathrm{Fin}(m)\mapsto \mathrm{pow}(factor(i),multiplicity(i))))I:\mathrm{Type}()=\mathrm{Sum}(\mathrm{Sigma}(\mathrm{Fin}(m),(i:\mathrm{Fin}(m)\mapsto \mathrm{Fin}(multiplicity(i)))),\mathrm{Fin}(referenceDepth+1))p:I\to \mathrm{Polynomial}(\mathbb{C}),\forall i:\mathrm{Fin}(m),j:\mathrm{Fin}(multiplicity(i)),p(\mathrm{inl}(i,j))=\mathrm{pow}(X+C(r(i)),j)\cdot \mathrm{pow}(factor(i),depth(i)-j)\cdot \mathrm{prodExcept}(\mathrm{Fin}(m),i,(k:\mathrm{Fin}(m)\mapsto \mathrm{pow}(factor(k),multiplicity(k))))\forall j:\mathrm{Fin}(referenceDepth+1),p(\mathrm{inr}(j))=D\cdot \mathrm{pow}(X,j)),\\ \mathrm{LinearIndependent}(\mathbb{C},p)\wedge \mathrm{span}(\mathbb{C},\mathrm{range}(p))=\mathrm{degreeLT}(\mathbb{C},q+referenceDepth+1).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/BlockStructure/CommonDenominatorPolynomialBasis.common_denominator_polynomial_basis (✓ std3). ∎

Source. Repository-derived.

Commentary.

The family is constructed from the supplied distinct nonzero complex parameters, their multiplicities, and the common polynomial denominator.

A local affine transport of the Bernstein family proves independence within each scale. Uniqueness of partial fractions then separates the scale blocks.

The reference block supplies the remaining top degrees. Independence and the matching finite dimension identify the span with the full bounded-degree polynomial subspace.

References

• Truth anchor: D5/S3/Observer/BlockStructure/CommonDenominatorPolynomialBasis.common_denominator_polynomial_basis