Full e=4 Polydegree column — v0.1.0 candidate

Anonymous unrefereed candidate

This prerelease fixes the exact public candidate package at commit 7ad032dbfd0fe937003ea6378bfe98f6475f5e39.

The principal manuscript presents a computer-assisted proof of

G_(d+4) subset closure(G_(d,5)) for every integer d >= 2.

Its gap-free degree stitch uses published input for 2 <= d < 20, an exact residue-one branch, 14,985 outward-rounded FLINT/Arb finite cases for 5 <= m < 5000 in residues 0, 2, 3, and an explicit uniform analytic certificate for m >= 5000.

Two companion manuscripts provide:

• a Lean 4.32.1 / Mathlib formalization of a universal bordered-Jacobian identity over arbitrary commutative rings; and
• a boundary-norm lemma, a finite-pencil equivalence, and a conditional transfer theorem with a six-sheet application.

GitHub Actions passed on Python 3.12 and 3.14 in normal and optimized modes, including three semantic mutation controls, and the Lean build and axiom audit passed.

This release does not solve Furter's R(3), monotone rigidity, the two-dimensional Jacobian conjecture, or the quartic Hessian conjecture. It records producer-side replay and internal AI editorial review, not independent reproduction, external specialist review, or journal peer review.

The ZIP, three PDFs, and SHA256SUMS constitute the complete release asset set. Original prose and data are dedicated under CC0 1.0; original non-Lean code is MIT; the Lean subtree retains its Apache-2.0 terms.

Reserved DOI: 10.5281/zenodo.22072044