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 \hypertarget{cont9:paper-ix-compatible-towers-with-prescribed-parameters}{%
2 \subsection{Chapter IX: compatible towers with prescribed
3 parameters}\label{cont9:paper-ix-compatible-towers-with-prescribed-parameters}}
4 
5 The construction gives actual compatible polynomial towers from initial
6 solved-block surjectivity, for every compatible integer parameter path.
7 For a prime base, it constructs such a path for every p-adic parameter
8 in the initial ball and proves an exact polynomial endpoint with all
9 retained precisions. The formal companion identifies the six supporting modules and their
10 recorded compiler and axiom-audit results.
11 
12 \hypertarget{cont9:statement-and-notation}{%
13 \subsubsection{Statement and notation}\label{cont9:statement-and-notation}}
14 
15 Let \(q>0\), \(L\ge1\), and \[
16 F\in\mathbb Z[Y_1,\ldots,Y_m,T_1,\ldots,T_k]^e,
17 \qquad x=(y_0,t_0)\in\mathbb Z^{m+k},
18 \qquad F(x)\in q^L\mathbb Z^e.
19 \] Write \(S_q=\mathbb Z/q\mathbb Z\), and let the actual reduced
20 Jacobian blocks be \[
21 J_x=D_YF(x)\bmod q:S_q^m\longrightarrow S_q^e,
22 \qquad K_x=D_TF(x)\bmod q:S_q^k\longrightarrow S_q^e.
23 \] Assume \(J_x\) is surjective. A vector divisibility condition below
24 is coordinatewise.
25 
26 \textbf{Integer prescribed-path theorem.} For every supplied path
27 \(t:\mathbb N\to\mathbb Z^k\) satisfying \[
28 t(0)=t_0,\qquad t(n+1)-t(n)\in q^{L+n}\mathbb Z^k,
29 \] there is a single tower \(z:\mathbb N\to\mathbb Z^{m+k}\) with \[
30 z(0)=x,\qquad \operatorname{free}(z(n))=t(n),
31 \] \[
32 F(z(n))\in q^{L+n}\mathbb Z^e,\qquad
33 z(n+1)-z(n)\in q^{L+n}\mathbb Z^{m+k}.
34 \] The parameter equality is exact in integers. For \(a\le b\), \[
35 z(b)-z(a)\in q^{L+a}\mathbb Z^{m+k},\qquad
36 DF(z(n))\bmod q=DF(x)\bmod q.
37 \] Consequently \(J_{z(n)}=J_x\) at every level. No later surjectivity
38 or per-step solvability is assumed. This theorem includes positive
39 composite bases and \(q=1\).
40 
41 \textbf{Arbitrary p-adic target theorem.} Now let \(q=p\) be prime. For
42 every \[
43 \tau\in t_0+p^L\mathbb Z_p^k,
44 \] there are a compatible integer tower \(z\) as above and
45 \(b\in\mathbb Z_p^{m+k}\) such that \[
46 z(n)\longrightarrow b,\qquad F(b)=0,\qquad
47 \operatorname{free}(b)=\tau,
48 \qquad b-z(n)\in p^{L+n}\mathbb Z_p^{m+k}\quad(n\ge0).
49 \] A compatible integer parameter path converging to \(\tau\) is
50 constructed in the proof, with its initial representative fixed exactly.
51 A separate theorem accepts every supplied compatible integer path with
52 limit \(\tau\) and retains its exact coordinates in the constructed
53 tower.
54 
55 \textbf{Exact branching.} At any stage \(n\), put \(N=L+n\). For every
56 parameter digit \(v\in\mathbb F_p^k\), let \[
57 \mathcal L_{n,v}=\left\{\bar w\in(\mathbb Z/p^{N+1}\mathbb Z)^{m+k}:
58 \begin{array}{l}
59 \bar w\equiv z(n)\pmod{p^N},\\
60 F(\bar w)=0,\\
61 \operatorname{free}(\bar w)=t(n)+p^Nv\pmod{p^{N+1}}
62 \end{array}\right\}.
63 \] Here \(p^Nv\) means any integer representative of \(v\), multiplied
64 by \(p^N\). The residue class does not depend on the representative.
65 Then \[
66 \#\mathcal L_{n,v}=p^{m-e}\qquad\text{for every }n\text{ and every }v.
67 \] Surjectivity implies \(e\le m\). This is a count of distinct actual
68 next-level residue classes. It does not count integer representatives or
69 entire infinite towers.
70 
71 \textbf{Square solved-block uniqueness.} If \(m=e\), every prescribed
72 \(\tau\) has exactly one root in the original ball: \[
73 \exists!\,b\in x+p^L\mathbb Z_p^{e+k}:\quad
74 F(b)=0,\qquad\operatorname{free}(b)=\tau.
75 \] Thus all valid integer parameter approximations and all lifting
76 choices with the same target have the same endpoint. This does not
77 assert uniqueness of the integer representatives in the tower. All prime
78 statements include \(p=2\).
79 
80 \hypertarget{cont9:proof}{%
81 \subsubsection{Proof}\label{cont9:proof}}
82 
83 At depth \(N\ge1\), suppose \(F(a)=q^Nr\) and a desired next integer
84 parameter target satisfies \(t'-\operatorname{free}(a)=q^Nw\), with
85 \(w\in\mathbb Z^k\). Surjectivity supplies a solved digit \(u\in S_q^m\)
86 satisfying \[
87 J_a u=-\bar r-K_a\bar w.
88 \] Choose an integer representative \(\widetilde u\), and set \[
89 a'=a+q^N(\widetilde u,w).
90 \] The parameter quotient is the supplied integer \(w\). Therefore
91 \(\operatorname{free}(a')=t'\) exactly. The checked polynomial Taylor
92 identity gives \[
93 F(a')\equiv F(a)+q^NDF(a)(\widetilde u,w)
94 \equiv0\pmod{q^{N+1}}.
95 \] Its quadratic remainder is divisible by \(q^{2N}\), and
96 \(2N\ge N+1\). Also \(a'\equiv a\pmod q\), so evaluation of every
97 polynomial partial derivative gives the same reduced Jacobian. Induction
98 on the level, carrying the root, exact parameters, and fixed solved
99 Jacobian as its state, constructs the entire integer tower. The
100 existence proof uses ordinary classical choice. It does not supply an
101 optimized computational lifting algorithm.
102 
103 For a p-adic target \(\tau\), use \(t(0)=t_0\) and, for \(n\ge1\), the
104 canonical integer representatives of \(\tau\bmod p^{L+n}\). The initial
105 congruence hypothesis and the truncation precision imply \[
106 \tau-t(n)\in p^{L+n}\mathbb Z_p^k.
107 \] Subtracting successive precision relations gives compatibility in
108 \(\mathbb Z_p\). The checked faithful integer-divisibility theorem gives
109 compatibility in \(\mathbb Z\). These precision relations also give
110 convergence to \(\tau\).
111 
112 The compatible vector-tower completion theorem constructs \(b\), proves
113 convergence, and retains every stage precision. Continuous polynomial
114 evaluation and the increasing root precision give \(F(b)=0\). Each
115 parameter coordinate has both the corresponding coordinate of \(b\) and
116 \(\tau\) as its limit, so uniqueness of limits gives exact parameter
117 equality.
118 
119 For every proposed next parameter digit, the previously checked
120 obstruction is \([\bar r+K_av]\in S_p^e/\operatorname{im}J_a\). The
121 fixed solved Jacobian is surjective, so this class vanishes for every
122 digit at every stage. The actual lift fiber is a torsor for
123 \(\ker J_a\). Rank-nullity gives its cardinality \(p^{m-e}\).
124 
125 When \(m=e\), the new solved-Jacobian definition is definitionally the
126 existing square block used by the checked continuous parameter chart.
127 Every root in the initial ball with the given parameters is that chart
128 point. Applying this to any two roots proves equality, including
129 endpoints obtained by different constructions.
130 
131 \hypertarget{cont9:scope-controls}{%
132 \subsubsection{Scope controls}\label{cont9:scope-controls}}
133 
134 The inherited checked example \(F(Y,T)=T\), \(p=2\), \(x=0\), \(L=1\)
135 has a surjective full Jacobian but zero solved block. Prescribing
136 parameter digit \(1\) forces \(T=2\pmod4\), so no next root exists.
137 Full-Jacobian surjectivity cannot replace the hypothesis on the
138 prescribed solved block.
139 
140 The new checked example \(F(Y_1,Y_2,T)=Y_1\) has a surjective solved
141 block \((1,0)\). Nevertheless \((0,0,0)\) and \((0,2,0)\) are distinct
142 exact roots in the same modulo-two ball with identical parameters.
143 Uniqueness therefore requires the square solved case. The corresponding
144 negative control deliberately attempts the stronger false conclusion and
145 must be rejected by Lean.
146 
147 Depth \(L\ge1\) is essential for the Taylor step used here. The general
148 singular case can have a nonzero next obstruction after an earlier zero
149 obstruction. Neither the finite one-step criterion nor this smooth
150 theorem establishes unrestricted singular persistence.

Back to source controls

Back to Realization Calculus