ND0327

FpCoefficientNegation(p,ab,ac,rb,rc,L)

At each strict index i<L, actual beta source and result coefficients satisfy FpNeg(p,a,r), namely bounded field addition a+r=0. The common representation length and highest-degree-first order are retained. Empty prefixes impose no coefficient condition, even at p=0; existence for canonical prime-field inputs is a separate theorem.

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

∀ pfs_index_polynomial_division_definition. Lt(pfs_index_polynomial_division_definition,L) → ∃ x. ∃ y. BetaAt(ab,ac,pfs_index_polynomial_division_definition,x) ∧ (BetaAt(rb,rc,pfs_index_polynomial_division_definition,y) ∧ FpAdd(p,x,y,0))

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

Hygienic expanded first-order definition 
forall pfs_index_polynomial_division_definition. (exists pfa_gap_polynomial_division_definitionindex. pfa_gap_polynomial_division_definitionindex + S (pfs_index_polynomial_division_definition) = ((L))) -> exists pfs_source_polynomial_division_definition pfs_result_polynomial_division_definition. ((((exists ff_h_pfp_polynomial_division_definitionsource. ff_h_pfp_polynomial_division_definitionsource + S (pfs_source_polynomial_division_definition) = S ((S (pfs_index_polynomial_division_definition)) * (ac))) /\ exists ff_q_pfp_polynomial_division_definitionsource. (ab) = ff_q_pfp_polynomial_division_definitionsource * S ((S (pfs_index_polynomial_division_definition)) * (ac)) + (pfs_source_polynomial_division_definition))) /\ (((((exists ff_h_pfp_polynomial_division_definitionresult. ff_h_pfp_polynomial_division_definitionresult + S (pfs_result_polynomial_division_definition) = S ((S (pfs_index_polynomial_division_definition)) * (rc))) /\ exists ff_q_pfp_polynomial_division_definitionresult. (rb) = ff_q_pfp_polynomial_division_definitionresult * S ((S (pfs_index_polynomial_division_definition)) * (rc)) + (pfs_result_polynomial_division_definition))) /\ ((((exists pfa_gap_polynomial_division_definitionoperationadditionleft. pfa_gap_polynomial_division_definitionoperationadditionleft + S (pfs_source_polynomial_division_definition) = ((p))) /\ (((exists pfa_gap_polynomial_division_definitionoperationadditionright. pfa_gap_polynomial_division_definitionoperationadditionright + S (pfs_result_polynomial_division_definition) = ((p))) /\ ((((exists pfa_gap_polynomial_division_definitionoperationadditionresultbound. pfa_gap_polynomial_division_definitionoperationadditionresultbound + S (0) = ((p))) /\ ((exists pfa_offset_left_polynomial_division_definitionoperationadditionresultcongruence pfa_offset_right_polynomial_division_definitionoperationadditionresultcongruence. ((pfs_source_polynomial_division_definition) + (pfs_result_polynomial_division_definition)) + ((p)) * pfa_offset_left_polynomial_division_definitionoperationadditionresultcongruence = (0) + ((p)) * pfa_offset_right_polynomial_division_definitionoperationadditionresultcongruence)))))))))))))

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

Direct definition dependencies

Lt(a,b)BetaAt(b,c,i,x)FpNeg(p,a,b)

Definitions depending on this notation

none

Checked theorems using this definition

PQ0003 · prime_field_polynomial_negate_emptyPQ0004 · prime_field_polynomial_negate_existsPQ0005 · prime_field_polynomial_negate_entryPQ0006 · prime_field_polynomial_negate_boundedPQ0007 · prime_field_polynomial_negate_functionalPQ0008 · prime_field_polynomial_negate_transportPQ0009 · prime_field_polynomial_negate_involutivePQ000A · prime_field_polynomial_negate_zeroPQ000B · prime_field_polynomial_negate_add_zeroPQ0016 · prime_field_polynomial_subtract_zero_left