# Formalization roadmap for the polynomial value-set lifting note

This file tracks the staged Lean translation of "Componentwise height bounds for
polynomial value-set lifting."  Status terms:

- `verified`: Lean theorem exists and builds without `sorry`.
- `partial`: supporting Lean lemmas exist, but not the manuscript theorem.
- `pending`: not yet formalized.

## Stage 1: polynomial algebra and quadratic sources

Status: partial.

- `prop:quadratic-source`: pending.  Needs a formal model of rational
  one-infinity components and birational polynomial parametrizations.
- `lem:engstrom`: pending.  Best formalized as an imported theorem if mathlib has
  Engstrom cancellation; otherwise isolate as a named theorem/axiom only after
  deciding how to prove it.
- `thm:quadratic-symmetry`: partial.  The file
  `HeightBoundsFormalization/QuadraticSources.lean` verifies the source-even
  algebra: classification of nonidentity affine involutions as reflections,
  the equivalence between reflection invariance `g(2c - Y) = g(Y)` and factoring
  through `(Y - c)^2`, even degree, odd-degree obstruction, and the parametrized
  identity `G((c + t E(t^2) - c)^2) = G(t^2 E(t^2)^2)`.  It also verifies the
  polynomial converse construction: from `g(Y)=G((Y-c)^2)` and
  `f(alpha U + beta)=G(U E(U)^2)`, Lean proves the parametrized identity
  `f(alpha t^2 + beta)=g(c+tE(t^2))`.  The forward parametrized direction is
  now formalized conditionally: Lean proves `g(B(-t))=g(B(t))` from
  `f(alpha t^2+beta)=g(B(t))`, and then proves `SourceEven g` from the exact
  nontrivial affine involutive symmetry output expected from Engstrom.
- `cor:fixed-g-square-root`: pending.  Should become a rewrite of
  `thm:quadratic-symmetry` once that theorem is formalized.
- `cor:monomial-square-root`: partial.  The odd-degree obstruction is verified in
  `not_sourceEven_of_odd_natDegree`; the complete even-degree classification is
  pending.
- `cor:generic-no-square-root`: partial.  The degree-parity obstruction is
  verified; the Zariski-generic coefficient-space statement is pending.
- `prop:detect-source-even` and `cor:no-quadratic-symmetry`: pending.

## Stage 2: polynomial multiplicity and thin sets

Status: pending.

- `def:thin sets`: formalize a reusable `Thin` predicate for rational points of
  varieties, probably specialized first to affine spaces and finite covers.
- `lem:thin-image`: pending.
- `def:degree-one component count`: pending.
- `thm:generic-fiber`: pending.
- `cor:multisection-cover`: pending.
- `thm:polynomial-multiplicity`: pending.
- `cor:polynomial-multisection`: pending.
- `prop:explicit-exceptional`: pending.

## Stage 3: component counts over number fields

Status: pending.

- `lem:S-height-count`: pending.  This will probably depend on existing mathlib
  height infrastructure plus imported/as-theorem-stated Schanuel-Barroero input.
- `lem:height-growth`: pending.  Likely formalizable using mathlib height
  functoriality if available.
- `lem:ngeo-finite`: pending.
- `prop:component-count`: pending.  This is a large target; first isolate the
  genus-zero one-infinity and two-infinity cases.

## Stage 4: main sparse lifting theorem

Status: pending.

- `lem:denominator-number-field`: pending.
- `lem:new-lifts-nongraph`: pending.
- `thm:number-field-sparse`: pending.
- `cor:number-field-exponent`: pending.
- `lem:integer-valued-coset`: pending.
- `thm:lower-bound`: pending.
- `cor:number-field-theta-asymp`: pending.
- `cor:Q-sparse`: pending.
- `cor:no-composition`: pending.

## Suggested next target

Continue inside Section 7 before moving into algebraic geometry:

1. State the polynomial-parametrized version of `thm:quadratic-symmetry` with
   explicit hypotheses `f(A(t)) = g(B(t))`, `A = alpha*t^2 + beta`, and
   `B` not even in `t`, using the new `EngstromHypothesis` wrapper for the
   only unverified forward-direction input.
2. Then state the geometric part of `thm:quadratic-symmetry` with explicit
   hypotheses on polynomial parametrizations, before introducing components of
   `f(X) - g(Y) = 0`.