Prime-Field Polynomial GCD and Bézout — Exact Proof Explorer

Construct a genuine trailing-zero prefix by the original beta-prefix extension theorem, including an empty source.

A real trailing zero preserves canonical field coefficients; characteristic two uses natural zero and one, not signed codes.

Two actual shifts agree on their successor-length decoded prefix; neither raw code nor any later entry is identified.

The actual shift of an all-zero prefix is again all zero, including the length-one shift of an empty input.

Trailing-zero extension leaves each actual zero-extended array value unchanged, at every natural index.

Conversely every zero-extended value of an actual shift is the original zero-extended value; this is not formal polynomial equality.

An actual trailing-zero shift of the right factor preserves exactly the same antidiagonal term witnesses in both directions.

Every actual convolution coefficient is preserved at every index, with the identical natural sum and residue witnesses; no primality is needed.

For two nonempty factors, shifting the right factor raises the proper product length by exactly one; empty factors are explicitly excluded.

For actual nonempty factors, the shifted product is exactly a trailing-zero extension of the original decoded product, at its proved successor length.

If either original factor is empty, both actual products are zero prefixes; no false successor-length equation is imposed.

At every nonzero modulus, the actual product with a shifted right factor is formally coefficient-equivalent to every actual shift of the original product, including both empty-factor cases.

Given a genuine shifted factor, construct its proper-length product and a genuine shift of the original output, then derive their formal equivalence without any output witness premise.

The actual constant coefficient of a trailing-zero shift is zero, even when the original representation is empty.

Each actual coefficient at power k becomes the same coefficient at power S k; together with constant zero this is genuine multiplication by X, not evaluation equality.

Pointwise scalar congruences lift through two actual natural Sum traces at every modulus, including zero and the empty length; no new sum witness is assumed equal to a desired total.

Actual coefficient scaling extends by genuine exterior zeros to a scalar congruence at every array index, with no condition on raw entries after the prefixes.

The uniquely identified complementary index and unchanged left coefficient turn actual right-input scaling into pointwise antidiagonal scalar congruence.

Two actual antidiagonal tables and their actual natural sums satisfy scalar congruence; no supplied output identity or Fubini oracle is used.

At every natural index the actual scaled-input convolution coefficient is the actual canonical product of k and the original coefficient, including all exterior coefficients and composite moduli.

Scaling the actual right input preserves the proper representation length and gives the actual scalar action on the product output, including empty factors and zero scalars.

Every actual product A*(k B) agrees coefficientwise with every actual scalar result k*(A*B), at the same proper length; no equality of beta codes follows.

At any nonzero modulus and canonical scalar, construct the actual scaled input, its actual convolution, and an independently encoded scalar output, then derive their exact decoded-prefix agreement.

Every actual scalar-zero output is an actually all-zero prefix, without primality and without dropping the scalar bound on an empty input.

An actual product with a scalar-zero right input has a genuine zero output prefix at its actual proper length, including empty factors and composite nonzero moduli.

Every actual appended prefix is the actual aligned sum of a genuine trailing-zero shift and the leading-padded singleton constant; the last and earlier entries are proved separately, including M=0.

Construct the shifted old prefix, a canonical singleton constant and its genuine leading padding, then prove their actual aligned sum is the given appended prefix.

At every natural coefficient index, an actual right append is the actual field sum of the old convolution coefficient and the product with the padded singleton constant, using genuine diagonal sums and residues rather than a finite-evaluation identity.

Construct actual shift and scalar outputs, harmless leading paddings to the common length L+S N, and their actual coefficient sum; the commuted S N+L bound is explicitly reconciled, including both empty inputs.

An actual right-factor append satisfies A*append(C,c) formally equivalent to X*(A*C)+c*A through genuine products and arbitrary actual aligned sum outputs. Lengths are not falsely equated in empty cases, and no finite-field evaluation agreement replaces all formal coefficients.

From an actual old product and a canonical next coefficient, construct the appended right factor, its proper product, the shift and scalar outputs, both aligned paddings and the actual sum, then prove the formal recurrence. No output existence or polynomial identity is assumed.

Two actual trailing-zero shifts preserve formal coefficient equivalence across arbitrary represented lengths, including empty prefixes. The proof obtains actual predecessor-power coefficients and compares decoded values, without any modulus, primality, coefficient-bound, raw-code identity, or evaluation-equality assumption.

For actual AB and AQ, multiplying an actual leading-pad-aligned sum XQ+cB by A is formally equivalent to every actual aligned sum X(AQ)+c(AB). All four intermediate products are genuinely constructed, scalar and shift outputs remain actual graph witnesses, proper product lengths are independent, and no associativity hypothesis or output equality is assumed.

Formal equivalence of two old prefixes preserves every actual aligned sum of their trailing-zero shifts with a fixed actual scalar multiple of the same source. Both old lengths, all shift/scale encodings, both leading paddings and the sum encodings remain independent; only formal output coefficients are concluded equal.

An actual formal-coefficient associativity hypothesis for one rightmost prefix extends through one genuine appended coefficient. Every old and new product is an actual proper-length convolution; the proof derives the canonical appended coefficient bound, constructs three real shift/scale/pad/add alignments and a real intermediate product, and concludes only the next formal equivalence. Empty factors are retained, no successor product-length identity is assumed, and the induction step alone is not full associativity.

At every nonzero modulus, actual Q=B*empty, R=P*empty and S=A*Q have formally equivalent all-zero outputs, for arbitrary actual P. The argument constructs the genuine empty zero-prefix fact and transports it through the real products; it assumes neither P=AB nor an output-length shortcut.

Draft universal rightmost-length induction for formal equivalence of actual (A*B)*C and A*(B*C). The induction predicate quantifies all rightmost codes and proper-length output triples, the successor genuinely constructs three prefix products and decodes the actual endpoint, and the empty base retains arbitrary encodings. This statement is not a successful proof observation until its original body and its exact step dependency are genuinely checked.

A genuine proper-length Q*D and formal equivalence to a canonical target give actual right-factor divisibility, with the quotient and output witnesses retained.

The actual witnessed convolution supplies a canonical divisor prefix, including zero-length divisors.

Right-factor divisibility is a relation on canonical target prefixes, not on arbitrary unbounded coefficient encodings.

Changing the canonical target by all-power formal coefficient equivalence preserves the same genuine quotient/product witnesses, independently of representation length.

Every canonical divisor divides every encoding of the empty polynomial, using an actual empty quotient and actual empty product. No prime, nonzero modulus or nonempty divisor assumption is needed.

An equivalent canonical right divisor preserves divisibility by constructing the quotient times the replacement at its own actual proper length. Formal output congruence, not a supplied output identity, gives the new witness.

Actual Q1*D equivalent to A and Q2*A equivalent to B give the actual composite quotient Q2*Q1. Three genuine intermediate products, formal associativity and right-input congruence prove its product with D equivalent to B. No commutativity, fixed representation lengths or raw-code identities are assumed.

The first actual antidiagonal term of a length-one left unit is the chosen right-input coefficient, without any primality or commutativity assumption.

Every later term is zero because its left input index is outside a genuine length-one prefix. The value of that prefix is irrelevant here.

An actual unit-left antidiagonal sum equals its first coefficient: construct the one-term sum and use the proved zero-tail invariant on all remaining actual summands.

The actual residue of the unit-left natural sum is its already bounded right-input value. No polynomial equality is hidden among the premises.

Every coefficient of an actual length-L product U*A agrees with A when U is a length-one unit, including the vacuous L=0 case.

Actual left multiplication by a length-one unit preserves formal coefficients, not just evaluations or a selected encoding.

Construct an actual canonical length-one unit and its actual length-L left product, formally equal to A. The proper length is zero when A is empty.

Every canonical polynomial right-divides itself using a constructed left unit and actual product. Empty and zero prefixes are included, without assuming commutative multiplication.

From L<=K construct a genuine leading-zero beta prefix of length K, retain canonical coefficients, and prove formal equivalence to the input, including empty prefixes.

Two prefixes already at one length serve as their actual common representatives; no new beta encoding or prime premise is needed.

Independent formal recodings of the original inputs preserve the same actual common representatives, without asserting a padding length inequality.

Construct two actual canonical common-length representatives by independent leading-zero padding at any supplied common upper bound.

Use the explicit common length L+M to construct real canonical representatives for any two independently sized inputs, including zero lengths.

Any two choices of common representatives are pairwise formally equivalent, even at different common lengths; no raw-code or length uniqueness is asserted.

Swapping the two original inputs and their actual representatives preserves the common-representation graph.

Package actual common representatives, an actual coefficient sum, and formal output equivalence while retaining all three original canonical coefficient guards.

Aligned addition includes canonical coefficients for the actual originals and output, not merely for equivalent witnesses.

Every genuine fixed-length addition supplies its own actual common representatives and is an aligned addition, without an extra prime hypothesis.

Independent formal recoding of all three canonical originals preserves a real aligned sum; canonicality is never inferred solely from equivalence.

Actual aligned addition commutes by swapping its real common representatives and the checked coefficient addition.

Two actual aligned sums represent the same formal polynomial even when their witnesses, original output lengths, and beta codes differ.

Construct a genuine canonical aligned sum at the explicit length L+M from any two canonical inputs, rather than assuming operation witnesses.

Realize the addition on any supplied canonical equal-length representatives: construct a sum, prove formal output uniqueness, then transport the actual operation by decoded coefficient equality.

A genuine fixed-length subtraction is an aligned subtraction because its actual coefficient graph supplies B+R=A.

Construct actual aligned field subtraction at length L+M, using real canonical common representatives and the genuine solution B+R=A.

Cancel a common addend from actual aligned sums: construct four real common-length prefixes, realize both additions and apply checked coefficient subtraction functionality.

Both actual bracketings of three independently sized polynomials give formally equivalent outputs; all seven comparison prefixes and all four coefficient operations are genuinely constructed.

Actual aligned subtraction has a formally unique result, including unequal lengths and unrelated beta encodings.

An actual fixed-length sum and actual trim supply real common representatives for the canonical product and trimmed remainder; no prime premise or equality of unused beta entries is needed.

Every actual prime-field division execution yields an actual proper Q*B product and the aligned formal identity A=Q*B+R, including an empty quotient whose ambient zero product has a different length.

Actual left products distribute over an independently represented aligned sum: construct real equal-length products of its witnesses and prove formal equivalence to the three supplied outputs, including empty-factor cases.

Actual right products distribute over an independently represented aligned sum: construct real equal-length products of its witnesses and prove formal equivalence to the three supplied outputs, including empty-factor cases.

The first actual antidiagonal term of a genuine left singleton is the ordered natural product k*a. No modulus, coefficient bound, or commutativity premise is needed.

The actual finite natural sum equals k*a: construct its one-term sum and use the existing zero-tail invariant for every subsequent summand. The total need not itself be a canonical field coefficient.

Every actual in-range constant-left convolution coefficient is the canonical residue of the ordered product k*a. Both input bounds and the actual natural-sum witness are explicit; primality is unnecessary for this implication.

An actual length-L product of a canonical left singleton and a length-L prefix yields the existing scalar graph, even when L=0. The scalar bound follows from the singleton rather than from vacuous output entries.

Recover the genuine LEFT-constant convolution on the supplied scalar-output codes. Every needed antidiagonal sum is actually constructed and its residue identified; the empty proper-length branch is separate, including scalar zero and characteristic two.

Construct the canonical singleton and actual scalar output, then prove their genuine left-factor product using those same output codes. Empty source prefixes still require a canonical scalar and singleton; no beta-code uniqueness or gcd endpoint is claimed.

Every actual normalized remainder has retained length at most d and strictly less than the actual divisor length S d. The zero branch is handled directly; the nonzero branch uses its genuine represented-degree length equation.

Actual division by the nonzero degree-zero divisor produces an empty normalized remainder, including an empty dividend. This assigns no degree to the zero polynomial.

A genuine scalar output is a right multiple of its source: construct an actual LEFT singleton quotient and actual product, then transport the independently encoded product to the supplied target by decoded-prefix equality. Empty inputs and scalar zero are included.

An actual monic normalization and its genuinely inverted scalar action supply actual right-divisibility witnesses in both directions. These witnesses use left constant quotients; no polynomial commutativity, unit-associate oracle, or equality of beta codes is used.

Construct a zero-or-monic right associate of every canonical polynomial, first trimming its actual leading zeros and then normalizing only a nonempty trim. Both divisibility directions have real product witnesses and are transported to the original representation. Empty and all-zero encodings need no degree or inverse of zero.

A common actual right divisor divides the genuine aligned add: construct the corresponding quotient operation and its proper product, use checked right distributivity and compare real aligned sums.

A common actual right divisor divides the genuine aligned subtract: construct the corresponding quotient operation and its proper product, use checked right distributivity and compare real aligned sums.

An actual right divisor of B divides every actual left multiple Q*B; the composed quotient is supplied by the checked constructive transitivity theorem.

A genuine Euclidean identity A=Q*B+R preserves precisely the actual common right divisors in both directions, using constructed quotient sums and differences.

Every genuine polynomial division execution preserves common right divisors, including the empty quotient and zero remainder, with its aligned identity constructed from the execution.

From genuine products and the actual difference T=U-V*Q, prove G=V*A+T*B by ordered distributivity, actual convolution associativity and aligned addition reassociation; the desired sum is a conclusion.

Construct W=V*Q, T=U-W, and genuine new products to turn an actual Bezout representation for (B,R) into one for (A,B), with both coefficient-update graphs returned as witnesses.

A real division execution automatically supplies the proper Euclidean identity and constructs the exact backward Bezout coefficient update, including an empty quotient.

Construct a real zero prefix at the input length and its formal equivalence to the empty polynomial, giving an actual aligned right-zero sum for every canonical input.

An actual right multiple G of A supplies its real left quotient U. With the empty coefficient V, construct V*B and an actual aligned sum to give G=U*A+V*B. The second input only needs canonical coefficients.

Independently recode both inputs and the result by formal coefficient equivalence, retaining the same Bezout coefficients. Construct both new proper products; output equivalences are proved, not supplied as premises. No primality is needed beyond a nonzero modulus.

Every actual common right divisor of A and B divides any actual Bezout representative G=U*A+V*B. This is the greatestness implication, not an assertion that an arbitrary Bezout representative divides either input.

The actual trim inside division supplies canonical remainder coefficients, including its empty branch; no primality or degree of zero is assumed.

Construct a formally equivalent canonical representative of no greater retained length, either empty or with an actual nonzero leading coefficient and represented degree. This trims stored leading zeros without requiring a prime modulus.

Construct an already zero-or-monic common divisor and actual Bezout coefficients for (A,empty), using genuine mutual right-associate witnesses. Empty and all-zero A, including (0,0), require no inverse or degree of zero.

Replace the second input by any formally equivalent canonical representation while keeping the same zero-or-monic common divisor and the same Bezout coefficients; both new products remain witnessed.

Carry an already normalized common divisor through an actual Euclidean step. Construct the new coefficients V and U-V*Q from actual products and aligned subtraction, preserving the same G.

Ordinary natural induction constructs actual normalized gcd and Bezout witnesses for every pair with second retained length at most n. Both input triples are generalized, a stored zero divisor is trimmed before division, and every genuine recursive call has a proved smaller bound.

Take the actual second representation length as induction bound. No supplied quotient, gcd, degree, termination certificate, or Bezout coefficients are premises.

A common right divisor with an actual Bezout representation satisfies the full universally quantified greatestness property, including a zero gcd; no normalization assumption is needed.

Every pair of canonical polynomials over a prime field has an actual zero-or-monic greatest common right divisor and actual Bezout coefficients. The normalized-gcd definition and the existing Bezout graph occur literally in the conclusion.

A nonzero coefficient at the leading power cannot be matched by an outside-prefix zero. This length bound needs neither primality nor canonical coefficients.

Formal equivalence preserves genuine represented degree across independently encoded and independently length-annotated nonzero-leading prefixes.

An actual product formally equal to a nonzero-leading representation cannot have an empty left factor. No degree is assigned to empty factors.

Trim the actual quotient, construct an independent proper-length product, and transport formal coefficients. Its genuine nonzero degree e satisfies e+d=a; no quotient degree or domain cancellation is assumed.

A nonzero represented right divisor has degree at most that of its nonzero represented multiple, using the actual retained quotient degree as the natural witness.

Both monic heads force an actual left singleton quotient to have coefficient one, by the ordered leading product k*1. The genuine left-unit convolution law then gives formal equivalence.

Equal-degree monic right divisibility has a genuinely constructed degree-zero quotient. Its head must be one, so divisor and target are formally equivalent.

Mutual right divisibility forces equal represented degrees. Both actual monic normalizations then force formal coefficient equivalence, without selecting unique beta codes.

An empty right divisor has only formally zero multiples, at any target representation length. The actual product length is zero; no zero-degree assertion or prime hypothesis is used.

Two zero-or-monic mutual right associates are formally equivalent, including both-zero and one-empty branches. Both normalization premises are essential; beta encodings need not agree.

The grouped normal/common-divisor/greatestness graph yields mutual right associates, hence uniqueness only up to formal coefficient equivalence. This does not assert unique beta codes or Bezout coefficients.