Beal: source and evidence / FORMAL_STATUS.md

Beal formal evidence

Final check report, 8 October 2026, America/Chicago. The original Block 47 and Block 48 sources passed a fresh check under their exact compiler and library pins. A new eleven-statement module passed strict source elaboration and axiom inspection for the ordinary cochain and affine linear algebra used in the reader.

Result and distinct scopes

Development	Exact pin used in the successful current run	Public statements checked	Fresh result
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
Block 48	The same Lean and mathlib pins	8	Unchanged source passed direct warning-as-error elaboration and all eight axiom reports
Reader affine module	Lean 4.19.0, mathlib `c44e0c8ee63ca166450922a373c7409c5d26b00b`	11	Final minimal-import source passed warning-as-error elaboration and all eleven axiom reports

These are forty named public statements in three scopes. The counts exclude the Block 48 private helper and the intentionally invalid negative controls. They are not forty proofs of the Beal conjecture or forty arithmetic realizations. No successful current axiom report contains sorryAx or a custom axiom. The dependencies are subsets of Lean's standard propext, Classical.choice and Quot.sound.

Historical source authentication and replay

All four Block 47 source hashes match the archived verification report. The Block 48 source hash matches its archived result. The recovered files and the historical compiler logs are preserved unchanged. Source authentication is recorded in formal/HISTORICAL_INPUT_AUTHENTICATION.json.

The historical Block 47 compiler is Lean 4.34.0-rc2 at commit 6a10ac8c22beadecabdbb0919c2b50214762f91d. Its compiler binary was reused from the preceding ABC check without modification. The exact historical mathlib checkout was freshly fetched at aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Its official cache downloader completed successfully and downloaded 8,849 cache objects. Fresh dependency checks matched every declared revision in both environments. All checked tracked package sources were clean. The eighteen dependency records, compiler hashes, and acquisition records are in formal/RUNTIME_DEPENDENCY_AUTHENTICATION.json and the mathlib acquisition and cache logs.

The original verify_block47.py was copied unchanged to a private working project. All four original sources compiled with warnings treated as errors. The source scan found no admitted proof, custom axiom, unsafe declaration or native_decide. All twenty-one requested theorem axiom reports appeared and used only the three standard axioms listed above.

The verifier assembled its original replay module and compiled it. The exact leanchecker then replayed only Beal47Replay, as requested. Imported pinned mathlib objects remain trusted in the ordinary workflow. This is a separate check of the project module, not a rebuild or independent verification of every mathlib dependency.

All three deliberate negative controls were rejected for their expected reasons: an invalid single-candidate choice across two tests, a false off-diagonal coefficient cancellation, and a placeholder proof under warning-as-error settings. The placeholder is a negative-control input and is never counted as a proved theorem.

Block 48's unchanged source separately compiled with one Lean worker and strict warnings. All eight public axiom reports appeared, with no nonstandard axiom dependency. The source bytes before and after both successful checks matched the recovered originals. The final current run is formal/historical_exact_run02.

What the historical statements establish

Block 47 has seven generic lane-certificate statements, five finite Boolean correlation statements and nine exact mod-seven polynomial or matrix statements. The generic exclusion implication explicitly assumes a complete lane cover, an attachment of a globally fixed candidate and soundness of each selected test. Compilation proves the implication with those hypotheses. It does not supply their arithmetic instantiation.

The polynomial module checks the cube of the displayed sextic over ZMod 7, four coefficient positions, their determinant expression, the assembled two-by-two matrix and its square. The module documentation explicitly leaves the identification of that coefficient matrix with a geometric Cartier operator outside the formalization.

Block 48 proves common-root and trace exclusions over any characteristic-seven field. It also proves the elementary bounded natural-number statement that d₀,d₁ ≤ 2 and (d₀+7*d₁) mod 48 = 8 force both dimensions to equal one. The curve's Frobenius polynomials, database eigenvalues, modular attachment, finite-flatness and the determinant-to-inertia dictionary are external arithmetic inputs. None becomes a checked arithmetic theorem merely because its associated polynomial calculation compiles.

New ordinary-cochain and affine statements

The final source is formal/BealAffineReader.lean, namespace KomorebiBeal.ReaderAffine. The matching project copy is supplied in formal/reader_project. Its eleven statements are:

Statement	Quantified domain and exact conclusion
`differential_add`	Arbitrary monoid and additive commutative coefficient group. The trivial-action differential is additive in the cochain
`differential_sub`	The same domain. The differential of a difference is the difference of differentials
`same_primitive_difference_additive`	Two cochains with equal differentials have an additive difference
`add_character_preserves_differential`	Adding an additive function preserves a cochain's differential
`fixed_primitive_differential`	A monoid character into field units and a supplied twisted cocycle. The explicit fixed primitive has the displayed negative cup differential
`fixed_primitive_trace`	The same field-unit setup. The explicit fixed primitive satisfies the displayed toric trace identity
`solvability_translation`	A linear map over an arbitrary commutative ring. `Az=t` is solvable if and only if `Az=t−Az₀` is solvable
`cokernel_origin_invariance`	The classes of `t` and `t−Az₀` in `W/im A` agree
`null_test_necessary`	An explicitly supplied linear map `N` annihilating the image gives `Nt=0` for every solvable target
`complete_null_test`	The stronger, explicit hypothesis `ker N=im A` makes `Nt=0` equivalent to target solvability
`fiber_is_kernel_translate`	After one solution is supplied, every other solution differs from it by an element of `ker A`

The differential convention is

\[ dp(g,h)=p(g)+p(h)-p(gh). \]

The field-valued formulas use a character into units, so every character value is nonzero. With a supplied cocycle alpha(gh)=alpha(g)+chi(g)*alpha(h), they define

\[ \beta(g)=(\chi(g)^{-1}-1)\lambda, \qquad p^{\mathrm{fix}}(g)=\lambda\chi(g)^{-1}\alpha(g). \]

The compiled conclusions are

\[ dp^{\mathrm{fix}}(g,h)=-\alpha(g)\chi(g)^{-1}\beta(h), \qquad (\chi(g)-1)p^{\mathrm{fix}}(g)+\alpha(g)\beta(g)=0. \]

These are general algebraic identities. The module does not encode continuity, an actual Galois group, the existence of a restricted primitive, or the uniqueness argument requiring a separating character value. Those application statements have their own prose proofs and source dependencies.

In the affine part, no completeness hypothesis is hidden. An arbitrary N with NA=0 supplies only the necessary test. The equivalence theorem requires ker N=im A explicitly. It does not compute the actual fifteen-by-ten matrix, prove its rank, construct a full left-null basis or evaluate an arithmetic target. It does not compute the finite cardinality of an affine fiber. Its last theorem describes that fiber once a solution has been supplied.

Reader source editions and current check

The corrected broad-import source is retained as formal/BealAffine.lean. It passed direct strict elaboration during development. Its provenance wrapper first requested a nonexistent optional Lean 4.19 checker binary, then a separate bounded attempt hit a one-core import timeout. A four-import edition subsequently revealed one missing library import.

The final BealAffineReader.lean replaces the broad import with the five actual library imports. All definitions, statements, proof bodies and axiom targets below those imports are byte-identical to the corrected broad-import source. formal/AFFINE_READER_IMPORT_PATCH.json records that change. No theorem statement was weakened and no linter was disabled.

The final run, formal/affine_formal_run04, checks the exact Lean 4.19 version, the exact mathlib revision, source hashes, strict elaboration, all eleven axiom reports and a nested-comment-aware forbidden-token scan. All passed. Compiler, dependency-manifest, shim and source hashes are recorded in its result. The official Lean 4.19 distribution here has no extra leanchecker executable. No separate checker replay is claimed for this new module. Its generated proofs are checked by Lean's normal elaboration kernel.

Host compatibility and failures

This host denies a process's own numeric /proc/PID/exe lookup while permitting /proc/self/exe. The already authenticated, narrowly scoped LD_PRELOAD shim redirects only that own-process executable lookup. Other paths pass unchanged. Its source is included as formal/proc_self_compat.c, and the binary used has SHA-256 f9d97611cfbbab4b36bfa7a33d0812a38f7f35384683c5fcab0954f7008bbcc1. Compiler and proof bytes were not edited by the compatibility layer.

All unsuccessful development and provenance attempts remain in the package. formal/DEVELOPMENT_FAILURES.md distinguishes the older-library import mismatch, the quotient-lemma API correction, the absent optional checker, the private runtime layout correction, the bounded import timeout and the missing narrow import. Failed records are not included in the passed counts. Original historical thread and cache failures are preserved separately as predecessor history.

Provenance and remaining mathematical boundary

The current two successful runs and five unsuccessful provenance runs each have a version 2 computation-audit manifest. All seven passed manifest validation with the project root, including actual input and output hash checks. An unsuccessful run can be a valid provenance record. Validation does not change its failure status or turn the record into a proof.

Commands, raw logs, input snapshots where relevant and exact result files are included. Compiler binaries, private workspaces and large dependency caches are external dependencies. Reproduction instructions and small Lake projects are in formal/REPRODUCE.md, formal/historical_project and formal/reader_project.

The formal evidence verifies the stated logical, polynomial, cochain and affine algebra. Finite-S Poitou–Tate duality, the arithmetic ordinary localization map, the actual bare primitive and its labelled evaluations, the seven or eight arithmetic affine obstruction coordinates, higher lifting and the connection to integer Beal solutions remain separate mathematical obligations. No successful compiler output supplies the missing arithmetic target.