Structure and computability of the single-quadratic existential fragment over the integers (paper)

The paper (APAL_MANUSCRIPT_v32.pdf) of the mpup release. It classifies the total functions definable over the integers by one polynomial equation of total degree at most two with unrestricted integer unknowns (the forward directions under the ternary-coset representation input TCER, derived in the paper from published work of Kane and Kim), proves finite-fibre bounds, the injective-dimension theorem and a structured infinite-fibre theorem, and places the fragment in the computability phase diagram under two named classical hypotheses (code-uniform decidability of integer quadratic solvability, after Grunewald and Segal, and DPRM over ℕ). Sections 2-9, and Section 10 except Lemma 10.8, are formalized in Lean 4; a generated Blueprint maps every numbered statement to its trust label and Lean names; the software record is linked below. MSC 2020: 03D25 (primary); 11D09, 11U05, 03B35, 11Y50, 68V15 (secondary).