Polynomial division prerequisites — Exact Proof Explorer

Construct a genuine bounded solution of b+r=a using actual additive inverse and addition witnesses.

The genuine bounded difference of a canonical coefficient from itself is natural zero.

Every pair of empty coefficient prefixes satisfies the operation, including modulus zero and arbitrary encodings.

Construct the entire actual canonical coefficient output by ordinary induction and beta-prefix extension; no output table is assumed.

Every actual decoded tuple satisfies the bounded scalar graph, independently of its existential witnesses.

The actual operation graph itself forces every source and result coefficient to be canonical.

The result is unique by existing decoded-prefix equality, never by equality of beta code numbers.

Independent beta recodings of every input and output preserve the actual aligned coefficient operation.

Reversing a genuine coefficientwise additive inverse gives the original values, without identifying encodings.

A genuinely encoded all-zero coefficient prefix is its own additive inverse.

Adding actual opposite coefficient values produces any genuine zero-prefix encoding.

Every pair of empty coefficient prefixes satisfies the operation, including modulus zero and arbitrary encodings.

Construct the entire actual canonical coefficient output by ordinary induction and beta-prefix extension; no output table is assumed.

Every actual decoded tuple satisfies the bounded scalar graph, independently of its existential witnesses.

The actual operation graph itself forces every source and result coefficient to be canonical.

The result is unique by existing decoded-prefix equality, never by equality of beta code numbers.

Independent beta recodings of every input and output preserve the actual aligned coefficient operation.

Relate the actual subtraction witnesses to the actual aligned B+R=A table; no algebraic identity is assumed.

Relate the actual subtraction witnesses to the actual aligned B+R=A table; no algebraic identity is assumed.

Subtracting a canonical prefix from itself constructs its genuine all-zero coefficient result.

Subtracting an actual zero prefix leaves the represented canonical coefficients unchanged.

Subtracting an actual canonical prefix from zero yields its actual coefficientwise additive inverse.

Equal aligned coefficients, in particular equal leading coefficients, leave actual zero at that result position.

Subtracting extensionally equal canonical prefixes gives an actual all-zero prefix even when their beta encodings differ.

Subtracting the actual first addend from an actual sum recovers the other addend by represented-prefix equality.

Two actual differences with the same subtrahend and result have equal represented minuend coefficients.

Construct every finite beta-coded suffix by the existing actual affine-slice constructor at stride one, including length zero.

Every actual output decoding equals the input coefficient at the supplied shifted index.

A genuine suffix ending at the annotated input length inherits every canonical coefficient bound.

Two actual suffix encodings agree at every decoded prefix position, without asserting equality of raw codes.

Finite induction scans actual decoded coefficients: either the entire prefix is zero or the first retained position has an actual nonzero value.

An actually constructed first-nonzero cut and actual suffix supply the normalized output head; no output-bound or algebra-law premise is assumed.

Every actual canonical input has a genuinely beta-coded leading-zero trim, for all moduli and all finite lengths including zero.

Every pair of output beta codes is a valid empty trim of every empty input, including modulus zero; raw encodings are deliberately unconstrained.

The actual trimmed coefficients are canonical below the same modulus; this is a consequence, not a clause assumed in Trim.

Both the number of removed leading zeroes and the retained length are bounded by the actual annotated input length.

When the retained length is positive, every actual input decoding at the cut position is nonzero.

An empty actual trim certifies that every coefficient of the entire input prefix is zero.

A genuinely all-zero input cannot have a nonempty normalized trim, proved using actual input and output beta values.

For an actual trim, empty output and an all-zero input prefix are constructively equivalent.

One normalized cut cannot lie after another: otherwise a supposedly leading nonzero coefficient belongs to the other removed zero prefix.

The number of removed leading zero coefficients is uniquely determined by the annotated input prefix.

The retained representation length is unique by the actual length split and additive cancellation.

All actual trims of the same input agree coefficientwise on the unique retained prefix; no beta-code identity follows.

Construct an actual trim and prove unique removed count, retained length and decoded coefficients against every other actual trim.

Every nonempty actual trim has the existing represented degree given by the predecessor of its retained length; the zero polynomial receives no degree.

Positive retained length constructs an actual represented degree, with no claim of a degree for empty output.

A canonical nonzero-leading representation trims to itself with zero removals, preserving its actual length and all decoded coefficients.

Every actual decoding of a monic leading coefficient is canonical one.

A monic prefix of annotated length S d has represented degree d, also for d=0.

Actual prefix reencoding preserves monicity, without constraining any outside entry.

The entire represented degree-zero monic prefix is the constant one, not an empty prefix.

The recorded scalar is an actual inverse of every decoding of the source leading coefficient.

Over a prime field the actual normalization scalar is nonzero; zero is never an inverse convention.

Each in-range output coefficient is the actual canonical product by the recorded inverse scalar.

The recorded scalar and every source and target coefficient are genuinely below the modulus.

The actual scaled leading coefficient equals one by the recorded inverse, not by a monic output premise.

Normalization yields a nonempty canonical monic prefix; all three properties are proved.

Scaling by the actual leading inverse preserves the annotated nonzero represented degree exactly.

Construct an actual inverse and actual scaled beta prefix from a canonical nonzero-leading representation over any prime, including two.

The recorded canonical leading inverse is unique even when the source and target beta encodings are not.

Two actual normalizations have the same decoded length-L prefix; beta-code equality is deliberately not asserted.

Every pair of actual in-range output decodings agrees; no claim is made for indices outside the prefix.

Reencode both actual coefficient prefixes while retaining the same genuine leading inverse and scale relation.

An already monic prefix normalizes by the actual scalar one using its original beta codes.

Every actual normalization of a nonzero constant representation is the constant one.

Construct a monic normalization of the same represented degree, with unique inverse scalar and unique decoded coefficient prefix.

Construct the normalized constant-one prefix from every actual nonzero represented constant over a prime field.

Every bounded prefix of a genuine Horner history is a genuine execution with its actually decoded terminal state.

All actually decoded states of a canonical Horner history are canonical field elements, including its initial and terminal states.

Construct the actual quotient code and remainder from a real modular Horner history, for every nonempty canonical coefficient prefix.

The synthetic remainder is the actual evaluation of the original input at the divisor root, not an assumed result certificate.

Each decoded quotient coefficient is precisely the actual Horner value of the corresponding nonempty input prefix.

The constructively encoded quotient has canonical coefficients at every one of its n positions; this includes an empty quotient for constants.

Every actual synthetic remainder is a canonical field value.

The remainder and all decoded quotient values are unique, independently of either beta encoding or the chosen execution history.

An actual one-step execution returns the decoded constant coefficient; coefficient bounds follow from the execution itself.

Adjacent actual prefix values satisfy the genuine multiply-then-add recurrence, even when their execution histories use different codes.

For a nonempty quotient its leading coefficient equals the original leading coefficient, including zero when the input has leading zeros.

Interior quotient coefficients satisfy q[i+1]=a*q[i]+f[i+1] by actual field operations, with the highest-degree-first indices explicit.

The remainder satisfies r=a*q[last]+f[last] by genuine canonical multiplication and addition.

Synthetic division of a nonzero-leading polynomial of positive represented degree S n produces a quotient of represented degree exactly n.

A constant has an empty quotient and its own coefficient as remainder, without assigning a degree to the empty quotient.

Every nonempty canonical input has a constructively encoded synthetic quotient and remainder, unique in decoded values rather than raw codes.

The actual synthetic remainder vanishes exactly when the actual input evaluation at a vanishes; a general convolution factor theorem remains a separate obligation.