Kummer for arbitrary finite multinomials — Exact Proof Explorer

Every empty decoded list has an empty bounded-valuation table.

A finite valuation table restricts to its predecessor prefix.

Each actual last table entry has the exact canonical valuation of its actual decoded factor.

Append an actual valuation and recode the complete finite table with all prior entries preserved.

Every finite decoded list has a genuinely constructed finite table of bounded power valuations.

For a prime and any nonzero finite factor list, the exact product valuation equals the finite sum of its actual factor valuations.

A real finite sum of factor valuations constructs the exact valuation of their nonzero product.

The empty multinomial factor prefix requires no binomial entries.

A complete binomial factor table restricts to the predecessor prefix.

Append one actual binomial factor while preserving every previously coded factor.

Construct all actual binomial factors for any finite decoded part and partial-sum tables.

Every actual multinomial binomial factor is strictly nonzero, including zero-valued input parts.

An actual finite sum of parts has an actual iterated-binomial multinomial coefficient.

Every finite natural part list, including the empty list, has a witnessed total and multinomial coefficient.

An actual multinomial coefficient is always nonzero; no undefined zero valuation is used in Kummer's theorem.

Apply the actual checked binary Kummer proof to every decoded addition row; the resulting certificate contains real quotient columns and carry bits.

For every prime and every finite natural part list, an actual multinomial coefficient has a constructed exact valuation equal to all witnessed column carries; the empty list and zero parts are included.

The empty multinomial has exactly total zero and coefficient one.

An actual empty finite addition has exactly zero column carries, with no prime-base assumption needed.