Prime-Field Polynomial Euclidean Division — Exact Proof Explorer

A genuine antidiagonal term below a shared left prefix survives changing its code and its declared input length.

The same actual first-N antidiagonal table remains valid after a left input prefix extension.

Every coefficient below the shared prefix is unchanged, with its actual diagonal and sum witnesses reused verbatim.

Appending one quotient coefficient cannot alter any already constructed earlier convolution coefficient.

At diagonal index N the absent N-th entry of a length-N left prefix contributes actual zero.

The sole new last antidiagonal term is exactly the appended coefficient times the nonempty right prefix head.

Compare two independently coded actual antidiagonal sums: their first N terms agree and their last terms are zero and the new leading product.

Appending a quotient coefficient changes its new convolution position by exactly its actual field product with the divisor head; all sum and residue witnesses are real.

A coefficient indexed by its power is genuinely inside the highest-degree-first prefix.

Every index in an actual left-padded window is in its zero block or has an actual bounded source index.

A power beyond the source degree can only access the actual added leading-zero block.

Every natural power has an actual decoded coefficient or the proved exterior zero, for arbitrary beta encodings.

The actual coefficient of a formal power is unique, including the exterior and empty-prefix cases.

An exact decoded-prefix recoding preserves every formal coefficient at the same annotated length.

Formal coefficient equivalence is symmetric without choosing canonical raw beta codes.

Transitivity obtains an actual intermediate coefficient; it never assumes existential decoding.

The inherited same-length decoded equality implies formal polynomial equivalence.

At a common annotated length, formal coefficient equivalence gives the exact inherited decoded-prefix equality.

Zero left padding uses the original code and changes no coefficient.

Finite induction genuinely constructs the zero block and appends every actual input coefficient, including empty input and arbitrary encodings.

Each copied coefficient is identified with the actual source value, without identifying codes.

Actual leading-zero padding preserves canonical prime-field bounds at its exact enlarged length.

Any two constructed left pads have equal decoded coefficients on the full padded length.

A real suffix after an actual zero block gives the reverse decoding needed by genuine left padding.

Actual trimming identifies its input as the retained coefficient prefix with exactly the removed leading zeros restored.

Adding actual leading zeros preserves each formal power coefficient, including the zero coefficients above the old leading power.

Leading-zero padding is harmless for formal polynomial coefficients, unlike right padding by trailing zeros.

The actually constructed trimmed representation has exactly the same formal coefficients as its original input.

Input and full-output recoding preserve the actual leading-zero block and every copied coefficient.

Common actual leading-zero padding preserves the genuine aligned add coefficient operation, including empty prefixes.

Common actual leading-zero padding preserves the genuine aligned subtract coefficient operation, including empty prefixes.

Common actual leading-zero padding preserves the genuine aligned scale coefficient operation, including empty prefixes.

Every formal power coefficient of an actual zero prefix is zero, including exterior powers.

An actual all-zero ambient convolution prefix represents the same formal polynomial as an empty product.

The actual antidiagonal coefficient with a length-one right factor is its actual scalar product, by triangular append and proved vanished prior support.

An actual proper-length constant-right polynomial product is the existing actual coefficient scalar action.

Recover a genuine convolution from scalar action by constructing every antidiagonal sum and identifying its residue, including the empty product case.

An actual inverse scalar gives the reverse coefficient action, with a constructed intermediate table and exact decoded transport; no unit-associate law is assumed.

The actual inverse scalar solves the triangular coefficient equation, including prime two and an arbitrary nonzero divisor head.

An execution step depends only on the actual previously built quotient prefix, never on unused beta entries.

The actual empty quotient execution exists for all encodings and makes no assertion about an unused scalar or entry.

Every earlier portion of an actual quotient execution is the same execution prefix.

Every actual bounded decoded quotient value has the exact subtraction-and-inverse-product execution witnesses.

The computed quotient prefix is canonical because every stored value is an actual bounded field-product output.

An actual beta-prefix extension preserves all earlier steps and adds the independently computed next quotient value.

Construct every quotient coefficient with actual sum, subtraction, inverse-scaling and beta-extension witnesses, by ordinary finite induction.

Every actual convolution coefficient below the constructed quotient length equals the corresponding input coefficient, proved from the execution rather than assumed.

The actual ambient product table agrees with the input throughout the computed quotient prefix, including the vacuous zero-length case.

Subtracting the constructed product gives an actually all-zero leading prefix of the residual table.

Construct the true nonnegative quotient length: zero for a shorter input, otherwise the positive difference L-d.

The constructed quotient prefix fits in the input and its length plus the divisor degree covers every input coefficient.

A normalized trim cannot stop inside a proved all-zero leading prefix; empty output is treated separately.

The actual trimmed residual has at most d coefficients after a length-q zero prefix is proved; no degree is assigned to the empty case.

An actual normalized remainder of length at most d is empty or has an actual represented degree strictly below d, even when d=0.

Construct the actual divisor head, inverse, quotient length and quotient table as one small independently checked construction stage.

Construct the actual ambient product, residual and normalized trim as a separate stage; none is supplied as an oracle or identity premise.

Construct general quotient and normalized remainder codes from any canonical input and actual nonzero divisor, without assuming any output identity or degree bound.

Every actual constructed remainder is empty or has genuinely represented degree below the divisor degree, including constant divisors and empty inputs.

Unconditionally construct an actual general division execution and derive its strict remainder-degree alternative; no theorem claims degree for zero.

A positive constructed quotient has exactly the proper product length L with the length-S d divisor.

For a nonempty quotient the actual ambient product is the actual proper polynomial convolution, not a Horner or synthetic surrogate.

An actual ambient convolution prefix of an empty quotient consists entirely of zero coefficients, regardless of its requested length.

Derive the actual coefficient identity A=P+U, where P is the proper product Q*B (or padded empty product), and the actual trim makes U precisely a leading-zero representation of the normalized remainder.

Actual pointwise additive congruences lift by finite induction to the three actual Sum endpoints, for every modulus and also for the empty prefix.

An actual coefficient sum extends by actual zeros to an additive congruence at every index; no claim is made about arbitrary decoded entries outside the original prefixes.

At one actual antidiagonal position, left multiplication carries the genuine padded coefficient sum to the sum of the two genuine multiplication terms modulo the same modulus.

At one actual antidiagonal position, right multiplication carries the genuine padded coefficient sum to the sum of the two genuine multiplication terms modulo the same modulus.

The three independently beta-coded actual antidiagonal sums obey left additive congruence, including empty sum prefixes and with no raw-code equality.

The three independently beta-coded actual antidiagonal sums obey right additive congruence, including empty sum prefixes and with no raw-code equality.

Three genuine convolution coefficients satisfy actual canonical field addition under left distributivity, proved from their independently witnessed natural sums and residues.

Three genuine convolution coefficients satisfy actual canonical field addition under right distributivity, proved from their independently witnessed natural sums and residues.

Every requested ambient output prefix of the three actual left products satisfies actual coefficientwise addition, including N=0 and prefixes extending past product support.

Every requested ambient output prefix of the three actual right products satisfies actual coefficientwise addition, including N=0 and prefixes extending past product support.

The three genuine left convolution prefixes preserve actual field subtraction coefficient by coefficient, with characteristic two and arbitrary beta reencodings included.

The three genuine right convolution prefixes preserve actual field subtraction coefficient by coefficient, with characteristic two and arbitrary beta reencodings included.

The existing proper-length convolution graphs obey actual left add distributivity; this is a formal coefficient law, not an evaluation test.

The existing proper-length convolution graphs obey actual right add distributivity; this is a formal coefficient law, not an evaluation test.

The existing proper-length convolution graphs obey actual left subtract distributivity; this is a formal coefficient law, not an evaluation test.

The existing proper-length convolution graphs obey actual right subtract distributivity; this is a formal coefficient law, not an evaluation test.

Construct all three genuine proper-length left products and then prove their coefficient-addition identity; the product witnesses and the distributive conclusion are outputs, never input assumptions.

Construct all three genuine proper-length right products and then prove their coefficient-addition identity; the product witnesses and the distributive conclusion are outputs, never input assumptions.

An actual triangular execution step has one decoded output, by beta and convolution functionality, additive cancellation, and product functionality.

Two genuine steps with equal previously computed coefficients agree, even when their beta encodings and unused entries differ.

Finite induction proves coefficientwise uniqueness of the actual quotient recursion, with no claim about beta code identity or unused entries.

The actual short-input or positive-length quotient convention determines exactly one natural length, including L=0 and d=0.

Actual trim witnesses transport under equality of the annotated input prefix, including its zero prefix and genuinely shifted suffix.

The actual divisor head, inverse, quotient length, and decoded quotient coefficients are unique; no primality or code-number equality is inserted.

Equal decoded quotients give equal actual ambient products and residuals, hence identical trim lengths and coefficientwise equal normalized remainders.

Two actual executions on the same annotated inputs agree in quotient and remainder lengths and decoded coefficients, not in beta codes.

Construct the actual execution over a prime field with nonzero divisor head and prove its coefficientwise uniqueness against every other execution.

Leading-zero padding preserves every shifted zero-extended coefficient, including indices outside the original finite prefix.

Every position in the actual added leading block has zero extended value zero; no source coefficient is read.

An actually zero prefix remains zero after genuine left padding, including an originally empty factor.

Two actual natural sum traces have equal totals when one term prefix is the genuine leading-zero padding of the other.

Appending a genuinely all-zero tail to an independently recoded natural summand prefix preserves its actual sum.

A genuine left factor leading-zero padding shifts the antidiagonal position while preserving each actual natural product term.

A genuine right factor leading-zero padding shifts the antidiagonal position while preserving each actual natural product term.

A genuine antidiagonal term is zero when its left factor index lies in the actual leading padding block.

A genuine antidiagonal term is zero when its right factor index lies in the actual leading padding block.

The two actual antidiagonal tables differ by a proved leading zero block and exact copied natural summands.

The two actual antidiagonal tables differ by a proved trailing zero block and exact copied natural summands.

Construct an actual padded antidiagonal table and actual sum trace, proving the shifted coefficient has the same canonical residue without assuming an equality of sums.

Construct an actual padded antidiagonal table and actual sum trace, proving the shifted coefficient has the same canonical residue without assuming an equality of sums.

Every actual convolution coefficient before the added leading block is zero at a nonzero modulus.

Every actual convolution coefficient before the added leading block is zero at a nonzero modulus.

For two nonempty input representations, padding the left factor increases the actual product length by exactly the padding count; empty factors are excluded explicitly.

For two nonempty input representations, padding the right factor increases the actual product length by exactly the padding count; empty factors are excluded explicitly.

Two actual nonempty-factor products are related by exact leading-zero output padding and its proved length equation; no raw beta-code equality is asserted.

Two actual nonempty-factor products are related by exact leading-zero output padding and its proved length equation; no raw beta-code equality is asserted.

Genuine leading-zero padding of the left factor preserves the formal polynomial product, including empty factors whose proper product lengths need not differ by the padding count.

Genuine leading-zero padding of the right factor preserves the formal polynomial product, including empty factors whose proper product lengths need not differ by the padding count.

Construct an actual intermediate product and compose the two proved factor-padding compatibilities; both empty and nonempty factors are covered.

For actual leading-zero paddings over a prime field, construct a genuine proper-length product and prove its formal equivalence to the original product; no output certificate or identity is supplied.

Formal equivalence to a prefix of length t+L forces its actual leading-zero block and every copied source coefficient; construct a real padding and transport it by decoded equality, with no prime assumption.

Actual add outputs inherit the genuine common leading-zero padding of their inputs: construct a padded original output, prove its operation, then identify the supplied output by functionality.

Actual subtract outputs inherit the genuine common leading-zero padding of their inputs: construct a padded original output, prove its operation, then identify the supplied output by functionality.

Pairwise formal-equivalent inputs give formal-equivalent actual add outputs at either ordering of the two aligned lengths, including empty prefixes; no output equivalence or raw-code equality is assumed.

Pairwise formal-equivalent inputs give formal-equivalent actual subtract outputs at either ordering of the two aligned lengths, including empty prefixes; no output equivalence or raw-code equality is assumed.

Formal coefficient equivalence of the left factor preserves two actual products at arbitrary representation lengths, including empty factors; actual leading padding is recovered in the appropriate direction.

Formal coefficient equivalence of the right factor preserves two actual products at arbitrary representation lengths, including empty factors; actual leading padding is recovered in the appropriate direction.

Two actual convolution outputs represent the same formal polynomial whenever their respective factors do, with all four representation lengths independent. A genuine mixed product is constructed from canonical inputs supplied by the actual products; no output identity or extra field hypothesis is assumed.