Realization Calculus

Download original file

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

Read the typeset paper

1 \section{Exact classical Euler tails and the remaining simplicity problem}
2 \label{app:root:scope}
3 
4 This appendix records the related classical Euler tail program at its
5 stationary-separation checkpoint of 5 October 2026. Its purpose is to state
6 the strongest proved reduction and its exact remaining obligation. The
7 universal simplicity problem below is a separate question from
8 Nishibuchi's Conjecture~3.9, which the congruence results of this chapter
9 resolve. It is also separate from the presentation and gluing questions
10 called Native~13.2 and Native~13.3 in the original Paper~IX.
11 
12 The tail results have mathematical proofs, supplemented in the indicated
13 families by complete coefficient certificates and proved bounds for every
14 omitted coefficient. Bounded sampled values support implementation checks.
15 They do not supply the universal quantifiers. The latest continuation did
16 not run Lean. Its mathematical claims must therefore be read with the
17 formal-coverage distinctions in the Lean guide.
18 
19 \subsection{The ordinary Euler packet identity}
20 \label{app:root:identity}
21 
22 To distinguish ordinary signed Euler numbers from the generalized numbers
23 of the main text, write
24 \[
25  \operatorname{sech}t=\sum_{n\ge0}\mathcal E_n\frac{t^n}{n!},
26  \qquad \frac{t}{e^t-1}=\sum_{n\ge0}B_n\frac{t^n}{n!},
27  \qquad B_1=-\frac12.
28 \]
29 Throughout this appendix, $v_2(2)=1$ and $v_2(0)=\infty$.
30 Let $s_2(n)$ be the number of ones in the binary expansion of the
31 nonnegative integer $n$. Define
32 \[
33  A(N)=\frac{3^{2N+2}-1}{4(2N+1)(2N+2)},\qquad
34  \left(\frac z{\sinh z}\right)^2=\sum_{m\ge0}\beta_m z^{2m},
35  \qquad \kappa_m=2^{2m}(2m)!\beta_m.
36 \]
37 The initial values are $\beta_0=\kappa_0=1$. For $m\ge1$, differentiation
38 of $z\coth z$ gives
39 \begin{equation}
40  \beta_m=-\frac{2^{2m}(2m-1)B_{2m}}{(2m)!},\qquad
41  \kappa_m=-2^{4m}(2m-1)B_{2m}.
42  \label{eq:root:beta}
43 \end{equation}
44 The classical dyadic Bernoulli denominator law
45 $v_2(B_{2m})=-1$ and Legendre's formula yield
46 \begin{equation}
47  v_2(\beta_m)=s_2(m)-1,\qquad
48  v_2(\kappa_m)=4m-1.\label{eq:root:weights}
49 \end{equation}
50 The source identity
51 \[
52  \sum_{N\ge0}A(N)\frac{t^{2N}}{(2N)!}
53  =\frac{\sinh(2t)\sinh t}{2t^2}
54 \]
55 implies, after multiplication by $4t^2/\sinh^2(2t)$,
56 \begin{equation}
57  \mathcal E_{2N}=\sum_{m=0}^N
58     \kappa_m\binom{2N}{2m}A(N-m).
59  \label{eq:root:packet}
60 \end{equation}
61 For a retained depth $M\ge0$, put
62 \[
63  \mathcal T_M(N)=\mathcal E_{2N}
64    -\sum_{m=0}^{\min(M,N)}\kappa_m\binom{2N}{2m}A(N-m).
65 \]
66 An empty tail, $N\le M$, is exactly zero.
67 
68 \begin{proposition}[Sharp uniform classical truncation bound]
69 For every $M,N\ge0$,
70 \[
71  v_2\bigl(\mathcal T_M(N)\bigr)\ge4M+3.
72 \]
73 For each fixed $M$, equality holds at $N=M+1$.
74 \end{proposition}
75 \begin{proof}
76 The source $A(n)$ is a dyadic unit for every nonnegative integer $n$.
77 Each nonempty summand has $m\ge M+1$, so
78 \eqref{eq:root:weights} and integrality of the binomial coefficient give
79 the asserted bound. At $N=M+1$, only the first omitted summand remains.
80 Its binomial coefficient and $A(0)$ both equal one.
81 \end{proof}
82 
83 Thus later row-dependent cancellation can improve a particular tail,
84 but cannot increase the uniform exponent required to hold at every row.
85 
86 \subsection{A finite carry minimum and an exact all-row factorization}
87 \label{app:root:factorization}
88 
89 Let $\mathbb Z_2\langle x\rangle$ denote the restricted power series:
90 their integral coefficients tend to zero dyadically. Extend $A$ by
91 \[
92  \mathscr A(x)=\frac{9^{x+1}-1}{8(x+1)(2x+1)},
93  \qquad \mathscr A(-1)=-\frac{\log9}{8}.
94 \]
95 The apparent singularity at $x=-1$ is removable. Since
96 $v_2(\log9)=3$, its convergent expansion is
97 \begin{equation}
98  \mathscr A(x)=\frac{\log9/8}{1+2x}
99    \sum_{h\ge0}\frac{(\log9)^h}{(h+1)!}(x+1)^h.
100  \label{eq:root:source}
101 \end{equation}
102 It follows coefficientwise that
103 $\mathscr A\in\mathbb Z_2\langle x\rangle^\times$,
104 $\mathscr A\equiv1\pmod2$, and $\mathscr A(N)=A(N)$.
105 
106 Set $r=M+1\ge1$ and define
107 \[
108  P_q(x)=\prod_{i=0}^{q-1}(x-i)(2x-(2i+1)),\qquad P_0=1,
109 \]
110 \[
111  H_r(x)=\sum_{q\ge0}8^q\frac{\beta_{r+q}}{\beta_r}
112                     P_q(x)\mathscr A(x-q).
113 \]
114 The coefficient valuations tend to infinity. At any nonnegative integer
115 $x$, terms with $q>x$ vanish. Cancelling the factorials in
116 \eqref{eq:root:packet} therefore gives the exact identity
117 \begin{equation}
118  \mathcal T_{r-1}(N)=\kappa_r\binom{2N}{2r}H_r(N-r)
119  \qquad(N\ge r).\label{eq:root:factor}
120 \end{equation}
121 This is a finite rational identity at every original Euler row.
122 
123 The scalar packet weights have exact valuations
124 \[
125  \lambda_r(q)=3q+s_2(r+q)-s_2(r).
126 \]
127 Put
128 \[
129  \mu_r=\min_{q\ge0}\lambda_r(q),\qquad
130  J_r=\{q:\lambda_r(q)=\mu_r\},\qquad G_r=2^{-\mu_r}H_r.
131 \]
132 Since $\lambda_r(0)=0$ and
133 $\lambda_r(q)\ge3q+1-s_2(r)$, every minimizing address satisfies
134 \begin{equation}
135  0\le q\le\left\lfloor\frac{s_2(r)-1}{3}\right\rfloor.
136  \label{eq:root:cutoff}
137 \end{equation}
138 In particular $\mu_r\le0$, and the minimum is found by a finite carry
139 calculation. Reduction of the whole series gives
140 \begin{equation}
141  \overline G_r(X)=\sum_{q\in J_r}X^{\underline q}
142        \quad\text{in }\mathbb F_2[X].
143  \label{eq:root:reduction}
144 \end{equation}
145 Its highest degree is $\max J_r$, with leading coefficient one.
146 Thus the normalization is the actual Gauss normalization.
147 
148 \begin{theorem}[Exact classical tail valuation]
149 For every $r\ge1$ and $N\ge r$,
150 \begin{equation}
151  v_2\bigl(\mathcal T_{r-1}(N)\bigr)
152  =4r-1+v_2\binom Nr+\mu_r+v_2G_r(N-r).
153  \label{eq:root:exactvaluation}
154 \end{equation}
155 There are unique factors
156 \[
157  G_r(X)=W_r(X)U_r(X),
158 \]
159 where $W_r\in\mathbb Z_2[X]$ is monic of degree $d_r=\max J_r$ and
160 $U_r\in\mathbb Z_2\langle X\rangle^\times$ satisfies $U_r\equiv1\pmod2$.
161 Consequently $v_2G_r(x)=v_2W_r(x)$ for every $x\in\mathbb Z_2$, and
162 \[
163  \deg W_r\le\left\lfloor\frac{s_2(r)-1}{3}\right\rfloor.
164 \]
165 \label{thm:root:finitepreparation}
166 \end{theorem}
167 \begin{proof}
168 Equation~\eqref{eq:root:factor}, the exact weight in
169 \eqref{eq:root:weights}, and the digit-sum identity
170 $v_2\binom{2N}{2r}=v_2\binom Nr$ prove
171 \eqref{eq:root:exactvaluation}. The binomial coefficients themselves
172 need not be equal.
173 
174 For preparation, start from the monic polynomial
175 $g=\overline G_r$ and its zero-one lift $W_1$, with $U_1=1$.
176 Suppose $G_r-W_kU_k$ is coefficientwise divisible by $2^k$.
177 Its divided reduction is a finite polynomial because $G_r$ is restricted.
178 Divide it by $g$ in $\mathbb F_2[X]$:
179 \[
180  \overline{(G_r-W_kU_k)/2^k}=gq+s,\qquad\deg s<d_r.
181 \]
182 With zero-one coefficient lifts, set
183 $W_{k+1}=W_k+2^ks$ and $U_{k+1}=U_k+2^kq$.
184 The error is now divisible by $2^{k+1}$, the polynomial remains monic of
185 degree $d_r$, and the unit reduces to one. The sequences converge in the
186 Gauss norm. Uniqueness of quotient and remainder at successive binary
187 digits proves uniqueness of the factors. For $d_r=0$, take $W_r=1$.
188 The degree bound follows from \eqref{eq:root:cutoff}.
189 \end{proof}
190 
191 This theorem reduces every depth to a finite polynomial without discarding
192 the infinite analytic tail. It does not explicitly classify every
193 $W_r$, decide every repeated root from a fixed precision, or prove that
194 all its dyadic roots are simple.
195 
196 \subsection{Regular walls: exact root emergence}
197 \label{app:root:regular}
198 
199 For a wall label $j\ge1$ and $0\le q<j$, define
200 \[
201  e_j(q)=3q+s_2(j-1)-s_2(j-q-1),\qquad
202  E_j=\min_{q<j}e_j(q),
203 \]
204 \[
205  \Theta(j)=3j+1+s_2(j-1),\qquad L_j=\Theta(j)-E_j.
206 \]
207 Here $E_j$ is a carry minimum, not an Euler number. A wall label is
208 \emph{regular} when $e_j(q)>0$ for $1\le q<j$.
209 For $r=2^L-j$ with $L>L_j$, put $\delta=L-L_j$.
210 The carry identities give
211 \[
212  \mu_r=E_j-\delta,\qquad J_r=\{j\},\qquad
213  G_r(x)=P_j(x)U(x-j)+2^\delta V(x),
214 \]
215 where $U\equiv1\pmod2$. For a regular label, also
216 $E_j=0$ and $V\equiv1\pmod2$.
217 
218 For $0\le i<j$, let
219 \[
220  d_i=v_2(i!)+v_2((j-1-i)!),\qquad
221  k_i=1+\left\lfloor\log_2\max(i,j-1-i)\right\rfloor,
222 \]
223 \[
224  B_i=i+2^{k_i}\mathbb Z_2,\qquad t_i=d_i+k_i.
225 \]
226 At $j=1$ use $d_0=k_0=t_0=0$. The balls $B_i$ partition
227 $\mathbb Z_2$. Indeed a residue represented twice among $0,\ldots,j-1$
228 splits into its two children. Every other represented residue remains
229 one ball. On each such ball,
230 \[
231  P_j(i+2^{k_i}y)=2^{t_i}yQ_i(y),\qquad
232  Q_i\in\mathbb Z_2\langle y\rangle^\times,
233  \qquad Q_i\equiv1\pmod2.
234 \]
235 
236 \begin{theorem}[Regular-wall root law]
237 For every regular label $j$ and every integer $\delta\ge1$,
238 \[
239  v_2G_r(x)=
240  \begin{cases}
241   \delta,&x\in B_i,\ \delta<t_i,\\
242   d_i+v_2(x-\alpha_i),&x\in B_i,\ \delta\ge t_i.
243  \end{cases}
244 \]
245 In the second case there is exactly one root $\alpha_i$ in $B_i$,
246 it is simple, and $v_2(\alpha_i-i)=\delta-d_i$.
247 Thus the number of dyadic roots is exactly
248 \[
249  \#\{i:0\le i<j,\ t_i\le\delta\}.
250 \]
251 \label{thm:root:regular}
252 \end{theorem}
253 \begin{proof}
254 If $\delta<t_i$, the unit perturbation has smaller valuation than
255 the skeleton term throughout $B_i$, so the valuation is exactly
256 $\delta$. Otherwise, after the ball substitution and division by
257 $2^{t_i}$, the coefficientwise reduction is $y+c$ for a constant
258 $c\in\mathbb F_2$. A restricted integral series with this reduction
259 is a dyadic isometry: division of its difference by $y-z$ gives an
260 odd linear coefficient plus even higher contributions. Binary lifting
261 therefore gives its unique root and exact distance law. Evaluating at
262 $x=i$ gives the stated displacement, since
263 $G_r(i)=2^\delta V(i)$ has exact valuation $\delta$.
264 The partition proves exhaustion of the roots.
265 \end{proof}
266 
267 The largest emergence threshold is
268 \[
269  \max_i t_i=v_2((j-1)!)+\lceil\log_2 j\rceil.
270 \]
271 For $j=2^a$, all thresholds equal $j-1$. There are no roots before
272 that distance and exactly $j$ simple roots at and after it, within the
273 positive-distance range. The equality and pre-wall cases are also
274 resolved: regular labels $j\ge2$ have no roots there. $j=1$ has one
275 simple odd root at equality.
276 
277 For example, $j=5$ has $(t_0,\ldots,t_4)=(6,3,4,3,6)$.
278 The exact root counts at distances $1,2,3,4,5,\ge6$ are
279 $0,0,2,3,3,5$. The older sufficient stages $3,5,7$ are not the
280 sharp emergence stages, which are $3,4,6$.
281 The first irregular label, $j=17$, has $V\equiv1+X\pmod2$.
282 The regular-wall theorem does not apply. Complete coefficient
283 certificates close distances $1$ through $19$, and the general separation
284 theorem gives all seventeen simple roots for $\delta\ge20$.
285 Those two kinds of evidence together resolve that family.
286 
287 \subsection{What the later simplicity reductions prove}
288 \label{app:root:families}
289 
290 For a general depth $r$, call $j_r=\max J_r$ its \emph{true terminal}.
291 This definition depends on the actual carry minimum. Rewriting the same
292 integer as another wall expression does not change $j_r$.
293 The universal simplicity target is
294 \begin{equation}
295  \text{for every integer }r\ge1\text{ and }x\in\mathbb Z_2,
296  \qquad G_r(x)=0\ \Longrightarrow\ G_r'(x)\ne0.
297  \label{eq:root:simplicitytarget}
298 \end{equation}
299 The following are completed restricted results of the later continuations.
300 Their family statements include a proof that the indicated label is the
301 true terminal throughout the displayed ranges.
302 
303 \begin{center}
304 \begin{tabular}{lll}
305 \toprule
306 Depth $r$ & Odd multiplier range & Outer scales\\
307 \midrule
308 $B2^L-129$ & $0<B<2^{89}$ & $L\ge392$\\
309 $B2^L-161$ & $0<B<2^{932}$ & $L\ge487$\\
310 \bottomrule
311 \end{tabular}
312 \end{center}
313 All dyadic roots are simple in both infinite integer families.
314 For arbitrary larger admissible multipliers, a multiple root with true
315 terminal $129$ can occur only at $L=515$ and in two necessary multiplier
316 classes modulo $2^{90}$. With true terminal $161$, it can occur only at
317 $L=640$ and in one necessary multiplier class modulo $2^{935}$.
318 These classes are necessary conditions. The records do not assert
319 existence of a singular ordinary Euler index in them.
320 
321 For terminal $161$, the neighboring phases are resolved uniformly:
322 $L=639$ has exactly one simple root and $L=641$ exactly three simple
323 roots, for every positive odd multiplier with that true terminal.
324 The middle phase is reduced, before the deeper certificate is applied,
325 to
326 \[
327  B\equiv17659\pmod{2^{18}},\qquad
328  x\equiv10202\pmod{2^{15}}.
329 \]
330 The $935$-bit multiplier condition composes this whole-phase reduction
331 with an inherited $917$-bit local parameter certificate. It is neither
332 a new $935$-bit reconstruction nor an all-precision interpolation of
333 the undepleted Euler family.
334 
335 The structural argument also extends beyond lower address one.
336 For a certified true-terminal wall, let $a$ be its last lower minimizing
337 address, $k=j_r-a$ the regular complement, and $t=v_2(k)$.
338 Under the regular lower-address hypotheses of the source theorem,
339 all roots above emerged complement balls are simple. Every root is
340 simple at every wall distance in the band
341 \[
342  \Theta(a)\le t<\Theta(a)+v_2(a!).
343 \]
344 Equality walls are simple even outside that band. This includes
345 certified terminal-$258$ walls with $a=2$, $k=256$, and $L\ge777$.
346 For $a=3$, $k=4096$, only $L=16385$ remains a possible critical scale.
347 Outside the band, the theorem gives necessary local valuation conditions.
348 It does not exclude the remaining unit cancellation. Irregular lower
349 addresses need their own prefix analysis.
350 
351 \subsection{The actual stationary discriminant}
352 \label{app:root:stationary}
353 
354 The current focused obstruction is the admitted ordinary-index family
355 \begin{equation}
356  r=(17659+2^{18}T)2^{640}-161,
357  \qquad T\in\mathbb Z_{\ge0},\qquad j_r=161.
358  \label{eq:root:focusedfamily}
359 \end{equation}
360 On its surviving chart define the \emph{actual}, undepleted function
361 \[
362  K_r(Z)=2^{-178}G_r(10202+2^{15}Z).
363 \]
364 The complete coefficient theorem gives
365 \begin{equation}
366  K_r(Z)=a_r+2b_rZ+u_rZ^2+256Z^3R_r(Z),
367  \quad a_r,b_r\in\mathbb Z_2,\quad
368  u_r\in\mathbb Z_2^\times,\quad
369  R_r\in\mathbb Z_2\langle Z\rangle.
370  \label{eq:root:quadraticclass}
371 \end{equation}
372 Its half derivative is a dyadic isometry. It therefore has a unique
373 critical point $c_r\in\mathbb Z_2$. Set
374 $\Phi_r^{\mathrm{act}}=K_r(c_r)$.
375 The earlier independent-undepletion notation for this same scalar is
376 $\Phi_r(2^{2r-25})$.
377 Excluding a multiple root on the surviving chart is exactly the assertion
378 $\Phi_r^{\mathrm{act}}\ne0$.
379 
380 \begin{proposition}[Exact quadratic compression]
381 There is a unique preparation
382 \[
383  K_r(Z)=\mathcal U_r(Z)\mathcal W_r(Z),\qquad
384  \mathcal W_r(Z)=Z^2+2\beta_rZ+\alpha_r,\qquad
385  \mathcal U_r\equiv u_r\pmod{256}.
386 \]
387 With $\delta_r=\beta_r^2-\alpha_r$ and
388 $\tau_r=\mathcal U_r'(c_r)/\mathcal U_r(c_r)$,
389 \begin{equation}
390  \delta_r=-\frac{\Phi_r^{\mathrm{act}}}{\mathcal U_r(c_r)}
391   \left(1-\frac{\tau_r^2\Phi_r^{\mathrm{act}}}{4\mathcal U_r(c_r)}\right),
392  \qquad v_2(\delta_r)=v_2(\Phi_r^{\mathrm{act}}).
393  \label{eq:root:discriminant}
394 \end{equation}
395 The equality includes the zero case.
396 \end{proposition}
397 \begin{proof}
398 The same successive monic polynomial division used in
399 Theorem~\ref{thm:root:finitepreparation}, started at precision eight,
400 preserves the quadratic and unit reductions of
401 \eqref{eq:root:quadraticclass}. Write
402 $W=Z^2+2\beta_rZ+\alpha_r$ and $w=W(c_r)$.
403 Stationarity gives $W'(c_r)=-\tau_rw$, while
404 $w=\Phi_r^{\mathrm{act}}/\mathcal U_r(c_r)$.
405 The quadratic identity
406 $\beta_r^2-\alpha_r=W'(c_r)^2/4-W(c_r)$ proves the formula.
407 Since $\tau_r\in256\mathbb Z_2$, its bracket is a unit.
408 \end{proof}
409 
410 This compression retains the unit-cofactor derivative. It does not
411 assert that $c_r$, $\alpha_r$, or $\beta_r$ is rational or algebraic
412 over $\mathbb Q$. The remaining arithmetic obligation is therefore
413 \begin{equation}
414  \delta_r\ne0\quad\text{for every admitted ordinary index in
415  \eqref{eq:root:focusedfamily}.}
416  \label{eq:root:remaining}
417 \end{equation}
418 Even this assertion would still leave the terminal-$129$ and higher-address
419 obligations in the universal target \eqref{eq:root:simplicitytarget}.
420 
421 \subsection{Approximation reaches every depth, but separation remains open}
422 \label{app:root:approximation}
423 
424 The latest continuation retains the exact Bernoulli undepletion factor
425 \[
426  e_{r,q}=\frac{1-2^{2r-1}}{1-2^{2r-1}4^q},\qquad q\ge0.
427 \]
428 It is a dyadic unit, including $e_{r,0}=1$. Multiplication by this
429 factor preserves the all-$q$ error of the shifted Jacobi moment model.
430 Consequently the actual model critical values satisfy, for every $m\ge25$,
431 \begin{equation}
432  v_2\bigl(\Phi_{r,m}^{\mathrm{act}}-\Phi_r^{\mathrm{act}}\bigr)
433  \ge L_m=8m-4s_2(m)-178,
434  \qquad L_m\longrightarrow\infty.
435  \label{eq:root:actualapprox}
436 \end{equation}
437 The estimate includes every packet and controls motion of the critical
438 point. There is no ceiling at the undepletion exponent $2r-25$.
439 For each fixed admitted $r$ it implies the exact equivalence
440 \begin{equation}
441  \Phi_r^{\mathrm{act}}\ne0
442  \quad\Longleftrightarrow\quad
443  \text{there exists }m\ge25\text{ such that }
444  v_2(\Phi_{r,m}^{\mathrm{act}})<L_m.
445  \label{eq:root:stricttest}
446 \end{equation}
447 Indeed a passing strict test has the same valuation as the limit. Conversely
448 any finite limit valuation is eventually smaller than $L_m$.
449 The existence of a passing depth for every ordinary index is unproved.
450 Nonzero models at every depth are compatible with an exactly zero limit.
451 
452 The degree-two preparation also reduces the old representative-height
453 cost to a linear cost, about $2P$ bits at precision $P$. This remains
454 larger than the $P$ bits needed for a strict nonzero residue certificate.
455 The fixed rational control $(Z-1/3)^2$ has zero critical value while
456 its least-residue integer discriminant representatives are nonzero at
457 every even $P\ge6$. Thus a nonzero integer representative alone cannot
458 prove a nonzero dyadic discriminant.
459 
460 One sufficient new arithmetic input would be an odd-denominator
461 projective quadratic
462 \[
463  A Z^2+2BZ+C\equiv A\mathcal W_r(Z)\pmod{2^P},\qquad A\text{ odd},
464  \qquad 0<|B^2-AC|<2^P,
465 \]
466 at a proved precision for every admitted ordinary $r$.
467 Then $(B^2-AC)/A^2\equiv\delta_r\pmod{2^P}$ cannot vanish
468 modulo $2^P$. No depth-independent theorem supplying this inequality
469 has been established. The tested recurrence and exterior-contact
470 identities retain balancing terms and do not force a contradiction.
471 Finite exponential models approximate the actual target at every depth,
472 but their order grows with precision, their clearing polynomial has
473 zeros on the actual chart, and their proved construction-specific height
474 cost does not give the required discriminant bound.
475 
476 \subsection{Status and source map}
477 \label{app:root:evidence}
478 
479 \begin{center}
480 \begin{tabular}{>{\raggedright\arraybackslash}p{0.64\linewidth}>{\raggedright\arraybackslash}p{0.26\linewidth}}
481 \toprule
482 Claim & Status at this edition\\
483 \midrule
484 Nishibuchi Conjecture~3.9 in its stated parameter range
485  & Resolved in the main text\\
486 Sharp uniform ordinary Euler tail exponent $4M+3$
487  & Proved, with earlier formal coverage\\
488 Exact tail factorization and finite polynomial at every depth
489  & Proved in the later prose development\\
490 Regular-wall emergence and indicated integer simplicity families
491  & Proved within their stated hypotheses\\
492 Actual quadratic compression and unbounded stationary approximation
493  & Proved. No fresh Lean build\\
494 Nonzero actual stationary discriminant for every admitted index
495  & Open\\
496 Universal simplicity of every $G_r$
497  & Open\\
498 Native~13.2 presentation invariance and Native~13.3 global/completed gluing
499  & Separate open general programs\\
500 \bottomrule
501 \end{tabular}
502 \end{center}
503 
504 The tail factorization, regular-wall proofs, finite preparation, and
505 coefficient cutoffs are recorded in the preserved
506 \nolinkurl{sources/euler_v4.md} of the regular-address checkpoint.
507 The two integer families and multiplier conditions are proved in its
508 \nolinkurl{next/terminal129/PROOF.md} and
509 \nolinkurl{next/critical_phases/PROOF.md}.
510 \nolinkurl{local_parameter/RECENTER_PROOF.md} supplies the inherited
511 local precision certificate. The higher-address extension is in
512 \nolinkurl{next/higher_address/regular_address_transversality.md}.
513 The stationary checkpoint records the exact discriminant identity in
514 \nolinkurl{stationary_separation/ordinary/QUADRATIC_COMPRESSION_AND_HEIGHT.md}
515 and actual convergence in
516 \nolinkurl{stationary_separation/root/ACTUAL_LIMIT_AND_SEPARATION.md}.
517 Its synthesis and proof reviews retain the failed
518 implications and the precise remaining arithmetic input.
519 
520 The source archive's \nolinkurl{evidence/root_scope_inventory.md} gives
521 the full checkpoint paths and content hashes used for this appendix.
522 The 2026-10-05 complete-work archive preserves the original layouts and
523 historical releases. Its stored hashes and verification receipts are
524 evidence of integrity and recorded execution. They are not substitutes
525 for a proof of the open assertions above.

Back to source controls

Back to Realization Calculus