On the Boundary Rigidity of the Planar Jacobian Conjecture Below Degree 125: A Computational Audit of the GGHV (72, 108) Candidate

Abstract

Second edition of a computational audit of the degree-(72,108) Newton-polygon candidate (GGHV Case (c)) for the planar Jacobian conjecture. Reports a Lean 4 machine-checked valuative-properness predicate for the identity, one elementary triangular automorphism, and arbitrary GL_2(k)-linear maps; refutation of four local elimination shortcuts; a corrected Newton-Puiseux branch census at the two points at infinity; a capped corner-transfer sieve (48 negative-weight modes, degree-71 centralizer kernel, 264/408 frozen full-lattice modes, rank-2 linearized corner composite); and the cancellation identity {P, Q^2-P^3} = 2Q with deg(Q^2-P^3) >= 38. Conclusion: Case (c) and Gate 7 remain underdetermined. Companion file jc2d_computational_verification_files.zip contains all Python/Singular scripts, run logs, the CASE_C_RESOLUTION.md ledger, and the Lean 4 project sources; jc125_paper_source_files.zip contains the full XeLaTeX source.