ABC: source and evidence reader

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

1 \section{Finite evidence, formal checks and reproducibility}\label{sec:evidence}
2 \subsection{The recovered sources and the new reader edition}
3 The immediate predecessor is the verified prime contact coherence publication from July 2026. Its rendered final edition has 142 pages. The larger complete historical source and the later 19 September jet determinant block are also recovered. Original archives remain unchanged. The new edition rearranges their proof spine, adds the conjecture foundations and spectral leaf treatment, incorporates the corrected normalization, and explicitly revises issues found in the current independent audit.
4 
5 The source and evidence package records input hashes, executable commands, outputs, audit notes and the new figure data. It distinguishes historical verification records from fresh runs. A prior report is evidence about its stated historical process, rather than a fresh certificate for every sentence of this edition.
6 
7 \subsection{Fresh exact computations}
8 The September jet verifier was replayed unchanged. Its scientific output matched the archive: 149,306 assertion evaluations, including 504 exact modular determinant valuation comparisons. These are evaluation counts, not numbers of independent theorems.
9 
10 \begin{center}
11 \begin{tabularx}{\linewidth}{@{}p{0.29\linewidth}X@{}}
12 \toprule
13 Jet test family & Declared finite range\\
14 \midrule
15 Coefficient cancellation & $m=0,\ldots,30$, indices $k=1,\ldots,80$\\
16 Finite Cauchy--Binet & Ranks $1,\ldots,5$, $K=r,\ldots,r+4$, arguments $1/3,2/3,-1/2$\\
17 Residue energy minimum & Primes $2,3,5,7$, ranks through six, subsets of the first eleven unit indices\\
18 Depleted valuations & Primes through seventeen in the selected seven-prime list, ranks through eight, $e=1,2,3$, three unit choices\\
19 Denominator budget & Ranks through eight, ordered indices through three hundred, plus rational determinant checks\\
20 Stored triangle rows & All 361 stored moduli and phase rows\\
21 \bottomrule
22 \end{tabularx}
23 \end{center}
24 The stored triangle replay checks its retained finite identities. It does not reconstruct every upstream phase from a primitive triple. The general theorems in the determinant chapters are proved in the text, rather than inferred from these bounded ranges.
25 
26 The unchanged canonical mathematical audit reproduced all seven archived output groups. Its phase Smith check covered 152,095 nondegenerate primitive triples with $a\le b$ and $c\le1000$. It also checked 195 polyphase cases, 2,499 seeded Wronskian packets, 5,001 divisor-packet examples, 391 Kummer examples and 254 diagonal Walsh packets. The Wronskian packets are sampling, and the Walsh model is an algebraic diagonal model, rather than an automorphic construction.
27 
28 The nine canonical implementation groups also reproduced their archived values, after two disclosed filesystem path adaptations. The mathematical code was unchanged. At $3+125=128$, the weighted derivative minimum is $\Theta=6$, while the exponent-free moving-search minimum is $\Phi=8$. They optimize different packets. The latter has obstruction multiple one and exact master gap one. At $1+4374=4375$, the moving-search minimum is 62 and its exact master gap is $248/243$.
29 
30 Some implementation companion checks are numerical. The polylogarithm residuals use eighty-digit arithmetic and fixed tolerances, without certified interval error bounds. They are reproduced numerical support. They are kept separate from exact integer, rational, modular and symbolic identities.
31 
32 \subsection{An independent primitive census}
33 A new exact enumeration covered every primitive positive triple with $a\le b$ and $2\le c\le10000$. It contains 15,198,743 triples. A separate Euler totient sieve gives the same count. Exactly 121 satisfy $c>R$, with membership decided by the integer inequality rather than a floating quality threshold.
34 
35 Within that declared domain, the largest displayed quality is approximately $1.567887$ at $1+4374=4375$, with $R=210$. The example $2+109\cdot3^{10}=23^5$ lies outside the census. This computation supplies neither a uniform conjectural constant nor a conclusion about unsearched triples.
36 
37 \subsection{Two controls on delicate local boundaries}
38 The CRT lift criterion was checked against complete finite brute force in 2,928 cases. Every individual coordinate interval must be nonempty. The sum-of-endpoints condition alone can incorrectly accept a target when one coordinate interval is empty. The preserved implementation already had the individual guard. The new theorem statement now includes it.
39 
40 The strict good-prime boundary was also tested with justified infinite-series tails. For rank two and $p=5=3r-1$, the raw determinant at $t=10$ has valuation four, while its depleted version has valuation three. For $p=7$ and $t=14$, both have valuation three. The modular precision levels were 6, 8, 12 and 16. The tail bounds in the computation report authenticate these named valuations. Thus the strict condition $p>3r-1$ cannot be weakened to equality in the universal exact-valuation theorem.
41 
42 At a small prime, a raw lower bound can even coexist with zero. For rank one at $p=2,t=2$, the standard convergent logarithm identity gives $\Li_1(2)=-\log_2(-1)=0$. Finite zero residues support this identity but do not prove it by themselves. The depleted moment at that argument has valuation one. This is why the all-prime budget theorem explicitly uses $v_p(0)=+\infty$ and does not promise raw nonvanishing at every small prime.
43 
44 \subsection{What the seven jet scripts actually formalize}
45 The original jet file has now been built with its exact Lean 4.19.0 and mathlib v4.19.0 versions. All seven theorem axiom checks passed. Its original source produces two style-linter warnings, so a warning-as-error elaboration fails. A separately preserved checked copy changes only the two tactic separators from \texttt{<;>} to \texttt{;}. That copy builds and elaborates with warnings treated as errors. The statements, coefficients, quantified domains and imported library are unchanged.
46 
47 The seven statements cover rational cancellation of the balanced factor, two-node and three-node polynomial Gram identities, a rank-two finite truncation formula, its cleared rational expression, its integer remainder and a rational coordinate change. Their standard logical axiom dependencies are recorded individually. There is no custom axiom or unfinished proof in the inspected outputs.
48 
49 These scripts do not formalize convergence, general infinite Hankel determinants, positivity, the all-rank valuation theorem, the residue-class minimum proof or the global $abc$ criterion. The Gram identities alone have no positivity hypotheses. The integer remainder identity is a polynomial equality, rather than a completed prime-divisibility theorem. The formal scope is finite algebra, distinct from the written analytic and arithmetic proofs.
50 
51 \subsection{The separate checked KTG interface}
52 The recovered KTG Block 03 is a different development with a different source history. Its exact Lean 4.34.0-rc2 clean replay passed all 24 build jobs and all 22 direct source elaborations with warnings treated as errors. A fresh axiom inspection covered 42 named theorems. Forty-one use no axioms, and one generic logical independence theorem uses the standard proposition-extensionality axiom.
53 
54 Its proved theorem is conditional. Given abstract typed data, realization and normalization certificates, a supplied witness-preservation theorem and a monotone observable, a hull containment yields the scalar observable bound. The source witness for an actual IUT instantiation is still missing. A finite Boolean model demonstrates that the earlier abstract fields do not logically imply the missing containment. That is an independence result inside the defined interface, rather than a counterexample to IUT or $abc$.
55 
56 Separate type fields distinguish roles but do not require pairwise unequal types. Its positive natural-number rank field does not enforce rank greater than one. Its grade-transfer equations check the chosen abstract definitions, rather than authenticate their interpretation as actual IUT log-volume or normalization objects. Those interpretation obligations remain mathematical work outside compilation.
57 
58 \subsection{Failures are part of the evidence}
59 The historical jet verifier first encountered a float at the rank-one empty product. The exact identity test detected it, and the accepted historical implementation corrected it. The latest replay uses the corrected exact source. The false unbalanced $Q$ target and the failed rational witness are mathematical corrections retained as explicit theorems.
60 
61 Current source review also corrected the missing CRT nonemptiness condition, unit-sector definitions, model and branch qualifications, and one draft jet coefficient. The runtime recovery had host-specific compiler startup and extraction failures, corrected by a disclosed compatibility layer for the process's own executable-path lookup. Compiler and proof bytes were unchanged. The exact commands, logs, changes and hashes are preserved in the evidence report.
62 
63 None of these successful finite or formal checks supplies the global arithmetic realization. The final missing implication remains the one stated in Section~\ref{sec:bridge}.

Back to source controls

Back to ABC: source and evidence reader