At every natural coefficient index, an actual right append is the actual field sum of the old convolution coefficient and the product with the padded singleton constant, using genuine diagonal sums and residues rather than a finite-evaluation identity.
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 kb kc tb tc i u v w. (~((p) = 1) /\ forall pfa_factor_left_append_coefficient_prime pfa_factor_right_append_coefficient_prime. (p) = pfa_factor_left_append_coefficient_prime * pfa_factor_right_append_coefficient_prime -> pfa_factor_left_append_coefficient_prime = 1 \/ pfa_factor_right_append_coefficient_prime = 1) -> (forall fom_index_pfp_append_coefficient_old_coefficients. (exists fom_gap_pfp_append_coefficient_old_coefficients_index_bound. fom_gap_pfp_append_coefficient_old_coefficients_index_bound + S (fom_index_pfp_append_coefficient_old_coefficients) = M) -> exists fom_value_pfp_append_coefficient_old_coefficients. ((((exists fom_beta_height_pfp_append_coefficient_old_coefficients_entry. fom_beta_height_pfp_append_coefficient_old_coefficients_entry + S (fom_value_pfp_append_coefficient_old_coefficients) = S ((S (fom_index_pfp_append_coefficient_old_coefficients)) * bc)) /\ exists fom_beta_quotient_pfp_append_coefficient_old_coefficients_entry. bb = fom_beta_quotient_pfp_append_coefficient_old_coefficients_entry * S ((S (fom_index_pfp_append_coefficient_old_coefficients)) * bc) + (fom_value_pfp_append_coefficient_old_coefficients))) /\ (exists fom_gap_pfp_append_coefficient_old_coefficients_value_bound. fom_gap_pfp_append_coefficient_old_coefficients_value_bound + S (fom_value_pfp_append_coefficient_old_coefficients) = p))) -> (exists pfa_gap_append_coefficient_scalar. pfa_gap_append_coefficient_scalar + S (c) = (p)) -> (forall mdr_i_pfp_append_coefficient_preserve mdr_a_pfp_append_coefficient_preserve. (exists mdr_gap_pfp_append_coefficient_preserveb. mdr_gap_pfp_append_coefficient_preserveb + S (mdr_i_pfp_append_coefficient_preserve) = (M)) -> (((exists ff_h_mdr_pfp_append_coefficient_preserveo. ff_h_mdr_pfp_append_coefficient_preserveo + S (mdr_a_pfp_append_coefficient_preserve) = S ((S (mdr_i_pfp_append_coefficient_preserve)) * bc)) /\ exists ff_q_mdr_pfp_append_coefficient_preserveo. bb = ff_q_mdr_pfp_append_coefficient_preserveo * S ((S (mdr_i_pfp_append_coefficient_preserve)) * bc) + (mdr_a_pfp_append_coefficient_preserve))) -> (((exists ff_h_mdr_pfp_append_coefficient_preserven. ff_h_mdr_pfp_append_coefficient_preserven + S (mdr_a_pfp_append_coefficient_preserve) = S ((S (mdr_i_pfp_append_coefficient_preserve)) * dc)) /\ exists ff_q_mdr_pfp_append_coefficient_preserven. db = ff_q_mdr_pfp_append_coefficient_preserven * S ((S (mdr_i_pfp_append_coefficient_preserve)) * dc) + (mdr_a_pfp_append_coefficient_preserve)))) -> (((exists ff_h_pfp_append_coefficient_actual_last. ff_h_pfp_append_coefficient_actual_last + S (c) = S ((S (M)) * dc)) /\ exists ff_q_pfp_append_coefficient_actual_last. db = ff_q_pfp_append_coefficient_actual_last * S ((S (M)) * dc) + (c))) -> (((exists ff_h_pfp_append_coefficient_singleton. ff_h_pfp_append_coefficient_singleton + S (c) = S ((S (0)) * kc)) /\ exists ff_q_pfp_append_coefficient_singleton. kb = ff_q_pfp_append_coefficient_singleton * S ((S (0)) * kc) + (c))) -> (((forall pfp_repeat_index_append_coefficient_padzeros. (exists pfa_gap_append_coefficient_padzerosindex. pfa_gap_append_coefficient_padzerosindex + S (pfp_repeat_index_append_coefficient_padzeros) = (M)) -> (((exists ff_h_pfp_append_coefficient_padzerosentry. ff_h_pfp_append_coefficient_padzerosentry + S (0) = S ((S (pfp_repeat_index_append_coefficient_padzeros)) * tc)) /\ exists ff_q_pfp_append_coefficient_padzerosentry. tb = ff_q_pfp_append_coefficient_padzerosentry * S ((S (pfp_repeat_index_append_coefficient_padzeros)) * tc) + (0)))) /\ ((forall pfrep_index_append_coefficient_pad pfrep_value_append_coefficient_pad. (exists pfa_gap_append_coefficient_padbound. pfa_gap_append_coefficient_padbound + S (pfrep_index_append_coefficient_pad) = (1)) -> (((exists ff_h_pfp_append_coefficient_padinput. ff_h_pfp_append_coefficient_padinput + S (pfrep_value_append_coefficient_pad) = S ((S (pfrep_index_append_coefficient_pad)) * kc)) /\ exists ff_q_pfp_append_coefficient_padinput. kb = ff_q_pfp_append_coefficient_padinput * S ((S (pfrep_index_append_coefficient_pad)) * kc) + (pfrep_value_append_coefficient_pad))) -> (((exists ff_h_pfp_append_coefficient_padoutput. ff_h_pfp_append_coefficient_padoutput + S (pfrep_value_append_coefficient_pad) = S ((S ((M)+pfrep_index_append_coefficient_pad)) * tc)) /\ exists ff_q_pfp_append_coefficient_padoutput. tb = ff_q_pfp_append_coefficient_padoutput * S ((S ((M)+pfrep_index_append_coefficient_pad)) * tc) + (pfrep_value_append_coefficient_pad))))))) -> (exists pfc_terms_code_append_coefficient_old pfc_terms_scale_append_coefficient_old pfc_natural_sum_append_coefficient_old. ((forall pfc_index_append_coefficient_olddiagonal. (exists pfa_gap_append_coefficient_olddiagonalbound. pfa_gap_append_coefficient_olddiagonalbound + S (pfc_index_append_coefficient_olddiagonal) = (S (i))) -> exists pfc_value_append_coefficient_olddiagonal. ((((exists ff_h_pfp_append_coefficient_olddiagonalentry. ff_h_pfp_append_coefficient_olddiagonalentry + S (pfc_value_append_coefficient_olddiagonal) = S ((S (pfc_index_append_coefficient_olddiagonal)) * pfc_terms_scale_append_coefficient_old)) /\ exists ff_q_pfp_append_coefficient_olddiagonalentry. pfc_terms_code_append_coefficient_old = ff_q_pfp_append_coefficient_olddiagonalentry * S ((S (pfc_index_append_coefficient_olddiagonal)) * pfc_terms_scale_append_coefficient_old) + (pfc_value_append_coefficient_olddiagonal))) /\ ((exists pfc_complement_append_coefficient_olddiagonalterm pfc_left_append_coefficient_olddiagonalterm pfc_right_append_coefficient_olddiagonalterm. (((pfc_index_append_coefficient_olddiagonal)+pfc_complement_append_coefficient_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_olddiagonaltermleftinside. pfa_gap_append_coefficient_olddiagonaltermleftinside + S (pfc_index_append_coefficient_olddiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_olddiagonaltermleftentry. ff_h_pfp_append_coefficient_olddiagonaltermleftentry + S (pfc_left_append_coefficient_olddiagonalterm) = S ((S (pfc_index_append_coefficient_olddiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_olddiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_olddiagonaltermleftentry * S ((S (pfc_index_append_coefficient_olddiagonal)) * ac) + (pfc_left_append_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_olddiagonaltermleftoutside. pfc_gap_append_coefficient_olddiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_olddiagonal)) /\ (((pfc_left_append_coefficient_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_olddiagonaltermrightinside. pfa_gap_append_coefficient_olddiagonaltermrightinside + S (pfc_complement_append_coefficient_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_append_coefficient_olddiagonaltermrightentry. ff_h_pfp_append_coefficient_olddiagonaltermrightentry + S (pfc_right_append_coefficient_olddiagonalterm) = S ((S (pfc_complement_append_coefficient_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_append_coefficient_olddiagonaltermrightentry. bb = ff_q_pfp_append_coefficient_olddiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_olddiagonalterm)) * bc) + (pfc_right_append_coefficient_olddiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_olddiagonaltermrightoutside. pfc_gap_append_coefficient_olddiagonaltermrightoutside+(M)=(pfc_complement_append_coefficient_olddiagonalterm)) /\ (((pfc_right_append_coefficient_olddiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_olddiagonal)=pfc_left_append_coefficient_olddiagonalterm*pfc_right_append_coefficient_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_oldsum fs_v_pfc_append_coefficient_oldsum. ((((exists fs_h_pfc_append_coefficient_oldsum_body_start. fs_h_pfc_append_coefficient_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_start. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_oldsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_terminal. fs_h_pfc_append_coefficient_oldsum_body_terminal + S (pfc_natural_sum_append_coefficient_old) = S ((S (S (i))) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_terminal. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_oldsum) + (pfc_natural_sum_append_coefficient_old))) /\ forall fs_i_pfc_append_coefficient_oldsum_body_steps. (exists fs_lt_pfc_append_coefficient_oldsum_body_steps_bound. fs_lt_pfc_append_coefficient_oldsum_body_steps_bound + S fs_i_pfc_append_coefficient_oldsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_oldsum_body_steps fs_r_pfc_append_coefficient_oldsum_body_steps fs_s_pfc_append_coefficient_oldsum_body_steps. ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_summand. fs_h_pfc_append_coefficient_oldsum_body_steps_summand + S (fs_a_pfc_append_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * pfc_terms_scale_append_coefficient_old)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_summand. pfc_terms_code_append_coefficient_old = fs_q_pfc_append_coefficient_oldsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * pfc_terms_scale_append_coefficient_old) + (fs_a_pfc_append_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_partial. fs_h_pfc_append_coefficient_oldsum_body_steps_partial + S (fs_r_pfc_append_coefficient_oldsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_partial. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum) + (fs_r_pfc_append_coefficient_oldsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_oldsum_body_steps_successor. fs_h_pfc_append_coefficient_oldsum_body_steps_successor + S (fs_s_pfc_append_coefficient_oldsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum)) /\ exists fs_q_pfc_append_coefficient_oldsum_body_steps_successor. fs_u_pfc_append_coefficient_oldsum = fs_q_pfc_append_coefficient_oldsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_oldsum_body_steps)) * fs_v_pfc_append_coefficient_oldsum) + (fs_s_pfc_append_coefficient_oldsum_body_steps))) /\ fs_s_pfc_append_coefficient_oldsum_body_steps = fs_r_pfc_append_coefficient_oldsum_body_steps + fs_a_pfc_append_coefficient_oldsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_oldresiduebound. pfa_gap_append_coefficient_oldresiduebound + S (u) = (p)) /\ ((exists pfa_offset_left_append_coefficient_oldresiduecongruence pfa_offset_right_append_coefficient_oldresiduecongruence. (pfc_natural_sum_append_coefficient_old) + (p) * pfa_offset_left_append_coefficient_oldresiduecongruence = (u) + (p) * pfa_offset_right_append_coefficient_oldresiduecongruence))))))))) -> (exists pfc_terms_code_append_coefficient_constant pfc_terms_scale_append_coefficient_constant pfc_natural_sum_append_coefficient_constant. ((forall pfc_index_append_coefficient_constantdiagonal. (exists pfa_gap_append_coefficient_constantdiagonalbound. pfa_gap_append_coefficient_constantdiagonalbound + S (pfc_index_append_coefficient_constantdiagonal) = (S (i))) -> exists pfc_value_append_coefficient_constantdiagonal. ((((exists ff_h_pfp_append_coefficient_constantdiagonalentry. ff_h_pfp_append_coefficient_constantdiagonalentry + S (pfc_value_append_coefficient_constantdiagonal) = S ((S (pfc_index_append_coefficient_constantdiagonal)) * pfc_terms_scale_append_coefficient_constant)) /\ exists ff_q_pfp_append_coefficient_constantdiagonalentry. pfc_terms_code_append_coefficient_constant = ff_q_pfp_append_coefficient_constantdiagonalentry * S ((S (pfc_index_append_coefficient_constantdiagonal)) * pfc_terms_scale_append_coefficient_constant) + (pfc_value_append_coefficient_constantdiagonal))) /\ ((exists pfc_complement_append_coefficient_constantdiagonalterm pfc_left_append_coefficient_constantdiagonalterm pfc_right_append_coefficient_constantdiagonalterm. (((pfc_index_append_coefficient_constantdiagonal)+pfc_complement_append_coefficient_constantdiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_constantdiagonaltermleftinside. pfa_gap_append_coefficient_constantdiagonaltermleftinside + S (pfc_index_append_coefficient_constantdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_constantdiagonaltermleftentry. ff_h_pfp_append_coefficient_constantdiagonaltermleftentry + S (pfc_left_append_coefficient_constantdiagonalterm) = S ((S (pfc_index_append_coefficient_constantdiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_constantdiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_constantdiagonaltermleftentry * S ((S (pfc_index_append_coefficient_constantdiagonal)) * ac) + (pfc_left_append_coefficient_constantdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_constantdiagonaltermleftoutside. pfc_gap_append_coefficient_constantdiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_constantdiagonal)) /\ (((pfc_left_append_coefficient_constantdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_constantdiagonaltermrightinside. pfa_gap_append_coefficient_constantdiagonaltermrightinside + S (pfc_complement_append_coefficient_constantdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_coefficient_constantdiagonaltermrightentry. ff_h_pfp_append_coefficient_constantdiagonaltermrightentry + S (pfc_right_append_coefficient_constantdiagonalterm) = S ((S (pfc_complement_append_coefficient_constantdiagonalterm)) * tc)) /\ exists ff_q_pfp_append_coefficient_constantdiagonaltermrightentry. tb = ff_q_pfp_append_coefficient_constantdiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_constantdiagonalterm)) * tc) + (pfc_right_append_coefficient_constantdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_constantdiagonaltermrightoutside. pfc_gap_append_coefficient_constantdiagonaltermrightoutside+(S M)=(pfc_complement_append_coefficient_constantdiagonalterm)) /\ (((pfc_right_append_coefficient_constantdiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_constantdiagonal)=pfc_left_append_coefficient_constantdiagonalterm*pfc_right_append_coefficient_constantdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_constantsum fs_v_pfc_append_coefficient_constantsum. ((((exists fs_h_pfc_append_coefficient_constantsum_body_start. fs_h_pfc_append_coefficient_constantsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_start. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_constantsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_terminal. fs_h_pfc_append_coefficient_constantsum_body_terminal + S (pfc_natural_sum_append_coefficient_constant) = S ((S (S (i))) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_terminal. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_constantsum) + (pfc_natural_sum_append_coefficient_constant))) /\ forall fs_i_pfc_append_coefficient_constantsum_body_steps. (exists fs_lt_pfc_append_coefficient_constantsum_body_steps_bound. fs_lt_pfc_append_coefficient_constantsum_body_steps_bound + S fs_i_pfc_append_coefficient_constantsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_constantsum_body_steps fs_r_pfc_append_coefficient_constantsum_body_steps fs_s_pfc_append_coefficient_constantsum_body_steps. ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_summand. fs_h_pfc_append_coefficient_constantsum_body_steps_summand + S (fs_a_pfc_append_coefficient_constantsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * pfc_terms_scale_append_coefficient_constant)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_summand. pfc_terms_code_append_coefficient_constant = fs_q_pfc_append_coefficient_constantsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * pfc_terms_scale_append_coefficient_constant) + (fs_a_pfc_append_coefficient_constantsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_partial. fs_h_pfc_append_coefficient_constantsum_body_steps_partial + S (fs_r_pfc_append_coefficient_constantsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_partial. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum) + (fs_r_pfc_append_coefficient_constantsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_constantsum_body_steps_successor. fs_h_pfc_append_coefficient_constantsum_body_steps_successor + S (fs_s_pfc_append_coefficient_constantsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum)) /\ exists fs_q_pfc_append_coefficient_constantsum_body_steps_successor. fs_u_pfc_append_coefficient_constantsum = fs_q_pfc_append_coefficient_constantsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_constantsum_body_steps)) * fs_v_pfc_append_coefficient_constantsum) + (fs_s_pfc_append_coefficient_constantsum_body_steps))) /\ fs_s_pfc_append_coefficient_constantsum_body_steps = fs_r_pfc_append_coefficient_constantsum_body_steps + fs_a_pfc_append_coefficient_constantsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_constantresiduebound. pfa_gap_append_coefficient_constantresiduebound + S (v) = (p)) /\ ((exists pfa_offset_left_append_coefficient_constantresiduecongruence pfa_offset_right_append_coefficient_constantresiduecongruence. (pfc_natural_sum_append_coefficient_constant) + (p) * pfa_offset_left_append_coefficient_constantresiduecongruence = (v) + (p) * pfa_offset_right_append_coefficient_constantresiduecongruence))))))))) -> (exists pfc_terms_code_append_coefficient_new pfc_terms_scale_append_coefficient_new pfc_natural_sum_append_coefficient_new. ((forall pfc_index_append_coefficient_newdiagonal. (exists pfa_gap_append_coefficient_newdiagonalbound. pfa_gap_append_coefficient_newdiagonalbound + S (pfc_index_append_coefficient_newdiagonal) = (S (i))) -> exists pfc_value_append_coefficient_newdiagonal. ((((exists ff_h_pfp_append_coefficient_newdiagonalentry. ff_h_pfp_append_coefficient_newdiagonalentry + S (pfc_value_append_coefficient_newdiagonal) = S ((S (pfc_index_append_coefficient_newdiagonal)) * pfc_terms_scale_append_coefficient_new)) /\ exists ff_q_pfp_append_coefficient_newdiagonalentry. pfc_terms_code_append_coefficient_new = ff_q_pfp_append_coefficient_newdiagonalentry * S ((S (pfc_index_append_coefficient_newdiagonal)) * pfc_terms_scale_append_coefficient_new) + (pfc_value_append_coefficient_newdiagonal))) /\ ((exists pfc_complement_append_coefficient_newdiagonalterm pfc_left_append_coefficient_newdiagonalterm pfc_right_append_coefficient_newdiagonalterm. (((pfc_index_append_coefficient_newdiagonal)+pfc_complement_append_coefficient_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_append_coefficient_newdiagonaltermleftinside. pfa_gap_append_coefficient_newdiagonaltermleftinside + S (pfc_index_append_coefficient_newdiagonal) = (L)) /\ ((((exists ff_h_pfp_append_coefficient_newdiagonaltermleftentry. ff_h_pfp_append_coefficient_newdiagonaltermleftentry + S (pfc_left_append_coefficient_newdiagonalterm) = S ((S (pfc_index_append_coefficient_newdiagonal)) * ac)) /\ exists ff_q_pfp_append_coefficient_newdiagonaltermleftentry. ab = ff_q_pfp_append_coefficient_newdiagonaltermleftentry * S ((S (pfc_index_append_coefficient_newdiagonal)) * ac) + (pfc_left_append_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_newdiagonaltermleftoutside. pfc_gap_append_coefficient_newdiagonaltermleftoutside+(L)=(pfc_index_append_coefficient_newdiagonal)) /\ (((pfc_left_append_coefficient_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_append_coefficient_newdiagonaltermrightinside. pfa_gap_append_coefficient_newdiagonaltermrightinside + S (pfc_complement_append_coefficient_newdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_append_coefficient_newdiagonaltermrightentry. ff_h_pfp_append_coefficient_newdiagonaltermrightentry + S (pfc_right_append_coefficient_newdiagonalterm) = S ((S (pfc_complement_append_coefficient_newdiagonalterm)) * dc)) /\ exists ff_q_pfp_append_coefficient_newdiagonaltermrightentry. db = ff_q_pfp_append_coefficient_newdiagonaltermrightentry * S ((S (pfc_complement_append_coefficient_newdiagonalterm)) * dc) + (pfc_right_append_coefficient_newdiagonalterm)))))) \/ (((exists pfc_gap_append_coefficient_newdiagonaltermrightoutside. pfc_gap_append_coefficient_newdiagonaltermrightoutside+(S M)=(pfc_complement_append_coefficient_newdiagonalterm)) /\ (((pfc_right_append_coefficient_newdiagonalterm)=0))))) /\ (((pfc_value_append_coefficient_newdiagonal)=pfc_left_append_coefficient_newdiagonalterm*pfc_right_append_coefficient_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_append_coefficient_newsum fs_v_pfc_append_coefficient_newsum. ((((exists fs_h_pfc_append_coefficient_newsum_body_start. fs_h_pfc_append_coefficient_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_start. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_start * S ((S (0)) * fs_v_pfc_append_coefficient_newsum) + (0))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_terminal. fs_h_pfc_append_coefficient_newsum_body_terminal + S (pfc_natural_sum_append_coefficient_new) = S ((S (S (i))) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_terminal. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_append_coefficient_newsum) + (pfc_natural_sum_append_coefficient_new))) /\ forall fs_i_pfc_append_coefficient_newsum_body_steps. (exists fs_lt_pfc_append_coefficient_newsum_body_steps_bound. fs_lt_pfc_append_coefficient_newsum_body_steps_bound + S fs_i_pfc_append_coefficient_newsum_body_steps = S (i)) -> exists fs_a_pfc_append_coefficient_newsum_body_steps fs_r_pfc_append_coefficient_newsum_body_steps fs_s_pfc_append_coefficient_newsum_body_steps. ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_summand. fs_h_pfc_append_coefficient_newsum_body_steps_summand + S (fs_a_pfc_append_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * pfc_terms_scale_append_coefficient_new)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_summand. pfc_terms_code_append_coefficient_new = fs_q_pfc_append_coefficient_newsum_body_steps_summand * S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * pfc_terms_scale_append_coefficient_new) + (fs_a_pfc_append_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_partial. fs_h_pfc_append_coefficient_newsum_body_steps_partial + S (fs_r_pfc_append_coefficient_newsum_body_steps) = S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_partial. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_steps_partial * S ((S (fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum) + (fs_r_pfc_append_coefficient_newsum_body_steps))) /\ ((((exists fs_h_pfc_append_coefficient_newsum_body_steps_successor. fs_h_pfc_append_coefficient_newsum_body_steps_successor + S (fs_s_pfc_append_coefficient_newsum_body_steps) = S ((S (S fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum)) /\ exists fs_q_pfc_append_coefficient_newsum_body_steps_successor. fs_u_pfc_append_coefficient_newsum = fs_q_pfc_append_coefficient_newsum_body_steps_successor * S ((S (S fs_i_pfc_append_coefficient_newsum_body_steps)) * fs_v_pfc_append_coefficient_newsum) + (fs_s_pfc_append_coefficient_newsum_body_steps))) /\ fs_s_pfc_append_coefficient_newsum_body_steps = fs_r_pfc_append_coefficient_newsum_body_steps + fs_a_pfc_append_coefficient_newsum_body_steps)))))) /\ ((((exists pfa_gap_append_coefficient_newresiduebound. pfa_gap_append_coefficient_newresiduebound + S (w) = (p)) /\ ((exists pfa_offset_left_append_coefficient_newresiduecongruence pfa_offset_right_append_coefficient_newresiduecongruence. (pfc_natural_sum_append_coefficient_new) + (p) * pfa_offset_left_append_coefficient_newresiduecongruence = (w) + (p) * pfa_offset_right_append_coefficient_newresiduecongruence))))))))) -> (((exists pfa_gap_append_coefficient_resultleft. pfa_gap_append_coefficient_resultleft + S (u) = (p)) /\ (((exists pfa_gap_append_coefficient_resultright. pfa_gap_append_coefficient_resultright + S (v) = (p)) /\ ((((exists pfa_gap_append_coefficient_resultresultbound. pfa_gap_append_coefficient_resultresultbound + S (w) = (p)) /\ ((exists pfa_offset_left_append_coefficient_resultresultcongruence pfa_offset_right_append_coefficient_resultresultcongruence. ((u) + (v)) + (p) * pfa_offset_left_append_coefficient_resultresultcongruence = (w) + (p) * pfa_offset_right_append_coefficient_resultresultcongruence)))))))))
Complete tactic proof in conservative notation
All 94 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 shift exists.