kellermap: certified reductions of polynomial Keller maps

Abstract

kellermap constructs and verifies reductions of polynomial maps with constantJacobian determinant. Every transformation is a certificate object that carriesits own obligations; verification names the obligation that failed rather thanreturning a boolean, and a collision is transported across each step andre-verified, so that a reduction of a counterexample is still a counterexample. Version 0.7 adds the multi-affine normal form of Theorem 2.1(b), a descentstep that deletes a coordinate two elementary changes have made triangular,and the arithmetic that makes the library correct over coefficient rings thatare not fields: elimination to a unit pivot rather than to a non-zero one, anddeterminants taken without dividing. Version 0.6 implemented the second andthird stages of the Bass-Connell-Wright Reduction Theorem, collision-hullcompression, and the symmetric lift to the gradient form of a quartic over afield containing i. Applied in sequence to the smallest degree-three map thisproject holds, the chain runs 11, 22, 23, 19, 38 variables with every stepverified and the collision arriving at the far end. The constructions are other people's. What this project contributes is thecomposition of them, the certificates, and eight reconstruction scripts thatrecompute the published results in plain SymPy without using the library. Nominimality and no priority is claimed for any figure: both figures this chainreaches were published elsewhere first, by a different route, and the recordof what this project claimed too widely and corrected is in `docs/errata.md`. Generative AI tools were used in two roles: one model wrote code, tests anddocumentation in conversation with the maintainer, and a different modelaudited the release candidates. `docs/provenance.md` names the tools and sayswhat each did. Every audit of this milestone found faults that the test suite,the coverage requirement and the mutation sweep had all passed, and more thanonce the fault was in a repair made for the previous audit. Neither model is anauthor. The maintainer set the tasks, ran the gates, read the deliveries anddecided what entered the repository.