Integral growth in rational cyclic power coordinates

Abstract

The whole primitive relation determines exact finite growth of every rational cyclic power lattice.

Let N be any positive natural number and T any N by N rational matrix. The vector b=root(N) has coordinate one at zero and zero elsewhere. For i and j in Fin N, powerMatrix(T)(i,j) is coordinate i of T raised to j applied to b. Write K=powerMatrix(T), and assume det K is nonzero. Let q be a primitive integer polynomial with positive leading coefficient A. Assume its coefficientwise rational image is C(A) times the characteristic polynomial of T. These are exactly the fields of Data: dimension N, positivity, T, the determinant condition, q, primitivity, positive leading coefficient and the displayed polynomial relation. Primitivity means that the coefficients generate the unit ideal. The whole polynomial may be reducible. No symmetry, sign, spectral stability or irreducibility premise is imposed, and A=1 is included. The dimension is the full dimension of T.

$\forall d\in Data,\mathrm{mapToRat}\left(\mathrm{relationPolynomial}\left(d\right)\right)=C\left(\mathrm{leadingCoeff}\left(\mathrm{relationPolynomial}\left(d\right)\right)\right)\cdot \mathrm{charpoly}\left(\mathrm{matrix}\left(d\right)\right)$

For d in Data define time(d)=K inverse times T times K and power(d,j)=time(d) raised to j applied to root(N), for every natural j. The inverse and the coordinate changes are rational matrix operations on this same K. For a rational polynomial p, rationalEvaluation(d,p) is K inverse applied to p(T)b. For an integer polynomial p, evaluation(d,p) first maps every coefficient to the rationals and then uses rationalEvaluation. It is an integer linear map into the rational vector space. In particular evaluation of the monomial c X raised to j is c times power(d,j).

For every natural L, lattice(d,L) is the integer span of power(d,j) for j less than L inside the single additive group of rational N-vectors. The notation coordinateZ(N) means the image of all integer N-vectors under coordinatewise inclusion into rational N-vectors. It is defined independently of the powers. SuccessiveQuotient(d,l) is lattice(d,l+1) modulo the subgroup of its elements that belong to lattice(d,l). Its distinguished quotientGenerator is the class of power(d,l). RelativeQuotient(d,L) similarly denotes lattice(d,L) modulo its subgroup of elements belonging to coordinateZ(N). All quotients therefore use subgroups of their actual larger lattices. The relative index has the smaller subgroup as its first argument. Neither an index in the ambient rational space nor a zero cardinality convention is used as evidence of finiteness.

Theorem 1.1 (Whole relation kernel, successive orders and finite relative index).

$$\forall d\in Data,\left(\forall j\in \mathrm{Fin}\left(\mathrm{dimension}\left(d\right)\right),\mathrm{power}\left(d,\mathrm{value}\left(j\right)\right)=\mathrm{standard}\left(\mathrm{dimension}\left(d\right),j\right)\right)\wedge \left(\left(\forall p\in \mathrm{Polynomial}\left(Int\right),\mathrm{evaluation}\left(d,p\right)=0\iff \mathrm{relationPolynomial}\left(d\right)\mid p\right)\wedge \left(\mathrm{lattice}\left(d,\mathrm{dimension}\left(d\right)\right)=\mathrm{coordinateZ}\left(\mathrm{dimension}\left(d\right)\right)\wedge \left(\left(\forall l\in Nat,\mathrm{dimension}\left(d\right)\le l\Rightarrow \left(\left(\forall n\in Int,\mathrm{zsmul}\left(n,\mathrm{power}\left(d,l\right)\right)\in \mathrm{lattice}\left(d,l\right)\iff \mathrm{leadingCoeff}\left(\mathrm{relationPolynomial}\left(d\right)\right)\mid n\right)\wedge \left(\mathrm{addOrderOf}\left(\mathrm{quotientGenerator}\left(d,l\right)\right)=\mathrm{natAbs}\left(\mathrm{leadingCoeff}\left(\mathrm{relationPolynomial}\left(d\right)\right)\right)\wedge \left(\mathrm{Finite}\left(\mathrm{SuccessiveQuotient}\left(d,l\right)\right)\wedge \mathrm{NatCard}\left(\mathrm{SuccessiveQuotient}\left(d,l\right)\right)=\mathrm{natAbs}\left(\mathrm{leadingCoeff}\left(\mathrm{relationPolynomial}\left(d\right)\right)\right)\right)\right)\right)\right)\wedge \left(\forall L\in Nat,\mathrm{dimension}\left(d\right)\le L\Rightarrow \left(\mathrm{Finite}\left(\mathrm{RelativeQuotient}\left(d,L\right)\right)\wedge \mathrm{relIndex}\left(\mathrm{coordinateZ}\left(\mathrm{dimension}\left(d\right)\right),\mathrm{lattice}\left(d,L\right)\right)=\mathrm{pow}\left(\mathrm{natAbs}\left(\mathrm{leadingCoeff}\left(\mathrm{relationPolynomial}\left(d\right)\right)\right),\mathrm{natSub}\left(L,\mathrm{dimension}\left(d\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CyclicPowerLattice.cyclic_power_lattice (✓ std3). ∎

Source. Repository-derived.

Commentary.

Here dimension(d)=d.N, matrix(d)=d.T, relationPolynomial(d)=d.q, and standard(N,j) is the rational vector with one at j and zero elsewhere. Fin(N) is the set of indices less than N and value(j) is its natural index. zsmul is multiplication by an integer, NatCard is natural cardinality, Finite asserts finite type cardinality, and natSub is natural subtraction. The quotient order and cardinality are natAbs(A); since A is positive this is A. Every l and L at least N is included. In particular L=N gives index one. The theorem also identifies every integral polynomial annihilating the actual input with an integral multiple of the whole q, rather than a polynomial vanishing at only one chosen root.

The conjugacy calculation gives power(d,j)=K inverse applied to T raised to j times b. For j less than N the corresponding column of K therefore gives the jth standard vector. A rational polynomial of degree below N evaluates to its coefficient vector in these coordinates. Divide an arbitrary rational polynomial by the monic characteristic polynomial. Cayley-Hamilton removes the multiple, while low-degree coordinate independence forces a vanishing remainder to be zero. Scaling by the nonzero A and applying the supplied primitive-divisibility theorem over the fraction field gives exactly the integral multiples of q. The Gauss step is Polynomial.IsPrimitive.dvd_of_fraction_map_dvd_fraction_map, with coefficient domain Int and fraction field Rat. It needs primitivity of q, without irreducibility.

For l at least N the polynomial q times X raised to l-N has degree l and leading coefficient A. Its lower terms show that A times power(d,l) belongs to lattice(d,l). Conversely an integer n times that new power lying in the earlier lattice gives an annihilator n X raised to l minus a polynomial of degree below l. If n is nonzero its leading coefficient is n, so the whole integral annihilator characterization forces A to divide n. The n=0 case is included directly. Thus the next quotient generator has exactly order A.

The successor lattice is the sum of the earlier lattice and the integer span of the new power. Hence that generator spans the entire successive quotient. Its positive finite order gives an explicit equivalence between a finite index set and its cyclic subgroup, proving quotient finiteness and cardinality A. The first N powers span coordinateZ(N). Multiplying the successive relative indices with AddSubgroup.relIndex_mul_relIndex yields A raised to L-N at every later length. Its nonzero value also gives finiteness of the full relative quotient.

For an acquired positive-link path the retained origin is x_star=T raised to 2N applied to b. This result supplies the algebraic lattice part of the finite-menu chronology argument once its actual K is proved invertible and its earned whole q has the stated normalization. Deriving that native invertibility from the path remains a separate correspondence. The positive stable vector s, the rational coordinate bound R, the integer C, bounded lattice-point counting, word reversal and the same affine baseline are additional steps. This theorem alone does not assert the all-length H less than A threshold or the equal-length collision at N+A C. The retained acquired phase, actual observation calls, historical versus advanced current field, continued service rights, archives and simultaneous numerical resources likewise require their own hypotheses and proofs. Removing an old length input in a different chronology task does not alter the retained-length assertion.

References

• Truth anchor: D5/S1/Recurrence/CyclicPowerLattice.cyclic_power_lattice