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{Open questions and further directions}
2 \label{sec:open}
3 
4 The arithmetic results above resolve Nishibuchi's conjecture throughout its
5 stated parameter range. The local analyticity and differentiability theorem
6 is also complete under its stated invertibility hypothesis. What remains is
7 a set of extensions and sharper classifications, together with the broader
8 questions raised by the original native seed-calculus program.
9 
10 \subsection{Singular persistence beyond an invertible solved block}
11 \label{subsec:singular-open}
12 
13 The weighted lifting theorem allows the solved Jacobian to be noninvertible
14 modulo $p$ provided that it is invertible over $\Qp$ with a controlled inverse.
15 This includes a substantial class of lifts often called singular modulo $p$.
16 The next problem is to understand Jacobians that remain rank-deficient over
17 $\Qp$, where the inverse construction is no longer available.
18 
19 For a fixed polynomial system $F\in\Z[X_1,\ldots,X_d]^e$, a precision $L\geq1$,
20 and a root $\bar x$ modulo $p^L$, let
21 \[
22 \mathcal L_{F,L}(\bar x)
23 =\{x'\in(\Z/p^{L+1}\Z)^d:
24 F(x')=0,\ x'\equiv\bar x\pmod{p^L}\}.
25 \]
26 The finite obstruction theorem decides whether this set is empty from the
27 residual digit and reduced Jacobian. When it is nonempty, the theorem also
28 determines its cardinality and affine kernel structure. The conclusion
29 concerns one level: vanishing of the obstruction permits the next step,
30 but does not guarantee that subsequent steps are possible.
31 
32 For example, $X^2-5$ has the root $1$ modulo $2$, and both $1$ and $3$ lift it
33 to roots modulo $4$. Every odd square is $1$ modulo $8$, so neither branch
34 continues to a root modulo $8$. Thus even a successful first correction can
35 lead to branches that stop at the following level.
36 
37 We seek structural hypotheses and higher obstruction data that control an
38 entire singular branch, including its behavior under coefficient and parameter
39 deformation. One route is to propagate suitable conditions from level to
40 level. Another is to prove existence at all levels in a form that yields
41 compatible branches. The finite obstruction calculus supplies the tests for
42 individual levels, but a persistence theorem needs a further argument linking
43 them. Any general formulation must allow multiple branches, later
44 obstructions, and changes in the rank of the Jacobian.
45 
46 \subsection{Native 13.2: presentation invariance}
47 \label{subsec:native132}
48 
49 The original conjecture asks for a canonical finite obstruction packet whose
50 vanishing is necessary and sufficient for a one-level lift in a finitely
51 presented arithmetic seed system. For a fixed finite polynomial presentation,
52 the chapter supplies the precise obstruction
53 \[
54 o_{F,\bar x}=[r]\in
55 \coker\!\left(J_{F,\bar x}:\F_p^d\longrightarrow\F_p^e\right),
56 \]
57 where $r$ is the residual digit. We have proved independence from the chosen
58 integer representative. Invariance under a change of equations or presentation
59 requires more.
60 
61 The raw cokernel already reveals the difficulty.
62 The presentations $F=(X)$ and $G=(X,0)$ describe the same zero locus over every
63 coefficient ring. At zero their Jacobians are, respectively,
64 \[
65 \F_p\xrightarrow{\,1\,}\F_p,
66 \qquad
67 \F_p\xrightarrow{\,(1,0)\,}\F_p^2.
68 \]
69 Their raw cokernels are $0$ and $\F_p$. Both distinguished obstruction classes
70 vanish, but the ambient obstruction groups are not isomorphic. The example
71 rules out the raw cokernel as a presentation-independent object while leaving
72 open the possibility of an intrinsic obstruction construction.
73 
74 A precise form of Native 13.2 therefore needs four ingredients:
75 \begin{enumerate}
76 \item a category of seed objects, including how the operators, relations,
77 projectors, weights, and topology enter an object;
78 \item specified changes of presentation and a proof that they preserve the
79 actual lift problem;
80 \item an obstruction object that respects dependencies among the relations,
81 together with comparison maps or a universal property;
82 \item a precise meaning of ``finite'' and ``canonical'', and a proof that
83 vanishing is equivalent to the intended one-step continuation.
84 \end{enumerate}
85 For commutative algebra presentations, the relation module offers a natural
86 way to account for dependencies among listed equations. To extend this
87 approach to the full seed vocabulary, we would need an encoding that preserves
88 the lift problem, together with a proof of that preservation. This is one of
89 the links still needed between the concrete obstruction theorem and Native 13.2.
90 
91 \subsection{Native 13.3: finite compatibility, completion, and descent}
92 \label{subsec:native133}
93 
94 The original proposed form is
95 \[
96 X\simeq X_2^{\mathrm{wt}}\times_C\prod_{p>2}'X_p.
97 \]
98 It leaves $X$, the distinguished subsets defining the restricted product,
99 the maps to $C$, the ambient category, and the universal meaning of
100 ``smallest'' unspecified. In particular, one must decide whether $X$ is a
101 global object or a completed object.
102 
103 The linear compatibility theorem provides one concrete part of this program.
104 If two local observations
105 $J:U\to V$ and $K:U\to W$ are linear maps from the \emph{same} correction
106 module, define
107 \[
108 C_{J,K}=U/(\ker J+\ker K).
109 \]
110 The attainable observations $\im J$ and $\im K$ have canonical labels in this
111 quotient. Equality of labels is equivalent to simultaneous realization by a
112 single correction. The joint image is exactly the fiber product over
113 $C_{J,K}$, with the proved linear universal property.
114 The declarations are
115 \begingroup\small\raggedright
116 \lean{Komorebi.SharedCorrection.labels_eq_iff_common},
117 \lean{Komorebi.SharedCorrection.joint_range_eq_fiber}, and
118 \lean{Komorebi.SharedCorrection.common_universal}.
119 \par\endgroup
120 To apply this result arithmetically, one must construct the common correction
121 module and the observation maps, then show that the resulting compatibility
122 condition agrees with the intended arithmetic one.
123 
124 \paragraph{Why the global/completed distinction is necessary.}
125 Consider constant sequences with integer initial value. Their global parameter
126 space is $\Z$, while their local parameter spaces are $\Z_p$. Under the
127 canonical local maps, the image of the global objects is the diagonal
128 \[
129 D=\{(n)_p:n\in\Z\}\subseteq\prod_p\Z_p.
130 \]
131 This diagonal is dense: a basic open set specifies finitely many congruences,
132 and the Chinese remainder theorem provides an integer satisfying them. It is
133 proper: the tuple with $2$-adic coordinate zero and all odd-adic coordinates
134 one is not the image of an integer. Indeed an integer zero in $\Z_2$ must be
135 zero, contradicting its $3$-adic coordinate.
136 
137 Consequently this canonical global diagonal cannot be an equality locus
138 \[
139 \{(a,b):f(a)=g(b)\}
140 \subseteq \Z_2\times\prod_{p>2}\Z_p
141 \]
142 for continuous maps to a Hausdorff space $C$. Such an equality locus is closed,
143 as the inverse image of the closed diagonal in $C\times C$, whereas $D$ is
144 proper and dense. This topological argument, retained from the native progress
145 note, concerns the stated topological interpretation. It has not been
146 formalized in Lean for this manuscript.
147 
148 Finite CRT reconstruction leads to the familiar completed object
149 $\widehat\Z=\prod_p\Z_p$, but does not identify which local tuples come from a
150 single global integer. A complete form of Native 13.3 must therefore specify
151 finite-level compatibility, transition maps and completion, and any additional
152 global descent condition. If recurrence, spectral, or Frobenius information
153 is to supply that condition, it must be expressed through defined maps or
154 constraints on the local data, with a precise account of how they enter $C$.
155 
156 The accompanying \nolinkurl{native/Native_Conjectures_Progress.md} records
157 further results in restricted settings: an intrinsic finite
158 $\operatorname{Ext}^1$ obstruction for finitely presented commutative integer
159 algebras, finite CRT reconstruction for polynomial solution sets, and a
160 characterization of rectangular finite relations by equality of common
161 labels. The obstruction result is a stated specialization of a classical
162 external theorem. The CRT and rectangularity results have prose proofs in
163 the note. These are preserved mathematical progress, with the restrictions
164 and source records given there, rather than Lean completions of the general
165 Native 13.2 and 13.3 statements.
166 
167 \subsection{Arithmetic refinements}
168 \label{subsec:arithmetic-open}
169 
170 Write $U_{N,j}(n)=j!C_{N,j}(n)$ and $U_j=U_{4,j}$, and use
171 $v_p(0)=\infty$ when discussing valuation bounds. The following classification
172 questions remain open in this program.
173 
174 \begin{enumerate}
175 \item \textbf{The remaining higher-difference classification.}
176 The new strengthening chapters determine every repeated-step valuation in addresses $j=0,1$, give the exact criterion for equality in the common mixed-step lower bound there, and determine address-two valuations at all power-of-two orders. What remains is a complete exact formula in address two at the other orders, a full classification in address three, and the amount of additional cancellation in mixed-step cases where the leading term vanishes. Numerical patterns through a finite range do not settle these questions.
177 
178 \item \textbf{Upper-half addresses at larger dyadic rank.}
179 The exact first-difference laws now include $N=2,4,8$ and every lower-half address for $N=2^a\ge4$. Larger upper-half addresses need a finer classification. Explicit counterexamples show that extrapolating one low-order Newton coefficient to a universal metric law is false. A least period is measured in packet rows. Its Euler-degree displacement is $NP$.
180 
181 \item \textbf{Exact affine Mahler-kernel valuations.}
182 For the kernel of Section~\ref{subsec:polyphase-exposition}, determine exact
183 values of
184 \[
185 v_p\bigl(\Theta_{M,s}(r,k)\bigr),\qquad
186 \Theta_{M,s}(r,k)=[z^r](1+z)^s((1+z)^M-1)^k,
187 \]
188 beyond the explicit special families. The minimum valuation of the summands
189 gives a lower bound. Equality requires a separate argument excluding
190 cancellation.
191 
192 \item \textbf{Classical tail root classification and simplicity.}
193 The later tail program gives an exact factorization, finite preparation for each fixed depth, and several infinite regular-wall and simplicity families, as summarized in Appendix~\ref{app:root:scope}. A universal explicit root classification and universal simplicity of the remaining analytic factor are still open. In the exceptional address-one quadratic reduction, the residual task is a nonvanishing discriminant condition. Empty tails remain exactly zero. This problem is distinct from the solved Nishibuchi congruence conjecture.
194 \end{enumerate}
195 
196 These refinements build on the proved estimates and exact cases, including
197 the sharp uniform classical dyadic bound and the resolution of Nishibuchi's
198 conjecture.
199 
200 \subsection{Historical material and interface work}
201 \label{subsec:historical-scope}
202 
203 The original Paper IX, with corrected proof-status labels, survives as a
204 28-page PDF. Its recovered formalization supports the framework, Euler
205 coordinates, Mahler differences,
206 unit coordinates, recurrence packets, and CRT results retained in this
207 manuscript. The exact original TeX bytes, original figure-generation files, and complete
208 historical experiment package were not recovered with that PDF.
209 The reconstructed Annals text is reproduced in Appendix~\ref{app:recovered},
210 with its separate provenance and local qualifications. Their older
211 figure and test counts remain historical records. Those computations have
212 not been reproduced for this consolidation.
213 
214 A reconstructed textual copy of the Annals manuscript was also recovered.
215 It includes finite-field mode and subgroup inversion, Fourier invariance,
216 Carmichael and matrix transfer, Amice pullbacks, depleted analytic Euler
217 branches, and extensive polyphase formulas. The sharp classical dyadic kernel
218 and truncation claims from that text have since been connected to checked
219 Lean proofs. The finite polyphase formulas used for explanation here have
220 short explicit algebraic derivations. The remaining claims in that larger
221 historical text have not all been formalized.
222 The source archive retains the text with its provenance, and the statement
223 map distinguishes these historical claims from the certified claims in the
224 present manuscript.
225 
226 Remaining recovery work includes the precise older odd-prime edge identities,
227 their stated ranges, and the binary digit-sum form of the checked weights.
228 For each item, the work is to recover the formula with its stated range,
229 check the proof, and identify any corresponding Lean declaration. Where the
230 historical source is still missing, the record remains incomplete.
231 
232 One further task is to connect the older chart constructions to the new
233 regularity theorem. That theorem applies to polynomials with arbitrary
234 coefficients in the ambient field $\Qp$ and identifies the analytic
235 germ of every continuous ambient-field root selection under its hypotheses.
236 Several older rectangular charts were defined using integer coefficients,
237 integer centers, or subtype-valued maps. Comparing each such historical
238 interface explicitly with the new ambient formulation remains to be done.
239 These comparisons would connect the existing constructions to the proved
240 analytic implicit-function theorem. General singular persistence remains the
241 separate problem described in Section~\ref{subsec:singular-open}.

Back to source controls

Back to Realization Calculus