PG0070

prime_field_polynomial_right_divides_represented_factorization

Trim the actual quotient, construct an independent proper-length product, and transport formal coefficients. Its genuine nonzero degree e satisfies e+d=a; no quotient degree or domain cancellation is assumed.

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. ∀ db. ∀ dc. ∀ D. ∀ d. ∀ ab. ∀ ac. ∀ L. ∀ a. Prime(p) → FpRepresentedDegree(p,db,dc,D,d) → FpRepresentedDegree(p,ab,ac,L,a) → FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. FpRepresentedDegree(p,x,y,S z,z) ∧ (FpPolyProduct(p,x,y,S z,db,dc,D,n,m,S a) ∧ (PolynomialEquivalent(n,m,S a,ab,ac,L) ∧ z + d = a))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 3PolynomialProductLength(L,M,N) · 1FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 3FpRepresentedDegree(p,b,c,L,d) · 6FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1PolynomialEquivalent(b,c,L,d,e,M) · 4FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1Prime(p) · 1

Actual proof prerequisites

prime_nonzero · checked external prerequisiteprime_field_polynomial_trim_exists · checked external prerequisiteprime_field_polynomial_trim_output_coefficients · checked external prerequisiteprime_field_polynomial_trim_equivalent · checked external prerequisitepolynomial_product_length_exists · checked external prerequisiteprime_field_polynomial_convolution_at_length_exists · checked external prerequisiteprime_field_polynomial_equivalent_transitive · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_convolution_equivalent_congruent_left · checked external prerequisiteprime_field_polynomial_product_equivalent_nonzero_left_nonemptyprime_field_polynomial_trim_nonempty_degree_exists · checked external prerequisiteprime_field_polynomial_convolution_represented_degree · checked external prerequisiteprime_field_polynomial_equivalent_represented_degrees_equal
Original expanded first-order statement 
forall p db dc D d ab ac L a. (~((p) = 1) /\ forall pfa_factor_left_factor_prime pfa_factor_right_factor_prime. (p) = pfa_factor_left_factor_prime * pfa_factor_right_factor_prime -> pfa_factor_left_factor_prime = 1 \/ pfa_factor_right_factor_prime = 1) -> ((((D)=S (d)) /\ (((forall fom_index_pfp_factor_divisorcoefficients. (exists fom_gap_pfp_factor_divisorcoefficients_index_bound. fom_gap_pfp_factor_divisorcoefficients_index_bound + S (fom_index_pfp_factor_divisorcoefficients) = D) -> exists fom_value_pfp_factor_divisorcoefficients. ((((exists fom_beta_height_pfp_factor_divisorcoefficients_entry. fom_beta_height_pfp_factor_divisorcoefficients_entry + S (fom_value_pfp_factor_divisorcoefficients) = S ((S (fom_index_pfp_factor_divisorcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_factor_divisorcoefficients_entry. db = fom_beta_quotient_pfp_factor_divisorcoefficients_entry * S ((S (fom_index_pfp_factor_divisorcoefficients)) * dc) + (fom_value_pfp_factor_divisorcoefficients))) /\ (exists fom_gap_pfp_factor_divisorcoefficients_value_bound. fom_gap_pfp_factor_divisorcoefficients_value_bound + S (fom_value_pfp_factor_divisorcoefficients) = p))) /\ ((exists pfd_leading_factor_divisor. ((((exists ff_h_pfp_factor_divisorentry. ff_h_pfp_factor_divisorentry + S (pfd_leading_factor_divisor) = S ((S (0)) * dc)) /\ exists ff_q_pfp_factor_divisorentry. db = ff_q_pfp_factor_divisorentry * S ((S (0)) * dc) + (pfd_leading_factor_divisor))) /\ ((~(pfd_leading_factor_divisor=0)))))))))) -> ((((L)=S (a)) /\ (((forall fom_index_pfp_factor_targetcoefficients. (exists fom_gap_pfp_factor_targetcoefficients_index_bound. fom_gap_pfp_factor_targetcoefficients_index_bound + S (fom_index_pfp_factor_targetcoefficients) = L) -> exists fom_value_pfp_factor_targetcoefficients. ((((exists fom_beta_height_pfp_factor_targetcoefficients_entry. fom_beta_height_pfp_factor_targetcoefficients_entry + S (fom_value_pfp_factor_targetcoefficients) = S ((S (fom_index_pfp_factor_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_factor_targetcoefficients_entry. ab = fom_beta_quotient_pfp_factor_targetcoefficients_entry * S ((S (fom_index_pfp_factor_targetcoefficients)) * ac) + (fom_value_pfp_factor_targetcoefficients))) /\ (exists fom_gap_pfp_factor_targetcoefficients_value_bound. fom_gap_pfp_factor_targetcoefficients_value_bound + S (fom_value_pfp_factor_targetcoefficients) = p))) /\ ((exists pfd_leading_factor_target. ((((exists ff_h_pfp_factor_targetentry. ff_h_pfp_factor_targetentry + S (pfd_leading_factor_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_factor_targetentry. ab = ff_q_pfp_factor_targetentry * S ((S (0)) * ac) + (pfd_leading_factor_target))) /\ ((~(pfd_leading_factor_target=0)))))))))) -> (((forall fom_index_pfp_factor_divisibility_canonical. (exists fom_gap_pfp_factor_divisibility_canonical_index_bound. fom_gap_pfp_factor_divisibility_canonical_index_bound + S (fom_index_pfp_factor_divisibility_canonical) = L) -> exists fom_value_pfp_factor_divisibility_canonical. ((((exists fom_beta_height_pfp_factor_divisibility_canonical_entry. fom_beta_height_pfp_factor_divisibility_canonical_entry + S (fom_value_pfp_factor_divisibility_canonical) = S ((S (fom_index_pfp_factor_divisibility_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_factor_divisibility_canonical_entry. ab = fom_beta_quotient_pfp_factor_divisibility_canonical_entry * S ((S (fom_index_pfp_factor_divisibility_canonical)) * ac) + (fom_value_pfp_factor_divisibility_canonical))) /\ (exists fom_gap_pfp_factor_divisibility_canonical_value_bound. fom_gap_pfp_factor_divisibility_canonical_value_bound + S (fom_value_pfp_factor_divisibility_canonical) = p))) /\ ((exists pfgu_qb_factor_divisibility pfgu_qc_factor_divisibility pfgu_Q_factor_divisibility pfgu_pb_factor_divisibility pfgu_pc_factor_divisibility pfgu_P_factor_divisibility. ((((forall fom_index_pfp_factor_divisibility_productleft. (exists fom_gap_pfp_factor_divisibility_productleft_index_bound. fom_gap_pfp_factor_divisibility_productleft_index_bound + S (fom_index_pfp_factor_divisibility_productleft) = pfgu_Q_factor_divisibility) -> exists fom_value_pfp_factor_divisibility_productleft. ((((exists fom_beta_height_pfp_factor_divisibility_productleft_entry. fom_beta_height_pfp_factor_divisibility_productleft_entry + S (fom_value_pfp_factor_divisibility_productleft) = S ((S (fom_index_pfp_factor_divisibility_productleft)) * pfgu_qc_factor_divisibility)) /\ exists fom_beta_quotient_pfp_factor_divisibility_productleft_entry. pfgu_qb_factor_divisibility = fom_beta_quotient_pfp_factor_divisibility_productleft_entry * S ((S (fom_index_pfp_factor_divisibility_productleft)) * pfgu_qc_factor_divisibility) + (fom_value_pfp_factor_divisibility_productleft))) /\ (exists fom_gap_pfp_factor_divisibility_productleft_value_bound. fom_gap_pfp_factor_divisibility_productleft_value_bound + S (fom_value_pfp_factor_divisibility_productleft) = p))) /\ (((forall fom_index_pfp_factor_divisibility_productright. (exists fom_gap_pfp_factor_divisibility_productright_index_bound. fom_gap_pfp_factor_divisibility_productright_index_bound + S (fom_index_pfp_factor_divisibility_productright) = D) -> exists fom_value_pfp_factor_divisibility_productright. ((((exists fom_beta_height_pfp_factor_divisibility_productright_entry. fom_beta_height_pfp_factor_divisibility_productright_entry + S (fom_value_pfp_factor_divisibility_productright) = S ((S (fom_index_pfp_factor_divisibility_productright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_divisibility_productright_entry. db = fom_beta_quotient_pfp_factor_divisibility_productright_entry * S ((S (fom_index_pfp_factor_divisibility_productright)) * dc) + (fom_value_pfp_factor_divisibility_productright))) /\ (exists fom_gap_pfp_factor_divisibility_productright_value_bound. fom_gap_pfp_factor_divisibility_productright_value_bound + S (fom_value_pfp_factor_divisibility_productright) = p))) /\ (((((((pfgu_Q_factor_divisibility)=0 \/ (D)=0) /\ (((pfgu_P_factor_divisibility)=0)))) \/ (((~((pfgu_Q_factor_divisibility)=0)) /\ (((~((D)=0)) /\ (((pfgu_Q_factor_divisibility)+(D)=S (pfgu_P_factor_divisibility)))))))) /\ ((forall pfc_index_factor_divisibility_productcoefficients. (exists pfa_gap_factor_divisibility_productcoefficientsbound. pfa_gap_factor_divisibility_productcoefficientsbound + S (pfc_index_factor_divisibility_productcoefficients) = (pfgu_P_factor_divisibility)) -> exists pfc_value_factor_divisibility_productcoefficients. ((((exists ff_h_pfp_factor_divisibility_productcoefficientsentry. ff_h_pfp_factor_divisibility_productcoefficientsentry + S (pfc_value_factor_divisibility_productcoefficients) = S ((S (pfc_index_factor_divisibility_productcoefficients)) * pfgu_pc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientsentry. pfgu_pb_factor_divisibility = ff_q_pfp_factor_divisibility_productcoefficientsentry * S ((S (pfc_index_factor_divisibility_productcoefficients)) * pfgu_pc_factor_divisibility) + (pfc_value_factor_divisibility_productcoefficients))) /\ ((exists pfc_terms_code_factor_divisibility_productcoefficientscoefficient pfc_terms_scale_factor_divisibility_productcoefficientscoefficient pfc_natural_sum_factor_divisibility_productcoefficientscoefficient. ((forall pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal. (exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonalbound. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonalbound + S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal) = (S (pfc_index_factor_divisibility_productcoefficients))) -> exists pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry + S (pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_divisibility_productcoefficientscoefficient = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient) + (pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm. (((pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)+pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm=(pfc_index_factor_divisibility_productcoefficients)) /\ ((((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal) = (pfgu_Q_factor_divisibility)) /\ ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_factor_divisibility = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_divisibility) + (pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_factor_divisibility)=(pfc_index_factor_divisibility_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_divisibility_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_divisibility_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_divisibility_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_divisibility_productcoefficientscoefficientdiagonal)=pfc_left_factor_divisibility_productcoefficientscoefficientdiagonalterm*pfc_right_factor_divisibility_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient) = S ((S (S (pfc_index_factor_divisibility_productcoefficients))) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_divisibility_productcoefficients))) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient))) /\ forall fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps = S (pfc_index_factor_divisibility_productcoefficients)) -> exists fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_divisibility_productcoefficientscoefficient = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_divisibility_productcoefficientscoefficient) + (fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_divisibility_productcoefficientscoefficientsum = fs_q_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_divisibility_productcoefficientscoefficientsum) + (fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_divisibility_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_divisibility_productcoefficientscoefficientresiduebound. pfa_gap_factor_divisibility_productcoefficientscoefficientresiduebound + S (pfc_value_factor_divisibility_productcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_divisibility_productcoefficientscoefficientresiduecongruence pfa_offset_right_factor_divisibility_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_divisibility_productcoefficientscoefficient) + (p) * pfa_offset_left_factor_divisibility_productcoefficientscoefficientresiduecongruence = (pfc_value_factor_divisibility_productcoefficients) + (p) * pfa_offset_right_factor_divisibility_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_factor_divisibility_target pfrep_left_factor_divisibility_target pfrep_right_factor_divisibility_target. ((exists pfrep_position_factor_divisibility_targetfirst. ((pfrep_position_factor_divisibility_targetfirst+S (pfrep_power_factor_divisibility_target)=(pfgu_P_factor_divisibility)) /\ ((((exists ff_h_pfp_factor_divisibility_targetfirstentry. ff_h_pfp_factor_divisibility_targetfirstentry + S (pfrep_left_factor_divisibility_target) = S ((S (pfrep_position_factor_divisibility_targetfirst)) * pfgu_pc_factor_divisibility)) /\ exists ff_q_pfp_factor_divisibility_targetfirstentry. pfgu_pb_factor_divisibility = ff_q_pfp_factor_divisibility_targetfirstentry * S ((S (pfrep_position_factor_divisibility_targetfirst)) * pfgu_pc_factor_divisibility) + (pfrep_left_factor_divisibility_target)))))) \/ (((exists pfrep_gap_factor_divisibility_targetfirstoutside. pfrep_gap_factor_divisibility_targetfirstoutside+(pfgu_P_factor_divisibility)=(pfrep_power_factor_divisibility_target)) /\ (((pfrep_left_factor_divisibility_target)=0))))) -> ((exists pfrep_position_factor_divisibility_targetsecond. ((pfrep_position_factor_divisibility_targetsecond+S (pfrep_power_factor_divisibility_target)=(L)) /\ ((((exists ff_h_pfp_factor_divisibility_targetsecondentry. ff_h_pfp_factor_divisibility_targetsecondentry + S (pfrep_right_factor_divisibility_target) = S ((S (pfrep_position_factor_divisibility_targetsecond)) * ac)) /\ exists ff_q_pfp_factor_divisibility_targetsecondentry. ab = ff_q_pfp_factor_divisibility_targetsecondentry * S ((S (pfrep_position_factor_divisibility_targetsecond)) * ac) + (pfrep_right_factor_divisibility_target)))))) \/ (((exists pfrep_gap_factor_divisibility_targetsecondoutside. pfrep_gap_factor_divisibility_targetsecondoutside+(L)=(pfrep_power_factor_divisibility_target)) /\ (((pfrep_right_factor_divisibility_target)=0))))) -> pfrep_left_factor_divisibility_target=pfrep_right_factor_divisibility_target))))))) -> (exists pfgu_qb_factor_result pfgu_qc_factor_result pfgu_e_factor_result pfgu_pb_factor_result pfgu_pc_factor_result. (((((S (pfgu_e_factor_result))=S (pfgu_e_factor_result)) /\ (((forall fom_index_pfp_factor_result_quotientcoefficients. (exists fom_gap_pfp_factor_result_quotientcoefficients_index_bound. fom_gap_pfp_factor_result_quotientcoefficients_index_bound + S (fom_index_pfp_factor_result_quotientcoefficients) = S (pfgu_e_factor_result)) -> exists fom_value_pfp_factor_result_quotientcoefficients. ((((exists fom_beta_height_pfp_factor_result_quotientcoefficients_entry. fom_beta_height_pfp_factor_result_quotientcoefficients_entry + S (fom_value_pfp_factor_result_quotientcoefficients) = S ((S (fom_index_pfp_factor_result_quotientcoefficients)) * pfgu_qc_factor_result)) /\ exists fom_beta_quotient_pfp_factor_result_quotientcoefficients_entry. pfgu_qb_factor_result = fom_beta_quotient_pfp_factor_result_quotientcoefficients_entry * S ((S (fom_index_pfp_factor_result_quotientcoefficients)) * pfgu_qc_factor_result) + (fom_value_pfp_factor_result_quotientcoefficients))) /\ (exists fom_gap_pfp_factor_result_quotientcoefficients_value_bound. fom_gap_pfp_factor_result_quotientcoefficients_value_bound + S (fom_value_pfp_factor_result_quotientcoefficients) = p))) /\ ((exists pfd_leading_factor_result_quotient. ((((exists ff_h_pfp_factor_result_quotiententry. ff_h_pfp_factor_result_quotiententry + S (pfd_leading_factor_result_quotient) = S ((S (0)) * pfgu_qc_factor_result)) /\ exists ff_q_pfp_factor_result_quotiententry. pfgu_qb_factor_result = ff_q_pfp_factor_result_quotiententry * S ((S (0)) * pfgu_qc_factor_result) + (pfd_leading_factor_result_quotient))) /\ ((~(pfd_leading_factor_result_quotient=0)))))))))) /\ (((((forall fom_index_pfp_factor_result_productleft. (exists fom_gap_pfp_factor_result_productleft_index_bound. fom_gap_pfp_factor_result_productleft_index_bound + S (fom_index_pfp_factor_result_productleft) = S (pfgu_e_factor_result)) -> exists fom_value_pfp_factor_result_productleft. ((((exists fom_beta_height_pfp_factor_result_productleft_entry. fom_beta_height_pfp_factor_result_productleft_entry + S (fom_value_pfp_factor_result_productleft) = S ((S (fom_index_pfp_factor_result_productleft)) * pfgu_qc_factor_result)) /\ exists fom_beta_quotient_pfp_factor_result_productleft_entry. pfgu_qb_factor_result = fom_beta_quotient_pfp_factor_result_productleft_entry * S ((S (fom_index_pfp_factor_result_productleft)) * pfgu_qc_factor_result) + (fom_value_pfp_factor_result_productleft))) /\ (exists fom_gap_pfp_factor_result_productleft_value_bound. fom_gap_pfp_factor_result_productleft_value_bound + S (fom_value_pfp_factor_result_productleft) = p))) /\ (((forall fom_index_pfp_factor_result_productright. (exists fom_gap_pfp_factor_result_productright_index_bound. fom_gap_pfp_factor_result_productright_index_bound + S (fom_index_pfp_factor_result_productright) = D) -> exists fom_value_pfp_factor_result_productright. ((((exists fom_beta_height_pfp_factor_result_productright_entry. fom_beta_height_pfp_factor_result_productright_entry + S (fom_value_pfp_factor_result_productright) = S ((S (fom_index_pfp_factor_result_productright)) * dc)) /\ exists fom_beta_quotient_pfp_factor_result_productright_entry. db = fom_beta_quotient_pfp_factor_result_productright_entry * S ((S (fom_index_pfp_factor_result_productright)) * dc) + (fom_value_pfp_factor_result_productright))) /\ (exists fom_gap_pfp_factor_result_productright_value_bound. fom_gap_pfp_factor_result_productright_value_bound + S (fom_value_pfp_factor_result_productright) = p))) /\ (((((((S (pfgu_e_factor_result))=0 \/ (D)=0) /\ (((S (a))=0)))) \/ (((~((S (pfgu_e_factor_result))=0)) /\ (((~((D)=0)) /\ (((S (pfgu_e_factor_result))+(D)=S (S (a))))))))) /\ ((forall pfc_index_factor_result_productcoefficients. (exists pfa_gap_factor_result_productcoefficientsbound. pfa_gap_factor_result_productcoefficientsbound + S (pfc_index_factor_result_productcoefficients) = (S (a))) -> exists pfc_value_factor_result_productcoefficients. ((((exists ff_h_pfp_factor_result_productcoefficientsentry. ff_h_pfp_factor_result_productcoefficientsentry + S (pfc_value_factor_result_productcoefficients) = S ((S (pfc_index_factor_result_productcoefficients)) * pfgu_pc_factor_result)) /\ exists ff_q_pfp_factor_result_productcoefficientsentry. pfgu_pb_factor_result = ff_q_pfp_factor_result_productcoefficientsentry * S ((S (pfc_index_factor_result_productcoefficients)) * pfgu_pc_factor_result) + (pfc_value_factor_result_productcoefficients))) /\ ((exists pfc_terms_code_factor_result_productcoefficientscoefficient pfc_terms_scale_factor_result_productcoefficientscoefficient pfc_natural_sum_factor_result_productcoefficientscoefficient. ((forall pfc_index_factor_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_factor_result_productcoefficientscoefficientdiagonalbound. pfa_gap_factor_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_factor_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_factor_result_productcoefficients))) -> exists pfc_value_factor_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_factor_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_factor_result_productcoefficientscoefficient = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_factor_result_productcoefficientscoefficient) + (pfc_value_factor_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm pfc_left_factor_result_productcoefficientscoefficientdiagonalterm pfc_right_factor_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_factor_result_productcoefficientscoefficientdiagonal)+pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm=(pfc_index_factor_result_productcoefficients)) /\ ((((((exists pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_factor_result_productcoefficientscoefficientdiagonal) = (S (pfgu_e_factor_result))) /\ ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_factor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_result)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_factor_result = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_factor_result_productcoefficientscoefficientdiagonal)) * pfgu_qc_factor_result) + (pfc_left_factor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermleftoutside+(S (pfgu_e_factor_result))=(pfc_index_factor_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_factor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_factor_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_factor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_factor_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_factor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_factor_result_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_factor_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_factor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_factor_result_productcoefficientscoefficientdiagonal)=pfc_left_factor_result_productcoefficientscoefficientdiagonalterm*pfc_right_factor_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_factor_result_productcoefficientscoefficientsum fs_v_pfc_factor_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_factor_result_productcoefficientscoefficient) = S ((S (S (pfc_index_factor_result_productcoefficients))) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_factor_result_productcoefficients))) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (pfc_natural_sum_factor_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_factor_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_factor_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_factor_result_productcoefficients)) -> exists fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_factor_result_productcoefficientscoefficient = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_factor_result_productcoefficientscoefficient) + (fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_factor_result_productcoefficientscoefficientsum = fs_q_pfc_factor_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_factor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_factor_result_productcoefficientscoefficientsum) + (fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_factor_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_factor_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_factor_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_factor_result_productcoefficientscoefficientresiduebound. pfa_gap_factor_result_productcoefficientscoefficientresiduebound + S (pfc_value_factor_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_factor_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_factor_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_factor_result_productcoefficientscoefficient) + (p) * pfa_offset_left_factor_result_productcoefficientscoefficientresiduecongruence = (pfc_value_factor_result_productcoefficients) + (p) * pfa_offset_right_factor_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((forall pfrep_power_factor_result_equivalent pfrep_left_factor_result_equivalent pfrep_right_factor_result_equivalent. ((exists pfrep_position_factor_result_equivalentfirst. ((pfrep_position_factor_result_equivalentfirst+S (pfrep_power_factor_result_equivalent)=(S (a))) /\ ((((exists ff_h_pfp_factor_result_equivalentfirstentry. ff_h_pfp_factor_result_equivalentfirstentry + S (pfrep_left_factor_result_equivalent) = S ((S (pfrep_position_factor_result_equivalentfirst)) * pfgu_pc_factor_result)) /\ exists ff_q_pfp_factor_result_equivalentfirstentry. pfgu_pb_factor_result = ff_q_pfp_factor_result_equivalentfirstentry * S ((S (pfrep_position_factor_result_equivalentfirst)) * pfgu_pc_factor_result) + (pfrep_left_factor_result_equivalent)))))) \/ (((exists pfrep_gap_factor_result_equivalentfirstoutside. pfrep_gap_factor_result_equivalentfirstoutside+(S (a))=(pfrep_power_factor_result_equivalent)) /\ (((pfrep_left_factor_result_equivalent)=0))))) -> ((exists pfrep_position_factor_result_equivalentsecond. ((pfrep_position_factor_result_equivalentsecond+S (pfrep_power_factor_result_equivalent)=(L)) /\ ((((exists ff_h_pfp_factor_result_equivalentsecondentry. ff_h_pfp_factor_result_equivalentsecondentry + S (pfrep_right_factor_result_equivalent) = S ((S (pfrep_position_factor_result_equivalentsecond)) * ac)) /\ exists ff_q_pfp_factor_result_equivalentsecondentry. ab = ff_q_pfp_factor_result_equivalentsecondentry * S ((S (pfrep_position_factor_result_equivalentsecond)) * ac) + (pfrep_right_factor_result_equivalent)))))) \/ (((exists pfrep_gap_factor_result_equivalentsecondoutside. pfrep_gap_factor_result_equivalentsecondoutside+(L)=(pfrep_power_factor_result_equivalent)) /\ (((pfrep_right_factor_result_equivalent)=0))))) -> pfrep_left_factor_result_equivalent=pfrep_right_factor_result_equivalent) /\ (((pfgu_e_factor_result)+(d)=(a)))))))))

Complete tactic proof in conservative notation

All 235 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

235 script commands · 50 reading checkpoints · 18 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 (2)
prime field polynomial product equivalent nonzero left nonemptyprime field polynomial equivalent represented degrees equal
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro db
  3. L3
    intro dc
  4. L4
    intro D
  5. L5
    intro d
  6. L6
    intro ab
  7. L7
    intro ac
  8. L8
    intro L
  9. L9
    intro a
  10. L10
    intro hp
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hd
  2. L12
    intro ha
  3. L13
    intro hrd
03Establish hpnL14–19

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

  1. L14
    have hpn : ~(p=0)
  2. L15
    intro hpzero
  3. L16
    specialize prime_nonzero (p)
  4. L17
    apply prime_nonzero
  5. L18
    exact hp
  6. L19
    exact hpzero
04Establish hdboundL20–20

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

  1. L20
    have hdbound : BetaPrefixInto(db,dc,D,p)Definitions: BetaPrefixInto(db,dc,D,p)Original native command in the exact edition
05Separate the logical casesL21–22

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

  1. L21
    cases hd
  2. L22
    cases hd_right
06Use earlier factsL23–23

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

  1. L23
    exact hd_right_left
07Separate the logical casesL24–31

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

  1. L24
    cases hrd
  2. L25
    cases hrd_right
  3. L26
    cases hrd_right_witness
  4. L27
    cases hrd_right_witness_witness
  5. L28
    cases hrd_right_witness_witness_witness
  6. L29
    cases hrd_right_witness_witness_witness_witness
  7. L30
    cases hrd_right_witness_witness_witness_witness_witness
  8. L31
    cases hrd_right_witness_witness_witness_witness_witness_witness
08Establish hqboundL32–32

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

  1. L32
    have hqbound : BetaPrefixInto(x,x1,x2,p)Definitions: BetaPrefixInto(x,x1,x2,p)Original native command in the exact edition
09Separate the logical casesL33–35

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

  1. L33
    cases hrd_right_witness_witness_witness_witness_witness_witness_left
  2. L34
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  3. L35
    cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
10Use earlier factsL36–36

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

  1. L36
    exact hrd_right_witness_witness_witness_witness_witness_witness_left_left
11Establish htL37–43

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

  1. L37
    have ht : ∃ t. ∃ tb. ∃ tc. ∃ T. FpPolynomialTrim(p,x,x1,x2,t,tb,tc,T)Definitions: FpPolynomialTrim(p,x,x1,x2,t,tb,tc,T)Original native command in the exact edition
  2. L38
    specialize prime_field_polynomial_trim_exists (p)
  3. L39
    specialize prime_field_polynomial_trim_exists (x)
  4. L40
    specialize prime_field_polynomial_trim_exists (x1)
  5. L41
    specialize prime_field_polynomial_trim_exists (x2)
  6. L42
    apply prime_field_polynomial_trim_exists
  7. L43
    exact hqbound
12Separate the logical casesL44–47

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

  1. L44
    cases ht
  2. L45
    cases ht_witness
  3. L46
    cases ht_witness_witness
  4. L47
    cases ht_witness_witness_witness
13Establish htboundL48–57

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

  1. L48
    have htbound : BetaPrefixInto(x7,x8,x9,p)Definitions: BetaPrefixInto(x7,x8,x9,p)Original native command in the exact edition
  2. L49
    specialize prime_field_polynomial_trim_output_coefficients (p)
  3. L50
    specialize prime_field_polynomial_trim_output_coefficients (x)
  4. L51
    specialize prime_field_polynomial_trim_output_coefficients (x1)
  5. L52
    specialize prime_field_polynomial_trim_output_coefficients (x2)
  6. L53
    specialize prime_field_polynomial_trim_output_coefficients (x6)
  7. L54
    specialize prime_field_polynomial_trim_output_coefficients (x7)
  8. L55
    specialize prime_field_polynomial_trim_output_coefficients (x8)
  9. L56
    specialize prime_field_polynomial_trim_output_coefficients (x9)
  10. L57
    apply prime_field_polynomial_trim_output_coefficients
14Use earlier factsL58–58

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

  1. L58
    exact ht_witness_witness_witness_witness
15Establish hqeL59–68

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

  1. L59
    have hqe : PolynomialEquivalent(x,x1,x2,x7,x8,x9)Definitions: PolynomialEquivalent(x,x1,x2,x7,x8,x9)Original native command in the exact edition
  2. L60
    specialize prime_field_polynomial_trim_equivalent (p)
  3. L61
    specialize prime_field_polynomial_trim_equivalent (x)
  4. L62
    specialize prime_field_polynomial_trim_equivalent (x1)
  5. L63
    specialize prime_field_polynomial_trim_equivalent (x2)
  6. L64
    specialize prime_field_polynomial_trim_equivalent (x6)
  7. L65
    specialize prime_field_polynomial_trim_equivalent (x7)
  8. L66
    specialize prime_field_polynomial_trim_equivalent (x8)
  9. L67
    specialize prime_field_polynomial_trim_equivalent (x9)
  10. L68
    apply prime_field_polynomial_trim_equivalent
16Use earlier factsL69–69

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

  1. L69
    exact ht_witness_witness_witness_witness
17Establish hplenL70–73

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

  1. L70
    have hplen : ∃ N. PolynomialProductLength(x9,D,N)Definitions: PolynomialProductLength(x9,D,N)Original native command in the exact edition
  2. L71
    specialize polynomial_product_length_exists (x9)
  3. L72
    specialize polynomial_product_length_exists (D)
  4. L73
    apply polynomial_product_length_exists
18Separate the logical casesL74–74

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

  1. L74
    cases hplen
19Establish hpnewL75–84

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. L75
    have hpnew : ∃ vb. ∃ vc. FpPolyProduct(p,x7,x8,x9,db,dc,D,vb,vc,x10)Definitions: FpPolyProduct(p,x7,x8,x9,db,dc,D,vb,vc,x10)Original native command in the exact edition
  2. L76
    specialize prime_field_polynomial_convolution_at_length_exists (p)
  3. L77
    specialize prime_field_polynomial_convolution_at_length_exists (x7)
  4. L78
    specialize prime_field_polynomial_convolution_at_length_exists (x8)
  5. L79
    specialize prime_field_polynomial_convolution_at_length_exists (x9)
  6. L80
    specialize prime_field_polynomial_convolution_at_length_exists (db)
  7. L81
    specialize prime_field_polynomial_convolution_at_length_exists (dc)
  8. L82
    specialize prime_field_polynomial_convolution_at_length_exists (D)
  9. L83
    specialize prime_field_polynomial_convolution_at_length_exists (x10)
  10. L84
    apply prime_field_polynomial_convolution_at_length_exists
20Use earlier factsL85–88

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

  1. L85
    exact hpn
  2. L86
    exact htbound
  3. L87
    exact hdbound
  4. L88
    exact hplen_witness
21Separate the logical casesL89–90

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

  1. L89
    cases hpnew
  2. L90
    cases hpnew_witness
22Establish hequivL91–100

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

  1. L91
    have hequiv : PolynomialEquivalent(x11,x12,x10,ab,ac,L)Definitions: PolynomialEquivalent(x11,x12,x10,ab,ac,L)Original native command in the exact edition
  2. L92
    specialize prime_field_polynomial_equivalent_transitive (x11)
  3. L93
    specialize prime_field_polynomial_equivalent_transitive (x12)
  4. L94
    specialize prime_field_polynomial_equivalent_transitive (x10)
  5. L95
    specialize prime_field_polynomial_equivalent_transitive (x3)
  6. L96
    specialize prime_field_polynomial_equivalent_transitive (x4)
  7. L97
    specialize prime_field_polynomial_equivalent_transitive (x5)
  8. L98
    specialize prime_field_polynomial_equivalent_transitive (ab)
  9. L99
    specialize prime_field_polynomial_equivalent_transitive (ac)
  10. L100
    specialize prime_field_polynomial_equivalent_transitive (L)
23Use earlier factsL101–110

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

  1. L101
    apply prime_field_polynomial_equivalent_transitive
  2. L102
    specialize prime_field_polynomial_equivalent_symmetric (x3)
  3. L103
    specialize prime_field_polynomial_equivalent_symmetric (x4)
  4. L104
    specialize prime_field_polynomial_equivalent_symmetric (x5)
  5. L105
    specialize prime_field_polynomial_equivalent_symmetric (x11)
  6. L106
    specialize prime_field_polynomial_equivalent_symmetric (x12)
  7. L107
    specialize prime_field_polynomial_equivalent_symmetric (x10)
  8. L108
    apply prime_field_polynomial_equivalent_symmetric
  9. L109
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  10. L110
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
24Use earlier factsL111–120

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

  1. L111
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  2. L112
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  3. L113
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (db)
  4. L114
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (dc)
  5. L115
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (D)
  6. L116
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x3)
  7. L117
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x4)
  8. L118
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x5)
  9. L119
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x7)
  10. L120
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x8)
25Use earlier factsL121–130

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

  1. L121
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x9)
  2. L122
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x11)
  3. L123
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x12)
  4. L124
    specialize prime_field_polynomial_convolution_equivalent_congruent_left (x10)
  5. L125
    apply prime_field_polynomial_convolution_equivalent_congruent_left
  6. L126
    exact hpn
  7. L127
    exact hqe
  8. L128
    exact hrd_right_witness_witness_witness_witness_witness_witness_left
  9. L129
    exact hpnew_witness_witness
  10. L130
    exact hrd_right_witness_witness_witness_witness_witness_witness_right
26Establish hnL131–140

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

  1. L131
    have hn : ~(x9=0)
  2. L132
    intro htzero
  3. L133
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (p)
  4. L134
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x7)
  5. L135
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x8)
  6. L136
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x9)
  7. L137
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (db)
  8. L138
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (dc)
  9. L139
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (D)
  10. L140
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x11)
27Use earlier factsL141–150

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

  1. L141
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x12)
  2. L142
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x10)
  3. L143
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ab)
  4. L144
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ac)
  5. L145
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (L)
  6. L146
    specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (a)
  7. L147
    apply prime_field_polynomial_product_equivalent_nonzero_left_nonempty
  8. L148
    exact ha
  9. L149
    exact hpnew_witness_witness
  10. L150
    exact hequiv
28Use earlier factsL151–151

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

  1. L151
    exact htzero
29Establish hqdL152–161

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

  1. L152
    have hqd : ∃ e. FpRepresentedDegree(p,x7,x8,x9,e)Definitions: FpRepresentedDegree(p,x7,x8,x9,e)Original native command in the exact edition
  2. L153
    specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  3. L154
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  4. L155
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  5. L156
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  6. L157
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x6)
  7. L158
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x7)
  8. L159
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x8)
  9. L160
    specialize prime_field_polynomial_trim_nonempty_degree_exists (x9)
  10. L161
    apply prime_field_polynomial_trim_nonempty_degree_exists
30Use earlier factsL162–163

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

  1. L162
    exact ht_witness_witness_witness_witness
  2. L163
    exact hn
31Separate the logical casesL164–164

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

  1. L164
    cases hqd
32Establish hpdL165–174

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

  1. L165
    have hpd : FpRepresentedDegree(p,x11,x12,x10,x13 + d)Definitions: FpRepresentedDegree(p,x11,x12,x10,x13 + d)Original native command in the exact edition
  2. L166
    specialize prime_field_polynomial_convolution_represented_degree (p)
  3. L167
    specialize prime_field_polynomial_convolution_represented_degree (x7)
  4. L168
    specialize prime_field_polynomial_convolution_represented_degree (x8)
  5. L169
    specialize prime_field_polynomial_convolution_represented_degree (x9)
  6. L170
    specialize prime_field_polynomial_convolution_represented_degree (x13)
  7. L171
    specialize prime_field_polynomial_convolution_represented_degree (db)
  8. L172
    specialize prime_field_polynomial_convolution_represented_degree (dc)
  9. L173
    specialize prime_field_polynomial_convolution_represented_degree (D)
  10. L174
    specialize prime_field_polynomial_convolution_represented_degree (d)
33Use earlier factsL175–182

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

  1. L175
    specialize prime_field_polynomial_convolution_represented_degree (x11)
  2. L176
    specialize prime_field_polynomial_convolution_represented_degree (x12)
  3. L177
    specialize prime_field_polynomial_convolution_represented_degree (x10)
  4. L178
    apply prime_field_polynomial_convolution_represented_degree
  5. L179
    exact hp
  6. L180
    exact hqd_witness
  7. L181
    exact hd
  8. L182
    exact hpnew_witness_witness
34Establish hsumL183–192

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

  1. L183
    have hsum : x13+d=a
  2. L184
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (p)
  3. L185
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x11)
  4. L186
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x12)
  5. L187
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x10)
  6. L188
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (x13+d)
  7. L189
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (ab)
  8. L190
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (ac)
  9. L191
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (L)
  10. L192
    specialize prime_field_polynomial_equivalent_represented_degrees_equal (a)
35Use earlier factsL193–196

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

  1. L193
    apply prime_field_polynomial_equivalent_represented_degrees_equal
  2. L194
    exact hpd
  3. L195
    exact ha
  4. L196
    exact hequiv
36Establish hqlenL197–197

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

  1. L197
    have hqlen : x9=S x13
37Separate the logical casesL198–198

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

  1. L198
    cases hqd_witness
38Use earlier factsL199–199

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

  1. L199
    exact hqd_witness_left
39Establish hplen2L200–200

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

  1. L200
    have hplen2 : x10=S a
40Separate the logical casesL201–201

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

  1. L201
    cases hpd
41Calculate and transport equalitiesL202–204

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

  1. L202
    rewrite hpd_left
  2. L203
    rewrite hsum
  3. L204
    refl
42Construct an explicit witnessL205–209

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

  1. L205
    exists x7
  2. L206
    exists x8
  3. L207
    exists x13
  4. L208
    exists x11
  5. L209
    exists x12
43Separate the logical casesL210–210

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

  1. L210
    split
44Establish hqdnewL211–215

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

  1. L211
    have hqdnew : FpRepresentedDegree(p,x7,x8,x9,x13)Definitions: FpRepresentedDegree(p,x7,x8,x9,x13)Original native command in the exact edition
  2. L212
    exact hqd_witness
  3. L213
    rewrite hqlen at hqdnew
  4. L214
    rewrite hqlen at hqdnew
  5. L215
    exact hqdnew
45Separate the logical casesL216–216

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

  1. L216
    split
46Establish hcpL217–226

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

  1. L217
    have hcp : FpPolyProduct(p,x7,x8,x9,db,dc,D,x11,x12,x10)Definitions: FpPolyProduct(p,x7,x8,x9,db,dc,D,x11,x12,x10)Original native command in the exact edition
  2. L218
    exact hpnew_witness_witness
  3. L219
    rewrite hqlen at hcp
  4. L220
    rewrite hqlen at hcp
  5. L221
    rewrite hqlen at hcp
  6. L222
    rewrite hqlen at hcp
  7. L223
    rewrite hqlen at hcp
  8. L224
    rewrite hqlen at hcp
  9. L225
    rewrite hplen2 at hcp
  10. L226
    rewrite hplen2 at hcp
47Calculate and transport equalitiesL227–227

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

  1. L227
    rewrite hplen2 at hcp
48Use earlier factsL228–228

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

  1. L228
    exact hcp
49Separate the logical casesL229–229

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

  1. L229
    split
50Establish hepL230–235

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

  1. L230
    have hep : PolynomialEquivalent(x11,x12,x10,ab,ac,L)Definitions: PolynomialEquivalent(x11,x12,x10,ab,ac,L)Original native command in the exact edition
  2. L231
    exact hequiv
  3. L232
    rewrite hplen2 at hep
  4. L233
    rewrite hplen2 at hep
  5. L234
    exact hep
  6. L235
    exact hsum

Library-wide reading audit

Original defined command ledger · 235 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro D
  5. 0005intro d
  6. 0006intro ab
  7. 0007intro ac
  8. 0008intro L
  9. 0009intro a
  10. 0010intro hp
  11. 0011intro hd
  12. 0012intro ha
  13. 0013intro hrd
  14. 0014have hpn : ~(p=0)
  15. 0015intro hpzero
  16. 0016specialize prime_nonzero (p)
  17. 0017apply prime_nonzero
  18. 0018exact hp
  19. 0019exact hpzero
  20. 0020have hdbound : BetaPrefixInto(db,dc,D,p)
  21. 0021cases hd
  22. 0022cases hd_right
  23. 0023exact hd_right_left
  24. 0024cases hrd
  25. 0025cases hrd_right
  26. 0026cases hrd_right_witness
  27. 0027cases hrd_right_witness_witness
  28. 0028cases hrd_right_witness_witness_witness
  29. 0029cases hrd_right_witness_witness_witness_witness
  30. 0030cases hrd_right_witness_witness_witness_witness_witness
  31. 0031cases hrd_right_witness_witness_witness_witness_witness_witness
  32. 0032have hqbound : BetaPrefixInto(x,x1,x2,p)
  33. 0033cases hrd_right_witness_witness_witness_witness_witness_witness_left
  34. 0034cases hrd_right_witness_witness_witness_witness_witness_witness_left_right
  35. 0035cases hrd_right_witness_witness_witness_witness_witness_witness_left_right_right
  36. 0036exact hrd_right_witness_witness_witness_witness_witness_witness_left_left
  37. 0037have ht : ∃ t. ∃ tb. ∃ tc. ∃ T. FpPolynomialTrim(p,x,x1,x2,t,tb,tc,T)
  38. 0038specialize prime_field_polynomial_trim_exists (p)
  39. 0039specialize prime_field_polynomial_trim_exists (x)
  40. 0040specialize prime_field_polynomial_trim_exists (x1)
  41. 0041specialize prime_field_polynomial_trim_exists (x2)
  42. 0042apply prime_field_polynomial_trim_exists
  43. 0043exact hqbound
  44. 0044cases ht
  45. 0045cases ht_witness
  46. 0046cases ht_witness_witness
  47. 0047cases ht_witness_witness_witness
  48. 0048have htbound : BetaPrefixInto(x7,x8,x9,p)
  49. 0049specialize prime_field_polynomial_trim_output_coefficients (p)
  50. 0050specialize prime_field_polynomial_trim_output_coefficients (x)
  51. 0051specialize prime_field_polynomial_trim_output_coefficients (x1)
  52. 0052specialize prime_field_polynomial_trim_output_coefficients (x2)
  53. 0053specialize prime_field_polynomial_trim_output_coefficients (x6)
  54. 0054specialize prime_field_polynomial_trim_output_coefficients (x7)
  55. 0055specialize prime_field_polynomial_trim_output_coefficients (x8)
  56. 0056specialize prime_field_polynomial_trim_output_coefficients (x9)
  57. 0057apply prime_field_polynomial_trim_output_coefficients
  58. 0058exact ht_witness_witness_witness_witness
  59. 0059have hqe : PolynomialEquivalent(x,x1,x2,x7,x8,x9)
  60. 0060specialize prime_field_polynomial_trim_equivalent (p)
  61. 0061specialize prime_field_polynomial_trim_equivalent (x)
  62. 0062specialize prime_field_polynomial_trim_equivalent (x1)
  63. 0063specialize prime_field_polynomial_trim_equivalent (x2)
  64. 0064specialize prime_field_polynomial_trim_equivalent (x6)
  65. 0065specialize prime_field_polynomial_trim_equivalent (x7)
  66. 0066specialize prime_field_polynomial_trim_equivalent (x8)
  67. 0067specialize prime_field_polynomial_trim_equivalent (x9)
  68. 0068apply prime_field_polynomial_trim_equivalent
  69. 0069exact ht_witness_witness_witness_witness
  70. 0070have hplen : ∃ N. PolynomialProductLength(x9,D,N)
  71. 0071specialize polynomial_product_length_exists (x9)
  72. 0072specialize polynomial_product_length_exists (D)
  73. 0073apply polynomial_product_length_exists
  74. 0074cases hplen
  75. 0075have hpnew : ∃ vb. ∃ vc. FpPolyProduct(p,x7,x8,x9,db,dc,D,vb,vc,x10)
  76. 0076specialize prime_field_polynomial_convolution_at_length_exists (p)
  77. 0077specialize prime_field_polynomial_convolution_at_length_exists (x7)
  78. 0078specialize prime_field_polynomial_convolution_at_length_exists (x8)
  79. 0079specialize prime_field_polynomial_convolution_at_length_exists (x9)
  80. 0080specialize prime_field_polynomial_convolution_at_length_exists (db)
  81. 0081specialize prime_field_polynomial_convolution_at_length_exists (dc)
  82. 0082specialize prime_field_polynomial_convolution_at_length_exists (D)
  83. 0083specialize prime_field_polynomial_convolution_at_length_exists (x10)
  84. 0084apply prime_field_polynomial_convolution_at_length_exists
  85. 0085exact hpn
  86. 0086exact htbound
  87. 0087exact hdbound
  88. 0088exact hplen_witness
  89. 0089cases hpnew
  90. 0090cases hpnew_witness
  91. 0091have hequiv : PolynomialEquivalent(x11,x12,x10,ab,ac,L)
  92. 0092specialize prime_field_polynomial_equivalent_transitive (x11)
  93. 0093specialize prime_field_polynomial_equivalent_transitive (x12)
  94. 0094specialize prime_field_polynomial_equivalent_transitive (x10)
  95. 0095specialize prime_field_polynomial_equivalent_transitive (x3)
  96. 0096specialize prime_field_polynomial_equivalent_transitive (x4)
  97. 0097specialize prime_field_polynomial_equivalent_transitive (x5)
  98. 0098specialize prime_field_polynomial_equivalent_transitive (ab)
  99. 0099specialize prime_field_polynomial_equivalent_transitive (ac)
  100. 0100specialize prime_field_polynomial_equivalent_transitive (L)
  101. 0101apply prime_field_polynomial_equivalent_transitive
  102. 0102specialize prime_field_polynomial_equivalent_symmetric (x3)
  103. 0103specialize prime_field_polynomial_equivalent_symmetric (x4)
  104. 0104specialize prime_field_polynomial_equivalent_symmetric (x5)
  105. 0105specialize prime_field_polynomial_equivalent_symmetric (x11)
  106. 0106specialize prime_field_polynomial_equivalent_symmetric (x12)
  107. 0107specialize prime_field_polynomial_equivalent_symmetric (x10)
  108. 0108apply prime_field_polynomial_equivalent_symmetric
  109. 0109specialize prime_field_polynomial_convolution_equivalent_congruent_left (p)
  110. 0110specialize prime_field_polynomial_convolution_equivalent_congruent_left (x)
  111. 0111specialize prime_field_polynomial_convolution_equivalent_congruent_left (x1)
  112. 0112specialize prime_field_polynomial_convolution_equivalent_congruent_left (x2)
  113. 0113specialize prime_field_polynomial_convolution_equivalent_congruent_left (db)
  114. 0114specialize prime_field_polynomial_convolution_equivalent_congruent_left (dc)
  115. 0115specialize prime_field_polynomial_convolution_equivalent_congruent_left (D)
  116. 0116specialize prime_field_polynomial_convolution_equivalent_congruent_left (x3)
  117. 0117specialize prime_field_polynomial_convolution_equivalent_congruent_left (x4)
  118. 0118specialize prime_field_polynomial_convolution_equivalent_congruent_left (x5)
  119. 0119specialize prime_field_polynomial_convolution_equivalent_congruent_left (x7)
  120. 0120specialize prime_field_polynomial_convolution_equivalent_congruent_left (x8)
  121. 0121specialize prime_field_polynomial_convolution_equivalent_congruent_left (x9)
  122. 0122specialize prime_field_polynomial_convolution_equivalent_congruent_left (x11)
  123. 0123specialize prime_field_polynomial_convolution_equivalent_congruent_left (x12)
  124. 0124specialize prime_field_polynomial_convolution_equivalent_congruent_left (x10)
  125. 0125apply prime_field_polynomial_convolution_equivalent_congruent_left
  126. 0126exact hpn
  127. 0127exact hqe
  128. 0128exact hrd_right_witness_witness_witness_witness_witness_witness_left
  129. 0129exact hpnew_witness_witness
  130. 0130exact hrd_right_witness_witness_witness_witness_witness_witness_right
  131. 0131have hn : ~(x9=0)
  132. 0132intro htzero
  133. 0133specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (p)
  134. 0134specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x7)
  135. 0135specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x8)
  136. 0136specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x9)
  137. 0137specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (db)
  138. 0138specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (dc)
  139. 0139specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (D)
  140. 0140specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x11)
  141. 0141specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x12)
  142. 0142specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (x10)
  143. 0143specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ab)
  144. 0144specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (ac)
  145. 0145specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (L)
  146. 0146specialize prime_field_polynomial_product_equivalent_nonzero_left_nonempty (a)
  147. 0147apply prime_field_polynomial_product_equivalent_nonzero_left_nonempty
  148. 0148exact ha
  149. 0149exact hpnew_witness_witness
  150. 0150exact hequiv
  151. 0151exact htzero
  152. 0152have hqd : ∃ e. FpRepresentedDegree(p,x7,x8,x9,e)
  153. 0153specialize prime_field_polynomial_trim_nonempty_degree_exists (p)
  154. 0154specialize prime_field_polynomial_trim_nonempty_degree_exists (x)
  155. 0155specialize prime_field_polynomial_trim_nonempty_degree_exists (x1)
  156. 0156specialize prime_field_polynomial_trim_nonempty_degree_exists (x2)
  157. 0157specialize prime_field_polynomial_trim_nonempty_degree_exists (x6)
  158. 0158specialize prime_field_polynomial_trim_nonempty_degree_exists (x7)
  159. 0159specialize prime_field_polynomial_trim_nonempty_degree_exists (x8)
  160. 0160specialize prime_field_polynomial_trim_nonempty_degree_exists (x9)
  161. 0161apply prime_field_polynomial_trim_nonempty_degree_exists
  162. 0162exact ht_witness_witness_witness_witness
  163. 0163exact hn
  164. 0164cases hqd
  165. 0165have hpd : FpRepresentedDegree(p,x11,x12,x10,x13 + d)
  166. 0166specialize prime_field_polynomial_convolution_represented_degree (p)
  167. 0167specialize prime_field_polynomial_convolution_represented_degree (x7)
  168. 0168specialize prime_field_polynomial_convolution_represented_degree (x8)
  169. 0169specialize prime_field_polynomial_convolution_represented_degree (x9)
  170. 0170specialize prime_field_polynomial_convolution_represented_degree (x13)
  171. 0171specialize prime_field_polynomial_convolution_represented_degree (db)
  172. 0172specialize prime_field_polynomial_convolution_represented_degree (dc)
  173. 0173specialize prime_field_polynomial_convolution_represented_degree (D)
  174. 0174specialize prime_field_polynomial_convolution_represented_degree (d)
  175. 0175specialize prime_field_polynomial_convolution_represented_degree (x11)
  176. 0176specialize prime_field_polynomial_convolution_represented_degree (x12)
  177. 0177specialize prime_field_polynomial_convolution_represented_degree (x10)
  178. 0178apply prime_field_polynomial_convolution_represented_degree
  179. 0179exact hp
  180. 0180exact hqd_witness
  181. 0181exact hd
  182. 0182exact hpnew_witness_witness
  183. 0183have hsum : x13+d=a
  184. 0184specialize prime_field_polynomial_equivalent_represented_degrees_equal (p)
  185. 0185specialize prime_field_polynomial_equivalent_represented_degrees_equal (x11)
  186. 0186specialize prime_field_polynomial_equivalent_represented_degrees_equal (x12)
  187. 0187specialize prime_field_polynomial_equivalent_represented_degrees_equal (x10)
  188. 0188specialize prime_field_polynomial_equivalent_represented_degrees_equal (x13+d)
  189. 0189specialize prime_field_polynomial_equivalent_represented_degrees_equal (ab)
  190. 0190specialize prime_field_polynomial_equivalent_represented_degrees_equal (ac)
  191. 0191specialize prime_field_polynomial_equivalent_represented_degrees_equal (L)
  192. 0192specialize prime_field_polynomial_equivalent_represented_degrees_equal (a)
  193. 0193apply prime_field_polynomial_equivalent_represented_degrees_equal
  194. 0194exact hpd
  195. 0195exact ha
  196. 0196exact hequiv
  197. 0197have hqlen : x9=S x13
  198. 0198cases hqd_witness
  199. 0199exact hqd_witness_left
  200. 0200have hplen2 : x10=S a
  201. 0201cases hpd
  202. 0202rewrite hpd_left
  203. 0203rewrite hsum
  204. 0204refl
  205. 0205exists x7
  206. 0206exists x8
  207. 0207exists x13
  208. 0208exists x11
  209. 0209exists x12
  210. 0210split
  211. 0211have hqdnew : FpRepresentedDegree(p,x7,x8,x9,x13)
  212. 0212exact hqd_witness
  213. 0213rewrite hqlen at hqdnew
  214. 0214rewrite hqlen at hqdnew
  215. 0215exact hqdnew
  216. 0216split
  217. 0217have hcp : FpPolyProduct(p,x7,x8,x9,db,dc,D,x11,x12,x10)
  218. 0218exact hpnew_witness_witness
  219. 0219rewrite hqlen at hcp
  220. 0220rewrite hqlen at hcp
  221. 0221rewrite hqlen at hcp
  222. 0222rewrite hqlen at hcp
  223. 0223rewrite hqlen at hcp
  224. 0224rewrite hqlen at hcp
  225. 0225rewrite hplen2 at hcp
  226. 0226rewrite hplen2 at hcp
  227. 0227rewrite hplen2 at hcp
  228. 0228exact hcp
  229. 0229split
  230. 0230have hep : PolynomialEquivalent(x11,x12,x10,ab,ac,L)
  231. 0231exact hequiv
  232. 0232rewrite hplen2 at hep
  233. 0233rewrite hplen2 at hep
  234. 0234exact hep
  235. 0235exact hsum