An actual right-factor append satisfies A*append(C,c) formally equivalent to X*(A*C)+c*A through genuine products and arbitrary actual aligned sum outputs. Lengths are not falsely equated in empty cases, and no finite-field evaluation agreement replaces all formal coefficients.
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 db dc pb pc N qb qc K ub uc vb vc UB UC VB VC rb rc. (~((p) = 1) /\ forall pfa_factor_left_append_recurrence_prime pfa_factor_right_append_recurrence_prime. (p) = pfa_factor_left_append_recurrence_prime * pfa_factor_right_append_recurrence_prime -> pfa_factor_left_append_recurrence_prime = 1 \/ pfa_factor_right_append_recurrence_prime = 1) -> (forall mdr_i_pfp_append_recurrence_preserve mdr_a_pfp_append_recurrence_preserve. (exists mdr_gap_pfp_append_recurrence_preserveb. mdr_gap_pfp_append_recurrence_preserveb + S (mdr_i_pfp_append_recurrence_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_recurrence_preserveo. ff_h_mdr_pfp_append_recurrence_preserveo + S (mdr_a_pfp_append_recurrence_preserve) = S ((S (mdr_i_pfp_append_recurrence_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_recurrence_preserveo. bb = ff_q_mdr_pfp_append_recurrence_preserveo * S ((S (mdr_i_pfp_append_recurrence_preserve)) * bc) + (mdr_a_pfp_append_recurrence_preserve))) -> (((exists ff_h_mdr_pfp_append_recurrence_preserven. ff_h_mdr_pfp_append_recurrence_preserven + S (mdr_a_pfp_append_recurrence_preserve) = S ((S (mdr_i_pfp_append_recurrence_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_recurrence_preserven. db = ff_q_mdr_pfp_append_recurrence_preserven * S ((S (mdr_i_pfp_append_recurrence_preserve)) * dc) + (mdr_a_pfp_append_recurrence_preserve)))) -> (((exists ff_h_pfp_append_recurrence_last. ff_h_pfp_append_recurrence_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_recurrence_last. db = ff_q_pfp_append_recurrence_last * S ((S (M)) * dc) + (c))) -> (((forall fom_index_pfp_append_recurrence_oldleft. (exists fom_gap_pfp_append_recurrence_oldleft_index_bound. fom_gap_pfp_append_recurrence_oldleft_index_bound + S (fom_index_pfp_append_recurrence_oldleft) = L) -> exists fom_value_pfp_append_recurrence_oldleft. ((((exists fom_beta_height_pfp_append_recurrence_oldleft_entry. fom_beta_height_pfp_append_recurrence_oldleft_entry + S (fom_value_pfp_append_recurrence_oldleft) = S ((S (fom_index_pfp_append_recurrence_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_recurrence_oldleft_entry. ab = fom_beta_quotient_pfp_append_recurrence_oldleft_entry * S ((S (fom_index_pfp_append_recurrence_oldleft)) * ac) + (fom_value_pfp_append_recurrence_oldleft))) /\ (exists fom_gap_pfp_append_recurrence_oldleft_value_bound. fom_gap_pfp_append_recurrence_oldleft_value_bound + S (fom_value_pfp_append_recurrence_oldleft) = p))) /\ (((forall fom_index_pfp_append_recurrence_oldright. (exists fom_gap_pfp_append_recurrence_oldright_index_bound. fom_gap_pfp_append_recurrence_oldright_index_bound + S (fom_index_pfp_append_recurrence_oldright) = M) -> exists fom_value_pfp_append_recurrence_oldright. ((((exists fom_beta_height_pfp_append_recurrence_oldright_entry. fom_beta_height_pfp_append_recurrence_oldright_entry + S (fom_value_pfp_append_recurrence_oldright) = S ((S (fom_index_pfp_append_recurrence_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_append_recurrence_oldright_entry. bb = fom_beta_quotient_pfp_append_recurrence_oldright_entry * S ((S (fom_index_pfp_append_recurrence_oldright)) * bc) + (fom_value_pfp_append_recurrence_oldright))) /\ (exists fom_gap_pfp_append_recurrence_oldright_value_bound. fom_gap_pfp_append_recurrence_oldright_value_bound + S (fom_value_pfp_append_recurrence_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_append_recurrence_oldcoefficients. (exists pfa_gap_append_recurrence_oldcoefficientsbound. pfa_gap_append_recurrence_oldcoefficientsbound + S (pfc_index_append_recurrence_oldcoefficients) = (N)) -> exists pfc_value_append_recurrence_oldcoefficients. ((((exists ff_h_pfp_append_recurrence_oldcoefficientsentry. ff_h_pfp_append_recurrence_oldcoefficientsentry + S (pfc_value_append_recurrence_oldcoefficients) = S ((S (pfc_index_append_recurrence_oldcoefficients)) * pc)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientsentry. pb = ff_q_pfp_append_recurrence_oldcoefficientsentry * S ((S (pfc_index_append_recurrence_oldcoefficients)) * pc) + (pfc_value_append_recurrence_oldcoefficients))) /\ ((exists pfc_terms_code_append_recurrence_oldcoefficientscoefficient pfc_terms_scale_append_recurrence_oldcoefficientscoefficient pfc_natural_sum_append_recurrence_oldcoefficientscoefficient. ((forall pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal. (exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonalbound. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonalbound + S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal) = (S (pfc_index_append_recurrence_oldcoefficients))) -> exists pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry + S (pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_append_recurrence_oldcoefficientscoefficient = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient) + (pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm. (((pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)+pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm=(pfc_index_append_recurrence_oldcoefficients)) /\ ((((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_recurrence_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_append_recurrence_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_recurrence_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_append_recurrence_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_recurrence_oldcoefficientscoefficientdiagonal)=pfc_left_append_recurrence_oldcoefficientscoefficientdiagonalterm*pfc_right_append_recurrence_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient) = S ((S (S (pfc_index_append_recurrence_oldcoefficients))) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_recurrence_oldcoefficients))) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient))) /\ forall fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps = S (pfc_index_append_recurrence_oldcoefficients)) -> exists fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_recurrence_oldcoefficientscoefficient = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_oldcoefficientscoefficient) + (fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_recurrence_oldcoefficientscoefficientsum = fs_q_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_oldcoefficientscoefficientsum) + (fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_append_recurrence_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_recurrence_oldcoefficientscoefficientresiduebound. pfa_gap_append_recurrence_oldcoefficientscoefficientresiduebound + S (pfc_value_append_recurrence_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_append_recurrence_oldcoefficientscoefficientresiduecongruence pfa_offset_right_append_recurrence_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_recurrence_oldcoefficientscoefficient) + (p) * pfa_offset_left_append_recurrence_oldcoefficientscoefficientresiduecongruence = (pfc_value_append_recurrence_oldcoefficients) + (p) * pfa_offset_right_append_recurrence_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_append_recurrence_newleft. (exists fom_gap_pfp_append_recurrence_newleft_index_bound. fom_gap_pfp_append_recurrence_newleft_index_bound + S (fom_index_pfp_append_recurrence_newleft) = L) -> exists fom_value_pfp_append_recurrence_newleft. ((((exists fom_beta_height_pfp_append_recurrence_newleft_entry. fom_beta_height_pfp_append_recurrence_newleft_entry + S (fom_value_pfp_append_recurrence_newleft) = S ((S (fom_index_pfp_append_recurrence_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_append_recurrence_newleft_entry. ab = fom_beta_quotient_pfp_append_recurrence_newleft_entry * S ((S (fom_index_pfp_append_recurrence_newleft)) * ac) + (fom_value_pfp_append_recurrence_newleft))) /\ (exists fom_gap_pfp_append_recurrence_newleft_value_bound. fom_gap_pfp_append_recurrence_newleft_value_bound + S (fom_value_pfp_append_recurrence_newleft) = p))) /\ (((forall fom_index_pfp_append_recurrence_newright. (exists fom_gap_pfp_append_recurrence_newright_index_bound. fom_gap_pfp_append_recurrence_newright_index_bound + S (fom_index_pfp_append_recurrence_newright) = S M) -> exists fom_value_pfp_append_recurrence_newright. ((((exists fom_beta_height_pfp_append_recurrence_newright_entry. fom_beta_height_pfp_append_recurrence_newright_entry + S (fom_value_pfp_append_recurrence_newright) = S ((S (fom_index_pfp_append_recurrence_newright)) * dc)) /\ exists fom_beta_quotient_pfp_append_recurrence_newright_entry. db = fom_beta_quotient_pfp_append_recurrence_newright_entry * S ((S (fom_index_pfp_append_recurrence_newright)) * dc) + (fom_value_pfp_append_recurrence_newright))) /\ (exists fom_gap_pfp_append_recurrence_newright_value_bound. fom_gap_pfp_append_recurrence_newright_value_bound + S (fom_value_pfp_append_recurrence_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_append_recurrence_newcoefficients. (exists pfa_gap_append_recurrence_newcoefficientsbound. pfa_gap_append_recurrence_newcoefficientsbound + S (pfc_index_append_recurrence_newcoefficients) = (K)) -> exists pfc_value_append_recurrence_newcoefficients. ((((exists ff_h_pfp_append_recurrence_newcoefficientsentry. ff_h_pfp_append_recurrence_newcoefficientsentry + S (pfc_value_append_recurrence_newcoefficients) = S ((S (pfc_index_append_recurrence_newcoefficients)) * qc)) /\ exists ff_q_pfp_append_recurrence_newcoefficientsentry. qb = ff_q_pfp_append_recurrence_newcoefficientsentry * S ((S (pfc_index_append_recurrence_newcoefficients)) * qc) + (pfc_value_append_recurrence_newcoefficients))) /\ ((exists pfc_terms_code_append_recurrence_newcoefficientscoefficient pfc_terms_scale_append_recurrence_newcoefficientscoefficient pfc_natural_sum_append_recurrence_newcoefficientscoefficient. ((forall pfc_index_append_recurrence_newcoefficientscoefficientdiagonal. (exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonalbound. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonalbound + S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal) = (S (pfc_index_append_recurrence_newcoefficients))) -> exists pfc_value_append_recurrence_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry + S (pfc_value_append_recurrence_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry. pfc_terms_code_append_recurrence_newcoefficientscoefficient = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient) + (pfc_value_append_recurrence_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm. (((pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)+pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm=(pfc_index_append_recurrence_newcoefficients)) /\ ((((((exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_append_recurrence_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_append_recurrence_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_append_recurrence_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_append_recurrence_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_append_recurrence_newcoefficientscoefficientdiagonal)=pfc_left_append_recurrence_newcoefficientscoefficientdiagonalterm*pfc_right_append_recurrence_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_recurrence_newcoefficientscoefficientsum fs_v_pfc_append_recurrence_newcoefficientscoefficientsum. ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_start. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_start. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_append_recurrence_newcoefficientscoefficient) = S ((S (S (pfc_index_append_recurrence_newcoefficients))) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_append_recurrence_newcoefficients))) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (pfc_natural_sum_append_recurrence_newcoefficientscoefficient))) /\ forall fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps = S (pfc_index_append_recurrence_newcoefficients)) -> exists fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_append_recurrence_newcoefficientscoefficient = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_append_recurrence_newcoefficientscoefficient) + (fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_append_recurrence_newcoefficientscoefficientsum = fs_q_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_append_recurrence_newcoefficientscoefficientsum) + (fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps = fs_r_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps + fs_a_pfc_append_recurrence_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_append_recurrence_newcoefficientscoefficientresiduebound. pfa_gap_append_recurrence_newcoefficientscoefficientresiduebound + S (pfc_value_append_recurrence_newcoefficients) = (p)) /\ ((exists pfa_offset_left_append_recurrence_newcoefficientscoefficientresiduecongruence pfa_offset_right_append_recurrence_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_append_recurrence_newcoefficientscoefficient) + (p) * pfa_offset_left_append_recurrence_newcoefficientscoefficientresiduecongruence = (pfc_value_append_recurrence_newcoefficients) + (p) * pfa_offset_right_append_recurrence_newcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall mdr_i_pfp_append_recurrence_shiftprefix mdr_a_pfp_append_recurrence_shiftprefix. (exists mdr_gap_pfp_append_recurrence_shiftprefixb. mdr_gap_pfp_append_recurrence_shiftprefixb + S (mdr_i_pfp_append_recurrence_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_append_recurrence_shiftprefixo. ff_h_mdr_pfp_append_recurrence_shiftprefixo + S (mdr_a_pfp_append_recurrence_shiftprefix) = S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * pc)) /\ exists ff_q_mdr_pfp_append_recurrence_shiftprefixo. pb = ff_q_mdr_pfp_append_recurrence_shiftprefixo * S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * pc) + (mdr_a_pfp_append_recurrence_shiftprefix))) -> (((exists ff_h_mdr_pfp_append_recurrence_shiftprefixn. ff_h_mdr_pfp_append_recurrence_shiftprefixn + S (mdr_a_pfp_append_recurrence_shiftprefix) = S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * uc)) /\ exists ff_q_mdr_pfp_append_recurrence_shiftprefixn. ub = ff_q_mdr_pfp_append_recurrence_shiftprefixn * S ((S (mdr_i_pfp_append_recurrence_shiftprefix)) * uc) + (mdr_a_pfp_append_recurrence_shiftprefix)))) /\ ((((exists ff_h_pfp_append_recurrence_shiftlast. ff_h_pfp_append_recurrence_shiftlast + S (0) = S ((S (N)) * uc)) /\ exists ff_q_pfp_append_recurrence_shiftlast. ub = ff_q_pfp_append_recurrence_shiftlast * S ((S (N)) * uc) + (0)))))) -> (((exists pfa_gap_append_recurrence_scalescalar. pfa_gap_append_recurrence_scalescalar + S (c) = (p)) /\ ((forall pfp_index_append_recurrence_scale. (exists pfa_gap_append_recurrence_scaleindex. pfa_gap_append_recurrence_scaleindex + S (pfp_index_append_recurrence_scale) = (L)) -> exists pfp_source_append_recurrence_scale pfp_value_append_recurrence_scale. ((((exists ff_h_pfp_append_recurrence_scalesource. ff_h_pfp_append_recurrence_scalesource + S (pfp_source_append_recurrence_scale) = S ((S (pfp_index_append_recurrence_scale)) * ac)) /\ exists ff_q_pfp_append_recurrence_scalesource. ab = ff_q_pfp_append_recurrence_scalesource * S ((S (pfp_index_append_recurrence_scale)) * ac) + (pfp_source_append_recurrence_scale))) /\ (((((exists ff_h_pfp_append_recurrence_scaletarget. ff_h_pfp_append_recurrence_scaletarget + S (pfp_value_append_recurrence_scale) = S ((S (pfp_index_append_recurrence_scale)) * vc)) /\ exists ff_q_pfp_append_recurrence_scaletarget. vb = ff_q_pfp_append_recurrence_scaletarget * S ((S (pfp_index_append_recurrence_scale)) * vc) + (pfp_value_append_recurrence_scale))) /\ ((((exists pfa_gap_append_recurrence_scaleoperationleft. pfa_gap_append_recurrence_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_append_recurrence_scaleoperationright. pfa_gap_append_recurrence_scaleoperationright + S (pfp_source_append_recurrence_scale) = (p)) /\ ((((exists pfa_gap_append_recurrence_scaleoperationresultbound. pfa_gap_append_recurrence_scaleoperationresultbound + S (pfp_value_append_recurrence_scale) = (p)) /\ ((exists pfa_offset_left_append_recurrence_scaleoperationresultcongruence pfa_offset_right_append_recurrence_scaleoperationresultcongruence. ((c) * (pfp_source_append_recurrence_scale)) + (p) * pfa_offset_left_append_recurrence_scaleoperationresultcongruence = (pfp_value_append_recurrence_scale) + (p) * pfa_offset_right_append_recurrence_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_append_recurrence_leftzeros. (exists pfa_gap_append_recurrence_leftzerosindex. pfa_gap_append_recurrence_leftzerosindex + S (pfp_repeat_index_append_recurrence_leftzeros) = (L)) -> (((exists ff_h_pfp_append_recurrence_leftzerosentry. ff_h_pfp_append_recurrence_leftzerosentry + S (0) = S ((S (pfp_repeat_index_append_recurrence_leftzeros)) * UC)) /\ exists ff_q_pfp_append_recurrence_leftzerosentry. UB = ff_q_pfp_append_recurrence_leftzerosentry * S ((S (pfp_repeat_index_append_recurrence_leftzeros)) * UC) + (0)))) /\ ((forall pfrep_index_append_recurrence_left pfrep_value_append_recurrence_left. (exists pfa_gap_append_recurrence_leftbound. pfa_gap_append_recurrence_leftbound + S (pfrep_index_append_recurrence_left) = (S N)) -> (((exists ff_h_pfp_append_recurrence_leftinput. ff_h_pfp_append_recurrence_leftinput + S (pfrep_value_append_recurrence_left) = S ((S (pfrep_index_append_recurrence_left)) * uc)) /\ exists ff_q_pfp_append_recurrence_leftinput. ub = ff_q_pfp_append_recurrence_leftinput * S ((S (pfrep_index_append_recurrence_left)) * uc) + (pfrep_value_append_recurrence_left))) -> (((exists ff_h_pfp_append_recurrence_leftoutput. ff_h_pfp_append_recurrence_leftoutput + S (pfrep_value_append_recurrence_left) = S ((S ((L)+pfrep_index_append_recurrence_left)) * UC)) /\ exists ff_q_pfp_append_recurrence_leftoutput. UB = ff_q_pfp_append_recurrence_leftoutput * S ((S ((L)+pfrep_index_append_recurrence_left)) * UC) + (pfrep_value_append_recurrence_left))))))) -> (((forall pfp_repeat_index_append_recurrence_rightzeros. (exists pfa_gap_append_recurrence_rightzerosindex. pfa_gap_append_recurrence_rightzerosindex + S (pfp_repeat_index_append_recurrence_rightzeros) = (S N)) -> (((exists ff_h_pfp_append_recurrence_rightzerosentry. ff_h_pfp_append_recurrence_rightzerosentry + S (0) = S ((S (pfp_repeat_index_append_recurrence_rightzeros)) * VC)) /\ exists ff_q_pfp_append_recurrence_rightzerosentry. VB = ff_q_pfp_append_recurrence_rightzerosentry * S ((S (pfp_repeat_index_append_recurrence_rightzeros)) * VC) + (0)))) /\ ((forall pfrep_index_append_recurrence_right pfrep_value_append_recurrence_right. (exists pfa_gap_append_recurrence_rightbound. pfa_gap_append_recurrence_rightbound + S (pfrep_index_append_recurrence_right) = (L)) -> (((exists ff_h_pfp_append_recurrence_rightinput. ff_h_pfp_append_recurrence_rightinput + S (pfrep_value_append_recurrence_right) = S ((S (pfrep_index_append_recurrence_right)) * vc)) /\ exists ff_q_pfp_append_recurrence_rightinput. vb = ff_q_pfp_append_recurrence_rightinput * S ((S (pfrep_index_append_recurrence_right)) * vc) + (pfrep_value_append_recurrence_right))) -> (((exists ff_h_pfp_append_recurrence_rightoutput. ff_h_pfp_append_recurrence_rightoutput + S (pfrep_value_append_recurrence_right) = S ((S ((S N)+pfrep_index_append_recurrence_right)) * VC)) /\ exists ff_q_pfp_append_recurrence_rightoutput. VB = ff_q_pfp_append_recurrence_rightoutput * S ((S ((S N)+pfrep_index_append_recurrence_right)) * VC) + (pfrep_value_append_recurrence_right))))))) -> (forall pfp_index_append_recurrence_sum. (exists pfa_gap_append_recurrence_sumindex. pfa_gap_append_recurrence_sumindex + S (pfp_index_append_recurrence_sum) = (L+S N)) -> exists pfp_left_append_recurrence_sum pfp_right_append_recurrence_sum pfp_value_append_recurrence_sum. ((((exists ff_h_pfp_append_recurrence_sumleft. ff_h_pfp_append_recurrence_sumleft + S (pfp_left_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * UC)) /\ exists ff_q_pfp_append_recurrence_sumleft. UB = ff_q_pfp_append_recurrence_sumleft * S ((S (pfp_index_append_recurrence_sum)) * UC) + (pfp_left_append_recurrence_sum))) /\ (((((exists ff_h_pfp_append_recurrence_sumright. ff_h_pfp_append_recurrence_sumright + S (pfp_right_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * VC)) /\ exists ff_q_pfp_append_recurrence_sumright. VB = ff_q_pfp_append_recurrence_sumright * S ((S (pfp_index_append_recurrence_sum)) * VC) + (pfp_right_append_recurrence_sum))) /\ (((((exists ff_h_pfp_append_recurrence_sumtarget. ff_h_pfp_append_recurrence_sumtarget + S (pfp_value_append_recurrence_sum) = S ((S (pfp_index_append_recurrence_sum)) * rc)) /\ exists ff_q_pfp_append_recurrence_sumtarget. rb = ff_q_pfp_append_recurrence_sumtarget * S ((S (pfp_index_append_recurrence_sum)) * rc) + (pfp_value_append_recurrence_sum))) /\ ((((exists pfa_gap_append_recurrence_sumoperationleft. pfa_gap_append_recurrence_sumoperationleft + S (pfp_left_append_recurrence_sum) = (p)) /\ (((exists pfa_gap_append_recurrence_sumoperationright. pfa_gap_append_recurrence_sumoperationright + S (pfp_right_append_recurrence_sum) = (p)) /\ ((((exists pfa_gap_append_recurrence_sumoperationresultbound. pfa_gap_append_recurrence_sumoperationresultbound + S (pfp_value_append_recurrence_sum) = (p)) /\ ((exists pfa_offset_left_append_recurrence_sumoperationresultcongruence pfa_offset_right_append_recurrence_sumoperationresultcongruence. ((pfp_left_append_recurrence_sum) + (pfp_right_append_recurrence_sum)) + (p) * pfa_offset_left_append_recurrence_sumoperationresultcongruence = (pfp_value_append_recurrence_sum) + (p) * pfa_offset_right_append_recurrence_sumoperationresultcongruence)))))))))))))))) -> (forall pfrep_power_append_recurrence_result pfrep_left_append_recurrence_result pfrep_right_append_recurrence_result. ((exists pfrep_position_append_recurrence_resultfirst. ((pfrep_position_append_recurrence_resultfirst+S (pfrep_power_append_recurrence_result)=(K)) /\ ((((exists ff_h_pfp_append_recurrence_resultfirstentry. ff_h_pfp_append_recurrence_resultfirstentry + S (pfrep_left_append_recurrence_result) = S ((S (pfrep_position_append_recurrence_resultfirst)) * qc)) /\ exists ff_q_pfp_append_recurrence_resultfirstentry. qb = ff_q_pfp_append_recurrence_resultfirstentry * S ((S (pfrep_position_append_recurrence_resultfirst)) * qc) + (pfrep_left_append_recurrence_result)))))) \/ (((exists pfrep_gap_append_recurrence_resultfirstoutside. pfrep_gap_append_recurrence_resultfirstoutside+(K)=(pfrep_power_append_recurrence_result)) /\ (((pfrep_left_append_recurrence_result)=0))))) -> ((exists pfrep_position_append_recurrence_resultsecond. ((pfrep_position_append_recurrence_resultsecond+S (pfrep_power_append_recurrence_result)=(L+S N)) /\ ((((exists ff_h_pfp_append_recurrence_resultsecondentry. ff_h_pfp_append_recurrence_resultsecondentry + S (pfrep_right_append_recurrence_result) = S ((S (pfrep_position_append_recurrence_resultsecond)) * rc)) /\ exists ff_q_pfp_append_recurrence_resultsecondentry. rb = ff_q_pfp_append_recurrence_resultsecondentry * S ((S (pfrep_position_append_recurrence_resultsecond)) * rc) + (pfrep_right_append_recurrence_result)))))) \/ (((exists pfrep_gap_append_recurrence_resultsecondoutside. pfrep_gap_append_recurrence_resultsecondoutside+(L+S N)=(pfrep_power_append_recurrence_result)) /\ (((pfrep_right_append_recurrence_result)=0))))) -> pfrep_left_append_recurrence_result=pfrep_right_append_recurrence_result)
Complete tactic proof in conservative notation
All 293 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 append shift constant decomposition exists.
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 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 left pad equivalent.