Beal: source and evidence

Download original file

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

Read the typeset paper

1 \section{What the evidence checks}\label{sec:evidence}
2 The source and evidence archive separates original recovered payloads, fresh computational records, formal sources and logs, literature leaves, and the new publication sources. This makes it possible to check a claim against the kind of evidence that actually supports it.
3 
4 \subsection{Exact finite arithmetic}
5 The final Block 80 assertions were replayed in the current session, including the immediate Block 79 predecessor. Primary and separate programs agree on their full scientific records. Their field bases, norms, self conductor unit calculations, and rank certificates differ. The final scope includes 592 residue symbol evaluations per arithmetic implementation, seven direct self uniformizer checks, sixteen rank minor certificates, 12\,348 Frobenius lift identity cases, and 12\,348 fixed primitive identity cases. The evaluator exercises eighty four image and nonimage targets, forty origin changes, and sixteen malformed inputs. A separate synthetic image family contains 560 tests.
6 
7 The additional audit independently checks twenty matrices by exact prime field ranks and integer minors, all 2401 products across the two quadratic field bases, 2940 basis field targets, 1960 image reconstructions, 1960 origin changes, thirty six invalid scalar encodings, and three symbolic identities. These numbers describe their declared finite domains. They are not independent arithmetic targets or Galois realizations.
8 
9 Selected historical computations also have fresh replay records. The portable scientific replays for Blocks 67 through 80 all passed at their unchanged documented bounds. Their precise source pins, options, output comparisons, resource limits, and failures are recorded in the computation report. The existence of many nested archives is not a claim that every historical wrapper was freshly run to completion. Where a portable scientific runner is used, its result is distinguished from the original packaging wrapper.
10 
11 Two current failures deserve an explicit place in the reader. The archival Block 69 wrapper reached an aggregate 840 second resource timeout without a completed certificate. That attempt is inconclusive, not a mathematical exclusion or a passed replay. Its separate portable scientific run subsequently passed and matched all seventeen result JSONs at the unchanged bounds. The unchanged original Block 67 verifier completed with status \texttt{PASS} and exit zero, comparing its eight scientific outputs and rejecting nine corruptions. A new generic wrapper then incorrectly required the different status string \texttt{PASS\_DECLARED\_CHECKS} and rejected that successful outcome. The failed wrapper record is retained. A separate pinned interpretation check identifies the actual original process result without overwriting it, and the portable scientific replay independently passed. The correction is in interpreting the current wrapper, not in silently repairing historical source bytes.
12 
13 The audit also found a legacy Block 71 display metadata error. One primary record said the unit domain modulo $49$ contained 2304 elements, but its loop checks $49^2-7^2=2352$ units. The independent record already reports 2352. The mod seventh power quotient size forty nine and its forty eight element fibers are unchanged. The original record is preserved, while the corrected domain count is stated here.
14 
15 Other failures remain visible in the history. Block 70 originally required beta itself to vanish in a bad alternative, instead of requiring both trace products to vanish. The rejected source and outputs are retained. Block 80 initially used a too strong full primitive residue generator requirement, although only a generator of the seventh power quotient was needed. A wrapper syntax failure stopped another attempt. Corrected executions have separate successful records.
16 
17 No actual affine target is authenticated by any finite test in this release. Exactly zero residual patterns are excluded by the final affine calculation. The finite ranks describe the operator, and the synthetic cases verify its evaluator.
18 
19 \subsection{The formal layer}
20 Forty named public Lean statements have fresh successful checks in three scopes. The original Block 47 has twenty one statements: seven generic lane certificate results, five Boolean correlation results, and nine exact mod seven polynomial or matrix identities. The original Block 48 has eight characteristic seven algebra and elementary bounded dimension statements. These unchanged historical sources were checked with Lean 4.34.0-rc2 and their exact mathlib revision. The Block 47 project module also passed its separate kernel replay, with three deliberately invalid controls rejected.
21 
22 The new reader module has eleven statements checked with Lean 4.19.0 and its exact mathlib revision. They prove ordinary differential additivity, primitive difference additivity, preservation under adding a character, the explicit fixed primitive differential and trace identity, affine solvability translation, cokernel origin invariance, a necessary null test, the complete null criterion under its explicit completeness hypothesis, and the kernel translate description of a fiber. They passed strict elaboration and axiom inspection. No separate optional checker binary is claimed for this new module.
23 
24 The successful axiom reports use only subsets of Lean's standard extensionality, classical choice, and quotient axioms, with no admitted proof or custom axiom. Failed import, API, runtime layout, and resource attempts are retained separately. They are not included in the forty passed statement count.
25 
26 The formal sources do not encode finite set Poitou--Tate duality, the actual Galois group, continuity of a primitive, the fifteen by ten arithmetic matrix, its full null basis, or the arithmetic target. Generic exclusion statements explicitly assume a complete lane cover and sound attachment to one fixed candidate. Compilation proves those implications. It does not supply their Diophantine instantiation.
27 
28 \subsection{Written proofs and independent scope review}
29 The reader supplies complete elementary proofs for the exponent reduction, valuation scaling, local squareclass criterion, depth matrix relation, discriminant collapse, period torsion equivalence, restricted unit kernel, fixed local primitive, and affine obstruction criterion. External applications retain their named source hypotheses. A separate internal reviewer checked the new proof text and its load bearing boundaries. This is useful adversarial review of the stated arguments, not independent human peer review or a certificate for every historical analytic geometric input.
30 
31 The final target remains mathematical rather than editorial. A defining arithmetic origin or equivalent duality calculation must evaluate $[t(p_0)]\in\coker A$. Successful linear algebra cannot replace this missing input. After a compatible first primitive is obtained, the prescribed upper geometry and higher integral realization remain to be solved. Broader conductors, higher depths, the minus component, other modular branches, and other signatures require their own exhaustive coverage.

Back to source controls

Back to Beal: source and evidence