PG0015

prime_field_polynomial_convolution_right_scale

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

Scaling the actual right input preserves the proper representation length and gives the actual scalar action on the product output, including empty factors and zero scalars.

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 sb sc cb cc N db dc K. (((exists pfa_gap_scalar_product_inputscalar. pfa_gap_scalar_product_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_product_input. (exists pfa_gap_scalar_product_inputindex. pfa_gap_scalar_product_inputindex + S (pfp_index_scalar_product_input) = (M)) -> exists pfp_source_scalar_product_input pfp_value_scalar_product_input. ((((exists ff_h_pfp_scalar_product_inputsource. ff_h_pfp_scalar_product_inputsource + S (pfp_source_scalar_product_input) = S ((S (pfp_index_scalar_product_input)) * bc)) /\ exists ff_q_pfp_scalar_product_inputsource. bb = ff_q_pfp_scalar_product_inputsource * S ((S (pfp_index_scalar_product_input)) * bc) + (pfp_source_scalar_product_input))) /\ (((((exists ff_h_pfp_scalar_product_inputtarget. ff_h_pfp_scalar_product_inputtarget + S (pfp_value_scalar_product_input) = S ((S (pfp_index_scalar_product_input)) * sc)) /\ exists ff_q_pfp_scalar_product_inputtarget. sb = ff_q_pfp_scalar_product_inputtarget * S ((S (pfp_index_scalar_product_input)) * sc) + (pfp_value_scalar_product_input))) /\ ((((exists pfa_gap_scalar_product_inputoperationleft. pfa_gap_scalar_product_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_product_inputoperationright. pfa_gap_scalar_product_inputoperationright + S (pfp_source_scalar_product_input) = (p)) /\ ((((exists pfa_gap_scalar_product_inputoperationresultbound. pfa_gap_scalar_product_inputoperationresultbound + S (pfp_value_scalar_product_input) = (p)) /\ ((exists pfa_offset_left_scalar_product_inputoperationresultcongruence pfa_offset_right_scalar_product_inputoperationresultcongruence. ((k) * (pfp_source_scalar_product_input)) + (p) * pfa_offset_left_scalar_product_inputoperationresultcongruence = (pfp_value_scalar_product_input) + (p) * pfa_offset_right_scalar_product_inputoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_scalar_product_oldleft. (exists fom_gap_pfp_scalar_product_oldleft_index_bound. fom_gap_pfp_scalar_product_oldleft_index_bound + S (fom_index_pfp_scalar_product_oldleft) = L) -> exists fom_value_pfp_scalar_product_oldleft. ((((exists fom_beta_height_pfp_scalar_product_oldleft_entry. fom_beta_height_pfp_scalar_product_oldleft_entry + S (fom_value_pfp_scalar_product_oldleft) = S ((S (fom_index_pfp_scalar_product_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_product_oldleft_entry. ab = fom_beta_quotient_pfp_scalar_product_oldleft_entry * S ((S (fom_index_pfp_scalar_product_oldleft)) * ac) + (fom_value_pfp_scalar_product_oldleft))) /\ (exists fom_gap_pfp_scalar_product_oldleft_value_bound. fom_gap_pfp_scalar_product_oldleft_value_bound + S (fom_value_pfp_scalar_product_oldleft) = p))) /\ (((forall fom_index_pfp_scalar_product_oldright. (exists fom_gap_pfp_scalar_product_oldright_index_bound. fom_gap_pfp_scalar_product_oldright_index_bound + S (fom_index_pfp_scalar_product_oldright) = M) -> exists fom_value_pfp_scalar_product_oldright. ((((exists fom_beta_height_pfp_scalar_product_oldright_entry. fom_beta_height_pfp_scalar_product_oldright_entry + S (fom_value_pfp_scalar_product_oldright) = S ((S (fom_index_pfp_scalar_product_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_product_oldright_entry. bb = fom_beta_quotient_pfp_scalar_product_oldright_entry * S ((S (fom_index_pfp_scalar_product_oldright)) * bc) + (fom_value_pfp_scalar_product_oldright))) /\ (exists fom_gap_pfp_scalar_product_oldright_value_bound. fom_gap_pfp_scalar_product_oldright_value_bound + S (fom_value_pfp_scalar_product_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_product_oldcoefficients. (exists pfa_gap_scalar_product_oldcoefficientsbound. pfa_gap_scalar_product_oldcoefficientsbound + S (pfc_index_scalar_product_oldcoefficients) = (N)) -> exists pfc_value_scalar_product_oldcoefficients. ((((exists ff_h_pfp_scalar_product_oldcoefficientsentry. ff_h_pfp_scalar_product_oldcoefficientsentry + S (pfc_value_scalar_product_oldcoefficients) = S ((S (pfc_index_scalar_product_oldcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_product_oldcoefficientsentry. cb = ff_q_pfp_scalar_product_oldcoefficientsentry * S ((S (pfc_index_scalar_product_oldcoefficients)) * cc) + (pfc_value_scalar_product_oldcoefficients))) /\ ((exists pfc_terms_code_scalar_product_oldcoefficientscoefficient pfc_terms_scale_scalar_product_oldcoefficientscoefficient pfc_natural_sum_scalar_product_oldcoefficientscoefficient. ((forall pfc_index_scalar_product_oldcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonalbound. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_product_oldcoefficients))) -> exists pfc_value_scalar_product_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_product_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_product_oldcoefficientscoefficient = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient) + (pfc_value_scalar_product_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)+pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm=(pfc_index_scalar_product_oldcoefficients)) /\ ((((((exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_product_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_product_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_oldcoefficientscoefficientdiagonal)=pfc_left_scalar_product_oldcoefficientscoefficientdiagonalterm*pfc_right_scalar_product_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_oldcoefficientscoefficientsum fs_v_pfc_scalar_product_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_oldcoefficientscoefficient) = S ((S (S (pfc_index_scalar_product_oldcoefficients))) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_product_oldcoefficients))) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (pfc_natural_sum_scalar_product_oldcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_product_oldcoefficients)) -> exists fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_product_oldcoefficientscoefficient = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_oldcoefficientscoefficient) + (fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_product_oldcoefficientscoefficientsum = fs_q_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_oldcoefficientscoefficientsum) + (fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_product_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_oldcoefficientscoefficientresiduebound. pfa_gap_scalar_product_oldcoefficientscoefficientresiduebound + S (pfc_value_scalar_product_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_product_oldcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_product_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_product_oldcoefficientscoefficient) + (p) * pfa_offset_left_scalar_product_oldcoefficientscoefficientresiduecongruence = (pfc_value_scalar_product_oldcoefficients) + (p) * pfa_offset_right_scalar_product_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_scalar_product_scaledleft. (exists fom_gap_pfp_scalar_product_scaledleft_index_bound. fom_gap_pfp_scalar_product_scaledleft_index_bound + S (fom_index_pfp_scalar_product_scaledleft) = L) -> exists fom_value_pfp_scalar_product_scaledleft. ((((exists fom_beta_height_pfp_scalar_product_scaledleft_entry. fom_beta_height_pfp_scalar_product_scaledleft_entry + S (fom_value_pfp_scalar_product_scaledleft) = S ((S (fom_index_pfp_scalar_product_scaledleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_product_scaledleft_entry. ab = fom_beta_quotient_pfp_scalar_product_scaledleft_entry * S ((S (fom_index_pfp_scalar_product_scaledleft)) * ac) + (fom_value_pfp_scalar_product_scaledleft))) /\ (exists fom_gap_pfp_scalar_product_scaledleft_value_bound. fom_gap_pfp_scalar_product_scaledleft_value_bound + S (fom_value_pfp_scalar_product_scaledleft) = p))) /\ (((forall fom_index_pfp_scalar_product_scaledright. (exists fom_gap_pfp_scalar_product_scaledright_index_bound. fom_gap_pfp_scalar_product_scaledright_index_bound + S (fom_index_pfp_scalar_product_scaledright) = M) -> exists fom_value_pfp_scalar_product_scaledright. ((((exists fom_beta_height_pfp_scalar_product_scaledright_entry. fom_beta_height_pfp_scalar_product_scaledright_entry + S (fom_value_pfp_scalar_product_scaledright) = S ((S (fom_index_pfp_scalar_product_scaledright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_product_scaledright_entry. sb = fom_beta_quotient_pfp_scalar_product_scaledright_entry * S ((S (fom_index_pfp_scalar_product_scaledright)) * sc) + (fom_value_pfp_scalar_product_scaledright))) /\ (exists fom_gap_pfp_scalar_product_scaledright_value_bound. fom_gap_pfp_scalar_product_scaledright_value_bound + S (fom_value_pfp_scalar_product_scaledright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (K)))))))) /\ ((forall pfc_index_scalar_product_scaledcoefficients. (exists pfa_gap_scalar_product_scaledcoefficientsbound. pfa_gap_scalar_product_scaledcoefficientsbound + S (pfc_index_scalar_product_scaledcoefficients) = (K)) -> exists pfc_value_scalar_product_scaledcoefficients. ((((exists ff_h_pfp_scalar_product_scaledcoefficientsentry. ff_h_pfp_scalar_product_scaledcoefficientsentry + S (pfc_value_scalar_product_scaledcoefficients) = S ((S (pfc_index_scalar_product_scaledcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientsentry. db = ff_q_pfp_scalar_product_scaledcoefficientsentry * S ((S (pfc_index_scalar_product_scaledcoefficients)) * dc) + (pfc_value_scalar_product_scaledcoefficients))) /\ ((exists pfc_terms_code_scalar_product_scaledcoefficientscoefficient pfc_terms_scale_scalar_product_scaledcoefficientscoefficient pfc_natural_sum_scalar_product_scaledcoefficientscoefficient. ((forall pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonalbound. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_product_scaledcoefficients))) -> exists pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_product_scaledcoefficientscoefficient = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient) + (pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)+pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm=(pfc_index_scalar_product_scaledcoefficients)) /\ ((((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_scaledcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_product_scaledcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_product_scaledcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_scaledcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_scaledcoefficientscoefficientdiagonal)=pfc_left_scalar_product_scaledcoefficientscoefficientdiagonalterm*pfc_right_scalar_product_scaledcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient) = S ((S (S (pfc_index_scalar_product_scaledcoefficients))) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_product_scaledcoefficients))) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_product_scaledcoefficients)) -> exists fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_product_scaledcoefficientscoefficient = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaledcoefficientscoefficient) + (fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_product_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaledcoefficientscoefficientsum) + (fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_product_scaledcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_scaledcoefficientscoefficientresiduebound. pfa_gap_scalar_product_scaledcoefficientscoefficientresiduebound + S (pfc_value_scalar_product_scaledcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_product_scaledcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_product_scaledcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_product_scaledcoefficientscoefficient) + (p) * pfa_offset_left_scalar_product_scaledcoefficientscoefficientresiduecongruence = (pfc_value_scalar_product_scaledcoefficients) + (p) * pfa_offset_right_scalar_product_scaledcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((K=N) /\ ((((exists pfa_gap_scalar_product_resultscalar. pfa_gap_scalar_product_resultscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_product_result. (exists pfa_gap_scalar_product_resultindex. pfa_gap_scalar_product_resultindex + S (pfp_index_scalar_product_result) = (N)) -> exists pfp_source_scalar_product_result pfp_value_scalar_product_result. ((((exists ff_h_pfp_scalar_product_resultsource. ff_h_pfp_scalar_product_resultsource + S (pfp_source_scalar_product_result) = S ((S (pfp_index_scalar_product_result)) * cc)) /\ exists ff_q_pfp_scalar_product_resultsource. cb = ff_q_pfp_scalar_product_resultsource * S ((S (pfp_index_scalar_product_result)) * cc) + (pfp_source_scalar_product_result))) /\ (((((exists ff_h_pfp_scalar_product_resulttarget. ff_h_pfp_scalar_product_resulttarget + S (pfp_value_scalar_product_result) = S ((S (pfp_index_scalar_product_result)) * dc)) /\ exists ff_q_pfp_scalar_product_resulttarget. db = ff_q_pfp_scalar_product_resulttarget * S ((S (pfp_index_scalar_product_result)) * dc) + (pfp_value_scalar_product_result))) /\ ((((exists pfa_gap_scalar_product_resultoperationleft. pfa_gap_scalar_product_resultoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_product_resultoperationright. pfa_gap_scalar_product_resultoperationright + S (pfp_source_scalar_product_result) = (p)) /\ ((((exists pfa_gap_scalar_product_resultoperationresultbound. pfa_gap_scalar_product_resultoperationresultbound + S (pfp_value_scalar_product_result) = (p)) /\ ((exists pfa_offset_left_scalar_product_resultoperationresultcongruence pfa_offset_right_scalar_product_resultoperationresultcongruence. ((k) * (pfp_source_scalar_product_result)) + (p) * pfa_offset_left_scalar_product_resultoperationresultcongruence = (pfp_value_scalar_product_result) + (p) * pfa_offset_right_scalar_product_resultoperationresultcongruence))))))))))))))))))))

Constructive proof overview

Generated structural guide

Scaling the actual right input preserves the proper representation length and gives the actual scalar action on the product output, including empty factors and zero scalars.

The unchanged tactic script uses 2 declared prerequisites and contains 78 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_product_length_functional Alpha theorem; checked-use authorized PG0014 prime_field_convolution_coefficient_right_scale

Direct dependents

PG0016 prime_field_polynomial_convolution_right_scale_equal

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

78 script commands · 20 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 (1)
prime field convolution coefficient right scale

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 sb
  10. L10
    intro sc
02Fix variables and assumptionsL11–19

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

  1. L11
    intro cb
  2. L12
    intro cc
  3. L13
    intro N
  4. L14
    intro db
  5. L15
    intro dc
  6. L16
    intro K
  7. L17
    intro hs
  8. L18
    intro hc
  9. L19
    intro hd
03Separate the logical casesL20–25

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

  1. L20
    cases hc
  2. L21
    cases hc_right
  3. L22
    cases hc_right_right
  4. L23
    cases hd
  5. L24
    cases hd_right
  6. L25
    cases hd_right_right
04Establish hkL26–33

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

  1. L26
    have hk : K=N
  2. L27
    specialize polynomial_product_length_functional (L)
  3. L28
    specialize polynomial_product_length_functional (M)
  4. L29
    specialize polynomial_product_length_functional (K)
  5. L30
    specialize polynomial_product_length_functional (N)
  6. L31
    apply polynomial_product_length_functional
  7. L32
    exact hd_right_right_left
  8. L33
    exact hc_right_right_left
05Separate the logical casesL34–34

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

  1. L34
    split
06Use earlier factsL35–35

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

  1. L35
    exact hk
07Establish hcopyL36–37

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

  1. L36
    have hcopy : FpPolyScale(p,k,bb,bc,sb,sc,M)Definitions: FpPolyScale
  2. L37
    exact hs
08Separate the logical casesL38–39

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

  1. L38
    cases hcopy
  2. L39
    split
09Use earlier factsL40–40

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

  1. L40
    exact hcopy_left
10Fix variables and assumptionsL41–42

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

  1. L41
    intro i
  2. L42
    intro hi
11Establish haL43–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hc right right right.

  1. L43
    have ha : ∃ a. BetaAt(cb,cc,i,a) ∧ FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,a)Definitions: FpConvolutionCoefficientBetaAt
  2. L44
    specialize hc_right_right_right (i)
  3. L45
    apply hc_right_right_right
  4. L46
    exact hi
12Separate the logical casesL47–48

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

  1. L47
    cases ha
  2. L48
    cases ha_witness
13Establish hbL49–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hd right right right.

  1. L49
    have hb : ∃ a. BetaAt(db,dc,i,a) ∧ FpConvolutionCoefficient(p,ab,ac,L,sb,sc,M,i,a)Definitions: FpConvolutionCoefficientBetaAt
  2. L50
    specialize hd_right_right_right (i)
  3. L51
    apply hd_right_right_right
  4. L52
    rewrite hk
  5. L53
    exact hi
14Separate the logical casesL54–55

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

  1. L54
    cases hb
  2. L55
    cases hb_witness
15Construct an explicit witnessL56–57

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

  1. L56
    exists x
  2. L57
    exists x1
16Separate the logical casesL58–58

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

  1. L58
    split
17Use earlier factsL59–59

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

  1. L59
    exact ha_witness_left
18Separate the logical casesL60–60

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

  1. L60
    split
19Use earlier factsL61–70

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

  1. L61
    exact hb_witness_left
  2. L62
    specialize prime_field_convolution_coefficient_right_scale (p)
  3. L63
    specialize prime_field_convolution_coefficient_right_scale (k)
  4. L64
    specialize prime_field_convolution_coefficient_right_scale (ab)
  5. L65
    specialize prime_field_convolution_coefficient_right_scale (ac)
  6. L66
    specialize prime_field_convolution_coefficient_right_scale (L)
  7. L67
    specialize prime_field_convolution_coefficient_right_scale (bb)
  8. L68
    specialize prime_field_convolution_coefficient_right_scale (bc)
  9. L69
    specialize prime_field_convolution_coefficient_right_scale (M)
  10. L70
    specialize prime_field_convolution_coefficient_right_scale (sb)
20Use earlier factsL71–78

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

  1. L71
    specialize prime_field_convolution_coefficient_right_scale (sc)
  2. L72
    specialize prime_field_convolution_coefficient_right_scale (i)
  3. L73
    specialize prime_field_convolution_coefficient_right_scale (x)
  4. L74
    specialize prime_field_convolution_coefficient_right_scale (x1)
  5. L75
    apply prime_field_convolution_coefficient_right_scale
  6. L76
    exact hs
  7. L77
    exact ha_witness_right
  8. L78
    exact hb_witness_right

Library-wide reading audit

Original exact command ledger · 78 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 sb
  10. 0010intro sc
  11. 0011intro cb
  12. 0012intro cc
  13. 0013intro N
  14. 0014intro db
  15. 0015intro dc
  16. 0016intro K
  17. 0017intro hs
  18. 0018intro hc
  19. 0019intro hd
  20. 0020cases hc
  21. 0021cases hc_right
  22. 0022cases hc_right_right
  23. 0023cases hd
  24. 0024cases hd_right
  25. 0025cases hd_right_right
  26. 0026have hk : K=N
  27. 0027specialize polynomial_product_length_functional (L)
  28. 0028specialize polynomial_product_length_functional (M)
  29. 0029specialize polynomial_product_length_functional (K)
  30. 0030specialize polynomial_product_length_functional (N)
  31. 0031apply polynomial_product_length_functional
  32. 0032exact hd_right_right_left
  33. 0033exact hc_right_right_left
  34. 0034split
  35. 0035exact hk
  36. 0036have hcopy : ((exists pfa_gap_scalar_product_scale_copyscalar. pfa_gap_scalar_product_scale_copyscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_product_scale_copy. (exists pfa_gap_scalar_product_scale_copyindex. pfa_gap_scalar_product_scale_copyindex + S (pfp_index_scalar_product_scale_copy) = (M)) -> exists pfp_source_scalar_product_scale_copy pfp_value_scalar_product_scale_copy. ((((exists ff_h_pfp_scalar_product_scale_copysource. ff_h_pfp_scalar_product_scale_copysource + S (pfp_source_scalar_product_scale_copy) = S ((S (pfp_index_scalar_product_scale_copy)) * bc)) /\ exists ff_q_pfp_scalar_product_scale_copysource. bb = ff_q_pfp_scalar_product_scale_copysource * S ((S (pfp_index_scalar_product_scale_copy)) * bc) + (pfp_source_scalar_product_scale_copy))) /\ (((((exists ff_h_pfp_scalar_product_scale_copytarget. ff_h_pfp_scalar_product_scale_copytarget + S (pfp_value_scalar_product_scale_copy) = S ((S (pfp_index_scalar_product_scale_copy)) * sc)) /\ exists ff_q_pfp_scalar_product_scale_copytarget. sb = ff_q_pfp_scalar_product_scale_copytarget * S ((S (pfp_index_scalar_product_scale_copy)) * sc) + (pfp_value_scalar_product_scale_copy))) /\ ((((exists pfa_gap_scalar_product_scale_copyoperationleft. pfa_gap_scalar_product_scale_copyoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_product_scale_copyoperationright. pfa_gap_scalar_product_scale_copyoperationright + S (pfp_source_scalar_product_scale_copy) = (p)) /\ ((((exists pfa_gap_scalar_product_scale_copyoperationresultbound. pfa_gap_scalar_product_scale_copyoperationresultbound + S (pfp_value_scalar_product_scale_copy) = (p)) /\ ((exists pfa_offset_left_scalar_product_scale_copyoperationresultcongruence pfa_offset_right_scalar_product_scale_copyoperationresultcongruence. ((k) * (pfp_source_scalar_product_scale_copy)) + (p) * pfa_offset_left_scalar_product_scale_copyoperationresultcongruence = (pfp_value_scalar_product_scale_copy) + (p) * pfa_offset_right_scalar_product_scale_copyoperationresultcongruence))))))))))))))))
  37. 0037exact hs
  38. 0038cases hcopy
  39. 0039split
  40. 0040exact hcopy_left
  41. 0041intro i
  42. 0042intro hi
  43. 0043have ha : exists a. ((((exists ff_h_pfp_scalar_product_original_entry. ff_h_pfp_scalar_product_original_entry + S (a) = S ((S (i)) * cc)) /\ exists ff_q_pfp_scalar_product_original_entry. cb = ff_q_pfp_scalar_product_original_entry * S ((S (i)) * cc) + (a))) /\ ((exists pfc_terms_code_scalar_product_original_coefficient pfc_terms_scale_scalar_product_original_coefficient pfc_natural_sum_scalar_product_original_coefficient. ((forall pfc_index_scalar_product_original_coefficientdiagonal. (exists pfa_gap_scalar_product_original_coefficientdiagonalbound. pfa_gap_scalar_product_original_coefficientdiagonalbound + S (pfc_index_scalar_product_original_coefficientdiagonal) = (S (i))) -> exists pfc_value_scalar_product_original_coefficientdiagonal. ((((exists ff_h_pfp_scalar_product_original_coefficientdiagonalentry. ff_h_pfp_scalar_product_original_coefficientdiagonalentry + S (pfc_value_scalar_product_original_coefficientdiagonal) = S ((S (pfc_index_scalar_product_original_coefficientdiagonal)) * pfc_terms_scale_scalar_product_original_coefficient)) /\ exists ff_q_pfp_scalar_product_original_coefficientdiagonalentry. pfc_terms_code_scalar_product_original_coefficient = ff_q_pfp_scalar_product_original_coefficientdiagonalentry * S ((S (pfc_index_scalar_product_original_coefficientdiagonal)) * pfc_terms_scale_scalar_product_original_coefficient) + (pfc_value_scalar_product_original_coefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_original_coefficientdiagonalterm pfc_left_scalar_product_original_coefficientdiagonalterm pfc_right_scalar_product_original_coefficientdiagonalterm. (((pfc_index_scalar_product_original_coefficientdiagonal)+pfc_complement_scalar_product_original_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_scalar_product_original_coefficientdiagonaltermleftinside. pfa_gap_scalar_product_original_coefficientdiagonaltermleftinside + S (pfc_index_scalar_product_original_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_original_coefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_original_coefficientdiagonaltermleftentry + S (pfc_left_scalar_product_original_coefficientdiagonalterm) = S ((S (pfc_index_scalar_product_original_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_original_coefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_original_coefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_original_coefficientdiagonal)) * ac) + (pfc_left_scalar_product_original_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_original_coefficientdiagonaltermleftoutside. pfc_gap_scalar_product_original_coefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_original_coefficientdiagonal)) /\ (((pfc_left_scalar_product_original_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_original_coefficientdiagonaltermrightinside. pfa_gap_scalar_product_original_coefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_original_coefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_original_coefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_original_coefficientdiagonaltermrightentry + S (pfc_right_scalar_product_original_coefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_original_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_product_original_coefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_product_original_coefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_original_coefficientdiagonalterm)) * bc) + (pfc_right_scalar_product_original_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_original_coefficientdiagonaltermrightoutside. pfc_gap_scalar_product_original_coefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_original_coefficientdiagonalterm)) /\ (((pfc_right_scalar_product_original_coefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_original_coefficientdiagonal)=pfc_left_scalar_product_original_coefficientdiagonalterm*pfc_right_scalar_product_original_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_original_coefficientsum fs_v_pfc_scalar_product_original_coefficientsum. ((((exists fs_h_pfc_scalar_product_original_coefficientsum_body_start. fs_h_pfc_scalar_product_original_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_original_coefficientsum)) /\ exists fs_q_pfc_scalar_product_original_coefficientsum_body_start. fs_u_pfc_scalar_product_original_coefficientsum = fs_q_pfc_scalar_product_original_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_original_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_original_coefficientsum_body_terminal. fs_h_pfc_scalar_product_original_coefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_original_coefficient) = S ((S (S (i))) * fs_v_pfc_scalar_product_original_coefficientsum)) /\ exists fs_q_pfc_scalar_product_original_coefficientsum_body_terminal. fs_u_pfc_scalar_product_original_coefficientsum = fs_q_pfc_scalar_product_original_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_scalar_product_original_coefficientsum) + (pfc_natural_sum_scalar_product_original_coefficient))) /\ forall fs_i_pfc_scalar_product_original_coefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_original_coefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_original_coefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_original_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_scalar_product_original_coefficientsum_body_steps fs_r_pfc_scalar_product_original_coefficientsum_body_steps fs_s_pfc_scalar_product_original_coefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_original_coefficientsum_body_steps_summand. fs_h_pfc_scalar_product_original_coefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_original_coefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * pfc_terms_scale_scalar_product_original_coefficient)) /\ exists fs_q_pfc_scalar_product_original_coefficientsum_body_steps_summand. pfc_terms_code_scalar_product_original_coefficient = fs_q_pfc_scalar_product_original_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * pfc_terms_scale_scalar_product_original_coefficient) + (fs_a_pfc_scalar_product_original_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_original_coefficientsum_body_steps_partial. fs_h_pfc_scalar_product_original_coefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_original_coefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_original_coefficientsum)) /\ exists fs_q_pfc_scalar_product_original_coefficientsum_body_steps_partial. fs_u_pfc_scalar_product_original_coefficientsum = fs_q_pfc_scalar_product_original_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_original_coefficientsum) + (fs_r_pfc_scalar_product_original_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_original_coefficientsum_body_steps_successor. fs_h_pfc_scalar_product_original_coefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_original_coefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_original_coefficientsum)) /\ exists fs_q_pfc_scalar_product_original_coefficientsum_body_steps_successor. fs_u_pfc_scalar_product_original_coefficientsum = fs_q_pfc_scalar_product_original_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_original_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_original_coefficientsum) + (fs_s_pfc_scalar_product_original_coefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_original_coefficientsum_body_steps = fs_r_pfc_scalar_product_original_coefficientsum_body_steps + fs_a_pfc_scalar_product_original_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_original_coefficientresiduebound. pfa_gap_scalar_product_original_coefficientresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_scalar_product_original_coefficientresiduecongruence pfa_offset_right_scalar_product_original_coefficientresiduecongruence. (pfc_natural_sum_scalar_product_original_coefficient) + (p) * pfa_offset_left_scalar_product_original_coefficientresiduecongruence = (a) + (p) * pfa_offset_right_scalar_product_original_coefficientresiduecongruence)))))))))))
  44. 0044specialize hc_right_right_right (i)
  45. 0045apply hc_right_right_right
  46. 0046exact hi
  47. 0047cases ha
  48. 0048cases ha_witness
  49. 0049have hb : exists a. ((((exists ff_h_pfp_scalar_product_scaled_entry. ff_h_pfp_scalar_product_scaled_entry + S (a) = S ((S (i)) * dc)) /\ exists ff_q_pfp_scalar_product_scaled_entry. db = ff_q_pfp_scalar_product_scaled_entry * S ((S (i)) * dc) + (a))) /\ ((exists pfc_terms_code_scalar_product_scaled_coefficient pfc_terms_scale_scalar_product_scaled_coefficient pfc_natural_sum_scalar_product_scaled_coefficient. ((forall pfc_index_scalar_product_scaled_coefficientdiagonal. (exists pfa_gap_scalar_product_scaled_coefficientdiagonalbound. pfa_gap_scalar_product_scaled_coefficientdiagonalbound + S (pfc_index_scalar_product_scaled_coefficientdiagonal) = (S (i))) -> exists pfc_value_scalar_product_scaled_coefficientdiagonal. ((((exists ff_h_pfp_scalar_product_scaled_coefficientdiagonalentry. ff_h_pfp_scalar_product_scaled_coefficientdiagonalentry + S (pfc_value_scalar_product_scaled_coefficientdiagonal) = S ((S (pfc_index_scalar_product_scaled_coefficientdiagonal)) * pfc_terms_scale_scalar_product_scaled_coefficient)) /\ exists ff_q_pfp_scalar_product_scaled_coefficientdiagonalentry. pfc_terms_code_scalar_product_scaled_coefficient = ff_q_pfp_scalar_product_scaled_coefficientdiagonalentry * S ((S (pfc_index_scalar_product_scaled_coefficientdiagonal)) * pfc_terms_scale_scalar_product_scaled_coefficient) + (pfc_value_scalar_product_scaled_coefficientdiagonal))) /\ ((exists pfc_complement_scalar_product_scaled_coefficientdiagonalterm pfc_left_scalar_product_scaled_coefficientdiagonalterm pfc_right_scalar_product_scaled_coefficientdiagonalterm. (((pfc_index_scalar_product_scaled_coefficientdiagonal)+pfc_complement_scalar_product_scaled_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_scalar_product_scaled_coefficientdiagonaltermleftinside. pfa_gap_scalar_product_scaled_coefficientdiagonaltermleftinside + S (pfc_index_scalar_product_scaled_coefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_product_scaled_coefficientdiagonaltermleftentry. ff_h_pfp_scalar_product_scaled_coefficientdiagonaltermleftentry + S (pfc_left_scalar_product_scaled_coefficientdiagonalterm) = S ((S (pfc_index_scalar_product_scaled_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_product_scaled_coefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_product_scaled_coefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_product_scaled_coefficientdiagonal)) * ac) + (pfc_left_scalar_product_scaled_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaled_coefficientdiagonaltermleftoutside. pfc_gap_scalar_product_scaled_coefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_product_scaled_coefficientdiagonal)) /\ (((pfc_left_scalar_product_scaled_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_product_scaled_coefficientdiagonaltermrightinside. pfa_gap_scalar_product_scaled_coefficientdiagonaltermrightinside + S (pfc_complement_scalar_product_scaled_coefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_product_scaled_coefficientdiagonaltermrightentry. ff_h_pfp_scalar_product_scaled_coefficientdiagonaltermrightentry + S (pfc_right_scalar_product_scaled_coefficientdiagonalterm) = S ((S (pfc_complement_scalar_product_scaled_coefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_product_scaled_coefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_product_scaled_coefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_product_scaled_coefficientdiagonalterm)) * sc) + (pfc_right_scalar_product_scaled_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_product_scaled_coefficientdiagonaltermrightoutside. pfc_gap_scalar_product_scaled_coefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_product_scaled_coefficientdiagonalterm)) /\ (((pfc_right_scalar_product_scaled_coefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_product_scaled_coefficientdiagonal)=pfc_left_scalar_product_scaled_coefficientdiagonalterm*pfc_right_scalar_product_scaled_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_product_scaled_coefficientsum fs_v_pfc_scalar_product_scaled_coefficientsum. ((((exists fs_h_pfc_scalar_product_scaled_coefficientsum_body_start. fs_h_pfc_scalar_product_scaled_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_product_scaled_coefficientsum)) /\ exists fs_q_pfc_scalar_product_scaled_coefficientsum_body_start. fs_u_pfc_scalar_product_scaled_coefficientsum = fs_q_pfc_scalar_product_scaled_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_product_scaled_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_product_scaled_coefficientsum_body_terminal. fs_h_pfc_scalar_product_scaled_coefficientsum_body_terminal + S (pfc_natural_sum_scalar_product_scaled_coefficient) = S ((S (S (i))) * fs_v_pfc_scalar_product_scaled_coefficientsum)) /\ exists fs_q_pfc_scalar_product_scaled_coefficientsum_body_terminal. fs_u_pfc_scalar_product_scaled_coefficientsum = fs_q_pfc_scalar_product_scaled_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_scalar_product_scaled_coefficientsum) + (pfc_natural_sum_scalar_product_scaled_coefficient))) /\ forall fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps. (exists fs_lt_pfc_scalar_product_scaled_coefficientsum_body_steps_bound. fs_lt_pfc_scalar_product_scaled_coefficientsum_body_steps_bound + S fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_scalar_product_scaled_coefficientsum_body_steps fs_r_pfc_scalar_product_scaled_coefficientsum_body_steps fs_s_pfc_scalar_product_scaled_coefficientsum_body_steps. ((((exists fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_summand. fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_summand + S (fs_a_pfc_scalar_product_scaled_coefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaled_coefficient)) /\ exists fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_summand. pfc_terms_code_scalar_product_scaled_coefficient = fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * pfc_terms_scale_scalar_product_scaled_coefficient) + (fs_a_pfc_scalar_product_scaled_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_partial. fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_partial + S (fs_r_pfc_scalar_product_scaled_coefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaled_coefficientsum)) /\ exists fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_partial. fs_u_pfc_scalar_product_scaled_coefficientsum = fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaled_coefficientsum) + (fs_r_pfc_scalar_product_scaled_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_successor. fs_h_pfc_scalar_product_scaled_coefficientsum_body_steps_successor + S (fs_s_pfc_scalar_product_scaled_coefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaled_coefficientsum)) /\ exists fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_successor. fs_u_pfc_scalar_product_scaled_coefficientsum = fs_q_pfc_scalar_product_scaled_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_product_scaled_coefficientsum_body_steps)) * fs_v_pfc_scalar_product_scaled_coefficientsum) + (fs_s_pfc_scalar_product_scaled_coefficientsum_body_steps))) /\ fs_s_pfc_scalar_product_scaled_coefficientsum_body_steps = fs_r_pfc_scalar_product_scaled_coefficientsum_body_steps + fs_a_pfc_scalar_product_scaled_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_product_scaled_coefficientresiduebound. pfa_gap_scalar_product_scaled_coefficientresiduebound + S (a) = (p)) /\ ((exists pfa_offset_left_scalar_product_scaled_coefficientresiduecongruence pfa_offset_right_scalar_product_scaled_coefficientresiduecongruence. (pfc_natural_sum_scalar_product_scaled_coefficient) + (p) * pfa_offset_left_scalar_product_scaled_coefficientresiduecongruence = (a) + (p) * pfa_offset_right_scalar_product_scaled_coefficientresiduecongruence)))))))))))
  50. 0050specialize hd_right_right_right (i)
  51. 0051apply hd_right_right_right
  52. 0052rewrite hk
  53. 0053exact hi
  54. 0054cases hb
  55. 0055cases hb_witness
  56. 0056exists x
  57. 0057exists x1
  58. 0058split
  59. 0059exact ha_witness_left
  60. 0060split
  61. 0061exact hb_witness_left
  62. 0062specialize prime_field_convolution_coefficient_right_scale (p)
  63. 0063specialize prime_field_convolution_coefficient_right_scale (k)
  64. 0064specialize prime_field_convolution_coefficient_right_scale (ab)
  65. 0065specialize prime_field_convolution_coefficient_right_scale (ac)
  66. 0066specialize prime_field_convolution_coefficient_right_scale (L)
  67. 0067specialize prime_field_convolution_coefficient_right_scale (bb)
  68. 0068specialize prime_field_convolution_coefficient_right_scale (bc)
  69. 0069specialize prime_field_convolution_coefficient_right_scale (M)
  70. 0070specialize prime_field_convolution_coefficient_right_scale (sb)
  71. 0071specialize prime_field_convolution_coefficient_right_scale (sc)
  72. 0072specialize prime_field_convolution_coefficient_right_scale (i)
  73. 0073specialize prime_field_convolution_coefficient_right_scale (x)
  74. 0074specialize prime_field_convolution_coefficient_right_scale (x1)
  75. 0075apply prime_field_convolution_coefficient_right_scale
  76. 0076exact hs
  77. 0077exact ha_witness_right
  78. 0078exact hb_witness_right