Degree profiles of uniform polynomial consequences: Linear lower bounds for Nullstellensatz and Polynomial Calculus

This preprint proves linear degree lower bounds for Nullstellensatz and Polynomial Calculus and a four-way classification of degree profiles for uniform polynomial consequences over fields of positive characteristic. It strengthens the author’s 2008–2009 refutation classification and extends it to uniform consequences. A common p-adic hardness spectrum describes the four types topologically. The archive contains the paper PDF and LaTeX sources, a detailed companion tutorial, Lean formalisation, verification records, finite-example checks and reproduction instructions. The formalisation’s precise scope, external inputs and recorded evidence are documented in lean/SCOPE.md and lean/EVIDENCE.md. No fresh Lean kernel replay was performed for this archival step. Mathematical direction and responsibility: Søren Riis. AI-assisted development and verification are disclosed in the documents. This is version 1.0.0, a preprint and supporting-material archive, not a claim of journal publication. Development repository: https://github.com/SR123/degree-profiles-linear-bounds