Actual add 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_add_output_prime pfa_factor_right_add_output_prime. (p) = pfa_factor_left_add_output_prime * pfa_factor_right_add_output_prime -> pfa_factor_left_add_output_prime = 1 \/ pfa_factor_right_add_output_prime = 1) -> (forall pfp_index_add_output_original. (exists pfa_gap_add_output_originalindex. pfa_gap_add_output_originalindex + S (pfp_index_add_output_original) = (L)) -> exists pfp_left_add_output_original pfp_right_add_output_original pfp_value_add_output_original. ((((exists ff_h_pfp_add_output_originalleft. ff_h_pfp_add_output_originalleft + S (pfp_left_add_output_original) = S ((S (pfp_index_add_output_original)) * ac)) /\ exists ff_q_pfp_add_output_originalleft. ab = ff_q_pfp_add_output_originalleft * S ((S (pfp_index_add_output_original)) * ac) + (pfp_left_add_output_original))) /\ (((((exists ff_h_pfp_add_output_originalright. ff_h_pfp_add_output_originalright + S (pfp_right_add_output_original) = S ((S (pfp_index_add_output_original)) * bc)) /\ exists ff_q_pfp_add_output_originalright. bb = ff_q_pfp_add_output_originalright * S ((S (pfp_index_add_output_original)) * bc) + (pfp_right_add_output_original))) /\ (((((exists ff_h_pfp_add_output_originaltarget. ff_h_pfp_add_output_originaltarget + S (pfp_value_add_output_original) = S ((S (pfp_index_add_output_original)) * cc)) /\ exists ff_q_pfp_add_output_originaltarget. cb = ff_q_pfp_add_output_originaltarget * S ((S (pfp_index_add_output_original)) * cc) + (pfp_value_add_output_original))) /\ ((((exists pfa_gap_add_output_originaloperationleft. pfa_gap_add_output_originaloperationleft + S (pfp_left_add_output_original) = (p)) /\ (((exists pfa_gap_add_output_originaloperationright. pfa_gap_add_output_originaloperationright + S (pfp_right_add_output_original) = (p)) /\ ((((exists pfa_gap_add_output_originaloperationresultbound. pfa_gap_add_output_originaloperationresultbound + S (pfp_value_add_output_original) = (p)) /\ ((exists pfa_offset_left_add_output_originaloperationresultcongruence pfa_offset_right_add_output_originaloperationresultcongruence. ((pfp_left_add_output_original) + (pfp_right_add_output_original)) + (p) * pfa_offset_left_add_output_originaloperationresultcongruence = (pfp_value_add_output_original) + (p) * pfa_offset_right_add_output_originaloperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_add_output_leftzeros. (exists pfa_gap_add_output_leftzerosindex. pfa_gap_add_output_leftzerosindex + S (pfp_repeat_index_add_output_leftzeros) = (t)) -> (((exists ff_h_pfp_add_output_leftzerosentry. ff_h_pfp_add_output_leftzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_leftzeros)) * AC)) /\ exists ff_q_pfp_add_output_leftzerosentry. AB = ff_q_pfp_add_output_leftzerosentry * S ((S (pfp_repeat_index_add_output_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_add_output_left pfrep_value_add_output_left. (exists pfa_gap_add_output_leftbound. pfa_gap_add_output_leftbound + S (pfrep_index_add_output_left) = (L)) -> (((exists ff_h_pfp_add_output_leftinput. ff_h_pfp_add_output_leftinput + S (pfrep_value_add_output_left) = S ((S (pfrep_index_add_output_left)) * ac)) /\ exists ff_q_pfp_add_output_leftinput. ab = ff_q_pfp_add_output_leftinput * S ((S (pfrep_index_add_output_left)) * ac) + (pfrep_value_add_output_left))) -> (((exists ff_h_pfp_add_output_leftoutput. ff_h_pfp_add_output_leftoutput + S (pfrep_value_add_output_left) = S ((S ((t)+pfrep_index_add_output_left)) * AC)) /\ exists ff_q_pfp_add_output_leftoutput. AB = ff_q_pfp_add_output_leftoutput * S ((S ((t)+pfrep_index_add_output_left)) * AC) + (pfrep_value_add_output_left))))))) -> (((forall pfp_repeat_index_add_output_rightzeros. (exists pfa_gap_add_output_rightzerosindex. pfa_gap_add_output_rightzerosindex + S (pfp_repeat_index_add_output_rightzeros) = (t)) -> (((exists ff_h_pfp_add_output_rightzerosentry. ff_h_pfp_add_output_rightzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_rightzeros)) * BC)) /\ exists ff_q_pfp_add_output_rightzerosentry. BB = ff_q_pfp_add_output_rightzerosentry * S ((S (pfp_repeat_index_add_output_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_add_output_right pfrep_value_add_output_right. (exists pfa_gap_add_output_rightbound. pfa_gap_add_output_rightbound + S (pfrep_index_add_output_right) = (L)) -> (((exists ff_h_pfp_add_output_rightinput. ff_h_pfp_add_output_rightinput + S (pfrep_value_add_output_right) = S ((S (pfrep_index_add_output_right)) * bc)) /\ exists ff_q_pfp_add_output_rightinput. bb = ff_q_pfp_add_output_rightinput * S ((S (pfrep_index_add_output_right)) * bc) + (pfrep_value_add_output_right))) -> (((exists ff_h_pfp_add_output_rightoutput. ff_h_pfp_add_output_rightoutput + S (pfrep_value_add_output_right) = S ((S ((t)+pfrep_index_add_output_right)) * BC)) /\ exists ff_q_pfp_add_output_rightoutput. BB = ff_q_pfp_add_output_rightoutput * S ((S ((t)+pfrep_index_add_output_right)) * BC) + (pfrep_value_add_output_right))))))) -> (forall pfp_index_add_output_padded. (exists pfa_gap_add_output_paddedindex. pfa_gap_add_output_paddedindex + S (pfp_index_add_output_padded) = (t+L)) -> exists pfp_left_add_output_padded pfp_right_add_output_padded pfp_value_add_output_padded. ((((exists ff_h_pfp_add_output_paddedleft. ff_h_pfp_add_output_paddedleft + S (pfp_left_add_output_padded) = S ((S (pfp_index_add_output_padded)) * AC)) /\ exists ff_q_pfp_add_output_paddedleft. AB = ff_q_pfp_add_output_paddedleft * S ((S (pfp_index_add_output_padded)) * AC) + (pfp_left_add_output_padded))) /\ (((((exists ff_h_pfp_add_output_paddedright. ff_h_pfp_add_output_paddedright + S (pfp_right_add_output_padded) = S ((S (pfp_index_add_output_padded)) * BC)) /\ exists ff_q_pfp_add_output_paddedright. BB = ff_q_pfp_add_output_paddedright * S ((S (pfp_index_add_output_padded)) * BC) + (pfp_right_add_output_padded))) /\ (((((exists ff_h_pfp_add_output_paddedtarget. ff_h_pfp_add_output_paddedtarget + S (pfp_value_add_output_padded) = S ((S (pfp_index_add_output_padded)) * CC)) /\ exists ff_q_pfp_add_output_paddedtarget. CB = ff_q_pfp_add_output_paddedtarget * S ((S (pfp_index_add_output_padded)) * CC) + (pfp_value_add_output_padded))) /\ ((((exists pfa_gap_add_output_paddedoperationleft. pfa_gap_add_output_paddedoperationleft + S (pfp_left_add_output_padded) = (p)) /\ (((exists pfa_gap_add_output_paddedoperationright. pfa_gap_add_output_paddedoperationright + S (pfp_right_add_output_padded) = (p)) /\ ((((exists pfa_gap_add_output_paddedoperationresultbound. pfa_gap_add_output_paddedoperationresultbound + S (pfp_value_add_output_padded) = (p)) /\ ((exists pfa_offset_left_add_output_paddedoperationresultcongruence pfa_offset_right_add_output_paddedoperationresultcongruence. ((pfp_left_add_output_padded) + (pfp_right_add_output_padded)) + (p) * pfa_offset_left_add_output_paddedoperationresultcongruence = (pfp_value_add_output_padded) + (p) * pfa_offset_right_add_output_paddedoperationresultcongruence)))))))))))))))) -> (((forall pfp_repeat_index_add_output_resultzeros. (exists pfa_gap_add_output_resultzerosindex. pfa_gap_add_output_resultzerosindex + S (pfp_repeat_index_add_output_resultzeros) = (t)) -> (((exists ff_h_pfp_add_output_resultzerosentry. ff_h_pfp_add_output_resultzerosentry + S (0) = S ((S (pfp_repeat_index_add_output_resultzeros)) * CC)) /\ exists ff_q_pfp_add_output_resultzerosentry. CB = ff_q_pfp_add_output_resultzerosentry * S ((S (pfp_repeat_index_add_output_resultzeros)) * CC) + (0)))) /\ ((forall pfrep_index_add_output_result pfrep_value_add_output_result. (exists pfa_gap_add_output_resultbound. pfa_gap_add_output_resultbound + S (pfrep_index_add_output_result) = (L)) -> (((exists ff_h_pfp_add_output_resultinput. ff_h_pfp_add_output_resultinput + S (pfrep_value_add_output_result) = S ((S (pfrep_index_add_output_result)) * cc)) /\ exists ff_q_pfp_add_output_resultinput. cb = ff_q_pfp_add_output_resultinput * S ((S (pfrep_index_add_output_result)) * cc) + (pfrep_value_add_output_result))) -> (((exists ff_h_pfp_add_output_resultoutput. ff_h_pfp_add_output_resultoutput + S (pfrep_value_add_output_result) = S ((S ((t)+pfrep_index_add_output_result)) * CC)) /\ exists ff_q_pfp_add_output_resultoutput. CB = ff_q_pfp_add_output_resultoutput * S ((S ((t)+pfrep_index_add_output_result)) * CC) + (pfrep_value_add_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.