v7.1.3 Iter Beal Not Route E Corrected

Docs-only. No Lean change. Corrects an error introduced in v7.1.2: docs/OPERA_NUMERORUM_LINKS.md and this README's 'wider work' section labeled the Beal Conjecture as 'Route E', implying it was a fifth entry in the Riemann Hypothesis Route A-D lettering. That is wrong: the Beal Conjecture is its own chamber of Opera Numerorum, spanning two companion repositories (this repository and beal-level-26-foundations), unrelated to the RH routes beyond both being chambers of the same wider project.

docs/OPERA_NUMERORUM_LINKS.md restructured: Beal now under its own heading 'The Beal Conjecture — housed in two companion repositories, level-26 unconditional none'; Routes A-D grouped under their own parent heading 'The Riemann Hypothesis — four independent routes' as #### Route A .. #### Route D. Same restructuring applied to the mirrored section in README.md.

check-v11-release.sh OK: all required DOI strings and 'conditionally complete' remain present elsewhere in README.md; no grep lock broken.

v7.1.2 Iter Readme Uniform Opera Links

Docs-only. No Lean change.

New file docs/OPERA_NUMERORUM_LINKS.md — the bulk-uploadable Opera Numerorum coordination index (identical text intended for every chamber repo): coordination index opera-numerorum, Route A-D companions, and Route E Beal Conjecture naming both this repository (conditionally complete v11.0.0, five explicit premises) and beal-level-26-foundations (UNCONDITIONAL v7.1.0 BOTH none).

README.md 'The wider work: Opera Numerorum and related repositories' section replaced with the uniform coordination-index text (now includes Route E naming this repo), and the 'Active level-26 foundations companion' block updated from the stale v1.2.1 22286630 pointer to v7.1.0 22632209 BOTH-none-unconditional, plus the v7.1.1 About catch-up 22635221, keeping old companions (v1.2.1 22286630, v1.2.0 22286222) listed for history.

check-v11-release.sh OK: all required DOI strings and 'conditionally complete' remain present elsewhere in README.md; no grep lock broken.

v11.0.0 — Conditionally complete

v11.0.0 — Conditionally complete

Version DOI: 10.5281/zenodo.22281075

This release closes the repository as a stable conditional theorem assembly.
The final theorem proves BealConjecture from exactly five named inputs:

1. J0DecompositionSoundness_26;
2. MwrankCertificateSoundness_26;
3. FormalImmersionSoundness_26;
4. FreyCurveExists;
5. LevelLowering_26.

It does not claim those inputs have been constructed.

The mod-3 matrix is derived from the normalized level-26 eigenform coefficient
lines and the explicit basis change (P), proving (PC_3=M_3). The remaining
geometric theorem is named
QExpansionCotangentCompatibilityAtInfinity26; it must identify that
coefficient map with the actual Abel--Jacobi cotangent map at the cusp.

The Selmer-cardinality module proves cardinality one for an explicitly
supplied carrier from a triviality theorem or a genuine ledger equivalence.
Its identification with the cohomological Selmer group remains an external
mathematical input; the finite audit is not relabeled as that comparison.

The companion Foundations release
10.5281/zenodo.22272714 contains
the corrected computable v1 evidence. The two repositories are companion
works, not versions of one another.

v10.0.0: ConditionalBealTheorem — Opera Numerorum — explicit premises

Focused build Beal.Final.ConditionalBealTheorem passed, Axiom only [propext, Classical.choice, Quot.sound], No new axiom/sorry/admit/True stubs. Premises: J0DecompositionSoundness_26, MwrankCertificateSoundness_26, FormalImmersionSoundness_26, FreyCurveExists (reuses FreyCurveConstruction_26), LevelLowering_26 (packages indexed modularity supplier + LevelLoweringCertificate_26). Chain v9.2+v9.3+v9.4+v10. Task #495 remains v10.0.1 hardening for explicit cotangent map M3.

v9.4.0: Formal immersion X0(26)->J0(26) at 2 via M3 rank 2

v9.4.0 — Formal immersion X0(26) -> J0(26) at 2 via M3 rank 2

This release adds a reproducible finite formal-immersion witness for the level-26 route.

Verification

• Formal-immersion JSON witness passed
• J0(26) JSON witness passed
• Focused Lean build passed
• Full CI passed
• Axiom output uses only propext, Classical.choice, and Quot.sound

Formal boundary

The explicit proposition-valued premises are J0DecompositionSoundness_26, MwrankCertificateSoundness_26, and FormalImmersionSoundness_26; they are not global axioms.

The chain is: v9.2 rank 0 (Selmer = {1}) + v9.3 dim J0(26) = 2 = 1 + 1 isogeny + v9.4 M3 rank 2 => X0(26)(Q) finite.

Follow-up Task #495 records construction of the level-26 cotangent map behind the finite witness.

v9.3.0: J0(26) decomposition — dim 2 = 26a x 26b isog

Verification: JSON witness check passed, Focused Lean build passed, No new axiom/sorry/admit, Main CI passed in 2m42s, PR #20 merged. Assets: j0_26_decomp.log, GENUINE certs, immutable JSON witness.

v9.1.0 Real Formal Immersion Matrix - M3=[[1,1],[0,2]] Rank 2 mod 3 Decided + A+B Real

v9.1.0: Phase C Real Matrix Rank - Formal Immersion at 3 Decided

Phase C now carries real finite formal-immersion matrix evidence at 3. The explicit differential evaluation table over ZMod 3 computes M3 = [[1,1],[0,2]], with determinant 2 != 0 mod 3 and rank two proved by decide.

Real finite chain

• Phase A: all 80 S-unit/quartic checks at p=2,13 pass; all eight candidates remain, so no singleton Selmer claim is made.
• Phase B: S2(26) q-expansion tables, Hecke checks at 2 and 13, distinctness, and dimension-two evidence.
• Phase C: degree-six hyperelliptic model, differential basis omega1=dx/y and omega2=x dx/y, four cusp reduction tokens, Abel-Jacobi replay rows, differential table, and the decided rank-two M3 certificate.

Verification

• Focused builds for FormalImmersion_26, J0_26_Decomp, SecondDescent_Real_26, and ConditionalBealTheorem passed.
• Full Lean build passed in GitHub Actions.
• The finite matrix rank theorem introduces no axioms.
• The combined transport/formal-immersion evidence uses only Lean foundations: propext, Classical.choice, Quot.sound.
• No new sorry, admit, opaque proof placeholder, sorryAx, Lean.ofReduceBool, or native_decide was introduced.

Honest boundary

The actual Abel-Jacobi map, smooth reduction, geometric implication to the four-cusp classification, the Jacobian isogeny J0(26) ~ E26a1 x E26b1, modularity, and level-lowering remain explicit conditional data. This release does not claim an unconditional proof of Beal's Conjecture.

Implementation merge: 0a28f24
Release snapshot: 62fd5db
Validation PR: #16
Concept DOI: https://doi.org/10.5281/zenodo.22041831

Archive: beal-conjecture-v9.1.0.tar.gz
Size: 182665 bytes
SHA-256: 581c9f3ce63e1a379c6163749a16bff55d837c999f0f57af39f506ce727b7b89

DOI

• Version DOI: https://doi.org/10.5281/zenodo.22240445
• Concept DOI: https://doi.org/10.5281/zenodo.22041831
• Zenodo record: https://zenodo.org/records/22240445

Zenodo preserves the GitHub-hook source ZIP; its README and Phase A/B/C release-critical Lean files were verified byte-for-byte against the annotated v9.1.0 tag. The canonical attached tarball remains beal-conjecture-v9.1.0.tar.gz with the size and SHA-256 listed above.

v9.0.0 — Real S₂(26) Decomposition Evidence — Phase B Hardened

v9.0.0 — Real S₂(26) Decomposition Evidence

Phase B is now backed by explicit finite evidence while the unavailable genus-two Jacobian isogeny remains an honest conditional boundary.

Real finite evidence

• LMFDB-sourced level-26 q-expansion rows through a₁₀₀, with the legacy first twenty coefficients checked by kernel decide.
• Explicit finite Hecke recurrence checks at p = 2 and p = 13.
• Decided distinctness of the two newform rows.
• dim S₂(26) = 2, tied to the existing certified genus-two token without claiming a new Riemann–Roch or Riemann–Hurwitz formalization.
• JacobianTransportCertificate_Real_26, combining q-expansion distinctness, Hecke evidence, dimension two, degree six, nonzero discriminant, genus two, and the existing mod-3 determinant certificate.

The finite q-expansion, Hecke, distinctness, and dimension facts depend on no axioms. The combined transport evidence uses only propext, Classical.choice, and Quot.sound.

Honest conditional boundary

The actual isogeny J₀(26) ~ E26a1 × E26b1 remains an explicit Prop-valued boundary because Lean 4.12/Mathlib does not supply the needed genus-two Jacobian and abelian-variety isogeny API. Phase A's eight S-unit representatives also remain after all 80 local checks, so SecondDescentHypothesis_26 is still conditional. Formal immersion, modularity, and level lowering remain explicit inputs. This release does not claim an unconditional proof of Beal's Conjecture.

Verification

• Commit: 5cee2e1e8e39b0924cc33bfa483ace875be734d6
• GitHub Actions run: 33562292862 — green
• Full Lean build passed.
• Repository axiom audits passed.
• Changed sources contain no sorry, admit, opaque, sorryAx, Lean.ofReduceBool, or native_decide.
• Immutable predecessor v8.9.0: 386e35e20ab857559668f6e92949f31fe857d746

Attached archive

• File: beal-conjecture-v9.0.0.tar.gz
• Size: 177603 bytes
• SHA-256: 90f412861e46f54e1857e7bd994d431f5118cb1a58bf22f8f96d34fe5e47929d

v8.9.0 — Real 80-Check Audit: Honest Level-26 Finite Descent + B+C+D Conditional Beal

v8.9.0 — Real 80-Check Audit

This release archives the immutable v8.9.0 tag at commit 386e35e20ab857559668f6e92949f31fe857d746.

What is real

• Complete finite grid of eight S-unit representatives against ten quartics: 80 entries.
• All 80 available local checks pass at p = 2 and p = 13.
• The audited declarations contain no sorry, admit, sorryAx, or Lean.ofReduceBool.

Honest boundary

All eight S-unit representatives remain. This is not a singleton 2-Selmer computation. SecondDescentHypothesis_26, the Jacobian transport, formal immersion, modularity, and level-lowering suppliers remain explicit conditional boundaries. The B+C+D Beal chain is therefore conditional; this release does not claim an unconditional proof of Beal's Conjecture.

Attached archive

• File: beal-conjecture-v8.9.0.tar.gz
• Size: 175208 bytes
• SHA-256: 61362de15bd0c2ea9f64fea47ce91e958c9eafd2a6aa034147fda68099266672

v8.8.0 — Conditional Phase D Level-26 Frey Endgame

Conditional Phase D — level-26 Frey endgame

This release archives the green GitHub main commit 881926ae90341b60bbaf8254475ad9c8fa7fd6a4.

Added

• lean/Beal/Mazur/Frey/LevelLowering_26.lean
• A proof-relevant conditional interface connecting a primitive Beal counterexample to a noncuspidal rational point on the displayed level-26 model.
• Explicit supplier boundaries for Frey construction, modularity and R=T, level lowering, second descent, Jacobian transport, and formal immersion.
• The final contradiction after the existing Phase A–C rank-zero and four-cusp certificates.

Formal status

This is a conditional formalization milestone, not an unconditional Lean proof of Beal’s conjecture. The new principal theorems compile with no sorryAx and depend only on Lean’s standard {propext, Classical.choice, Quot.sound} foundations. No executable sorry, admit, axiom, opaque, or Boolean proof stub was introduced.

The release does not claim that the modularity, level-lowering, Frey-construction, or displayed-model interpretation boundaries have been proved in Mathlib 4.12.

Verification

• Local target: lake build Beal.Mazur.Frey.LevelLowering_26
• GitHub Actions: https://github.com/DavidFox998/beal-conjecture/actions/runs/33488644874
• CI conclusion: success
• Base commit: bb8ebb354164418748c0c6ec4f8febdc85feb227
• Version DOI: https://doi.org/10.5281/zenodo.22235410
• Concept DOI: https://doi.org/10.5281/zenodo.22041831