Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Unimodular coordinate obstruction

Abstract

An integral unimodular action with a vanishing inverse coordinate forces unbounded prime-index violations of local Dold divisibility.

The local Dold condition in D5/L/Scale/chuysurichay2026fibdold requires every positive integer n to divide the integer Möbius sum of the p-parts of a(d), over positive divisors d of n. The repository derivation here supplies a sufficient obstruction for positive coordinates of integer unimodular dynamics.

Definition 1.1 (Prime part).

Lean statement: D5/S3/Arith/LocalDold/UnimodularObstruction.pPart

Formalization. D5/S3/Arith/LocalDold/UnimodularObstruction.pPart (✓ std3).

Source. Repository-derived.

Commentary.

For natural numbers p and x, pPart(p,x) is p raised to padicValNat(p,x). The theorem uses prime p and strictly positive x; no claim relies on the valuation convention at zero.

Definition 1.2 (Integral invertible matrices).

Lean statement: D5/S3/Arith/LocalDold/UnimodularObstruction.GLInt

Formalization. D5/S3/Arith/LocalDold/UnimodularObstruction.GLInt (✓ std3).

Source. Repository-derived.

Commentary.

For every natural dimension d, GLInt(d) is Mathlib’s general linear group on Fin d over the integers. Its inverse is integral.

Theorem 1.3 (Unbounded prime-index violations).

Lean statement: D5/S3/Arith/LocalDold/UnimodularObstruction.unimodular_coordinate_obstruction

Proof. Machine-checked in Lean as D5/S3/Arith/LocalDold/UnimodularObstruction.unimodular_coordinate_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural d, A in GLInt(d), integral vector v and i in Fin d, assume (A inverse applied to v)(i)=0. Let a be a natural sequence such that, for every positive n, a(n)=(A^n v)(i) and a(n)>0, and assume a(1)=1. For every prime p and every natural bound H, there exists a prime q>H for which S=sum over d dividing q of μ(q/d) pPart(p,a(d)) satisfies 0<S<q and q does not divide S in the integers. Both p=2 and H=0 are included.

Reduction of A modulo p lies in a finite general linear group, giving a positive period T. In the commutative ring of integer polynomials, Mathlib SModEq.pow_pow_add_one gives (1+pX)^(p^j)-1 in the ideal generated by p^(j+1). Evaluating at the integral matrix C in A^T=I+pC gives A^(T*p^j)=I+p^(j+1)D. Polynomial.aeval allows this noncommutative target. This weak lift works at 2 and does not require an exact matrix order or an LTE formula.

Set r=pT-1 and e=valuation_p(a(r)). The actual inverse observation gives p dividing a(r); positivity gives a(r) nonzero and e>=1. For M=T*p^e, one has 0<r<M and gcd(r,M)=1, even when p divides T. The lifted period modulo p^(e+1) preserves the exact valuation e throughout the positive progression r+kM. Dirichlet supplies a prime in this class above H, r and p^e-1. Its Möbius sum is p^e-1, a positive integer smaller than q.

The source prints the prefixes T=(1,1,2,4,…) and B=(1,1,1,2,5,…). Interpreting them by the sum of the preceding three and four terms respectively, the native companion time map at u=1 acts on reversed states. T uses v=(1,1,0), with inverse state (1,0,0); B uses v=(1,1,1,-1), with inverse state (1,1,-1,0). In both cases the last coordinate is the observed positive-index sequence. The value -1 is only B’s integer modeling extension at zero. Applying the generic obstruction to each source sequence requires these native coordinate identifications and positivity at every positive index; it requires no positive value at index zero.

References