PG002B — prime_field_polynomial_right_divides_equivalent_divisor

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. ∀ ab. ∀ ac. ∀ L. ∀ eb. ∀ ec. ∀ E. ¬p = 0 → BetaPrefixInto(eb,ec,E,p) → PolynomialEquivalent(db,dc,D,eb,ec,E) → FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) → FpPolynomialRightDivides(p,eb,ec,E,ab,ac,L)

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 1 PolynomialProductLength(L,M,N) · 1 FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2 PolynomialEquivalent(b,c,L,d,e,M) · 1 FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 2

Actual proof prerequisites

polynomial_product_length_exists · checked external prerequisite prime_field_polynomial_convolution_at_length_exists · checked external prerequisite prime_field_polynomial_right_divides_from_product prime_field_polynomial_equivalent_transitive · checked external prerequisite prime_field_polynomial_equivalent_symmetric · checked external prerequisite prime_field_polynomial_convolution_equivalent_congruent_right · checked external prerequisite

Original expanded first-order statement

forall p db dc D ab ac L eb ec E. (~(p=0)) -> (forall fom_index_pfp_right_divisor_replacement_bound. (exists fom_gap_pfp_right_divisor_replacement_bound_index_bound. fom_gap_pfp_right_divisor_replacement_bound_index_bound + S (fom_index_pfp_right_divisor_replacement_bound) = E) -> exists fom_value_pfp_right_divisor_replacement_bound. ((((exists fom_beta_height_pfp_right_divisor_replacement_bound_entry. fom_beta_height_pfp_right_divisor_replacement_bound_entry + S (fom_value_pfp_right_divisor_replacement_bound) = S ((S (fom_index_pfp_right_divisor_replacement_bound)) * ec)) /\ exists fom_beta_quotient_pfp_right_divisor_replacement_bound_entry. eb = fom_beta_quotient_pfp_right_divisor_replacement_bound_entry * S ((S (fom_index_pfp_right_divisor_replacement_bound)) * ec) + (fom_value_pfp_right_divisor_replacement_bound))) /\ (exists fom_gap_pfp_right_divisor_replacement_bound_value_bound. fom_gap_pfp_right_divisor_replacement_bound_value_bound + S (fom_value_pfp_right_divisor_replacement_bound) = p))) -> (forall pfrep_power_right_divisor_equivalent pfrep_left_right_divisor_equivalent pfrep_right_right_divisor_equivalent. ((exists pfrep_position_right_divisor_equivalentfirst. ((pfrep_position_right_divisor_equivalentfirst+S (pfrep_power_right_divisor_equivalent)=(D)) /\ ((((exists ff_h_pfp_right_divisor_equivalentfirstentry. ff_h_pfp_right_divisor_equivalentfirstentry + S (pfrep_left_right_divisor_equivalent) = S ((S (pfrep_position_right_divisor_equivalentfirst)) * dc)) /\ exists ff_q_pfp_right_divisor_equivalentfirstentry. db = ff_q_pfp_right_divisor_equivalentfirstentry * S ((S (pfrep_position_right_divisor_equivalentfirst)) * dc) + (pfrep_left_right_divisor_equivalent)))))) \/ (((exists pfrep_gap_right_divisor_equivalentfirstoutside. pfrep_gap_right_divisor_equivalentfirstoutside+(D)=(pfrep_power_right_divisor_equivalent)) /\ (((pfrep_left_right_divisor_equivalent)=0))))) -> ((exists pfrep_position_right_divisor_equivalentsecond. ((pfrep_position_right_divisor_equivalentsecond+S (pfrep_power_right_divisor_equivalent)=(E)) /\ ((((exists ff_h_pfp_right_divisor_equivalentsecondentry. ff_h_pfp_right_divisor_equivalentsecondentry + S (pfrep_right_right_divisor_equivalent) = S ((S (pfrep_position_right_divisor_equivalentsecond)) * ec)) /\ exists ff_q_pfp_right_divisor_equivalentsecondentry. eb = ff_q_pfp_right_divisor_equivalentsecondentry * S ((S (pfrep_position_right_divisor_equivalentsecond)) * ec) + (pfrep_right_right_divisor_equivalent)))))) \/ (((exists pfrep_gap_right_divisor_equivalentsecondoutside. pfrep_gap_right_divisor_equivalentsecondoutside+(E)=(pfrep_power_right_divisor_equivalent)) /\ (((pfrep_right_right_divisor_equivalent)=0))))) -> pfrep_left_right_divisor_equivalent=pfrep_right_right_divisor_equivalent) -> (((forall fom_index_pfp_right_divisor_source_canonical. (exists fom_gap_pfp_right_divisor_source_canonical_index_bound. fom_gap_pfp_right_divisor_source_canonical_index_bound + S (fom_index_pfp_right_divisor_source_canonical) = L) -> exists fom_value_pfp_right_divisor_source_canonical. ((((exists fom_beta_height_pfp_right_divisor_source_canonical_entry. fom_beta_height_pfp_right_divisor_source_canonical_entry + S (fom_value_pfp_right_divisor_source_canonical) = S ((S (fom_index_pfp_right_divisor_source_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_divisor_source_canonical_entry. ab = fom_beta_quotient_pfp_right_divisor_source_canonical_entry * S ((S (fom_index_pfp_right_divisor_source_canonical)) * ac) + (fom_value_pfp_right_divisor_source_canonical))) /\ (exists fom_gap_pfp_right_divisor_source_canonical_value_bound. fom_gap_pfp_right_divisor_source_canonical_value_bound + S (fom_value_pfp_right_divisor_source_canonical) = p))) /\ ((exists pfrd_qb_right_divisor_source pfrd_qc_right_divisor_source pfrd_qlen_right_divisor_source pfrd_pb_right_divisor_source pfrd_pc_right_divisor_source pfrd_plen_right_divisor_source. ((((forall fom_index_pfp_right_divisor_source_productleft. (exists fom_gap_pfp_right_divisor_source_productleft_index_bound. fom_gap_pfp_right_divisor_source_productleft_index_bound + S (fom_index_pfp_right_divisor_source_productleft) = pfrd_qlen_right_divisor_source) -> exists fom_value_pfp_right_divisor_source_productleft. ((((exists fom_beta_height_pfp_right_divisor_source_productleft_entry. fom_beta_height_pfp_right_divisor_source_productleft_entry + S (fom_value_pfp_right_divisor_source_productleft) = S ((S (fom_index_pfp_right_divisor_source_productleft)) * pfrd_qc_right_divisor_source)) /\ exists fom_beta_quotient_pfp_right_divisor_source_productleft_entry. pfrd_qb_right_divisor_source = fom_beta_quotient_pfp_right_divisor_source_productleft_entry * S ((S (fom_index_pfp_right_divisor_source_productleft)) * pfrd_qc_right_divisor_source) + (fom_value_pfp_right_divisor_source_productleft))) /\ (exists fom_gap_pfp_right_divisor_source_productleft_value_bound. fom_gap_pfp_right_divisor_source_productleft_value_bound + S (fom_value_pfp_right_divisor_source_productleft) = p))) /\ (((forall fom_index_pfp_right_divisor_source_productright. (exists fom_gap_pfp_right_divisor_source_productright_index_bound. fom_gap_pfp_right_divisor_source_productright_index_bound + S (fom_index_pfp_right_divisor_source_productright) = D) -> exists fom_value_pfp_right_divisor_source_productright. ((((exists fom_beta_height_pfp_right_divisor_source_productright_entry. fom_beta_height_pfp_right_divisor_source_productright_entry + S (fom_value_pfp_right_divisor_source_productright) = S ((S (fom_index_pfp_right_divisor_source_productright)) * dc)) /\ exists fom_beta_quotient_pfp_right_divisor_source_productright_entry. db = fom_beta_quotient_pfp_right_divisor_source_productright_entry * S ((S (fom_index_pfp_right_divisor_source_productright)) * dc) + (fom_value_pfp_right_divisor_source_productright))) /\ (exists fom_gap_pfp_right_divisor_source_productright_value_bound. fom_gap_pfp_right_divisor_source_productright_value_bound + S (fom_value_pfp_right_divisor_source_productright) = p))) /\ (((((((pfrd_qlen_right_divisor_source)=0 \/ (D)=0) /\ (((pfrd_plen_right_divisor_source)=0)))) \/ (((~((pfrd_qlen_right_divisor_source)=0)) /\ (((~((D)=0)) /\ (((pfrd_qlen_right_divisor_source)+(D)=S (pfrd_plen_right_divisor_source)))))))) /\ ((forall pfc_index_right_divisor_source_productcoefficients. (exists pfa_gap_right_divisor_source_productcoefficientsbound. pfa_gap_right_divisor_source_productcoefficientsbound + S (pfc_index_right_divisor_source_productcoefficients) = (pfrd_plen_right_divisor_source)) -> exists pfc_value_right_divisor_source_productcoefficients. ((((exists ff_h_pfp_right_divisor_source_productcoefficientsentry. ff_h_pfp_right_divisor_source_productcoefficientsentry + S (pfc_value_right_divisor_source_productcoefficients) = S ((S (pfc_index_right_divisor_source_productcoefficients)) * pfrd_pc_right_divisor_source)) /\ exists ff_q_pfp_right_divisor_source_productcoefficientsentry. pfrd_pb_right_divisor_source = ff_q_pfp_right_divisor_source_productcoefficientsentry * S ((S (pfc_index_right_divisor_source_productcoefficients)) * pfrd_pc_right_divisor_source) + (pfc_value_right_divisor_source_productcoefficients))) /\ ((exists pfc_terms_code_right_divisor_source_productcoefficientscoefficient pfc_terms_scale_right_divisor_source_productcoefficientscoefficient pfc_natural_sum_right_divisor_source_productcoefficientscoefficient. ((forall pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonalbound. pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_divisor_source_productcoefficients))) -> exists pfc_value_right_divisor_source_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_divisor_source_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_source_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_divisor_source_productcoefficientscoefficient = ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_source_productcoefficientscoefficient) + (pfc_value_right_divisor_source_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm pfc_left_right_divisor_source_productcoefficientscoefficientdiagonalterm pfc_right_right_divisor_source_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)+pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm=(pfc_index_right_divisor_source_productcoefficients)) /\ ((((((exists pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_divisor_source)) /\ ((((exists ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_divisor_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_source)) /\ exists ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_divisor_source = ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_source) + (pfc_left_right_divisor_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_divisor_source)=(pfc_index_right_divisor_source_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_divisor_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_divisor_source_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_right_divisor_source_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_right_divisor_source_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_divisor_source_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_right_divisor_source_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_divisor_source_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_divisor_source_productcoefficientscoefficientdiagonal)=pfc_left_right_divisor_source_productcoefficientscoefficientdiagonalterm*pfc_right_right_divisor_source_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_divisor_source_productcoefficientscoefficientsum fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_divisor_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_divisor_source_productcoefficientscoefficient) = S ((S (S (pfc_index_right_divisor_source_productcoefficients))) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_divisor_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_divisor_source_productcoefficients))) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum) + (pfc_natural_sum_right_divisor_source_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_divisor_source_productcoefficients)) -> exists fs_a_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_source_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_divisor_source_productcoefficientscoefficient = fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_source_productcoefficientscoefficient) + (fs_a_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_divisor_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum) + (fs_r_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_divisor_source_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_source_productcoefficientscoefficientsum) + (fs_s_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_divisor_source_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_divisor_source_productcoefficientscoefficientresiduebound. pfa_gap_right_divisor_source_productcoefficientscoefficientresiduebound + S (pfc_value_right_divisor_source_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_divisor_source_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_divisor_source_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_divisor_source_productcoefficientscoefficient) + (p) * pfa_offset_left_right_divisor_source_productcoefficientscoefficientresiduecongruence = (pfc_value_right_divisor_source_productcoefficients) + (p) * pfa_offset_right_right_divisor_source_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_divisor_source_target pfrep_left_right_divisor_source_target pfrep_right_right_divisor_source_target. ((exists pfrep_position_right_divisor_source_targetfirst. ((pfrep_position_right_divisor_source_targetfirst+S (pfrep_power_right_divisor_source_target)=(pfrd_plen_right_divisor_source)) /\ ((((exists ff_h_pfp_right_divisor_source_targetfirstentry. ff_h_pfp_right_divisor_source_targetfirstentry + S (pfrep_left_right_divisor_source_target) = S ((S (pfrep_position_right_divisor_source_targetfirst)) * pfrd_pc_right_divisor_source)) /\ exists ff_q_pfp_right_divisor_source_targetfirstentry. pfrd_pb_right_divisor_source = ff_q_pfp_right_divisor_source_targetfirstentry * S ((S (pfrep_position_right_divisor_source_targetfirst)) * pfrd_pc_right_divisor_source) + (pfrep_left_right_divisor_source_target)))))) \/ (((exists pfrep_gap_right_divisor_source_targetfirstoutside. pfrep_gap_right_divisor_source_targetfirstoutside+(pfrd_plen_right_divisor_source)=(pfrep_power_right_divisor_source_target)) /\ (((pfrep_left_right_divisor_source_target)=0))))) -> ((exists pfrep_position_right_divisor_source_targetsecond. ((pfrep_position_right_divisor_source_targetsecond+S (pfrep_power_right_divisor_source_target)=(L)) /\ ((((exists ff_h_pfp_right_divisor_source_targetsecondentry. ff_h_pfp_right_divisor_source_targetsecondentry + S (pfrep_right_right_divisor_source_target) = S ((S (pfrep_position_right_divisor_source_targetsecond)) * ac)) /\ exists ff_q_pfp_right_divisor_source_targetsecondentry. ab = ff_q_pfp_right_divisor_source_targetsecondentry * S ((S (pfrep_position_right_divisor_source_targetsecond)) * ac) + (pfrep_right_right_divisor_source_target)))))) \/ (((exists pfrep_gap_right_divisor_source_targetsecondoutside. pfrep_gap_right_divisor_source_targetsecondoutside+(L)=(pfrep_power_right_divisor_source_target)) /\ (((pfrep_right_right_divisor_source_target)=0))))) -> pfrep_left_right_divisor_source_target=pfrep_right_right_divisor_source_target))))))) -> (((forall fom_index_pfp_right_divisor_result_canonical. (exists fom_gap_pfp_right_divisor_result_canonical_index_bound. fom_gap_pfp_right_divisor_result_canonical_index_bound + S (fom_index_pfp_right_divisor_result_canonical) = L) -> exists fom_value_pfp_right_divisor_result_canonical. ((((exists fom_beta_height_pfp_right_divisor_result_canonical_entry. fom_beta_height_pfp_right_divisor_result_canonical_entry + S (fom_value_pfp_right_divisor_result_canonical) = S ((S (fom_index_pfp_right_divisor_result_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_right_divisor_result_canonical_entry. ab = fom_beta_quotient_pfp_right_divisor_result_canonical_entry * S ((S (fom_index_pfp_right_divisor_result_canonical)) * ac) + (fom_value_pfp_right_divisor_result_canonical))) /\ (exists fom_gap_pfp_right_divisor_result_canonical_value_bound. fom_gap_pfp_right_divisor_result_canonical_value_bound + S (fom_value_pfp_right_divisor_result_canonical) = p))) /\ ((exists pfrd_qb_right_divisor_result pfrd_qc_right_divisor_result pfrd_qlen_right_divisor_result pfrd_pb_right_divisor_result pfrd_pc_right_divisor_result pfrd_plen_right_divisor_result. ((((forall fom_index_pfp_right_divisor_result_productleft. (exists fom_gap_pfp_right_divisor_result_productleft_index_bound. fom_gap_pfp_right_divisor_result_productleft_index_bound + S (fom_index_pfp_right_divisor_result_productleft) = pfrd_qlen_right_divisor_result) -> exists fom_value_pfp_right_divisor_result_productleft. ((((exists fom_beta_height_pfp_right_divisor_result_productleft_entry. fom_beta_height_pfp_right_divisor_result_productleft_entry + S (fom_value_pfp_right_divisor_result_productleft) = S ((S (fom_index_pfp_right_divisor_result_productleft)) * pfrd_qc_right_divisor_result)) /\ exists fom_beta_quotient_pfp_right_divisor_result_productleft_entry. pfrd_qb_right_divisor_result = fom_beta_quotient_pfp_right_divisor_result_productleft_entry * S ((S (fom_index_pfp_right_divisor_result_productleft)) * pfrd_qc_right_divisor_result) + (fom_value_pfp_right_divisor_result_productleft))) /\ (exists fom_gap_pfp_right_divisor_result_productleft_value_bound. fom_gap_pfp_right_divisor_result_productleft_value_bound + S (fom_value_pfp_right_divisor_result_productleft) = p))) /\ (((forall fom_index_pfp_right_divisor_result_productright. (exists fom_gap_pfp_right_divisor_result_productright_index_bound. fom_gap_pfp_right_divisor_result_productright_index_bound + S (fom_index_pfp_right_divisor_result_productright) = E) -> exists fom_value_pfp_right_divisor_result_productright. ((((exists fom_beta_height_pfp_right_divisor_result_productright_entry. fom_beta_height_pfp_right_divisor_result_productright_entry + S (fom_value_pfp_right_divisor_result_productright) = S ((S (fom_index_pfp_right_divisor_result_productright)) * ec)) /\ exists fom_beta_quotient_pfp_right_divisor_result_productright_entry. eb = fom_beta_quotient_pfp_right_divisor_result_productright_entry * S ((S (fom_index_pfp_right_divisor_result_productright)) * ec) + (fom_value_pfp_right_divisor_result_productright))) /\ (exists fom_gap_pfp_right_divisor_result_productright_value_bound. fom_gap_pfp_right_divisor_result_productright_value_bound + S (fom_value_pfp_right_divisor_result_productright) = p))) /\ (((((((pfrd_qlen_right_divisor_result)=0 \/ (E)=0) /\ (((pfrd_plen_right_divisor_result)=0)))) \/ (((~((pfrd_qlen_right_divisor_result)=0)) /\ (((~((E)=0)) /\ (((pfrd_qlen_right_divisor_result)+(E)=S (pfrd_plen_right_divisor_result)))))))) /\ ((forall pfc_index_right_divisor_result_productcoefficients. (exists pfa_gap_right_divisor_result_productcoefficientsbound. pfa_gap_right_divisor_result_productcoefficientsbound + S (pfc_index_right_divisor_result_productcoefficients) = (pfrd_plen_right_divisor_result)) -> exists pfc_value_right_divisor_result_productcoefficients. ((((exists ff_h_pfp_right_divisor_result_productcoefficientsentry. ff_h_pfp_right_divisor_result_productcoefficientsentry + S (pfc_value_right_divisor_result_productcoefficients) = S ((S (pfc_index_right_divisor_result_productcoefficients)) * pfrd_pc_right_divisor_result)) /\ exists ff_q_pfp_right_divisor_result_productcoefficientsentry. pfrd_pb_right_divisor_result = ff_q_pfp_right_divisor_result_productcoefficientsentry * S ((S (pfc_index_right_divisor_result_productcoefficients)) * pfrd_pc_right_divisor_result) + (pfc_value_right_divisor_result_productcoefficients))) /\ ((exists pfc_terms_code_right_divisor_result_productcoefficientscoefficient pfc_terms_scale_right_divisor_result_productcoefficientscoefficient pfc_natural_sum_right_divisor_result_productcoefficientscoefficient. ((forall pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal. (exists pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonalbound. pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonalbound + S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal) = (S (pfc_index_right_divisor_result_productcoefficients))) -> exists pfc_value_right_divisor_result_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonalentry. ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonalentry + S (pfc_value_right_divisor_result_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_result_productcoefficientscoefficient)) /\ exists ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonalentry. pfc_terms_code_right_divisor_result_productcoefficientscoefficient = ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_right_divisor_result_productcoefficientscoefficient) + (pfc_value_right_divisor_result_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm pfc_left_right_divisor_result_productcoefficientscoefficientdiagonalterm pfc_right_right_divisor_result_productcoefficientscoefficientdiagonalterm. (((pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)+pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm=(pfc_index_right_divisor_result_productcoefficients)) /\ ((((((exists pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal) = (pfrd_qlen_right_divisor_result)) /\ ((((exists ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_right_divisor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_result)) /\ exists ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermleftentry. pfrd_qb_right_divisor_result = ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)) * pfrd_qc_right_divisor_result) + (pfc_left_right_divisor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermleftoutside+(pfrd_qlen_right_divisor_result)=(pfc_index_right_divisor_result_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_right_divisor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm) = (E)) /\ ((((exists ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_right_divisor_result_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm)) * ec)) /\ exists ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermrightentry. eb = ff_q_pfp_right_divisor_result_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm)) * ec) + (pfc_right_right_divisor_result_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_right_divisor_result_productcoefficientscoefficientdiagonaltermrightoutside+(E)=(pfc_complement_right_divisor_result_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_right_divisor_result_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_right_divisor_result_productcoefficientscoefficientdiagonal)=pfc_left_right_divisor_result_productcoefficientscoefficientdiagonalterm*pfc_right_right_divisor_result_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_right_divisor_result_productcoefficientscoefficientsum fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum. ((((exists fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_start. fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_start. fs_u_pfc_right_divisor_result_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_right_divisor_result_productcoefficientscoefficient) = S ((S (S (pfc_index_right_divisor_result_productcoefficients))) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_right_divisor_result_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_right_divisor_result_productcoefficients))) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum) + (pfc_natural_sum_right_divisor_result_productcoefficientscoefficient))) /\ forall fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps = S (pfc_index_right_divisor_result_productcoefficients)) -> exists fs_a_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps fs_r_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps fs_s_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_result_productcoefficientscoefficient)) /\ exists fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_right_divisor_result_productcoefficientscoefficient = fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_right_divisor_result_productcoefficientscoefficient) + (fs_a_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_right_divisor_result_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum) + (fs_r_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_right_divisor_result_productcoefficientscoefficientsum = fs_q_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_right_divisor_result_productcoefficientscoefficientsum) + (fs_s_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps = fs_r_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps + fs_a_pfc_right_divisor_result_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_right_divisor_result_productcoefficientscoefficientresiduebound. pfa_gap_right_divisor_result_productcoefficientscoefficientresiduebound + S (pfc_value_right_divisor_result_productcoefficients) = (p)) /\ ((exists pfa_offset_left_right_divisor_result_productcoefficientscoefficientresiduecongruence pfa_offset_right_right_divisor_result_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_right_divisor_result_productcoefficientscoefficient) + (p) * pfa_offset_left_right_divisor_result_productcoefficientscoefficientresiduecongruence = (pfc_value_right_divisor_result_productcoefficients) + (p) * pfa_offset_right_right_divisor_result_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_right_divisor_result_target pfrep_left_right_divisor_result_target pfrep_right_right_divisor_result_target. ((exists pfrep_position_right_divisor_result_targetfirst. ((pfrep_position_right_divisor_result_targetfirst+S (pfrep_power_right_divisor_result_target)=(pfrd_plen_right_divisor_result)) /\ ((((exists ff_h_pfp_right_divisor_result_targetfirstentry. ff_h_pfp_right_divisor_result_targetfirstentry + S (pfrep_left_right_divisor_result_target) = S ((S (pfrep_position_right_divisor_result_targetfirst)) * pfrd_pc_right_divisor_result)) /\ exists ff_q_pfp_right_divisor_result_targetfirstentry. pfrd_pb_right_divisor_result = ff_q_pfp_right_divisor_result_targetfirstentry * S ((S (pfrep_position_right_divisor_result_targetfirst)) * pfrd_pc_right_divisor_result) + (pfrep_left_right_divisor_result_target)))))) \/ (((exists pfrep_gap_right_divisor_result_targetfirstoutside. pfrep_gap_right_divisor_result_targetfirstoutside+(pfrd_plen_right_divisor_result)=(pfrep_power_right_divisor_result_target)) /\ (((pfrep_left_right_divisor_result_target)=0))))) -> ((exists pfrep_position_right_divisor_result_targetsecond. ((pfrep_position_right_divisor_result_targetsecond+S (pfrep_power_right_divisor_result_target)=(L)) /\ ((((exists ff_h_pfp_right_divisor_result_targetsecondentry. ff_h_pfp_right_divisor_result_targetsecondentry + S (pfrep_right_right_divisor_result_target) = S ((S (pfrep_position_right_divisor_result_targetsecond)) * ac)) /\ exists ff_q_pfp_right_divisor_result_targetsecondentry. ab = ff_q_pfp_right_divisor_result_targetsecondentry * S ((S (pfrep_position_right_divisor_result_targetsecond)) * ac) + (pfrep_right_right_divisor_result_target)))))) \/ (((exists pfrep_gap_right_divisor_result_targetsecondoutside. pfrep_gap_right_divisor_result_targetsecondoutside+(L)=(pfrep_power_right_divisor_result_target)) /\ (((pfrep_right_right_divisor_result_target)=0))))) -> pfrep_left_right_divisor_result_target=pfrep_right_right_divisor_result_target)))))))

Complete tactic proof in conservative notation

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

103 script commands · 16 reading checkpoints · 3 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 (1)

prime field polynomial right divides from product

01Fix variables and assumptionsL1–10

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

L1
intro p
L2
intro db
L3
intro dc
L4
intro D
L5
intro ab
L6
intro ac
L7
intro L
L8
intro eb
L9
intro ec
L10
intro E

02Fix variables and assumptionsL11–14

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

L11
intro hp0
L12
intro hE
L13
intro hequivalent
L14
intro hdivides

03Separate the logical casesL15–22

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

L15
cases hdivides
L16
cases hdivides_right
L17
cases hdivides_right_witness
L18
cases hdivides_right_witness_witness
L19
cases hdivides_right_witness_witness_witness
L20
cases hdivides_right_witness_witness_witness_witness
L21
cases hdivides_right_witness_witness_witness_witness_witness
L22
cases hdivides_right_witness_witness_witness_witness_witness_witness

04Establish hsourceL23–24

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

L23
have hsource : FpPolyProduct(p,x,x1,x2,db,dc,D,x3,x4,x5)Definitions: FpPolyProduct(p,x,x1,x2,db,dc,D,x3,x4,x5)Original native command in the exact edition
L24
exact hdivides_right_witness_witness_witness_witness_witness_witness_left

05Separate the logical casesL25–27

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

L25
cases hsource
L26
cases hsource_right
L27
cases hsource_right_right

06Establish hnew_lengthL28–31

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

L28
have hnew_length : ∃ n. PolynomialProductLength(x2,E,n)Definitions: PolynomialProductLength(x2,E,n)Original native command in the exact edition
L29
specialize polynomial_product_length_exists (x2)
L30
specialize polynomial_product_length_exists (E)
L31
apply polynomial_product_length_exists

07Separate the logical casesL32–32

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

L32
cases hnew_length

08Establish hnew_productL33–42

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.

L33
have hnew_product : ∃ b. ∃ c. FpPolyProduct(p,x,x1,x2,eb,ec,E,b,c,x6)Definitions: FpPolyProduct(p,x,x1,x2,eb,ec,E,b,c,x6)Original native command in the exact edition
L34
specialize prime_field_polynomial_convolution_at_length_exists (p)
L35
specialize prime_field_polynomial_convolution_at_length_exists (x)
L36
specialize prime_field_polynomial_convolution_at_length_exists (x1)
L37
specialize prime_field_polynomial_convolution_at_length_exists (x2)
L38
specialize prime_field_polynomial_convolution_at_length_exists (eb)
L39
specialize prime_field_polynomial_convolution_at_length_exists (ec)
L40
specialize prime_field_polynomial_convolution_at_length_exists (E)
L41
specialize prime_field_polynomial_convolution_at_length_exists (x6)
L42
apply prime_field_polynomial_convolution_at_length_exists

09Use earlier factsL43–46