Actual antidiagonal sums · canonical residues · nonzero leading terms · Constructive arithmetic

Canonical polynomial products and represented degree

Prime(p) ∧ FpRepresentedDegree(p,ab,ac,L,d) ∧ FpRepresentedDegree(p,bb,bc,M,e) ∧ FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) ⇒ FpRepresentedDegree(p,cb,cc,N,d+e)

Construct highest-degree-first coefficient convolution, prove its finite support, and establish degree addition for genuinely nonzero-leading prime-field representations.

Open the definition-aware map Read the final theorem See campaign milestone G091

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact certificate

Fully expanded arithmetic

Inspect all 2496 native tactic lines and 123 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PC0035 and follow only the lemmas and conservative definitions supporting prime_field_polynomial_convolution_represented_degree_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: PC0029 prime_field_polynomial_convolution_exists_unique · PC002D prime_field_polynomial_convolution_outside_zero · PC0035 prime_field_polynomial_convolution_represented_degree_exists.
Independently verified Alpha v34 checked-use theorem family: 53 dependency-curried kernel-checked theorem bodies · 123 proof prerequisites · 19 linked definitions · 30 definition-dependency arrows · 2496 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 210 bundle nodes; SHA-256 55f12903e1b1d3b4832f6c728cb366c20868c4e88810a736316b30cddf01dde3.
Exact mathematical boundary: Coefficients are highest-degree-first and every representation carries its explicit length. Empty inputs give an empty product; zero extension does not constrain unrelated beta entries past the prefix. Represented degree requires a decoded nonzero leading coefficient and does not assign a degree to zero. This checkpoint claims coefficient convolution and degree addition, not polynomial division, gcd, irreducible search, an evaluation-product identity, or general prime-power extension fields; full G091 remains open.