Finite Fibonacci Sampling Smith Defect

Abstract

Strictly increasing Fibonacci samples have an integral rectangular normal form and an exact modular kernel defect.

Theorem 1.1 (Fibonacci sampling has a gcd controlled Smith defect).

$$\forall m\in \mathbb{N},\forall t:\mathrm{Fin}\left(m\right)\to \mathbb{N},(2\le m\wedge \mathrm{StrictMono}\left(t\right)\Rightarrow leti0=\mathrm{zero}\left(\mathrm{Fin}\left(m\right)\right),letg=\gcd \left(\mathrm{erase}\left(\mathrm{univ}\left(\mathrm{Fin}\left(m\right)\right),i0\right),funi\Rightarrow t\left(i\right)-t\left(i0\right)\right),letH:\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(2\right),\mathbb{Z}\right)=funi\Rightarrow \mathrm{row}\left(\mathrm{IntCast}\left(\mathrm{fib}\left(t\left(i\right)\right)\right),\mathrm{IntCast}\left(\mathrm{fib}\left(t\left(i\right)+1\right)\right)\right),letD:\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(2\right),\mathbb{Z}\right)=funi,j\Rightarrow \mathrm{if}\left((\mathrm{val}\left(i\right)=0)\wedge (j=0),1,\mathrm{if}\left((\mathrm{val}\left(i\right)=1)\wedge (j=1),\mathrm{IntCast}\left(\mathrm{fib}\left(g\right)\right),0\right)\right),in0<\mathrm{fib}\left(g\right)\wedge \exists U:\mathrm{Units}\left(\mathrm{Matrix}\left(\mathrm{Fin}\left(m\right),\mathrm{Fin}\left(m\right),\mathbb{Z}\right)\right),\exists V:\mathrm{Units}\left(\mathrm{Matrix}\left(\mathrm{Fin}\left(2\right),\mathrm{Fin}\left(2\right),\mathbb{Z}\right)\right),(\mathrm{mul}\left(\mathrm{val}\left(U\right),H,\mathrm{val}\left(V\right)\right)=D)\wedge (\forall N\in \mathbb{N},(0<N\Rightarrow ((\mathrm{card}\left(\ker \left(\mathrm{mulVecLin}\left(\mathrm{map}\left(H,\mathrm{castRingHom}\left(\mathrm{ZMod}\left(N\right)\right)\right)\right)\right)\right)=\gcd \left(N,\mathrm{fib}\left(g\right)\right))\wedge (\mathrm{Injective}\left(\mathrm{mulVec}\left(\mathrm{map}\left(H,\mathrm{castRingHom}\left(\mathrm{ZMod}\left(N\right)\right)\right)\right)\right)⟺\gcd \left(N,\mathrm{fib}\left(g\right)\right)=1)))))$$

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

Source. Repository-derived.

Commentary.

Let m be at least two and let t : Fin(m) -> N be strictly increasing. The first sample index is i0 = 0, and g is the finite gcd of all noninitial differences t(i) - t(i0). The actual row at i is (Nat.fib(t(i)), Nat.fib(t(i)+1)) over Z; no abstract replacement matrix is used.

The theorem supplies units U and V over the displayed rectangular integer matrix spaces. Their product with H is the displayed D: a 1 at (0,0), Nat.fib(g) at (1,1), and zero elsewhere. Nat.fib(g) is positive as the second factor, including the smallest admissible time configuration.

For every positive natural modulus N, including N = 1, reduce the same actual matrix by Int.castRingHom into ZMod(N). Its mulVecLin kernel has cardinality gcd(N, Nat.fib(g)), and its mulVec is injective exactly when that gcd is one. The proof clears the first row, applies the finite Bezout column automorphism, and transports the scalar kernel through the unit matrices.

The statement records the integral normal form and the modular kernel and injectivity consequences only; it makes no claim about a cokernel or free-part decomposition.

References

• Truth anchor: D5/S1/Recurrence/FiniteSamplingSmithDefect.finite_sampling_smith_defect
• Dependency: D5/S1/Recurrence/FibVajda
• Dependency: D5/S1/Recurrence/FiniteColumnGcdNormalization
• Dependency: D5/S1/Recurrence/LucasCompanion
• Dependency: D5/S1/Scale/Fibonacci