PX0079

prime_field_polynomial_convolution_equivalent_congruent

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Two actual convolution outputs represent the same formal polynomial whenever their respective factors do, with all four representation lengths independent. A genuine mixed product is constructed from canonical inputs supplied by the actual products; no output identity or extra field hypothesis is assumed.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N AB AC H BB BC I CB CC K. (~(p=0)) -> (forall pfrep_power_congruent_both_left pfrep_left_congruent_both_left pfrep_right_congruent_both_left. ((exists pfrep_position_congruent_both_leftfirst. ((pfrep_position_congruent_both_leftfirst+S (pfrep_power_congruent_both_left)=(L)) /\ ((((exists ff_h_pfp_congruent_both_leftfirstentry. ff_h_pfp_congruent_both_leftfirstentry + S (pfrep_left_congruent_both_left) = S ((S (pfrep_position_congruent_both_leftfirst)) * ac)) /\ exists ff_q_pfp_congruent_both_leftfirstentry. ab = ff_q_pfp_congruent_both_leftfirstentry * S ((S (pfrep_position_congruent_both_leftfirst)) * ac) + (pfrep_left_congruent_both_left)))))) \/ (((exists pfrep_gap_congruent_both_leftfirstoutside. pfrep_gap_congruent_both_leftfirstoutside+(L)=(pfrep_power_congruent_both_left)) /\ (((pfrep_left_congruent_both_left)=0))))) -> ((exists pfrep_position_congruent_both_leftsecond. ((pfrep_position_congruent_both_leftsecond+S (pfrep_power_congruent_both_left)=(H)) /\ ((((exists ff_h_pfp_congruent_both_leftsecondentry. ff_h_pfp_congruent_both_leftsecondentry + S (pfrep_right_congruent_both_left) = S ((S (pfrep_position_congruent_both_leftsecond)) * AC)) /\ exists ff_q_pfp_congruent_both_leftsecondentry. AB = ff_q_pfp_congruent_both_leftsecondentry * S ((S (pfrep_position_congruent_both_leftsecond)) * AC) + (pfrep_right_congruent_both_left)))))) \/ (((exists pfrep_gap_congruent_both_leftsecondoutside. pfrep_gap_congruent_both_leftsecondoutside+(H)=(pfrep_power_congruent_both_left)) /\ (((pfrep_right_congruent_both_left)=0))))) -> pfrep_left_congruent_both_left=pfrep_right_congruent_both_left) -> (forall pfrep_power_congruent_both_right pfrep_left_congruent_both_right pfrep_right_congruent_both_right. ((exists pfrep_position_congruent_both_rightfirst. ((pfrep_position_congruent_both_rightfirst+S (pfrep_power_congruent_both_right)=(M)) /\ ((((exists ff_h_pfp_congruent_both_rightfirstentry. ff_h_pfp_congruent_both_rightfirstentry + S (pfrep_left_congruent_both_right) = S ((S (pfrep_position_congruent_both_rightfirst)) * bc)) /\ exists ff_q_pfp_congruent_both_rightfirstentry. bb = ff_q_pfp_congruent_both_rightfirstentry * S ((S (pfrep_position_congruent_both_rightfirst)) * bc) + (pfrep_left_congruent_both_right)))))) \/ (((exists pfrep_gap_congruent_both_rightfirstoutside. pfrep_gap_congruent_both_rightfirstoutside+(M)=(pfrep_power_congruent_both_right)) /\ (((pfrep_left_congruent_both_right)=0))))) -> ((exists pfrep_position_congruent_both_rightsecond. ((pfrep_position_congruent_both_rightsecond+S (pfrep_power_congruent_both_right)=(I)) /\ ((((exists ff_h_pfp_congruent_both_rightsecondentry. ff_h_pfp_congruent_both_rightsecondentry + S (pfrep_right_congruent_both_right) = S ((S (pfrep_position_congruent_both_rightsecond)) * BC)) /\ exists ff_q_pfp_congruent_both_rightsecondentry. BB = ff_q_pfp_congruent_both_rightsecondentry * S ((S (pfrep_position_congruent_both_rightsecond)) * BC) + (pfrep_right_congruent_both_right)))))) \/ (((exists pfrep_gap_congruent_both_rightsecondoutside. pfrep_gap_congruent_both_rightsecondoutside+(I)=(pfrep_power_congruent_both_right)) /\ (((pfrep_right_congruent_both_right)=0))))) -> pfrep_left_congruent_both_right=pfrep_right_congruent_both_right) -> (((forall fom_index_pfp_congruent_both_originalleft. (exists fom_gap_pfp_congruent_both_originalleft_index_bound. fom_gap_pfp_congruent_both_originalleft_index_bound + S (fom_index_pfp_congruent_both_originalleft) = L) -> exists fom_value_pfp_congruent_both_originalleft. ((((exists fom_beta_height_pfp_congruent_both_originalleft_entry. fom_beta_height_pfp_congruent_both_originalleft_entry + S (fom_value_pfp_congruent_both_originalleft) = S ((S (fom_index_pfp_congruent_both_originalleft)) * ac)) /\ exists fom_beta_quotient_pfp_congruent_both_originalleft_entry. ab = fom_beta_quotient_pfp_congruent_both_originalleft_entry * S ((S (fom_index_pfp_congruent_both_originalleft)) * ac) + (fom_value_pfp_congruent_both_originalleft))) /\ (exists fom_gap_pfp_congruent_both_originalleft_value_bound. fom_gap_pfp_congruent_both_originalleft_value_bound + S (fom_value_pfp_congruent_both_originalleft) = p))) /\ (((forall fom_index_pfp_congruent_both_originalright. (exists fom_gap_pfp_congruent_both_originalright_index_bound. fom_gap_pfp_congruent_both_originalright_index_bound + S (fom_index_pfp_congruent_both_originalright) = M) -> exists fom_value_pfp_congruent_both_originalright. ((((exists fom_beta_height_pfp_congruent_both_originalright_entry. fom_beta_height_pfp_congruent_both_originalright_entry + S (fom_value_pfp_congruent_both_originalright) = S ((S (fom_index_pfp_congruent_both_originalright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_both_originalright_entry. bb = fom_beta_quotient_pfp_congruent_both_originalright_entry * S ((S (fom_index_pfp_congruent_both_originalright)) * bc) + (fom_value_pfp_congruent_both_originalright))) /\ (exists fom_gap_pfp_congruent_both_originalright_value_bound. fom_gap_pfp_congruent_both_originalright_value_bound + S (fom_value_pfp_congruent_both_originalright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_congruent_both_originalcoefficients. (exists pfa_gap_congruent_both_originalcoefficientsbound. pfa_gap_congruent_both_originalcoefficientsbound + S (pfc_index_congruent_both_originalcoefficients) = (N)) -> exists pfc_value_congruent_both_originalcoefficients. ((((exists ff_h_pfp_congruent_both_originalcoefficientsentry. ff_h_pfp_congruent_both_originalcoefficientsentry + S (pfc_value_congruent_both_originalcoefficients) = S ((S (pfc_index_congruent_both_originalcoefficients)) * cc)) /\ exists ff_q_pfp_congruent_both_originalcoefficientsentry. cb = ff_q_pfp_congruent_both_originalcoefficientsentry * S ((S (pfc_index_congruent_both_originalcoefficients)) * cc) + (pfc_value_congruent_both_originalcoefficients))) /\ ((exists pfc_terms_code_congruent_both_originalcoefficientscoefficient pfc_terms_scale_congruent_both_originalcoefficientscoefficient pfc_natural_sum_congruent_both_originalcoefficientscoefficient. ((forall pfc_index_congruent_both_originalcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonalbound. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_both_originalcoefficients))) -> exists pfc_value_congruent_both_originalcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_both_originalcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_both_originalcoefficientscoefficient = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient) + (pfc_value_congruent_both_originalcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)+pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm=(pfc_index_congruent_both_originalcoefficients)) /\ ((((((exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * ac) + (pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_both_originalcoefficientscoefficientdiagonal)=pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm*pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_both_originalcoefficientscoefficientsum fs_v_pfc_congruent_both_originalcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_both_originalcoefficientscoefficient) = S ((S (S (pfc_index_congruent_both_originalcoefficients))) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_both_originalcoefficients))) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (pfc_natural_sum_congruent_both_originalcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_both_originalcoefficients)) -> exists fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_both_originalcoefficientscoefficient = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient) + (fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_both_originalcoefficientscoefficientresiduebound. pfa_gap_congruent_both_originalcoefficientscoefficientresiduebound + S (pfc_value_congruent_both_originalcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_both_originalcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_both_originalcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_both_originalcoefficientscoefficient) + (p) * pfa_offset_left_congruent_both_originalcoefficientscoefficientresiduecongruence = (pfc_value_congruent_both_originalcoefficients) + (p) * pfa_offset_right_congruent_both_originalcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_congruent_both_otherleft. (exists fom_gap_pfp_congruent_both_otherleft_index_bound. fom_gap_pfp_congruent_both_otherleft_index_bound + S (fom_index_pfp_congruent_both_otherleft) = H) -> exists fom_value_pfp_congruent_both_otherleft. ((((exists fom_beta_height_pfp_congruent_both_otherleft_entry. fom_beta_height_pfp_congruent_both_otherleft_entry + S (fom_value_pfp_congruent_both_otherleft) = S ((S (fom_index_pfp_congruent_both_otherleft)) * AC)) /\ exists fom_beta_quotient_pfp_congruent_both_otherleft_entry. AB = fom_beta_quotient_pfp_congruent_both_otherleft_entry * S ((S (fom_index_pfp_congruent_both_otherleft)) * AC) + (fom_value_pfp_congruent_both_otherleft))) /\ (exists fom_gap_pfp_congruent_both_otherleft_value_bound. fom_gap_pfp_congruent_both_otherleft_value_bound + S (fom_value_pfp_congruent_both_otherleft) = p))) /\ (((forall fom_index_pfp_congruent_both_otherright. (exists fom_gap_pfp_congruent_both_otherright_index_bound. fom_gap_pfp_congruent_both_otherright_index_bound + S (fom_index_pfp_congruent_both_otherright) = I) -> exists fom_value_pfp_congruent_both_otherright. ((((exists fom_beta_height_pfp_congruent_both_otherright_entry. fom_beta_height_pfp_congruent_both_otherright_entry + S (fom_value_pfp_congruent_both_otherright) = S ((S (fom_index_pfp_congruent_both_otherright)) * BC)) /\ exists fom_beta_quotient_pfp_congruent_both_otherright_entry. BB = fom_beta_quotient_pfp_congruent_both_otherright_entry * S ((S (fom_index_pfp_congruent_both_otherright)) * BC) + (fom_value_pfp_congruent_both_otherright))) /\ (exists fom_gap_pfp_congruent_both_otherright_value_bound. fom_gap_pfp_congruent_both_otherright_value_bound + S (fom_value_pfp_congruent_both_otherright) = p))) /\ (((((((H)=0 \/ (I)=0) /\ (((K)=0)))) \/ (((~((H)=0)) /\ (((~((I)=0)) /\ (((H)+(I)=S (K)))))))) /\ ((forall pfc_index_congruent_both_othercoefficients. (exists pfa_gap_congruent_both_othercoefficientsbound. pfa_gap_congruent_both_othercoefficientsbound + S (pfc_index_congruent_both_othercoefficients) = (K)) -> exists pfc_value_congruent_both_othercoefficients. ((((exists ff_h_pfp_congruent_both_othercoefficientsentry. ff_h_pfp_congruent_both_othercoefficientsentry + S (pfc_value_congruent_both_othercoefficients) = S ((S (pfc_index_congruent_both_othercoefficients)) * CC)) /\ exists ff_q_pfp_congruent_both_othercoefficientsentry. CB = ff_q_pfp_congruent_both_othercoefficientsentry * S ((S (pfc_index_congruent_both_othercoefficients)) * CC) + (pfc_value_congruent_both_othercoefficients))) /\ ((exists pfc_terms_code_congruent_both_othercoefficientscoefficient pfc_terms_scale_congruent_both_othercoefficientscoefficient pfc_natural_sum_congruent_both_othercoefficientscoefficient. ((forall pfc_index_congruent_both_othercoefficientscoefficientdiagonal. (exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonalbound. pfa_gap_congruent_both_othercoefficientscoefficientdiagonalbound + S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal) = (S (pfc_index_congruent_both_othercoefficients))) -> exists pfc_value_congruent_both_othercoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonalentry + S (pfc_value_congruent_both_othercoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_both_othercoefficientscoefficient = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient) + (pfc_value_congruent_both_othercoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm. (((pfc_index_congruent_both_othercoefficientscoefficientdiagonal)+pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm=(pfc_index_congruent_both_othercoefficients)) /\ ((((((exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * AC) + (pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm) = (I)) /\ ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightoutside+(I)=(pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_both_othercoefficientscoefficientdiagonal)=pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm*pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_both_othercoefficientscoefficientsum fs_v_pfc_congruent_both_othercoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_start. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_start. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_both_othercoefficientscoefficient) = S ((S (S (pfc_index_congruent_both_othercoefficients))) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_both_othercoefficients))) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (pfc_natural_sum_congruent_both_othercoefficientscoefficient))) /\ forall fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps = S (pfc_index_congruent_both_othercoefficients)) -> exists fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_both_othercoefficientscoefficient = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient) + (fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_both_othercoefficientscoefficientresiduebound. pfa_gap_congruent_both_othercoefficientscoefficientresiduebound + S (pfc_value_congruent_both_othercoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_both_othercoefficientscoefficientresiduecongruence pfa_offset_right_congruent_both_othercoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_both_othercoefficientscoefficient) + (p) * pfa_offset_left_congruent_both_othercoefficientscoefficientresiduecongruence = (pfc_value_congruent_both_othercoefficients) + (p) * pfa_offset_right_congruent_both_othercoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_congruent_both_result pfrep_left_congruent_both_result pfrep_right_congruent_both_result. ((exists pfrep_position_congruent_both_resultfirst. ((pfrep_position_congruent_both_resultfirst+S (pfrep_power_congruent_both_result)=(N)) /\ ((((exists ff_h_pfp_congruent_both_resultfirstentry. ff_h_pfp_congruent_both_resultfirstentry + S (pfrep_left_congruent_both_result) = S ((S (pfrep_position_congruent_both_resultfirst)) * cc)) /\ exists ff_q_pfp_congruent_both_resultfirstentry. cb = ff_q_pfp_congruent_both_resultfirstentry * S ((S (pfrep_position_congruent_both_resultfirst)) * cc) + (pfrep_left_congruent_both_result)))))) \/ (((exists pfrep_gap_congruent_both_resultfirstoutside. pfrep_gap_congruent_both_resultfirstoutside+(N)=(pfrep_power_congruent_both_result)) /\ (((pfrep_left_congruent_both_result)=0))))) -> ((exists pfrep_position_congruent_both_resultsecond. ((pfrep_position_congruent_both_resultsecond+S (pfrep_power_congruent_both_result)=(K)) /\ ((((exists ff_h_pfp_congruent_both_resultsecondentry. ff_h_pfp_congruent_both_resultsecondentry + S (pfrep_right_congruent_both_result) = S ((S (pfrep_position_congruent_both_resultsecond)) * CC)) /\ exists ff_q_pfp_congruent_both_resultsecondentry. CB = ff_q_pfp_congruent_both_resultsecondentry * S ((S (pfrep_position_congruent_both_resultsecond)) * CC) + (pfrep_right_congruent_both_result)))))) \/ (((exists pfrep_gap_congruent_both_resultsecondoutside. pfrep_gap_congruent_both_resultsecondoutside+(K)=(pfrep_power_congruent_both_result)) /\ (((pfrep_right_congruent_both_result)=0))))) -> pfrep_left_congruent_both_result=pfrep_right_congruent_both_result)

Constructive proof overview

Generated structural guide

Two actual convolution outputs represent the same formal polynomial whenever their respective factors do, with all four representation lengths independent. A genuine mixed product is constructed from canonical inputs supplied by the actual products; no output identity or extra field hypothesis is assumed.

The unchanged tactic script uses 5 declared prerequisites and contains 107 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

polynomial_product_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized PX0010 prime_field_polynomial_equivalent_transitive PX0077 prime_field_polynomial_convolution_equivalent_congruent_left PX0078 prime_field_polynomial_convolution_equivalent_congruent_right

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

107 script commands · 18 reading checkpoints · 4 local claims

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.

Named ingredients (3)
prime field polynomial equivalent transitiveprime field polynomial convolution equivalent congruent leftprime field polynomial convolution equivalent congruent right

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro cb
  9. L9
    intro cc
  10. L10
    intro N
02Fix variables and assumptionsL11–20

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro AB
  2. L12
    intro AC
  3. L13
    intro H
  4. L14
    intro BB
  5. L15
    intro BC
  6. L16
    intro I
  7. L17
    intro CB
  8. L18
    intro CC
  9. L19
    intro K
  10. L20
    intro hp
03Fix variables and assumptionsL21–24

Work with arbitrary variables or the premises of the current implication.

  1. L21
    intro hA
  2. L22
    intro hB
  3. L23
    intro hc
  4. L24
    intro hd
04Establish hsourceL25–26

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hsource : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Definitions: FpPolyProduct
  2. L26
    exact hc
05Separate the logical casesL27–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    cases hsource
  2. L28
    cases hsource_right
  3. L29
    cases hsource_right_right
06Establish htargetL30–31

Establish this local claim before using it. It is not an additional assumption.

  1. L30
    have htarget : FpPolyProduct(p,AB,AC,H,BB,BC,I,CB,CC,K)Definitions: FpPolyProduct
  2. L31
    exact hd
07Separate the logical casesL32–34

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L32
    cases htarget
  2. L33
    cases htarget_right
  3. L34
    cases htarget_right_right
08Establish hlengthL35–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial product length exists.

  1. L35
    have hlength : exists J. ((((H)=0 \/ (M)=0) /\ (((J)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (J)))))))
  2. L36
    specialize polynomial_product_length_exists (H)
  3. L37
    specialize polynomial_product_length_exists (M)
  4. L38
    apply polynomial_product_length_exists
09Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hlength
10Establish hmiddleL40–49

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.

  1. L40
    have hmiddle : ∃ db. ∃ dc. FpPolyProduct(p,AB,AC,H,bb,bc,M,db,dc,x)Definitions: FpPolyProduct
  2. L41
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L42
    specialize prime_field_polynomial_convolution_at_length_exists (AB)
  4. L43
    specialize prime_field_polynomial_convolution_at_length_exists (AC)
  5. L44
    specialize prime_field_polynomial_convolution_at_length_exists (H)
  6. L45
    specialize prime_field_polynomial_convolution_at_length_exists (bb)
  7. L46
    specialize prime_field_polynomial_convolution_at_length_exists (bc)
  8. L47
    specialize prime_field_polynomial_convolution_at_length_exists (M)
  9. L48
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  10. L49
    apply prime_field_polynomial_convolution_at_length_exists
11Use earlier factsL50–53

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L50
    exact hp
  2. L51
    exact htarget_left
  3. L52
    exact hsource_right_left
  4. L53
    exact hlength_witness
12Separate the logical casesL54–55

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    cases hmiddle
  2. L55
    cases hmiddle_witness
13Use earlier factsL56–65

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L56
    specialize prime_field_polynomial_equivalent_transitive (cb)
  2. L57
    specialize prime_field_polynomial_equivalent_transitive (cc)
  3. L58
    specialize prime_field_polynomial_equivalent_transitive (N)
  4. L59
    specialize prime_field_polynomial_equivalent_transitive (x1)
  5. L60
    specialize prime_field_polynomial_equivalent_transitive (x2)
  6. L61
    specialize prime_field_polynomial_equivalent_transitive (x)
  7. L62
    specialize prime_field_polynomial_equivalent_transitive (CB)
  8. L63
    specialize prime_field_polynomial_equivalent_transitive (CC)
  9. L64
    specialize prime_field_polynomial_equivalent_transitive (K)
  10. L65
    apply prime_field_polynomial_equivalent_transitive
14Use earlier factsL66–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L66
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  2. L67
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (ab)
  3. L68
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (ac)
  4. L69
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (L)
  5. L70
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (bb)
  6. L71
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (bc)
  7. L72
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (M)
  8. L73
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (cb)
  9. L74
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (cc)
  10. L75
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (N)
15Use earlier factsL76–85

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L76
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (AB)
  2. L77
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (AC)
  3. L78
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (H)
  4. L79
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  5. L80
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  6. L81
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
  7. L82
    apply prime_field_polynomial_convolution_equivalent_congruent_left
  8. L83
    exact hp
  9. L84
    exact hA
  10. L85
    exact hc
16Use earlier factsL86–95

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L86
    exact hmiddle_witness_witness
  2. L87
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)
  3. L88
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (AB)
  4. L89
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (AC)
  5. L90
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (H)
  6. L91
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb)
  7. L92
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc)
  8. L93
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (M)
  9. L94
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (x1)
  10. L95
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (x2)
17Use earlier factsL96–105

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L96
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (x)
  2. L97
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (BB)
  3. L98
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (BC)
  4. L99
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (I)
  5. L100
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (CB)
  6. L101
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (CC)
  7. L102
    specialize prime_field_polynomial_convolution_equivalent_congruent_right (K)
  8. L103
    apply prime_field_polynomial_convolution_equivalent_congruent_right
  9. L104
    exact hp
  10. L105
    exact hB
18Use earlier factsL106–107

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L106
    exact hmiddle_witness_witness
  2. L107
    exact hd

Library-wide reading audit

Original exact command ledger · 107 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro N
  11. 0011intro AB
  12. 0012intro AC
  13. 0013intro H
  14. 0014intro BB
  15. 0015intro BC
  16. 0016intro I
  17. 0017intro CB
  18. 0018intro CC
  19. 0019intro K
  20. 0020intro hp
  21. 0021intro hA
  22. 0022intro hB
  23. 0023intro hc
  24. 0024intro hd
  25. 0025have hsource : ((forall fom_index_pfp_congruent_both_originalleft. (exists fom_gap_pfp_congruent_both_originalleft_index_bound. fom_gap_pfp_congruent_both_originalleft_index_bound + S (fom_index_pfp_congruent_both_originalleft) = L) -> exists fom_value_pfp_congruent_both_originalleft. ((((exists fom_beta_height_pfp_congruent_both_originalleft_entry. fom_beta_height_pfp_congruent_both_originalleft_entry + S (fom_value_pfp_congruent_both_originalleft) = S ((S (fom_index_pfp_congruent_both_originalleft)) * ac)) /\ exists fom_beta_quotient_pfp_congruent_both_originalleft_entry. ab = fom_beta_quotient_pfp_congruent_both_originalleft_entry * S ((S (fom_index_pfp_congruent_both_originalleft)) * ac) + (fom_value_pfp_congruent_both_originalleft))) /\ (exists fom_gap_pfp_congruent_both_originalleft_value_bound. fom_gap_pfp_congruent_both_originalleft_value_bound + S (fom_value_pfp_congruent_both_originalleft) = p))) /\ (((forall fom_index_pfp_congruent_both_originalright. (exists fom_gap_pfp_congruent_both_originalright_index_bound. fom_gap_pfp_congruent_both_originalright_index_bound + S (fom_index_pfp_congruent_both_originalright) = M) -> exists fom_value_pfp_congruent_both_originalright. ((((exists fom_beta_height_pfp_congruent_both_originalright_entry. fom_beta_height_pfp_congruent_both_originalright_entry + S (fom_value_pfp_congruent_both_originalright) = S ((S (fom_index_pfp_congruent_both_originalright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_both_originalright_entry. bb = fom_beta_quotient_pfp_congruent_both_originalright_entry * S ((S (fom_index_pfp_congruent_both_originalright)) * bc) + (fom_value_pfp_congruent_both_originalright))) /\ (exists fom_gap_pfp_congruent_both_originalright_value_bound. fom_gap_pfp_congruent_both_originalright_value_bound + S (fom_value_pfp_congruent_both_originalright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_congruent_both_originalcoefficients. (exists pfa_gap_congruent_both_originalcoefficientsbound. pfa_gap_congruent_both_originalcoefficientsbound + S (pfc_index_congruent_both_originalcoefficients) = (N)) -> exists pfc_value_congruent_both_originalcoefficients. ((((exists ff_h_pfp_congruent_both_originalcoefficientsentry. ff_h_pfp_congruent_both_originalcoefficientsentry + S (pfc_value_congruent_both_originalcoefficients) = S ((S (pfc_index_congruent_both_originalcoefficients)) * cc)) /\ exists ff_q_pfp_congruent_both_originalcoefficientsentry. cb = ff_q_pfp_congruent_both_originalcoefficientsentry * S ((S (pfc_index_congruent_both_originalcoefficients)) * cc) + (pfc_value_congruent_both_originalcoefficients))) /\ ((exists pfc_terms_code_congruent_both_originalcoefficientscoefficient pfc_terms_scale_congruent_both_originalcoefficientscoefficient pfc_natural_sum_congruent_both_originalcoefficientscoefficient. ((forall pfc_index_congruent_both_originalcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonalbound. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_both_originalcoefficients))) -> exists pfc_value_congruent_both_originalcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_both_originalcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_both_originalcoefficientscoefficient = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient) + (pfc_value_congruent_both_originalcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)+pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm=(pfc_index_congruent_both_originalcoefficients)) /\ ((((((exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) * ac) + (pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_congruent_both_originalcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_both_originalcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_both_originalcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_both_originalcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_both_originalcoefficientscoefficientdiagonal)=pfc_left_congruent_both_originalcoefficientscoefficientdiagonalterm*pfc_right_congruent_both_originalcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_both_originalcoefficientscoefficientsum fs_v_pfc_congruent_both_originalcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_both_originalcoefficientscoefficient) = S ((S (S (pfc_index_congruent_both_originalcoefficients))) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_both_originalcoefficients))) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (pfc_natural_sum_congruent_both_originalcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_both_originalcoefficients)) -> exists fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_both_originalcoefficientscoefficient = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_originalcoefficientscoefficient) + (fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_both_originalcoefficientscoefficientsum = fs_q_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_originalcoefficientscoefficientsum) + (fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_both_originalcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_both_originalcoefficientscoefficientresiduebound. pfa_gap_congruent_both_originalcoefficientscoefficientresiduebound + S (pfc_value_congruent_both_originalcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_both_originalcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_both_originalcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_both_originalcoefficientscoefficient) + (p) * pfa_offset_left_congruent_both_originalcoefficientscoefficientresiduecongruence = (pfc_value_congruent_both_originalcoefficients) + (p) * pfa_offset_right_congruent_both_originalcoefficientscoefficientresiduecongruence))))))))))))))))))
  26. 0026exact hc
  27. 0027cases hsource
  28. 0028cases hsource_right
  29. 0029cases hsource_right_right
  30. 0030have htarget : ((forall fom_index_pfp_congruent_both_otherleft. (exists fom_gap_pfp_congruent_both_otherleft_index_bound. fom_gap_pfp_congruent_both_otherleft_index_bound + S (fom_index_pfp_congruent_both_otherleft) = H) -> exists fom_value_pfp_congruent_both_otherleft. ((((exists fom_beta_height_pfp_congruent_both_otherleft_entry. fom_beta_height_pfp_congruent_both_otherleft_entry + S (fom_value_pfp_congruent_both_otherleft) = S ((S (fom_index_pfp_congruent_both_otherleft)) * AC)) /\ exists fom_beta_quotient_pfp_congruent_both_otherleft_entry. AB = fom_beta_quotient_pfp_congruent_both_otherleft_entry * S ((S (fom_index_pfp_congruent_both_otherleft)) * AC) + (fom_value_pfp_congruent_both_otherleft))) /\ (exists fom_gap_pfp_congruent_both_otherleft_value_bound. fom_gap_pfp_congruent_both_otherleft_value_bound + S (fom_value_pfp_congruent_both_otherleft) = p))) /\ (((forall fom_index_pfp_congruent_both_otherright. (exists fom_gap_pfp_congruent_both_otherright_index_bound. fom_gap_pfp_congruent_both_otherright_index_bound + S (fom_index_pfp_congruent_both_otherright) = I) -> exists fom_value_pfp_congruent_both_otherright. ((((exists fom_beta_height_pfp_congruent_both_otherright_entry. fom_beta_height_pfp_congruent_both_otherright_entry + S (fom_value_pfp_congruent_both_otherright) = S ((S (fom_index_pfp_congruent_both_otherright)) * BC)) /\ exists fom_beta_quotient_pfp_congruent_both_otherright_entry. BB = fom_beta_quotient_pfp_congruent_both_otherright_entry * S ((S (fom_index_pfp_congruent_both_otherright)) * BC) + (fom_value_pfp_congruent_both_otherright))) /\ (exists fom_gap_pfp_congruent_both_otherright_value_bound. fom_gap_pfp_congruent_both_otherright_value_bound + S (fom_value_pfp_congruent_both_otherright) = p))) /\ (((((((H)=0 \/ (I)=0) /\ (((K)=0)))) \/ (((~((H)=0)) /\ (((~((I)=0)) /\ (((H)+(I)=S (K)))))))) /\ ((forall pfc_index_congruent_both_othercoefficients. (exists pfa_gap_congruent_both_othercoefficientsbound. pfa_gap_congruent_both_othercoefficientsbound + S (pfc_index_congruent_both_othercoefficients) = (K)) -> exists pfc_value_congruent_both_othercoefficients. ((((exists ff_h_pfp_congruent_both_othercoefficientsentry. ff_h_pfp_congruent_both_othercoefficientsentry + S (pfc_value_congruent_both_othercoefficients) = S ((S (pfc_index_congruent_both_othercoefficients)) * CC)) /\ exists ff_q_pfp_congruent_both_othercoefficientsentry. CB = ff_q_pfp_congruent_both_othercoefficientsentry * S ((S (pfc_index_congruent_both_othercoefficients)) * CC) + (pfc_value_congruent_both_othercoefficients))) /\ ((exists pfc_terms_code_congruent_both_othercoefficientscoefficient pfc_terms_scale_congruent_both_othercoefficientscoefficient pfc_natural_sum_congruent_both_othercoefficientscoefficient. ((forall pfc_index_congruent_both_othercoefficientscoefficientdiagonal. (exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonalbound. pfa_gap_congruent_both_othercoefficientscoefficientdiagonalbound + S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal) = (S (pfc_index_congruent_both_othercoefficients))) -> exists pfc_value_congruent_both_othercoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonalentry + S (pfc_value_congruent_both_othercoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_both_othercoefficientscoefficient = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient) + (pfc_value_congruent_both_othercoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm. (((pfc_index_congruent_both_othercoefficientscoefficientdiagonal)+pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm=(pfc_index_congruent_both_othercoefficients)) /\ ((((((exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) * AC) + (pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_congruent_both_othercoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm) = (I)) /\ ((((exists ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_congruent_both_othercoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_both_othercoefficientscoefficientdiagonaltermrightoutside+(I)=(pfc_complement_congruent_both_othercoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_both_othercoefficientscoefficientdiagonal)=pfc_left_congruent_both_othercoefficientscoefficientdiagonalterm*pfc_right_congruent_both_othercoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_both_othercoefficientscoefficientsum fs_v_pfc_congruent_both_othercoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_start. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_start. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_both_othercoefficientscoefficient) = S ((S (S (pfc_index_congruent_both_othercoefficients))) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_both_othercoefficients))) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (pfc_natural_sum_congruent_both_othercoefficientscoefficient))) /\ forall fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps = S (pfc_index_congruent_both_othercoefficients)) -> exists fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_both_othercoefficientscoefficient = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_both_othercoefficientscoefficient) + (fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_both_othercoefficientscoefficientsum = fs_q_pfc_congruent_both_othercoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_both_othercoefficientscoefficientsum) + (fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_both_othercoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_both_othercoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_both_othercoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_both_othercoefficientscoefficientresiduebound. pfa_gap_congruent_both_othercoefficientscoefficientresiduebound + S (pfc_value_congruent_both_othercoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_both_othercoefficientscoefficientresiduecongruence pfa_offset_right_congruent_both_othercoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_both_othercoefficientscoefficient) + (p) * pfa_offset_left_congruent_both_othercoefficientscoefficientresiduecongruence = (pfc_value_congruent_both_othercoefficients) + (p) * pfa_offset_right_congruent_both_othercoefficientscoefficientresiduecongruence))))))))))))))))))
  31. 0031exact hd
  32. 0032cases htarget
  33. 0033cases htarget_right
  34. 0034cases htarget_right_right
  35. 0035have hlength : exists J. ((((H)=0 \/ (M)=0) /\ (((J)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (J)))))))
  36. 0036specialize polynomial_product_length_exists (H)
  37. 0037specialize polynomial_product_length_exists (M)
  38. 0038apply polynomial_product_length_exists
  39. 0039cases hlength
  40. 0040have hmiddle : exists db dc. ((forall fom_index_pfp_congruent_middle_productleft. (exists fom_gap_pfp_congruent_middle_productleft_index_bound. fom_gap_pfp_congruent_middle_productleft_index_bound + S (fom_index_pfp_congruent_middle_productleft) = H) -> exists fom_value_pfp_congruent_middle_productleft. ((((exists fom_beta_height_pfp_congruent_middle_productleft_entry. fom_beta_height_pfp_congruent_middle_productleft_entry + S (fom_value_pfp_congruent_middle_productleft) = S ((S (fom_index_pfp_congruent_middle_productleft)) * AC)) /\ exists fom_beta_quotient_pfp_congruent_middle_productleft_entry. AB = fom_beta_quotient_pfp_congruent_middle_productleft_entry * S ((S (fom_index_pfp_congruent_middle_productleft)) * AC) + (fom_value_pfp_congruent_middle_productleft))) /\ (exists fom_gap_pfp_congruent_middle_productleft_value_bound. fom_gap_pfp_congruent_middle_productleft_value_bound + S (fom_value_pfp_congruent_middle_productleft) = p))) /\ (((forall fom_index_pfp_congruent_middle_productright. (exists fom_gap_pfp_congruent_middle_productright_index_bound. fom_gap_pfp_congruent_middle_productright_index_bound + S (fom_index_pfp_congruent_middle_productright) = M) -> exists fom_value_pfp_congruent_middle_productright. ((((exists fom_beta_height_pfp_congruent_middle_productright_entry. fom_beta_height_pfp_congruent_middle_productright_entry + S (fom_value_pfp_congruent_middle_productright) = S ((S (fom_index_pfp_congruent_middle_productright)) * bc)) /\ exists fom_beta_quotient_pfp_congruent_middle_productright_entry. bb = fom_beta_quotient_pfp_congruent_middle_productright_entry * S ((S (fom_index_pfp_congruent_middle_productright)) * bc) + (fom_value_pfp_congruent_middle_productright))) /\ (exists fom_gap_pfp_congruent_middle_productright_value_bound. fom_gap_pfp_congruent_middle_productright_value_bound + S (fom_value_pfp_congruent_middle_productright) = p))) /\ (((((((H)=0 \/ (M)=0) /\ (((x)=0)))) \/ (((~((H)=0)) /\ (((~((M)=0)) /\ (((H)+(M)=S (x)))))))) /\ ((forall pfc_index_congruent_middle_productcoefficients. (exists pfa_gap_congruent_middle_productcoefficientsbound. pfa_gap_congruent_middle_productcoefficientsbound + S (pfc_index_congruent_middle_productcoefficients) = (x)) -> exists pfc_value_congruent_middle_productcoefficients. ((((exists ff_h_pfp_congruent_middle_productcoefficientsentry. ff_h_pfp_congruent_middle_productcoefficientsentry + S (pfc_value_congruent_middle_productcoefficients) = S ((S (pfc_index_congruent_middle_productcoefficients)) * dc)) /\ exists ff_q_pfp_congruent_middle_productcoefficientsentry. db = ff_q_pfp_congruent_middle_productcoefficientsentry * S ((S (pfc_index_congruent_middle_productcoefficients)) * dc) + (pfc_value_congruent_middle_productcoefficients))) /\ ((exists pfc_terms_code_congruent_middle_productcoefficientscoefficient pfc_terms_scale_congruent_middle_productcoefficientscoefficient pfc_natural_sum_congruent_middle_productcoefficientscoefficient. ((forall pfc_index_congruent_middle_productcoefficientscoefficientdiagonal. (exists pfa_gap_congruent_middle_productcoefficientscoefficientdiagonalbound. pfa_gap_congruent_middle_productcoefficientscoefficientdiagonalbound + S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal) = (S (pfc_index_congruent_middle_productcoefficients))) -> exists pfc_value_congruent_middle_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonalentry. ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonalentry + S (pfc_value_congruent_middle_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_middle_productcoefficientscoefficient)) /\ exists ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonalentry. pfc_terms_code_congruent_middle_productcoefficientscoefficient = ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_congruent_middle_productcoefficientscoefficient) + (pfc_value_congruent_middle_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm pfc_left_congruent_middle_productcoefficientscoefficientdiagonalterm pfc_right_congruent_middle_productcoefficientscoefficientdiagonalterm. (((pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)+pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm=(pfc_index_congruent_middle_productcoefficients)) /\ ((((((exists pfa_gap_congruent_middle_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_congruent_middle_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal) = (H)) /\ ((((exists ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_congruent_middle_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)) * AC) + (pfc_left_congruent_middle_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_middle_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_congruent_middle_productcoefficientscoefficientdiagonaltermleftoutside+(H)=(pfc_index_congruent_middle_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_congruent_middle_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_congruent_middle_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_congruent_middle_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_congruent_middle_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_congruent_middle_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_congruent_middle_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_congruent_middle_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_congruent_middle_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_congruent_middle_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_congruent_middle_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_congruent_middle_productcoefficientscoefficientdiagonal)=pfc_left_congruent_middle_productcoefficientscoefficientdiagonalterm*pfc_right_congruent_middle_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_congruent_middle_productcoefficientscoefficientsum fs_v_pfc_congruent_middle_productcoefficientscoefficientsum. ((((exists fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_start. fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_start. fs_u_pfc_congruent_middle_productcoefficientscoefficientsum = fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_congruent_middle_productcoefficientscoefficient) = S ((S (S (pfc_index_congruent_middle_productcoefficients))) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_congruent_middle_productcoefficientscoefficientsum = fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_congruent_middle_productcoefficients))) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum) + (pfc_natural_sum_congruent_middle_productcoefficientscoefficient))) /\ forall fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps = S (pfc_index_congruent_middle_productcoefficients)) -> exists fs_a_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps fs_r_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps fs_s_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_middle_productcoefficientscoefficient)) /\ exists fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_congruent_middle_productcoefficientscoefficient = fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_congruent_middle_productcoefficientscoefficient) + (fs_a_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_congruent_middle_productcoefficientscoefficientsum = fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum) + (fs_r_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_congruent_middle_productcoefficientscoefficientsum = fs_q_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_congruent_middle_productcoefficientscoefficientsum) + (fs_s_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps = fs_r_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps + fs_a_pfc_congruent_middle_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_congruent_middle_productcoefficientscoefficientresiduebound. pfa_gap_congruent_middle_productcoefficientscoefficientresiduebound + S (pfc_value_congruent_middle_productcoefficients) = (p)) /\ ((exists pfa_offset_left_congruent_middle_productcoefficientscoefficientresiduecongruence pfa_offset_right_congruent_middle_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_congruent_middle_productcoefficientscoefficient) + (p) * pfa_offset_left_congruent_middle_productcoefficientscoefficientresiduecongruence = (pfc_value_congruent_middle_productcoefficients) + (p) * pfa_offset_right_congruent_middle_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  41. 0041specialize prime_field_polynomial_convolution_at_length_exists (p)
  42. 0042specialize prime_field_polynomial_convolution_at_length_exists (AB)
  43. 0043specialize prime_field_polynomial_convolution_at_length_exists (AC)
  44. 0044specialize prime_field_polynomial_convolution_at_length_exists (H)
  45. 0045specialize prime_field_polynomial_convolution_at_length_exists (bb)
  46. 0046specialize prime_field_polynomial_convolution_at_length_exists (bc)
  47. 0047specialize prime_field_polynomial_convolution_at_length_exists (M)
  48. 0048specialize prime_field_polynomial_convolution_at_length_exists (x)
  49. 0049apply prime_field_polynomial_convolution_at_length_exists
  50. 0050exact hp
  51. 0051exact htarget_left
  52. 0052exact hsource_right_left
  53. 0053exact hlength_witness
  54. 0054cases hmiddle
  55. 0055cases hmiddle_witness
  56. 0056specialize prime_field_polynomial_equivalent_transitive (cb)
  57. 0057specialize prime_field_polynomial_equivalent_transitive (cc)
  58. 0058specialize prime_field_polynomial_equivalent_transitive (N)
  59. 0059specialize prime_field_polynomial_equivalent_transitive (x1)
  60. 0060specialize prime_field_polynomial_equivalent_transitive (x2)
  61. 0061specialize prime_field_polynomial_equivalent_transitive (x)
  62. 0062specialize prime_field_polynomial_equivalent_transitive (CB)
  63. 0063specialize prime_field_polynomial_equivalent_transitive (CC)
  64. 0064specialize prime_field_polynomial_equivalent_transitive (K)
  65. 0065apply prime_field_polynomial_equivalent_transitive
  66. 0066specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  67. 0067specialize prime_field_polynomial_convolution_equivalent_congruent_left (ab)
  68. 0068specialize prime_field_polynomial_convolution_equivalent_congruent_left (ac)
  69. 0069specialize prime_field_polynomial_convolution_equivalent_congruent_left (L)
  70. 0070specialize prime_field_polynomial_convolution_equivalent_congruent_left (bb)
  71. 0071specialize prime_field_polynomial_convolution_equivalent_congruent_left (bc)
  72. 0072specialize prime_field_polynomial_convolution_equivalent_congruent_left (M)
  73. 0073specialize prime_field_polynomial_convolution_equivalent_congruent_left (cb)
  74. 0074specialize prime_field_polynomial_convolution_equivalent_congruent_left (cc)
  75. 0075specialize prime_field_polynomial_convolution_equivalent_congruent_left (N)
  76. 0076specialize prime_field_polynomial_convolution_equivalent_congruent_left (AB)
  77. 0077specialize prime_field_polynomial_convolution_equivalent_congruent_left (AC)
  78. 0078specialize prime_field_polynomial_convolution_equivalent_congruent_left (H)
  79. 0079specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  80. 0080specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  81. 0081specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
  82. 0082apply prime_field_polynomial_convolution_equivalent_congruent_left
  83. 0083exact hp
  84. 0084exact hA
  85. 0085exact hc
  86. 0086exact hmiddle_witness_witness
  87. 0087specialize prime_field_polynomial_convolution_equivalent_congruent_right (p)
  88. 0088specialize prime_field_polynomial_convolution_equivalent_congruent_right (AB)
  89. 0089specialize prime_field_polynomial_convolution_equivalent_congruent_right (AC)
  90. 0090specialize prime_field_polynomial_convolution_equivalent_congruent_right (H)
  91. 0091specialize prime_field_polynomial_convolution_equivalent_congruent_right (bb)
  92. 0092specialize prime_field_polynomial_convolution_equivalent_congruent_right (bc)
  93. 0093specialize prime_field_polynomial_convolution_equivalent_congruent_right (M)
  94. 0094specialize prime_field_polynomial_convolution_equivalent_congruent_right (x1)
  95. 0095specialize prime_field_polynomial_convolution_equivalent_congruent_right (x2)
  96. 0096specialize prime_field_polynomial_convolution_equivalent_congruent_right (x)
  97. 0097specialize prime_field_polynomial_convolution_equivalent_congruent_right (BB)
  98. 0098specialize prime_field_polynomial_convolution_equivalent_congruent_right (BC)
  99. 0099specialize prime_field_polynomial_convolution_equivalent_congruent_right (I)
  100. 0100specialize prime_field_polynomial_convolution_equivalent_congruent_right (CB)
  101. 0101specialize prime_field_polynomial_convolution_equivalent_congruent_right (CC)
  102. 0102specialize prime_field_polynomial_convolution_equivalent_congruent_right (K)
  103. 0103apply prime_field_polynomial_convolution_equivalent_congruent_right
  104. 0104exact hp
  105. 0105exact hB
  106. 0106exact hmiddle_witness_witness
  107. 0107exact hd