PX006F

prime_field_polynomial_convolution_left_padding_equivalent_right

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

Genuine leading-zero padding of the right factor preserves the formal polynomial product, including empty factors whose proper product lengths need not differ by the padding count.

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

Exact expanded first-order arithmetic statement

forall p ab ac L bb bc M cb cc N BB BC t CB CC K. (~(p=0)) -> (((forall pfp_repeat_index_product_factor_padding_rightzeros. (exists pfa_gap_product_factor_padding_rightzerosindex. pfa_gap_product_factor_padding_rightzerosindex + S (pfp_repeat_index_product_factor_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_product_factor_padding_rightzerosentry. ff_h_pfp_product_factor_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_product_factor_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_product_factor_padding_rightzerosentry. BB = ff_q_pfp_product_factor_padding_rightzerosentry * S ((S (pfp_repeat_index_product_factor_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_product_factor_padding_right pfrep_value_product_factor_padding_right. (exists pfa_gap_product_factor_padding_rightbound. pfa_gap_product_factor_padding_rightbound + S (pfrep_index_product_factor_padding_right) = (M)) -> (((exists ff_h_pfp_product_factor_padding_rightinput. ff_h_pfp_product_factor_padding_rightinput + S (pfrep_value_product_factor_padding_right) = S ((S (pfrep_index_product_factor_padding_right)) * bc)) /\ exists ff_q_pfp_product_factor_padding_rightinput. bb = ff_q_pfp_product_factor_padding_rightinput * S ((S (pfrep_index_product_factor_padding_right)) * bc) + (pfrep_value_product_factor_padding_right))) -> (((exists ff_h_pfp_product_factor_padding_rightoutput. ff_h_pfp_product_factor_padding_rightoutput + S (pfrep_value_product_factor_padding_right) = S ((S ((t)+pfrep_index_product_factor_padding_right)) * BC)) /\ exists ff_q_pfp_product_factor_padding_rightoutput. BB = ff_q_pfp_product_factor_padding_rightoutput * S ((S ((t)+pfrep_index_product_factor_padding_right)) * BC) + (pfrep_value_product_factor_padding_right))))))) -> (((forall fom_index_pfp_product_original_rightleft. (exists fom_gap_pfp_product_original_rightleft_index_bound. fom_gap_pfp_product_original_rightleft_index_bound + S (fom_index_pfp_product_original_rightleft) = L) -> exists fom_value_pfp_product_original_rightleft. ((((exists fom_beta_height_pfp_product_original_rightleft_entry. fom_beta_height_pfp_product_original_rightleft_entry + S (fom_value_pfp_product_original_rightleft) = S ((S (fom_index_pfp_product_original_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_product_original_rightleft_entry. ab = fom_beta_quotient_pfp_product_original_rightleft_entry * S ((S (fom_index_pfp_product_original_rightleft)) * ac) + (fom_value_pfp_product_original_rightleft))) /\ (exists fom_gap_pfp_product_original_rightleft_value_bound. fom_gap_pfp_product_original_rightleft_value_bound + S (fom_value_pfp_product_original_rightleft) = p))) /\ (((forall fom_index_pfp_product_original_rightright. (exists fom_gap_pfp_product_original_rightright_index_bound. fom_gap_pfp_product_original_rightright_index_bound + S (fom_index_pfp_product_original_rightright) = M) -> exists fom_value_pfp_product_original_rightright. ((((exists fom_beta_height_pfp_product_original_rightright_entry. fom_beta_height_pfp_product_original_rightright_entry + S (fom_value_pfp_product_original_rightright) = S ((S (fom_index_pfp_product_original_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_product_original_rightright_entry. bb = fom_beta_quotient_pfp_product_original_rightright_entry * S ((S (fom_index_pfp_product_original_rightright)) * bc) + (fom_value_pfp_product_original_rightright))) /\ (exists fom_gap_pfp_product_original_rightright_value_bound. fom_gap_pfp_product_original_rightright_value_bound + S (fom_value_pfp_product_original_rightright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_product_original_rightcoefficients. (exists pfa_gap_product_original_rightcoefficientsbound. pfa_gap_product_original_rightcoefficientsbound + S (pfc_index_product_original_rightcoefficients) = (N)) -> exists pfc_value_product_original_rightcoefficients. ((((exists ff_h_pfp_product_original_rightcoefficientsentry. ff_h_pfp_product_original_rightcoefficientsentry + S (pfc_value_product_original_rightcoefficients) = S ((S (pfc_index_product_original_rightcoefficients)) * cc)) /\ exists ff_q_pfp_product_original_rightcoefficientsentry. cb = ff_q_pfp_product_original_rightcoefficientsentry * S ((S (pfc_index_product_original_rightcoefficients)) * cc) + (pfc_value_product_original_rightcoefficients))) /\ ((exists pfc_terms_code_product_original_rightcoefficientscoefficient pfc_terms_scale_product_original_rightcoefficientscoefficient pfc_natural_sum_product_original_rightcoefficientscoefficient. ((forall pfc_index_product_original_rightcoefficientscoefficientdiagonal. (exists pfa_gap_product_original_rightcoefficientscoefficientdiagonalbound. pfa_gap_product_original_rightcoefficientscoefficientdiagonalbound + S (pfc_index_product_original_rightcoefficientscoefficientdiagonal) = (S (pfc_index_product_original_rightcoefficients))) -> exists pfc_value_product_original_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonalentry + S (pfc_value_product_original_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_rightcoefficientscoefficient)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_product_original_rightcoefficientscoefficient = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_rightcoefficientscoefficient) + (pfc_value_product_original_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm pfc_left_product_original_rightcoefficientscoefficientdiagonalterm pfc_right_product_original_rightcoefficientscoefficientdiagonalterm. (((pfc_index_product_original_rightcoefficientscoefficientdiagonal)+pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm=(pfc_index_product_original_rightcoefficients)) /\ ((((((exists pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_original_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_product_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_product_original_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_product_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_original_rightcoefficientscoefficientdiagonal)=pfc_left_product_original_rightcoefficientscoefficientdiagonalterm*pfc_right_product_original_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_original_rightcoefficientscoefficientsum fs_v_pfc_product_original_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_start. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_start. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_original_rightcoefficientscoefficient) = S ((S (S (pfc_index_product_original_rightcoefficients))) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_original_rightcoefficients))) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (pfc_natural_sum_product_original_rightcoefficientscoefficient))) /\ forall fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_original_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_original_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps = S (pfc_index_product_original_rightcoefficients)) -> exists fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_rightcoefficientscoefficient)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_original_rightcoefficientscoefficient = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_rightcoefficientscoefficient) + (fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_original_rightcoefficientscoefficientresiduebound. pfa_gap_product_original_rightcoefficientscoefficientresiduebound + S (pfc_value_product_original_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_product_original_rightcoefficientscoefficientresiduecongruence pfa_offset_right_product_original_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_original_rightcoefficientscoefficient) + (p) * pfa_offset_left_product_original_rightcoefficientscoefficientresiduecongruence = (pfc_value_product_original_rightcoefficients) + (p) * pfa_offset_right_product_original_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_product_padded_rightleft. (exists fom_gap_pfp_product_padded_rightleft_index_bound. fom_gap_pfp_product_padded_rightleft_index_bound + S (fom_index_pfp_product_padded_rightleft) = L) -> exists fom_value_pfp_product_padded_rightleft. ((((exists fom_beta_height_pfp_product_padded_rightleft_entry. fom_beta_height_pfp_product_padded_rightleft_entry + S (fom_value_pfp_product_padded_rightleft) = S ((S (fom_index_pfp_product_padded_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_product_padded_rightleft_entry. ab = fom_beta_quotient_pfp_product_padded_rightleft_entry * S ((S (fom_index_pfp_product_padded_rightleft)) * ac) + (fom_value_pfp_product_padded_rightleft))) /\ (exists fom_gap_pfp_product_padded_rightleft_value_bound. fom_gap_pfp_product_padded_rightleft_value_bound + S (fom_value_pfp_product_padded_rightleft) = p))) /\ (((forall fom_index_pfp_product_padded_rightright. (exists fom_gap_pfp_product_padded_rightright_index_bound. fom_gap_pfp_product_padded_rightright_index_bound + S (fom_index_pfp_product_padded_rightright) = t+M) -> exists fom_value_pfp_product_padded_rightright. ((((exists fom_beta_height_pfp_product_padded_rightright_entry. fom_beta_height_pfp_product_padded_rightright_entry + S (fom_value_pfp_product_padded_rightright) = S ((S (fom_index_pfp_product_padded_rightright)) * BC)) /\ exists fom_beta_quotient_pfp_product_padded_rightright_entry. BB = fom_beta_quotient_pfp_product_padded_rightright_entry * S ((S (fom_index_pfp_product_padded_rightright)) * BC) + (fom_value_pfp_product_padded_rightright))) /\ (exists fom_gap_pfp_product_padded_rightright_value_bound. fom_gap_pfp_product_padded_rightright_value_bound + S (fom_value_pfp_product_padded_rightright) = p))) /\ (((((((L)=0 \/ (t+M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((t+M)=0)) /\ (((L)+(t+M)=S (K)))))))) /\ ((forall pfc_index_product_padded_rightcoefficients. (exists pfa_gap_product_padded_rightcoefficientsbound. pfa_gap_product_padded_rightcoefficientsbound + S (pfc_index_product_padded_rightcoefficients) = (K)) -> exists pfc_value_product_padded_rightcoefficients. ((((exists ff_h_pfp_product_padded_rightcoefficientsentry. ff_h_pfp_product_padded_rightcoefficientsentry + S (pfc_value_product_padded_rightcoefficients) = S ((S (pfc_index_product_padded_rightcoefficients)) * CC)) /\ exists ff_q_pfp_product_padded_rightcoefficientsentry. CB = ff_q_pfp_product_padded_rightcoefficientsentry * S ((S (pfc_index_product_padded_rightcoefficients)) * CC) + (pfc_value_product_padded_rightcoefficients))) /\ ((exists pfc_terms_code_product_padded_rightcoefficientscoefficient pfc_terms_scale_product_padded_rightcoefficientscoefficient pfc_natural_sum_product_padded_rightcoefficientscoefficient. ((forall pfc_index_product_padded_rightcoefficientscoefficientdiagonal. (exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonalbound. pfa_gap_product_padded_rightcoefficientscoefficientdiagonalbound + S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal) = (S (pfc_index_product_padded_rightcoefficients))) -> exists pfc_value_product_padded_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonalentry + S (pfc_value_product_padded_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_product_padded_rightcoefficientscoefficient = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient) + (pfc_value_product_padded_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm. (((pfc_index_product_padded_rightcoefficientscoefficientdiagonal)+pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm=(pfc_index_product_padded_rightcoefficients)) /\ ((((((exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightoutside+(t+M)=(pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_padded_rightcoefficientscoefficientdiagonal)=pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm*pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_padded_rightcoefficientscoefficientsum fs_v_pfc_product_padded_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_start. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_start. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_padded_rightcoefficientscoefficient) = S ((S (S (pfc_index_product_padded_rightcoefficients))) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_padded_rightcoefficients))) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (pfc_natural_sum_product_padded_rightcoefficientscoefficient))) /\ forall fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps = S (pfc_index_product_padded_rightcoefficients)) -> exists fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_padded_rightcoefficientscoefficient = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient) + (fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_padded_rightcoefficientscoefficientresiduebound. pfa_gap_product_padded_rightcoefficientscoefficientresiduebound + S (pfc_value_product_padded_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_product_padded_rightcoefficientscoefficientresiduecongruence pfa_offset_right_product_padded_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_padded_rightcoefficientscoefficient) + (p) * pfa_offset_left_product_padded_rightcoefficientscoefficientresiduecongruence = (pfc_value_product_padded_rightcoefficients) + (p) * pfa_offset_right_product_padded_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_product_equivalent_right pfrep_left_product_equivalent_right pfrep_right_product_equivalent_right. ((exists pfrep_position_product_equivalent_rightfirst. ((pfrep_position_product_equivalent_rightfirst+S (pfrep_power_product_equivalent_right)=(N)) /\ ((((exists ff_h_pfp_product_equivalent_rightfirstentry. ff_h_pfp_product_equivalent_rightfirstentry + S (pfrep_left_product_equivalent_right) = S ((S (pfrep_position_product_equivalent_rightfirst)) * cc)) /\ exists ff_q_pfp_product_equivalent_rightfirstentry. cb = ff_q_pfp_product_equivalent_rightfirstentry * S ((S (pfrep_position_product_equivalent_rightfirst)) * cc) + (pfrep_left_product_equivalent_right)))))) \/ (((exists pfrep_gap_product_equivalent_rightfirstoutside. pfrep_gap_product_equivalent_rightfirstoutside+(N)=(pfrep_power_product_equivalent_right)) /\ (((pfrep_left_product_equivalent_right)=0))))) -> ((exists pfrep_position_product_equivalent_rightsecond. ((pfrep_position_product_equivalent_rightsecond+S (pfrep_power_product_equivalent_right)=(K)) /\ ((((exists ff_h_pfp_product_equivalent_rightsecondentry. ff_h_pfp_product_equivalent_rightsecondentry + S (pfrep_right_product_equivalent_right) = S ((S (pfrep_position_product_equivalent_rightsecond)) * CC)) /\ exists ff_q_pfp_product_equivalent_rightsecondentry. CB = ff_q_pfp_product_equivalent_rightsecondentry * S ((S (pfrep_position_product_equivalent_rightsecond)) * CC) + (pfrep_right_product_equivalent_right)))))) \/ (((exists pfrep_gap_product_equivalent_rightsecondoutside. pfrep_gap_product_equivalent_rightsecondoutside+(K)=(pfrep_power_product_equivalent_right)) /\ (((pfrep_right_product_equivalent_right)=0))))) -> pfrep_left_product_equivalent_right=pfrep_right_product_equivalent_right)

Constructive proof overview

Generated structural guide

Genuine leading-zero padding of the right factor preserves the formal polynomial product, including empty factors whose proper product lengths need not differ by the padding count.

The unchanged tactic script uses 10 declared prerequisites and contains 211 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Alpha theorem; checked-use authorized matrix_rank_no_index_below_zero Alpha theorem; checked-use authorized prime_field_polynomial_convolution_zero_left Alpha theorem; checked-use authorized prime_field_polynomial_convolution_zero_right Alpha theorem; checked-use authorized PX005D polynomial_left_pad_zero_prefix PX0022 prime_field_polynomial_zero_prefix_equivalent_empty PX0010 prime_field_polynomial_equivalent_transitive PX000F prime_field_polynomial_equivalent_symmetric PX006D prime_field_polynomial_convolution_left_padding_nonempty_right PX001B prime_field_polynomial_left_pad_equivalent

Direct dependents

PX0070 prime_field_polynomial_convolution_both_left_paddings_equivalent PX0078 prime_field_polynomial_convolution_equivalent_congruent_right

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

211 script commands · 35 reading checkpoints · 13 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 (6)
polynomial left pad zero prefixprime field polynomial zero prefix equivalent emptyprime field polynomial equivalent transitiveprime field polynomial equivalent symmetricprime field polynomial convolution left padding nonempty rightprime field polynomial left pad equivalent

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

01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro BB
  2. L12
    intro BC
  3. L13
    intro t
  4. L14
    intro CB
  5. L15
    intro CC
  6. L16
    intro K
  7. L17
    intro hp
  8. L18
    intro hpad
  9. L19
    intro hc
  10. L20
    intro hn
03Establish hLL21–24

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

  1. L21
    have hL : L=0 \/ ~(L=0)
  2. L22
    specialize eq_decidable (L)
  3. L23
    specialize eq_decidable (0)
  4. L24
    apply eq_decidable
04Separate the logical casesL25–25

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

  1. L25
    cases hL
05Establish hzL26–29

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

  1. L26
    have hz : forall pfp_repeat_index_empty_factor_zero_rightleft. (exists pfa_gap_empty_factor_zero_rightleftindex. pfa_gap_empty_factor_zero_rightleftindex + S (pfp_repeat_index_empty_factor_zero_rightleft) = (L)) -> (((exists ff_h_pfp_empty_factor_zero_rightleftentry. ff_h_pfp_empty_factor_zero_rightleftentry + S (0) = S ((S (pfp_repeat_index_empty_factor_zero_rightleft)) * ac)) /\ exists ff_q_pfp_empty_factor_zero_rightleftentry. ab = ff_q_pfp_empty_factor_zero_rightleftentry * S ((S (pfp_repeat_index_empty_factor_zero_rightleft)) * ac) + (0)))
  2. L27
    intro j
  3. L28
    intro hj
  4. L29
    rewrite hL_left at hj
06Separate the logical casesL30–30

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

  1. L30
    exfalso
07Use earlier factsL31–33

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

  1. L31
    specialize matrix_rank_no_index_below_zero (j)
  2. L32
    apply matrix_rank_no_index_below_zero
  3. L33
    exact hj
08Establish hc0L34–43

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

  1. L34
    have hc0 : Repeat(cb,cc,0,N)Definitions: Repeat
  2. L35
    specialize prime_field_polynomial_convolution_zero_left (p)
  3. L36
    specialize prime_field_polynomial_convolution_zero_left (ab)
  4. L37
    specialize prime_field_polynomial_convolution_zero_left (ac)
  5. L38
    specialize prime_field_polynomial_convolution_zero_left (L)
  6. L39
    specialize prime_field_polynomial_convolution_zero_left (bb)
  7. L40
    specialize prime_field_polynomial_convolution_zero_left (bc)
  8. L41
    specialize prime_field_polynomial_convolution_zero_left (M)
  9. L42
    specialize prime_field_polynomial_convolution_zero_left (cb)
  10. L43
    specialize prime_field_polynomial_convolution_zero_left (cc)
09Use earlier factsL44–48

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

  1. L44
    specialize prime_field_polynomial_convolution_zero_left (N)
  2. L45
    apply prime_field_polynomial_convolution_zero_left
  3. L46
    exact hp
  4. L47
    exact hz
  5. L48
    exact hc
10Establish hn0L49–58

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

  1. L49
    have hn0 : forall pfp_repeat_index_empty_padded_product_rightleft. (exists pfa_gap_empty_padded_product_rightleftindex. pfa_gap_empty_padded_product_rightleftindex + S (pfp_repeat_index_empty_padded_product_rightleft) = (K)) -> (((exists ff_h_pfp_empty_padded_product_rightleftentry. ff_h_pfp_empty_padded_product_rightleftentry + S (0) = S ((S (pfp_repeat_index_empty_padded_product_rightleft)) * CC)) /\ exists ff_q_pfp_empty_padded_product_rightleftentry. CB = ff_q_pfp_empty_padded_product_rightleftentry * S ((S (pfp_repeat_index_empty_padded_product_rightleft)) * CC) + (0)))
  2. L50
    specialize prime_field_polynomial_convolution_zero_left (p)
  3. L51
    specialize prime_field_polynomial_convolution_zero_left (ab)
  4. L52
    specialize prime_field_polynomial_convolution_zero_left (ac)
  5. L53
    specialize prime_field_polynomial_convolution_zero_left (L)
  6. L54
    specialize prime_field_polynomial_convolution_zero_left (BB)
  7. L55
    specialize prime_field_polynomial_convolution_zero_left (BC)
  8. L56
    specialize prime_field_polynomial_convolution_zero_left (t+M)
  9. L57
    specialize prime_field_polynomial_convolution_zero_left (CB)
  10. L58
    specialize prime_field_polynomial_convolution_zero_left (CC)
11Use earlier factsL59–63

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

  1. L59
    specialize prime_field_polynomial_convolution_zero_left (K)
  2. L60
    apply prime_field_polynomial_convolution_zero_left
  3. L61
    exact hp
  4. L62
    exact hz
  5. L63
    exact hn
12Establish hecL64–69

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial zero prefix equivalent empty.

  1. L64
    have hec : PolynomialEquivalent(cb,cc,N,0,0,0)Definitions: PolynomialEquivalent
  2. L65
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  3. L66
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  4. L67
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  5. L68
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L69
    exact hc0
13Establish henL70–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial zero prefix equivalent empty.

  1. L70
    have hen : PolynomialEquivalent(CB,CC,K,0,0,0)Definitions: PolynomialEquivalent
  2. L71
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  3. L72
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  4. L73
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  5. L74
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L75
    exact hn0
  7. L76
    specialize prime_field_polynomial_equivalent_transitive (cb)
  8. L77
    specialize prime_field_polynomial_equivalent_transitive (cc)
  9. L78
    specialize prime_field_polynomial_equivalent_transitive (N)
  10. L79
    specialize prime_field_polynomial_equivalent_transitive (0)
14Use earlier factsL80–89

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

  1. L80
    specialize prime_field_polynomial_equivalent_transitive (0)
  2. L81
    specialize prime_field_polynomial_equivalent_transitive (0)
  3. L82
    specialize prime_field_polynomial_equivalent_transitive (CB)
  4. L83
    specialize prime_field_polynomial_equivalent_transitive (CC)
  5. L84
    specialize prime_field_polynomial_equivalent_transitive (K)
  6. L85
    apply prime_field_polynomial_equivalent_transitive
  7. L86
    exact hec
  8. L87
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  9. L88
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  10. L89
    specialize prime_field_polynomial_equivalent_symmetric (K)
15Use earlier factsL90–94

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

  1. L90
    specialize prime_field_polynomial_equivalent_symmetric (0)
  2. L91
    specialize prime_field_polynomial_equivalent_symmetric (0)
  3. L92
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L93
    apply prime_field_polynomial_equivalent_symmetric
  5. L94
    exact hen
16Establish hML95–98

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

  1. L95
    have hM : M=0 \/ ~(M=0)
  2. L96
    specialize eq_decidable (M)
  3. L97
    specialize eq_decidable (0)
  4. L98
    apply eq_decidable
17Separate the logical casesL99–99

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

  1. L99
    cases hM
18Establish hzL100–103

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

  1. L100
    have hz : forall pfp_repeat_index_empty_factor_zero_rightright. (exists pfa_gap_empty_factor_zero_rightrightindex. pfa_gap_empty_factor_zero_rightrightindex + S (pfp_repeat_index_empty_factor_zero_rightright) = (M)) -> (((exists ff_h_pfp_empty_factor_zero_rightrightentry. ff_h_pfp_empty_factor_zero_rightrightentry + S (0) = S ((S (pfp_repeat_index_empty_factor_zero_rightright)) * bc)) /\ exists ff_q_pfp_empty_factor_zero_rightrightentry. bb = ff_q_pfp_empty_factor_zero_rightrightentry * S ((S (pfp_repeat_index_empty_factor_zero_rightright)) * bc) + (0)))
  2. L101
    intro j
  3. L102
    intro hj
  4. L103
    rewrite hM_left at hj
19Separate the logical casesL104–104

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

  1. L104
    exfalso
20Use earlier factsL105–107

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

  1. L105
    specialize matrix_rank_no_index_below_zero (j)
  2. L106
    apply matrix_rank_no_index_below_zero
  3. L107
    exact hj
21Establish hc0L108–117

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

  1. L108
    have hc0 : Repeat(cb,cc,0,N)Definitions: Repeat
  2. L109
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L110
    specialize prime_field_polynomial_convolution_zero_right (ab)
  4. L111
    specialize prime_field_polynomial_convolution_zero_right (ac)
  5. L112
    specialize prime_field_polynomial_convolution_zero_right (L)
  6. L113
    specialize prime_field_polynomial_convolution_zero_right (bb)
  7. L114
    specialize prime_field_polynomial_convolution_zero_right (bc)
  8. L115
    specialize prime_field_polynomial_convolution_zero_right (M)
  9. L116
    specialize prime_field_polynomial_convolution_zero_right (cb)
  10. L117
    specialize prime_field_polynomial_convolution_zero_right (cc)
22Use earlier factsL118–122

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

  1. L118
    specialize prime_field_polynomial_convolution_zero_right (N)
  2. L119
    apply prime_field_polynomial_convolution_zero_right
  3. L120
    exact hp
  4. L121
    exact hz
  5. L122
    exact hc
23Establish hn0L123–132

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

  1. L123
    have hn0 : forall pfp_repeat_index_empty_padded_product_rightright. (exists pfa_gap_empty_padded_product_rightrightindex. pfa_gap_empty_padded_product_rightrightindex + S (pfp_repeat_index_empty_padded_product_rightright) = (K)) -> (((exists ff_h_pfp_empty_padded_product_rightrightentry. ff_h_pfp_empty_padded_product_rightrightentry + S (0) = S ((S (pfp_repeat_index_empty_padded_product_rightright)) * CC)) /\ exists ff_q_pfp_empty_padded_product_rightrightentry. CB = ff_q_pfp_empty_padded_product_rightrightentry * S ((S (pfp_repeat_index_empty_padded_product_rightright)) * CC) + (0)))
  2. L124
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L125
    specialize prime_field_polynomial_convolution_zero_right (ab)
  4. L126
    specialize prime_field_polynomial_convolution_zero_right (ac)
  5. L127
    specialize prime_field_polynomial_convolution_zero_right (L)
  6. L128
    specialize prime_field_polynomial_convolution_zero_right (BB)
  7. L129
    specialize prime_field_polynomial_convolution_zero_right (BC)
  8. L130
    specialize prime_field_polynomial_convolution_zero_right (t+M)
  9. L131
    specialize prime_field_polynomial_convolution_zero_right (CB)
  10. L132
    specialize prime_field_polynomial_convolution_zero_right (CC)
24Use earlier factsL133–142

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

  1. L133
    specialize prime_field_polynomial_convolution_zero_right (K)
  2. L134
    apply prime_field_polynomial_convolution_zero_right
  3. L135
    exact hp
  4. L136
    specialize polynomial_left_pad_zero_prefix (bb)
  5. L137
    specialize polynomial_left_pad_zero_prefix (bc)
  6. L138
    specialize polynomial_left_pad_zero_prefix (M)
  7. L139
    specialize polynomial_left_pad_zero_prefix (t)
  8. L140
    specialize polynomial_left_pad_zero_prefix (BB)
  9. L141
    specialize polynomial_left_pad_zero_prefix (BC)
  10. L142
    apply polynomial_left_pad_zero_prefix
25Use earlier factsL143–145

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

  1. L143
    exact hz
  2. L144
    exact hpad
  3. L145
    exact hn
26Establish hecL146–151

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial zero prefix equivalent empty.

  1. L146
    have hec : PolynomialEquivalent(cb,cc,N,0,0,0)Definitions: PolynomialEquivalent
  2. L147
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  3. L148
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  4. L149
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  5. L150
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L151
    exact hc0
27Establish henL152–161

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial zero prefix equivalent empty.

  1. L152
    have hen : PolynomialEquivalent(CB,CC,K,0,0,0)Definitions: PolynomialEquivalent
  2. L153
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  3. L154
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  4. L155
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  5. L156
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L157
    exact hn0
  7. L158
    specialize prime_field_polynomial_equivalent_transitive (cb)
  8. L159
    specialize prime_field_polynomial_equivalent_transitive (cc)
  9. L160
    specialize prime_field_polynomial_equivalent_transitive (N)
  10. L161
    specialize prime_field_polynomial_equivalent_transitive (0)
28Use earlier factsL162–171

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

  1. L162
    specialize prime_field_polynomial_equivalent_transitive (0)
  2. L163
    specialize prime_field_polynomial_equivalent_transitive (0)
  3. L164
    specialize prime_field_polynomial_equivalent_transitive (CB)
  4. L165
    specialize prime_field_polynomial_equivalent_transitive (CC)
  5. L166
    specialize prime_field_polynomial_equivalent_transitive (K)
  6. L167
    apply prime_field_polynomial_equivalent_transitive
  7. L168
    exact hec
  8. L169
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  9. L170
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  10. L171
    specialize prime_field_polynomial_equivalent_symmetric (K)
29Use earlier factsL172–176

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

  1. L172
    specialize prime_field_polynomial_equivalent_symmetric (0)
  2. L173
    specialize prime_field_polynomial_equivalent_symmetric (0)
  3. L174
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L175
    apply prime_field_polynomial_equivalent_symmetric
  5. L176
    exact hen
30Establish hdL177–186

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

  1. L177
    have hd : K = t + N ∧ PolynomialLeftPad(cb,cc,N,t,CB,CC)Definitions: PolynomialLeftPad
  2. L178
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (p)
  3. L179
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ab)
  4. L180
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ac)
  5. L181
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (L)
  6. L182
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bb)
  7. L183
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bc)
  8. L184
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (M)
  9. L185
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cb)
  10. L186
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cc)
31Use earlier factsL187–196

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

  1. L187
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (N)
  2. L188
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BB)
  3. L189
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BC)
  4. L190
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (t)
  5. L191
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CB)
  6. L192
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CC)
  7. L193
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (K)
  8. L194
    apply prime_field_polynomial_convolution_left_padding_nonempty_right
  9. L195
    exact hp
  10. L196
    exact hL_right
32Use earlier factsL197–200

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

  1. L197
    exact hM_right
  2. L198
    exact hpad
  3. L199
    exact hc
  4. L200
    exact hn
33Separate the logical casesL201–201

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

  1. L201
    cases hd
34Calculate and transport equalitiesL202–203

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L202
    rewrite hd_left
  2. L203
    rewrite hd_left
35Use earlier factsL204–211

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

  1. L204
    specialize prime_field_polynomial_left_pad_equivalent (cb)
  2. L205
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  3. L206
    specialize prime_field_polynomial_left_pad_equivalent (N)
  4. L207
    specialize prime_field_polynomial_left_pad_equivalent (t)
  5. L208
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  6. L209
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  7. L210
    apply prime_field_polynomial_left_pad_equivalent
  8. L211
    exact hd_right

Library-wide reading audit

Original exact command ledger · 211 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro cb
  9. 0009intro cc
  10. 0010intro N
  11. 0011intro BB
  12. 0012intro BC
  13. 0013intro t
  14. 0014intro CB
  15. 0015intro CC
  16. 0016intro K
  17. 0017intro hp
  18. 0018intro hpad
  19. 0019intro hc
  20. 0020intro hn
  21. 0021have hL : L=0 \/ ~(L=0)
  22. 0022specialize eq_decidable (L)
  23. 0023specialize eq_decidable (0)
  24. 0024apply eq_decidable
  25. 0025cases hL
  26. 0026have hz : forall pfp_repeat_index_empty_factor_zero_rightleft. (exists pfa_gap_empty_factor_zero_rightleftindex. pfa_gap_empty_factor_zero_rightleftindex + S (pfp_repeat_index_empty_factor_zero_rightleft) = (L)) -> (((exists ff_h_pfp_empty_factor_zero_rightleftentry. ff_h_pfp_empty_factor_zero_rightleftentry + S (0) = S ((S (pfp_repeat_index_empty_factor_zero_rightleft)) * ac)) /\ exists ff_q_pfp_empty_factor_zero_rightleftentry. ab = ff_q_pfp_empty_factor_zero_rightleftentry * S ((S (pfp_repeat_index_empty_factor_zero_rightleft)) * ac) + (0)))
  27. 0027intro j
  28. 0028intro hj
  29. 0029rewrite hL_left at hj
  30. 0030exfalso
  31. 0031specialize matrix_rank_no_index_below_zero (j)
  32. 0032apply matrix_rank_no_index_below_zero
  33. 0033exact hj
  34. 0034have hc0 : forall pfp_repeat_index_empty_original_product_rightleft. (exists pfa_gap_empty_original_product_rightleftindex. pfa_gap_empty_original_product_rightleftindex + S (pfp_repeat_index_empty_original_product_rightleft) = (N)) -> (((exists ff_h_pfp_empty_original_product_rightleftentry. ff_h_pfp_empty_original_product_rightleftentry + S (0) = S ((S (pfp_repeat_index_empty_original_product_rightleft)) * cc)) /\ exists ff_q_pfp_empty_original_product_rightleftentry. cb = ff_q_pfp_empty_original_product_rightleftentry * S ((S (pfp_repeat_index_empty_original_product_rightleft)) * cc) + (0)))
  35. 0035specialize prime_field_polynomial_convolution_zero_left (p)
  36. 0036specialize prime_field_polynomial_convolution_zero_left (ab)
  37. 0037specialize prime_field_polynomial_convolution_zero_left (ac)
  38. 0038specialize prime_field_polynomial_convolution_zero_left (L)
  39. 0039specialize prime_field_polynomial_convolution_zero_left (bb)
  40. 0040specialize prime_field_polynomial_convolution_zero_left (bc)
  41. 0041specialize prime_field_polynomial_convolution_zero_left (M)
  42. 0042specialize prime_field_polynomial_convolution_zero_left (cb)
  43. 0043specialize prime_field_polynomial_convolution_zero_left (cc)
  44. 0044specialize prime_field_polynomial_convolution_zero_left (N)
  45. 0045apply prime_field_polynomial_convolution_zero_left
  46. 0046exact hp
  47. 0047exact hz
  48. 0048exact hc
  49. 0049have hn0 : forall pfp_repeat_index_empty_padded_product_rightleft. (exists pfa_gap_empty_padded_product_rightleftindex. pfa_gap_empty_padded_product_rightleftindex + S (pfp_repeat_index_empty_padded_product_rightleft) = (K)) -> (((exists ff_h_pfp_empty_padded_product_rightleftentry. ff_h_pfp_empty_padded_product_rightleftentry + S (0) = S ((S (pfp_repeat_index_empty_padded_product_rightleft)) * CC)) /\ exists ff_q_pfp_empty_padded_product_rightleftentry. CB = ff_q_pfp_empty_padded_product_rightleftentry * S ((S (pfp_repeat_index_empty_padded_product_rightleft)) * CC) + (0)))
  50. 0050specialize prime_field_polynomial_convolution_zero_left (p)
  51. 0051specialize prime_field_polynomial_convolution_zero_left (ab)
  52. 0052specialize prime_field_polynomial_convolution_zero_left (ac)
  53. 0053specialize prime_field_polynomial_convolution_zero_left (L)
  54. 0054specialize prime_field_polynomial_convolution_zero_left (BB)
  55. 0055specialize prime_field_polynomial_convolution_zero_left (BC)
  56. 0056specialize prime_field_polynomial_convolution_zero_left (t+M)
  57. 0057specialize prime_field_polynomial_convolution_zero_left (CB)
  58. 0058specialize prime_field_polynomial_convolution_zero_left (CC)
  59. 0059specialize prime_field_polynomial_convolution_zero_left (K)
  60. 0060apply prime_field_polynomial_convolution_zero_left
  61. 0061exact hp
  62. 0062exact hz
  63. 0063exact hn
  64. 0064have hec : forall pfrep_power_empty_first_equivalence_rightleft pfrep_left_empty_first_equivalence_rightleft pfrep_right_empty_first_equivalence_rightleft. ((exists pfrep_position_empty_first_equivalence_rightleftfirst. ((pfrep_position_empty_first_equivalence_rightleftfirst+S (pfrep_power_empty_first_equivalence_rightleft)=(N)) /\ ((((exists ff_h_pfp_empty_first_equivalence_rightleftfirstentry. ff_h_pfp_empty_first_equivalence_rightleftfirstentry + S (pfrep_left_empty_first_equivalence_rightleft) = S ((S (pfrep_position_empty_first_equivalence_rightleftfirst)) * cc)) /\ exists ff_q_pfp_empty_first_equivalence_rightleftfirstentry. cb = ff_q_pfp_empty_first_equivalence_rightleftfirstentry * S ((S (pfrep_position_empty_first_equivalence_rightleftfirst)) * cc) + (pfrep_left_empty_first_equivalence_rightleft)))))) \/ (((exists pfrep_gap_empty_first_equivalence_rightleftfirstoutside. pfrep_gap_empty_first_equivalence_rightleftfirstoutside+(N)=(pfrep_power_empty_first_equivalence_rightleft)) /\ (((pfrep_left_empty_first_equivalence_rightleft)=0))))) -> ((exists pfrep_position_empty_first_equivalence_rightleftsecond. ((pfrep_position_empty_first_equivalence_rightleftsecond+S (pfrep_power_empty_first_equivalence_rightleft)=(0)) /\ ((((exists ff_h_pfp_empty_first_equivalence_rightleftsecondentry. ff_h_pfp_empty_first_equivalence_rightleftsecondentry + S (pfrep_right_empty_first_equivalence_rightleft) = S ((S (pfrep_position_empty_first_equivalence_rightleftsecond)) * 0)) /\ exists ff_q_pfp_empty_first_equivalence_rightleftsecondentry. 0 = ff_q_pfp_empty_first_equivalence_rightleftsecondentry * S ((S (pfrep_position_empty_first_equivalence_rightleftsecond)) * 0) + (pfrep_right_empty_first_equivalence_rightleft)))))) \/ (((exists pfrep_gap_empty_first_equivalence_rightleftsecondoutside. pfrep_gap_empty_first_equivalence_rightleftsecondoutside+(0)=(pfrep_power_empty_first_equivalence_rightleft)) /\ (((pfrep_right_empty_first_equivalence_rightleft)=0))))) -> pfrep_left_empty_first_equivalence_rightleft=pfrep_right_empty_first_equivalence_rightleft
  65. 0065specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  66. 0066specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  67. 0067specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  68. 0068apply prime_field_polynomial_zero_prefix_equivalent_empty
  69. 0069exact hc0
  70. 0070have hen : forall pfrep_power_empty_second_equivalence_rightleft pfrep_left_empty_second_equivalence_rightleft pfrep_right_empty_second_equivalence_rightleft. ((exists pfrep_position_empty_second_equivalence_rightleftfirst. ((pfrep_position_empty_second_equivalence_rightleftfirst+S (pfrep_power_empty_second_equivalence_rightleft)=(K)) /\ ((((exists ff_h_pfp_empty_second_equivalence_rightleftfirstentry. ff_h_pfp_empty_second_equivalence_rightleftfirstentry + S (pfrep_left_empty_second_equivalence_rightleft) = S ((S (pfrep_position_empty_second_equivalence_rightleftfirst)) * CC)) /\ exists ff_q_pfp_empty_second_equivalence_rightleftfirstentry. CB = ff_q_pfp_empty_second_equivalence_rightleftfirstentry * S ((S (pfrep_position_empty_second_equivalence_rightleftfirst)) * CC) + (pfrep_left_empty_second_equivalence_rightleft)))))) \/ (((exists pfrep_gap_empty_second_equivalence_rightleftfirstoutside. pfrep_gap_empty_second_equivalence_rightleftfirstoutside+(K)=(pfrep_power_empty_second_equivalence_rightleft)) /\ (((pfrep_left_empty_second_equivalence_rightleft)=0))))) -> ((exists pfrep_position_empty_second_equivalence_rightleftsecond. ((pfrep_position_empty_second_equivalence_rightleftsecond+S (pfrep_power_empty_second_equivalence_rightleft)=(0)) /\ ((((exists ff_h_pfp_empty_second_equivalence_rightleftsecondentry. ff_h_pfp_empty_second_equivalence_rightleftsecondentry + S (pfrep_right_empty_second_equivalence_rightleft) = S ((S (pfrep_position_empty_second_equivalence_rightleftsecond)) * 0)) /\ exists ff_q_pfp_empty_second_equivalence_rightleftsecondentry. 0 = ff_q_pfp_empty_second_equivalence_rightleftsecondentry * S ((S (pfrep_position_empty_second_equivalence_rightleftsecond)) * 0) + (pfrep_right_empty_second_equivalence_rightleft)))))) \/ (((exists pfrep_gap_empty_second_equivalence_rightleftsecondoutside. pfrep_gap_empty_second_equivalence_rightleftsecondoutside+(0)=(pfrep_power_empty_second_equivalence_rightleft)) /\ (((pfrep_right_empty_second_equivalence_rightleft)=0))))) -> pfrep_left_empty_second_equivalence_rightleft=pfrep_right_empty_second_equivalence_rightleft
  71. 0071specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  72. 0072specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  73. 0073specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  74. 0074apply prime_field_polynomial_zero_prefix_equivalent_empty
  75. 0075exact hn0
  76. 0076specialize prime_field_polynomial_equivalent_transitive (cb)
  77. 0077specialize prime_field_polynomial_equivalent_transitive (cc)
  78. 0078specialize prime_field_polynomial_equivalent_transitive (N)
  79. 0079specialize prime_field_polynomial_equivalent_transitive (0)
  80. 0080specialize prime_field_polynomial_equivalent_transitive (0)
  81. 0081specialize prime_field_polynomial_equivalent_transitive (0)
  82. 0082specialize prime_field_polynomial_equivalent_transitive (CB)
  83. 0083specialize prime_field_polynomial_equivalent_transitive (CC)
  84. 0084specialize prime_field_polynomial_equivalent_transitive (K)
  85. 0085apply prime_field_polynomial_equivalent_transitive
  86. 0086exact hec
  87. 0087specialize prime_field_polynomial_equivalent_symmetric (CB)
  88. 0088specialize prime_field_polynomial_equivalent_symmetric (CC)
  89. 0089specialize prime_field_polynomial_equivalent_symmetric (K)
  90. 0090specialize prime_field_polynomial_equivalent_symmetric (0)
  91. 0091specialize prime_field_polynomial_equivalent_symmetric (0)
  92. 0092specialize prime_field_polynomial_equivalent_symmetric (0)
  93. 0093apply prime_field_polynomial_equivalent_symmetric
  94. 0094exact hen
  95. 0095have hM : M=0 \/ ~(M=0)
  96. 0096specialize eq_decidable (M)
  97. 0097specialize eq_decidable (0)
  98. 0098apply eq_decidable
  99. 0099cases hM
  100. 0100have hz : forall pfp_repeat_index_empty_factor_zero_rightright. (exists pfa_gap_empty_factor_zero_rightrightindex. pfa_gap_empty_factor_zero_rightrightindex + S (pfp_repeat_index_empty_factor_zero_rightright) = (M)) -> (((exists ff_h_pfp_empty_factor_zero_rightrightentry. ff_h_pfp_empty_factor_zero_rightrightentry + S (0) = S ((S (pfp_repeat_index_empty_factor_zero_rightright)) * bc)) /\ exists ff_q_pfp_empty_factor_zero_rightrightentry. bb = ff_q_pfp_empty_factor_zero_rightrightentry * S ((S (pfp_repeat_index_empty_factor_zero_rightright)) * bc) + (0)))
  101. 0101intro j
  102. 0102intro hj
  103. 0103rewrite hM_left at hj
  104. 0104exfalso
  105. 0105specialize matrix_rank_no_index_below_zero (j)
  106. 0106apply matrix_rank_no_index_below_zero
  107. 0107exact hj
  108. 0108have hc0 : forall pfp_repeat_index_empty_original_product_rightright. (exists pfa_gap_empty_original_product_rightrightindex. pfa_gap_empty_original_product_rightrightindex + S (pfp_repeat_index_empty_original_product_rightright) = (N)) -> (((exists ff_h_pfp_empty_original_product_rightrightentry. ff_h_pfp_empty_original_product_rightrightentry + S (0) = S ((S (pfp_repeat_index_empty_original_product_rightright)) * cc)) /\ exists ff_q_pfp_empty_original_product_rightrightentry. cb = ff_q_pfp_empty_original_product_rightrightentry * S ((S (pfp_repeat_index_empty_original_product_rightright)) * cc) + (0)))
  109. 0109specialize prime_field_polynomial_convolution_zero_right (p)
  110. 0110specialize prime_field_polynomial_convolution_zero_right (ab)
  111. 0111specialize prime_field_polynomial_convolution_zero_right (ac)
  112. 0112specialize prime_field_polynomial_convolution_zero_right (L)
  113. 0113specialize prime_field_polynomial_convolution_zero_right (bb)
  114. 0114specialize prime_field_polynomial_convolution_zero_right (bc)
  115. 0115specialize prime_field_polynomial_convolution_zero_right (M)
  116. 0116specialize prime_field_polynomial_convolution_zero_right (cb)
  117. 0117specialize prime_field_polynomial_convolution_zero_right (cc)
  118. 0118specialize prime_field_polynomial_convolution_zero_right (N)
  119. 0119apply prime_field_polynomial_convolution_zero_right
  120. 0120exact hp
  121. 0121exact hz
  122. 0122exact hc
  123. 0123have hn0 : forall pfp_repeat_index_empty_padded_product_rightright. (exists pfa_gap_empty_padded_product_rightrightindex. pfa_gap_empty_padded_product_rightrightindex + S (pfp_repeat_index_empty_padded_product_rightright) = (K)) -> (((exists ff_h_pfp_empty_padded_product_rightrightentry. ff_h_pfp_empty_padded_product_rightrightentry + S (0) = S ((S (pfp_repeat_index_empty_padded_product_rightright)) * CC)) /\ exists ff_q_pfp_empty_padded_product_rightrightentry. CB = ff_q_pfp_empty_padded_product_rightrightentry * S ((S (pfp_repeat_index_empty_padded_product_rightright)) * CC) + (0)))
  124. 0124specialize prime_field_polynomial_convolution_zero_right (p)
  125. 0125specialize prime_field_polynomial_convolution_zero_right (ab)
  126. 0126specialize prime_field_polynomial_convolution_zero_right (ac)
  127. 0127specialize prime_field_polynomial_convolution_zero_right (L)
  128. 0128specialize prime_field_polynomial_convolution_zero_right (BB)
  129. 0129specialize prime_field_polynomial_convolution_zero_right (BC)
  130. 0130specialize prime_field_polynomial_convolution_zero_right (t+M)
  131. 0131specialize prime_field_polynomial_convolution_zero_right (CB)
  132. 0132specialize prime_field_polynomial_convolution_zero_right (CC)
  133. 0133specialize prime_field_polynomial_convolution_zero_right (K)
  134. 0134apply prime_field_polynomial_convolution_zero_right
  135. 0135exact hp
  136. 0136specialize polynomial_left_pad_zero_prefix (bb)
  137. 0137specialize polynomial_left_pad_zero_prefix (bc)
  138. 0138specialize polynomial_left_pad_zero_prefix (M)
  139. 0139specialize polynomial_left_pad_zero_prefix (t)
  140. 0140specialize polynomial_left_pad_zero_prefix (BB)
  141. 0141specialize polynomial_left_pad_zero_prefix (BC)
  142. 0142apply polynomial_left_pad_zero_prefix
  143. 0143exact hz
  144. 0144exact hpad
  145. 0145exact hn
  146. 0146have hec : forall pfrep_power_empty_first_equivalence_rightright pfrep_left_empty_first_equivalence_rightright pfrep_right_empty_first_equivalence_rightright. ((exists pfrep_position_empty_first_equivalence_rightrightfirst. ((pfrep_position_empty_first_equivalence_rightrightfirst+S (pfrep_power_empty_first_equivalence_rightright)=(N)) /\ ((((exists ff_h_pfp_empty_first_equivalence_rightrightfirstentry. ff_h_pfp_empty_first_equivalence_rightrightfirstentry + S (pfrep_left_empty_first_equivalence_rightright) = S ((S (pfrep_position_empty_first_equivalence_rightrightfirst)) * cc)) /\ exists ff_q_pfp_empty_first_equivalence_rightrightfirstentry. cb = ff_q_pfp_empty_first_equivalence_rightrightfirstentry * S ((S (pfrep_position_empty_first_equivalence_rightrightfirst)) * cc) + (pfrep_left_empty_first_equivalence_rightright)))))) \/ (((exists pfrep_gap_empty_first_equivalence_rightrightfirstoutside. pfrep_gap_empty_first_equivalence_rightrightfirstoutside+(N)=(pfrep_power_empty_first_equivalence_rightright)) /\ (((pfrep_left_empty_first_equivalence_rightright)=0))))) -> ((exists pfrep_position_empty_first_equivalence_rightrightsecond. ((pfrep_position_empty_first_equivalence_rightrightsecond+S (pfrep_power_empty_first_equivalence_rightright)=(0)) /\ ((((exists ff_h_pfp_empty_first_equivalence_rightrightsecondentry. ff_h_pfp_empty_first_equivalence_rightrightsecondentry + S (pfrep_right_empty_first_equivalence_rightright) = S ((S (pfrep_position_empty_first_equivalence_rightrightsecond)) * 0)) /\ exists ff_q_pfp_empty_first_equivalence_rightrightsecondentry. 0 = ff_q_pfp_empty_first_equivalence_rightrightsecondentry * S ((S (pfrep_position_empty_first_equivalence_rightrightsecond)) * 0) + (pfrep_right_empty_first_equivalence_rightright)))))) \/ (((exists pfrep_gap_empty_first_equivalence_rightrightsecondoutside. pfrep_gap_empty_first_equivalence_rightrightsecondoutside+(0)=(pfrep_power_empty_first_equivalence_rightright)) /\ (((pfrep_right_empty_first_equivalence_rightright)=0))))) -> pfrep_left_empty_first_equivalence_rightright=pfrep_right_empty_first_equivalence_rightright
  147. 0147specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  148. 0148specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  149. 0149specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  150. 0150apply prime_field_polynomial_zero_prefix_equivalent_empty
  151. 0151exact hc0
  152. 0152have hen : forall pfrep_power_empty_second_equivalence_rightright pfrep_left_empty_second_equivalence_rightright pfrep_right_empty_second_equivalence_rightright. ((exists pfrep_position_empty_second_equivalence_rightrightfirst. ((pfrep_position_empty_second_equivalence_rightrightfirst+S (pfrep_power_empty_second_equivalence_rightright)=(K)) /\ ((((exists ff_h_pfp_empty_second_equivalence_rightrightfirstentry. ff_h_pfp_empty_second_equivalence_rightrightfirstentry + S (pfrep_left_empty_second_equivalence_rightright) = S ((S (pfrep_position_empty_second_equivalence_rightrightfirst)) * CC)) /\ exists ff_q_pfp_empty_second_equivalence_rightrightfirstentry. CB = ff_q_pfp_empty_second_equivalence_rightrightfirstentry * S ((S (pfrep_position_empty_second_equivalence_rightrightfirst)) * CC) + (pfrep_left_empty_second_equivalence_rightright)))))) \/ (((exists pfrep_gap_empty_second_equivalence_rightrightfirstoutside. pfrep_gap_empty_second_equivalence_rightrightfirstoutside+(K)=(pfrep_power_empty_second_equivalence_rightright)) /\ (((pfrep_left_empty_second_equivalence_rightright)=0))))) -> ((exists pfrep_position_empty_second_equivalence_rightrightsecond. ((pfrep_position_empty_second_equivalence_rightrightsecond+S (pfrep_power_empty_second_equivalence_rightright)=(0)) /\ ((((exists ff_h_pfp_empty_second_equivalence_rightrightsecondentry. ff_h_pfp_empty_second_equivalence_rightrightsecondentry + S (pfrep_right_empty_second_equivalence_rightright) = S ((S (pfrep_position_empty_second_equivalence_rightrightsecond)) * 0)) /\ exists ff_q_pfp_empty_second_equivalence_rightrightsecondentry. 0 = ff_q_pfp_empty_second_equivalence_rightrightsecondentry * S ((S (pfrep_position_empty_second_equivalence_rightrightsecond)) * 0) + (pfrep_right_empty_second_equivalence_rightright)))))) \/ (((exists pfrep_gap_empty_second_equivalence_rightrightsecondoutside. pfrep_gap_empty_second_equivalence_rightrightsecondoutside+(0)=(pfrep_power_empty_second_equivalence_rightright)) /\ (((pfrep_right_empty_second_equivalence_rightright)=0))))) -> pfrep_left_empty_second_equivalence_rightright=pfrep_right_empty_second_equivalence_rightright
  153. 0153specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  154. 0154specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  155. 0155specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  156. 0156apply prime_field_polynomial_zero_prefix_equivalent_empty
  157. 0157exact hn0
  158. 0158specialize prime_field_polynomial_equivalent_transitive (cb)
  159. 0159specialize prime_field_polynomial_equivalent_transitive (cc)
  160. 0160specialize prime_field_polynomial_equivalent_transitive (N)
  161. 0161specialize prime_field_polynomial_equivalent_transitive (0)
  162. 0162specialize prime_field_polynomial_equivalent_transitive (0)
  163. 0163specialize prime_field_polynomial_equivalent_transitive (0)
  164. 0164specialize prime_field_polynomial_equivalent_transitive (CB)
  165. 0165specialize prime_field_polynomial_equivalent_transitive (CC)
  166. 0166specialize prime_field_polynomial_equivalent_transitive (K)
  167. 0167apply prime_field_polynomial_equivalent_transitive
  168. 0168exact hec
  169. 0169specialize prime_field_polynomial_equivalent_symmetric (CB)
  170. 0170specialize prime_field_polynomial_equivalent_symmetric (CC)
  171. 0171specialize prime_field_polynomial_equivalent_symmetric (K)
  172. 0172specialize prime_field_polynomial_equivalent_symmetric (0)
  173. 0173specialize prime_field_polynomial_equivalent_symmetric (0)
  174. 0174specialize prime_field_polynomial_equivalent_symmetric (0)
  175. 0175apply prime_field_polynomial_equivalent_symmetric
  176. 0176exact hen
  177. 0177have hd : ((K=t+N) /\ ((((forall pfp_repeat_index_product_equivalent_padding_rightzeros. (exists pfa_gap_product_equivalent_padding_rightzerosindex. pfa_gap_product_equivalent_padding_rightzerosindex + S (pfp_repeat_index_product_equivalent_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_product_equivalent_padding_rightzerosentry. ff_h_pfp_product_equivalent_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_product_equivalent_padding_rightzeros)) * CC)) /\ exists ff_q_pfp_product_equivalent_padding_rightzerosentry. CB = ff_q_pfp_product_equivalent_padding_rightzerosentry * S ((S (pfp_repeat_index_product_equivalent_padding_rightzeros)) * CC) + (0)))) /\ ((forall pfrep_index_product_equivalent_padding_right pfrep_value_product_equivalent_padding_right. (exists pfa_gap_product_equivalent_padding_rightbound. pfa_gap_product_equivalent_padding_rightbound + S (pfrep_index_product_equivalent_padding_right) = (N)) -> (((exists ff_h_pfp_product_equivalent_padding_rightinput. ff_h_pfp_product_equivalent_padding_rightinput + S (pfrep_value_product_equivalent_padding_right) = S ((S (pfrep_index_product_equivalent_padding_right)) * cc)) /\ exists ff_q_pfp_product_equivalent_padding_rightinput. cb = ff_q_pfp_product_equivalent_padding_rightinput * S ((S (pfrep_index_product_equivalent_padding_right)) * cc) + (pfrep_value_product_equivalent_padding_right))) -> (((exists ff_h_pfp_product_equivalent_padding_rightoutput. ff_h_pfp_product_equivalent_padding_rightoutput + S (pfrep_value_product_equivalent_padding_right) = S ((S ((t)+pfrep_index_product_equivalent_padding_right)) * CC)) /\ exists ff_q_pfp_product_equivalent_padding_rightoutput. CB = ff_q_pfp_product_equivalent_padding_rightoutput * S ((S ((t)+pfrep_index_product_equivalent_padding_right)) * CC) + (pfrep_value_product_equivalent_padding_right)))))))))
  178. 0178specialize prime_field_polynomial_convolution_left_padding_nonempty_right (p)
  179. 0179specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ab)
  180. 0180specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ac)
  181. 0181specialize prime_field_polynomial_convolution_left_padding_nonempty_right (L)
  182. 0182specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bb)
  183. 0183specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bc)
  184. 0184specialize prime_field_polynomial_convolution_left_padding_nonempty_right (M)
  185. 0185specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cb)
  186. 0186specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cc)
  187. 0187specialize prime_field_polynomial_convolution_left_padding_nonempty_right (N)
  188. 0188specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BB)
  189. 0189specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BC)
  190. 0190specialize prime_field_polynomial_convolution_left_padding_nonempty_right (t)
  191. 0191specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CB)
  192. 0192specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CC)
  193. 0193specialize prime_field_polynomial_convolution_left_padding_nonempty_right (K)
  194. 0194apply prime_field_polynomial_convolution_left_padding_nonempty_right
  195. 0195exact hp
  196. 0196exact hL_right
  197. 0197exact hM_right
  198. 0198exact hpad
  199. 0199exact hc
  200. 0200exact hn
  201. 0201cases hd
  202. 0202rewrite hd_left
  203. 0203rewrite hd_left
  204. 0204specialize prime_field_polynomial_left_pad_equivalent (cb)
  205. 0205specialize prime_field_polynomial_left_pad_equivalent (cc)
  206. 0206specialize prime_field_polynomial_left_pad_equivalent (N)
  207. 0207specialize prime_field_polynomial_left_pad_equivalent (t)
  208. 0208specialize prime_field_polynomial_left_pad_equivalent (CB)
  209. 0209specialize prime_field_polynomial_left_pad_equivalent (CC)
  210. 0210apply prime_field_polynomial_left_pad_equivalent
  211. 0211exact hd_right