Actual subtract outputs inherit the genuine common leading-zero padding of their inputs: construct a padded original output, prove its operation, then identify the supplied output by functionality.
Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable
Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.
forall p ab ac bb bc cb cc L t AB AC BB BC CB CC. (~((p) = 1) /\ forall pfa_factor_left_subtract_output_prime pfa_factor_right_subtract_output_prime. (p) = pfa_factor_left_subtract_output_prime * pfa_factor_right_subtract_output_prime -> pfa_factor_left_subtract_output_prime = 1 \/ pfa_factor_right_subtract_output_prime = 1) -> (forall pfs_index_subtract_output_original. (exists pfa_gap_subtract_output_originalindex. pfa_gap_subtract_output_originalindex + S (pfs_index_subtract_output_original) = (L)) -> exists pfs_left_subtract_output_original pfs_right_subtract_output_original pfs_result_subtract_output_original. ((((exists ff_h_pfp_subtract_output_originalleft. ff_h_pfp_subtract_output_originalleft + S (pfs_left_subtract_output_original) = S ((S (pfs_index_subtract_output_original)) * ac)) /\ exists ff_q_pfp_subtract_output_originalleft. ab = ff_q_pfp_subtract_output_originalleft * S ((S (pfs_index_subtract_output_original)) * ac) + (pfs_left_subtract_output_original))) /\ (((((exists ff_h_pfp_subtract_output_originalright. ff_h_pfp_subtract_output_originalright + S (pfs_right_subtract_output_original) = S ((S (pfs_index_subtract_output_original)) * bc)) /\ exists ff_q_pfp_subtract_output_originalright. bb = ff_q_pfp_subtract_output_originalright * S ((S (pfs_index_subtract_output_original)) * bc) + (pfs_right_subtract_output_original))) /\ (((((exists ff_h_pfp_subtract_output_originalresult. ff_h_pfp_subtract_output_originalresult + S (pfs_result_subtract_output_original) = S ((S (pfs_index_subtract_output_original)) * cc)) /\ exists ff_q_pfp_subtract_output_originalresult. cb = ff_q_pfp_subtract_output_originalresult * S ((S (pfs_index_subtract_output_original)) * cc) + (pfs_result_subtract_output_original))) /\ ((((exists pfa_gap_subtract_output_originaloperationleft. pfa_gap_subtract_output_originaloperationleft + S (pfs_right_subtract_output_original) = (p)) /\ (((exists pfa_gap_subtract_output_originaloperationright. pfa_gap_subtract_output_originaloperationright + S (pfs_result_subtract_output_original) = (p)) /\ ((((exists pfa_gap_subtract_output_originaloperationresultbound. pfa_gap_subtract_output_originaloperationresultbound + S (pfs_left_subtract_output_original) = (p)) /\ ((exists pfa_offset_left_subtract_output_originaloperationresultcongruence pfa_offset_right_subtract_output_originaloperationresultcongruence. ((pfs_right_subtract_output_original) + (pfs_result_subtract_output_original)) + (p) * pfa_offset_left_subtract_output_originaloperationresultcongruence = (pfs_left_subtract_output_original) + (p) * pfa_offset_right_subtract_output_originaloperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_subtract_output_leftzeros. (exists pfa_gap_subtract_output_leftzerosindex. pfa_gap_subtract_output_leftzerosindex + S (pfp_repeat_index_subtract_output_leftzeros) = (t)) -> (((exists ff_h_pfp_subtract_output_leftzerosentry. ff_h_pfp_subtract_output_leftzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_output_leftzeros)) * AC)) /\ exists ff_q_pfp_subtract_output_leftzerosentry. AB = ff_q_pfp_subtract_output_leftzerosentry * S ((S (pfp_repeat_index_subtract_output_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_subtract_output_left pfrep_value_subtract_output_left. (exists pfa_gap_subtract_output_leftbound. pfa_gap_subtract_output_leftbound + S (pfrep_index_subtract_output_left) = (L)) -> (((exists ff_h_pfp_subtract_output_leftinput. ff_h_pfp_subtract_output_leftinput + S (pfrep_value_subtract_output_left) = S ((S (pfrep_index_subtract_output_left)) * ac)) /\ exists ff_q_pfp_subtract_output_leftinput. ab = ff_q_pfp_subtract_output_leftinput * S ((S (pfrep_index_subtract_output_left)) * ac) + (pfrep_value_subtract_output_left))) -> (((exists ff_h_pfp_subtract_output_leftoutput. ff_h_pfp_subtract_output_leftoutput + S (pfrep_value_subtract_output_left) = S ((S ((t)+pfrep_index_subtract_output_left)) * AC)) /\ exists ff_q_pfp_subtract_output_leftoutput. AB = ff_q_pfp_subtract_output_leftoutput * S ((S ((t)+pfrep_index_subtract_output_left)) * AC) + (pfrep_value_subtract_output_left))))))) -> (((forall pfp_repeat_index_subtract_output_rightzeros. (exists pfa_gap_subtract_output_rightzerosindex. pfa_gap_subtract_output_rightzerosindex + S (pfp_repeat_index_subtract_output_rightzeros) = (t)) -> (((exists ff_h_pfp_subtract_output_rightzerosentry. ff_h_pfp_subtract_output_rightzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_output_rightzeros)) * BC)) /\ exists ff_q_pfp_subtract_output_rightzerosentry. BB = ff_q_pfp_subtract_output_rightzerosentry * S ((S (pfp_repeat_index_subtract_output_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_subtract_output_right pfrep_value_subtract_output_right. (exists pfa_gap_subtract_output_rightbound. pfa_gap_subtract_output_rightbound + S (pfrep_index_subtract_output_right) = (L)) -> (((exists ff_h_pfp_subtract_output_rightinput. ff_h_pfp_subtract_output_rightinput + S (pfrep_value_subtract_output_right) = S ((S (pfrep_index_subtract_output_right)) * bc)) /\ exists ff_q_pfp_subtract_output_rightinput. bb = ff_q_pfp_subtract_output_rightinput * S ((S (pfrep_index_subtract_output_right)) * bc) + (pfrep_value_subtract_output_right))) -> (((exists ff_h_pfp_subtract_output_rightoutput. ff_h_pfp_subtract_output_rightoutput + S (pfrep_value_subtract_output_right) = S ((S ((t)+pfrep_index_subtract_output_right)) * BC)) /\ exists ff_q_pfp_subtract_output_rightoutput. BB = ff_q_pfp_subtract_output_rightoutput * S ((S ((t)+pfrep_index_subtract_output_right)) * BC) + (pfrep_value_subtract_output_right))))))) -> (forall pfs_index_subtract_output_padded. (exists pfa_gap_subtract_output_paddedindex. pfa_gap_subtract_output_paddedindex + S (pfs_index_subtract_output_padded) = (t+L)) -> exists pfs_left_subtract_output_padded pfs_right_subtract_output_padded pfs_result_subtract_output_padded. ((((exists ff_h_pfp_subtract_output_paddedleft. ff_h_pfp_subtract_output_paddedleft + S (pfs_left_subtract_output_padded) = S ((S (pfs_index_subtract_output_padded)) * AC)) /\ exists ff_q_pfp_subtract_output_paddedleft. AB = ff_q_pfp_subtract_output_paddedleft * S ((S (pfs_index_subtract_output_padded)) * AC) + (pfs_left_subtract_output_padded))) /\ (((((exists ff_h_pfp_subtract_output_paddedright. ff_h_pfp_subtract_output_paddedright + S (pfs_right_subtract_output_padded) = S ((S (pfs_index_subtract_output_padded)) * BC)) /\ exists ff_q_pfp_subtract_output_paddedright. BB = ff_q_pfp_subtract_output_paddedright * S ((S (pfs_index_subtract_output_padded)) * BC) + (pfs_right_subtract_output_padded))) /\ (((((exists ff_h_pfp_subtract_output_paddedresult. ff_h_pfp_subtract_output_paddedresult + S (pfs_result_subtract_output_padded) = S ((S (pfs_index_subtract_output_padded)) * CC)) /\ exists ff_q_pfp_subtract_output_paddedresult. CB = ff_q_pfp_subtract_output_paddedresult * S ((S (pfs_index_subtract_output_padded)) * CC) + (pfs_result_subtract_output_padded))) /\ ((((exists pfa_gap_subtract_output_paddedoperationleft. pfa_gap_subtract_output_paddedoperationleft + S (pfs_right_subtract_output_padded) = (p)) /\ (((exists pfa_gap_subtract_output_paddedoperationright. pfa_gap_subtract_output_paddedoperationright + S (pfs_result_subtract_output_padded) = (p)) /\ ((((exists pfa_gap_subtract_output_paddedoperationresultbound. pfa_gap_subtract_output_paddedoperationresultbound + S (pfs_left_subtract_output_padded) = (p)) /\ ((exists pfa_offset_left_subtract_output_paddedoperationresultcongruence pfa_offset_right_subtract_output_paddedoperationresultcongruence. ((pfs_right_subtract_output_padded) + (pfs_result_subtract_output_padded)) + (p) * pfa_offset_left_subtract_output_paddedoperationresultcongruence = (pfs_left_subtract_output_padded) + (p) * pfa_offset_right_subtract_output_paddedoperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_subtract_output_resultzeros. (exists pfa_gap_subtract_output_resultzerosindex. pfa_gap_subtract_output_resultzerosindex + S (pfp_repeat_index_subtract_output_resultzeros) = (t)) -> (((exists ff_h_pfp_subtract_output_resultzerosentry. ff_h_pfp_subtract_output_resultzerosentry + S (0) = S ((S (pfp_repeat_index_subtract_output_resultzeros)) * CC)) /\ exists ff_q_pfp_subtract_output_resultzerosentry. CB = ff_q_pfp_subtract_output_resultzerosentry * S ((S (pfp_repeat_index_subtract_output_resultzeros)) * CC) + (0)))) /\ ((forall pfrep_index_subtract_output_result pfrep_value_subtract_output_result. (exists pfa_gap_subtract_output_resultbound. pfa_gap_subtract_output_resultbound + S (pfrep_index_subtract_output_result) = (L)) -> (((exists ff_h_pfp_subtract_output_resultinput. ff_h_pfp_subtract_output_resultinput + S (pfrep_value_subtract_output_result) = S ((S (pfrep_index_subtract_output_result)) * cc)) /\ exists ff_q_pfp_subtract_output_resultinput. cb = ff_q_pfp_subtract_output_resultinput * S ((S (pfrep_index_subtract_output_result)) * cc) + (pfrep_value_subtract_output_result))) -> (((exists ff_h_pfp_subtract_output_resultoutput. ff_h_pfp_subtract_output_resultoutput + S (pfrep_value_subtract_output_result) = S ((S ((t)+pfrep_index_subtract_output_result)) * CC)) /\ exists ff_q_pfp_subtract_output_resultoutput. CB = ff_q_pfp_subtract_output_resultoutput * S ((S ((t)+pfrep_index_subtract_output_result)) * CC) + (pfrep_value_subtract_output_result)))))))
Complete tactic proof in conservative notation
All 82 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.
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.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad exists.