ND0292

PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t)

Witness k with j+k=i and multiply the two actual zero-extended coefficients. These are natural products in a highest-degree-first antidiagonal, before reduction modulo the field prime.

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

∃ pfc_complement_lowercontinuation. ∃ pfc_left_lowercontinuation. ∃ pfc_right_lowercontinuation. j + pfc_complement_lowercontinuation = i ∧ (BetaZeroExtend(ab,ac,L,j,pfc_left_lowercontinuation) ∧ (BetaZeroExtend(bb,bc,M,pfc_complement_lowercontinuation,pfc_right_lowercontinuation) ∧ t = pfc_left_lowercontinuation · pfc_right_lowercontinuation))

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

Hygienic expanded first-order definition 
exists pfc_complement_lowercontinuation pfc_left_lowercontinuation pfc_right_lowercontinuation. ((((j))+pfc_complement_lowercontinuation=((i))) /\ ((((((exists pfa_gap_lowercontinuationleftinside. pfa_gap_lowercontinuationleftinside + S ((j)) = ((L))) /\ ((((exists ff_h_pfp_lowercontinuationleftentry. ff_h_pfp_lowercontinuationleftentry + S (pfc_left_lowercontinuation) = S ((S ((j))) * (ac))) /\ exists ff_q_pfp_lowercontinuationleftentry. (ab) = ff_q_pfp_lowercontinuationleftentry * S ((S ((j))) * (ac)) + (pfc_left_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationleftoutside. pfc_gap_lowercontinuationleftoutside+((L))=((j))) /\ (((pfc_left_lowercontinuation)=0))))) /\ ((((((exists pfa_gap_lowercontinuationrightinside. pfa_gap_lowercontinuationrightinside + S (pfc_complement_lowercontinuation) = ((M))) /\ ((((exists ff_h_pfp_lowercontinuationrightentry. ff_h_pfp_lowercontinuationrightentry + S (pfc_right_lowercontinuation) = S ((S (pfc_complement_lowercontinuation)) * (bc))) /\ exists ff_q_pfp_lowercontinuationrightentry. (bb) = ff_q_pfp_lowercontinuationrightentry * S ((S (pfc_complement_lowercontinuation)) * (bc)) + (pfc_right_lowercontinuation)))))) \/ (((exists pfc_gap_lowercontinuationrightoutside. pfc_gap_lowercontinuationrightoutside+((M))=(pfc_complement_lowercontinuation)) /\ (((pfc_right_lowercontinuation)=0))))) /\ ((((t))=pfc_left_lowercontinuation*pfc_right_lowercontinuation)))))))

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

Direct definition dependencies

BetaZeroExtend(b,c,L,i,a)

Definitions depending on this notation

PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l)

Checked theorems using this definition

PG0007 · polynomial_diagonal_term_shift_right_iffPG0008 · prime_field_convolution_coefficient_shift_right_iffPG0012 · polynomial_diagonal_term_right_scale_congruentPG002D · polynomial_diagonal_left_unit_first_termPG002E · polynomial_diagonal_left_unit_tail_termPG002F · polynomial_diagonal_left_unit_natural_sumPG004D · polynomial_diagonal_left_constant_first_termPG004E · polynomial_diagonal_left_constant_natural_sum