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 \clearpage\section{Restricted native progress and complete prose proofs}\label{app:native}
2 This appendix reproduces the mathematical parts of the 8 September 2026
3 native progress note. The polynomial obstruction, finite reconstruction,
4 rectangularity and topological arguments are prose proofs. The intrinsic
5 commutative-algebra obstruction is the stated classical Stacks specialization,
6 with its original source record and finiteness argument. None of these prose
7 arguments is promoted to a new Lean run or to a completion of unrestricted
8 Native 13.2 or 13.3.
9 \hypertarget{native:a-complete-polynomial-obstruction-theorem}{%
10 \subsection{2. A complete polynomial obstruction
11 theorem}\label{native:a-complete-polynomial-obstruction-theorem}}
12 
13 \textbf{Scope.} Fix a prime \(p\), an integer \(L\ge1\), finite natural
14 numbers \(d,r\), and polynomials
15 \(F_1,\ldots,F_r\in\mathbb Z[X_1,\ldots,X_d]\). Let
16 \(\bar x\in(\mathbb Z/p^L\mathbb Z)^d\) satisfy every equation
17 \(F_i(\bar x)=0\). Choose any integer representative
18 \(x\in\mathbb Z^d\). Set
19 
20 \[e_i=F_i(x)/p^L\pmod p,\qquad J_{ij}=\frac{\partial F_i}{\partial X_j}(x)\pmod p.\]
21 
22 The divisions are exact integer divisions. Regard \(J\) as a linear map
23 \(\mathbb F_p^d\to\mathbb F_p^r\). Define
24 
25 \[O_{F,\bar x}=\mathbb F_p^r/\operatorname{im}J,\qquad o_{F,\bar x}=[e].\]
26 
27 \textbf{Theorem.} For this fixed polynomial presentation, the group and
28 distinguished class are independent of the chosen integer
29 representative. The class vanishes if and only if \(\bar x\) lifts to a
30 solution modulo \(p^{L+1}\). The obstruction group has
31 \(p^{r-\operatorname{rank}J}\) elements. When lifts exist, their set is
32 a torsor for \(\ker J\) and contains exactly
33 \(p^{d-\operatorname{rank}J}\) elements.
34 
35 \textbf{Proof.} For every integer correction vector \(t\), expansion of
36 each monomial gives
37 
38 \[F(x+p^Lt)\equiv F(x)+p^LJ(x)t\pmod {p^{L+1}}.\tag{1}\]
39 
40 Indeed, each term involving at least two correction factors is divisible
41 by \(p^{2L}\), and \(2L\ge L+1\). Constant and linear correction terms
42 give the two displayed summands. Adding the monomial expansions proves
43 (1) for every polynomial, with no denominator or analytic convergence
44 issue.
45 
46 Every element reducing to \(\bar x\) is uniquely expressible modulo
47 \(p^{L+1}\) as \(x+p^Lt\) with \(t\in\mathbb F_p^d\). By (1), it solves
48 the equations exactly when
49 
50 \[e+Jt=0\quad\text{in }\mathbb F_p^r.\tag{2}\]
51 
52 Equation (2) is soluble exactly when \(e\in\operatorname{im}J\): the
53 sign makes no difference because the image is a subspace. This is
54 equivalent to \([e]=0\).
55 
56 Another representative has the form \(x'=x+p^Ls\). Since \(L\ge1\), its
57 Jacobian is the same modulo \(p\). Dividing (1) by \(p^L\) shows that
58 its residual digit is \(e'=e+Js\), so it gives exactly the same quotient
59 class. If \(t_0\) solves (2), all its solutions are \(t_0+\ker J\), and
60 no others. The finite cardinalities follow from rank-nullity. This also
61 covers no variables, no equations, zero Jacobian and singular solutions.
62 \(\square\)
63 
64 The proof is a universal mathematical argument. The accompanying Python
65 checks are independently bounded evidence about an implementation, not a
66 substitute for that argument. The standalone Lean specialization does
67 not formalize multivariable polynomial expansion (1), unless its own
68 checked source explicitly says so.
69 
70 \hypertarget{native:necessary-boundaries-and-exact-examples}{%
71 \subsubsection{Necessary boundaries and exact
72 examples}\label{native:necessary-boundaries-and-exact-examples}}
73 
74 \begin{itemize}
75 \tightlist
76 \item
77   \textbf{A failed singular lift:} \(p=3\), \(L=1\), \(F(X)=X^2-3\),
78   \(x=0\). Here \(e=-1\ne0\) in \(\mathbb F_3\) and \(J=0\). There are
79   no lifts of zero modulo 3 to a root modulo 9.
80 \item
81   \textbf{Representative independence is a quotient assertion:} for
82   \(F(X)=X^2-1\), \(p=3\), \(L=1\), representatives \(1\) and \(4\) have
83   residual digits \(0\) and \(2\). Their common Jacobian is \(2\), with
84   full image, and both give zero obstruction. Their corrected
85   representatives \(1\) and \(10\) are the same root modulo 9.
86 \item
87   \textbf{A successful step need not give indefinite continuation:} for
88   \(F(X)=X^2-5\), \(p=2\), the root \(1\) modulo 2 has zero obstruction
89   and lifts to \(1,3\) modulo 4. Both have nonzero obstruction at the
90   next step. There is no root modulo 8 and no compatible infinite lift.
91 \item
92   \textbf{The raw Jacobian cokernel need not be presentation
93   independent:} the presentations \(F=(X)\) and \(G=(X,0)\) define the
94   same solution system. Their raw obstruction groups at zero are
95   respectively zero and \(\mathbb F_p\). Both actual distinguished
96   obstructions are zero. Thus one cannot claim a canonical isomorphism
97   of these two raw groups merely because the equations define the same
98   seed.
99 \end{itemize}
100 
101 \hypertarget{native:an-intrinsic-finite-obstruction-under-an-algebraic-restriction}{%
102 \subsection{3. An intrinsic finite obstruction under an algebraic
103 restriction}\label{native:an-intrinsic-finite-obstruction-under-an-algebraic-restriction}}
104 
105 Let \(B\) be a finitely presented commutative \(\mathbb Z\)-algebra,
106 \(p\) prime and \(L\ge1\). For a ring map
107 \(f:B\to\mathbb Z/p^L\mathbb Z\), use its reduction to make
108 \(\mathbb F_p\) a \(B\)-module. There is a canonical class
109 
110 \[o(f)\in\operatorname{Ext}^1_B(\mathrm{NL}_{B/\mathbb Z},\mathbb F_p)\]
111 
112 whose vanishing is equivalent to a lift
113 \(B\to\mathbb Z/p^{L+1}\mathbb Z\). This follows from the ring-map
114 lifting theorem in
115 \href{https://stacks.math.columbia.edu/tag/08S5}{Stacks Project, Lemma
116 91.2.1, tag 08S5}. Specialize the source extension to
117 \(0\to0\to B\to B\) and the target extension to the kernel
118 \(p^L/p^{L+1}\cong\mathbb F_p\). The base maps are identities of
119 \(\mathbb Z\). The kernel is square zero because \(L\ge1\).
120 
121 The comparison in
122 \href{https://stacks.math.columbia.edu/tag/00S1}{Stacks Project, Lemma
123 10.134.2, tag 00S1} identifies the complex from a polynomial
124 presentation with the canonical naive cotangent complex up to homotopy.
125 Thus this construction is intrinsic, up to the stated canonical
126 comparison.
127 
128 The group is finite. Choose a finite presentation
129 \(P=\mathbb Z[X_1,\ldots,X_d]\twoheadrightarrow B\) with finitely
130 generated kernel \(I\). The presentation description in
131 \href{https://stacks.math.columbia.edu/tag/0GPU}{Stacks Project, Remark
132 91.2.4, tag 0GPU} identifies the group as
133 
134 \[\operatorname{coker}\left(\operatorname{Hom}_B(\Omega_{P/\mathbb Z}\otimes_P B,\mathbb F_p)\longrightarrow\operatorname{Hom}_B(I/I^2,\mathbb F_p)\right).\]
135 
136 If \(I\) has \(r\) chosen generators, evaluation on their classes
137 injects the latter Hom module into \(\mathbb F_p^r\). Hence its quotient
138 is finite. The relation module \(I/I^2\) retains dependencies between
139 equations, including redundant zero equations, which the raw target
140 \(\mathbb F_p^r\) does not.
141 
142 \textbf{Status:} externally proved after the exact stated
143 specialization, with the finiteness argument above. This theorem is not
144 independently formalized in the accompanying Lean file. Extending it to
145 all operator/recurrence/module systems admitted by manuscript Definition
146 1.1 requires a specified encoding and a proof that its notion of lift is
147 preserved. That is the missing implication for applying it to native
148 Conjecture 13.2 without restriction.
149 
150 \textbf{Source record.} The Stacks Project authors, live primary text
151 inspected 2026-09-08, tags 08S5, 0GPU and 00S1. Full theorem/proof text
152 was inspected, not only search snippets. No immutable source revision
153 was pinned or downloaded. The use is a classical specialization, not a
154 novelty search or a claim of a new obstruction theory. No broader paper
155 or source cache was changed.
156 
157 \hypertarget{native:a-topological-obstruction-to-the-proposed-spine-formula}{%
158 \subsection{4. A topological obstruction to the proposed spine
159 formula}\label{native:a-topological-obstruction-to-the-proposed-spine-formula}}
160 
161 Consider the recurrence \(a_{n+1}=a_n\) with integer initial value. Its
162 global parameter space is \(X=\mathbb Z\). Its local parameter spaces
163 are \(X_p=\mathbb Z_p\), and every local realization has the same
164 prime-independent recurrence. Give the local factors their usual
165 \(p\)-adic topologies and the product its product topology. For these
166 integral local factors, the restricted product relative to all
167 \(\mathbb Z_p\) is the ordinary product. Write
168 
169 \[A=\mathbb Z_2,\qquad B=\prod_{p>2}\mathbb Z_p,\qquad D=\{(n,(n)_{p>2}):n\in\mathbb Z\}\subset A\times B.\]
170 
171 \textbf{Theorem.} There are no Hausdorff space \(C\) and continuous maps
172 \(f:A\to C\), \(g:B\to C\) for which the equality locus
173 
174 \[\{(a,b):f(a)=g(b)\}\]
175 
176 is exactly \(D\). Thus the canonical local realizations of global
177 integer constant sequences cannot satisfy the manuscript's fiber-product
178 formula in this Hausdorff topological interpretation.
179 
180 \textbf{Proof.} The equality locus is closed: it is the inverse image of
181 the diagonal of \(C\times C\) under the continuous map \(f\times g\),
182 and a Hausdorff space has closed diagonal.
183 
184 The set \(D\) is dense in \(A\times B\). A nonempty basic open set
185 prescribes congruences at only finitely many primes and finite precision
186 at each. The moduli are pairwise coprime. The finite Chinese remainder
187 theorem supplies an integer meeting all those congruences, so every such
188 open set meets \(D\).
189 
190 However, \(D\) is not the whole product. The element with 2-adic
191 coordinate zero and every odd-adic coordinate one is not diagonal. If an
192 integer had zero 2-adic coordinate, it would be divisible by every power
193 of two, forcing it to be zero. Its 3-adic coordinate would then be zero,
194 not one. Consequently \(D\) is a proper dense subset and is not closed.
195 It cannot be the equality locus above. \(\square\)
196 
197 This is not asserted to refute the original, underspecified sentence
198 under every possible reading. It refutes the explicit and natural
199 interpretation just stated. The assumptions of continuity, Hausdorffness
200 and identification through the canonical local maps are essential to
201 this claim.
202 
203 \hypertarget{native:a-precise-reconstruction-that-does-hold}{%
204 \subsubsection{A precise reconstruction that does
205 hold}\label{native:a-precise-reconstruction-that-does-hold}}
206 
207 For a finite set \(S\) of primes, positive precisions \(L_p\), and a
208 fixed integer polynomial system \(F\), put
209 
210 \[N=\prod_{p\in S}p^{L_p},\qquad\operatorname{Sol}_F(R)=\{x\in R^d:F(x)=0\}.\]
211 
212 Then coefficientwise CRT gives a canonical bijection
213 
214 \[\operatorname{Sol}_F(\mathbb Z/N\mathbb Z)\cong\prod_{p\in S}\operatorname{Sol}_F(\mathbb Z/p^{L_p}\mathbb Z).\]
215 
216 The reason is exact: the CRT ring isomorphism preserves polynomial
217 evaluation, and zero in a finite product is equivalent to zero in every
218 component. For \(F\) empty, passing to all compatible finite congruences
219 identifies the profinite completion \(\widehat{\mathbb Z}\) with
220 \(\prod_p\mathbb Z_p\). The same finite reconstruction is compatible
221 with coefficient projections and integer recurrence matrices because
222 these operations commute with reduction and CRT.
223 
224 Here the polynomial equations or recurrence matrices are fixed common
225 data. The theorem reconstructs finite or profinite objects. It does not
226 identify a ``smallest'' spine, impose additional spectral descent, or
227 recover global \(\mathbb Z\) from arbitrary tuples of local points. A
228 completed version of 13.3 must say exactly which object is completed and
229 specify its universal property.
230 
231 \hypertarget{native:a-finite-compatibility-criterion-with-a-precise-universal-property}{%
232 \subsubsection{A finite compatibility criterion with a precise universal
233 property}\label{native:a-finite-compatibility-criterion-with-a-precise-universal-property}}
234 
235 Fix finite sets \(A,B\) of local packets and an explicitly given
236 relation \(R\subseteq A\times B\). Say that \(R\) is rectangular when
237 
238 \[R(a,b),\ R(a',b),\ R(a',b')\quad\Longrightarrow\quad R(a,b')\]
239 
240 for all \(a,a'\in A\) and \(b,b'\in B\).
241 
242 \textbf{Theorem.} The relation \(R\) can be represented exactly as
243 
244 \[R(a,b)\quad\Longleftrightarrow\quad f(a)=g(b)\]
245 
246 for maps from \(A\) and \(B\) to a common set if and only if \(R\) is
247 rectangular. In that case a canonical finite choice of common set is the
248 connected-component set \(C_R\) of the bipartite graph with vertex set
249 \(A\sqcup B\) and edges given by \(R\).
250 
251 The component maps \(f_R:A\to C_R\) and \(g_R:B\to C_R\) have the
252 following universal property. For every set \(Y\) and maps \(h:A\to Y\),
253 \(k:B\to Y\) satisfying \(h(a)=k(b)\) whenever \(R(a,b)\), there is a
254 unique map \(u:C_R\to Y\) with \(u\circ f_R=h\) and \(u\circ g_R=k\).
255 
256 \textbf{Proof.} Any equality representation is rectangular, since the
257 three assumed equalities imply \(f(a)=g(b)=f(a')=g(b')\).
258 
259 Conversely, suppose \(R\) is rectangular. An edge always gives equal
260 component labels. If \(a\in A\) and \(b\in B\) have equal component
261 labels, there is a finite path between them. Its length is odd. A path
262 of length one is already an \(R\)-edge. A longer path begins with three
263 edges \(a-b_1-a_1-b_2\). Rectangularity gives the edge \(a-b_2\).
264 Replacing these three edges by that edge shortens the path by two.
265 Induction therefore yields \(R(a,b)\). This proves the exact equality
266 representation. Finiteness follows because the component set is a
267 quotient of the finite set \(A\sqcup B\).
268 
269 For the universal property, combine \(h\) and \(k\) into a function on
270 \(A\sqcup B\). It is constant across every edge by hypothesis, hence
271 along every finite path. It therefore descends to a well-defined
272 function on components. The two required factorization identities hold
273 by construction. They determine the value on every component, proving
274 uniqueness. \(\square\)
275 
276 For example, the three pairs \((a_0,b_0),(a_1,b_0),(a_1,b_1)\) without
277 \((a_0,b_1)\) fail rectangularity. Every equality-label representation
278 agreeing on those three pairs also admits the fourth pair, so it cannot
279 represent that relation exactly.
280 
281 This is a precise finite gluing obligation: future arithmetic
282 applications must define \(A\), \(B\) and \(R\) and prove
283 rectangularity. The universal property holds for the component quotient
284 even when rectangularity fails, but then the equality locus strictly
285 enlarges \(R\). The theorem establishes neither a minimum number of
286 labels nor a smallest spine in the manuscript's unspecified category. It
287 carries no automatic topology, spectral information or Frobenius
288 compatibility. \textbf{Evidence: prose proof in this note, not a Lean
289 formalization.}

Back to source controls

Back to Realization Calculus