From an actual old product and a canonical next coefficient, construct the appended right factor, its proper product, the shift and scalar outputs, both aligned paddings and the actual sum, then prove the formal recurrence. No output existence or polynomial identity is assumed.
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 p ab ac L bb bc M c pb pc N. (~((p) = 1) /\ forall pfa_factor_left_append_exists_prime pfa_factor_right_append_exists_prime. (p) = pfa_factor_left_append_exists_prime * pfa_factor_right_append_exists_prime -> pfa_factor_left_append_exists_prime = 1 \/ pfa_factor_right_append_exists_prime = 1) -> (exists pfa_gap_append_exists_scalar. pfa_gap_append_exists_scalar + S (c) = (p)) -> (((forall fom_index_pfp_append_exists_oldleft. (exists fom_gap_pfp_append_exists_oldleft_index_bound. fom_gap_pfp_append_exists_oldleft_index_bound + S (fom_index_pfp_append_exists_oldleft) = L) -> exists fom_value_pfp_append_exists_oldleft. ((((exists fom_beta_height_pfp_append_exists_oldleft_entry. fom_beta_height_pfp_append_exists_oldleft_entry + S (fom_value_pfp_append_exists_oldleft) = S ((S (fom_index_pfp_append_exists_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_exists_oldleft_entry. ab = fom_beta_quotient_pfp_append_exists_oldleft_entry * S ((S (fom_index_pfp_append_exists_oldleft)) * ac) + (fom_value_pfp_append_exists_oldleft))) /\ (exists fom_gap_pfp_append_exists_oldleft_value_bound. fom_gap_pfp_append_exists_oldleft_value_bound + S (fom_value_pfp_append_exists_oldleft) = p))) /\ (((forall fom_index_pfp_append_exists_oldright. (exists fom_gap_pfp_append_exists_oldright_index_bound. fom_gap_pfp_append_exists_oldright_index_bound + S (fom_index_pfp_append_exists_oldright) = M) -> exists fom_value_pfp_append_exists_oldright. ((((exists fom_beta_height_pfp_append_exists_oldright_entry. fom_beta_height_pfp_append_exists_oldright_entry + S (fom_value_pfp_append_exists_oldright) = S ((S (fom_index_pfp_append_exists_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_append_exists_oldright_entry. bb = fom_beta_quotient_pfp_append_exists_oldright_entry * S ((S (fom_index_pfp_append_exists_oldright)) * bc) + (fom_value_pfp_append_exists_oldright))) /\ (exists fom_gap_pfp_append_exists_oldright_value_bound. fom_gap_pfp_append_exists_oldright_value_bound + S (fom_value_pfp_append_exists_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_exists_oldcoefficients. (exists pfa_gap_append_exists_oldcoefficientsbound. pfa_gap_append_exists_oldcoefficientsbound + S (pfc_index_append_exists_oldcoefficients) = (N)) -> exists pfc_value_append_exists_oldcoefficients. ((((exists ff_h_pfp_append_exists_oldcoefficientsentry. ff_h_pfp_append_exists_oldcoefficientsentry + S (pfc_value_append_exists_oldcoefficients) = S ((S (pfc_index_append_exists_oldcoefficients)) * pc)) /\ exists ff_q_pfp_append_exists_oldcoefficientsentry. pb = ff_q_pfp_append_exists_oldcoefficientsentry * S ((S (pfc_index_append_exists_oldcoefficients)) * pc) + (pfc_value_append_exists_oldcoefficients))) /\ ((exists pfc_terms_code_append_exists_oldcoefficientscoefficient pfc_terms_scale_append_exists_oldcoefficientscoefficient pfc_natural_sum_append_exists_oldcoefficientscoefficient. ((forall pfc_index_append_exists_oldcoefficientscoefficientdiagonal. (exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonalbound. pfa_gap_append_exists_oldcoefficientscoefficientdiagonalbound + S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal) = (S (pfc_index_append_exists_oldcoefficients))) -> exists pfc_value_append_exists_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonalentry + S (pfc_value_append_exists_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_append_exists_oldcoefficientscoefficient = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient) + (pfc_value_append_exists_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm. (((pfc_index_append_exists_oldcoefficientscoefficientdiagonal)+pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm=(pfc_index_append_exists_oldcoefficients)) /\ ((((((exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_exists_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_exists_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_exists_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_exists_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_exists_oldcoefficientscoefficientdiagonal)=pfc_left_append_exists_oldcoefficientscoefficientdiagonalterm*pfc_right_append_exists_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_exists_oldcoefficientscoefficientsum fs_v_pfc_append_exists_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_start. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_start. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_exists_oldcoefficientscoefficient) = S ((S (S (pfc_index_append_exists_oldcoefficients))) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_exists_oldcoefficients))) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (pfc_natural_sum_append_exists_oldcoefficientscoefficient))) /\ forall fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps = S (pfc_index_append_exists_oldcoefficients)) -> exists fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_exists_oldcoefficientscoefficient = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_oldcoefficientscoefficient) + (fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_exists_oldcoefficientscoefficientsum = fs_q_pfc_append_exists_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_oldcoefficientscoefficientsum) + (fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_exists_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_append_exists_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_append_exists_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_exists_oldcoefficientscoefficientresiduebound. pfa_gap_append_exists_oldcoefficientscoefficientresiduebound + S (pfc_value_append_exists_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_append_exists_oldcoefficientscoefficientresiduecongruence pfa_offset_right_append_exists_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_exists_oldcoefficientscoefficient) + (p) * pfa_offset_left_append_exists_oldcoefficientscoefficientresiduecongruence = (pfc_value_append_exists_oldcoefficients) + (p) * pfa_offset_right_append_exists_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (exists db dc K qb qc ub uc vb vc UB UC VB VC rb rc. ((forall mdr_i_pfp_append_exists_preserve mdr_a_pfp_append_exists_preserve. (exists mdr_gap_pfp_append_exists_preserveb. mdr_gap_pfp_append_exists_preserveb + S (mdr_i_pfp_append_exists_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_exists_preserveo. ff_h_mdr_pfp_append_exists_preserveo + S (mdr_a_pfp_append_exists_preserve) = S ((S (mdr_i_pfp_append_exists_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_exists_preserveo. bb = ff_q_mdr_pfp_append_exists_preserveo * S ((S (mdr_i_pfp_append_exists_preserve)) * bc) + (mdr_a_pfp_append_exists_preserve))) -> (((exists ff_h_mdr_pfp_append_exists_preserven. ff_h_mdr_pfp_append_exists_preserven + S (mdr_a_pfp_append_exists_preserve) = S ((S (mdr_i_pfp_append_exists_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_exists_preserven. db = ff_q_mdr_pfp_append_exists_preserven * S ((S (mdr_i_pfp_append_exists_preserve)) * dc) + (mdr_a_pfp_append_exists_preserve)))) /\ (((((exists ff_h_pfp_append_exists_last. ff_h_pfp_append_exists_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_exists_last. db = ff_q_pfp_append_exists_last * S ((S (M)) * dc) + (c))) /\ (((((forall fom_index_pfp_append_exists_newleft. (exists fom_gap_pfp_append_exists_newleft_index_bound. fom_gap_pfp_append_exists_newleft_index_bound + S (fom_index_pfp_append_exists_newleft) = L) -> exists fom_value_pfp_append_exists_newleft. ((((exists fom_beta_height_pfp_append_exists_newleft_entry. fom_beta_height_pfp_append_exists_newleft_entry + S (fom_value_pfp_append_exists_newleft) = S ((S (fom_index_pfp_append_exists_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_exists_newleft_entry. ab = fom_beta_quotient_pfp_append_exists_newleft_entry * S ((S (fom_index_pfp_append_exists_newleft)) * ac) + (fom_value_pfp_append_exists_newleft))) /\ (exists fom_gap_pfp_append_exists_newleft_value_bound. fom_gap_pfp_append_exists_newleft_value_bound + S (fom_value_pfp_append_exists_newleft) = p))) /\ (((forall fom_index_pfp_append_exists_newright. (exists fom_gap_pfp_append_exists_newright_index_bound. fom_gap_pfp_append_exists_newright_index_bound + S (fom_index_pfp_append_exists_newright) = S M) -> exists fom_value_pfp_append_exists_newright. ((((exists fom_beta_height_pfp_append_exists_newright_entry. fom_beta_height_pfp_append_exists_newright_entry + S (fom_value_pfp_append_exists_newright) = S ((S (fom_index_pfp_append_exists_newright)) * dc)) /\ exists fom_beta_quotient_pfp_append_exists_newright_entry. db = fom_beta_quotient_pfp_append_exists_newright_entry * S ((S (fom_index_pfp_append_exists_newright)) * dc) + (fom_value_pfp_append_exists_newright))) /\ (exists fom_gap_pfp_append_exists_newright_value_bound. fom_gap_pfp_append_exists_newright_value_bound + S (fom_value_pfp_append_exists_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_append_exists_newcoefficients. (exists pfa_gap_append_exists_newcoefficientsbound. pfa_gap_append_exists_newcoefficientsbound + S (pfc_index_append_exists_newcoefficients) = (K)) -> exists pfc_value_append_exists_newcoefficients. ((((exists ff_h_pfp_append_exists_newcoefficientsentry. ff_h_pfp_append_exists_newcoefficientsentry + S (pfc_value_append_exists_newcoefficients) = S ((S (pfc_index_append_exists_newcoefficients)) * qc)) /\ exists ff_q_pfp_append_exists_newcoefficientsentry. qb = ff_q_pfp_append_exists_newcoefficientsentry * S ((S (pfc_index_append_exists_newcoefficients)) * qc) + (pfc_value_append_exists_newcoefficients))) /\ ((exists pfc_terms_code_append_exists_newcoefficientscoefficient pfc_terms_scale_append_exists_newcoefficientscoefficient pfc_natural_sum_append_exists_newcoefficientscoefficient. ((forall pfc_index_append_exists_newcoefficientscoefficientdiagonal. (exists pfa_gap_append_exists_newcoefficientscoefficientdiagonalbound. pfa_gap_append_exists_newcoefficientscoefficientdiagonalbound + S (pfc_index_append_exists_newcoefficientscoefficientdiagonal) = (S (pfc_index_append_exists_newcoefficients))) -> exists pfc_value_append_exists_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonalentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonalentry + S (pfc_value_append_exists_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_newcoefficientscoefficient)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonalentry. pfc_terms_code_append_exists_newcoefficientscoefficient = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_exists_newcoefficientscoefficient) + (pfc_value_append_exists_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm pfc_left_append_exists_newcoefficientscoefficientdiagonalterm pfc_right_append_exists_newcoefficientscoefficientdiagonalterm. (((pfc_index_append_exists_newcoefficientscoefficientdiagonal)+pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm=(pfc_index_append_exists_newcoefficients)) /\ ((((((exists pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_exists_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_exists_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_exists_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_exists_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_exists_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_exists_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_append_exists_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_exists_newcoefficientscoefficientdiagonal)=pfc_left_append_exists_newcoefficientscoefficientdiagonalterm*pfc_right_append_exists_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_exists_newcoefficientscoefficientsum fs_v_pfc_append_exists_newcoefficientscoefficientsum. ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_start. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_start. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_exists_newcoefficientscoefficient) = S ((S (S (pfc_index_append_exists_newcoefficients))) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_exists_newcoefficients))) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (pfc_natural_sum_append_exists_newcoefficientscoefficient))) /\ forall fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_exists_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_exists_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps = S (pfc_index_append_exists_newcoefficients)) -> exists fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_newcoefficientscoefficient)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_exists_newcoefficientscoefficient = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_exists_newcoefficientscoefficient) + (fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_exists_newcoefficientscoefficientsum = fs_q_pfc_append_exists_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_exists_newcoefficientscoefficientsum) + (fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_exists_newcoefficientscoefficientsum_body_steps = fs_r_pfc_append_exists_newcoefficientscoefficientsum_body_steps + fs_a_pfc_append_exists_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_exists_newcoefficientscoefficientresiduebound. pfa_gap_append_exists_newcoefficientscoefficientresiduebound + S (pfc_value_append_exists_newcoefficients) = (p)) /\ ((exists pfa_offset_left_append_exists_newcoefficientscoefficientresiduecongruence pfa_offset_right_append_exists_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_exists_newcoefficientscoefficient) + (p) * pfa_offset_left_append_exists_newcoefficientscoefficientresiduecongruence = (pfc_value_append_exists_newcoefficients) + (p) * pfa_offset_right_append_exists_newcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall mdr_i_pfp_append_exists_result_shiftprefix mdr_a_pfp_append_exists_result_shiftprefix. (exists mdr_gap_pfp_append_exists_result_shiftprefixb. mdr_gap_pfp_append_exists_result_shiftprefixb + S (mdr_i_pfp_append_exists_result_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_append_exists_result_shiftprefixo. ff_h_mdr_pfp_append_exists_result_shiftprefixo + S (mdr_a_pfp_append_exists_result_shiftprefix) = S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * pc)) /\ exists ff_q_mdr_pfp_append_exists_result_shiftprefixo. pb = ff_q_mdr_pfp_append_exists_result_shiftprefixo * S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * pc) + (mdr_a_pfp_append_exists_result_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_exists_result_shiftprefixn. ff_h_mdr_pfp_append_exists_result_shiftprefixn + S (mdr_a_pfp_append_exists_result_shiftprefix) = S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_exists_result_shiftprefixn. ub = ff_q_mdr_pfp_append_exists_result_shiftprefixn * S ((S (mdr_i_pfp_append_exists_result_shiftprefix)) * uc) + (mdr_a_pfp_append_exists_result_shiftprefix)))) /\ ((((exists ff_h_pfp_append_exists_result_shiftlast. ff_h_pfp_append_exists_result_shiftlast + S (0) = S ((S (N)) * uc)) /\ exists ff_q_pfp_append_exists_result_shiftlast. ub = ff_q_pfp_append_exists_result_shiftlast * S ((S (N)) * uc) + (0)))))) /\ (((((exists pfa_gap_append_exists_result_scalescalar. pfa_gap_append_exists_result_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_exists_result_scale. (exists pfa_gap_append_exists_result_scaleindex. pfa_gap_append_exists_result_scaleindex + S (pfp_index_append_exists_result_scale) = (L)) -> exists pfp_source_append_exists_result_scale pfp_value_append_exists_result_scale. ((((exists ff_h_pfp_append_exists_result_scalesource. ff_h_pfp_append_exists_result_scalesource + S (pfp_source_append_exists_result_scale) = S ((S (pfp_index_append_exists_result_scale)) * ac)) /\ exists ff_q_pfp_append_exists_result_scalesource. ab = ff_q_pfp_append_exists_result_scalesource * S ((S (pfp_index_append_exists_result_scale)) * ac) + (pfp_source_append_exists_result_scale))) /\ (((((exists ff_h_pfp_append_exists_result_scaletarget. ff_h_pfp_append_exists_result_scaletarget + S (pfp_value_append_exists_result_scale) = S ((S (pfp_index_append_exists_result_scale)) * vc)) /\ exists ff_q_pfp_append_exists_result_scaletarget. vb = ff_q_pfp_append_exists_result_scaletarget * S ((S (pfp_index_append_exists_result_scale)) * vc) + (pfp_value_append_exists_result_scale))) /\ ((((exists pfa_gap_append_exists_result_scaleoperationleft. pfa_gap_append_exists_result_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_exists_result_scaleoperationright. pfa_gap_append_exists_result_scaleoperationright + S (pfp_source_append_exists_result_scale) = (p)) /\ ((((exists pfa_gap_append_exists_result_scaleoperationresultbound. pfa_gap_append_exists_result_scaleoperationresultbound + S (pfp_value_append_exists_result_scale) = (p)) /\ ((exists pfa_offset_left_append_exists_result_scaleoperationresultcongruence pfa_offset_right_append_exists_result_scaleoperationresultcongruence. ((c) * (pfp_source_append_exists_result_scale)) + (p) * pfa_offset_left_append_exists_result_scaleoperationresultcongruence = (pfp_value_append_exists_result_scale) + (p) * pfa_offset_right_append_exists_result_scaleoperationresultcongruence))))))))))))))))) /\ (((((forall pfp_repeat_index_append_exists_result_leftzeros. (exists pfa_gap_append_exists_result_leftzerosindex. pfa_gap_append_exists_result_leftzerosindex + S (pfp_repeat_index_append_exists_result_leftzeros) = (L)) -> (((exists ff_h_pfp_append_exists_result_leftzerosentry. ff_h_pfp_append_exists_result_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_exists_result_leftzeros)) * UC)) /\ exists ff_q_pfp_append_exists_result_leftzerosentry. UB = ff_q_pfp_append_exists_result_leftzerosentry * S ((S (pfp_repeat_index_append_exists_result_leftzeros)) * UC) + (0)))) /\ ((forall pfrep_index_append_exists_result_left pfrep_value_append_exists_result_left. (exists pfa_gap_append_exists_result_leftbound. pfa_gap_append_exists_result_leftbound + S (pfrep_index_append_exists_result_left) = (S N)) -> (((exists ff_h_pfp_append_exists_result_leftinput. ff_h_pfp_append_exists_result_leftinput + S (pfrep_value_append_exists_result_left) = S ((S (pfrep_index_append_exists_result_left)) * uc)) /\ exists ff_q_pfp_append_exists_result_leftinput. ub = ff_q_pfp_append_exists_result_leftinput * S ((S (pfrep_index_append_exists_result_left)) * uc) + (pfrep_value_append_exists_result_left))) -> (((exists ff_h_pfp_append_exists_result_leftoutput. ff_h_pfp_append_exists_result_leftoutput + S (pfrep_value_append_exists_result_left) = S ((S ((L)+pfrep_index_append_exists_result_left)) * UC)) /\ exists ff_q_pfp_append_exists_result_leftoutput. UB = ff_q_pfp_append_exists_result_leftoutput * S ((S ((L)+pfrep_index_append_exists_result_left)) * UC) + (pfrep_value_append_exists_result_left))))))) /\ (((((forall pfp_repeat_index_append_exists_result_rightzeros. (exists pfa_gap_append_exists_result_rightzerosindex. pfa_gap_append_exists_result_rightzerosindex + S (pfp_repeat_index_append_exists_result_rightzeros) = (S N)) -> (((exists ff_h_pfp_append_exists_result_rightzerosentry. ff_h_pfp_append_exists_result_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_exists_result_rightzeros)) * VC)) /\ exists ff_q_pfp_append_exists_result_rightzerosentry. VB = ff_q_pfp_append_exists_result_rightzerosentry * S ((S (pfp_repeat_index_append_exists_result_rightzeros)) * VC) + (0)))) /\ ((forall pfrep_index_append_exists_result_right pfrep_value_append_exists_result_right. (exists pfa_gap_append_exists_result_rightbound. pfa_gap_append_exists_result_rightbound + S (pfrep_index_append_exists_result_right) = (L)) -> (((exists ff_h_pfp_append_exists_result_rightinput. ff_h_pfp_append_exists_result_rightinput + S (pfrep_value_append_exists_result_right) = S ((S (pfrep_index_append_exists_result_right)) * vc)) /\ exists ff_q_pfp_append_exists_result_rightinput. vb = ff_q_pfp_append_exists_result_rightinput * S ((S (pfrep_index_append_exists_result_right)) * vc) + (pfrep_value_append_exists_result_right))) -> (((exists ff_h_pfp_append_exists_result_rightoutput. ff_h_pfp_append_exists_result_rightoutput + S (pfrep_value_append_exists_result_right) = S ((S ((S N)+pfrep_index_append_exists_result_right)) * VC)) /\ exists ff_q_pfp_append_exists_result_rightoutput. VB = ff_q_pfp_append_exists_result_rightoutput * S ((S ((S N)+pfrep_index_append_exists_result_right)) * VC) + (pfrep_value_append_exists_result_right))))))) /\ (((forall pfp_index_append_exists_result_sum. (exists pfa_gap_append_exists_result_sumindex. pfa_gap_append_exists_result_sumindex + S (pfp_index_append_exists_result_sum) = (L+S N)) -> exists pfp_left_append_exists_result_sum pfp_right_append_exists_result_sum pfp_value_append_exists_result_sum. ((((exists ff_h_pfp_append_exists_result_sumleft. ff_h_pfp_append_exists_result_sumleft + S (pfp_left_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * UC)) /\ exists ff_q_pfp_append_exists_result_sumleft. UB = ff_q_pfp_append_exists_result_sumleft * S ((S (pfp_index_append_exists_result_sum)) * UC) + (pfp_left_append_exists_result_sum))) /\ (((((exists ff_h_pfp_append_exists_result_sumright. ff_h_pfp_append_exists_result_sumright + S (pfp_right_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * VC)) /\ exists ff_q_pfp_append_exists_result_sumright. VB = ff_q_pfp_append_exists_result_sumright * S ((S (pfp_index_append_exists_result_sum)) * VC) + (pfp_right_append_exists_result_sum))) /\ (((((exists ff_h_pfp_append_exists_result_sumtarget. ff_h_pfp_append_exists_result_sumtarget + S (pfp_value_append_exists_result_sum) = S ((S (pfp_index_append_exists_result_sum)) * rc)) /\ exists ff_q_pfp_append_exists_result_sumtarget. rb = ff_q_pfp_append_exists_result_sumtarget * S ((S (pfp_index_append_exists_result_sum)) * rc) + (pfp_value_append_exists_result_sum))) /\ ((((exists pfa_gap_append_exists_result_sumoperationleft. pfa_gap_append_exists_result_sumoperationleft + S (pfp_left_append_exists_result_sum) = (p)) /\ (((exists pfa_gap_append_exists_result_sumoperationright. pfa_gap_append_exists_result_sumoperationright + S (pfp_right_append_exists_result_sum) = (p)) /\ ((((exists pfa_gap_append_exists_result_sumoperationresultbound. pfa_gap_append_exists_result_sumoperationresultbound + S (pfp_value_append_exists_result_sum) = (p)) /\ ((exists pfa_offset_left_append_exists_result_sumoperationresultcongruence pfa_offset_right_append_exists_result_sumoperationresultcongruence. ((pfp_left_append_exists_result_sum) + (pfp_right_append_exists_result_sum)) + (p) * pfa_offset_left_append_exists_result_sumoperationresultcongruence = (pfp_value_append_exists_result_sum) + (p) * pfa_offset_right_append_exists_result_sumoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_append_exists_equivalence pfrep_left_append_exists_equivalence pfrep_right_append_exists_equivalence. ((exists pfrep_position_append_exists_equivalencefirst. ((pfrep_position_append_exists_equivalencefirst+S (pfrep_power_append_exists_equivalence)=(K)) /\ ((((exists ff_h_pfp_append_exists_equivalencefirstentry. ff_h_pfp_append_exists_equivalencefirstentry + S (pfrep_left_append_exists_equivalence) = S ((S (pfrep_position_append_exists_equivalencefirst)) * qc)) /\ exists ff_q_pfp_append_exists_equivalencefirstentry. qb = ff_q_pfp_append_exists_equivalencefirstentry * S ((S (pfrep_position_append_exists_equivalencefirst)) * qc) + (pfrep_left_append_exists_equivalence)))))) \/ (((exists pfrep_gap_append_exists_equivalencefirstoutside. pfrep_gap_append_exists_equivalencefirstoutside+(K)=(pfrep_power_append_exists_equivalence)) /\ (((pfrep_left_append_exists_equivalence)=0))))) -> ((exists pfrep_position_append_exists_equivalencesecond. ((pfrep_position_append_exists_equivalencesecond+S (pfrep_power_append_exists_equivalence)=(L+S N)) /\ ((((exists ff_h_pfp_append_exists_equivalencesecondentry. ff_h_pfp_append_exists_equivalencesecondentry + S (pfrep_right_append_exists_equivalence) = S ((S (pfrep_position_append_exists_equivalencesecond)) * rc)) /\ exists ff_q_pfp_append_exists_equivalencesecondentry. rb = ff_q_pfp_append_exists_equivalencesecondentry * S ((S (pfrep_position_append_exists_equivalencesecond)) * rc) + (pfrep_right_append_exists_equivalence)))))) \/ (((exists pfrep_gap_append_exists_equivalencesecondoutside. pfrep_gap_append_exists_equivalencesecondoutside+(L+S N)=(pfrep_power_append_exists_equivalence)) /\ (((pfrep_right_append_exists_equivalence)=0))))) -> pfrep_left_append_exists_equivalence=pfrep_right_append_exists_equivalence))))))))))))))))))
Complete tactic proof in conservative notation
All 180 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 convolution at length exists.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial shift scale aligned sum exists.