Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \clearpage\subsection{Sixth Lean Block Supplement}\label{app:sup6}
2 \noindent\textbf{Checkpoint scope.} This complete source body retains the status of its dated original supplement. Earlier pending or partial-coverage labels are historical; the final core records their resolution.\par\medskip
3 \subsubsection*{Scope and result}
4 This release completes Theorem 9.1 and Corollary 9.2 of the unchanged 28-page status-corrected manuscript. The preceding 28 proof modules and five supplements remain unchanged.
5 
6 \textbf{Twenty-two of 24 named manuscript-proved items now have formal coverage; two remain pending.} Three classical inputs and two conjectures are tracked separately. The cumulative corpus has \textbf{382 named theorem declarations and 84 explicit definitions across 31 modules}.
7 
8 \begin{center}
9 \begin{tabular}{@{}p{.42\textwidth}p{.24\textwidth}rr@{}}
10 \toprule
11 New module & Scope & Theorems & Defs.\\\midrule
12 \mcode{CompanionPackets} & General jump and recurrence & 17 & 2\\
13 \mcode{FibonacciPackets} & Actual Fibonacci specialization & 18 & 4\\
14 \mcode{RecurrenceExamples} & Examples and boundary cases & 14 & 1\\\midrule
15 Total added & Two named items & 49 & 7\\\bottomrule
16 \end{tabular}
17 \end{center}
18 These counts include supporting lemmas and examples, not 49 independent mathematical discoveries. The principal statements are universal over their explicit inputs, not finite numerical observations.
19 
20 \subsubsection*{The main mathematical connection}
21 A sampled state $u_k=v_{Nk+j}$ evolves by the actual jump matrix $C^N$. Its recurrence is derived from the characteristic polynomial of that matrix. No scalar recurrence or spectral decomposition is supplied as a substitute for the desired conclusion.
22 
23 For Fibonacci numbers, the state is independently defined from Mathlib's actual sequence. The Lucas sequence is independently defined by its initial values and recurrence. The trace and determinant of $C^N$ are then proved to supply the sampled recurrence coefficients.
24 
25 \subsubsection*{Important qualification}
26 A $d$-dimensional state system supplies a recurrence of \textbf{order at most $d$}. Its minimal recurrence need not have order $d$. The original statement is read as the characteristic-polynomial recurrence, not a minimal-order claim. The formal equations also handle singular matrices, zero-dimensional spaces and zero step.
27 
28 \par\medskip
29 \pageheading{1. Actual matrix orbits and arithmetic jumps}{Theorem 9.1; manuscript page 22}
30 Let $R$ be a commutative ring, $I$ a finite coordinate type and $d=|I|$. For $C\in M_I(R)$ and $v_0\in R^I$, define
31 \[
32  \operatorname{orbit}(C,v_0,n)=C^nv_0,
33  \qquad u_k=\operatorname{packet}(C,v_0,N,j,k)=C^{Nk+j}v_0.
34 \]
35 The implementation uses actual matrix powers and matrix--vector multiplication. A separately supplied sequence $v$ with
36 \[
37  v_{n+1}=Cv_n
38 \]
39 is proved by induction to equal this power orbit. Thus the source-sequence formulation is connected to the construction.
40 
41 \subsection*{The jump formula}
42 Associativity and the laws for powers of one matrix give
43 \[
44  \boxed{u_k=C^j(C^N)^kv_0=(C^N)^k(C^jv_0).}
45 \]
46 Only powers of the same matrix are interchanged. The argument does not assume that arbitrary matrices commute. In particular,
47 \[
48  u_{k+1}=C^Nu_k,\qquad u_{k+a}=(C^N)^a u_k.
49 \]
50 The step matrix is $C^N$, not $C$. A checked example with the Fibonacci matrix and $N=2$ rejects replacing the jump with a single original step.
51 
52 \subsection*{Refinement of an arithmetic address}
53 Taking another subsequence with step $M$ and offset $s$ yields
54 \[
55  u_{Mk+s}=v_{(NM)k+(Ns+j)}.
56 \]
57 The formal proof establishes this identity for the actual packet function by checking the index arithmetic. It is not inferred from a diagram or a naming convention.
58 
59 \subsection*{Endpoints and interpretation}
60 The algebraic identities allow $N=0$, in which case $u_k=v_j$ is constant. Positive-modulus residue packets are the special case $N>0$ and $0\le j<N$. The formula also permits offsets beyond that standard range. No inverse matrix, diagonalization, eigenvalue, or characteristic-zero assumption is needed.
61 
62 \textbf{Principal targets.}\par
63 \target{Companion.orbit_of_recurrence}\par
64 \target{Companion.companion_jump, Companion.source_companion_jump}\par
65 \target{Companion.packet_step, Companion.packet_advance}\par
66 \target{Companion.packet_refinement, Companion.packet_zero_step}
67 \par\medskip
68 \pageheading{2. From the characteristic polynomial to a recurrence}{Theorem 9.1, continued}
69 Put $D=C^N$ and let
70 \[
71  \chi_D(X)=\det(XI-D)=X^d+\sum_{a=0}^{d-1}c_aX^a
72 \]
73 be its actual characteristic polynomial. The implementation reuses the pinned Mathlib Cayley--Hamilton theorem, expands polynomial evaluation into a finite sum and proves
74 \[
75  \sum_{a=0}^{d}\chi_D[a]D^a=0,
76  \qquad \chi_D[d]=1.
77 \]
78 Here $\chi_D[a]$ denotes the coefficient at index $a$. The identities hold over any commutative coefficient ring; the zero-ring case is handled explicitly by the proof's subsingleton branch.
79 
80 \subsection*{The complete vector recurrence}
81 Apply the matrix identity to the actual state $u_k$. The already proved advance identity identifies each $D^a u_k$ with $u_{k+a}$. Consequently,
82 \[
83  \sum_{a=0}^{d}\chi_D[a]u_{k+a}=0,
84  \qquad
85  \boxed{u_{k+d}=-\sum_{a=0}^{d-1}c_a u_{k+a}.}
86 \]
87 This is the desired recurrence, with its monic leading coefficient and all earlier coefficients supplied by $\chi_D$. It is not an assumption on the packet sequence.
88 
89 Every coordinate and every $R$-linear scalar observation $\lambda:R^I\to R$ satisfies the corresponding equation:
90 \[
91  \lambda(u_{k+d})=-\sum_{a=0}^{d-1}c_a\lambda(u_{k+a}).
92 \]
93 A separate source-sequence theorem transports the recurrence back to the original $v_{Nk+j}$ notation.
94 
95 \subsection*{Order versus minimal order}
96 The characteristic polynomial gives a recurrence of order at most $d$. For example, $C=I_2$ gives a degree-two characteristic polynomial, but every orbit is constant and obeys $u_{k+1}=u_k$. Both statements are checked. No minimal-polynomial classification is claimed.
97 
98 For $d=0$, the unique empty vector is zero and the formula remains valid. For singular matrices, Cayley--Hamilton still applies: invertibility is irrelevant. The nilpotent example $C=\left(\begin{smallmatrix}0&1\\0&0\end{smallmatrix}\right)$ has $C^2=0$ and $\chi_C=X^2$.
99 
100 \textbf{Principal targets.}\par
101 \target{Companion.charpoly_sum_powers, Companion.charpoly_coeff_dimension}\par
102 \target{Companion.packet_charpoly_annihilation}\par
103 \target{Companion.packet_charpoly_recurrence}\par
104 \target{Companion.packet_coordinate_recurrence}\par
105 \target{Companion.packet_observable_recurrence}
106 \par\medskip
107 \pageheading{3. Fibonacci and Lucas coefficients are derived}{Corollary 9.2; manuscript page 22}
108 Define the actual integer matrix and state
109 \[
110  C=\begin{pmatrix}1&1\\1&0\end{pmatrix},
111  \qquad v_n=\begin{pmatrix}F_{n+1}\\F_n\end{pmatrix},
112  \qquad v_0=\begin{pmatrix}1\\0\end{pmatrix}.
113 \]
114 The values $F_n$ are Mathlib's \mcode{Nat.fib}, cast into $\Z$. Its basic recurrence proves $v_{n+1}=Cv_n$. The second coordinate of the packet state is therefore proved to be the intended $F_{Nk+j}$, not a newly assumed sequence.
115 
116 \subsection*{An independent Lucas sequence}
117 Define
118 \[
119  L_0=2,\quad L_1=1,\quad L_{n+2}=L_n+L_{n+1}.
120 \]
121 Direct finite matrix arithmetic proves $C^2=C+I$. Multiplication by $C^n$ gives $C^{n+2}=C^n+C^{n+1}$. Taking traces shows that $\operatorname{tr}(C^n)$ satisfies the same recurrence and initial values as $L_n$. Induction yields
122 \[
123  \boxed{\operatorname{tr}(C^N)=L_N.}
124 \]
125 The implementation separately proves
126 \[
127  \det C=-1,\qquad \det(C^N)=(-1)^N,
128  \qquad L_N=2F_{N+1}-F_N.
129 \]
130 No Binet roots or diagonalizability argument is needed.
131 
132 \subsection*{The sampled Fibonacci recurrence}
133 The actual two-by-two characteristic-polynomial formula gives
134 \[
135  \chi_{C^N}(X)=X^2-L_NX+(-1)^N.
136 \]
137 Insert these coefficients into the general packet recurrence and take the second coordinate:
138 \[
139  \boxed{F_{N(k+2)+j}=L_NF_{N(k+1)+j}-(-1)^NF_{Nk+j}.}
140 \]
141 The full two-coordinate state satisfies the same equation. All subtraction is in $\Z$, not truncated natural-number subtraction. The result holds for all natural $N,j,k$, including zero step and zero initial values.
142 
143 \textbf{Principal targets.}\par
144 \target{FibonacciPackets.state_is_orbit, FibonacciPackets.packet_is_fibonacci}\par
145 \target{FibonacciPackets.trace_power_is_lucas, FibonacciPackets.det_power}\par
146 \target{FibonacciPackets.jump_charpoly}\par
147 \target{FibonacciPackets.fibonacci_packet_recurrence}
148 \par\medskip
149 \pageheading{4. Exact examples and meaningful boundary checks}{Example 9.3 and supporting results}
150 The independently defined Lucas recurrence gives
151 \[
152  (L_0,L_1,L_2,L_3,L_4,L_5)=(2,1,3,4,7,11).
153 \]
154 For $N=3$, the general theorem therefore specializes to
155 \[
156  u_{k+2}=4u_{k+1}+u_k.
157 \]
158 The implementation proves this for every offset $j$ and every $k$, not only the displayed sample. At $j=2$, direct evaluation of the actual Fibonacci sequence gives
159 \[
160  (F_2,F_5,F_8,F_{11},F_{14},F_{17})=(1,5,21,89,377,1597).
161 \]
162 This is the exact manuscript example.
163 
164 \subsection*{The parity sign cannot be removed}
165 For $N=2$, the recurrence is
166 \[
167  u_{k+2}=3u_{k+1}-u_k.
168 \]
169 At $j=1,k=0$, the correct equation is $5=3\cdot2-1$. Replacing the minus sign with a plus would assert $5=7$. The source proves the inequality, and a separate invalid-proof control attempts and rejects the false equation.
170 
171 At $N=1$ the ordinary Fibonacci recurrence is recovered. At $N=0$, $L_0=2$ and the packet is constant, so the same formula becomes $u=2u-u$.
172 
173 \subsection*{Uniqueness from the first two packet values}
174 For a fixed $N,j$, any integer sequence satisfying the proved sampled recurrence and starting at $F_j,F_{N+j}$ agrees with $F_{Nk+j}$ for all $k$. This is proved by two-step induction. It is a consequence of the established coefficients and recurrence, not a premise used to identify Fibonacci values initially.
175 
176 \subsection*{Independent finite mirrors}
177 A pure-Python exact-arithmetic implementation computes characteristic polynomials by the permutation determinant and states by repeated matrix application. It checks 280 matrix systems over integers, rationals and several modular rings, including composite moduli and the zero ring. Separately it computes sampled Fibonacci sequences recursively and compares them with direct Fibonacci evaluation. These are useful regression checks, not Lean extraction or universal proofs.
178 
179 \textbf{Principal targets.}\par
180 \target{RecurrenceExamples.manuscript_sequence}\par
181 \target{RecurrenceExamples.manuscript_step_three, RecurrenceExamples.step_two}\par
182 \target{FibonacciPackets.fibonacci_packet_unique}\par
183 \target{RecurrenceExamples.even_step_wrong_sign}\par
184 \target{RecurrenceExamples.wrong_jump_matrix}
185 \par\medskip
186 \pageheading{5. Verification, provenance and remaining work}{Cumulative checks and exact scope}
187 \textbf{Lean.} The fresh cumulative run uses Lean 4.34.0-rc2 and Mathlib revision
188 \begin{center}\small\mcode{aeb72f1e9981b6d35b426b16dca7759be3e7ba06}.\end{center}
189 All 31 modules compile with warnings treated as errors. The inventory contains 382 theorem declarations and 84 explicit definitions; all 466 expected axiom reports must match. Allowed dependencies are \mcode{propext}, \mcode{Classical.choice} and \mcode{Quot.sound}, or subsets. The source-policy check excludes admitted proofs, added axioms and selected trust bypasses. All nine package revision pins are checked.
190 
191 \textbf{Controls and tests.} Twenty invalid-proof controls are expected to fail for mathematical reasons, not missing imports or timeouts. The three new controls test the Fibonacci sign, the jump matrix and the trace coefficient. All 131 infrastructure and release tests pass. These include 28 new sixth-block tests and preserved earlier arithmetic tests.
192 
193 \begin{center}
194 \begin{tabular}{@{}lr@{}}
195 \toprule
196 Independent exact finite check & Cases\\\midrule
197 Matrix systems across seven coefficient domains & 280\\
198 Jump identities and characteristic recurrences & 1,680 each\\
199 One-step packet transitions & 1,400\\
200 Nested packet addresses & 280\\
201 Fibonacci packet sequences & 357\\
202 Fibonacci scalar recurrence steps & 11,067\\
203 Lucas trace, determinant and Fibonacci identities & 81\\
204 Invalid numerical inputs rejected & 10\\\bottomrule
205 \end{tabular}
206 \end{center}
207 \textbf{Development failures.} Four Lean development checks failed before correction. The errors concerned a matrix-associativity step, recursive simplification, coefficient simplification and an ineffective coordinate for a counterexample. Their source snapshots and compiler logs are retained. An initial unit-test run failed two stale baseline-count assertions; those expected counts were updated, not the mathematical tests weakened.
208 
209 \textbf{Trust boundary.} Pinned Mathlib supplies Cayley--Hamilton, characteristic-polynomial facts, matrix algebra and the basic Fibonacci recurrence. Its compiled cache is reused, not independently rebuilt. Python mirrors do not execute extracted Lean definitions. The historical numerical suite and earlier papers are not rerun. The original manuscript and all 28 upstream proof files remain unchanged.
210 
211 \textbf{Remaining pair.} Theorem 7.5, the global odd-prime Euler finite-difference estimate, and Corollary 8.5, the uniform standard-window period, remain pending. The two conjectures are still unproved. This block does not use those claims as assumptions.
212 
213 Detailed compiler logs, inventories, amendments, the completed item crosswalk, and fresh-extraction integrity evidence accompany the release. Manuscript-to-Lean correspondence is a mathematical review, not an automatically certified semantic equivalence.

Back to source controls

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation