PG0034

prime_field_polynomial_right_divides_reflexive

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

Every canonical polynomial right-divides itself using a constructed left unit and actual product. Empty and zero prefixes are included, without assuming commutative multiplication.

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 ab ac L. (~((p) = 1) /\ forall pfa_factor_left_unit_divides_prime pfa_factor_right_unit_divides_prime. (p) = pfa_factor_left_unit_divides_prime * pfa_factor_right_unit_divides_prime -> pfa_factor_left_unit_divides_prime = 1 \/ pfa_factor_right_unit_divides_prime = 1) -> (forall fom_index_pfp_unit_divides_A. (exists fom_gap_pfp_unit_divides_A_index_bound. fom_gap_pfp_unit_divides_A_index_bound + S (fom_index_pfp_unit_divides_A) = L) -> exists fom_value_pfp_unit_divides_A. ((((exists fom_beta_height_pfp_unit_divides_A_entry. fom_beta_height_pfp_unit_divides_A_entry + S (fom_value_pfp_unit_divides_A) = S ((S (fom_index_pfp_unit_divides_A)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_A_entry. ab = fom_beta_quotient_pfp_unit_divides_A_entry * S ((S (fom_index_pfp_unit_divides_A)) * ac) + (fom_value_pfp_unit_divides_A))) /\ (exists fom_gap_pfp_unit_divides_A_value_bound. fom_gap_pfp_unit_divides_A_value_bound + S (fom_value_pfp_unit_divides_A) = p))) -> (((forall fom_index_pfp_unit_divides_bound. (exists fom_gap_pfp_unit_divides_bound_index_bound. fom_gap_pfp_unit_divides_bound_index_bound + S (fom_index_pfp_unit_divides_bound) = L) -> exists fom_value_pfp_unit_divides_bound. ((((exists fom_beta_height_pfp_unit_divides_bound_entry. fom_beta_height_pfp_unit_divides_bound_entry + S (fom_value_pfp_unit_divides_bound) = S ((S (fom_index_pfp_unit_divides_bound)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_bound_entry. ab = fom_beta_quotient_pfp_unit_divides_bound_entry * S ((S (fom_index_pfp_unit_divides_bound)) * ac) + (fom_value_pfp_unit_divides_bound))) /\ (exists fom_gap_pfp_unit_divides_bound_value_bound. fom_gap_pfp_unit_divides_bound_value_bound + S (fom_value_pfp_unit_divides_bound) = p))) /\ ((exists qb qc Q pb pc P. ((((forall fom_index_pfp_unit_divides_productleft. (exists fom_gap_pfp_unit_divides_productleft_index_bound. fom_gap_pfp_unit_divides_productleft_index_bound + S (fom_index_pfp_unit_divides_productleft) = Q) -> exists fom_value_pfp_unit_divides_productleft. ((((exists fom_beta_height_pfp_unit_divides_productleft_entry. fom_beta_height_pfp_unit_divides_productleft_entry + S (fom_value_pfp_unit_divides_productleft) = S ((S (fom_index_pfp_unit_divides_productleft)) * qc)) /\ exists fom_beta_quotient_pfp_unit_divides_productleft_entry. qb = fom_beta_quotient_pfp_unit_divides_productleft_entry * S ((S (fom_index_pfp_unit_divides_productleft)) * qc) + (fom_value_pfp_unit_divides_productleft))) /\ (exists fom_gap_pfp_unit_divides_productleft_value_bound. fom_gap_pfp_unit_divides_productleft_value_bound + S (fom_value_pfp_unit_divides_productleft) = p))) /\ (((forall fom_index_pfp_unit_divides_productright. (exists fom_gap_pfp_unit_divides_productright_index_bound. fom_gap_pfp_unit_divides_productright_index_bound + S (fom_index_pfp_unit_divides_productright) = L) -> exists fom_value_pfp_unit_divides_productright. ((((exists fom_beta_height_pfp_unit_divides_productright_entry. fom_beta_height_pfp_unit_divides_productright_entry + S (fom_value_pfp_unit_divides_productright) = S ((S (fom_index_pfp_unit_divides_productright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_productright_entry. ab = fom_beta_quotient_pfp_unit_divides_productright_entry * S ((S (fom_index_pfp_unit_divides_productright)) * ac) + (fom_value_pfp_unit_divides_productright))) /\ (exists fom_gap_pfp_unit_divides_productright_value_bound. fom_gap_pfp_unit_divides_productright_value_bound + S (fom_value_pfp_unit_divides_productright) = p))) /\ (((((((Q)=0 \/ (L)=0) /\ (((P)=0)))) \/ (((~((Q)=0)) /\ (((~((L)=0)) /\ (((Q)+(L)=S (P)))))))) /\ ((forall pfc_index_unit_divides_productcoefficients. (exists pfa_gap_unit_divides_productcoefficientsbound. pfa_gap_unit_divides_productcoefficientsbound + S (pfc_index_unit_divides_productcoefficients) = (P)) -> exists pfc_value_unit_divides_productcoefficients. ((((exists ff_h_pfp_unit_divides_productcoefficientsentry. ff_h_pfp_unit_divides_productcoefficientsentry + S (pfc_value_unit_divides_productcoefficients) = S ((S (pfc_index_unit_divides_productcoefficients)) * pc)) /\ exists ff_q_pfp_unit_divides_productcoefficientsentry. pb = ff_q_pfp_unit_divides_productcoefficientsentry * S ((S (pfc_index_unit_divides_productcoefficients)) * pc) + (pfc_value_unit_divides_productcoefficients))) /\ ((exists pfc_terms_code_unit_divides_productcoefficientscoefficient pfc_terms_scale_unit_divides_productcoefficientscoefficient pfc_natural_sum_unit_divides_productcoefficientscoefficient. ((forall pfc_index_unit_divides_productcoefficientscoefficientdiagonal. (exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonalbound. pfa_gap_unit_divides_productcoefficientscoefficientdiagonalbound + S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal) = (S (pfc_index_unit_divides_productcoefficients))) -> exists pfc_value_unit_divides_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonalentry + S (pfc_value_unit_divides_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_divides_productcoefficientscoefficient = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient) + (pfc_value_unit_divides_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm. (((pfc_index_unit_divides_productcoefficientscoefficientdiagonal)+pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm=(pfc_index_unit_divides_productcoefficients)) /\ ((((((exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal) = (Q)) /\ ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry. qb = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) * qc) + (pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermleftoutside+(Q)=(pfc_index_unit_divides_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_divides_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_divides_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_divides_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_divides_productcoefficientscoefficientdiagonal)=pfc_left_unit_divides_productcoefficientscoefficientdiagonalterm*pfc_right_unit_divides_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_divides_productcoefficientscoefficientsum fs_v_pfc_unit_divides_productcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_start. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_start. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_divides_productcoefficientscoefficient) = S ((S (S (pfc_index_unit_divides_productcoefficients))) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_divides_productcoefficients))) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (pfc_natural_sum_unit_divides_productcoefficientscoefficient))) /\ forall fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps = S (pfc_index_unit_divides_productcoefficients)) -> exists fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_divides_productcoefficientscoefficient = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_productcoefficientscoefficient) + (fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_divides_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_productcoefficientscoefficientsum) + (fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_divides_productcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_divides_productcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_divides_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_divides_productcoefficientscoefficientresiduebound. pfa_gap_unit_divides_productcoefficientscoefficientresiduebound + S (pfc_value_unit_divides_productcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_divides_productcoefficientscoefficientresiduecongruence pfa_offset_right_unit_divides_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_divides_productcoefficientscoefficient) + (p) * pfa_offset_left_unit_divides_productcoefficientscoefficientresiduecongruence = (pfc_value_unit_divides_productcoefficients) + (p) * pfa_offset_right_unit_divides_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_unit_divides_equivalent pfrep_left_unit_divides_equivalent pfrep_right_unit_divides_equivalent. ((exists pfrep_position_unit_divides_equivalentfirst. ((pfrep_position_unit_divides_equivalentfirst+S (pfrep_power_unit_divides_equivalent)=(P)) /\ ((((exists ff_h_pfp_unit_divides_equivalentfirstentry. ff_h_pfp_unit_divides_equivalentfirstentry + S (pfrep_left_unit_divides_equivalent) = S ((S (pfrep_position_unit_divides_equivalentfirst)) * pc)) /\ exists ff_q_pfp_unit_divides_equivalentfirstentry. pb = ff_q_pfp_unit_divides_equivalentfirstentry * S ((S (pfrep_position_unit_divides_equivalentfirst)) * pc) + (pfrep_left_unit_divides_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_equivalentfirstoutside. pfrep_gap_unit_divides_equivalentfirstoutside+(P)=(pfrep_power_unit_divides_equivalent)) /\ (((pfrep_left_unit_divides_equivalent)=0))))) -> ((exists pfrep_position_unit_divides_equivalentsecond. ((pfrep_position_unit_divides_equivalentsecond+S (pfrep_power_unit_divides_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_divides_equivalentsecondentry. ff_h_pfp_unit_divides_equivalentsecondentry + S (pfrep_right_unit_divides_equivalent) = S ((S (pfrep_position_unit_divides_equivalentsecond)) * ac)) /\ exists ff_q_pfp_unit_divides_equivalentsecondentry. ab = ff_q_pfp_unit_divides_equivalentsecondentry * S ((S (pfrep_position_unit_divides_equivalentsecond)) * ac) + (pfrep_right_unit_divides_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_equivalentsecondoutside. pfrep_gap_unit_divides_equivalentsecondoutside+(L)=(pfrep_power_unit_divides_equivalent)) /\ (((pfrep_right_unit_divides_equivalent)=0))))) -> pfrep_left_unit_divides_equivalent=pfrep_right_unit_divides_equivalent)))))))

Constructive proof overview

Generated structural guide

Every canonical polynomial right-divides itself using a constructed left unit and actual product. Empty and zero prefixes are included, without assuming commutative multiplication.

The unchanged tactic script uses 2 declared prerequisites 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

PG0033 prime_field_polynomial_convolution_left_unit_exists PG0026 prime_field_polynomial_right_divides_from_product

Direct dependents

none

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 · 5 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 (2)
prime field polynomial convolution left unit existsprime field polynomial right divides from product

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–6

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro hp
  6. L6
    intro hA
02Establish huL7–14

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

  1. L7
    have hu : ∃ ub. ∃ uc. ∃ cb. ∃ cc. BetaPrefixInto(ub,uc,1,p) ∧ (BetaAt(ub,uc,0,1) ∧ (FpPolyProduct(p,ub,uc,1,ab,ac,L,cb,cc,L) ∧ PolynomialEquivalent(cb,cc,L,ab,ac,L)))Definitions: BetaPrefixIntoFpPolyProductPolynomialEquivalentBetaAt
  2. L8
    specialize prime_field_polynomial_convolution_left_unit_exists (p)
  3. L9
    specialize prime_field_polynomial_convolution_left_unit_exists (ab)
  4. L10
    specialize prime_field_polynomial_convolution_left_unit_exists (ac)
  5. L11
    specialize prime_field_polynomial_convolution_left_unit_exists (L)
  6. L12
    apply prime_field_polynomial_convolution_left_unit_exists
  7. L13
    exact hp
  8. L14
    exact hA
03Separate the logical casesL15–21

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

  1. L15
    cases hu
  2. L16
    cases hu_witness
  3. L17
    cases hu_witness_witness
  4. L18
    cases hu_witness_witness_witness
  5. L19
    cases hu_witness_witness_witness_witness
  6. L20
    cases hu_witness_witness_witness_witness_right
  7. L21
    cases hu_witness_witness_witness_witness_right_right
04Use earlier factsL22–31

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

  1. L22
    specialize prime_field_polynomial_right_divides_from_product (p)
  2. L23
    specialize prime_field_polynomial_right_divides_from_product (ab)
  3. L24
    specialize prime_field_polynomial_right_divides_from_product (ac)
  4. L25
    specialize prime_field_polynomial_right_divides_from_product (L)
  5. L26
    specialize prime_field_polynomial_right_divides_from_product (ab)
  6. L27
    specialize prime_field_polynomial_right_divides_from_product (ac)
  7. L28
    specialize prime_field_polynomial_right_divides_from_product (L)
  8. L29
    specialize prime_field_polynomial_right_divides_from_product (x)
  9. L30
    specialize prime_field_polynomial_right_divides_from_product (x1)
  10. L31
    specialize prime_field_polynomial_right_divides_from_product (1)
05Use earlier factsL32–38

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

  1. L32
    specialize prime_field_polynomial_right_divides_from_product (x2)
  2. L33
    specialize prime_field_polynomial_right_divides_from_product (x3)
  3. L34
    specialize prime_field_polynomial_right_divides_from_product (L)
  4. L35
    apply prime_field_polynomial_right_divides_from_product
  5. L36
    exact hA
  6. L37
    exact hu_witness_witness_witness_witness_right_right_left
  7. L38
    exact hu_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro hp
  6. 0006intro hA
  7. 0007have hu : exists ub uc cb cc. ((forall fom_index_pfp_unit_divides_witness_unit_bound. (exists fom_gap_pfp_unit_divides_witness_unit_bound_index_bound. fom_gap_pfp_unit_divides_witness_unit_bound_index_bound + S (fom_index_pfp_unit_divides_witness_unit_bound) = 1) -> exists fom_value_pfp_unit_divides_witness_unit_bound. ((((exists fom_beta_height_pfp_unit_divides_witness_unit_bound_entry. fom_beta_height_pfp_unit_divides_witness_unit_bound_entry + S (fom_value_pfp_unit_divides_witness_unit_bound) = S ((S (fom_index_pfp_unit_divides_witness_unit_bound)) * uc)) /\ exists fom_beta_quotient_pfp_unit_divides_witness_unit_bound_entry. ub = fom_beta_quotient_pfp_unit_divides_witness_unit_bound_entry * S ((S (fom_index_pfp_unit_divides_witness_unit_bound)) * uc) + (fom_value_pfp_unit_divides_witness_unit_bound))) /\ (exists fom_gap_pfp_unit_divides_witness_unit_bound_value_bound. fom_gap_pfp_unit_divides_witness_unit_bound_value_bound + S (fom_value_pfp_unit_divides_witness_unit_bound) = p))) /\ (((((exists ff_h_pfp_unit_divides_witness_unit_value. ff_h_pfp_unit_divides_witness_unit_value + S (1) = S ((S (0)) * uc)) /\ exists ff_q_pfp_unit_divides_witness_unit_value. ub = ff_q_pfp_unit_divides_witness_unit_value * S ((S (0)) * uc) + (1))) /\ (((((forall fom_index_pfp_unit_divides_witness_productleft. (exists fom_gap_pfp_unit_divides_witness_productleft_index_bound. fom_gap_pfp_unit_divides_witness_productleft_index_bound + S (fom_index_pfp_unit_divides_witness_productleft) = 1) -> exists fom_value_pfp_unit_divides_witness_productleft. ((((exists fom_beta_height_pfp_unit_divides_witness_productleft_entry. fom_beta_height_pfp_unit_divides_witness_productleft_entry + S (fom_value_pfp_unit_divides_witness_productleft) = S ((S (fom_index_pfp_unit_divides_witness_productleft)) * uc)) /\ exists fom_beta_quotient_pfp_unit_divides_witness_productleft_entry. ub = fom_beta_quotient_pfp_unit_divides_witness_productleft_entry * S ((S (fom_index_pfp_unit_divides_witness_productleft)) * uc) + (fom_value_pfp_unit_divides_witness_productleft))) /\ (exists fom_gap_pfp_unit_divides_witness_productleft_value_bound. fom_gap_pfp_unit_divides_witness_productleft_value_bound + S (fom_value_pfp_unit_divides_witness_productleft) = p))) /\ (((forall fom_index_pfp_unit_divides_witness_productright. (exists fom_gap_pfp_unit_divides_witness_productright_index_bound. fom_gap_pfp_unit_divides_witness_productright_index_bound + S (fom_index_pfp_unit_divides_witness_productright) = L) -> exists fom_value_pfp_unit_divides_witness_productright. ((((exists fom_beta_height_pfp_unit_divides_witness_productright_entry. fom_beta_height_pfp_unit_divides_witness_productright_entry + S (fom_value_pfp_unit_divides_witness_productright) = S ((S (fom_index_pfp_unit_divides_witness_productright)) * ac)) /\ exists fom_beta_quotient_pfp_unit_divides_witness_productright_entry. ab = fom_beta_quotient_pfp_unit_divides_witness_productright_entry * S ((S (fom_index_pfp_unit_divides_witness_productright)) * ac) + (fom_value_pfp_unit_divides_witness_productright))) /\ (exists fom_gap_pfp_unit_divides_witness_productright_value_bound. fom_gap_pfp_unit_divides_witness_productright_value_bound + S (fom_value_pfp_unit_divides_witness_productright) = p))) /\ (((((((1)=0 \/ (L)=0) /\ (((L)=0)))) \/ (((~((1)=0)) /\ (((~((L)=0)) /\ (((1)+(L)=S (L)))))))) /\ ((forall pfc_index_unit_divides_witness_productcoefficients. (exists pfa_gap_unit_divides_witness_productcoefficientsbound. pfa_gap_unit_divides_witness_productcoefficientsbound + S (pfc_index_unit_divides_witness_productcoefficients) = (L)) -> exists pfc_value_unit_divides_witness_productcoefficients. ((((exists ff_h_pfp_unit_divides_witness_productcoefficientsentry. ff_h_pfp_unit_divides_witness_productcoefficientsentry + S (pfc_value_unit_divides_witness_productcoefficients) = S ((S (pfc_index_unit_divides_witness_productcoefficients)) * cc)) /\ exists ff_q_pfp_unit_divides_witness_productcoefficientsentry. cb = ff_q_pfp_unit_divides_witness_productcoefficientsentry * S ((S (pfc_index_unit_divides_witness_productcoefficients)) * cc) + (pfc_value_unit_divides_witness_productcoefficients))) /\ ((exists pfc_terms_code_unit_divides_witness_productcoefficientscoefficient pfc_terms_scale_unit_divides_witness_productcoefficientscoefficient pfc_natural_sum_unit_divides_witness_productcoefficientscoefficient. ((forall pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal. (exists pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonalbound. pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonalbound + S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal) = (S (pfc_index_unit_divides_witness_productcoefficients))) -> exists pfc_value_unit_divides_witness_productcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonalentry. ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonalentry + S (pfc_value_unit_divides_witness_productcoefficientscoefficientdiagonal) = S ((S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_witness_productcoefficientscoefficient)) /\ exists ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonalentry. pfc_terms_code_unit_divides_witness_productcoefficientscoefficient = ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonalentry * S ((S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)) * pfc_terms_scale_unit_divides_witness_productcoefficientscoefficient) + (pfc_value_unit_divides_witness_productcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm pfc_left_unit_divides_witness_productcoefficientscoefficientdiagonalterm pfc_right_unit_divides_witness_productcoefficientscoefficientdiagonalterm. (((pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)+pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm=(pfc_index_unit_divides_witness_productcoefficients)) /\ ((((((exists pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftinside. pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal) = (1)) /\ ((((exists ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_unit_divides_witness_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)) * uc)) /\ exists ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftentry. ub = ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)) * uc) + (pfc_left_unit_divides_witness_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermleftoutside+(1)=(pfc_index_unit_divides_witness_productcoefficientscoefficientdiagonal)) /\ (((pfc_left_unit_divides_witness_productcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightinside. pfa_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_unit_divides_witness_productcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm)) * ac)) /\ exists ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightentry. ab = ff_q_pfp_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm)) * ac) + (pfc_right_unit_divides_witness_productcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_unit_divides_witness_productcoefficientscoefficientdiagonaltermrightoutside+(L)=(pfc_complement_unit_divides_witness_productcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_unit_divides_witness_productcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_unit_divides_witness_productcoefficientscoefficientdiagonal)=pfc_left_unit_divides_witness_productcoefficientscoefficientdiagonalterm*pfc_right_unit_divides_witness_productcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_unit_divides_witness_productcoefficientscoefficientsum fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum. ((((exists fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_start. fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_start. fs_u_pfc_unit_divides_witness_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_terminal. fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_unit_divides_witness_productcoefficientscoefficient) = S ((S (S (pfc_index_unit_divides_witness_productcoefficients))) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_terminal. fs_u_pfc_unit_divides_witness_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_unit_divides_witness_productcoefficients))) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum) + (pfc_natural_sum_unit_divides_witness_productcoefficientscoefficient))) /\ forall fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps = S (pfc_index_unit_divides_witness_productcoefficients)) -> exists fs_a_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps fs_r_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps fs_s_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_witness_productcoefficientscoefficient)) /\ exists fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_unit_divides_witness_productcoefficientscoefficient = fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_unit_divides_witness_productcoefficientscoefficient) + (fs_a_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_unit_divides_witness_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum) + (fs_r_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum)) /\ exists fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_unit_divides_witness_productcoefficientscoefficientsum = fs_q_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)) * fs_v_pfc_unit_divides_witness_productcoefficientscoefficientsum) + (fs_s_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps = fs_r_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps + fs_a_pfc_unit_divides_witness_productcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_unit_divides_witness_productcoefficientscoefficientresiduebound. pfa_gap_unit_divides_witness_productcoefficientscoefficientresiduebound + S (pfc_value_unit_divides_witness_productcoefficients) = (p)) /\ ((exists pfa_offset_left_unit_divides_witness_productcoefficientscoefficientresiduecongruence pfa_offset_right_unit_divides_witness_productcoefficientscoefficientresiduecongruence. (pfc_natural_sum_unit_divides_witness_productcoefficientscoefficient) + (p) * pfa_offset_left_unit_divides_witness_productcoefficientscoefficientresiduecongruence = (pfc_value_unit_divides_witness_productcoefficients) + (p) * pfa_offset_right_unit_divides_witness_productcoefficientscoefficientresiduecongruence))))))))))))))))))) /\ ((forall pfrep_power_unit_divides_witness_equivalent pfrep_left_unit_divides_witness_equivalent pfrep_right_unit_divides_witness_equivalent. ((exists pfrep_position_unit_divides_witness_equivalentfirst. ((pfrep_position_unit_divides_witness_equivalentfirst+S (pfrep_power_unit_divides_witness_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_divides_witness_equivalentfirstentry. ff_h_pfp_unit_divides_witness_equivalentfirstentry + S (pfrep_left_unit_divides_witness_equivalent) = S ((S (pfrep_position_unit_divides_witness_equivalentfirst)) * cc)) /\ exists ff_q_pfp_unit_divides_witness_equivalentfirstentry. cb = ff_q_pfp_unit_divides_witness_equivalentfirstentry * S ((S (pfrep_position_unit_divides_witness_equivalentfirst)) * cc) + (pfrep_left_unit_divides_witness_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_witness_equivalentfirstoutside. pfrep_gap_unit_divides_witness_equivalentfirstoutside+(L)=(pfrep_power_unit_divides_witness_equivalent)) /\ (((pfrep_left_unit_divides_witness_equivalent)=0))))) -> ((exists pfrep_position_unit_divides_witness_equivalentsecond. ((pfrep_position_unit_divides_witness_equivalentsecond+S (pfrep_power_unit_divides_witness_equivalent)=(L)) /\ ((((exists ff_h_pfp_unit_divides_witness_equivalentsecondentry. ff_h_pfp_unit_divides_witness_equivalentsecondentry + S (pfrep_right_unit_divides_witness_equivalent) = S ((S (pfrep_position_unit_divides_witness_equivalentsecond)) * ac)) /\ exists ff_q_pfp_unit_divides_witness_equivalentsecondentry. ab = ff_q_pfp_unit_divides_witness_equivalentsecondentry * S ((S (pfrep_position_unit_divides_witness_equivalentsecond)) * ac) + (pfrep_right_unit_divides_witness_equivalent)))))) \/ (((exists pfrep_gap_unit_divides_witness_equivalentsecondoutside. pfrep_gap_unit_divides_witness_equivalentsecondoutside+(L)=(pfrep_power_unit_divides_witness_equivalent)) /\ (((pfrep_right_unit_divides_witness_equivalent)=0))))) -> pfrep_left_unit_divides_witness_equivalent=pfrep_right_unit_divides_witness_equivalent)))))))
  8. 0008specialize prime_field_polynomial_convolution_left_unit_exists (p)
  9. 0009specialize prime_field_polynomial_convolution_left_unit_exists (ab)
  10. 0010specialize prime_field_polynomial_convolution_left_unit_exists (ac)
  11. 0011specialize prime_field_polynomial_convolution_left_unit_exists (L)
  12. 0012apply prime_field_polynomial_convolution_left_unit_exists
  13. 0013exact hp
  14. 0014exact hA
  15. 0015cases hu
  16. 0016cases hu_witness
  17. 0017cases hu_witness_witness
  18. 0018cases hu_witness_witness_witness
  19. 0019cases hu_witness_witness_witness_witness
  20. 0020cases hu_witness_witness_witness_witness_right
  21. 0021cases hu_witness_witness_witness_witness_right_right
  22. 0022specialize prime_field_polynomial_right_divides_from_product (p)
  23. 0023specialize prime_field_polynomial_right_divides_from_product (ab)
  24. 0024specialize prime_field_polynomial_right_divides_from_product (ac)
  25. 0025specialize prime_field_polynomial_right_divides_from_product (L)
  26. 0026specialize prime_field_polynomial_right_divides_from_product (ab)
  27. 0027specialize prime_field_polynomial_right_divides_from_product (ac)
  28. 0028specialize prime_field_polynomial_right_divides_from_product (L)
  29. 0029specialize prime_field_polynomial_right_divides_from_product (x)
  30. 0030specialize prime_field_polynomial_right_divides_from_product (x1)
  31. 0031specialize prime_field_polynomial_right_divides_from_product (1)
  32. 0032specialize prime_field_polynomial_right_divides_from_product (x2)
  33. 0033specialize prime_field_polynomial_right_divides_from_product (x3)
  34. 0034specialize prime_field_polynomial_right_divides_from_product (L)
  35. 0035apply prime_field_polynomial_right_divides_from_product
  36. 0036exact hA
  37. 0037exact hu_witness_witness_witness_witness_right_right_left
  38. 0038exact hu_witness_witness_witness_witness_right_right_right