FORMAL_STATUS.md
Beal: source and evidence
FORMAL_STATUS.md
1 # Beal formal evidence
2
3 **Final check report, 8 October 2026, America/Chicago.** The original Block 47
4 and Block 48 sources passed a fresh check under their exact compiler and library
5 pins. A new eleven-statement module passed strict source elaboration and axiom
6 inspection for the ordinary cochain and affine linear algebra used in the reader.
7
8 ## Result and distinct scopes
9
10 | Development | Exact pin used in the successful current run | Public statements checked | Fresh result |
11 |---|---|---:|---|
12 | Block 47 | Lean 4.34.0-rc2, mathlib `aeb72f1e9981b6d35b426b16dca7759be3e7ba06` | 21 | Unchanged verifier passed strict compilation, all axiom reports, project-only kernel replay and three expected rejected negative controls |
13 | Block 48 | The same Lean and mathlib pins | 8 | Unchanged source passed direct warning-as-error elaboration and all eight axiom reports |
14 | Reader affine module | Lean 4.19.0, mathlib `c44e0c8ee63ca166450922a373c7409c5d26b00b` | 11 | Final minimal-import source passed warning-as-error elaboration and all eleven axiom reports |
15
16 These are forty named public statements in three scopes. The counts exclude the
17 Block 48 private helper and the intentionally invalid negative controls. They
18 are not forty proofs of the Beal conjecture or forty arithmetic realizations.
19 No successful current axiom report contains `sorryAx` or a custom axiom. The
20 dependencies are subsets of Lean's standard `propext`, `Classical.choice` and
21 `Quot.sound`.
22
23 ## Historical source authentication and replay
24
25 All four Block 47 source hashes match the archived verification report. The
26 Block 48 source hash matches its archived result. The recovered files and the
27 historical compiler logs are preserved unchanged. Source authentication is
28 recorded in `formal/HISTORICAL_INPUT_AUTHENTICATION.json`.
29
30 The historical Block 47 compiler is Lean 4.34.0-rc2 at commit
31 `6a10ac8c22beadecabdbb0919c2b50214762f91d`. Its compiler binary was reused from
32 the preceding ABC check without modification. The exact historical mathlib
33 checkout was freshly fetched at
34 `aeb72f1e9981b6d35b426b16dca7759be3e7ba06`. Its official cache downloader
35 completed successfully and downloaded 8,849 cache objects. Fresh dependency
36 checks matched every declared revision in both environments. All checked tracked
37 package sources were clean. The eighteen dependency records, compiler hashes,
38 and acquisition records are in `formal/RUNTIME_DEPENDENCY_AUTHENTICATION.json`
39 and the mathlib acquisition and cache logs.
40
41 The original `verify_block47.py` was copied unchanged to a private working
42 project. All four original sources compiled with warnings treated as errors.
43 The source scan found no admitted proof, custom axiom, unsafe declaration or
44 `native_decide`. All twenty-one requested theorem axiom reports appeared and
45 used only the three standard axioms listed above.
46
47 The verifier assembled its original replay module and compiled it. The exact
48 `leanchecker` then replayed only `Beal47Replay`, as requested. Imported pinned
49 mathlib objects remain trusted in the ordinary workflow. This is a separate
50 check of the project module, not a rebuild or independent verification of every
51 mathlib dependency.
52
53 All three deliberate negative controls were rejected for their expected reasons:
54 an invalid single-candidate choice across two tests, a false off-diagonal
55 coefficient cancellation, and a placeholder proof under warning-as-error
56 settings. The placeholder is a negative-control input and is never counted as
57 a proved theorem.
58
59 Block 48's unchanged source separately compiled with one Lean worker and strict
60 warnings. All eight public axiom reports appeared, with no nonstandard axiom
61 dependency. The source bytes before and after both successful checks matched
62 the recovered originals. The final current run is
63 `formal/historical_exact_run02`.
64
65 ## What the historical statements establish
66
67 Block 47 has seven generic lane-certificate statements, five finite Boolean
68 correlation statements and nine exact mod-seven polynomial or matrix statements.
69 The generic exclusion implication explicitly assumes a complete lane cover,
70 an attachment of a globally fixed candidate and soundness of each selected test.
71 Compilation proves the implication with those hypotheses. It does not supply
72 their arithmetic instantiation.
73
74 The polynomial module checks the cube of the displayed sextic over `ZMod 7`,
75 four coefficient positions, their determinant expression, the assembled
76 two-by-two matrix and its square. The module documentation explicitly leaves
77 the identification of that coefficient matrix with a geometric Cartier operator
78 outside the formalization.
79
80 Block 48 proves common-root and trace exclusions over any characteristic-seven
81 field. It also proves the elementary bounded natural-number statement that
82 `d₀,d₁ ≤ 2` and `(d₀+7*d₁) mod 48 = 8` force both dimensions to equal one.
83 The curve's Frobenius polynomials, database eigenvalues, modular attachment,
84 finite-flatness and the determinant-to-inertia dictionary are external arithmetic
85 inputs. None becomes a checked arithmetic theorem merely because its associated
86 polynomial calculation compiles.
87
88 ## New ordinary-cochain and affine statements
89
90 The final source is `formal/BealAffineReader.lean`, namespace
91 `KomorebiBeal.ReaderAffine`. The matching project copy is supplied in
92 `formal/reader_project`. Its eleven statements are:
93
94 | Statement | Quantified domain and exact conclusion |
95 |---|---|
96 | `differential_add` | Arbitrary monoid and additive commutative coefficient group. The trivial-action differential is additive in the cochain |
97 | `differential_sub` | The same domain. The differential of a difference is the difference of differentials |
98 | `same_primitive_difference_additive` | Two cochains with equal differentials have an additive difference |
99 | `add_character_preserves_differential` | Adding an additive function preserves a cochain's differential |
100 | `fixed_primitive_differential` | A monoid character into field units and a supplied twisted cocycle. The explicit fixed primitive has the displayed negative cup differential |
101 | `fixed_primitive_trace` | The same field-unit setup. The explicit fixed primitive satisfies the displayed toric trace identity |
102 | `solvability_translation` | A linear map over an arbitrary commutative ring. `Az=t` is solvable if and only if `Az=t−Az₀` is solvable |
103 | `cokernel_origin_invariance` | The classes of `t` and `t−Az₀` in `W/im A` agree |
104 | `null_test_necessary` | An explicitly supplied linear map `N` annihilating the image gives `Nt=0` for every solvable target |
105 | `complete_null_test` | The stronger, explicit hypothesis `ker N=im A` makes `Nt=0` equivalent to target solvability |
106 | `fiber_is_kernel_translate` | After one solution is supplied, every other solution differs from it by an element of `ker A` |
107
108 The differential convention is
109
110 \[
111 dp(g,h)=p(g)+p(h)-p(gh).
112 \]
113
114 The field-valued formulas use a character into units, so every character value
115 is nonzero. With a supplied cocycle
116 `alpha(gh)=alpha(g)+chi(g)*alpha(h)`, they define
117
118 \[
119 \beta(g)=(\chi(g)^{-1}-1)\lambda,
120 \qquad p^{\mathrm{fix}}(g)=\lambda\chi(g)^{-1}\alpha(g).
121 \]
122
123 The compiled conclusions are
124
125 \[
126 dp^{\mathrm{fix}}(g,h)=-\alpha(g)\chi(g)^{-1}\beta(h),
127 \qquad
128 (\chi(g)-1)p^{\mathrm{fix}}(g)+\alpha(g)\beta(g)=0.
129 \]
130
131 These are general algebraic identities. The module does not encode continuity,
132 an actual Galois group, the existence of a restricted primitive, or the uniqueness
133 argument requiring a separating character value. Those application statements
134 have their own prose proofs and source dependencies.
135
136 In the affine part, no completeness hypothesis is hidden. An arbitrary `N`
137 with `NA=0` supplies only the necessary test. The equivalence theorem requires
138 `ker N=im A` explicitly. It does not compute the actual fifteen-by-ten matrix,
139 prove its rank, construct a full left-null basis or evaluate an arithmetic
140 target. It does not compute the finite cardinality of an affine fiber. Its
141 last theorem describes that fiber once a solution has been supplied.
142
143 ## Reader source editions and current check
144
145 The corrected broad-import source is retained as `formal/BealAffine.lean`.
146 It passed direct strict elaboration during development. Its provenance wrapper
147 first requested a nonexistent optional Lean 4.19 checker binary, then a separate
148 bounded attempt hit a one-core import timeout. A four-import edition subsequently
149 revealed one missing library import.
150
151 The final `BealAffineReader.lean` replaces the broad import with the five actual
152 library imports. All definitions, statements, proof bodies and axiom targets
153 below those imports are byte-identical to the corrected broad-import source.
154 `formal/AFFINE_READER_IMPORT_PATCH.json` records that change. No theorem statement
155 was weakened and no linter was disabled.
156
157 The final run, `formal/affine_formal_run04`, checks the exact Lean 4.19 version,
158 the exact mathlib revision, source hashes, strict elaboration, all eleven axiom
159 reports and a nested-comment-aware forbidden-token scan. All passed. Compiler,
160 dependency-manifest, shim and source hashes are recorded in its result. The
161 official Lean 4.19 distribution here has no extra `leanchecker` executable.
162 No separate checker replay is claimed for this new module. Its generated proofs
163 are checked by Lean's normal elaboration kernel.
164
165 ## Host compatibility and failures
166
167 This host denies a process's own numeric `/proc/PID/exe` lookup while permitting
168 `/proc/self/exe`. The already authenticated, narrowly scoped `LD_PRELOAD` shim
169 redirects only that own-process executable lookup. Other paths pass unchanged.
170 Its source is included as `formal/proc_self_compat.c`, and the binary used has
171 SHA-256
172 `f9d97611cfbbab4b36bfa7a33d0812a38f7f35384683c5fcab0954f7008bbcc1`.
173 Compiler and proof bytes were not edited by the compatibility layer.
174
175 All unsuccessful development and provenance attempts remain in the package.
176 `formal/DEVELOPMENT_FAILURES.md` distinguishes the older-library import mismatch,
177 the quotient-lemma API correction, the absent optional checker, the private
178 runtime layout correction, the bounded import timeout and the missing narrow
179 import. Failed records are not included in the passed counts. Original historical
180 thread and cache failures are preserved separately as predecessor history.
181
182 ## Provenance and remaining mathematical boundary
183
184 The current two successful runs and five unsuccessful provenance runs each have
185 a version 2 computation-audit manifest. All seven passed manifest validation with
186 the project root, including actual input and output hash checks. An unsuccessful
187 run can be a valid provenance record. Validation does not change its failure
188 status or turn the record into a proof.
189
190 Commands, raw logs, input snapshots where relevant and exact result files are
191 included. Compiler binaries, private workspaces and large dependency caches are
192 external dependencies. Reproduction instructions and small Lake projects are in
193 `formal/REPRODUCE.md`, `formal/historical_project` and `formal/reader_project`.
194
195 The formal evidence verifies the stated logical, polynomial, cochain and affine
196 algebra. Finite-S Poitou–Tate duality, the arithmetic ordinary localization map,
197 the actual bare primitive and its labelled evaluations, the seven or eight
198 arithmetic affine obstruction coordinates, higher lifting and the connection to
199 integer Beal solutions remain separate mathematical obligations. No successful
200 compiler output supplies the missing arithmetic target.