ND0339

PolynomialQuotientLength(L,d,q)

The representation length q is zero with L<=d, or q is nonzero with q+d=L. Here the divisor has length S d. This specifies max(L-d,0) without a subtraction function and says nothing about the resulting polynomial degree or a quotient identity.

Conservative notation; not a theorem, primitive, or axiom.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Definition in prerequisite notation

q = 0 ∧ Le(L,d) ∨ ¬q = 0 ∧ q + d = L

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
(((((q))=0) /\ ((exists pfc_gap_working_euclidean_definitionshort. pfc_gap_working_euclidean_definitionshort+((L))=((d)))))) \/ (((~(((q))=0)) /\ ((((q))+((d))=((L))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Le(a,b)

Definitions depending on this notation

FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R)

Checked theorems using this definition

PX0032 · polynomial_quotient_length_existsPX0033 · polynomial_quotient_length_boundsPX0037 · prime_field_polynomial_division_quotient_data_existsPX0039 · prime_field_polynomial_division_execution_existsPX003C · polynomial_quotient_length_productPX003D · prime_field_polynomial_quotient_proper_productPX0055 · polynomial_quotient_length_functionalPX0057 · prime_field_polynomial_division_quotient_data_functional