Hilbert 12: cubic divisor development

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 polarized algebraic phase target}\label{sec:polarization}
2 \noindent\textit{Source anchor Q: preserved mathematical development; exact source path and hash are in the claim/source inventory. Retained local equation numbers carry this prefix.}\par
3 \noindent\textit{Numerical intervals and decimal diagnostics in this source-derived arithmetic section are retained historical checkpoint evidence; they are not the fresh v0.14 replay and are not newly certified by this edition.}\par
4 \hypertarget{Q-fixed-field-branch-and-distinct-involutions}{%
5 \subsection{Fixed field, branch, and distinct
6 involutions}\label{Q-fixed-field-branch-and-distinct-involutions}}
7 
8 Let
9 
10 \[
11  \omega^2+\omega+1=0,\quad J=2+3\omega,\quad
12  \beta^3=7,\quad \xi^3=J.
13 \]
14 
15 Use the fixed embedding \(\omega=e^{2\pi i/3}\),
16 \(\beta=7^{1/3}\omega^2\), and the retained Gauss branch
17 
18 \[
19  \xi=\beta^{-1}\sum_{k=1}^6\chi_7(k)e^{6\pi i k/7},
20  \qquad (\chi_7(1),\ldots,\chi_7(6))=(1,\omega,\omega^2,\omega^2,\omega,1).
21 \]
22 
23 The inherited arithmetic construction identifies
24 
25 \[
26  E=\mathbb Q(\omega,\beta,\xi),\quad F_0=\mathbb Q(\omega),
27  \qquad \operatorname{Gal}(E/F_0)=C_3^2.
28 \]
29 
30 The actual arithmetic candidate \(U=U_{\rm alg}\) is defined by the
31 retained rational formulas in \nolinkurl{prior/ARITHMETIC_INPUT.md}. This
32 block starts from those formulas. No gamma value is used to find or fit
33 coefficients.
34 
35 Define the three CM units
36 
37 \[
38  a_0=(1+\omega)\xi^2-\xi+1,\quad
39  a_1=-\xi^2+(1+\omega)\xi+1,\quad
40  a_2=-\omega\xi^2-\omega\xi+1.
41 \]
42 
43 They satisfy
44 
45 \[
46  a_0a_1a_2=1,\qquad a_j^3-3a_j^2+6\omega a_j-1=0.
47 \]
48 
49 Write
50 
51 \[
52  \epsilon_j=2-\omega^j\beta,\qquad \epsilon=\epsilon_0,
53  \qquad \epsilon_0\epsilon_1\epsilon_2=1.
54 \]
55 
56 In the fixed embedding \(\epsilon_1=2-7^{1/3}>0\), and
57 \(\epsilon_2=\overline\epsilon\).
58 
59 Two involutions must remain distinct:
60 
61 \[
62  \iota(\beta)=\beta,\quad \iota(\omega)=\omega^2,\quad \iota(\xi)=\beta/\xi,
63 \]
64 
65 whereas actual complex conjugation \(\kappa\) is
66 
67 \[
68  \kappa(\beta)=\omega^2\beta,\quad \kappa(\omega)=\omega^2,
69  \quad \kappa(\xi)=\omega\beta/\xi.
70 \]
71 
72 Direct substitution gives the useful index relation
73 
74 \[
75  \boxed{\kappa(a_j)=\iota(a_{j+1})},\qquad j\pmod3. \tag{Q1}
76 \]
77 
78 All displayed algebraic identities are checked in an 18-dimensional
79 rational quotient implementation. Construction of \(U\), the cubic
80 coordinate, and the \(a_j\) is also independently repeated by SymPy
81 Groebner reduction over \(\mathbb Q\).
82 
83 \hypertarget{Q-exact-reconstruction-from-four-cubic-subfield-norms}{%
84 \subsection{Exact reconstruction from four cubic-subfield
85 norms}\label{Q-exact-reconstruction-from-four-cubic-subfield-norms}}
86 
87 Let \(\gamma_{ij}\) fix \(\omega\) and send
88 
89 \[
90  \beta\mapsto\omega^i\beta,\qquad \xi\mapsto\omega^j\xi.
91 \]
92 
93 There are four order-three subgroups of \(C_3^2\), generated by
94 
95 \[
96  (1,0),\ (0,1),\ (1,1),\ (1,2).
97 \]
98 
99 Every nonidentity group element lies in exactly one of these four
100 subgroups; the identity lies in all four. Hence, for any nonzero
101 \(z\in E\),
102 
103 \[
104  \boxed{
105  \prod_{H\text{ a line}}N_{E/E^H}(z)
106    =z^3N_{E/F_0}(z).
107  } \tag{Q2}
108 \]
109 
110 This is a multiplicative incidence identity, not a theorem asserting an
111 analytic Artin action. The finite algebra is compiled in
112 \texttt{H12LineNorms} over a commutative ring, with its field division
113 corollary under the explicit nonzero norm hypothesis.
114 
115 Put
116 
117 \[
118  \mathcal A=a_0a_1^3=\frac{a_1^2}{a_2},\qquad
119  \mathcal B=a_0^2a_1^4=\left(\frac{a_1}{a_2}\right)^2.
120 \]
121 
122 For the actual \(U\), exact field arithmetic gives:
123 
124 \begin{longtable}[]{@{}lll@{}}
125 \toprule\noalign{}
126 Line generator & Fixed field & Norm of U \\
127 \midrule\noalign{}
128 \endhead
129 \bottomrule\noalign{}
130 \endlastfoot
131 (1,0) & \(F_0(\xi)\) & \(\omega\mathcal A\) \\
132 (0,1) & \(F_0(\beta)\) & \(\omega\epsilon_2/\epsilon_1\) \\
133 (1,1) & \(F_0(\beta/\xi)\) & \(\omega/\iota(\mathcal A)\) \\
134 (1,2) & \(F_0(\beta\xi)\) & \(\omega\) \\\
135 \end{longtable}
136 
137 Also \(N_{E/F_0}(U)=1\). Thus (Q2) proves
138 
139 \[
140  \boxed{
141  U_{\rm alg}^3=\omega\frac{\epsilon_2}{\epsilon_1}
142                  \frac{\mathcal A}{\iota(\mathcal A)}.
143  } \tag{Q3}
144 \]
145 
146 The same calculation for the inherited pre-smoothing unit \(W\) gives
147 line norms
148 
149 \[
150  -\mathcal B,\quad -\epsilon_2/\epsilon_1,\quad
151  -1/\iota(\mathcal B),\quad -1,
152 \]
153 
154 and total norm \(-1\). Consequently
155 
156 \[
157  \boxed{W^3=-\frac{\epsilon_2}{\epsilon_1}
158                    \frac{\mathcal B}{\iota(\mathcal B)}.} \tag{Q4}
159 \]
160 
161 The minus sign comes from division by the total norm and must be
162 retained.
163 
164 \hypertarget{Q-a-direct-lean-certificate-for-q3}{%
165 \subsubsection{A direct Lean certificate for
166 (Q3)}\label{Q-a-direct-lean-certificate-for-q3}}
167 
168 The normalized polynomial \(U_{21}(\beta,\xi,\omega)=21U\) is explicitly
169 defined in \texttt{H12CMNormCertificate.lean}. It is the normal form of
170 the inherited candidate, as checked in both rational implementations.
171 Also
172 
173 \[
174  \mathcal A=4(1+\omega)\xi^2-(6\omega+4)\xi+1,
175 \]
176 
177 \[
178  7\iota(\mathcal A)
179  =-8\beta^2\omega\xi-12\beta^2\xi
180     +6\beta\omega\xi^2+16\beta\xi^2+7.
181 \]
182 
183 Lean proves the denominator-free relation
184 
185 \[
186  U_{21}^3(2-\omega\beta)(7\iota\mathcal A)
187  =64827\,\omega[2+(1+\omega)\beta]\mathcal A,
188 \]
189 
190 using only \(\beta^3=7\), \(\xi^3=2+3\omega\), and
191 \(\omega^2+\omega+1=0\). Here \(64827=21^3\cdot7\). Five small
192 polynomial reductions replace one resource-heavy monolithic certificate.
193 The field corollary gives (Q3) with explicit nonzero denominator
194 hypotheses.
195 
196 The geometric field interpretation and the conversion from the original
197 rational Gauss formula to \(U_{21}\) are not silently assumed as axioms
198 in Lean: the formal statement is about that explicit polynomial
199 presentation, while the conversion is verified by the two separate exact
200 arithmetic implementations.
201 
202 \hypertarget{Q-polarization-recovers-the-full-algebraic-phase}{%
203 \subsection{Polarization recovers the full algebraic
204 phase}\label{Q-polarization-recovers-the-full-algebraic-phase}}
205 
206 By (Q1),
207 
208 \[
209  \iota(\mathcal A)=\frac{\kappa(a_0)^2}{\kappa(a_1)},
210 \]
211 
212 and \(a_0a_1a_2=1\) therefore gives
213 
214 \[
215  \frac{\mathcal A}{\iota\mathcal A}
216   =\frac{a_1^2\overline{a_1}^{\,3}\overline{a_2}^{\,2}}{a_2}.
217 \]
218 
219 Moreover \(\epsilon_2/\epsilon_1=\epsilon\overline\epsilon^{\,2}\).
220 Equation (Q3) becomes
221 
222 \[
223  U_{\rm alg}^3=
224  \omega\epsilon\overline\epsilon^{\,2}
225  \frac{a_1^2\overline{a_1}^{\,3}\overline{a_2}^{\,2}}{a_2}. \tag{Q5}
226 \]
227 
228 Define the explicit nonzero algebraic factor
229 
230 \[
231  \boxed{C=\frac{\epsilon a_1a_2^3}{\omega}}
232 \]
233 
234 and the positive real algebraic number
235 
236 \[
237  R_+=|\epsilon|^4|a_1|^6|a_2|^4.
238 \]
239 
240 Multiplication of (Q5) gives the exact phase theorem
241 
242 \[
243  \boxed{C U_{\rm alg}^3=R_+>0.} \tag{Q6}
244 \]
245 
246 The positivity uses actual complex conjugation, not \(\iota\). The
247 polynomial factor rearrangement and positivity implication are checked
248 in Lean, with their hypotheses exposed.
249 
250 Numerically,
251 
252 \[
253  C\approx13.80641265880838653-46.68563220754137422i,
254 \]
255 
256 \[
257  R_+\approx3619549.58981670163340845644692077486836844.
258 \]
259 
260 These decimals illustrate the exact identities; they are not their
261 proof.
262 
263 \hypertarget{Q-why-the-naive-complex-lift-of-the-modulus-is-false}{%
264 \subsection{Why the naive complex lift of the modulus is
265 false}\label{Q-why-the-naive-complex-lift-of-the-modulus-is-false}}
266 
267 The retained Stark calculation gives
268 
269 \[
270  |U_\Gamma|^3=|\epsilon^3a_2a_1^5|.
271 \]
272 
273 Deleting absolute-value signs would assert a false identity even for
274 \(U_{\rm alg}\). In fact
275 
276 \[
277  \boxed{
278  \frac{U_{\rm alg}^3}{\epsilon^3a_2a_1^5}
279  =\omega\left(\frac{\overline\epsilon}{\epsilon}\right)^2
280        \left(\frac{\overline{a_1}}{a_1}\right)^3
281        \left(\frac{\overline{a_2}}{a_2}\right)^2.
282  } \tag{Q7}
283 \]
284 
285 The right side has modulus one but is not in \(\mu_6\): the rational
286 quotient calculation proves its sixth power differs from one. Its value
287 is approximately
288 
289 \[
290  0.2625544763772951843-0.9649171710225931849i.
291 \]
292 
293 We do not claim here that it is not a root of unity of any order. The
294 verified negative statement is precisely that it is not a sixth root of
295 unity. This correction is different from the still-unidentified
296 discrepancy \(U_\Gamma/U_{\rm alg}\).
297 
298 \hypertarget{Q-the-remaining-gamma-theorem-can-be-a-reality-theorem}{%
299 \subsection{The remaining gamma theorem can be a reality
300 theorem}\label{Q-the-remaining-gamma-theorem-can-be-a-reality-theorem}}
301 
302 Use the inherited exact modulus theorem \(|U_\Gamma|=|U_{\rm alg}|\). It
303 is not re-proved in the corresponding source checkpoint. From (Q6),
304 
305 \[
306  |C U_\Gamma^3|=R_+.
307 \]
308 
309 The retained historical directed-interval calculation reported
310 
311 \[
312  3.6\cdot10^6<\Re(C U_\Gamma^3)<3.7\cdot10^6.
313 \]
314 
315 Therefore the single still-unproved assertion
316 
317 \[
318  \boxed{\Im(C U_\Gamma^3)=0} \tag{Q8}
319 \]
320 
321 would imply \(C U_\Gamma^3=R_+\), then \(U_\Gamma^3=U_{\rm alg}^3\). The
322 retained historical checkpoint distance bound \(|U_\Gamma/U_{\rm alg}-1|<1/2\)
323 would select \(U_\Gamma=U_{\rm alg}\).
324 
325 \texttt{H12PolarizedReality.normalized\_reality\_with\_branch} proves
326 this implication in Lean. Exact reality, modulus equality, nonzero
327 factors, positive real parts, and the branch enclosure are separate
328 visible hypotheses. The function does not manufacture (Q8).
329 
330 Equivalently, the missing phase condition is
331 
332 \[
333  \overline{C U_\Gamma^3}=C U_\Gamma^3,
334  \qquad
335  \left(\frac{U_\Gamma}{\overline{U_\Gamma}}\right)^3
336    =\frac{\overline C}{C}. \tag{Q9}
337 \]
338 
339 This singles out a conjugation-sensitive comparison, rather than
340 suggesting that ordinary norms by themselves recover phase.
341 
342 \hypertarget{Q-a-conjugate-chart-version-of-the-next-target}{%
343 \subsubsection{A conjugate-chart version of the next
344 target}\label{Q-a-conjugate-chart-version-of-the-next-target}}
345 
346 From the defining product and its continuation,
347 
348 \[
349  \overline{F_{t,s}(z)}=F_{-\bar t,-\bar s}(-\bar z).
350 \]
351 
352 At the actual thirds, the inherited inversion identity gives
353 
354 \[
355  F_{-\bar t,-\bar s}(1/3)=\overline{U_\Gamma}^{\,-1}.
356 \]
357 
358 Thus (Q9) is equivalently a prescribed value for the cube of the product
359 of the gamma special values in the original and conjugate charts. No
360 Artin action on gamma values is assumed. Establishing that complex
361 transport identity remains an open route, not an executed proof in the
362 corresponding source checkpoint.

Back to source controls

Back to Hilbert 12: cubic divisor development