PQ0017 — prime_field_polynomial_subtract_equal_entry_zero

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

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ l. ∀ i. ∀ a. ∀ r. Prime(p) → FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l) → Lt(i,l) → BetaAt(ab,ac,i,a) → BetaAt(bb,bc,i,a) → BetaAt(rb,rc,i,r) → r = 0

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1 Lt(a,b) · 1 Prime(p) · 1 BetaAt(b,c,i,x) · 3

Actual proof prerequisites

prime_field_subtract_equal_zero prime_field_polynomial_subtract_entry

Original expanded first-order statement

forall p ab ac bb bc rb rc l i a r. (~((p) = 1) /\ forall pfa_factor_left_sub_entry_zero_prime pfa_factor_right_sub_entry_zero_prime. (p) = pfa_factor_left_sub_entry_zero_prime * pfa_factor_right_sub_entry_zero_prime -> pfa_factor_left_sub_entry_zero_prime = 1 \/ pfa_factor_right_sub_entry_zero_prime = 1) -> (forall pfs_index_sub_entry_zero_graph. (exists pfa_gap_sub_entry_zero_graphindex. pfa_gap_sub_entry_zero_graphindex + S (pfs_index_sub_entry_zero_graph) = (l)) -> exists pfs_left_sub_entry_zero_graph pfs_right_sub_entry_zero_graph pfs_result_sub_entry_zero_graph. ((((exists ff_h_pfp_sub_entry_zero_graphleft. ff_h_pfp_sub_entry_zero_graphleft + S (pfs_left_sub_entry_zero_graph) = S ((S (pfs_index_sub_entry_zero_graph)) * ac)) /\ exists ff_q_pfp_sub_entry_zero_graphleft. ab = ff_q_pfp_sub_entry_zero_graphleft * S ((S (pfs_index_sub_entry_zero_graph)) * ac) + (pfs_left_sub_entry_zero_graph))) /\ (((((exists ff_h_pfp_sub_entry_zero_graphright. ff_h_pfp_sub_entry_zero_graphright + S (pfs_right_sub_entry_zero_graph) = S ((S (pfs_index_sub_entry_zero_graph)) * bc)) /\ exists ff_q_pfp_sub_entry_zero_graphright. bb = ff_q_pfp_sub_entry_zero_graphright * S ((S (pfs_index_sub_entry_zero_graph)) * bc) + (pfs_right_sub_entry_zero_graph))) /\ (((((exists ff_h_pfp_sub_entry_zero_graphresult. ff_h_pfp_sub_entry_zero_graphresult + S (pfs_result_sub_entry_zero_graph) = S ((S (pfs_index_sub_entry_zero_graph)) * rc)) /\ exists ff_q_pfp_sub_entry_zero_graphresult. rb = ff_q_pfp_sub_entry_zero_graphresult * S ((S (pfs_index_sub_entry_zero_graph)) * rc) + (pfs_result_sub_entry_zero_graph))) /\ ((((exists pfa_gap_sub_entry_zero_graphoperationleft. pfa_gap_sub_entry_zero_graphoperationleft + S (pfs_right_sub_entry_zero_graph) = (p)) /\ (((exists pfa_gap_sub_entry_zero_graphoperationright. pfa_gap_sub_entry_zero_graphoperationright + S (pfs_result_sub_entry_zero_graph) = (p)) /\ ((((exists pfa_gap_sub_entry_zero_graphoperationresultbound. pfa_gap_sub_entry_zero_graphoperationresultbound + S (pfs_left_sub_entry_zero_graph) = (p)) /\ ((exists pfa_offset_left_sub_entry_zero_graphoperationresultcongruence pfa_offset_right_sub_entry_zero_graphoperationresultcongruence. ((pfs_right_sub_entry_zero_graph) + (pfs_result_sub_entry_zero_graph)) + (p) * pfa_offset_left_sub_entry_zero_graphoperationresultcongruence = (pfs_left_sub_entry_zero_graph) + (p) * pfa_offset_right_sub_entry_zero_graphoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_sub_entry_zero_index. pfa_gap_sub_entry_zero_index + S (i) = (l)) -> (((exists ff_h_pfp_sub_entry_zero_a. ff_h_pfp_sub_entry_zero_a + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_sub_entry_zero_a. ab = ff_q_pfp_sub_entry_zero_a * S ((S (i)) * ac) + (a))) -> (((exists ff_h_pfp_sub_entry_zero_b. ff_h_pfp_sub_entry_zero_b + S (a) = S ((S (i)) * bc)) /\ exists ff_q_pfp_sub_entry_zero_b. bb = ff_q_pfp_sub_entry_zero_b * S ((S (i)) * bc) + (a))) -> (((exists ff_h_pfp_sub_entry_zero_r. ff_h_pfp_sub_entry_zero_r + S (r) = S ((S (i)) * rc)) /\ exists ff_q_pfp_sub_entry_zero_r. rb = ff_q_pfp_sub_entry_zero_r * S ((S (i)) * rc) + (r))) -> r=0

Complete tactic proof in conservative notation

All 40 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

40 script commands · 5 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)

prime field subtract equal zero prime field polynomial subtract entry

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.