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.

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

Equal aligned coefficients, in particular equal leading coefficients, leave actual zero at that result position.

The unchanged tactic script uses 2 declared prerequisites and contains 40 exact native proof lines.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PQ0002 prime_field_subtract_equal_zero PQ000E prime_field_polynomial_subtract_entry

Direct dependents

PQ0018 prime_field_polynomial_subtract_equal_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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.