PQ0019 — prime_field_polynomial_subtract_add_cancel

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 cb cc rb rc l. (forall pfp_index_sub_cancel_sum. (exists pfa_gap_sub_cancel_sumindex. pfa_gap_sub_cancel_sumindex + S (pfp_index_sub_cancel_sum) = (l)) -> exists pfp_left_sub_cancel_sum pfp_right_sub_cancel_sum pfp_value_sub_cancel_sum. ((((exists ff_h_pfp_sub_cancel_sumleft. ff_h_pfp_sub_cancel_sumleft + S (pfp_left_sub_cancel_sum) = S ((S (pfp_index_sub_cancel_sum)) * ac)) /\ exists ff_q_pfp_sub_cancel_sumleft. ab = ff_q_pfp_sub_cancel_sumleft * S ((S (pfp_index_sub_cancel_sum)) * ac) + (pfp_left_sub_cancel_sum))) /\ (((((exists ff_h_pfp_sub_cancel_sumright. ff_h_pfp_sub_cancel_sumright + S (pfp_right_sub_cancel_sum) = S ((S (pfp_index_sub_cancel_sum)) * bc)) /\ exists ff_q_pfp_sub_cancel_sumright. bb = ff_q_pfp_sub_cancel_sumright * S ((S (pfp_index_sub_cancel_sum)) * bc) + (pfp_right_sub_cancel_sum))) /\ (((((exists ff_h_pfp_sub_cancel_sumtarget. ff_h_pfp_sub_cancel_sumtarget + S (pfp_value_sub_cancel_sum) = S ((S (pfp_index_sub_cancel_sum)) * cc)) /\ exists ff_q_pfp_sub_cancel_sumtarget. cb = ff_q_pfp_sub_cancel_sumtarget * S ((S (pfp_index_sub_cancel_sum)) * cc) + (pfp_value_sub_cancel_sum))) /\ ((((exists pfa_gap_sub_cancel_sumoperationleft. pfa_gap_sub_cancel_sumoperationleft + S (pfp_left_sub_cancel_sum) = (p)) /\ (((exists pfa_gap_sub_cancel_sumoperationright. pfa_gap_sub_cancel_sumoperationright + S (pfp_right_sub_cancel_sum) = (p)) /\ ((((exists pfa_gap_sub_cancel_sumoperationresultbound. pfa_gap_sub_cancel_sumoperationresultbound + S (pfp_value_sub_cancel_sum) = (p)) /\ ((exists pfa_offset_left_sub_cancel_sumoperationresultcongruence pfa_offset_right_sub_cancel_sumoperationresultcongruence. ((pfp_left_sub_cancel_sum) + (pfp_right_sub_cancel_sum)) + (p) * pfa_offset_left_sub_cancel_sumoperationresultcongruence = (pfp_value_sub_cancel_sum) + (p) * pfa_offset_right_sub_cancel_sumoperationresultcongruence)))))))))))))))) -> (forall pfs_index_sub_cancel_difference. (exists pfa_gap_sub_cancel_differenceindex. pfa_gap_sub_cancel_differenceindex + S (pfs_index_sub_cancel_difference) = (l)) -> exists pfs_left_sub_cancel_difference pfs_right_sub_cancel_difference pfs_result_sub_cancel_difference. ((((exists ff_h_pfp_sub_cancel_differenceleft. ff_h_pfp_sub_cancel_differenceleft + S (pfs_left_sub_cancel_difference) = S ((S (pfs_index_sub_cancel_difference)) * cc)) /\ exists ff_q_pfp_sub_cancel_differenceleft. cb = ff_q_pfp_sub_cancel_differenceleft * S ((S (pfs_index_sub_cancel_difference)) * cc) + (pfs_left_sub_cancel_difference))) /\ (((((exists ff_h_pfp_sub_cancel_differenceright. ff_h_pfp_sub_cancel_differenceright + S (pfs_right_sub_cancel_difference) = S ((S (pfs_index_sub_cancel_difference)) * ac)) /\ exists ff_q_pfp_sub_cancel_differenceright. ab = ff_q_pfp_sub_cancel_differenceright * S ((S (pfs_index_sub_cancel_difference)) * ac) + (pfs_right_sub_cancel_difference))) /\ (((((exists ff_h_pfp_sub_cancel_differenceresult. ff_h_pfp_sub_cancel_differenceresult + S (pfs_result_sub_cancel_difference) = S ((S (pfs_index_sub_cancel_difference)) * rc)) /\ exists ff_q_pfp_sub_cancel_differenceresult. rb = ff_q_pfp_sub_cancel_differenceresult * S ((S (pfs_index_sub_cancel_difference)) * rc) + (pfs_result_sub_cancel_difference))) /\ ((((exists pfa_gap_sub_cancel_differenceoperationleft. pfa_gap_sub_cancel_differenceoperationleft + S (pfs_right_sub_cancel_difference) = (p)) /\ (((exists pfa_gap_sub_cancel_differenceoperationright. pfa_gap_sub_cancel_differenceoperationright + S (pfs_result_sub_cancel_difference) = (p)) /\ ((((exists pfa_gap_sub_cancel_differenceoperationresultbound. pfa_gap_sub_cancel_differenceoperationresultbound + S (pfs_left_sub_cancel_difference) = (p)) /\ ((exists pfa_offset_left_sub_cancel_differenceoperationresultcongruence pfa_offset_right_sub_cancel_differenceoperationresultcongruence. ((pfs_right_sub_cancel_difference) + (pfs_result_sub_cancel_difference)) + (p) * pfa_offset_left_sub_cancel_differenceoperationresultcongruence = (pfs_left_sub_cancel_difference) + (p) * pfa_offset_right_sub_cancel_differenceoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_sub_cancel_result mdr_a_pfp_sub_cancel_result. (exists mdr_gap_pfp_sub_cancel_resultb. mdr_gap_pfp_sub_cancel_resultb + S (mdr_i_pfp_sub_cancel_result) = (l)) -> (((exists ff_h_mdr_pfp_sub_cancel_resulto. ff_h_mdr_pfp_sub_cancel_resulto + S (mdr_a_pfp_sub_cancel_result) = S ((S (mdr_i_pfp_sub_cancel_result)) * bc)) /\ exists ff_q_mdr_pfp_sub_cancel_resulto. bb = ff_q_mdr_pfp_sub_cancel_resulto * S ((S (mdr_i_pfp_sub_cancel_result)) * bc) + (mdr_a_pfp_sub_cancel_result))) -> (((exists ff_h_mdr_pfp_sub_cancel_resultn. ff_h_mdr_pfp_sub_cancel_resultn + S (mdr_a_pfp_sub_cancel_result) = S ((S (mdr_i_pfp_sub_cancel_result)) * rc)) /\ exists ff_q_mdr_pfp_sub_cancel_resultn. rb = ff_q_mdr_pfp_sub_cancel_resultn * S ((S (mdr_i_pfp_sub_cancel_result)) * rc) + (mdr_a_pfp_sub_cancel_result))))

Constructive proof overview

Generated structural guide

Subtracting the actual first addend from an actual sum recovers the other addend by represented-prefix equality.

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

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

Proof neighborhood

Direct dependencies

PQ0010 prime_field_polynomial_subtract_functional PQ0013 prime_field_polynomial_subtract_from_add

Direct dependents

none

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

34 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 polynomial subtract functional prime field polynomial subtract from add

01Fix variables and assumptionsL1–10

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