PG0073

prime_field_polynomial_monic_equal_degree_right_divides_equivalent

Equal-degree monic right divisibility has a genuinely constructed degree-zero quotient. Its head must be one, so divisor and target are formally equivalent.

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. ∀ ab. ∀ ac. ∀ d. Prime(p) → FpMonic(p,db,dc,S d) → FpMonic(p,ab,ac,S d) → FpPolynomialRightDivides(p,db,dc,S d,ab,ac,S d) → PolynomialEquivalent(db,dc,S d,ab,ac,S d)

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

Definition DAG

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2FpRepresentedDegree(p,b,c,L,d) · 3FpMonic(p,b,c,L) · 2PolynomialEquivalent(b,c,L,d,e,M) · 2FpPolynomialRightDivides(p,db,dc,D,ab,ac,L) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_monic_represented_degree · checked external prerequisiteprime_field_polynomial_right_divides_represented_factorizationadd_right_cancel · checked external prerequisitezero_add · checked external prerequisiteprime_field_polynomial_monic_singleton_multiple_equivalent
Original expanded first-order statement 
forall p db dc ab ac d. (~((p) = 1) /\ forall pfa_factor_left_monic_degree_prime pfa_factor_right_monic_degree_prime. (p) = pfa_factor_left_monic_degree_prime * pfa_factor_right_monic_degree_prime -> pfa_factor_left_monic_degree_prime = 1 \/ pfa_factor_right_monic_degree_prime = 1) -> (((~((S d) = 0)) /\ (((forall fom_index_pfp_monic_degree_Dcoefficients. (exists fom_gap_pfp_monic_degree_Dcoefficients_index_bound. fom_gap_pfp_monic_degree_Dcoefficients_index_bound + S (fom_index_pfp_monic_degree_Dcoefficients) = S d) -> exists fom_value_pfp_monic_degree_Dcoefficients. ((((exists fom_beta_height_pfp_monic_degree_Dcoefficients_entry. fom_beta_height_pfp_monic_degree_Dcoefficients_entry + S (fom_value_pfp_monic_degree_Dcoefficients) = S ((S (fom_index_pfp_monic_degree_Dcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_Dcoefficients_entry. db = fom_beta_quotient_pfp_monic_degree_Dcoefficients_entry * S ((S (fom_index_pfp_monic_degree_Dcoefficients)) * dc) + (fom_value_pfp_monic_degree_Dcoefficients))) /\ (exists fom_gap_pfp_monic_degree_Dcoefficients_value_bound. fom_gap_pfp_monic_degree_Dcoefficients_value_bound + S (fom_value_pfp_monic_degree_Dcoefficients) = p))) /\ ((((exists ff_h_pfp_monic_degree_Dleading. ff_h_pfp_monic_degree_Dleading + S (1) = S ((S (0)) * dc)) /\ exists ff_q_pfp_monic_degree_Dleading. db = ff_q_pfp_monic_degree_Dleading * S ((S (0)) * dc) + (1)))))))) -> (((~((S d) = 0)) /\ (((forall fom_index_pfp_monic_degree_Acoefficients. (exists fom_gap_pfp_monic_degree_Acoefficients_index_bound. fom_gap_pfp_monic_degree_Acoefficients_index_bound + S (fom_index_pfp_monic_degree_Acoefficients) = S d) -> exists fom_value_pfp_monic_degree_Acoefficients. ((((exists fom_beta_height_pfp_monic_degree_Acoefficients_entry. fom_beta_height_pfp_monic_degree_Acoefficients_entry + S (fom_value_pfp_monic_degree_Acoefficients) = S ((S (fom_index_pfp_monic_degree_Acoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_monic_degree_Acoefficients_entry. ab = fom_beta_quotient_pfp_monic_degree_Acoefficients_entry * S ((S (fom_index_pfp_monic_degree_Acoefficients)) * ac) + (fom_value_pfp_monic_degree_Acoefficients))) /\ (exists fom_gap_pfp_monic_degree_Acoefficients_value_bound. fom_gap_pfp_monic_degree_Acoefficients_value_bound + S (fom_value_pfp_monic_degree_Acoefficients) = p))) /\ ((((exists ff_h_pfp_monic_degree_Aleading. ff_h_pfp_monic_degree_Aleading + S (1) = S ((S (0)) * ac)) /\ exists ff_q_pfp_monic_degree_Aleading. ab = ff_q_pfp_monic_degree_Aleading * S ((S (0)) * ac) + (1)))))))) -> (((forall fom_index_pfp_monic_degree_RD_canonical. (exists fom_gap_pfp_monic_degree_RD_canonical_index_bound. fom_gap_pfp_monic_degree_RD_canonical_index_bound + S (fom_index_pfp_monic_degree_RD_canonical) = S d) -> exists fom_value_pfp_monic_degree_RD_canonical. ((((exists fom_beta_height_pfp_monic_degree_RD_canonical_entry. fom_beta_height_pfp_monic_degree_RD_canonical_entry + S (fom_value_pfp_monic_degree_RD_canonical) = S ((S (fom_index_pfp_monic_degree_RD_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_canonical_entry. ab = fom_beta_quotient_pfp_monic_degree_RD_canonical_entry * S ((S (fom_index_pfp_monic_degree_RD_canonical)) * ac) + (fom_value_pfp_monic_degree_RD_canonical))) /\ (exists fom_gap_pfp_monic_degree_RD_canonical_value_bound. fom_gap_pfp_monic_degree_RD_canonical_value_bound + S (fom_value_pfp_monic_degree_RD_canonical) = p))) /\ ((exists pfgu_qb_monic_degree_RD pfgu_qc_monic_degree_RD pfgu_Q_monic_degree_RD pfgu_pb_monic_degree_RD pfgu_pc_monic_degree_RD pfgu_P_monic_degree_RD. ((((forall fom_index_pfp_monic_degree_RD_productleft. (exists fom_gap_pfp_monic_degree_RD_productleft_index_bound. fom_gap_pfp_monic_degree_RD_productleft_index_bound + S (fom_index_pfp_monic_degree_RD_productleft) = pfgu_Q_monic_degree_RD) -> exists fom_value_pfp_monic_degree_RD_productleft. ((((exists fom_beta_height_pfp_monic_degree_RD_productleft_entry. fom_beta_height_pfp_monic_degree_RD_productleft_entry + S (fom_value_pfp_monic_degree_RD_productleft) = S ((S (fom_index_pfp_monic_degree_RD_productleft)) * pfgu_qc_monic_degree_RD)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_productleft_entry. pfgu_qb_monic_degree_RD = fom_beta_quotient_pfp_monic_degree_RD_productleft_entry * S ((S (fom_index_pfp_monic_degree_RD_productleft)) * pfgu_qc_monic_degree_RD) + (fom_value_pfp_monic_degree_RD_productleft))) /\ (exists fom_gap_pfp_monic_degree_RD_productleft_value_bound. fom_gap_pfp_monic_degree_RD_productleft_value_bound + S (fom_value_pfp_monic_degree_RD_productleft) = p))) /\ (((forall fom_index_pfp_monic_degree_RD_productright. (exists fom_gap_pfp_monic_degree_RD_productright_index_bound. fom_gap_pfp_monic_degree_RD_productright_index_bound + S (fom_index_pfp_monic_degree_RD_productright) = S d) -> exists fom_value_pfp_monic_degree_RD_productright. ((((exists fom_beta_height_pfp_monic_degree_RD_productright_entry. fom_beta_height_pfp_monic_degree_RD_productright_entry + S (fom_value_pfp_monic_degree_RD_productright) = S ((S (fom_index_pfp_monic_degree_RD_productright)) * dc)) /\ exists fom_beta_quotient_pfp_monic_degree_RD_productright_entry. db = fom_beta_quotient_pfp_monic_degree_RD_productright_entry * S ((S (fom_index_pfp_monic_degree_RD_productright)) * dc) + (fom_value_pfp_monic_degree_RD_productright))) /\ (exists fom_gap_pfp_monic_degree_RD_productright_value_bound. fom_gap_pfp_monic_degree_RD_productright_value_bound + S (fom_value_pfp_monic_degree_RD_productright) = p))) /\ (((((((pfgu_Q_monic_degree_RD)=0 \/ (S d)=0) /\ (((pfgu_P_monic_degree_RD)=0)))) \/ (((~((pfgu_Q_monic_degree_RD)=0)) /\ (((~((S d)=0)) /\ (((pfgu_Q_monic_degree_RD)+(S d)=S (pfgu_P_monic_degree_RD)))))))) /\ ((forall pfc_index_monic_degree_RD_productcoefficients. (exists pfa_gap_monic_degree_RD_productcoefficientsbound. pfa_gap_monic_degree_RD_productcoefficientsbound + S (pfc_index_monic_degree_RD_productcoefficients) = (pfgu_P_monic_degree_RD)) -> exists pfc_value_monic_degree_RD_productcoefficients. ((((exists ff_h_pfp_monic_degree_RD_productcoefficientsentry. ff_h_pfp_monic_degree_RD_productcoefficientsentry + S (pfc_value_monic_degree_RD_productcoefficients) = S ((S (pfc_index_monic_degree_RD_productcoefficients)) * pfgu_pc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientsentry. pfgu_pb_monic_degree_RD = ff_q_pfp_monic_degree_RD_productcoefficientsentry * S ((S (pfc_index_monic_degree_RD_productcoefficients)) * pfgu_pc_monic_degree_RD) + (pfc_value_monic_degree_RD_productcoefficients))) /\ ((exists pfc_terms_code_monic_degree_RD_productcoefficientscoefficient pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient. ((forall pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal. (exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonalbound. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonalbound + S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal) = (S (pfc_index_monic_degree_RD_productcoefficients))) -> exists pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry + S (pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry. pfc_terms_code_monic_degree_RD_productcoefficientscoefficient = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient) + (pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm. (((pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)+pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm=(pfc_index_monic_degree_RD_productcoefficients)) /\ ((((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal) = (pfgu_Q_monic_degree_RD)) /\ ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_monic_degree_RD = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) * pfgu_qc_monic_degree_RD) + (pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_monic_degree_RD)=(pfc_index_monic_degree_RD_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_monic_degree_RD_productcoefficientscoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_monic_degree_RD_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_monic_degree_RD_productcoefficientscoefficientdiagonal)=pfc_left_monic_degree_RD_productcoefficientscoefficientdiagonalterm*pfc_right_monic_degree_RD_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum. ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient) = S ((S (S (pfc_index_monic_degree_RD_productcoefficients))) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_monic_degree_RD_productcoefficients))) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient))) /\ forall fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps = S (pfc_index_monic_degree_RD_productcoefficients)) -> exists fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_monic_degree_RD_productcoefficientscoefficient = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_monic_degree_RD_productcoefficientscoefficient) + (fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_monic_degree_RD_productcoefficientscoefficientsum = fs_q_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_monic_degree_RD_productcoefficientscoefficientsum) + (fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps = fs_r_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps + fs_a_pfc_monic_degree_RD_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_monic_degree_RD_productcoefficientscoefficientresiduebound. pfa_gap_monic_degree_RD_productcoefficientscoefficientresiduebound + S (pfc_value_monic_degree_RD_productcoefficients) = (p)) /\ ((exists pfa_offset_left_monic_degree_RD_productcoefficientscoefficientresiduecongruence pfa_offset_right_monic_degree_RD_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_monic_degree_RD_productcoefficientscoefficient) + (p) * pfa_offset_left_monic_degree_RD_productcoefficientscoefficientresiduecongruence = (pfc_value_monic_degree_RD_productcoefficients) + (p) * pfa_offset_right_monic_degree_RD_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_monic_degree_RD_target pfrep_left_monic_degree_RD_target pfrep_right_monic_degree_RD_target. ((exists pfrep_position_monic_degree_RD_targetfirst. ((pfrep_position_monic_degree_RD_targetfirst+S (pfrep_power_monic_degree_RD_target)=(pfgu_P_monic_degree_RD)) /\ ((((exists ff_h_pfp_monic_degree_RD_targetfirstentry. ff_h_pfp_monic_degree_RD_targetfirstentry + S (pfrep_left_monic_degree_RD_target) = S ((S (pfrep_position_monic_degree_RD_targetfirst)) * pfgu_pc_monic_degree_RD)) /\ exists ff_q_pfp_monic_degree_RD_targetfirstentry. pfgu_pb_monic_degree_RD = ff_q_pfp_monic_degree_RD_targetfirstentry * S ((S (pfrep_position_monic_degree_RD_targetfirst)) * pfgu_pc_monic_degree_RD) + (pfrep_left_monic_degree_RD_target)))))) \/ (((exists pfrep_gap_monic_degree_RD_targetfirstoutside. pfrep_gap_monic_degree_RD_targetfirstoutside+(pfgu_P_monic_degree_RD)=(pfrep_power_monic_degree_RD_target)) /\ (((pfrep_left_monic_degree_RD_target)=0))))) -> ((exists pfrep_position_monic_degree_RD_targetsecond. ((pfrep_position_monic_degree_RD_targetsecond+S (pfrep_power_monic_degree_RD_target)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_RD_targetsecondentry. ff_h_pfp_monic_degree_RD_targetsecondentry + S (pfrep_right_monic_degree_RD_target) = S ((S (pfrep_position_monic_degree_RD_targetsecond)) * ac)) /\ exists ff_q_pfp_monic_degree_RD_targetsecondentry. ab = ff_q_pfp_monic_degree_RD_targetsecondentry * S ((S (pfrep_position_monic_degree_RD_targetsecond)) * ac) + (pfrep_right_monic_degree_RD_target)))))) \/ (((exists pfrep_gap_monic_degree_RD_targetsecondoutside. pfrep_gap_monic_degree_RD_targetsecondoutside+(S d)=(pfrep_power_monic_degree_RD_target)) /\ (((pfrep_right_monic_degree_RD_target)=0))))) -> pfrep_left_monic_degree_RD_target=pfrep_right_monic_degree_RD_target))))))) -> (forall pfrep_power_monic_degree_result pfrep_left_monic_degree_result pfrep_right_monic_degree_result. ((exists pfrep_position_monic_degree_resultfirst. ((pfrep_position_monic_degree_resultfirst+S (pfrep_power_monic_degree_result)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_resultfirstentry. ff_h_pfp_monic_degree_resultfirstentry + S (pfrep_left_monic_degree_result) = S ((S (pfrep_position_monic_degree_resultfirst)) * dc)) /\ exists ff_q_pfp_monic_degree_resultfirstentry. db = ff_q_pfp_monic_degree_resultfirstentry * S ((S (pfrep_position_monic_degree_resultfirst)) * dc) + (pfrep_left_monic_degree_result)))))) \/ (((exists pfrep_gap_monic_degree_resultfirstoutside. pfrep_gap_monic_degree_resultfirstoutside+(S d)=(pfrep_power_monic_degree_result)) /\ (((pfrep_left_monic_degree_result)=0))))) -> ((exists pfrep_position_monic_degree_resultsecond. ((pfrep_position_monic_degree_resultsecond+S (pfrep_power_monic_degree_result)=(S d)) /\ ((((exists ff_h_pfp_monic_degree_resultsecondentry. ff_h_pfp_monic_degree_resultsecondentry + S (pfrep_right_monic_degree_result) = S ((S (pfrep_position_monic_degree_resultsecond)) * ac)) /\ exists ff_q_pfp_monic_degree_resultsecondentry. ab = ff_q_pfp_monic_degree_resultsecondentry * S ((S (pfrep_position_monic_degree_resultsecond)) * ac) + (pfrep_right_monic_degree_result)))))) \/ (((exists pfrep_gap_monic_degree_resultsecondoutside. pfrep_gap_monic_degree_resultsecondoutside+(S d)=(pfrep_power_monic_degree_result)) /\ (((pfrep_right_monic_degree_result)=0))))) -> pfrep_left_monic_degree_result=pfrep_right_monic_degree_result)

Complete tactic proof in conservative notation

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

84 script commands · 10 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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

Named ingredients (2)
prime field polynomial right divides represented factorizationprime field polynomial monic singleton multiple equivalent
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 ab
  5. L5
    intro ac
  6. L6
    intro d
  7. L7
    intro hp
  8. L8
    intro hd
  9. L9
    intro ha
  10. L10
    intro hrd
02Establish hddL11–19

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

  1. L11
    have hdd : FpRepresentedDegree(p,db,dc,S d,d)Definitions: FpRepresentedDegree(p,db,dc,S d,d)Original native command in the exact edition
  2. L12
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L13
    specialize prime_field_polynomial_monic_represented_degree (db)
  4. L14
    specialize prime_field_polynomial_monic_represented_degree (dc)
  5. L15
    specialize prime_field_polynomial_monic_represented_degree (S d)
  6. L16
    specialize prime_field_polynomial_monic_represented_degree (d)
  7. L17
    apply prime_field_polynomial_monic_represented_degree
  8. L18
    exact hd
  9. L19
    refl
03Establish hadL20–28

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

  1. L20
    have had : FpRepresentedDegree(p,ab,ac,S d,d)Definitions: FpRepresentedDegree(p,ab,ac,S d,d)Original native command in the exact edition
  2. L21
    specialize prime_field_polynomial_monic_represented_degree (p)
  3. L22
    specialize prime_field_polynomial_monic_represented_degree (ab)
  4. L23
    specialize prime_field_polynomial_monic_represented_degree (ac)
  5. L24
    specialize prime_field_polynomial_monic_represented_degree (S d)
  6. L25
    specialize prime_field_polynomial_monic_represented_degree (d)
  7. L26
    apply prime_field_polynomial_monic_represented_degree
  8. L27
    exact ha
  9. L28
    refl
04Establish hfL29–38

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

  1. L29
    have hf · expand full local formula (607 characters)have hf : ∃ pfgu_qb_monic_degree_factor. ∃ pfgu_qc_monic_degree_factor. ∃ pfgu_e_monic_degree_factor. ∃ pfgu_pb_monic_degree_factor. ∃ pfgu_pc_monic_degree_factor. FpRepresentedDegree(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,pfgu_e_monic_degree_factor) ∧ (FpPolyProduct(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,db,dc,S d,pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d) ∧ (PolynomialEquivalent(pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d,ab,ac,S d) ∧ pfgu_e_monic_degree_factor + d = d))
    Definitions: FpRepresentedDegree(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,pfgu_e_monic_degree_factor)FpPolyProduct(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,db,dc,S d,pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d)PolynomialEquivalent(pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d,ab,ac,S d)Original native command in the exact edition
  2. L30
    specialize prime_field_polynomial_right_divides_represented_factorization (p)
  3. L31
    specialize prime_field_polynomial_right_divides_represented_factorization (db)
  4. L32
    specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  5. L33
    specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  6. L34
    specialize prime_field_polynomial_right_divides_represented_factorization (d)
  7. L35
    specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  8. L36
    specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  9. L37
    specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  10. L38
    specialize prime_field_polynomial_right_divides_represented_factorization (d)
05Use earlier factsL39–43

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

  1. L39
    apply prime_field_polynomial_right_divides_represented_factorization
  2. L40
    exact hp
  3. L41
    exact hdd
  4. L42
    exact had
  5. L43
    exact hrd
06Separate the logical casesL44–51

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

  1. L44
    cases hf
  2. L45
    cases hf_witness
  3. L46
    cases hf_witness_witness
  4. L47
    cases hf_witness_witness_witness
  5. L48
    cases hf_witness_witness_witness_witness
  6. L49
    cases hf_witness_witness_witness_witness_witness
  7. L50
    cases hf_witness_witness_witness_witness_witness_right
  8. L51
    cases hf_witness_witness_witness_witness_witness_right_right
07Establish hezeroL52–61

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

  1. L52
    have hezero : x2=0
  2. L53
    specialize add_right_cancel (x2)
  3. L54
    specialize add_right_cancel (0)
  4. L55
    specialize add_right_cancel (d)
  5. L56
    apply add_right_cancel
  6. L57
    trans d
  7. L58
    exact hf_witness_witness_witness_witness_witness_right_right_right
  8. L59
    symm
  9. L60
    apply zero_add
  10. L61
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (p)
08Use earlier factsL62–71

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

  1. L62
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x)
  2. L63
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x1)
  3. L64
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (db)
  4. L65
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (dc)
  5. L66
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ab)
  6. L67
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ac)
  7. L68
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (d)
  8. L69
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x3)
  9. L70
    specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x4)
  10. L71
    apply prime_field_polynomial_monic_singleton_multiple_equivalent
09Use earlier factsL72–74

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

  1. L72
    exact hp
  2. L73
    exact hd
  3. L74
    exact ha
10Establish hproductL75–84

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

  1. L75
    have hproduct : FpPolyProduct(p,x,x1,S x2,db,dc,S d,x3,x4,S d)Definitions: FpPolyProduct(p,x,x1,S x2,db,dc,S d,x3,x4,S d)Original native command in the exact edition
  2. L76
    exact hf_witness_witness_witness_witness_witness_right_left
  3. L77
    rewrite hezero at hproduct
  4. L78
    rewrite hezero at hproduct
  5. L79
    rewrite hezero at hproduct
  6. L80
    rewrite hezero at hproduct
  7. L81
    rewrite hezero at hproduct
  8. L82
    rewrite hezero at hproduct
  9. L83
    exact hproduct
  10. L84
    exact hf_witness_witness_witness_witness_witness_right_right_left

Library-wide reading audit

Original defined command ledger · 84 lines
  1. 0001intro p
  2. 0002intro db
  3. 0003intro dc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro d
  7. 0007intro hp
  8. 0008intro hd
  9. 0009intro ha
  10. 0010intro hrd
  11. 0011have hdd : FpRepresentedDegree(p,db,dc,S d,d)
  12. 0012specialize prime_field_polynomial_monic_represented_degree (p)
  13. 0013specialize prime_field_polynomial_monic_represented_degree (db)
  14. 0014specialize prime_field_polynomial_monic_represented_degree (dc)
  15. 0015specialize prime_field_polynomial_monic_represented_degree (S d)
  16. 0016specialize prime_field_polynomial_monic_represented_degree (d)
  17. 0017apply prime_field_polynomial_monic_represented_degree
  18. 0018exact hd
  19. 0019refl
  20. 0020have had : FpRepresentedDegree(p,ab,ac,S d,d)
  21. 0021specialize prime_field_polynomial_monic_represented_degree (p)
  22. 0022specialize prime_field_polynomial_monic_represented_degree (ab)
  23. 0023specialize prime_field_polynomial_monic_represented_degree (ac)
  24. 0024specialize prime_field_polynomial_monic_represented_degree (S d)
  25. 0025specialize prime_field_polynomial_monic_represented_degree (d)
  26. 0026apply prime_field_polynomial_monic_represented_degree
  27. 0027exact ha
  28. 0028refl
  29. 0029have hf : ∃ pfgu_qb_monic_degree_factor. ∃ pfgu_qc_monic_degree_factor. ∃ pfgu_e_monic_degree_factor. ∃ pfgu_pb_monic_degree_factor. ∃ pfgu_pc_monic_degree_factor. FpRepresentedDegree(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,pfgu_e_monic_degree_factor) ∧ (FpPolyProduct(p,pfgu_qb_monic_degree_factor,pfgu_qc_monic_degree_factor,S pfgu_e_monic_degree_factor,db,dc,S d,pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d) ∧ (PolynomialEquivalent(pfgu_pb_monic_degree_factor,pfgu_pc_monic_degree_factor,S d,ab,ac,S d) ∧ pfgu_e_monic_degree_factor + d = d))
  30. 0030specialize prime_field_polynomial_right_divides_represented_factorization (p)
  31. 0031specialize prime_field_polynomial_right_divides_represented_factorization (db)
  32. 0032specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  33. 0033specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  34. 0034specialize prime_field_polynomial_right_divides_represented_factorization (d)
  35. 0035specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  36. 0036specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  37. 0037specialize prime_field_polynomial_right_divides_represented_factorization (S d)
  38. 0038specialize prime_field_polynomial_right_divides_represented_factorization (d)
  39. 0039apply prime_field_polynomial_right_divides_represented_factorization
  40. 0040exact hp
  41. 0041exact hdd
  42. 0042exact had
  43. 0043exact hrd
  44. 0044cases hf
  45. 0045cases hf_witness
  46. 0046cases hf_witness_witness
  47. 0047cases hf_witness_witness_witness
  48. 0048cases hf_witness_witness_witness_witness
  49. 0049cases hf_witness_witness_witness_witness_witness
  50. 0050cases hf_witness_witness_witness_witness_witness_right
  51. 0051cases hf_witness_witness_witness_witness_witness_right_right
  52. 0052have hezero : x2=0
  53. 0053specialize add_right_cancel (x2)
  54. 0054specialize add_right_cancel (0)
  55. 0055specialize add_right_cancel (d)
  56. 0056apply add_right_cancel
  57. 0057trans d
  58. 0058exact hf_witness_witness_witness_witness_witness_right_right_right
  59. 0059symm
  60. 0060apply zero_add
  61. 0061specialize prime_field_polynomial_monic_singleton_multiple_equivalent (p)
  62. 0062specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x)
  63. 0063specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x1)
  64. 0064specialize prime_field_polynomial_monic_singleton_multiple_equivalent (db)
  65. 0065specialize prime_field_polynomial_monic_singleton_multiple_equivalent (dc)
  66. 0066specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ab)
  67. 0067specialize prime_field_polynomial_monic_singleton_multiple_equivalent (ac)
  68. 0068specialize prime_field_polynomial_monic_singleton_multiple_equivalent (d)
  69. 0069specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x3)
  70. 0070specialize prime_field_polynomial_monic_singleton_multiple_equivalent (x4)
  71. 0071apply prime_field_polynomial_monic_singleton_multiple_equivalent
  72. 0072exact hp
  73. 0073exact hd
  74. 0074exact ha
  75. 0075have hproduct : FpPolyProduct(p,x,x1,S x2,db,dc,S d,x3,x4,S d)
  76. 0076exact hf_witness_witness_witness_witness_witness_right_left
  77. 0077rewrite hezero at hproduct
  78. 0078rewrite hezero at hproduct
  79. 0079rewrite hezero at hproduct
  80. 0080rewrite hezero at hproduct
  81. 0081rewrite hezero at hproduct
  82. 0082rewrite hezero at hproduct
  83. 0083exact hproduct
  84. 0084exact hf_witness_witness_witness_witness_witness_right_right_left