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