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

1 \section{The object: rows, degrees, and normalization}
2 
3 The visual guide accompanies \emph{Euler Congruences: Completion, Factorial Strengthening,
4 and Sharp Dyadic Geometry}. It makes the indexing,
5 precision gains, and boundaries of the results visible. The main paper contains
6 the proofs. The separate Lean guide records which statements are already
7 formalized and which belong to the new mathematical extension.
8 
9 \begin{figure}[ht]
10 \centering
11 \includegraphics[width=.96\linewidth]{../figures/normalization.pdf}
12 \caption{The actual reciprocal series is the source of every coefficient in
13 this guide. The factorial normalization changes valuations as well as the
14 constant term.}
15 \end{figure}
16 
17 There are two coefficient conventions, and they must stay distinct:
18 \[
19  C_{N,j}(0)=1,
20  \qquad E_0^{(N,j)}=j!,
21  \qquad
22  v_2(E_{Nn}^{(N,j)})=v_2(C_{N,j}(n))+v_2(j!).
23 \]
24 The last equality uses $v_2(0)=+\infty$. Congruences of dyadic rational numbers
25 mean membership in the corresponding ideal of $\mathbb Z_2$; a displayed
26 rational denominator is invertible modulo $2^r$ when it is odd.
27 
28 \begin{center}
29 \begin{tabular}{lll}
30 \toprule
31 Symbol & Meaning & At rank four \\
32 \midrule
33 $n$ & packed row index & Euler degree $4n$ \\
34 $H$ & positive row step & Euler degree step $4H$ \\
35 $k$ & number of differences & order $k$, independent of $n$ \\
36 $j$ & address within a section & $0,1,2,3$ \\
37 \bottomrule
38 \end{tabular}
39 \end{center}
40 
41 For example, $C_{4,1}(1)=-1/5$ and $C_{4,1}(2)=121/45$.
42 Their difference is $26/9$, of valuation one. The row difference joins Euler
43 degrees $4$ and $8$.
44 
45 \clearpage
46 \section{What the original conjecture asked}
47 
48 Nishibuchi's Conjecture 3.9 concerns a prime $p$, a positive integer $m$ with
49 $m\mid p-1$ or $m=2$, and every address $0\le j<mp$. Put
50 \[
51  N=mp, \qquad q=\operatorname{lcm}(2,p-1).
52 \]
53 It asserts $p$-adic integrality of the actual generalized Euler coefficients and
54 eventual periodicity at every precision:
55 \[
56  \text{for every }r\ge1,\quad
57  E_{mpn+qp^r}^{(mp,j)}\equiv E_{mpn}^{(mp,j)}\pmod {p^r}
58  \quad\text{for all sufficiently large }n.
59 \]
60 The completed theorem gives the explicit sufficient threshold $n\ge r$ in
61 every permitted branch. Its formal capstone is the theorem named
62 \texttt{NishibuchiCompletion.conjecture\_3\_9}. No conjectural flatness premise
63 is supplied to that theorem.
64 
65 \begin{center}
66 \begin{tabular}{llll}
67 \toprule
68 Prime branch & Allowed $m$ & $q$ & Row step for the original shift \\
69 \midrule
70 $p=2$ & $1$ & $2$ & $2^r$ \\
71 $p=2$ & $2$ & $2$ & $2^{r-1}$ \\
72 $p$ odd & $m\mid p-1$ & $p-1$ & $\dfrac{p-1}{m}p^{r-1}$ \\
73 \bottomrule
74 \end{tabular}
75 \end{center}
76 
77 For odd primes, $m=2$ is already in the divisor branch. The conversion is exact:
78 \[
79  N\left(\frac qm p^{r-1}\right)=qp^r.
80 \]
81 At $p=2,m=2$, the original conjectured Euler-degree shift $2^{r+1}$ is the row
82 step $2^{r-1}$ for the rank-four sequence.
83 
84 The source already contains special cases. In particular, Nishibuchi's
85 Proposition 3.10 treats the rank-four address-zero dyadic period from row zero
86 and an eventual cubic case. The completion covers the full quantified
87 conjecture; the new dyadic work then removes starting-row restrictions from
88 higher differences and determines substantially more precise laws.
89 
90 The conjecture's primary source is Yuta Nishibuchi, \emph{$p$-adic Congruences of
91 Generalized Euler Numbers and Relations to Even Zeta Values},
92 arXiv:2605.10677v2, revised 1 June 2026. The statement above uses that version's
93 normalization and actual Euler degrees.
94 
95 \clearpage
96 \section{Removing the starting-row threshold}
97 
98 At rank four the earlier completed estimate was
99 $v_2(\Delta_H^k C_j(n))\ge\min(k,n)$. The strengthened theorem reaches every
100 starting row, including $n=0$, and every order, including $k>n$.
101 
102 \begin{figure}[ht]
103 \centering
104 \includegraphics[width=\linewidth]{../figures/threshold.pdf}
105 \caption{Unit-step lower bounds on a finite display window. Each colored cell
106 is obtained from a proved formula, rather than from sampled coefficients.
107 The dashed line indicates $k=n$.}
108 \end{figure}
109 
110 For \emph{every} dyadic section size $N=2^a$, $a\ge0$, every permitted address,
111 and all positive steps,
112 \[
113  v_2\!\left(\Delta_{H_1}\cdots\Delta_{H_k}C_{N,j}(n)\right)
114  \ge k+\sum_{\nu=1}^k v_2(H_\nu),
115  \qquad n\ge0.
116 \]
117 The corresponding statement for $E_{Nn}^{(N,j)}$ adds $v_2(j!)$.
118 
119 The proof acts on the full factorial-scaled power series before it extracts a
120 packed row. This avoids the old extraction constraint $k\le n$. Reciprocal
121 induction controls the unique term with the highest inverse order in the
122 commuting product expansion; all other terms are covered by the preceding
123 induction stages.
124 
125 The figure displays the gain at unit step. An even step contributes additional
126 precision, and the theorem permits different steps in the same difference.
127 
128 \clearpage
129 \section{Each step contributes its own precision}
130 
131 Write $Sf(n)=f(n+1)$ and $\Delta_H=S^H-1$. Mixed differences commute. Their
132 exact finite expression is
133 \[
134  \Delta_{H_1}\cdots\Delta_{H_k}f(n)
135  =\sum_{A\subseteq\{1,\ldots,k\}}
136  (-1)^{k-|A|}
137  f\!\left(n+\sum_{i\in A}H_i\right).
138 \]
139 Repeated subset offsets are combined with their signed multiplicities.
140 
141 \begin{figure}[ht]
142 \centering
143 \includegraphics[width=\linewidth]{../figures/mixed_stencil.pdf}
144 \caption{For steps $(1,2,4)$ all eight offsets are distinct. This is an exact
145 signed stencil, rather than an approximate derivative.}
146 \end{figure}
147 
148 For this stencil, the general dyadic bound is
149 \[
150  3+v_2(1)+v_2(2)+v_2(4)=6.
151 \]
152 At rank four the factorial theorem improves it to seven for addresses zero
153 and one. Exact rational evaluation gives
154 $v_2(\Delta_1\Delta_2\Delta_4 C_0(0))=7$.
155 The order is odd, so the mixed-step equality criterion also proves this
156 valuation at \emph{every} starting row.
157 
158 There is a prime-power extension. For $N=p^a$, $a\ge1$, the sign-corrected
159 operator is
160 \[
161  T_H=S^H-(-1)^H,
162  \qquad
163  v_p\!\left(T_{H_1}\cdots T_{H_k}E^{(N,j)}(n)\right)
164  \ge v_p(j!)+\sum_{i=1}^k\bigl(1+v_p(H_i)\bigr).
165 \]
166 Here $E^{(N,j)}(n)=E_{Nn}^{(N,j)}$. For an odd prime, an ordinary first
167 difference need not have positive valuation: at address zero its first two
168 normalized values are $1$ and $-1$, with difference $-2$. The sign correction
169 is therefore essential to this prime-power theorem.
170 
171 \clearpage
172 \section{The final rank-four congruence}
173 
174 For $n\ge0$, $k\ge1$, and $H\ge1$, the actual Euler coefficients satisfy
175 \[
176  \sum_{i=0}^k(-1)^{k-i}\binom ki
177  E_{4(n+iH)}^{(4,j)}
178  \equiv0\pmod {2^{\,v_2(k!)+k v_2(H)+A_j(k)}},
179 \]
180 where
181 \[
182 \begin{aligned}
183  A_0(k)=A_1(k)&=k,\\
184  A_2(k)&=\max\{k+4,\ 2k+\lfloor k/2\rfloor+1\},\\
185  A_3(k)&=k+2.
186 \end{aligned}
187 \]
188 
189 \begin{figure}[ht]
190 \centering
191 \includegraphics[width=\linewidth]{../figures/final_exponents.pdf}
192 \caption{The exponent of the final Euler congruence at unit step. The address
193 zero and one curve is exact at every order. Marked address-two orders are
194 universally exact; the other displayed address-two and address-three values
195 are proved lower bounds.}
196 \end{figure}
197 
198 At a common step with $v_2(H)=s$, add $ks$ to every displayed exponent. Thus a
199 doubling of the step gains one additional bit \emph{per difference}, rather
200 than one bit for the whole expression.
201 
202 This statement combines two different proved bounds at address two. A lower
203 bound is not automatically an exact valuation: divisibility may be stronger
204 at unmarked orders or at particular starting rows.
205 
206 \clearpage
207 \section{Why address two has a different slope}
208 
209 The normalized address-two sequence obeys both
210 \[
211 \begin{aligned}
212  v_2(\Delta_{H_1}\cdots\Delta_{H_k}C_2(n))
213  &\ge k+v_2(k!)+3+\sum_i v_2(H_i),\\
214  v_2(\Delta_{H_1}\cdots\Delta_{H_k}C_2(n))
215  &\ge2k+v_2(k!)+\lfloor k/2\rfloor+\sum_i v_2(H_i).
216 \end{aligned}
217 \]
218 Their maximum supplies the useful envelope.
219 
220 \begin{figure}[ht]
221 \centering
222 \includegraphics[width=\linewidth]{../figures/address_two_envelope.pdf}
223 \caption{Normalized address-two precision. The paired filtration controls the
224 large-order slope. At order one the constant-surplus bound is stronger.}
225 \end{figure}
226 
227 For every base row and every positive step list, equality is proved when
228 $k$ is a power of two:
229 \[
230  v_2(\Delta_{H_1}\cdots\Delta_{H_k}C_2(n))
231  =V_2(k)+\sum_i v_2(H_i),
232 \]
233 with $V_2(1)=4$, $V_2(2)=6$, and
234 $V_2(k)=2k+v_2(k!)+k/2$ for $k=2^r\ge4$.
235 The infinite marked family establishes sharpness at unbounded orders.
236 
237 For original Euler coefficients add one, since $v_2(2!)=1$.
238 The extra $\lfloor k/2\rfloor$ comes from a paired divided-power filtration in
239 the Bernoulli transformation. It does not arise by fitting the plotted points.
240 
241 \clearpage
242 \section{When mixed steps attain the baseline}
243 
244 For addresses $j=0,1$, put
245 \[
246  V=k+v_2(k!)+\sum_i v_2(H_i),
247  \qquad q=\#\{i:H_i\text{ is even}\}.
248 \]
249 The valuation equals $V$ exactly when $k$ is odd or $q$ is even.
250 
251 \begin{center}
252 \begin{tabular}{lll}
253 \toprule
254 Order parity & Number of even steps & Conclusion \\
255 \midrule
256 $k$ odd & either parity & exact valuation $V$ \\
257 $k$ even & $q$ even & exact valuation $V$ \\
258 $k$ even & $q$ odd & valuation at least $V+1$ \\
259 \bottomrule
260 \end{tabular}
261 \end{center}
262 
263 \begin{figure}[ht]
264 \centering
265 \includegraphics[width=\linewidth]{../figures/mixed_cancellation.pdf}
266 \caption{Exact rational examples at order two and base zero. Strict cases
267 show why the factorial baseline cannot always be called an equality for
268 mixed steps. The universal parity criterion is proved separately.}
269 \end{figure}
270 
271 For instance,
272 \[
273  \Delta_1\Delta_2 C_0(0)=-33728,
274  \qquad v_2(-33728)=6,
275  \qquad V=4.
276 \]
277 Cancellation removes the leading term, and here it removes two bits beyond
278 the baseline. The parity theorem proves strictness in this case; it does not
279 give a complete formula for the further depth.
280 
281 With a common step, $q$ is either zero or $k$. Consequently the exceptional
282 parity never occurs, and the homogeneous address-zero/one formula is always
283 exact.
284 
285 \clearpage
286 \section{First differences determine an exact metric}
287 
288 All four rank-four sequences satisfy the sharp first-difference law
289 \[
290  v_2(C_j(n+H)-C_j(n))=v_2(H)+b_j,
291  \qquad b=(1,1,4,2).
292 \]
293 For the actual Euler coefficients this becomes
294 \[
295  v_2(E_{4(n+H)}^{(4,j)}-E_{4n}^{(4,j)})=v_2(H)+B_j,
296  \qquad B=(1,1,5,3).
297 \]
298 Both laws hold at every starting row and every positive integer step.
299 
300 \begin{figure}[ht]
301 \centering
302 \includegraphics[width=\linewidth]{../figures/metric.pdf}
303 \caption{The proved Euler metric laws, with exact modular sample points at
304 base zero and steps $H=2^s$. Addresses zero and one have the same scale;
305 their circle and square marks overlap.}
306 \end{figure}
307 
308 In dyadic distance, $|x|_2=2^{-v_2(x)}$. After continuous interpolation to
309 $\mathbb Z_2$, the law reads
310 \[
311  |E^{(4,j)}(x)-E^{(4,j)}(y)|_2
312  =2^{-B_j}|x-y|_2.
313 \]
314 It says exactly how much the map shrinks distances. It also prevents any
315 hidden collision at finer precision: distinct inputs remain distinct after
316 the known scale is removed.
317 
318 The scale of address two is $2^{-5}$ in the original normalization and
319 $2^{-4}$ in the normalized sequence. Omitting its factor $2!$ would change
320 the period claimed for the original coefficients.
321 
322 \clearpage
323 \section{Least periods, rather than sufficient periods}
324 
325 At precision $2^r$ the least positive \emph{row} period is
326 \[
327  P_j(r)=2^{\max(0,r-B_j)},\qquad B=(1,1,5,3).
328 \]
329 The exact valuation law proves both periodicity and minimality. A step $H$
330 is a period precisely when $v_2(H)+B_j\ge r$.
331 
332 \begin{figure}[ht]
333 \centering
334 \includegraphics[width=\linewidth]{../figures/periods.pdf}
335 \caption{Binary logarithms of the least row periods. A height of zero means
336 period one. These are theorem-derived values, valid at every precision.}
337 \end{figure}
338 
339 Modulo $256=2^8$, the least periods are
340 \[
341  (P_0(8),P_1(8),P_2(8),P_3(8))=(128,128,8,32).
342 \]
343 In actual Euler degree, multiply by four:
344 \[
345  (512,512,32,128).
346 \]
347 For address two, precision at most $2^5$ already has row period one. Its
348 Euler coefficients all lie in $2+32\mathbb Z_2$; further precision resolves
349 additional dyadic digits within that residue class.
350 
351 The original rank-four conjectural shift has row step $2^{r-1}$. It remains
352 a valid period for every address, but addresses two and three usually admit
353 shorter periods. The sharp theorem identifies the shortest one.
354 
355 \clearpage
356 \section{A full period visits every allowed residue}
357 
358 For each address the exact interpolation image is
359 \[
360  E^{(4,j)}(\mathbb Z_2)=j!+2^{B_j}\mathbb Z_2.
361 \]
362 When $r>B_j$, a least period lists every residue in this coset modulo $2^r$
363 exactly once. The following figure checks this assertion by exact arithmetic
364 at precision $256$.
365 
366 \begin{figure}[ht]
367 \centering
368 \includegraphics[width=\linewidth]{../figures/residue_permutations.pdf}
369 \caption{Exact residue permutations modulo $256$. The vertical coordinate is
370 $y_n=(E_{4n}^{(4,j)}-j!)/2^{B_j}$ modulo $P_j(8)$.
371 Each panel contains one full least period; every vertical residue occurs once.}
372 \end{figure}
373 
374 No decimal approximation is used to form these residues. The generating
375 series is inverted modulo $2^{256}$ using odd denominators, then the exact
376 result is reduced modulo $256$. An independent rational inversion checks the
377 initial coefficients.
378 
379 The shapes are permutations, not monotone real functions. Their organizing
380 property is dyadic distance: agreement in input low bits forces the same
381 agreement in the scaled output low bits.
382 
383 \clearpage
384 \section{Seeing the scaled isometry}
385 
386 The map
387 \[
388  x\longmapsto \frac{E^{(4,j)}(x)-j!}{2^{B_j}}
389 \]
390 is a bijective isometry of $\mathbb Z_2$. Its finite reductions preserve the
391 number of common low binary digits.
392 
393 \begin{figure}[ht]
394 \centering
395 \includegraphics[width=\linewidth]{../figures/isometry_matrices.pdf}
396 \caption{Address two modulo $256$ gives an eight-element quotient. The
397 two exact matrices coincide: every pair of distinct rows has the same dyadic
398 valuation before and after the scale is removed. The diagonal represents
399 $v_2(0)=+\infty$ and is left blank.}
400 \end{figure}
401 
402 If $n-m$ is odd, the rows disagree in their first binary digit and the matrix
403 entry is zero. If it is divisible by two but not four, they share exactly one
404 low digit. An entry two means agreement through two low digits.
405 
406 This structure explains the residue permutation in the preceding section.
407 At each new precision, every input residue has exactly two lifts. An
408 isometry distinguishes those lifts at the corresponding output precision.
409 Starting from the single residue at the scale threshold, induction gives
410 surjectivity and a unique inverse residue at every finite level.
411 
412 The finite matrix is an illustration of that proof. Its eight rows alone
413 would not establish a statement about the whole of $\mathbb Z_2$.
414 
415 \clearpage
416 \section{How far the simple metric law extends}
417 
418 Sharp first-difference laws hold for every address at ranks $2$, $4$, and $8$.
419 The arrays below give their normalized scales $b_{N,j}$ and original Euler
420 scales $B_{N,j}=b_{N,j}+v_2(j!)$.
421 
422 \begin{figure}[ht]
423 \centering
424 \includegraphics[width=\linewidth]{../figures/rank_scales.pdf}
425 \caption{Proved scale arrays for the three small ranks. Blank cells are
426 outside the address range. The Euler normalization contributes the factorial
427 valuation, which is already substantial at the larger addresses of rank eight.}
428 \end{figure}
429 
430 There is also an infinite family: at every $N=2^a\ge4$, all lower-half
431 addresses $j<N/2$ have normalized scale one. Their Euler scale is
432 $1+v_2(j!)$.
433 
434 The same constant-scale proposal fails at some upper-half addresses:
435 \begin{center}
436 \begin{tabular}{rrrr}
437 \toprule
438 $(N,j)$ & $v_2(C(1)-C(0))$ & Step-two prediction & Actual step-two valuation \\
439 \midrule
440 $(16,9)$ & $5$ & $6$ & $7$ \\
441 $(32,18)$ & $6$ & $7$ & $6$ \\
442 $(32,19)$ & $5$ & $6$ & $7$ \\
443 \bottomrule
444 \end{tabular}
445 \end{center}
446 
447 These are exact rational counterexamples to the additional metric proposal.
448 They do not contradict the universal higher-difference \emph{lower} bound,
449 which continues to hold at every address of every dyadic rank.
450 
451 \clearpage
452 \section{From factorial gain to analytic radius}
453 
454 At every center $x_0\in\mathbb Z_2$, the interpolations admit ordinary Taylor
455 series $C_j(x_0+z)=\sum_{d\ge0}a_{j,d}(x_0)z^d$. For positive degrees,
456 \[
457 \begin{aligned}
458  v_2(a_{j,d}(x_0))&=d &&(j=0,1),\\
459  v_2(a_{2,d}(x_0))&\ge\max\{2d+\lfloor d/2\rfloor,\ d+3\},\\
460  v_2(a_{3,d}(x_0))&\ge d.
461 \end{aligned}
462 \]
463 At address two equality with $5d/2$ holds along every power-of-two degree
464 $d\ge4$.
465 
466 \begin{figure}[ht]
467 \centering
468 \includegraphics[width=\linewidth]{../figures/analytic_slopes.pdf}
469 \caption{The Taylor coefficient precision slopes. The degree-zero
470 coefficient is excluded. Marked address-two degrees belong to an unbounded
471 proved equality family, rather than a finite observed pattern.}
472 \end{figure}
473 
474 The radius is $2^{\liminf_d v_2(a_d)/d}$ in the normalized dyadic absolute
475 value. Hence
476 \[
477  R_0=R_1=2,\qquad R_2=2^{5/2},\qquad R_3\ge2.
478 \]
479 The exact radius of address three is not asserted. For address two, the
480 lower bound gives convergence inside the claimed radius and the unbounded
481 equality family prevents a larger one.
482 
483 The proof converts the factorial Newton estimates into ordinary Taylor
484 coefficients with the Stirling relations. Generic continuity or first-order
485 Lipschitz bounds alone do not supply this analytic conclusion.
486 
487 \clearpage
488 \section{Which evidence does which job}
489 
490 The package has three complementary levels of evidence. They answer
491 different questions, and the final claims retain those distinctions.
492 
493 \begin{center}
494 \begin{tabular}{p{.23\linewidth}p{.34\linewidth}p{.34\linewidth}}
495 \toprule
496 Evidence & What it establishes & Scope of the final release \\
497 \midrule
498 Lean theorem & The precise formal statement follows from its recorded
499 dependencies and the accepted foundational axioms. & The completed Nishibuchi
500 conjecture, earlier Paper IX theory, and the inherited rank-four ordinary-step,
501 sharp-period, and isometry results; see the Lean guide for build provenance. \\
502 \addlinespace
503 Algebraic proof and audit & A universal mathematical result, subject to the
504 written proof and its stated inputs. & The new general prime-power transfer,
505 mixed-step and factorial gains, exact higher-order families, broader dyadic
506 metric laws, and radius results. \\
507 \addlinespace
508 Exact computation & The implemented assertion holds in its recorded finite
509 domain, or an exact counterexample refutes an extension. & Coefficient
510 regressions, period illustrations, and sharpness or cancellation checks. \\
511 \bottomrule
512 \end{tabular}
513 \end{center}
514 
515 The generic theorem uses the integral Hurwitz-series product and reciprocal
516 induction. The factorial theorem uses divided powers and explicit transforms
517 of the ordinary Euler and Bernoulli series. The ordinary Euler arithmetic
518 input is the classical Frobenius congruence, with normalization checked against
519 Gessel's primary exposition. Address two has a self-contained central-factorial
520 Bernoulli argument; addresses one and three use the proved tangent and
521 cotangent transfers.
522 
523 The broad exact regression through row $512$ contains more than $1.8$ million
524 bounded difference assertions. Smaller later runs test the strengthened
525 address-two filtration and the exact mixed parity law. Their manifests pin
526 precision, coefficient definitions, input versions, and executed ranges.
527 
528 The figures in this guide have a separate reproducibility record:
529 \texttt{sources/generate\_figures.py},
530 \texttt{figures/exact\_figure\_data.json}, and
531 \texttt{figures/figure\_manifest.json}. Its exact assertions validate the
532 illustration data; theorem-derived curves are explicitly recorded as such.
533 
534 The new general transfer, mixed-step, factorial, and analytic extension has
535 not been newly formalized in Lean. The rank-four ordinary-step and sharp-period
536 results have inherited Lean coverage, as mapped in the companion. Mathematical audits
537 in this package are internal reviews, not claims of external peer review.
538 
539 \clearpage
540 \section{Reading the conclusion at the right strength}
541 
542 The original quantified Nishibuchi conjecture is completed. The stronger
543 dyadic result applies without a starting-row threshold, and the rank-four
544 theory now has factorial precision, exact common-step laws for addresses zero
545 and one, an infinite exact address-two family, optimal periods, and exact
546 analytic radii for three addresses.
547 
548 For a common step, the final congruence to use is
549 \[
550  \Delta_H^k E^{(4,j)}(n)
551  \equiv0\pmod {2^{v_2(k!)+k v_2(H)+A_j(k)}},
552  \quad n\ge0,\ k,H\ge1,
553 \]
554 with
555 \[
556  (A_0,A_1,A_2,A_3)
557  =\bigl(k,k,\max\{k+4,2k+\lfloor k/2\rfloor+1\},k+2\bigr).
558 \]
559 For different steps, replace $k v_2(H)$ by $\sum_i v_2(H_i)$ in the lower
560 bound. The address-zero/one equality rule then depends on order parity and the
561 number of even steps.
562 
563 \begin{center}
564 \begin{tabular}{p{.55\linewidth}p{.35\linewidth}}
565 \toprule
566 Statement & Final status \\
567 \midrule
568 Nishibuchi Conjecture 3.9, all allowed branches & completed; formal capstone \\
569 All-row dyadic mixed-difference bound & proved and audited \\
570 Rank-four factorial and paired bounds & proved and audited \\
571 All common-step exact valuations, $j=0,1$ & proved at all rows and orders \\
572 Address-two exact valuations at power-of-two orders & proved for all positive step lists \\
573 Complete exact address-two formula at other orders & open \\
574 Complete exact higher-order address-three formula & open \\
575 Exact address-three analytic radius & open \\
576 Simple constant metric at every upper-half address & false; exact witnesses retained \\
577 Separate Euler-tail universal simplicity problem & open; a distinct research program \\
578 \bottomrule
579 \end{tabular}
580 \end{center}
581 
582 The remaining questions do not weaken the completed conjecture. They specify
583 the next boundary of the stronger theory. The main paper gives the proofs and
584 precise dependency statements, while the Lean guide supplies the formal
585 coverage map and a reproducible route to its recorded checks.

Back to source controls

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