First-vertex cyclic companion module

Abstract

Forward companion time is cyclic at the first vertex over every commutative ring.

A is any commutative ring, u is any element, and q is positive. CommRingType includes the ring instance; Positive(q) is the premise 0<q. The zero ring and q=1 are included. No involution, unit, nontriviality, domain or field assumption occurs. Row(A,q) means Fin q -> A. Forward time is exactly (Tv)(0)=(sum over j in Fin q of v(j))u and (Tv)(j+1)=v(j). The linear map extends FiniteCompanionSquareDefect.time with J(a)=au. The vector e0 has 1 at vertex zero and 0 elsewhere and serves as the cyclic generator.

Set H(u,j)=X^j-C(u)*sum over k<j of X^k, and P(u,q)=H(u,q). CyclicQ is the canonical ring quotient A[X]/(P), with its polynomial-module action. projection sends a polynomial to its class. coordinatePolynomial(u,q,v) is sum over j in Fin q of C(v(j))*H(u,j). Module.AEval’ time is the row module where X acts by forward time; of is its underlying A-linear identification. evaluate(f)=f(T)e0 is polynomial-linear.

Theorem 1.1 (Exact polynomial kernel).

$$\forall A\in CommRingType,u\in A,q\in Nat,hq\in \mathrm{Positive}\left(q\right),\ker \left(\mathrm{evaluate}\left(u,q,hq\right)\right)=\mathrm{principalIdeal}\left(P\left(u,q\right)\right)$$

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

Source. Repository-derived.

Commentary.

The kernel is exactly the principal ideal generated by P. The quotient coordinate map sends f(T)e0 back to projection(f), so no additional polynomial relation is lost. Conversely P(T)e0=0 annihilates every multiple of P. This exact equality is used by the quotient equivalence constructor.

Theorem 1.2 (Normalized equivalence and explicit inverse).

$$\forall A\in CommRingType,u\in A,q\in Nat,hq\in \mathrm{Positive}\left(q\right),\left(\forall f\in \mathrm{Polynomial}\left(A\right),\mathrm{cyclicEquiv}\left(u,q,hq,\mathrm{projection}\left(u,q,f\right)\right)=\mathrm{of}\left(\mathrm{time}\left(u,q,hq\right),\mathrm{apply}\left(\mathrm{aeval}\left(\mathrm{time}\left(u,q,hq\right),f\right),\mathrm{ezero}\left(q,hq\right)\right)\right)\right)\wedge \left(\left(\forall v\in \mathrm{Row}\left(A,q\right),\mathrm{inverse}\left(\mathrm{cyclicEquiv}\left(u,q,hq\right),\mathrm{of}\left(\mathrm{time}\left(u,q,hq\right),v\right)\right)=\mathrm{projection}\left(u,q,\mathrm{coordinatePolynomial}\left(u,q,v\right)\right)\right)\wedge \mathrm{cyclicEquiv}\left(u,q,hq,1\right)=\mathrm{of}\left(\mathrm{time}\left(u,q,hq\right),\mathrm{ezero}\left(q,hq\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

cyclicEquiv is an A[X]-linear equivalence. The displayed forward formula, coordinate inverse and normalization are all conjuncts of the Lean theorem. H(u,0)=1 and H(u,j+1)=X*H(u,j)-C(u). The original time equations give H(u,j)(T)e0=e(j) for j<q, and H(u,q)(T)e0=0. The coordinate map intertwines T with X and reconstructs every row. Polynomial linearity and its value 1 at e0 give the other inverse identity. This proof uses no degree reindexing, so it works uniformly over the zero ring. At q=1, P=X-C(u), time is multiplication by u, and the inverse is projection(C(v(0))).

The intended next consumer specializes A to the literal integer sign group ring and u to its reset label. The normalization sends e0 to the polynomial class 1, while forward time is X. This supplies the module presentation needed to relate the original square quotient by range(id+Theta^2) to the additional polynomial relation 1+X^2. That image correspondence, native bridge, oriented branch classifications, five-clock equality and full-action character remain separate proof obligations. This module establishes no global Sign-equivariance, history lift, later classification or literature novelty.

References

• Truth anchor: D5/S1/Recurrence/FiniteCompanionCyclicModule.cyclic_presentation
• Truth anchor: D5/S1/Recurrence/FiniteCompanionCyclicModule.evaluate_ker
• Dependency: D5/S1/Recurrence/FiniteCompanionSquareDefect