Main result
The main theorem separates the remaining contributions by component geometry. Active rational one-infinity components give the power-log terms; rational two-infinity components contribute only unit-theoretic polylogarithmic growth; the remaining components contribute finitely many inputs. A separate quadratic-source section isolates the square-root boundary and shows that it forces an affine involution of the source polynomial.
- Contribution type
- New argument; partial Lean formalization
- Contribution
- Componentwise sparse height bounds for polynomial value-set lifting after removing graph components.
- Core mechanism
- Graph removal, active one-infinity components, unit growth, quadratic source-even obstruction
- arXiv
- arXiv:2605.12903, submitted May 13, 2026; math.NT and math.AG
- Lean scope
- Section 7 algebra around affine involutions, source-even polynomials, odd-degree obstruction, and the parametrized quadratic-source converse.
- Lean theorem family
HeightBoundsFormalization.QuadraticSources- Lean and mathlib
- Lean 4.30.0-rc2, mathlib v4.30.0-rc2
- Build command
lake build