PG0017

prime_field_polynomial_convolution_right_scale_exists

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

At any nonzero modulus and canonical scalar, construct the actual scaled input, its actual convolution, and an independently encoded scalar output, then derive their exact decoded-prefix agreement.

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 k ab ac L bb bc M cb cc N. (~(p=0)) -> (exists pfa_gap_scalar_exists_scalar. pfa_gap_scalar_exists_scalar + S (k) = (p)) -> (((forall fom_index_pfp_scalar_exists_originalleft. (exists fom_gap_pfp_scalar_exists_originalleft_index_bound. fom_gap_pfp_scalar_exists_originalleft_index_bound + S (fom_index_pfp_scalar_exists_originalleft) = L) -> exists fom_value_pfp_scalar_exists_originalleft. ((((exists fom_beta_height_pfp_scalar_exists_originalleft_entry. fom_beta_height_pfp_scalar_exists_originalleft_entry + S (fom_value_pfp_scalar_exists_originalleft) = S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_originalleft_entry * S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac) + (fom_value_pfp_scalar_exists_originalleft))) /\ (exists fom_gap_pfp_scalar_exists_originalleft_value_bound. fom_gap_pfp_scalar_exists_originalleft_value_bound + S (fom_value_pfp_scalar_exists_originalleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_originalright. (exists fom_gap_pfp_scalar_exists_originalright_index_bound. fom_gap_pfp_scalar_exists_originalright_index_bound + S (fom_index_pfp_scalar_exists_originalright) = M) -> exists fom_value_pfp_scalar_exists_originalright. ((((exists fom_beta_height_pfp_scalar_exists_originalright_entry. fom_beta_height_pfp_scalar_exists_originalright_entry + S (fom_value_pfp_scalar_exists_originalright) = S ((S (fom_index_pfp_scalar_exists_originalright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalright_entry. bb = fom_beta_quotient_pfp_scalar_exists_originalright_entry * S ((S (fom_index_pfp_scalar_exists_originalright)) * bc) + (fom_value_pfp_scalar_exists_originalright))) /\ (exists fom_gap_pfp_scalar_exists_originalright_value_bound. fom_gap_pfp_scalar_exists_originalright_value_bound + S (fom_value_pfp_scalar_exists_originalright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_originalcoefficients. (exists pfa_gap_scalar_exists_originalcoefficientsbound. pfa_gap_scalar_exists_originalcoefficientsbound + S (pfc_index_scalar_exists_originalcoefficients) = (N)) -> exists pfc_value_scalar_exists_originalcoefficients. ((((exists ff_h_pfp_scalar_exists_originalcoefficientsentry. ff_h_pfp_scalar_exists_originalcoefficientsentry + S (pfc_value_scalar_exists_originalcoefficients) = S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientsentry. cb = ff_q_pfp_scalar_exists_originalcoefficientsentry * S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc) + (pfc_value_scalar_exists_originalcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_originalcoefficientscoefficient pfc_terms_scale_scalar_exists_originalcoefficientscoefficient pfc_natural_sum_scalar_exists_originalcoefficientscoefficient. ((forall pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_originalcoefficients))) -> exists pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_originalcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_originalcoefficients)) -> exists fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_originalcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_originalcoefficients) + (p) * pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (exists sb sc db dc eb ec. ((((exists pfa_gap_scalar_exists_inputscalar. pfa_gap_scalar_exists_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_input. (exists pfa_gap_scalar_exists_inputindex. pfa_gap_scalar_exists_inputindex + S (pfp_index_scalar_exists_input) = (M)) -> exists pfp_source_scalar_exists_input pfp_value_scalar_exists_input. ((((exists ff_h_pfp_scalar_exists_inputsource. ff_h_pfp_scalar_exists_inputsource + S (pfp_source_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * bc)) /\ exists ff_q_pfp_scalar_exists_inputsource. bb = ff_q_pfp_scalar_exists_inputsource * S ((S (pfp_index_scalar_exists_input)) * bc) + (pfp_source_scalar_exists_input))) /\ (((((exists ff_h_pfp_scalar_exists_inputtarget. ff_h_pfp_scalar_exists_inputtarget + S (pfp_value_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * sc)) /\ exists ff_q_pfp_scalar_exists_inputtarget. sb = ff_q_pfp_scalar_exists_inputtarget * S ((S (pfp_index_scalar_exists_input)) * sc) + (pfp_value_scalar_exists_input))) /\ ((((exists pfa_gap_scalar_exists_inputoperationleft. pfa_gap_scalar_exists_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_inputoperationright. pfa_gap_scalar_exists_inputoperationright + S (pfp_source_scalar_exists_input) = (p)) /\ ((((exists pfa_gap_scalar_exists_inputoperationresultbound. pfa_gap_scalar_exists_inputoperationresultbound + S (pfp_value_scalar_exists_input) = (p)) /\ ((exists pfa_offset_left_scalar_exists_inputoperationresultcongruence pfa_offset_right_scalar_exists_inputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_input)) + (p) * pfa_offset_left_scalar_exists_inputoperationresultcongruence = (pfp_value_scalar_exists_input) + (p) * pfa_offset_right_scalar_exists_inputoperationresultcongruence))))))))))))))))) /\ (((((forall fom_index_pfp_scalar_exists_newleft. (exists fom_gap_pfp_scalar_exists_newleft_index_bound. fom_gap_pfp_scalar_exists_newleft_index_bound + S (fom_index_pfp_scalar_exists_newleft) = L) -> exists fom_value_pfp_scalar_exists_newleft. ((((exists fom_beta_height_pfp_scalar_exists_newleft_entry. fom_beta_height_pfp_scalar_exists_newleft_entry + S (fom_value_pfp_scalar_exists_newleft) = S ((S (fom_index_pfp_scalar_exists_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_newleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_newleft_entry * S ((S (fom_index_pfp_scalar_exists_newleft)) * ac) + (fom_value_pfp_scalar_exists_newleft))) /\ (exists fom_gap_pfp_scalar_exists_newleft_value_bound. fom_gap_pfp_scalar_exists_newleft_value_bound + S (fom_value_pfp_scalar_exists_newleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_newright. (exists fom_gap_pfp_scalar_exists_newright_index_bound. fom_gap_pfp_scalar_exists_newright_index_bound + S (fom_index_pfp_scalar_exists_newright) = M) -> exists fom_value_pfp_scalar_exists_newright. ((((exists fom_beta_height_pfp_scalar_exists_newright_entry. fom_beta_height_pfp_scalar_exists_newright_entry + S (fom_value_pfp_scalar_exists_newright) = S ((S (fom_index_pfp_scalar_exists_newright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_exists_newright_entry. sb = fom_beta_quotient_pfp_scalar_exists_newright_entry * S ((S (fom_index_pfp_scalar_exists_newright)) * sc) + (fom_value_pfp_scalar_exists_newright))) /\ (exists fom_gap_pfp_scalar_exists_newright_value_bound. fom_gap_pfp_scalar_exists_newright_value_bound + S (fom_value_pfp_scalar_exists_newright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_newcoefficients. (exists pfa_gap_scalar_exists_newcoefficientsbound. pfa_gap_scalar_exists_newcoefficientsbound + S (pfc_index_scalar_exists_newcoefficients) = (N)) -> exists pfc_value_scalar_exists_newcoefficients. ((((exists ff_h_pfp_scalar_exists_newcoefficientsentry. ff_h_pfp_scalar_exists_newcoefficientsentry + S (pfc_value_scalar_exists_newcoefficients) = S ((S (pfc_index_scalar_exists_newcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_exists_newcoefficientsentry. db = ff_q_pfp_scalar_exists_newcoefficientsentry * S ((S (pfc_index_scalar_exists_newcoefficients)) * dc) + (pfc_value_scalar_exists_newcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_newcoefficientscoefficient pfc_terms_scale_scalar_exists_newcoefficientscoefficient pfc_natural_sum_scalar_exists_newcoefficientscoefficient. ((forall pfc_index_scalar_exists_newcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_newcoefficients))) -> exists pfc_value_scalar_exists_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_newcoefficientscoefficient = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient) + (pfc_value_scalar_exists_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_newcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_exists_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_newcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_newcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_newcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_newcoefficientscoefficientsum fs_v_pfc_scalar_exists_newcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_newcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_newcoefficients))) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_newcoefficients))) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_newcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_newcoefficients)) -> exists fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_newcoefficientscoefficient = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_newcoefficientscoefficient) + (fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_newcoefficientscoefficientsum = fs_q_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_newcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_newcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_newcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_newcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_newcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_newcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_newcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_newcoefficients) + (p) * pfa_offset_right_scalar_exists_newcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((exists pfa_gap_scalar_exists_outputscalar. pfa_gap_scalar_exists_outputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_output. (exists pfa_gap_scalar_exists_outputindex. pfa_gap_scalar_exists_outputindex + S (pfp_index_scalar_exists_output) = (N)) -> exists pfp_source_scalar_exists_output pfp_value_scalar_exists_output. ((((exists ff_h_pfp_scalar_exists_outputsource. ff_h_pfp_scalar_exists_outputsource + S (pfp_source_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * cc)) /\ exists ff_q_pfp_scalar_exists_outputsource. cb = ff_q_pfp_scalar_exists_outputsource * S ((S (pfp_index_scalar_exists_output)) * cc) + (pfp_source_scalar_exists_output))) /\ (((((exists ff_h_pfp_scalar_exists_outputtarget. ff_h_pfp_scalar_exists_outputtarget + S (pfp_value_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * ec)) /\ exists ff_q_pfp_scalar_exists_outputtarget. eb = ff_q_pfp_scalar_exists_outputtarget * S ((S (pfp_index_scalar_exists_output)) * ec) + (pfp_value_scalar_exists_output))) /\ ((((exists pfa_gap_scalar_exists_outputoperationleft. pfa_gap_scalar_exists_outputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_outputoperationright. pfa_gap_scalar_exists_outputoperationright + S (pfp_source_scalar_exists_output) = (p)) /\ ((((exists pfa_gap_scalar_exists_outputoperationresultbound. pfa_gap_scalar_exists_outputoperationresultbound + S (pfp_value_scalar_exists_output) = (p)) /\ ((exists pfa_offset_left_scalar_exists_outputoperationresultcongruence pfa_offset_right_scalar_exists_outputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_output)) + (p) * pfa_offset_left_scalar_exists_outputoperationresultcongruence = (pfp_value_scalar_exists_output) + (p) * pfa_offset_right_scalar_exists_outputoperationresultcongruence))))))))))))))))) /\ ((forall mdr_i_pfp_scalar_exists_equal mdr_a_pfp_scalar_exists_equal. (exists mdr_gap_pfp_scalar_exists_equalb. mdr_gap_pfp_scalar_exists_equalb + S (mdr_i_pfp_scalar_exists_equal) = (N)) -> (((exists ff_h_mdr_pfp_scalar_exists_equalo. ff_h_mdr_pfp_scalar_exists_equalo + S (mdr_a_pfp_scalar_exists_equal) = S ((S (mdr_i_pfp_scalar_exists_equal)) * dc)) /\ exists ff_q_mdr_pfp_scalar_exists_equalo. db = ff_q_mdr_pfp_scalar_exists_equalo * S ((S (mdr_i_pfp_scalar_exists_equal)) * dc) + (mdr_a_pfp_scalar_exists_equal))) -> (((exists ff_h_mdr_pfp_scalar_exists_equaln. ff_h_mdr_pfp_scalar_exists_equaln + S (mdr_a_pfp_scalar_exists_equal) = S ((S (mdr_i_pfp_scalar_exists_equal)) * ec)) /\ exists ff_q_mdr_pfp_scalar_exists_equaln. eb = ff_q_mdr_pfp_scalar_exists_equaln * S ((S (mdr_i_pfp_scalar_exists_equal)) * ec) + (mdr_a_pfp_scalar_exists_equal)))))))))))

Constructive proof overview

Generated structural guide

At any nonzero modulus and canonical scalar, construct the actual scaled input, its actual convolution, and an independently encoded scalar output, then derive their exact decoded-prefix agreement.

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

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_scale_exists Alpha theorem; checked-use authorized prime_field_polynomial_scale_bounded Alpha theorem; checked-use authorized prime_field_polynomial_convolution_at_length_exists Alpha theorem; checked-use authorized prime_field_polynomial_convolution_bounded Alpha theorem; checked-use authorized PG0016 prime_field_polynomial_convolution_right_scale_equal

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

119 script commands · 27 reading checkpoints · 6 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 (1)
prime field polynomial convolution right scale equal

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 k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro L
  6. L6
    intro bb
  7. L7
    intro bc
  8. L8
    intro M
  9. L9
    intro cb
  10. L10
    intro cc
02Fix variables and assumptionsL11–14

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

  1. L11
    intro N
  2. L12
    intro hp
  3. L13
    intro hk
  4. L14
    intro hc
03Establish hcopyL15–16

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

  1. L15
    have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Definitions: FpPolyProduct
  2. L16
    exact hc
04Separate the logical casesL17–19

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

  1. L17
    cases hcopy
  2. L18
    cases hcopy_right
  3. L19
    cases hcopy_right_right
05Establish hsL20–29

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

  1. L20
    have hs : ∃ sb. ∃ sc. FpPolyScale(p,k,bb,bc,sb,sc,M)Definitions: FpPolyScale
  2. L21
    specialize prime_field_polynomial_scale_exists (p)
  3. L22
    specialize prime_field_polynomial_scale_exists (k)
  4. L23
    specialize prime_field_polynomial_scale_exists (bb)
  5. L24
    specialize prime_field_polynomial_scale_exists (bc)
  6. L25
    specialize prime_field_polynomial_scale_exists (M)
  7. L26
    apply prime_field_polynomial_scale_exists
  8. L27
    exact hp
  9. L28
    exact hk
  10. L29
    exact hcopy_right_left
06Separate the logical casesL30–31

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

  1. L30
    cases hs
  2. L31
    cases hs_witness
07Establish hbL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial scale bounded.

  1. L32
    have hb : BetaPrefixInto(bb,bc,M,p) ∧ BetaPrefixInto(x,x1,M,p)Definitions: BetaPrefixInto
  2. L33
    specialize prime_field_polynomial_scale_bounded (p)
  3. L34
    specialize prime_field_polynomial_scale_bounded (k)
  4. L35
    specialize prime_field_polynomial_scale_bounded (bb)
  5. L36
    specialize prime_field_polynomial_scale_bounded (bc)
  6. L37
    specialize prime_field_polynomial_scale_bounded (x)
  7. L38
    specialize prime_field_polynomial_scale_bounded (x1)
  8. L39
    specialize prime_field_polynomial_scale_bounded (M)
  9. L40
    apply prime_field_polynomial_scale_bounded
  10. L41
    exact hs_witness_witness
08Separate the logical casesL42–42

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

  1. L42
    cases hb
09Establish hdL43–52

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. L43
    have hd : ∃ d. ∃ e. FpPolyProduct(p,ab,ac,L,x,x1,M,d,e,N)Definitions: FpPolyProduct
  2. L44
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L45
    specialize prime_field_polynomial_convolution_at_length_exists (ab)
  4. L46
    specialize prime_field_polynomial_convolution_at_length_exists (ac)
  5. L47
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  6. L48
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  7. L49
    specialize prime_field_polynomial_convolution_at_length_exists (x1)
  8. L50
    specialize prime_field_polynomial_convolution_at_length_exists (M)
  9. L51
    specialize prime_field_polynomial_convolution_at_length_exists (N)
  10. L52
    apply prime_field_polynomial_convolution_at_length_exists
10Use earlier factsL53–56

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

  1. L53
    exact hp
  2. L54
    exact hcopy_left
  3. L55
    exact hb_right
  4. L56
    exact hcopy_right_right_left
11Separate the logical casesL57–58

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

  1. L57
    cases hd
  2. L58
    cases hd_witness
12Establish heL59–68

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

  1. L59
    have he : ∃ eb. ∃ ec. FpPolyScale(p,k,cb,cc,eb,ec,N)Definitions: FpPolyScale
  2. L60
    specialize prime_field_polynomial_scale_exists (p)
  3. L61
    specialize prime_field_polynomial_scale_exists (k)
  4. L62
    specialize prime_field_polynomial_scale_exists (cb)
  5. L63
    specialize prime_field_polynomial_scale_exists (cc)
  6. L64
    specialize prime_field_polynomial_scale_exists (N)
  7. L65
    apply prime_field_polynomial_scale_exists
  8. L66
    exact hp
  9. L67
    exact hk
  10. L68
    specialize prime_field_polynomial_convolution_bounded (p)
13Use earlier factsL69–78

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

  1. L69
    specialize prime_field_polynomial_convolution_bounded (ab)
  2. L70
    specialize prime_field_polynomial_convolution_bounded (ac)
  3. L71
    specialize prime_field_polynomial_convolution_bounded (L)
  4. L72
    specialize prime_field_polynomial_convolution_bounded (bb)
  5. L73
    specialize prime_field_polynomial_convolution_bounded (bc)
  6. L74
    specialize prime_field_polynomial_convolution_bounded (M)
  7. L75
    specialize prime_field_polynomial_convolution_bounded (cb)
  8. L76
    specialize prime_field_polynomial_convolution_bounded (cc)
  9. L77
    specialize prime_field_polynomial_convolution_bounded (N)
  10. L78
    apply prime_field_polynomial_convolution_bounded
14Use earlier factsL79–79

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

  1. L79
    exact hc
15Separate the logical casesL80–81

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

  1. L80
    cases he
  2. L81
    cases he_witness
16Construct an explicit witnessL82–87

Supply the displayed value, then prove that it has the required property.

  1. L82
    exists x
  2. L83
    exists x1
  3. L84
    exists x2
  4. L85
    exists x3
  5. L86
    exists x4
  6. L87
    exists x5
17Separate the logical casesL88–88

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

  1. L88
    split
18Use earlier factsL89–89

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

  1. L89
    exact hs_witness_witness
19Separate the logical casesL90–90

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

  1. L90
    split
20Use earlier factsL91–91

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

  1. L91
    exact hd_witness_witness
21Separate the logical casesL92–92

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

  1. L92
    split
22Use earlier factsL93–93

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

  1. L93
    exact he_witness_witness
23Establish hdataL94–103

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

  1. L94
    have hdata : N = N ∧ BetaPrefixEqual(x2,x3,x4,x5,N)Definitions: BetaPrefixEqual
  2. L95
    specialize prime_field_polynomial_convolution_right_scale_equal (p)
  3. L96
    specialize prime_field_polynomial_convolution_right_scale_equal (k)
  4. L97
    specialize prime_field_polynomial_convolution_right_scale_equal (ab)
  5. L98
    specialize prime_field_polynomial_convolution_right_scale_equal (ac)
  6. L99
    specialize prime_field_polynomial_convolution_right_scale_equal (L)
  7. L100
    specialize prime_field_polynomial_convolution_right_scale_equal (bb)
  8. L101
    specialize prime_field_polynomial_convolution_right_scale_equal (bc)
  9. L102
    specialize prime_field_polynomial_convolution_right_scale_equal (M)
  10. L103
    specialize prime_field_polynomial_convolution_right_scale_equal (x)
24Use earlier factsL104–113

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

  1. L104
    specialize prime_field_polynomial_convolution_right_scale_equal (x1)
  2. L105
    specialize prime_field_polynomial_convolution_right_scale_equal (cb)
  3. L106
    specialize prime_field_polynomial_convolution_right_scale_equal (cc)
  4. L107
    specialize prime_field_polynomial_convolution_right_scale_equal (N)
  5. L108
    specialize prime_field_polynomial_convolution_right_scale_equal (x2)
  6. L109
    specialize prime_field_polynomial_convolution_right_scale_equal (x3)
  7. L110
    specialize prime_field_polynomial_convolution_right_scale_equal (N)
  8. L111
    specialize prime_field_polynomial_convolution_right_scale_equal (x4)
  9. L112
    specialize prime_field_polynomial_convolution_right_scale_equal (x5)
  10. L113
    apply prime_field_polynomial_convolution_right_scale_equal
25Use earlier factsL114–117

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

  1. L114
    exact hs_witness_witness
  2. L115
    exact hc
  3. L116
    exact hd_witness_witness
  4. L117
    exact he_witness_witness
26Separate the logical casesL118–118

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

  1. L118
    cases hdata
27Use earlier factsL119–119

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

  1. L119
    exact hdata_right

Library-wide reading audit

Original exact command ledger · 119 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro L
  6. 0006intro bb
  7. 0007intro bc
  8. 0008intro M
  9. 0009intro cb
  10. 0010intro cc
  11. 0011intro N
  12. 0012intro hp
  13. 0013intro hk
  14. 0014intro hc
  15. 0015have hcopy : ((forall fom_index_pfp_scalar_exists_originalleft. (exists fom_gap_pfp_scalar_exists_originalleft_index_bound. fom_gap_pfp_scalar_exists_originalleft_index_bound + S (fom_index_pfp_scalar_exists_originalleft) = L) -> exists fom_value_pfp_scalar_exists_originalleft. ((((exists fom_beta_height_pfp_scalar_exists_originalleft_entry. fom_beta_height_pfp_scalar_exists_originalleft_entry + S (fom_value_pfp_scalar_exists_originalleft) = S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_originalleft_entry * S ((S (fom_index_pfp_scalar_exists_originalleft)) * ac) + (fom_value_pfp_scalar_exists_originalleft))) /\ (exists fom_gap_pfp_scalar_exists_originalleft_value_bound. fom_gap_pfp_scalar_exists_originalleft_value_bound + S (fom_value_pfp_scalar_exists_originalleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_originalright. (exists fom_gap_pfp_scalar_exists_originalright_index_bound. fom_gap_pfp_scalar_exists_originalright_index_bound + S (fom_index_pfp_scalar_exists_originalright) = M) -> exists fom_value_pfp_scalar_exists_originalright. ((((exists fom_beta_height_pfp_scalar_exists_originalright_entry. fom_beta_height_pfp_scalar_exists_originalright_entry + S (fom_value_pfp_scalar_exists_originalright) = S ((S (fom_index_pfp_scalar_exists_originalright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_exists_originalright_entry. bb = fom_beta_quotient_pfp_scalar_exists_originalright_entry * S ((S (fom_index_pfp_scalar_exists_originalright)) * bc) + (fom_value_pfp_scalar_exists_originalright))) /\ (exists fom_gap_pfp_scalar_exists_originalright_value_bound. fom_gap_pfp_scalar_exists_originalright_value_bound + S (fom_value_pfp_scalar_exists_originalright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_originalcoefficients. (exists pfa_gap_scalar_exists_originalcoefficientsbound. pfa_gap_scalar_exists_originalcoefficientsbound + S (pfc_index_scalar_exists_originalcoefficients) = (N)) -> exists pfc_value_scalar_exists_originalcoefficients. ((((exists ff_h_pfp_scalar_exists_originalcoefficientsentry. ff_h_pfp_scalar_exists_originalcoefficientsentry + S (pfc_value_scalar_exists_originalcoefficients) = S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientsentry. cb = ff_q_pfp_scalar_exists_originalcoefficientsentry * S ((S (pfc_index_scalar_exists_originalcoefficients)) * cc) + (pfc_value_scalar_exists_originalcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_originalcoefficientscoefficient pfc_terms_scale_scalar_exists_originalcoefficientscoefficient pfc_natural_sum_scalar_exists_originalcoefficientscoefficient. ((forall pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_originalcoefficients))) -> exists pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_originalcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_originalcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_exists_originalcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_originalcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_originalcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_originalcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_originalcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_originalcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_originalcoefficients))) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_originalcoefficients)) -> exists fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_originalcoefficientscoefficient = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_originalcoefficientscoefficient) + (fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_originalcoefficientscoefficientsum = fs_q_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_originalcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_originalcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_originalcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_originalcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_originalcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_originalcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_originalcoefficients) + (p) * pfa_offset_right_scalar_exists_originalcoefficientscoefficientresiduecongruence))))))))))))))))))
  16. 0016exact hc
  17. 0017cases hcopy
  18. 0018cases hcopy_right
  19. 0019cases hcopy_right_right
  20. 0020have hs : exists sb sc. ((exists pfa_gap_scalar_exists_inputscalar. pfa_gap_scalar_exists_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_input. (exists pfa_gap_scalar_exists_inputindex. pfa_gap_scalar_exists_inputindex + S (pfp_index_scalar_exists_input) = (M)) -> exists pfp_source_scalar_exists_input pfp_value_scalar_exists_input. ((((exists ff_h_pfp_scalar_exists_inputsource. ff_h_pfp_scalar_exists_inputsource + S (pfp_source_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * bc)) /\ exists ff_q_pfp_scalar_exists_inputsource. bb = ff_q_pfp_scalar_exists_inputsource * S ((S (pfp_index_scalar_exists_input)) * bc) + (pfp_source_scalar_exists_input))) /\ (((((exists ff_h_pfp_scalar_exists_inputtarget. ff_h_pfp_scalar_exists_inputtarget + S (pfp_value_scalar_exists_input) = S ((S (pfp_index_scalar_exists_input)) * sc)) /\ exists ff_q_pfp_scalar_exists_inputtarget. sb = ff_q_pfp_scalar_exists_inputtarget * S ((S (pfp_index_scalar_exists_input)) * sc) + (pfp_value_scalar_exists_input))) /\ ((((exists pfa_gap_scalar_exists_inputoperationleft. pfa_gap_scalar_exists_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_inputoperationright. pfa_gap_scalar_exists_inputoperationright + S (pfp_source_scalar_exists_input) = (p)) /\ ((((exists pfa_gap_scalar_exists_inputoperationresultbound. pfa_gap_scalar_exists_inputoperationresultbound + S (pfp_value_scalar_exists_input) = (p)) /\ ((exists pfa_offset_left_scalar_exists_inputoperationresultcongruence pfa_offset_right_scalar_exists_inputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_input)) + (p) * pfa_offset_left_scalar_exists_inputoperationresultcongruence = (pfp_value_scalar_exists_input) + (p) * pfa_offset_right_scalar_exists_inputoperationresultcongruence))))))))))))))))
  21. 0021specialize prime_field_polynomial_scale_exists (p)
  22. 0022specialize prime_field_polynomial_scale_exists (k)
  23. 0023specialize prime_field_polynomial_scale_exists (bb)
  24. 0024specialize prime_field_polynomial_scale_exists (bc)
  25. 0025specialize prime_field_polynomial_scale_exists (M)
  26. 0026apply prime_field_polynomial_scale_exists
  27. 0027exact hp
  28. 0028exact hk
  29. 0029exact hcopy_right_left
  30. 0030cases hs
  31. 0031cases hs_witness
  32. 0032have hb : ((forall fom_index_pfp_scalar_exists_old_bound. (exists fom_gap_pfp_scalar_exists_old_bound_index_bound. fom_gap_pfp_scalar_exists_old_bound_index_bound + S (fom_index_pfp_scalar_exists_old_bound) = M) -> exists fom_value_pfp_scalar_exists_old_bound. ((((exists fom_beta_height_pfp_scalar_exists_old_bound_entry. fom_beta_height_pfp_scalar_exists_old_bound_entry + S (fom_value_pfp_scalar_exists_old_bound) = S ((S (fom_index_pfp_scalar_exists_old_bound)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_exists_old_bound_entry. bb = fom_beta_quotient_pfp_scalar_exists_old_bound_entry * S ((S (fom_index_pfp_scalar_exists_old_bound)) * bc) + (fom_value_pfp_scalar_exists_old_bound))) /\ (exists fom_gap_pfp_scalar_exists_old_bound_value_bound. fom_gap_pfp_scalar_exists_old_bound_value_bound + S (fom_value_pfp_scalar_exists_old_bound) = p))) /\ ((forall fom_index_pfp_scalar_exists_scaled_bound. (exists fom_gap_pfp_scalar_exists_scaled_bound_index_bound. fom_gap_pfp_scalar_exists_scaled_bound_index_bound + S (fom_index_pfp_scalar_exists_scaled_bound) = M) -> exists fom_value_pfp_scalar_exists_scaled_bound. ((((exists fom_beta_height_pfp_scalar_exists_scaled_bound_entry. fom_beta_height_pfp_scalar_exists_scaled_bound_entry + S (fom_value_pfp_scalar_exists_scaled_bound) = S ((S (fom_index_pfp_scalar_exists_scaled_bound)) * x1)) /\ exists fom_beta_quotient_pfp_scalar_exists_scaled_bound_entry. x = fom_beta_quotient_pfp_scalar_exists_scaled_bound_entry * S ((S (fom_index_pfp_scalar_exists_scaled_bound)) * x1) + (fom_value_pfp_scalar_exists_scaled_bound))) /\ (exists fom_gap_pfp_scalar_exists_scaled_bound_value_bound. fom_gap_pfp_scalar_exists_scaled_bound_value_bound + S (fom_value_pfp_scalar_exists_scaled_bound) = p)))))
  33. 0033specialize prime_field_polynomial_scale_bounded (p)
  34. 0034specialize prime_field_polynomial_scale_bounded (k)
  35. 0035specialize prime_field_polynomial_scale_bounded (bb)
  36. 0036specialize prime_field_polynomial_scale_bounded (bc)
  37. 0037specialize prime_field_polynomial_scale_bounded (x)
  38. 0038specialize prime_field_polynomial_scale_bounded (x1)
  39. 0039specialize prime_field_polynomial_scale_bounded (M)
  40. 0040apply prime_field_polynomial_scale_bounded
  41. 0041exact hs_witness_witness
  42. 0042cases hb
  43. 0043have hd : exists d e. ((forall fom_index_pfp_scalar_exists_chosen_productleft. (exists fom_gap_pfp_scalar_exists_chosen_productleft_index_bound. fom_gap_pfp_scalar_exists_chosen_productleft_index_bound + S (fom_index_pfp_scalar_exists_chosen_productleft) = L) -> exists fom_value_pfp_scalar_exists_chosen_productleft. ((((exists fom_beta_height_pfp_scalar_exists_chosen_productleft_entry. fom_beta_height_pfp_scalar_exists_chosen_productleft_entry + S (fom_value_pfp_scalar_exists_chosen_productleft) = S ((S (fom_index_pfp_scalar_exists_chosen_productleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_exists_chosen_productleft_entry. ab = fom_beta_quotient_pfp_scalar_exists_chosen_productleft_entry * S ((S (fom_index_pfp_scalar_exists_chosen_productleft)) * ac) + (fom_value_pfp_scalar_exists_chosen_productleft))) /\ (exists fom_gap_pfp_scalar_exists_chosen_productleft_value_bound. fom_gap_pfp_scalar_exists_chosen_productleft_value_bound + S (fom_value_pfp_scalar_exists_chosen_productleft) = p))) /\ (((forall fom_index_pfp_scalar_exists_chosen_productright. (exists fom_gap_pfp_scalar_exists_chosen_productright_index_bound. fom_gap_pfp_scalar_exists_chosen_productright_index_bound + S (fom_index_pfp_scalar_exists_chosen_productright) = M) -> exists fom_value_pfp_scalar_exists_chosen_productright. ((((exists fom_beta_height_pfp_scalar_exists_chosen_productright_entry. fom_beta_height_pfp_scalar_exists_chosen_productright_entry + S (fom_value_pfp_scalar_exists_chosen_productright) = S ((S (fom_index_pfp_scalar_exists_chosen_productright)) * x1)) /\ exists fom_beta_quotient_pfp_scalar_exists_chosen_productright_entry. x = fom_beta_quotient_pfp_scalar_exists_chosen_productright_entry * S ((S (fom_index_pfp_scalar_exists_chosen_productright)) * x1) + (fom_value_pfp_scalar_exists_chosen_productright))) /\ (exists fom_gap_pfp_scalar_exists_chosen_productright_value_bound. fom_gap_pfp_scalar_exists_chosen_productright_value_bound + S (fom_value_pfp_scalar_exists_chosen_productright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_exists_chosen_productcoefficients. (exists pfa_gap_scalar_exists_chosen_productcoefficientsbound. pfa_gap_scalar_exists_chosen_productcoefficientsbound + S (pfc_index_scalar_exists_chosen_productcoefficients) = (N)) -> exists pfc_value_scalar_exists_chosen_productcoefficients. ((((exists ff_h_pfp_scalar_exists_chosen_productcoefficientsentry. ff_h_pfp_scalar_exists_chosen_productcoefficientsentry + S (pfc_value_scalar_exists_chosen_productcoefficients) = S ((S (pfc_index_scalar_exists_chosen_productcoefficients)) * e)) /\ exists ff_q_pfp_scalar_exists_chosen_productcoefficientsentry. d = ff_q_pfp_scalar_exists_chosen_productcoefficientsentry * S ((S (pfc_index_scalar_exists_chosen_productcoefficients)) * e) + (pfc_value_scalar_exists_chosen_productcoefficients))) /\ ((exists pfc_terms_code_scalar_exists_chosen_productcoefficientscoefficient pfc_terms_scale_scalar_exists_chosen_productcoefficientscoefficient pfc_natural_sum_scalar_exists_chosen_productcoefficientscoefficient. ((forall pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonalbound. pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_exists_chosen_productcoefficients))) -> exists pfc_value_scalar_exists_chosen_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_exists_chosen_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_chosen_productcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_exists_chosen_productcoefficientscoefficient = ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_exists_chosen_productcoefficientscoefficient) + (pfc_value_scalar_exists_chosen_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm pfc_left_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm pfc_right_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)+pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm=(pfc_index_scalar_exists_chosen_productcoefficients)) /\ ((((((exists pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_exists_chosen_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)) * x1)) /\ exists ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightentry. x = ff_q_pfp_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)) * x1) + (pfc_right_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_exists_chosen_productcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_exists_chosen_productcoefficientscoefficientdiagonal)=pfc_left_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm*pfc_right_scalar_exists_chosen_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_exists_chosen_productcoefficientscoefficientsum fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_exists_chosen_productcoefficientscoefficientsum = fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_exists_chosen_productcoefficientscoefficient) = S ((S (S (pfc_index_scalar_exists_chosen_productcoefficients))) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_exists_chosen_productcoefficientscoefficientsum = fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_exists_chosen_productcoefficients))) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum) + (pfc_natural_sum_scalar_exists_chosen_productcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_exists_chosen_productcoefficients)) -> exists fs_a_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_chosen_productcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_exists_chosen_productcoefficientscoefficient = fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_exists_chosen_productcoefficientscoefficient) + (fs_a_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_exists_chosen_productcoefficientscoefficientsum = fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum) + (fs_r_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_exists_chosen_productcoefficientscoefficientsum = fs_q_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_exists_chosen_productcoefficientscoefficientsum) + (fs_s_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_exists_chosen_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_exists_chosen_productcoefficientscoefficientresiduebound. pfa_gap_scalar_exists_chosen_productcoefficientscoefficientresiduebound + S (pfc_value_scalar_exists_chosen_productcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_exists_chosen_productcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_exists_chosen_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_exists_chosen_productcoefficientscoefficient) + (p) * pfa_offset_left_scalar_exists_chosen_productcoefficientscoefficientresiduecongruence = (pfc_value_scalar_exists_chosen_productcoefficients) + (p) * pfa_offset_right_scalar_exists_chosen_productcoefficientscoefficientresiduecongruence))))))))))))))))))
  44. 0044specialize prime_field_polynomial_convolution_at_length_exists (p)
  45. 0045specialize prime_field_polynomial_convolution_at_length_exists (ab)
  46. 0046specialize prime_field_polynomial_convolution_at_length_exists (ac)
  47. 0047specialize prime_field_polynomial_convolution_at_length_exists (L)
  48. 0048specialize prime_field_polynomial_convolution_at_length_exists (x)
  49. 0049specialize prime_field_polynomial_convolution_at_length_exists (x1)
  50. 0050specialize prime_field_polynomial_convolution_at_length_exists (M)
  51. 0051specialize prime_field_polynomial_convolution_at_length_exists (N)
  52. 0052apply prime_field_polynomial_convolution_at_length_exists
  53. 0053exact hp
  54. 0054exact hcopy_left
  55. 0055exact hb_right
  56. 0056exact hcopy_right_right_left
  57. 0057cases hd
  58. 0058cases hd_witness
  59. 0059have he : exists eb ec. ((exists pfa_gap_scalar_exists_outputscalar. pfa_gap_scalar_exists_outputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_exists_output. (exists pfa_gap_scalar_exists_outputindex. pfa_gap_scalar_exists_outputindex + S (pfp_index_scalar_exists_output) = (N)) -> exists pfp_source_scalar_exists_output pfp_value_scalar_exists_output. ((((exists ff_h_pfp_scalar_exists_outputsource. ff_h_pfp_scalar_exists_outputsource + S (pfp_source_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * cc)) /\ exists ff_q_pfp_scalar_exists_outputsource. cb = ff_q_pfp_scalar_exists_outputsource * S ((S (pfp_index_scalar_exists_output)) * cc) + (pfp_source_scalar_exists_output))) /\ (((((exists ff_h_pfp_scalar_exists_outputtarget. ff_h_pfp_scalar_exists_outputtarget + S (pfp_value_scalar_exists_output) = S ((S (pfp_index_scalar_exists_output)) * ec)) /\ exists ff_q_pfp_scalar_exists_outputtarget. eb = ff_q_pfp_scalar_exists_outputtarget * S ((S (pfp_index_scalar_exists_output)) * ec) + (pfp_value_scalar_exists_output))) /\ ((((exists pfa_gap_scalar_exists_outputoperationleft. pfa_gap_scalar_exists_outputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_exists_outputoperationright. pfa_gap_scalar_exists_outputoperationright + S (pfp_source_scalar_exists_output) = (p)) /\ ((((exists pfa_gap_scalar_exists_outputoperationresultbound. pfa_gap_scalar_exists_outputoperationresultbound + S (pfp_value_scalar_exists_output) = (p)) /\ ((exists pfa_offset_left_scalar_exists_outputoperationresultcongruence pfa_offset_right_scalar_exists_outputoperationresultcongruence. ((k) * (pfp_source_scalar_exists_output)) + (p) * pfa_offset_left_scalar_exists_outputoperationresultcongruence = (pfp_value_scalar_exists_output) + (p) * pfa_offset_right_scalar_exists_outputoperationresultcongruence))))))))))))))))
  60. 0060specialize prime_field_polynomial_scale_exists (p)
  61. 0061specialize prime_field_polynomial_scale_exists (k)
  62. 0062specialize prime_field_polynomial_scale_exists (cb)
  63. 0063specialize prime_field_polynomial_scale_exists (cc)
  64. 0064specialize prime_field_polynomial_scale_exists (N)
  65. 0065apply prime_field_polynomial_scale_exists
  66. 0066exact hp
  67. 0067exact hk
  68. 0068specialize prime_field_polynomial_convolution_bounded (p)
  69. 0069specialize prime_field_polynomial_convolution_bounded (ab)
  70. 0070specialize prime_field_polynomial_convolution_bounded (ac)
  71. 0071specialize prime_field_polynomial_convolution_bounded (L)
  72. 0072specialize prime_field_polynomial_convolution_bounded (bb)
  73. 0073specialize prime_field_polynomial_convolution_bounded (bc)
  74. 0074specialize prime_field_polynomial_convolution_bounded (M)
  75. 0075specialize prime_field_polynomial_convolution_bounded (cb)
  76. 0076specialize prime_field_polynomial_convolution_bounded (cc)
  77. 0077specialize prime_field_polynomial_convolution_bounded (N)
  78. 0078apply prime_field_polynomial_convolution_bounded
  79. 0079exact hc
  80. 0080cases he
  81. 0081cases he_witness
  82. 0082exists x
  83. 0083exists x1
  84. 0084exists x2
  85. 0085exists x3
  86. 0086exists x4
  87. 0087exists x5
  88. 0088split
  89. 0089exact hs_witness_witness
  90. 0090split
  91. 0091exact hd_witness_witness
  92. 0092split
  93. 0093exact he_witness_witness
  94. 0094have hdata : ((N=N) /\ ((forall mdr_i_pfp_scalar_exists_comparison mdr_a_pfp_scalar_exists_comparison. (exists mdr_gap_pfp_scalar_exists_comparisonb. mdr_gap_pfp_scalar_exists_comparisonb + S (mdr_i_pfp_scalar_exists_comparison) = (N)) -> (((exists ff_h_mdr_pfp_scalar_exists_comparisono. ff_h_mdr_pfp_scalar_exists_comparisono + S (mdr_a_pfp_scalar_exists_comparison) = S ((S (mdr_i_pfp_scalar_exists_comparison)) * x3)) /\ exists ff_q_mdr_pfp_scalar_exists_comparisono. x2 = ff_q_mdr_pfp_scalar_exists_comparisono * S ((S (mdr_i_pfp_scalar_exists_comparison)) * x3) + (mdr_a_pfp_scalar_exists_comparison))) -> (((exists ff_h_mdr_pfp_scalar_exists_comparisonn. ff_h_mdr_pfp_scalar_exists_comparisonn + S (mdr_a_pfp_scalar_exists_comparison) = S ((S (mdr_i_pfp_scalar_exists_comparison)) * x5)) /\ exists ff_q_mdr_pfp_scalar_exists_comparisonn. x4 = ff_q_mdr_pfp_scalar_exists_comparisonn * S ((S (mdr_i_pfp_scalar_exists_comparison)) * x5) + (mdr_a_pfp_scalar_exists_comparison))))))
  95. 0095specialize prime_field_polynomial_convolution_right_scale_equal (p)
  96. 0096specialize prime_field_polynomial_convolution_right_scale_equal (k)
  97. 0097specialize prime_field_polynomial_convolution_right_scale_equal (ab)
  98. 0098specialize prime_field_polynomial_convolution_right_scale_equal (ac)
  99. 0099specialize prime_field_polynomial_convolution_right_scale_equal (L)
  100. 0100specialize prime_field_polynomial_convolution_right_scale_equal (bb)
  101. 0101specialize prime_field_polynomial_convolution_right_scale_equal (bc)
  102. 0102specialize prime_field_polynomial_convolution_right_scale_equal (M)
  103. 0103specialize prime_field_polynomial_convolution_right_scale_equal (x)
  104. 0104specialize prime_field_polynomial_convolution_right_scale_equal (x1)
  105. 0105specialize prime_field_polynomial_convolution_right_scale_equal (cb)
  106. 0106specialize prime_field_polynomial_convolution_right_scale_equal (cc)
  107. 0107specialize prime_field_polynomial_convolution_right_scale_equal (N)
  108. 0108specialize prime_field_polynomial_convolution_right_scale_equal (x2)
  109. 0109specialize prime_field_polynomial_convolution_right_scale_equal (x3)
  110. 0110specialize prime_field_polynomial_convolution_right_scale_equal (N)
  111. 0111specialize prime_field_polynomial_convolution_right_scale_equal (x4)
  112. 0112specialize prime_field_polynomial_convolution_right_scale_equal (x5)
  113. 0113apply prime_field_polynomial_convolution_right_scale_equal
  114. 0114exact hs_witness_witness
  115. 0115exact hc
  116. 0116exact hd_witness_witness
  117. 0117exact he_witness_witness
  118. 0118cases hdata
  119. 0119exact hdata_right