PG0071

prime_field_polynomial_right_divides_represented_degree_bound

A nonzero represented right divisor has degree at most that of its nonzero represented multiple, using the actual retained quotient degree as the natural witness.

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) → Le(d,a)

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

Definition DAG

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

Actual proof prerequisites

prime_field_polynomial_right_divides_represented_factorization
Original expanded first-order statement 
forall p db dc D d ab ac L a. (~((p) = 1) /\ forall pfa_factor_left_bound_prime pfa_factor_right_bound_prime. (p) = pfa_factor_left_bound_prime * pfa_factor_right_bound_prime -> pfa_factor_left_bound_prime = 1 \/ pfa_factor_right_bound_prime = 1) -> ((((D)=S (d)) /\ (((forall fom_index_pfp_bound_divisorcoefficients. (exists fom_gap_pfp_bound_divisorcoefficients_index_bound. fom_gap_pfp_bound_divisorcoefficients_index_bound + S (fom_index_pfp_bound_divisorcoefficients) = D) -> exists fom_value_pfp_bound_divisorcoefficients. ((((exists fom_beta_height_pfp_bound_divisorcoefficients_entry. fom_beta_height_pfp_bound_divisorcoefficients_entry + S (fom_value_pfp_bound_divisorcoefficients) = S ((S (fom_index_pfp_bound_divisorcoefficients)) * dc)) /\ exists fom_beta_quotient_pfp_bound_divisorcoefficients_entry. db = fom_beta_quotient_pfp_bound_divisorcoefficients_entry * S ((S (fom_index_pfp_bound_divisorcoefficients)) * dc) + (fom_value_pfp_bound_divisorcoefficients))) /\ (exists fom_gap_pfp_bound_divisorcoefficients_value_bound. fom_gap_pfp_bound_divisorcoefficients_value_bound + S (fom_value_pfp_bound_divisorcoefficients) = p))) /\ ((exists pfd_leading_bound_divisor. ((((exists ff_h_pfp_bound_divisorentry. ff_h_pfp_bound_divisorentry + S (pfd_leading_bound_divisor) = S ((S (0)) * dc)) /\ exists ff_q_pfp_bound_divisorentry. db = ff_q_pfp_bound_divisorentry * S ((S (0)) * dc) + (pfd_leading_bound_divisor))) /\ ((~(pfd_leading_bound_divisor=0)))))))))) -> ((((L)=S (a)) /\ (((forall fom_index_pfp_bound_targetcoefficients. (exists fom_gap_pfp_bound_targetcoefficients_index_bound. fom_gap_pfp_bound_targetcoefficients_index_bound + S (fom_index_pfp_bound_targetcoefficients) = L) -> exists fom_value_pfp_bound_targetcoefficients. ((((exists fom_beta_height_pfp_bound_targetcoefficients_entry. fom_beta_height_pfp_bound_targetcoefficients_entry + S (fom_value_pfp_bound_targetcoefficients) = S ((S (fom_index_pfp_bound_targetcoefficients)) * ac)) /\ exists fom_beta_quotient_pfp_bound_targetcoefficients_entry. ab = fom_beta_quotient_pfp_bound_targetcoefficients_entry * S ((S (fom_index_pfp_bound_targetcoefficients)) * ac) + (fom_value_pfp_bound_targetcoefficients))) /\ (exists fom_gap_pfp_bound_targetcoefficients_value_bound. fom_gap_pfp_bound_targetcoefficients_value_bound + S (fom_value_pfp_bound_targetcoefficients) = p))) /\ ((exists pfd_leading_bound_target. ((((exists ff_h_pfp_bound_targetentry. ff_h_pfp_bound_targetentry + S (pfd_leading_bound_target) = S ((S (0)) * ac)) /\ exists ff_q_pfp_bound_targetentry. ab = ff_q_pfp_bound_targetentry * S ((S (0)) * ac) + (pfd_leading_bound_target))) /\ ((~(pfd_leading_bound_target=0)))))))))) -> (((forall fom_index_pfp_bound_divisibility_canonical. (exists fom_gap_pfp_bound_divisibility_canonical_index_bound. fom_gap_pfp_bound_divisibility_canonical_index_bound + S (fom_index_pfp_bound_divisibility_canonical) = L) -> exists fom_value_pfp_bound_divisibility_canonical. ((((exists fom_beta_height_pfp_bound_divisibility_canonical_entry. fom_beta_height_pfp_bound_divisibility_canonical_entry + S (fom_value_pfp_bound_divisibility_canonical) = S ((S (fom_index_pfp_bound_divisibility_canonical)) * ac)) /\ exists fom_beta_quotient_pfp_bound_divisibility_canonical_entry. ab = fom_beta_quotient_pfp_bound_divisibility_canonical_entry * S ((S (fom_index_pfp_bound_divisibility_canonical)) * ac) + (fom_value_pfp_bound_divisibility_canonical))) /\ (exists fom_gap_pfp_bound_divisibility_canonical_value_bound. fom_gap_pfp_bound_divisibility_canonical_value_bound + S (fom_value_pfp_bound_divisibility_canonical) = p))) /\ ((exists pfgu_qb_bound_divisibility pfgu_qc_bound_divisibility pfgu_Q_bound_divisibility pfgu_pb_bound_divisibility pfgu_pc_bound_divisibility pfgu_P_bound_divisibility. ((((forall fom_index_pfp_bound_divisibility_productleft. (exists fom_gap_pfp_bound_divisibility_productleft_index_bound. fom_gap_pfp_bound_divisibility_productleft_index_bound + S (fom_index_pfp_bound_divisibility_productleft) = pfgu_Q_bound_divisibility) -> exists fom_value_pfp_bound_divisibility_productleft. ((((exists fom_beta_height_pfp_bound_divisibility_productleft_entry. fom_beta_height_pfp_bound_divisibility_productleft_entry + S (fom_value_pfp_bound_divisibility_productleft) = S ((S (fom_index_pfp_bound_divisibility_productleft)) * pfgu_qc_bound_divisibility)) /\ exists fom_beta_quotient_pfp_bound_divisibility_productleft_entry. pfgu_qb_bound_divisibility = fom_beta_quotient_pfp_bound_divisibility_productleft_entry * S ((S (fom_index_pfp_bound_divisibility_productleft)) * pfgu_qc_bound_divisibility) + (fom_value_pfp_bound_divisibility_productleft))) /\ (exists fom_gap_pfp_bound_divisibility_productleft_value_bound. fom_gap_pfp_bound_divisibility_productleft_value_bound + S (fom_value_pfp_bound_divisibility_productleft) = p))) /\ (((forall fom_index_pfp_bound_divisibility_productright. (exists fom_gap_pfp_bound_divisibility_productright_index_bound. fom_gap_pfp_bound_divisibility_productright_index_bound + S (fom_index_pfp_bound_divisibility_productright) = D) -> exists fom_value_pfp_bound_divisibility_productright. ((((exists fom_beta_height_pfp_bound_divisibility_productright_entry. fom_beta_height_pfp_bound_divisibility_productright_entry + S (fom_value_pfp_bound_divisibility_productright) = S ((S (fom_index_pfp_bound_divisibility_productright)) * dc)) /\ exists fom_beta_quotient_pfp_bound_divisibility_productright_entry. db = fom_beta_quotient_pfp_bound_divisibility_productright_entry * S ((S (fom_index_pfp_bound_divisibility_productright)) * dc) + (fom_value_pfp_bound_divisibility_productright))) /\ (exists fom_gap_pfp_bound_divisibility_productright_value_bound. fom_gap_pfp_bound_divisibility_productright_value_bound + S (fom_value_pfp_bound_divisibility_productright) = p))) /\ (((((((pfgu_Q_bound_divisibility)=0 \/ (D)=0) /\ (((pfgu_P_bound_divisibility)=0)))) \/ (((~((pfgu_Q_bound_divisibility)=0)) /\ (((~((D)=0)) /\ (((pfgu_Q_bound_divisibility)+(D)=S (pfgu_P_bound_divisibility)))))))) /\ ((forall pfc_index_bound_divisibility_productcoefficients. (exists pfa_gap_bound_divisibility_productcoefficientsbound. pfa_gap_bound_divisibility_productcoefficientsbound + S (pfc_index_bound_divisibility_productcoefficients) = (pfgu_P_bound_divisibility)) -> exists pfc_value_bound_divisibility_productcoefficients. ((((exists ff_h_pfp_bound_divisibility_productcoefficientsentry. ff_h_pfp_bound_divisibility_productcoefficientsentry + S (pfc_value_bound_divisibility_productcoefficients) = S ((S (pfc_index_bound_divisibility_productcoefficients)) * pfgu_pc_bound_divisibility)) /\ exists ff_q_pfp_bound_divisibility_productcoefficientsentry. pfgu_pb_bound_divisibility = ff_q_pfp_bound_divisibility_productcoefficientsentry * S ((S (pfc_index_bound_divisibility_productcoefficients)) * pfgu_pc_bound_divisibility) + (pfc_value_bound_divisibility_productcoefficients))) /\ ((exists pfc_terms_code_bound_divisibility_productcoefficientscoefficient pfc_terms_scale_bound_divisibility_productcoefficientscoefficient pfc_natural_sum_bound_divisibility_productcoefficientscoefficient. ((forall pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal. (exists pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonalbound. pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonalbound + S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal) = (S (pfc_index_bound_divisibility_productcoefficients))) -> exists pfc_value_bound_divisibility_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonalentry + S (pfc_value_bound_divisibility_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bound_divisibility_productcoefficientscoefficient)) /\ exists ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bound_divisibility_productcoefficientscoefficient = ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bound_divisibility_productcoefficientscoefficient) + (pfc_value_bound_divisibility_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm pfc_left_bound_divisibility_productcoefficientscoefficientdiagonalterm pfc_right_bound_divisibility_productcoefficientscoefficientdiagonalterm. (((pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)+pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm=(pfc_index_bound_divisibility_productcoefficients)) /\ ((((((exists pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal) = (pfgu_Q_bound_divisibility)) /\ ((((exists ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bound_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_bound_divisibility)) /\ exists ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_bound_divisibility = ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)) * pfgu_qc_bound_divisibility) + (pfc_left_bound_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermleftoutside+(pfgu_Q_bound_divisibility)=(pfc_index_bound_divisibility_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bound_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bound_divisibility_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_bound_divisibility_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_bound_divisibility_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bound_divisibility_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_bound_divisibility_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bound_divisibility_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bound_divisibility_productcoefficientscoefficientdiagonal)=pfc_left_bound_divisibility_productcoefficientscoefficientdiagonalterm*pfc_right_bound_divisibility_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bound_divisibility_productcoefficientscoefficientsum fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_start. fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_start. fs_u_pfc_bound_divisibility_productcoefficientscoefficientsum = fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bound_divisibility_productcoefficientscoefficient) = S ((S (S (pfc_index_bound_divisibility_productcoefficients))) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bound_divisibility_productcoefficientscoefficientsum = fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bound_divisibility_productcoefficients))) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum) + (pfc_natural_sum_bound_divisibility_productcoefficientscoefficient))) /\ forall fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps = S (pfc_index_bound_divisibility_productcoefficients)) -> exists fs_a_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps fs_r_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps fs_s_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bound_divisibility_productcoefficientscoefficient)) /\ exists fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bound_divisibility_productcoefficientscoefficient = fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bound_divisibility_productcoefficientscoefficient) + (fs_a_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bound_divisibility_productcoefficientscoefficientsum = fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum) + (fs_r_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bound_divisibility_productcoefficientscoefficientsum = fs_q_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_divisibility_productcoefficientscoefficientsum) + (fs_s_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bound_divisibility_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bound_divisibility_productcoefficientscoefficientresiduebound. pfa_gap_bound_divisibility_productcoefficientscoefficientresiduebound + S (pfc_value_bound_divisibility_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bound_divisibility_productcoefficientscoefficientresiduecongruence pfa_offset_right_bound_divisibility_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bound_divisibility_productcoefficientscoefficient) + (p) * pfa_offset_left_bound_divisibility_productcoefficientscoefficientresiduecongruence = (pfc_value_bound_divisibility_productcoefficients) + (p) * pfa_offset_right_bound_divisibility_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_bound_divisibility_target pfrep_left_bound_divisibility_target pfrep_right_bound_divisibility_target. ((exists pfrep_position_bound_divisibility_targetfirst. ((pfrep_position_bound_divisibility_targetfirst+S (pfrep_power_bound_divisibility_target)=(pfgu_P_bound_divisibility)) /\ ((((exists ff_h_pfp_bound_divisibility_targetfirstentry. ff_h_pfp_bound_divisibility_targetfirstentry + S (pfrep_left_bound_divisibility_target) = S ((S (pfrep_position_bound_divisibility_targetfirst)) * pfgu_pc_bound_divisibility)) /\ exists ff_q_pfp_bound_divisibility_targetfirstentry. pfgu_pb_bound_divisibility = ff_q_pfp_bound_divisibility_targetfirstentry * S ((S (pfrep_position_bound_divisibility_targetfirst)) * pfgu_pc_bound_divisibility) + (pfrep_left_bound_divisibility_target)))))) \/ (((exists pfrep_gap_bound_divisibility_targetfirstoutside. pfrep_gap_bound_divisibility_targetfirstoutside+(pfgu_P_bound_divisibility)=(pfrep_power_bound_divisibility_target)) /\ (((pfrep_left_bound_divisibility_target)=0))))) -> ((exists pfrep_position_bound_divisibility_targetsecond. ((pfrep_position_bound_divisibility_targetsecond+S (pfrep_power_bound_divisibility_target)=(L)) /\ ((((exists ff_h_pfp_bound_divisibility_targetsecondentry. ff_h_pfp_bound_divisibility_targetsecondentry + S (pfrep_right_bound_divisibility_target) = S ((S (pfrep_position_bound_divisibility_targetsecond)) * ac)) /\ exists ff_q_pfp_bound_divisibility_targetsecondentry. ab = ff_q_pfp_bound_divisibility_targetsecondentry * S ((S (pfrep_position_bound_divisibility_targetsecond)) * ac) + (pfrep_right_bound_divisibility_target)))))) \/ (((exists pfrep_gap_bound_divisibility_targetsecondoutside. pfrep_gap_bound_divisibility_targetsecondoutside+(L)=(pfrep_power_bound_divisibility_target)) /\ (((pfrep_right_bound_divisibility_target)=0))))) -> pfrep_left_bound_divisibility_target=pfrep_right_bound_divisibility_target))))))) -> (exists pfc_gap_bound_result. pfc_gap_bound_result+(d)=(a))

Complete tactic proof in conservative notation

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

38 script commands · 7 reading checkpoints · 1 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 represented factorization
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 hfL14–23

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

  1. L14
    have hf : ∃ pfgu_qb_bound_factor. ∃ pfgu_qc_bound_factor. ∃ pfgu_e_bound_factor. ∃ pfgu_pb_bound_factor. ∃ pfgu_pc_bound_factor. FpRepresentedDegree(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,pfgu_e_bound_factor) ∧ (FpPolyProduct(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,db,dc,D,pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a) ∧ (PolynomialEquivalent(pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a,ab,ac,L) ∧ pfgu_e_bound_factor + d = a))Definitions: FpRepresentedDegree(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,pfgu_e_bound_factor)FpPolyProduct(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,db,dc,D,pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a)PolynomialEquivalent(pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a,ab,ac,L)Original native command in the exact edition
  2. L15
    specialize prime_field_polynomial_right_divides_represented_factorization (p)
  3. L16
    specialize prime_field_polynomial_right_divides_represented_factorization (db)
  4. L17
    specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  5. L18
    specialize prime_field_polynomial_right_divides_represented_factorization (D)
  6. L19
    specialize prime_field_polynomial_right_divides_represented_factorization (d)
  7. L20
    specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  8. L21
    specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  9. L22
    specialize prime_field_polynomial_right_divides_represented_factorization (L)
  10. L23
    specialize prime_field_polynomial_right_divides_represented_factorization (a)
04Use earlier factsL24–28

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

  1. L24
    apply prime_field_polynomial_right_divides_represented_factorization
  2. L25
    exact hp
  3. L26
    exact hd
  4. L27
    exact ha
  5. L28
    exact hrd
05Separate the logical casesL29–36

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

  1. L29
    cases hf
  2. L30
    cases hf_witness
  3. L31
    cases hf_witness_witness
  4. L32
    cases hf_witness_witness_witness
  5. L33
    cases hf_witness_witness_witness_witness
  6. L34
    cases hf_witness_witness_witness_witness_witness
  7. L35
    cases hf_witness_witness_witness_witness_witness_right
  8. L36
    cases hf_witness_witness_witness_witness_witness_right_right
06Construct an explicit witnessL37–37

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

  1. L37
    exists x2
07Use earlier factsL38–38

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

  1. L38
    exact hf_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 38 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 hf : ∃ pfgu_qb_bound_factor. ∃ pfgu_qc_bound_factor. ∃ pfgu_e_bound_factor. ∃ pfgu_pb_bound_factor. ∃ pfgu_pc_bound_factor. FpRepresentedDegree(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,pfgu_e_bound_factor) ∧ (FpPolyProduct(p,pfgu_qb_bound_factor,pfgu_qc_bound_factor,S pfgu_e_bound_factor,db,dc,D,pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a) ∧ (PolynomialEquivalent(pfgu_pb_bound_factor,pfgu_pc_bound_factor,S a,ab,ac,L) ∧ pfgu_e_bound_factor + d = a))
  15. 0015specialize prime_field_polynomial_right_divides_represented_factorization (p)
  16. 0016specialize prime_field_polynomial_right_divides_represented_factorization (db)
  17. 0017specialize prime_field_polynomial_right_divides_represented_factorization (dc)
  18. 0018specialize prime_field_polynomial_right_divides_represented_factorization (D)
  19. 0019specialize prime_field_polynomial_right_divides_represented_factorization (d)
  20. 0020specialize prime_field_polynomial_right_divides_represented_factorization (ab)
  21. 0021specialize prime_field_polynomial_right_divides_represented_factorization (ac)
  22. 0022specialize prime_field_polynomial_right_divides_represented_factorization (L)
  23. 0023specialize prime_field_polynomial_right_divides_represented_factorization (a)
  24. 0024apply prime_field_polynomial_right_divides_represented_factorization
  25. 0025exact hp
  26. 0026exact hd
  27. 0027exact ha
  28. 0028exact hrd
  29. 0029cases hf
  30. 0030cases hf_witness
  31. 0031cases hf_witness_witness
  32. 0032cases hf_witness_witness_witness
  33. 0033cases hf_witness_witness_witness_witness
  34. 0034cases hf_witness_witness_witness_witness_witness
  35. 0035cases hf_witness_witness_witness_witness_witness_right
  36. 0036cases hf_witness_witness_witness_witness_witness_right_right
  37. 0037exists x2
  38. 0038exact hf_witness_witness_witness_witness_witness_right_right_right