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{Fresh verification and its exact scope}\label{sec:verification}
2 All computations in this section are fresh replay evidence for this final companion edition. Original checkpoint outputs remain archived as historical evidence and are not relabeled as fresh runs. The evidence directories contain their input/source hashes, commands, exact assertions and controls. Runtime variations do not change a mathematical statement.
3 
4 \subsection{Current integer Lean core}
5 The freshly checked current v0.14 block has 25 theorem declarations: 14 inherited unchanged from the principal-divisor block and 11 cubic-growth coefficient theorems. The fresh one-worker compilation treats warnings as errors. All 25 transitive axiom audits allow only the standard dependencies \texttt{propext}, \texttt{Classical.choice} and \texttt{Quot.sound}; no \texttt{sorryAx} or custom axioms occur. The false control is rejected. The precise inventory is in the separate Lean guide and \texttt{lean/verification/current/BUILD\_AUDIT.json}.
6 
7 These declarations concern triples of integers, ceiling/digit algebra, smoothing weights, bounded coefficient values and family identities. They do not formalize complex orders, local finiteness, cubic analytic counting, Jensen's theorem, normal convergence, canonical products, fourth-log differentiation, the cubic-exponential reconstruction, gamma arithmetic or a class-field identification.
8 
9 \begin{longtable}{p{.28\linewidth}p{.29\linewidth}p{.35\linewidth}}
10 \toprule Manuscript claim & Formal consequence checked & Ordinary input outside that consequence\\\midrule\endhead
11 Theorem~\ref{thm:complete-divisor} & Integer lift, ceiling carry and signed coefficient identity & Product zeros/poles and divisor interpretation\\
12 Coefficient values $\{-4,-1,0,1,4\}$ & Universal step-function and smoothing-weight bound & Identification with complex orders\\
13 Theorem~\ref{thm:cubic-growth} families & Integer chamber, congruence and weight values & Complex parameter injection, radius estimates and infinite counting\\
14 Theorem~\ref{thm:regularizer} & No current analytic formalization & Absolute sums, normal convergence and divisor products\\
15 Theorems~\ref{thm:reconstruction}, \ref{thm:cube} & Exact symbolic finite exponent controls support replay & Ordinary complex logarithms, differentiation and infinite products\\
16 Equation~\eqref{eq:remaining-reality} & Not proved & Exact gamma arithmetic/phase comparison remains open\\\bottomrule
17 \end{longtable}
18 The deduplicated inherited selection contains 42 mathematical modules and 453 distinct theorem declarations. Fresh complete type and transitive-axiom checks cover every declaration: 438 module audits, eight focused CM-norm audits and seven exact-source-prefix phase-regulator audits. The only dependencies are the same three standard axioms, with no \texttt{sorryAx} or custom axioms. The single all-import/combined process remains incomplete under the three-gigabyte memory limit; the independent module/declaration checks are complete. The current 25-declaration subset is also checked separately. This distinction is recorded in the Lean companion and its ledger; the inherited coverage must not be described as a successful combined process.
19 
20 \subsection{Exact and numerical replay}
21 The current exact checker passes 20 named assertions with five negative controls. Its finite lift range contains 2,197 triples, and its family run checks 92,480 points for $1\le n\le16$. A separate finite extension passes nine named checks and four controls over 4,913 triples, 15,125 family points for $1\le n\le10$, 135 actual complex positions at $n=3$ and three exact polynomial samples.
22 
23 At requested precisions 40 and 70 decimal digits (65 and 95 actual working digits, including 25 guards) the current numerical replay checks four reflection/anchor identities, one quadratic-jet diagnostic and three negative controls. The maximum identity errors are approximately $1.9204\times10^{-62}$ and $1.2792\times10^{-92}$. The finite-difference jet residual is approximately $3.9284\times10^{-11}$ at both precisions: its fixed step causes a truncation residual, so it is a diagnostic rather than an exact identity proof. The independent extension checks 15 floating identities at 80 working digits, with maximum error approximately $2.1231\times10^{-72}$.
24 
25 These floating calculations are not directed interval certificates. They evaluate neither the full infinite divisor product nor an exact gamma/class-field equality. Finite equality checks and negative controls can detect implementation and transcription errors within their tested ranges; the universal conclusions rest on the ordinary proofs.
26 
27 \subsection{Authoring and proofread boundary}
28 The source originals are preserved. Mathematical prose from the proper-TeX theta, modulus and polarization sources is integrated with prefixed local equation numbers. The assembler protects mathematical spans before converting prose citations and compares every such span after only declared notation substitutions. The plaintext principal-divisor and reconstruction formulas are manually typeset and separately checked against the originals; their audit is recorded independently rather than being called an unchanged-token copy.
29 
30 During authoring, the first citation transformation attempted to replace the mathematical torsion notation $E_t[2]$ by a citation. The mathematical-token guard rejected this draft before it entered the manuscript. Protecting display and inline math before prose transformations corrected the conversion. This failure and fix are retained in the scoped proofread report. No mathematical assertion is inferred from a rejected authoring draft.
31 
32 The final proofread audit distinguishes conservative typography from deliberate notation namespacing, the scoped finite-theta grammar, and ordinary proof dependencies. PDF checks inspect the actual final rendered pages. Layout validation and finite computation do not convert unformalized analytic arguments into Lean theorems.

Back to source controls

Back to Hilbert 12: cubic divisor development