An actual trailing-zero shift of the right factor preserves exactly the same antidiagonal term witnesses in both directions.
Alpha v34 checked-use · first admitted v34 · 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.
All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
forall ab ac L bb bc M BB BC i j t. (((forall mdr_i_pfp_shift_term_relationprefix mdr_a_pfp_shift_term_relationprefix. (exists mdr_gap_pfp_shift_term_relationprefixb. mdr_gap_pfp_shift_term_relationprefixb + S (mdr_i_pfp_shift_term_relationprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_term_relationprefixo. ff_h_mdr_pfp_shift_term_relationprefixo + S (mdr_a_pfp_shift_term_relationprefix) = S ((S (mdr_i_pfp_shift_term_relationprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_term_relationprefixo. bb = ff_q_mdr_pfp_shift_term_relationprefixo * S ((S (mdr_i_pfp_shift_term_relationprefix)) * bc) + (mdr_a_pfp_shift_term_relationprefix))) -> (((exists ff_h_mdr_pfp_shift_term_relationprefixn. ff_h_mdr_pfp_shift_term_relationprefixn + S (mdr_a_pfp_shift_term_relationprefix) = S ((S (mdr_i_pfp_shift_term_relationprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_term_relationprefixn. BB = ff_q_mdr_pfp_shift_term_relationprefixn * S ((S (mdr_i_pfp_shift_term_relationprefix)) * BC) + (mdr_a_pfp_shift_term_relationprefix)))) /\ ((((exists ff_h_pfp_shift_term_relationlast. ff_h_pfp_shift_term_relationlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_term_relationlast. BB = ff_q_pfp_shift_term_relationlast * S ((S (M)) * BC) + (0)))))) -> ((((exists pfc_complement_shift_term_old pfc_left_shift_term_old pfc_right_shift_term_old. (((j)+pfc_complement_shift_term_old=(i)) /\ ((((((exists pfa_gap_shift_term_oldleftinside. pfa_gap_shift_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_oldleftentry. ff_h_pfp_shift_term_oldleftentry + S (pfc_left_shift_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_oldleftentry. ab = ff_q_pfp_shift_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldleftoutside. pfc_gap_shift_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_old)=0))))) /\ ((((((exists pfa_gap_shift_term_oldrightinside. pfa_gap_shift_term_oldrightinside + S (pfc_complement_shift_term_old) = (M)) /\ ((((exists ff_h_pfp_shift_term_oldrightentry. ff_h_pfp_shift_term_oldrightentry + S (pfc_right_shift_term_old) = S ((S (pfc_complement_shift_term_old)) * bc)) /\ exists ff_q_pfp_shift_term_oldrightentry. bb = ff_q_pfp_shift_term_oldrightentry * S ((S (pfc_complement_shift_term_old)) * bc) + (pfc_right_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldrightoutside. pfc_gap_shift_term_oldrightoutside+(M)=(pfc_complement_shift_term_old)) /\ (((pfc_right_shift_term_old)=0))))) /\ (((t)=pfc_left_shift_term_old*pfc_right_shift_term_old)))))))) -> (exists pfc_complement_shift_term_new pfc_left_shift_term_new pfc_right_shift_term_new. (((j)+pfc_complement_shift_term_new=(i)) /\ ((((((exists pfa_gap_shift_term_newleftinside. pfa_gap_shift_term_newleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_newleftentry. ff_h_pfp_shift_term_newleftentry + S (pfc_left_shift_term_new) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_newleftentry. ab = ff_q_pfp_shift_term_newleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newleftoutside. pfc_gap_shift_term_newleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_new)=0))))) /\ ((((((exists pfa_gap_shift_term_newrightinside. pfa_gap_shift_term_newrightinside + S (pfc_complement_shift_term_new) = (S M)) /\ ((((exists ff_h_pfp_shift_term_newrightentry. ff_h_pfp_shift_term_newrightentry + S (pfc_right_shift_term_new) = S ((S (pfc_complement_shift_term_new)) * BC)) /\ exists ff_q_pfp_shift_term_newrightentry. BB = ff_q_pfp_shift_term_newrightentry * S ((S (pfc_complement_shift_term_new)) * BC) + (pfc_right_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newrightoutside. pfc_gap_shift_term_newrightoutside+(S M)=(pfc_complement_shift_term_new)) /\ (((pfc_right_shift_term_new)=0))))) /\ (((t)=pfc_left_shift_term_new*pfc_right_shift_term_new))))))))) /\ (((exists pfc_complement_shift_term_new pfc_left_shift_term_new pfc_right_shift_term_new. (((j)+pfc_complement_shift_term_new=(i)) /\ ((((((exists pfa_gap_shift_term_newleftinside. pfa_gap_shift_term_newleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_newleftentry. ff_h_pfp_shift_term_newleftentry + S (pfc_left_shift_term_new) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_newleftentry. ab = ff_q_pfp_shift_term_newleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newleftoutside. pfc_gap_shift_term_newleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_new)=0))))) /\ ((((((exists pfa_gap_shift_term_newrightinside. pfa_gap_shift_term_newrightinside + S (pfc_complement_shift_term_new) = (S M)) /\ ((((exists ff_h_pfp_shift_term_newrightentry. ff_h_pfp_shift_term_newrightentry + S (pfc_right_shift_term_new) = S ((S (pfc_complement_shift_term_new)) * BC)) /\ exists ff_q_pfp_shift_term_newrightentry. BB = ff_q_pfp_shift_term_newrightentry * S ((S (pfc_complement_shift_term_new)) * BC) + (pfc_right_shift_term_new)))))) \/ (((exists pfc_gap_shift_term_newrightoutside. pfc_gap_shift_term_newrightoutside+(S M)=(pfc_complement_shift_term_new)) /\ (((pfc_right_shift_term_new)=0))))) /\ (((t)=pfc_left_shift_term_new*pfc_right_shift_term_new)))))))) -> (exists pfc_complement_shift_term_old pfc_left_shift_term_old pfc_right_shift_term_old. (((j)+pfc_complement_shift_term_old=(i)) /\ ((((((exists pfa_gap_shift_term_oldleftinside. pfa_gap_shift_term_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_shift_term_oldleftentry. ff_h_pfp_shift_term_oldleftentry + S (pfc_left_shift_term_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_shift_term_oldleftentry. ab = ff_q_pfp_shift_term_oldleftentry * S ((S (j)) * ac) + (pfc_left_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldleftoutside. pfc_gap_shift_term_oldleftoutside+(L)=(j)) /\ (((pfc_left_shift_term_old)=0))))) /\ ((((((exists pfa_gap_shift_term_oldrightinside. pfa_gap_shift_term_oldrightinside + S (pfc_complement_shift_term_old) = (M)) /\ ((((exists ff_h_pfp_shift_term_oldrightentry. ff_h_pfp_shift_term_oldrightentry + S (pfc_right_shift_term_old) = S ((S (pfc_complement_shift_term_old)) * bc)) /\ exists ff_q_pfp_shift_term_oldrightentry. bb = ff_q_pfp_shift_term_oldrightentry * S ((S (pfc_complement_shift_term_old)) * bc) + (pfc_right_shift_term_old)))))) \/ (((exists pfc_gap_shift_term_oldrightoutside. pfc_gap_shift_term_oldrightoutside+(M)=(pfc_complement_shift_term_old)) /\ (((pfc_right_shift_term_old)=0))))) /\ (((t)=pfc_left_shift_term_old*pfc_right_shift_term_old))))))))))))
Complete tactic proof in conservative notation
All 65 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.