Prime-field coefficient tables and Horner evaluation — Exact Proof Explorer

Actual finite quotient/remainder witnesses give genuine coefficientwise canonical normalization.

Every natural coefficient table has an actual canonical reduction at every nonzero modulus, including empty tables.

All decoded entries satisfy normalization, not just the initially chosen beta witnesses.

The normalized table really has every coefficient strictly below the modulus.

Normalized coefficient values are unique, while their actual beta encodings may differ.

A table already consisting of canonical coefficients normalizes to itself.

Reencoding both finite prefixes preserves every actual normalization witness.

Reducing a normalized polynomial again leaves every coefficient unchanged, not necessarily its raw code.

A genuinely repeated canonical value forms a bounded coefficient table, including length zero.

Construct a finite coefficient table containing exactly the chosen canonical coefficient at every position.

Every prime admits an actual all-zero coefficient table of every finite representation length.

Normalize a genuine natural pointwise sum to obtain actual canonical field sums at every coefficient.

Construct the actual finite canonical coefficient sum, without supplying a table or an addition-law premise.

Every decoded coefficient triple obeys the actual field-addition graph, independently of witness choices.

All three prefixes in an actual polynomial addition consist of canonical coefficients.

The sum is unique as a coefficient prefix; arbitrary beta recodings remain admissible.

Independent beta recoding of both inputs and the output preserves actual coefficient addition.

Coefficient addition commutes for actual finite tables, including the empty table.

An actual all-zero table is an additive identity at every finite representation length.

Normalize an actual pointwise product with a repeated scalar to obtain genuine canonical scalar multiplication.

Every canonical scalar has an actual finite coefficient-product table, including scalar zero and empty inputs.

Every decoded input/output pair of the scalar table satisfies actual canonical multiplication.

Both the input and the constructed output of scalar multiplication have bounded coefficients.

The scalar product has a unique decoded coefficient prefix, not a unique raw beta code.

Independent recoding of the source and target preserves actual scalar multiplication.

The actual canonical scalar one acts identically on every finite coefficient prefix.

Scalar zero produces a genuinely encoded zero polynomial, not merely a zero output claim.

Both actual bracketings of three finite coefficient additions yield extensionally equal prefixes.

Two successive canonical scalar actions agree coefficientwise with the actual canonical product scalar.

Actual scalar multiplication distributes over actual coefficient addition, with code-independent output equality.

Acting by an actual sum of scalars agrees with adding their separately constructed coefficient actions.

Construct an actual canonical multiply-then-add step from proved residues of the corresponding natural step.

Reducing all l+1 states of a genuine natural Horner trace constructs a genuine canonical execution, including its zero initial state.

Every canonical coefficient prefix and canonical base have an actual finite modular Horner history; no trace or norm invariant is supplied.

The actual execution graph entails canonical input coefficients and base; no separate input-bound certificates are hidden in its steps.

The empty polynomial execution returns zero by its actual initial and terminal beta entries.

An actual successor execution decomposes into its actual prefix and final multiply-then-add step in highest-degree-first order.

Coefficient reencoding preserves the same real execution trace and result, without asserting equality of raw code numbers.

Ordinary induction proves the residue invariant against arbitrary natural coefficients and their actual coefficientwise reduction; the invariant is not part of the execution definition.

Actual modular evaluation has exactly the canonical residue of the existing natural T12 Horner value.

Every actual modular execution of the same coefficient prefix and base has the same canonical result.

Constructive totality and uniqueness of genuine finite prime-field polynomial evaluation, including p=2 and length zero.

Construct an actual zero-result execution of every empty coefficient prefix, retaining the canonical base guard.

Every actual canonical last multiply/add step extends an actual prefix to a full execution; the required coefficient bounds are derived, not assumed.

A one-coefficient prefix evaluates to that actual constant, including zero and characteristic two.

Every actually encoded all-zero coefficient prefix has a genuine zero-result modular execution, including length zero.

After actual coefficient reduction, the genuine modular execution exists with exactly—and every—canonical residue of the original natural T12 evaluation.

Every genuine execution result is strictly below p, including the empty and zero-polynomial boundary cases.

For arbitrary finite natural coefficients construct their canonical prime-field table and an actual Horner execution, and prove agreement with every natural T12 evaluation.