PG0071

prime_field_polynomial_right_divides_represented_degree_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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.

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

Exact expanded first-order arithmetic 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))

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 1 declared prerequisite and contains 38 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG0070 prime_field_polynomial_right_divides_represented_factorization

Direct dependents

PG0074 prime_field_polynomial_monic_right_associates_equivalent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
prime field polynomial right divides represented factorization

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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: FpPolyProductFpRepresentedDegreePolynomialEquivalent
  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 exact 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 : exists pfgu_qb_bound_factor pfgu_qc_bound_factor pfgu_e_bound_factor pfgu_pb_bound_factor pfgu_pc_bound_factor. (((((S (pfgu_e_bound_factor))=S (pfgu_e_bound_factor)) /\ (((forall fom_index_pfp_bound_factor_quotientcoefficients. (exists fom_gap_pfp_bound_factor_quotientcoefficients_index_bound. fom_gap_pfp_bound_factor_quotientcoefficients_index_bound + S (fom_index_pfp_bound_factor_quotientcoefficients) = S (pfgu_e_bound_factor)) -> exists fom_value_pfp_bound_factor_quotientcoefficients. ((((exists fom_beta_height_pfp_bound_factor_quotientcoefficients_entry. fom_beta_height_pfp_bound_factor_quotientcoefficients_entry + S (fom_value_pfp_bound_factor_quotientcoefficients) = S ((S (fom_index_pfp_bound_factor_quotientcoefficients)) * pfgu_qc_bound_factor)) /\ exists fom_beta_quotient_pfp_bound_factor_quotientcoefficients_entry. pfgu_qb_bound_factor = fom_beta_quotient_pfp_bound_factor_quotientcoefficients_entry * S ((S (fom_index_pfp_bound_factor_quotientcoefficients)) * pfgu_qc_bound_factor) + (fom_value_pfp_bound_factor_quotientcoefficients))) /\ (exists fom_gap_pfp_bound_factor_quotientcoefficients_value_bound. fom_gap_pfp_bound_factor_quotientcoefficients_value_bound + S (fom_value_pfp_bound_factor_quotientcoefficients) = p))) /\ ((exists pfd_leading_bound_factor_quotient. ((((exists ff_h_pfp_bound_factor_quotiententry. ff_h_pfp_bound_factor_quotiententry + S (pfd_leading_bound_factor_quotient) = S ((S (0)) * pfgu_qc_bound_factor)) /\ exists ff_q_pfp_bound_factor_quotiententry. pfgu_qb_bound_factor = ff_q_pfp_bound_factor_quotiententry * S ((S (0)) * pfgu_qc_bound_factor) + (pfd_leading_bound_factor_quotient))) /\ ((~(pfd_leading_bound_factor_quotient=0)))))))))) /\ (((((forall fom_index_pfp_bound_factor_productleft. (exists fom_gap_pfp_bound_factor_productleft_index_bound. fom_gap_pfp_bound_factor_productleft_index_bound + S (fom_index_pfp_bound_factor_productleft) = S (pfgu_e_bound_factor)) -> exists fom_value_pfp_bound_factor_productleft. ((((exists fom_beta_height_pfp_bound_factor_productleft_entry. fom_beta_height_pfp_bound_factor_productleft_entry + S (fom_value_pfp_bound_factor_productleft) = S ((S (fom_index_pfp_bound_factor_productleft)) * pfgu_qc_bound_factor)) /\ exists fom_beta_quotient_pfp_bound_factor_productleft_entry. pfgu_qb_bound_factor = fom_beta_quotient_pfp_bound_factor_productleft_entry * S ((S (fom_index_pfp_bound_factor_productleft)) * pfgu_qc_bound_factor) + (fom_value_pfp_bound_factor_productleft))) /\ (exists fom_gap_pfp_bound_factor_productleft_value_bound. fom_gap_pfp_bound_factor_productleft_value_bound + S (fom_value_pfp_bound_factor_productleft) = p))) /\ (((forall fom_index_pfp_bound_factor_productright. (exists fom_gap_pfp_bound_factor_productright_index_bound. fom_gap_pfp_bound_factor_productright_index_bound + S (fom_index_pfp_bound_factor_productright) = D) -> exists fom_value_pfp_bound_factor_productright. ((((exists fom_beta_height_pfp_bound_factor_productright_entry. fom_beta_height_pfp_bound_factor_productright_entry + S (fom_value_pfp_bound_factor_productright) = S ((S (fom_index_pfp_bound_factor_productright)) * dc)) /\ exists fom_beta_quotient_pfp_bound_factor_productright_entry. db = fom_beta_quotient_pfp_bound_factor_productright_entry * S ((S (fom_index_pfp_bound_factor_productright)) * dc) + (fom_value_pfp_bound_factor_productright))) /\ (exists fom_gap_pfp_bound_factor_productright_value_bound. fom_gap_pfp_bound_factor_productright_value_bound + S (fom_value_pfp_bound_factor_productright) = p))) /\ (((((((S (pfgu_e_bound_factor))=0 \/ (D)=0) /\ (((S (a))=0)))) \/ (((~((S (pfgu_e_bound_factor))=0)) /\ (((~((D)=0)) /\ (((S (pfgu_e_bound_factor))+(D)=S (S (a))))))))) /\ ((forall pfc_index_bound_factor_productcoefficients. (exists pfa_gap_bound_factor_productcoefficientsbound. pfa_gap_bound_factor_productcoefficientsbound + S (pfc_index_bound_factor_productcoefficients) = (S (a))) -> exists pfc_value_bound_factor_productcoefficients. ((((exists ff_h_pfp_bound_factor_productcoefficientsentry. ff_h_pfp_bound_factor_productcoefficientsentry + S (pfc_value_bound_factor_productcoefficients) = S ((S (pfc_index_bound_factor_productcoefficients)) * pfgu_pc_bound_factor)) /\ exists ff_q_pfp_bound_factor_productcoefficientsentry. pfgu_pb_bound_factor = ff_q_pfp_bound_factor_productcoefficientsentry * S ((S (pfc_index_bound_factor_productcoefficients)) * pfgu_pc_bound_factor) + (pfc_value_bound_factor_productcoefficients))) /\ ((exists pfc_terms_code_bound_factor_productcoefficientscoefficient pfc_terms_scale_bound_factor_productcoefficientscoefficient pfc_natural_sum_bound_factor_productcoefficientscoefficient. ((forall pfc_index_bound_factor_productcoefficientscoefficientdiagonal. (exists pfa_gap_bound_factor_productcoefficientscoefficientdiagonalbound. pfa_gap_bound_factor_productcoefficientscoefficientdiagonalbound + S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal) = (S (pfc_index_bound_factor_productcoefficients))) -> exists pfc_value_bound_factor_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonalentry. ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonalentry + S (pfc_value_bound_factor_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bound_factor_productcoefficientscoefficient)) /\ exists ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonalentry. pfc_terms_code_bound_factor_productcoefficientscoefficient = ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_bound_factor_productcoefficientscoefficient) + (pfc_value_bound_factor_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm pfc_left_bound_factor_productcoefficientscoefficientdiagonalterm pfc_right_bound_factor_productcoefficientscoefficientdiagonalterm. (((pfc_index_bound_factor_productcoefficientscoefficientdiagonal)+pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm=(pfc_index_bound_factor_productcoefficients)) /\ ((((((exists pfa_gap_bound_factor_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_bound_factor_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal) = (S (pfgu_e_bound_factor))) /\ ((((exists ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_bound_factor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal)) * pfgu_qc_bound_factor)) /\ exists ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonaltermleftentry. pfgu_qb_bound_factor = ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_bound_factor_productcoefficientscoefficientdiagonal)) * pfgu_qc_bound_factor) + (pfc_left_bound_factor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bound_factor_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_bound_factor_productcoefficientscoefficientdiagonaltermleftoutside+(S (pfgu_e_bound_factor))=(pfc_index_bound_factor_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_bound_factor_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_bound_factor_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_bound_factor_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm) = (D)) /\ ((((exists ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_bound_factor_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_bound_factor_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm)) * dc)) /\ exists ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonaltermrightentry. db = ff_q_pfp_bound_factor_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm)) * dc) + (pfc_right_bound_factor_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_bound_factor_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_bound_factor_productcoefficientscoefficientdiagonaltermrightoutside+(D)=(pfc_complement_bound_factor_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_bound_factor_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_bound_factor_productcoefficientscoefficientdiagonal)=pfc_left_bound_factor_productcoefficientscoefficientdiagonalterm*pfc_right_bound_factor_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_bound_factor_productcoefficientscoefficientsum fs_v_pfc_bound_factor_productcoefficientscoefficientsum. ((((exists fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_start. fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_start. fs_u_pfc_bound_factor_productcoefficientscoefficientsum = fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_bound_factor_productcoefficientscoefficient) = S ((S (S (pfc_index_bound_factor_productcoefficients))) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_bound_factor_productcoefficientscoefficientsum = fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_bound_factor_productcoefficients))) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum) + (pfc_natural_sum_bound_factor_productcoefficientscoefficient))) /\ forall fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps = S (pfc_index_bound_factor_productcoefficients)) -> exists fs_a_pfc_bound_factor_productcoefficientscoefficientsum_body_steps fs_r_pfc_bound_factor_productcoefficientscoefficientsum_body_steps fs_s_pfc_bound_factor_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_bound_factor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bound_factor_productcoefficientscoefficient)) /\ exists fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_bound_factor_productcoefficientscoefficient = fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_bound_factor_productcoefficientscoefficient) + (fs_a_pfc_bound_factor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_bound_factor_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_bound_factor_productcoefficientscoefficientsum = fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum) + (fs_r_pfc_bound_factor_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_bound_factor_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_bound_factor_productcoefficientscoefficientsum = fs_q_pfc_bound_factor_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_bound_factor_productcoefficientscoefficientsum) + (fs_s_pfc_bound_factor_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_bound_factor_productcoefficientscoefficientsum_body_steps = fs_r_pfc_bound_factor_productcoefficientscoefficientsum_body_steps + fs_a_pfc_bound_factor_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_bound_factor_productcoefficientscoefficientresiduebound. pfa_gap_bound_factor_productcoefficientscoefficientresiduebound + S (pfc_value_bound_factor_productcoefficients) = (p)) /\ ((exists pfa_offset_left_bound_factor_productcoefficientscoefficientresiduecongruence pfa_offset_right_bound_factor_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_bound_factor_productcoefficientscoefficient) + (p) * pfa_offset_left_bound_factor_productcoefficientscoefficientresiduecongruence = (pfc_value_bound_factor_productcoefficients) + (p) * pfa_offset_right_bound_factor_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ (((forall pfrep_power_bound_factor_equivalent pfrep_left_bound_factor_equivalent pfrep_right_bound_factor_equivalent. ((exists pfrep_position_bound_factor_equivalentfirst. ((pfrep_position_bound_factor_equivalentfirst+S (pfrep_power_bound_factor_equivalent)=(S (a))) /\ ((((exists ff_h_pfp_bound_factor_equivalentfirstentry. ff_h_pfp_bound_factor_equivalentfirstentry + S (pfrep_left_bound_factor_equivalent) = S ((S (pfrep_position_bound_factor_equivalentfirst)) * pfgu_pc_bound_factor)) /\ exists ff_q_pfp_bound_factor_equivalentfirstentry. pfgu_pb_bound_factor = ff_q_pfp_bound_factor_equivalentfirstentry * S ((S (pfrep_position_bound_factor_equivalentfirst)) * pfgu_pc_bound_factor) + (pfrep_left_bound_factor_equivalent)))))) \/ (((exists pfrep_gap_bound_factor_equivalentfirstoutside. pfrep_gap_bound_factor_equivalentfirstoutside+(S (a))=(pfrep_power_bound_factor_equivalent)) /\ (((pfrep_left_bound_factor_equivalent)=0))))) -> ((exists pfrep_position_bound_factor_equivalentsecond. ((pfrep_position_bound_factor_equivalentsecond+S (pfrep_power_bound_factor_equivalent)=(L)) /\ ((((exists ff_h_pfp_bound_factor_equivalentsecondentry. ff_h_pfp_bound_factor_equivalentsecondentry + S (pfrep_right_bound_factor_equivalent) = S ((S (pfrep_position_bound_factor_equivalentsecond)) * ac)) /\ exists ff_q_pfp_bound_factor_equivalentsecondentry. ab = ff_q_pfp_bound_factor_equivalentsecondentry * S ((S (pfrep_position_bound_factor_equivalentsecond)) * ac) + (pfrep_right_bound_factor_equivalent)))))) \/ (((exists pfrep_gap_bound_factor_equivalentsecondoutside. pfrep_gap_bound_factor_equivalentsecondoutside+(L)=(pfrep_power_bound_factor_equivalent)) /\ (((pfrep_right_bound_factor_equivalent)=0))))) -> pfrep_left_bound_factor_equivalent=pfrep_right_bound_factor_equivalent) /\ (((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