PG000D

prime_field_polynomial_convolution_shift_right_exists

Given a genuine shifted factor, construct its proper-length product and a genuine shift of the original output, then derive their formal equivalence without any output witness premise.

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

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

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ cb. ∀ cc. ∀ N. ∀ BB. ∀ BC. Prime(p) → PolynomialShift(bb,bc,M,BB,BC) → FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. FpPolyProduct(p,ab,ac,L,BB,BC,S M,y,z,x) ∧ (PolynomialShift(cb,cc,N,n,m) ∧ PolynomialEquivalent(y,z,x,n,m,S N))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

PolynomialProductLength(L,M,N) · 1FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 4PolynomialEquivalent(b,c,L,d,e,M) · 1PolynomialShift(b,c,L,d,e) · 3Prime(p) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisitepolynomial_product_length_exists · checked external prerequisiteprime_field_polynomial_convolution_at_length_exists · checked external prerequisiteprime_field_polynomial_shift_boundedprime_field_polynomial_shift_existsprime_field_polynomial_convolution_shift_right_equivalent
Original expanded first-order statement 
forall p ab ac L bb bc M cb cc N BB BC. (~((p) = 1) /\ forall pfa_factor_left_shift_exists_product_prime pfa_factor_right_shift_exists_product_prime. (p) = pfa_factor_left_shift_exists_product_prime * pfa_factor_right_shift_exists_product_prime -> pfa_factor_left_shift_exists_product_prime = 1 \/ pfa_factor_right_shift_exists_product_prime = 1) -> (((forall mdr_i_pfp_shift_exists_product_factorprefix mdr_a_pfp_shift_exists_product_factorprefix. (exists mdr_gap_pfp_shift_exists_product_factorprefixb. mdr_gap_pfp_shift_exists_product_factorprefixb + S (mdr_i_pfp_shift_exists_product_factorprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_exists_product_factorprefixo. ff_h_mdr_pfp_shift_exists_product_factorprefixo + S (mdr_a_pfp_shift_exists_product_factorprefix) = S ((S (mdr_i_pfp_shift_exists_product_factorprefix)) * bc)) /\ exists ff_q_mdr_pfp_shift_exists_product_factorprefixo. bb = ff_q_mdr_pfp_shift_exists_product_factorprefixo * S ((S (mdr_i_pfp_shift_exists_product_factorprefix)) * bc) + (mdr_a_pfp_shift_exists_product_factorprefix))) -> (((exists ff_h_mdr_pfp_shift_exists_product_factorprefixn. ff_h_mdr_pfp_shift_exists_product_factorprefixn + S (mdr_a_pfp_shift_exists_product_factorprefix) = S ((S (mdr_i_pfp_shift_exists_product_factorprefix)) * BC)) /\ exists ff_q_mdr_pfp_shift_exists_product_factorprefixn. BB = ff_q_mdr_pfp_shift_exists_product_factorprefixn * S ((S (mdr_i_pfp_shift_exists_product_factorprefix)) * BC) + (mdr_a_pfp_shift_exists_product_factorprefix)))) /\ ((((exists ff_h_pfp_shift_exists_product_factorlast. ff_h_pfp_shift_exists_product_factorlast + S (0) = S ((S (M)) * BC)) /\ exists ff_q_pfp_shift_exists_product_factorlast. BB = ff_q_pfp_shift_exists_product_factorlast * S ((S (M)) * BC) + (0)))))) -> (((forall fom_index_pfp_shift_exists_product_oldleft. (exists fom_gap_pfp_shift_exists_product_oldleft_index_bound. fom_gap_pfp_shift_exists_product_oldleft_index_bound + S (fom_index_pfp_shift_exists_product_oldleft) = L) -> exists fom_value_pfp_shift_exists_product_oldleft. ((((exists fom_beta_height_pfp_shift_exists_product_oldleft_entry. fom_beta_height_pfp_shift_exists_product_oldleft_entry + S (fom_value_pfp_shift_exists_product_oldleft) = S ((S (fom_index_pfp_shift_exists_product_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_exists_product_oldleft_entry. ab = fom_beta_quotient_pfp_shift_exists_product_oldleft_entry * S ((S (fom_index_pfp_shift_exists_product_oldleft)) * ac) + (fom_value_pfp_shift_exists_product_oldleft))) /\ (exists fom_gap_pfp_shift_exists_product_oldleft_value_bound. fom_gap_pfp_shift_exists_product_oldleft_value_bound + S (fom_value_pfp_shift_exists_product_oldleft) = p))) /\ (((forall fom_index_pfp_shift_exists_product_oldright. (exists fom_gap_pfp_shift_exists_product_oldright_index_bound. fom_gap_pfp_shift_exists_product_oldright_index_bound + S (fom_index_pfp_shift_exists_product_oldright) = M) -> exists fom_value_pfp_shift_exists_product_oldright. ((((exists fom_beta_height_pfp_shift_exists_product_oldright_entry. fom_beta_height_pfp_shift_exists_product_oldright_entry + S (fom_value_pfp_shift_exists_product_oldright) = S ((S (fom_index_pfp_shift_exists_product_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_shift_exists_product_oldright_entry. bb = fom_beta_quotient_pfp_shift_exists_product_oldright_entry * S ((S (fom_index_pfp_shift_exists_product_oldright)) * bc) + (fom_value_pfp_shift_exists_product_oldright))) /\ (exists fom_gap_pfp_shift_exists_product_oldright_value_bound. fom_gap_pfp_shift_exists_product_oldright_value_bound + S (fom_value_pfp_shift_exists_product_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_shift_exists_product_oldcoefficients. (exists pfa_gap_shift_exists_product_oldcoefficientsbound. pfa_gap_shift_exists_product_oldcoefficientsbound + S (pfc_index_shift_exists_product_oldcoefficients) = (N)) -> exists pfc_value_shift_exists_product_oldcoefficients. ((((exists ff_h_pfp_shift_exists_product_oldcoefficientsentry. ff_h_pfp_shift_exists_product_oldcoefficientsentry + S (pfc_value_shift_exists_product_oldcoefficients) = S ((S (pfc_index_shift_exists_product_oldcoefficients)) * cc)) /\ exists ff_q_pfp_shift_exists_product_oldcoefficientsentry. cb = ff_q_pfp_shift_exists_product_oldcoefficientsentry * S ((S (pfc_index_shift_exists_product_oldcoefficients)) * cc) + (pfc_value_shift_exists_product_oldcoefficients))) /\ ((exists pfc_terms_code_shift_exists_product_oldcoefficientscoefficient pfc_terms_scale_shift_exists_product_oldcoefficientscoefficient pfc_natural_sum_shift_exists_product_oldcoefficientscoefficient. ((forall pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal. (exists pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonalbound. pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonalbound + S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal) = (S (pfc_index_shift_exists_product_oldcoefficients))) -> exists pfc_value_shift_exists_product_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonalentry + S (pfc_value_shift_exists_product_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_exists_product_oldcoefficientscoefficient)) /\ exists ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_exists_product_oldcoefficientscoefficient = ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_exists_product_oldcoefficientscoefficient) + (pfc_value_shift_exists_product_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm pfc_left_shift_exists_product_oldcoefficientscoefficientdiagonalterm pfc_right_shift_exists_product_oldcoefficientscoefficientdiagonalterm. (((pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)+pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm=(pfc_index_shift_exists_product_oldcoefficients)) /\ ((((((exists pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_exists_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_exists_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_exists_product_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_exists_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_exists_product_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_shift_exists_product_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_exists_product_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_shift_exists_product_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_exists_product_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_exists_product_oldcoefficientscoefficientdiagonal)=pfc_left_shift_exists_product_oldcoefficientscoefficientdiagonalterm*pfc_right_shift_exists_product_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_exists_product_oldcoefficientscoefficientsum fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_start. fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_start. fs_u_pfc_shift_exists_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_exists_product_oldcoefficientscoefficient) = S ((S (S (pfc_index_shift_exists_product_oldcoefficients))) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_exists_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_exists_product_oldcoefficients))) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum) + (pfc_natural_sum_shift_exists_product_oldcoefficientscoefficient))) /\ forall fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps = S (pfc_index_shift_exists_product_oldcoefficients)) -> exists fs_a_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps fs_r_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps fs_s_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_exists_product_oldcoefficientscoefficient)) /\ exists fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_exists_product_oldcoefficientscoefficient = fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_exists_product_oldcoefficientscoefficient) + (fs_a_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_exists_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum) + (fs_r_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_exists_product_oldcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_oldcoefficientscoefficientsum) + (fs_s_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_exists_product_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_exists_product_oldcoefficientscoefficientresiduebound. pfa_gap_shift_exists_product_oldcoefficientscoefficientresiduebound + S (pfc_value_shift_exists_product_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_exists_product_oldcoefficientscoefficientresiduecongruence pfa_offset_right_shift_exists_product_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_exists_product_oldcoefficientscoefficient) + (p) * pfa_offset_left_shift_exists_product_oldcoefficientscoefficientresiduecongruence = (pfc_value_shift_exists_product_oldcoefficients) + (p) * pfa_offset_right_shift_exists_product_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (exists K db dc eb ec. ((((forall fom_index_pfp_shift_exists_product_newleft. (exists fom_gap_pfp_shift_exists_product_newleft_index_bound. fom_gap_pfp_shift_exists_product_newleft_index_bound + S (fom_index_pfp_shift_exists_product_newleft) = L) -> exists fom_value_pfp_shift_exists_product_newleft. ((((exists fom_beta_height_pfp_shift_exists_product_newleft_entry. fom_beta_height_pfp_shift_exists_product_newleft_entry + S (fom_value_pfp_shift_exists_product_newleft) = S ((S (fom_index_pfp_shift_exists_product_newleft)) * ac)) /\ exists fom_beta_quotient_pfp_shift_exists_product_newleft_entry. ab = fom_beta_quotient_pfp_shift_exists_product_newleft_entry * S ((S (fom_index_pfp_shift_exists_product_newleft)) * ac) + (fom_value_pfp_shift_exists_product_newleft))) /\ (exists fom_gap_pfp_shift_exists_product_newleft_value_bound. fom_gap_pfp_shift_exists_product_newleft_value_bound + S (fom_value_pfp_shift_exists_product_newleft) = p))) /\ (((forall fom_index_pfp_shift_exists_product_newright. (exists fom_gap_pfp_shift_exists_product_newright_index_bound. fom_gap_pfp_shift_exists_product_newright_index_bound + S (fom_index_pfp_shift_exists_product_newright) = S M) -> exists fom_value_pfp_shift_exists_product_newright. ((((exists fom_beta_height_pfp_shift_exists_product_newright_entry. fom_beta_height_pfp_shift_exists_product_newright_entry + S (fom_value_pfp_shift_exists_product_newright) = S ((S (fom_index_pfp_shift_exists_product_newright)) * BC)) /\ exists fom_beta_quotient_pfp_shift_exists_product_newright_entry. BB = fom_beta_quotient_pfp_shift_exists_product_newright_entry * S ((S (fom_index_pfp_shift_exists_product_newright)) * BC) + (fom_value_pfp_shift_exists_product_newright))) /\ (exists fom_gap_pfp_shift_exists_product_newright_value_bound. fom_gap_pfp_shift_exists_product_newright_value_bound + S (fom_value_pfp_shift_exists_product_newright) = p))) /\ (((((((L)=0 \/ (S M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((S M)=0)) /\ (((L)+(S M)=S (K)))))))) /\ ((forall pfc_index_shift_exists_product_newcoefficients. (exists pfa_gap_shift_exists_product_newcoefficientsbound. pfa_gap_shift_exists_product_newcoefficientsbound + S (pfc_index_shift_exists_product_newcoefficients) = (K)) -> exists pfc_value_shift_exists_product_newcoefficients. ((((exists ff_h_pfp_shift_exists_product_newcoefficientsentry. ff_h_pfp_shift_exists_product_newcoefficientsentry + S (pfc_value_shift_exists_product_newcoefficients) = S ((S (pfc_index_shift_exists_product_newcoefficients)) * dc)) /\ exists ff_q_pfp_shift_exists_product_newcoefficientsentry. db = ff_q_pfp_shift_exists_product_newcoefficientsentry * S ((S (pfc_index_shift_exists_product_newcoefficients)) * dc) + (pfc_value_shift_exists_product_newcoefficients))) /\ ((exists pfc_terms_code_shift_exists_product_newcoefficientscoefficient pfc_terms_scale_shift_exists_product_newcoefficientscoefficient pfc_natural_sum_shift_exists_product_newcoefficientscoefficient. ((forall pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal. (exists pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonalbound. pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonalbound + S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal) = (S (pfc_index_shift_exists_product_newcoefficients))) -> exists pfc_value_shift_exists_product_newcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonalentry. ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonalentry + S (pfc_value_shift_exists_product_newcoefficientscoefficientdiagonal) = S ((S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_exists_product_newcoefficientscoefficient)) /\ exists ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonalentry. pfc_terms_code_shift_exists_product_newcoefficientscoefficient = ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonalentry * S ((S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)) * pfc_terms_scale_shift_exists_product_newcoefficientscoefficient) + (pfc_value_shift_exists_product_newcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm pfc_left_shift_exists_product_newcoefficientscoefficientdiagonalterm pfc_right_shift_exists_product_newcoefficientscoefficientdiagonalterm. (((pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)+pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm=(pfc_index_shift_exists_product_newcoefficients)) /\ ((((((exists pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermleftinside. pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_shift_exists_product_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)) * ac) + (pfc_left_shift_exists_product_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_shift_exists_product_newcoefficientscoefficientdiagonal)) /\ (((pfc_left_shift_exists_product_newcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermrightinside. pfa_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm) = (S M)) /\ ((((exists ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_shift_exists_product_newcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_shift_exists_product_newcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_shift_exists_product_newcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_shift_exists_product_newcoefficientscoefficientdiagonaltermrightoutside+(S M)=(pfc_complement_shift_exists_product_newcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_shift_exists_product_newcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_shift_exists_product_newcoefficientscoefficientdiagonal)=pfc_left_shift_exists_product_newcoefficientscoefficientdiagonalterm*pfc_right_shift_exists_product_newcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_shift_exists_product_newcoefficientscoefficientsum fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum. ((((exists fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_start. fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_start. fs_u_pfc_shift_exists_product_newcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_terminal. fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_shift_exists_product_newcoefficientscoefficient) = S ((S (S (pfc_index_shift_exists_product_newcoefficients))) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_terminal. fs_u_pfc_shift_exists_product_newcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_shift_exists_product_newcoefficients))) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum) + (pfc_natural_sum_shift_exists_product_newcoefficientscoefficient))) /\ forall fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps = S (pfc_index_shift_exists_product_newcoefficients)) -> exists fs_a_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps fs_r_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps fs_s_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_exists_product_newcoefficientscoefficient)) /\ exists fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_shift_exists_product_newcoefficientscoefficient = fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_shift_exists_product_newcoefficientscoefficient) + (fs_a_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_shift_exists_product_newcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum) + (fs_r_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum)) /\ exists fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_shift_exists_product_newcoefficientscoefficientsum = fs_q_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)) * fs_v_pfc_shift_exists_product_newcoefficientscoefficientsum) + (fs_s_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps = fs_r_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps + fs_a_pfc_shift_exists_product_newcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_shift_exists_product_newcoefficientscoefficientresiduebound. pfa_gap_shift_exists_product_newcoefficientscoefficientresiduebound + S (pfc_value_shift_exists_product_newcoefficients) = (p)) /\ ((exists pfa_offset_left_shift_exists_product_newcoefficientscoefficientresiduecongruence pfa_offset_right_shift_exists_product_newcoefficientscoefficientresiduecongruence. (pfc_natural_sum_shift_exists_product_newcoefficientscoefficient) + (p) * pfa_offset_left_shift_exists_product_newcoefficientscoefficientresiduecongruence = (pfc_value_shift_exists_product_newcoefficients) + (p) * pfa_offset_right_shift_exists_product_newcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((((forall mdr_i_pfp_shift_exists_product_shiftprefix mdr_a_pfp_shift_exists_product_shiftprefix. (exists mdr_gap_pfp_shift_exists_product_shiftprefixb. mdr_gap_pfp_shift_exists_product_shiftprefixb + S (mdr_i_pfp_shift_exists_product_shiftprefix) = (N)) -> (((exists ff_h_mdr_pfp_shift_exists_product_shiftprefixo. ff_h_mdr_pfp_shift_exists_product_shiftprefixo + S (mdr_a_pfp_shift_exists_product_shiftprefix) = S ((S (mdr_i_pfp_shift_exists_product_shiftprefix)) * cc)) /\ exists ff_q_mdr_pfp_shift_exists_product_shiftprefixo. cb = ff_q_mdr_pfp_shift_exists_product_shiftprefixo * S ((S (mdr_i_pfp_shift_exists_product_shiftprefix)) * cc) + (mdr_a_pfp_shift_exists_product_shiftprefix))) -> (((exists ff_h_mdr_pfp_shift_exists_product_shiftprefixn. ff_h_mdr_pfp_shift_exists_product_shiftprefixn + S (mdr_a_pfp_shift_exists_product_shiftprefix) = S ((S (mdr_i_pfp_shift_exists_product_shiftprefix)) * ec)) /\ exists ff_q_mdr_pfp_shift_exists_product_shiftprefixn. eb = ff_q_mdr_pfp_shift_exists_product_shiftprefixn * S ((S (mdr_i_pfp_shift_exists_product_shiftprefix)) * ec) + (mdr_a_pfp_shift_exists_product_shiftprefix)))) /\ ((((exists ff_h_pfp_shift_exists_product_shiftlast. ff_h_pfp_shift_exists_product_shiftlast + S (0) = S ((S (N)) * ec)) /\ exists ff_q_pfp_shift_exists_product_shiftlast. eb = ff_q_pfp_shift_exists_product_shiftlast * S ((S (N)) * ec) + (0)))))) /\ ((forall pfrep_power_shift_exists_product_equivalence pfrep_left_shift_exists_product_equivalence pfrep_right_shift_exists_product_equivalence. ((exists pfrep_position_shift_exists_product_equivalencefirst. ((pfrep_position_shift_exists_product_equivalencefirst+S (pfrep_power_shift_exists_product_equivalence)=(K)) /\ ((((exists ff_h_pfp_shift_exists_product_equivalencefirstentry. ff_h_pfp_shift_exists_product_equivalencefirstentry + S (pfrep_left_shift_exists_product_equivalence) = S ((S (pfrep_position_shift_exists_product_equivalencefirst)) * dc)) /\ exists ff_q_pfp_shift_exists_product_equivalencefirstentry. db = ff_q_pfp_shift_exists_product_equivalencefirstentry * S ((S (pfrep_position_shift_exists_product_equivalencefirst)) * dc) + (pfrep_left_shift_exists_product_equivalence)))))) \/ (((exists pfrep_gap_shift_exists_product_equivalencefirstoutside. pfrep_gap_shift_exists_product_equivalencefirstoutside+(K)=(pfrep_power_shift_exists_product_equivalence)) /\ (((pfrep_left_shift_exists_product_equivalence)=0))))) -> ((exists pfrep_position_shift_exists_product_equivalencesecond. ((pfrep_position_shift_exists_product_equivalencesecond+S (pfrep_power_shift_exists_product_equivalence)=(S N)) /\ ((((exists ff_h_pfp_shift_exists_product_equivalencesecondentry. ff_h_pfp_shift_exists_product_equivalencesecondentry + S (pfrep_right_shift_exists_product_equivalence) = S ((S (pfrep_position_shift_exists_product_equivalencesecond)) * ec)) /\ exists ff_q_pfp_shift_exists_product_equivalencesecondentry. eb = ff_q_pfp_shift_exists_product_equivalencesecondentry * S ((S (pfrep_position_shift_exists_product_equivalencesecond)) * ec) + (pfrep_right_shift_exists_product_equivalence)))))) \/ (((exists pfrep_gap_shift_exists_product_equivalencesecondoutside. pfrep_gap_shift_exists_product_equivalencesecondoutside+(S N)=(pfrep_power_shift_exists_product_equivalence)) /\ (((pfrep_right_shift_exists_product_equivalence)=0))))) -> pfrep_left_shift_exists_product_equivalence=pfrep_right_shift_exists_product_equivalence))))))

Complete tactic proof in conservative notation

All 95 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

95 script commands · 20 reading checkpoints · 5 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (3)
prime field polynomial shift boundedprime field polynomial shift existsprime field polynomial convolution shift right equivalent
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–15

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

  1. L11
    intro BB
  2. L12
    intro BC
  3. L13
    intro hprime
  4. L14
    intro hs
  5. L15
    intro hc
03Establish hcopyL16–17

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

  1. L16
    have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Definitions: FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)Original native command in the exact edition
  2. L17
    exact hc
04Separate the logical casesL18–20

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

  1. L18
    cases hcopy
  2. L19
    cases hcopy_right
  3. L20
    cases hcopy_right_right
05Establish hpL21–26

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

  1. L21
    have hp : ~(p=0)
  2. L22
    intro hz
  3. L23
    specialize prime_nonzero (p)
  4. L24
    apply prime_nonzero
  5. L25
    exact hprime
  6. L26
    exact hz
06Establish hlengthL27–30

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

  1. L27
    have hlength : ∃ K. PolynomialProductLength(L,S M,K)Definitions: PolynomialProductLength(L,S M,K)Original native command in the exact edition
  2. L28
    specialize polynomial_product_length_exists (L)
  3. L29
    specialize polynomial_product_length_exists (S M)
  4. L30
    apply polynomial_product_length_exists
07Separate the logical casesL31–31

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

  1. L31
    cases hlength
08Establish hvL32–41

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

  1. L32
    have hv : ∃ d. ∃ e. FpPolyProduct(p,ab,ac,L,BB,BC,S M,d,e,x)Definitions: FpPolyProduct(p,ab,ac,L,BB,BC,S M,d,e,x)Original native command in the exact edition
  2. L33
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L34
    specialize prime_field_polynomial_convolution_at_length_exists (ab)
  4. L35
    specialize prime_field_polynomial_convolution_at_length_exists (ac)
  5. L36
    specialize prime_field_polynomial_convolution_at_length_exists (L)
  6. L37
    specialize prime_field_polynomial_convolution_at_length_exists (BB)
  7. L38
    specialize prime_field_polynomial_convolution_at_length_exists (BC)
  8. L39
    specialize prime_field_polynomial_convolution_at_length_exists (S M)
  9. L40
    specialize prime_field_polynomial_convolution_at_length_exists (x)
  10. L41
    apply prime_field_polynomial_convolution_at_length_exists
09Use earlier factsL42–51

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

  1. L42
    exact hp
  2. L43
    exact hcopy_left
  3. L44
    specialize prime_field_polynomial_shift_bounded (p)
  4. L45
    specialize prime_field_polynomial_shift_bounded (bb)
  5. L46
    specialize prime_field_polynomial_shift_bounded (bc)
  6. L47
    specialize prime_field_polynomial_shift_bounded (M)
  7. L48
    specialize prime_field_polynomial_shift_bounded (BB)
  8. L49
    specialize prime_field_polynomial_shift_bounded (BC)
  9. L50
    apply prime_field_polynomial_shift_bounded
  10. L51
    exact hprime
10Use earlier factsL52–54

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

  1. L52
    exact hcopy_right_left
  2. L53
    exact hs
  3. L54
    exact hlength_witness
11Separate the logical casesL55–56

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

  1. L55
    cases hv
  2. L56
    cases hv_witness
12Establish heL57–61

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

  1. L57
    have he : ∃ e. ∃ f. PolynomialShift(cb,cc,N,e,f)Definitions: PolynomialShift(cb,cc,N,e,f)Original native command in the exact edition
  2. L58
    specialize prime_field_polynomial_shift_exists (cb)
  3. L59
    specialize prime_field_polynomial_shift_exists (cc)
  4. L60
    specialize prime_field_polynomial_shift_exists (N)
  5. L61
    apply prime_field_polynomial_shift_exists
13Separate the logical casesL62–63

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

  1. L62
    cases he
  2. L63
    cases he_witness
14Construct an explicit witnessL64–68

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

  1. L64
    exists x
  2. L65
    exists x1
  3. L66
    exists x2
  4. L67
    exists x3
  5. L68
    exists x4
15Separate the logical casesL69–69

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

  1. L69
    split
16Use earlier factsL70–70

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

  1. L70
    exact hv_witness_witness
17Separate the logical casesL71–71

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

  1. L71
    split
18Use earlier factsL72–81

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

  1. L72
    exact he_witness_witness
  2. L73
    specialize prime_field_polynomial_convolution_shift_right_equivalent (p)
  3. L74
    specialize prime_field_polynomial_convolution_shift_right_equivalent (ab)
  4. L75
    specialize prime_field_polynomial_convolution_shift_right_equivalent (ac)
  5. L76
    specialize prime_field_polynomial_convolution_shift_right_equivalent (L)
  6. L77
    specialize prime_field_polynomial_convolution_shift_right_equivalent (bb)
  7. L78
    specialize prime_field_polynomial_convolution_shift_right_equivalent (bc)
  8. L79
    specialize prime_field_polynomial_convolution_shift_right_equivalent (M)
  9. L80
    specialize prime_field_polynomial_convolution_shift_right_equivalent (cb)
  10. L81
    specialize prime_field_polynomial_convolution_shift_right_equivalent (cc)
19Use earlier factsL82–91

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

  1. L82
    specialize prime_field_polynomial_convolution_shift_right_equivalent (N)
  2. L83
    specialize prime_field_polynomial_convolution_shift_right_equivalent (BB)
  3. L84
    specialize prime_field_polynomial_convolution_shift_right_equivalent (BC)
  4. L85
    specialize prime_field_polynomial_convolution_shift_right_equivalent (x1)
  5. L86
    specialize prime_field_polynomial_convolution_shift_right_equivalent (x2)
  6. L87
    specialize prime_field_polynomial_convolution_shift_right_equivalent (x)
  7. L88
    specialize prime_field_polynomial_convolution_shift_right_equivalent (x3)
  8. L89
    specialize prime_field_polynomial_convolution_shift_right_equivalent (x4)
  9. L90
    apply prime_field_polynomial_convolution_shift_right_equivalent
  10. L91
    exact hp
20Use earlier factsL92–95

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

  1. L92
    exact hs
  2. L93
    exact hc
  3. L94
    exact hv_witness_witness
  4. L95
    exact he_witness_witness

Library-wide reading audit

Original defined command ledger · 95 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 hprime
  14. 0014intro hs
  15. 0015intro hc
  16. 0016have hcopy : FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N)
  17. 0017exact hc
  18. 0018cases hcopy
  19. 0019cases hcopy_right
  20. 0020cases hcopy_right_right
  21. 0021have hp : ~(p=0)
  22. 0022intro hz
  23. 0023specialize prime_nonzero (p)
  24. 0024apply prime_nonzero
  25. 0025exact hprime
  26. 0026exact hz
  27. 0027have hlength : ∃ K. PolynomialProductLength(L,S M,K)
  28. 0028specialize polynomial_product_length_exists (L)
  29. 0029specialize polynomial_product_length_exists (S M)
  30. 0030apply polynomial_product_length_exists
  31. 0031cases hlength
  32. 0032have hv : ∃ d. ∃ e. FpPolyProduct(p,ab,ac,L,BB,BC,S M,d,e,x)
  33. 0033specialize prime_field_polynomial_convolution_at_length_exists (p)
  34. 0034specialize prime_field_polynomial_convolution_at_length_exists (ab)
  35. 0035specialize prime_field_polynomial_convolution_at_length_exists (ac)
  36. 0036specialize prime_field_polynomial_convolution_at_length_exists (L)
  37. 0037specialize prime_field_polynomial_convolution_at_length_exists (BB)
  38. 0038specialize prime_field_polynomial_convolution_at_length_exists (BC)
  39. 0039specialize prime_field_polynomial_convolution_at_length_exists (S M)
  40. 0040specialize prime_field_polynomial_convolution_at_length_exists (x)
  41. 0041apply prime_field_polynomial_convolution_at_length_exists
  42. 0042exact hp
  43. 0043exact hcopy_left
  44. 0044specialize prime_field_polynomial_shift_bounded (p)
  45. 0045specialize prime_field_polynomial_shift_bounded (bb)
  46. 0046specialize prime_field_polynomial_shift_bounded (bc)
  47. 0047specialize prime_field_polynomial_shift_bounded (M)
  48. 0048specialize prime_field_polynomial_shift_bounded (BB)
  49. 0049specialize prime_field_polynomial_shift_bounded (BC)
  50. 0050apply prime_field_polynomial_shift_bounded
  51. 0051exact hprime
  52. 0052exact hcopy_right_left
  53. 0053exact hs
  54. 0054exact hlength_witness
  55. 0055cases hv
  56. 0056cases hv_witness
  57. 0057have he : ∃ e. ∃ f. PolynomialShift(cb,cc,N,e,f)
  58. 0058specialize prime_field_polynomial_shift_exists (cb)
  59. 0059specialize prime_field_polynomial_shift_exists (cc)
  60. 0060specialize prime_field_polynomial_shift_exists (N)
  61. 0061apply prime_field_polynomial_shift_exists
  62. 0062cases he
  63. 0063cases he_witness
  64. 0064exists x
  65. 0065exists x1
  66. 0066exists x2
  67. 0067exists x3
  68. 0068exists x4
  69. 0069split
  70. 0070exact hv_witness_witness
  71. 0071split
  72. 0072exact he_witness_witness
  73. 0073specialize prime_field_polynomial_convolution_shift_right_equivalent (p)
  74. 0074specialize prime_field_polynomial_convolution_shift_right_equivalent (ab)
  75. 0075specialize prime_field_polynomial_convolution_shift_right_equivalent (ac)
  76. 0076specialize prime_field_polynomial_convolution_shift_right_equivalent (L)
  77. 0077specialize prime_field_polynomial_convolution_shift_right_equivalent (bb)
  78. 0078specialize prime_field_polynomial_convolution_shift_right_equivalent (bc)
  79. 0079specialize prime_field_polynomial_convolution_shift_right_equivalent (M)
  80. 0080specialize prime_field_polynomial_convolution_shift_right_equivalent (cb)
  81. 0081specialize prime_field_polynomial_convolution_shift_right_equivalent (cc)
  82. 0082specialize prime_field_polynomial_convolution_shift_right_equivalent (N)
  83. 0083specialize prime_field_polynomial_convolution_shift_right_equivalent (BB)
  84. 0084specialize prime_field_polynomial_convolution_shift_right_equivalent (BC)
  85. 0085specialize prime_field_polynomial_convolution_shift_right_equivalent (x1)
  86. 0086specialize prime_field_polynomial_convolution_shift_right_equivalent (x2)
  87. 0087specialize prime_field_polynomial_convolution_shift_right_equivalent (x)
  88. 0088specialize prime_field_polynomial_convolution_shift_right_equivalent (x3)
  89. 0089specialize prime_field_polynomial_convolution_shift_right_equivalent (x4)
  90. 0090apply prime_field_polynomial_convolution_shift_right_equivalent
  91. 0091exact hp
  92. 0092exact hs
  93. 0093exact hc
  94. 0094exact hv_witness_witness
  95. 0095exact he_witness_witness