PX0038

prime_field_polynomial_division_residual_data_exists

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

Construct the actual ambient product, residual and normalized trim as a separate stage; none is supplied as an oracle or identity premise.

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 bb bc d qb qc q. (~((p) = 1) /\ forall pfa_factor_left_division_residual_data_prime pfa_factor_right_division_residual_data_prime. (p) = pfa_factor_left_division_residual_data_prime * pfa_factor_right_division_residual_data_prime -> pfa_factor_left_division_residual_data_prime = 1 \/ pfa_factor_right_division_residual_data_prime = 1) -> (forall fom_index_pfp_division_residual_data_input. (exists fom_gap_pfp_division_residual_data_input_index_bound. fom_gap_pfp_division_residual_data_input_index_bound + S (fom_index_pfp_division_residual_data_input) = L) -> exists fom_value_pfp_division_residual_data_input. ((((exists fom_beta_height_pfp_division_residual_data_input_entry. fom_beta_height_pfp_division_residual_data_input_entry + S (fom_value_pfp_division_residual_data_input) = S ((S (fom_index_pfp_division_residual_data_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_residual_data_input_entry. ab = fom_beta_quotient_pfp_division_residual_data_input_entry * S ((S (fom_index_pfp_division_residual_data_input)) * ac) + (fom_value_pfp_division_residual_data_input))) /\ (exists fom_gap_pfp_division_residual_data_input_value_bound. fom_gap_pfp_division_residual_data_input_value_bound + S (fom_value_pfp_division_residual_data_input) = p))) -> exists pb pc ub uc t rb rc R. (((forall pfc_index_division_residual_data_resultproduct. (exists pfa_gap_division_residual_data_resultproductbound. pfa_gap_division_residual_data_resultproductbound + S (pfc_index_division_residual_data_resultproduct) = (L)) -> exists pfc_value_division_residual_data_resultproduct. ((((exists ff_h_pfp_division_residual_data_resultproductentry. ff_h_pfp_division_residual_data_resultproductentry + S (pfc_value_division_residual_data_resultproduct) = S ((S (pfc_index_division_residual_data_resultproduct)) * pc)) /\ exists ff_q_pfp_division_residual_data_resultproductentry. pb = ff_q_pfp_division_residual_data_resultproductentry * S ((S (pfc_index_division_residual_data_resultproduct)) * pc) + (pfc_value_division_residual_data_resultproduct))) /\ ((exists pfc_terms_code_division_residual_data_resultproductcoefficient pfc_terms_scale_division_residual_data_resultproductcoefficient pfc_natural_sum_division_residual_data_resultproductcoefficient. ((forall pfc_index_division_residual_data_resultproductcoefficientdiagonal. (exists pfa_gap_division_residual_data_resultproductcoefficientdiagonalbound. pfa_gap_division_residual_data_resultproductcoefficientdiagonalbound + S (pfc_index_division_residual_data_resultproductcoefficientdiagonal) = (S (pfc_index_division_residual_data_resultproduct))) -> exists pfc_value_division_residual_data_resultproductcoefficientdiagonal. ((((exists ff_h_pfp_division_residual_data_resultproductcoefficientdiagonalentry. ff_h_pfp_division_residual_data_resultproductcoefficientdiagonalentry + S (pfc_value_division_residual_data_resultproductcoefficientdiagonal) = S ((S (pfc_index_division_residual_data_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_residual_data_resultproductcoefficient)) /\ exists ff_q_pfp_division_residual_data_resultproductcoefficientdiagonalentry. pfc_terms_code_division_residual_data_resultproductcoefficient = ff_q_pfp_division_residual_data_resultproductcoefficientdiagonalentry * S ((S (pfc_index_division_residual_data_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_residual_data_resultproductcoefficient) + (pfc_value_division_residual_data_resultproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm pfc_left_division_residual_data_resultproductcoefficientdiagonalterm pfc_right_division_residual_data_resultproductcoefficientdiagonalterm. (((pfc_index_division_residual_data_resultproductcoefficientdiagonal)+pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm=(pfc_index_division_residual_data_resultproduct)) /\ ((((((exists pfa_gap_division_residual_data_resultproductcoefficientdiagonaltermleftinside. pfa_gap_division_residual_data_resultproductcoefficientdiagonaltermleftinside + S (pfc_index_division_residual_data_resultproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_residual_data_resultproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_residual_data_resultproductcoefficientdiagonaltermleftentry + S (pfc_left_division_residual_data_resultproductcoefficientdiagonalterm) = S ((S (pfc_index_division_residual_data_resultproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_residual_data_resultproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_residual_data_resultproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_residual_data_resultproductcoefficientdiagonal)) * qc) + (pfc_left_division_residual_data_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_residual_data_resultproductcoefficientdiagonaltermleftoutside. pfc_gap_division_residual_data_resultproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_residual_data_resultproductcoefficientdiagonal)) /\ (((pfc_left_division_residual_data_resultproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_residual_data_resultproductcoefficientdiagonaltermrightinside. pfa_gap_division_residual_data_resultproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_residual_data_resultproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_residual_data_resultproductcoefficientdiagonaltermrightentry + S (pfc_right_division_residual_data_resultproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_residual_data_resultproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_residual_data_resultproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_residual_data_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_residual_data_resultproductcoefficientdiagonaltermrightoutside. pfc_gap_division_residual_data_resultproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_residual_data_resultproductcoefficientdiagonalterm)) /\ (((pfc_right_division_residual_data_resultproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_residual_data_resultproductcoefficientdiagonal)=pfc_left_division_residual_data_resultproductcoefficientdiagonalterm*pfc_right_division_residual_data_resultproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_residual_data_resultproductcoefficientsum fs_v_pfc_division_residual_data_resultproductcoefficientsum. ((((exists fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_start. fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_start. fs_u_pfc_division_residual_data_resultproductcoefficientsum = fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_terminal. fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_residual_data_resultproductcoefficient) = S ((S (S (pfc_index_division_residual_data_resultproduct))) * fs_v_pfc_division_residual_data_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_terminal. fs_u_pfc_division_residual_data_resultproductcoefficientsum = fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_residual_data_resultproduct))) * fs_v_pfc_division_residual_data_resultproductcoefficientsum) + (pfc_natural_sum_division_residual_data_resultproductcoefficient))) /\ forall fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_residual_data_resultproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_residual_data_resultproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps = S (pfc_index_division_residual_data_resultproduct)) -> exists fs_a_pfc_division_residual_data_resultproductcoefficientsum_body_steps fs_r_pfc_division_residual_data_resultproductcoefficientsum_body_steps fs_s_pfc_division_residual_data_resultproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_summand. fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_residual_data_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_residual_data_resultproductcoefficient)) /\ exists fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_summand. pfc_terms_code_division_residual_data_resultproductcoefficient = fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_residual_data_resultproductcoefficient) + (fs_a_pfc_division_residual_data_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_partial. fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_residual_data_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_partial. fs_u_pfc_division_residual_data_resultproductcoefficientsum = fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum) + (fs_r_pfc_division_residual_data_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_successor. fs_h_pfc_division_residual_data_resultproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_residual_data_resultproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_successor. fs_u_pfc_division_residual_data_resultproductcoefficientsum = fs_q_pfc_division_residual_data_resultproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_residual_data_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_residual_data_resultproductcoefficientsum) + (fs_s_pfc_division_residual_data_resultproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_residual_data_resultproductcoefficientsum_body_steps = fs_r_pfc_division_residual_data_resultproductcoefficientsum_body_steps + fs_a_pfc_division_residual_data_resultproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_residual_data_resultproductcoefficientresiduebound. pfa_gap_division_residual_data_resultproductcoefficientresiduebound + S (pfc_value_division_residual_data_resultproduct) = (p)) /\ ((exists pfa_offset_left_division_residual_data_resultproductcoefficientresiduecongruence pfa_offset_right_division_residual_data_resultproductcoefficientresiduecongruence. (pfc_natural_sum_division_residual_data_resultproductcoefficient) + (p) * pfa_offset_left_division_residual_data_resultproductcoefficientresiduecongruence = (pfc_value_division_residual_data_resultproduct) + (p) * pfa_offset_right_division_residual_data_resultproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_residual_data_resultdifference. (exists pfa_gap_division_residual_data_resultdifferenceindex. pfa_gap_division_residual_data_resultdifferenceindex + S (pfs_index_division_residual_data_resultdifference) = (L)) -> exists pfs_left_division_residual_data_resultdifference pfs_right_division_residual_data_resultdifference pfs_result_division_residual_data_resultdifference. ((((exists ff_h_pfp_division_residual_data_resultdifferenceleft. ff_h_pfp_division_residual_data_resultdifferenceleft + S (pfs_left_division_residual_data_resultdifference) = S ((S (pfs_index_division_residual_data_resultdifference)) * ac)) /\ exists ff_q_pfp_division_residual_data_resultdifferenceleft. ab = ff_q_pfp_division_residual_data_resultdifferenceleft * S ((S (pfs_index_division_residual_data_resultdifference)) * ac) + (pfs_left_division_residual_data_resultdifference))) /\ (((((exists ff_h_pfp_division_residual_data_resultdifferenceright. ff_h_pfp_division_residual_data_resultdifferenceright + S (pfs_right_division_residual_data_resultdifference) = S ((S (pfs_index_division_residual_data_resultdifference)) * pc)) /\ exists ff_q_pfp_division_residual_data_resultdifferenceright. pb = ff_q_pfp_division_residual_data_resultdifferenceright * S ((S (pfs_index_division_residual_data_resultdifference)) * pc) + (pfs_right_division_residual_data_resultdifference))) /\ (((((exists ff_h_pfp_division_residual_data_resultdifferenceresult. ff_h_pfp_division_residual_data_resultdifferenceresult + S (pfs_result_division_residual_data_resultdifference) = S ((S (pfs_index_division_residual_data_resultdifference)) * uc)) /\ exists ff_q_pfp_division_residual_data_resultdifferenceresult. ub = ff_q_pfp_division_residual_data_resultdifferenceresult * S ((S (pfs_index_division_residual_data_resultdifference)) * uc) + (pfs_result_division_residual_data_resultdifference))) /\ ((((exists pfa_gap_division_residual_data_resultdifferenceoperationleft. pfa_gap_division_residual_data_resultdifferenceoperationleft + S (pfs_right_division_residual_data_resultdifference) = (p)) /\ (((exists pfa_gap_division_residual_data_resultdifferenceoperationright. pfa_gap_division_residual_data_resultdifferenceoperationright + S (pfs_result_division_residual_data_resultdifference) = (p)) /\ ((((exists pfa_gap_division_residual_data_resultdifferenceoperationresultbound. pfa_gap_division_residual_data_resultdifferenceoperationresultbound + S (pfs_left_division_residual_data_resultdifference) = (p)) /\ ((exists pfa_offset_left_division_residual_data_resultdifferenceoperationresultcongruence pfa_offset_right_division_residual_data_resultdifferenceoperationresultcongruence. ((pfs_right_division_residual_data_resultdifference) + (pfs_result_division_residual_data_resultdifference)) + (p) * pfa_offset_left_division_residual_data_resultdifferenceoperationresultcongruence = (pfs_left_division_residual_data_resultdifference) + (p) * pfa_offset_right_division_residual_data_resultdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_residual_data_resulttriminput. (exists fom_gap_pfp_division_residual_data_resulttriminput_index_bound. fom_gap_pfp_division_residual_data_resulttriminput_index_bound + S (fom_index_pfp_division_residual_data_resulttriminput) = L) -> exists fom_value_pfp_division_residual_data_resulttriminput. ((((exists fom_beta_height_pfp_division_residual_data_resulttriminput_entry. fom_beta_height_pfp_division_residual_data_resulttriminput_entry + S (fom_value_pfp_division_residual_data_resulttriminput) = S ((S (fom_index_pfp_division_residual_data_resulttriminput)) * uc)) /\ exists fom_beta_quotient_pfp_division_residual_data_resulttriminput_entry. ub = fom_beta_quotient_pfp_division_residual_data_resulttriminput_entry * S ((S (fom_index_pfp_division_residual_data_resulttriminput)) * uc) + (fom_value_pfp_division_residual_data_resulttriminput))) /\ (exists fom_gap_pfp_division_residual_data_resulttriminput_value_bound. fom_gap_pfp_division_residual_data_resulttriminput_value_bound + S (fom_value_pfp_division_residual_data_resulttriminput) = p))) /\ (((forall pfp_repeat_index_division_residual_data_resulttrimremoved. (exists pfa_gap_division_residual_data_resulttrimremovedindex. pfa_gap_division_residual_data_resulttrimremovedindex + S (pfp_repeat_index_division_residual_data_resulttrimremoved) = (t)) -> (((exists ff_h_pfp_division_residual_data_resulttrimremovedentry. ff_h_pfp_division_residual_data_resulttrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_residual_data_resulttrimremoved)) * uc)) /\ exists ff_q_pfp_division_residual_data_resulttrimremovedentry. ub = ff_q_pfp_division_residual_data_resulttrimremovedentry * S ((S (pfp_repeat_index_division_residual_data_resulttrimremoved)) * uc) + (0)))) /\ (((forall pftrim_index_division_residual_data_resulttrimsuffix pftrim_value_division_residual_data_resulttrimsuffix. (exists pfa_gap_division_residual_data_resulttrimsuffixbound. pfa_gap_division_residual_data_resulttrimsuffixbound + S (pftrim_index_division_residual_data_resulttrimsuffix) = (R)) -> (((exists ff_h_pfp_division_residual_data_resulttrimsuffixsource. ff_h_pfp_division_residual_data_resulttrimsuffixsource + S (pftrim_value_division_residual_data_resulttrimsuffix) = S ((S ((t)+pftrim_index_division_residual_data_resulttrimsuffix)) * uc)) /\ exists ff_q_pfp_division_residual_data_resulttrimsuffixsource. ub = ff_q_pfp_division_residual_data_resulttrimsuffixsource * S ((S ((t)+pftrim_index_division_residual_data_resulttrimsuffix)) * uc) + (pftrim_value_division_residual_data_resulttrimsuffix))) -> (((exists ff_h_pfp_division_residual_data_resulttrimsuffixoutput. ff_h_pfp_division_residual_data_resulttrimsuffixoutput + S (pftrim_value_division_residual_data_resulttrimsuffix) = S ((S (pftrim_index_division_residual_data_resulttrimsuffix)) * rc)) /\ exists ff_q_pfp_division_residual_data_resulttrimsuffixoutput. rb = ff_q_pfp_division_residual_data_resulttrimsuffixoutput * S ((S (pftrim_index_division_residual_data_resulttrimsuffix)) * rc) + (pftrim_value_division_residual_data_resulttrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_residual_data_resulttrimnormal. ((((exists ff_h_pfp_division_residual_data_resulttrimnormalentry. ff_h_pfp_division_residual_data_resulttrimnormalentry + S (pftrim_leading_division_residual_data_resulttrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_residual_data_resulttrimnormalentry. rb = ff_q_pfp_division_residual_data_resulttrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_residual_data_resulttrimnormal))) /\ ((~(pftrim_leading_division_residual_data_resulttrimnormal=0))))))))))))))))))))

Constructive proof overview

Generated structural guide

Construct the actual ambient product, residual and normalized trim as a separate stage; none is supplied as an oracle or identity premise.

The unchanged tactic script uses 6 declared prerequisites and contains 90 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_convolution_prefix_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized prime_field_polynomial_subtract_exists Alpha theorem; checked-use authorized prime_field_convolution_prefix_bounded Alpha theorem; checked-use authorized prime_field_polynomial_trim_exists Alpha theorem; checked-use authorized prime_field_polynomial_subtract_bounded Alpha theorem; checked-use authorized

Direct dependents

PX0039 prime_field_polynomial_division_execution_exists

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

90 script commands · 21 reading checkpoints · 4 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.

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 ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro q
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hp
  2. L12
    intro ha
03Establish hproductL13–22

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

  1. L13
    have hproduct : ∃ pb. ∃ pc. FpConvolutionPrefix(p,qb,qc,q,bb,bc,S d,pb,pc,L)Definitions: FpConvolutionPrefix
  2. L14
    specialize prime_field_convolution_prefix_exists (p)
  3. L15
    specialize prime_field_convolution_prefix_exists (qb)
  4. L16
    specialize prime_field_convolution_prefix_exists (qc)
  5. L17
    specialize prime_field_convolution_prefix_exists (q)
  6. L18
    specialize prime_field_convolution_prefix_exists (bb)
  7. L19
    specialize prime_field_convolution_prefix_exists (bc)
  8. L20
    specialize prime_field_convolution_prefix_exists (S d)
  9. L21
    specialize prime_field_convolution_prefix_exists (L)
  10. L22
    apply prime_field_convolution_prefix_exists
04Fix variables and assumptionsL23–23

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

  1. L23
    intro hz
05Use earlier factsL24–27

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

  1. L24
    specialize prime_nonzero (p)
  2. L25
    apply prime_nonzero
  3. L26
    exact hp
  4. L27
    exact hz
06Separate the logical casesL28–29

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

  1. L28
    cases hproduct
  2. L29
    cases hproduct_witness
07Establish hresidualL30–39

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

  1. L30
    have hresidual : ∃ ub. ∃ uc. FpCoefficientSubtraction(p,ab,ac,x,x1,ub,uc,L)Definitions: FpCoefficientSubtraction
  2. L31
    specialize prime_field_polynomial_subtract_exists (p)
  3. L32
    specialize prime_field_polynomial_subtract_exists (ab)
  4. L33
    specialize prime_field_polynomial_subtract_exists (ac)
  5. L34
    specialize prime_field_polynomial_subtract_exists (x)
  6. L35
    specialize prime_field_polynomial_subtract_exists (x1)
  7. L36
    specialize prime_field_polynomial_subtract_exists (L)
  8. L37
    apply prime_field_polynomial_subtract_exists
  9. L38
    exact hp
  10. L39
    exact ha
08Use earlier factsL40–49

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

  1. L40
    specialize prime_field_convolution_prefix_bounded (p)
  2. L41
    specialize prime_field_convolution_prefix_bounded (qb)
  3. L42
    specialize prime_field_convolution_prefix_bounded (qc)
  4. L43
    specialize prime_field_convolution_prefix_bounded (q)
  5. L44
    specialize prime_field_convolution_prefix_bounded (bb)
  6. L45
    specialize prime_field_convolution_prefix_bounded (bc)
  7. L46
    specialize prime_field_convolution_prefix_bounded (S d)
  8. L47
    specialize prime_field_convolution_prefix_bounded (x)
  9. L48
    specialize prime_field_convolution_prefix_bounded (x1)
  10. L49
    specialize prime_field_convolution_prefix_bounded (L)
09Use earlier factsL50–51

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

  1. L50
    apply prime_field_convolution_prefix_bounded
  2. L51
    exact hproduct_witness_witness
10Separate the logical casesL52–53

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

  1. L52
    cases hresidual
  2. L53
    cases hresidual_witness
11Establish htrimL54–59

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

  1. L54
    have htrim : ∃ t. ∃ rb. ∃ rc. ∃ R. FpPolynomialTrim(p,x2,x3,L,t,rb,rc,R)Definitions: FpPolynomialTrim
  2. L55
    specialize prime_field_polynomial_trim_exists (p)
  3. L56
    specialize prime_field_polynomial_trim_exists (x2)
  4. L57
    specialize prime_field_polynomial_trim_exists (x3)
  5. L58
    specialize prime_field_polynomial_trim_exists (L)
  6. L59
    apply prime_field_polynomial_trim_exists
12Establish hcanonicalL60–69

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

  1. L60
    have hcanonical : BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(x,x1,L,p) ∧ BetaPrefixInto(x2,x3,L,p))Definitions: BetaPrefixInto
  2. L61
    specialize prime_field_polynomial_subtract_bounded (p)
  3. L62
    specialize prime_field_polynomial_subtract_bounded (ab)
  4. L63
    specialize prime_field_polynomial_subtract_bounded (ac)
  5. L64
    specialize prime_field_polynomial_subtract_bounded (x)
  6. L65
    specialize prime_field_polynomial_subtract_bounded (x1)
  7. L66
    specialize prime_field_polynomial_subtract_bounded (x2)
  8. L67
    specialize prime_field_polynomial_subtract_bounded (x3)
  9. L68
    specialize prime_field_polynomial_subtract_bounded (L)
  10. L69
    apply prime_field_polynomial_subtract_bounded
13Use earlier factsL70–70

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

  1. L70
    exact hresidual_witness_witness
14Separate the logical casesL71–72

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

  1. L71
    cases hcanonical
  2. L72
    cases hcanonical_right
15Use earlier factsL73–73

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

  1. L73
    exact hcanonical_right_right
16Separate the logical casesL74–77

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

  1. L74
    cases htrim
  2. L75
    cases htrim_witness
  3. L76
    cases htrim_witness_witness
  4. L77
    cases htrim_witness_witness_witness
17Construct an explicit witnessL78–85

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

  1. L78
    exists x
  2. L79
    exists x1
  3. L80
    exists x2
  4. L81
    exists x3
  5. L82
    exists x4
  6. L83
    exists x5
  7. L84
    exists x6
  8. L85
    exists x7
18Separate the logical casesL86–86

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

  1. L86
    split
19Use earlier factsL87–87

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

  1. L87
    exact hproduct_witness_witness
20Separate the logical casesL88–88

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

  1. L88
    split
21Use earlier factsL89–90

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

  1. L89
    exact hresidual_witness_witness
  2. L90
    exact htrim_witness_witness_witness_witness

Library-wide reading audit

Original exact command ledger · 90 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro q
  11. 0011intro hp
  12. 0012intro ha
  13. 0013have hproduct : exists pb pc. (forall pfc_index_division_residual_product. (exists pfa_gap_division_residual_productbound. pfa_gap_division_residual_productbound + S (pfc_index_division_residual_product) = (L)) -> exists pfc_value_division_residual_product. ((((exists ff_h_pfp_division_residual_productentry. ff_h_pfp_division_residual_productentry + S (pfc_value_division_residual_product) = S ((S (pfc_index_division_residual_product)) * pc)) /\ exists ff_q_pfp_division_residual_productentry. pb = ff_q_pfp_division_residual_productentry * S ((S (pfc_index_division_residual_product)) * pc) + (pfc_value_division_residual_product))) /\ ((exists pfc_terms_code_division_residual_productcoefficient pfc_terms_scale_division_residual_productcoefficient pfc_natural_sum_division_residual_productcoefficient. ((forall pfc_index_division_residual_productcoefficientdiagonal. (exists pfa_gap_division_residual_productcoefficientdiagonalbound. pfa_gap_division_residual_productcoefficientdiagonalbound + S (pfc_index_division_residual_productcoefficientdiagonal) = (S (pfc_index_division_residual_product))) -> exists pfc_value_division_residual_productcoefficientdiagonal. ((((exists ff_h_pfp_division_residual_productcoefficientdiagonalentry. ff_h_pfp_division_residual_productcoefficientdiagonalentry + S (pfc_value_division_residual_productcoefficientdiagonal) = S ((S (pfc_index_division_residual_productcoefficientdiagonal)) * pfc_terms_scale_division_residual_productcoefficient)) /\ exists ff_q_pfp_division_residual_productcoefficientdiagonalentry. pfc_terms_code_division_residual_productcoefficient = ff_q_pfp_division_residual_productcoefficientdiagonalentry * S ((S (pfc_index_division_residual_productcoefficientdiagonal)) * pfc_terms_scale_division_residual_productcoefficient) + (pfc_value_division_residual_productcoefficientdiagonal))) /\ ((exists pfc_complement_division_residual_productcoefficientdiagonalterm pfc_left_division_residual_productcoefficientdiagonalterm pfc_right_division_residual_productcoefficientdiagonalterm. (((pfc_index_division_residual_productcoefficientdiagonal)+pfc_complement_division_residual_productcoefficientdiagonalterm=(pfc_index_division_residual_product)) /\ ((((((exists pfa_gap_division_residual_productcoefficientdiagonaltermleftinside. pfa_gap_division_residual_productcoefficientdiagonaltermleftinside + S (pfc_index_division_residual_productcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_residual_productcoefficientdiagonaltermleftentry. ff_h_pfp_division_residual_productcoefficientdiagonaltermleftentry + S (pfc_left_division_residual_productcoefficientdiagonalterm) = S ((S (pfc_index_division_residual_productcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_residual_productcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_residual_productcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_residual_productcoefficientdiagonal)) * qc) + (pfc_left_division_residual_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_residual_productcoefficientdiagonaltermleftoutside. pfc_gap_division_residual_productcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_residual_productcoefficientdiagonal)) /\ (((pfc_left_division_residual_productcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_residual_productcoefficientdiagonaltermrightinside. pfa_gap_division_residual_productcoefficientdiagonaltermrightinside + S (pfc_complement_division_residual_productcoefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_residual_productcoefficientdiagonaltermrightentry. ff_h_pfp_division_residual_productcoefficientdiagonaltermrightentry + S (pfc_right_division_residual_productcoefficientdiagonalterm) = S ((S (pfc_complement_division_residual_productcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_residual_productcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_residual_productcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_residual_productcoefficientdiagonalterm)) * bc) + (pfc_right_division_residual_productcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_residual_productcoefficientdiagonaltermrightoutside. pfc_gap_division_residual_productcoefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_residual_productcoefficientdiagonalterm)) /\ (((pfc_right_division_residual_productcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_residual_productcoefficientdiagonal)=pfc_left_division_residual_productcoefficientdiagonalterm*pfc_right_division_residual_productcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_residual_productcoefficientsum fs_v_pfc_division_residual_productcoefficientsum. ((((exists fs_h_pfc_division_residual_productcoefficientsum_body_start. fs_h_pfc_division_residual_productcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_residual_productcoefficientsum)) /\ exists fs_q_pfc_division_residual_productcoefficientsum_body_start. fs_u_pfc_division_residual_productcoefficientsum = fs_q_pfc_division_residual_productcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_residual_productcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_residual_productcoefficientsum_body_terminal. fs_h_pfc_division_residual_productcoefficientsum_body_terminal + S (pfc_natural_sum_division_residual_productcoefficient) = S ((S (S (pfc_index_division_residual_product))) * fs_v_pfc_division_residual_productcoefficientsum)) /\ exists fs_q_pfc_division_residual_productcoefficientsum_body_terminal. fs_u_pfc_division_residual_productcoefficientsum = fs_q_pfc_division_residual_productcoefficientsum_body_terminal * S ((S (S (pfc_index_division_residual_product))) * fs_v_pfc_division_residual_productcoefficientsum) + (pfc_natural_sum_division_residual_productcoefficient))) /\ forall fs_i_pfc_division_residual_productcoefficientsum_body_steps. (exists fs_lt_pfc_division_residual_productcoefficientsum_body_steps_bound. fs_lt_pfc_division_residual_productcoefficientsum_body_steps_bound + S fs_i_pfc_division_residual_productcoefficientsum_body_steps = S (pfc_index_division_residual_product)) -> exists fs_a_pfc_division_residual_productcoefficientsum_body_steps fs_r_pfc_division_residual_productcoefficientsum_body_steps fs_s_pfc_division_residual_productcoefficientsum_body_steps. ((((exists fs_h_pfc_division_residual_productcoefficientsum_body_steps_summand. fs_h_pfc_division_residual_productcoefficientsum_body_steps_summand + S (fs_a_pfc_division_residual_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * pfc_terms_scale_division_residual_productcoefficient)) /\ exists fs_q_pfc_division_residual_productcoefficientsum_body_steps_summand. pfc_terms_code_division_residual_productcoefficient = fs_q_pfc_division_residual_productcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * pfc_terms_scale_division_residual_productcoefficient) + (fs_a_pfc_division_residual_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_residual_productcoefficientsum_body_steps_partial. fs_h_pfc_division_residual_productcoefficientsum_body_steps_partial + S (fs_r_pfc_division_residual_productcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * fs_v_pfc_division_residual_productcoefficientsum)) /\ exists fs_q_pfc_division_residual_productcoefficientsum_body_steps_partial. fs_u_pfc_division_residual_productcoefficientsum = fs_q_pfc_division_residual_productcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * fs_v_pfc_division_residual_productcoefficientsum) + (fs_r_pfc_division_residual_productcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_residual_productcoefficientsum_body_steps_successor. fs_h_pfc_division_residual_productcoefficientsum_body_steps_successor + S (fs_s_pfc_division_residual_productcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * fs_v_pfc_division_residual_productcoefficientsum)) /\ exists fs_q_pfc_division_residual_productcoefficientsum_body_steps_successor. fs_u_pfc_division_residual_productcoefficientsum = fs_q_pfc_division_residual_productcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_residual_productcoefficientsum_body_steps)) * fs_v_pfc_division_residual_productcoefficientsum) + (fs_s_pfc_division_residual_productcoefficientsum_body_steps))) /\ fs_s_pfc_division_residual_productcoefficientsum_body_steps = fs_r_pfc_division_residual_productcoefficientsum_body_steps + fs_a_pfc_division_residual_productcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_residual_productcoefficientresiduebound. pfa_gap_division_residual_productcoefficientresiduebound + S (pfc_value_division_residual_product) = (p)) /\ ((exists pfa_offset_left_division_residual_productcoefficientresiduecongruence pfa_offset_right_division_residual_productcoefficientresiduecongruence. (pfc_natural_sum_division_residual_productcoefficient) + (p) * pfa_offset_left_division_residual_productcoefficientresiduecongruence = (pfc_value_division_residual_product) + (p) * pfa_offset_right_division_residual_productcoefficientresiduecongruence))))))))))))
  14. 0014specialize prime_field_convolution_prefix_exists (p)
  15. 0015specialize prime_field_convolution_prefix_exists (qb)
  16. 0016specialize prime_field_convolution_prefix_exists (qc)
  17. 0017specialize prime_field_convolution_prefix_exists (q)
  18. 0018specialize prime_field_convolution_prefix_exists (bb)
  19. 0019specialize prime_field_convolution_prefix_exists (bc)
  20. 0020specialize prime_field_convolution_prefix_exists (S d)
  21. 0021specialize prime_field_convolution_prefix_exists (L)
  22. 0022apply prime_field_convolution_prefix_exists
  23. 0023intro hz
  24. 0024specialize prime_nonzero (p)
  25. 0025apply prime_nonzero
  26. 0026exact hp
  27. 0027exact hz
  28. 0028cases hproduct
  29. 0029cases hproduct_witness
  30. 0030have hresidual : exists ub uc. (forall pfs_index_division_residual_difference. (exists pfa_gap_division_residual_differenceindex. pfa_gap_division_residual_differenceindex + S (pfs_index_division_residual_difference) = (L)) -> exists pfs_left_division_residual_difference pfs_right_division_residual_difference pfs_result_division_residual_difference. ((((exists ff_h_pfp_division_residual_differenceleft. ff_h_pfp_division_residual_differenceleft + S (pfs_left_division_residual_difference) = S ((S (pfs_index_division_residual_difference)) * ac)) /\ exists ff_q_pfp_division_residual_differenceleft. ab = ff_q_pfp_division_residual_differenceleft * S ((S (pfs_index_division_residual_difference)) * ac) + (pfs_left_division_residual_difference))) /\ (((((exists ff_h_pfp_division_residual_differenceright. ff_h_pfp_division_residual_differenceright + S (pfs_right_division_residual_difference) = S ((S (pfs_index_division_residual_difference)) * x1)) /\ exists ff_q_pfp_division_residual_differenceright. x = ff_q_pfp_division_residual_differenceright * S ((S (pfs_index_division_residual_difference)) * x1) + (pfs_right_division_residual_difference))) /\ (((((exists ff_h_pfp_division_residual_differenceresult. ff_h_pfp_division_residual_differenceresult + S (pfs_result_division_residual_difference) = S ((S (pfs_index_division_residual_difference)) * uc)) /\ exists ff_q_pfp_division_residual_differenceresult. ub = ff_q_pfp_division_residual_differenceresult * S ((S (pfs_index_division_residual_difference)) * uc) + (pfs_result_division_residual_difference))) /\ ((((exists pfa_gap_division_residual_differenceoperationleft. pfa_gap_division_residual_differenceoperationleft + S (pfs_right_division_residual_difference) = (p)) /\ (((exists pfa_gap_division_residual_differenceoperationright. pfa_gap_division_residual_differenceoperationright + S (pfs_result_division_residual_difference) = (p)) /\ ((((exists pfa_gap_division_residual_differenceoperationresultbound. pfa_gap_division_residual_differenceoperationresultbound + S (pfs_left_division_residual_difference) = (p)) /\ ((exists pfa_offset_left_division_residual_differenceoperationresultcongruence pfa_offset_right_division_residual_differenceoperationresultcongruence. ((pfs_right_division_residual_difference) + (pfs_result_division_residual_difference)) + (p) * pfa_offset_left_division_residual_differenceoperationresultcongruence = (pfs_left_division_residual_difference) + (p) * pfa_offset_right_division_residual_differenceoperationresultcongruence))))))))))))))))
  31. 0031specialize prime_field_polynomial_subtract_exists (p)
  32. 0032specialize prime_field_polynomial_subtract_exists (ab)
  33. 0033specialize prime_field_polynomial_subtract_exists (ac)
  34. 0034specialize prime_field_polynomial_subtract_exists (x)
  35. 0035specialize prime_field_polynomial_subtract_exists (x1)
  36. 0036specialize prime_field_polynomial_subtract_exists (L)
  37. 0037apply prime_field_polynomial_subtract_exists
  38. 0038exact hp
  39. 0039exact ha
  40. 0040specialize prime_field_convolution_prefix_bounded (p)
  41. 0041specialize prime_field_convolution_prefix_bounded (qb)
  42. 0042specialize prime_field_convolution_prefix_bounded (qc)
  43. 0043specialize prime_field_convolution_prefix_bounded (q)
  44. 0044specialize prime_field_convolution_prefix_bounded (bb)
  45. 0045specialize prime_field_convolution_prefix_bounded (bc)
  46. 0046specialize prime_field_convolution_prefix_bounded (S d)
  47. 0047specialize prime_field_convolution_prefix_bounded (x)
  48. 0048specialize prime_field_convolution_prefix_bounded (x1)
  49. 0049specialize prime_field_convolution_prefix_bounded (L)
  50. 0050apply prime_field_convolution_prefix_bounded
  51. 0051exact hproduct_witness_witness
  52. 0052cases hresidual
  53. 0053cases hresidual_witness
  54. 0054have htrim : exists t rb rc R. ((((L)=(t)+(R)) /\ (((forall fom_index_pfp_division_residual_triminput. (exists fom_gap_pfp_division_residual_triminput_index_bound. fom_gap_pfp_division_residual_triminput_index_bound + S (fom_index_pfp_division_residual_triminput) = L) -> exists fom_value_pfp_division_residual_triminput. ((((exists fom_beta_height_pfp_division_residual_triminput_entry. fom_beta_height_pfp_division_residual_triminput_entry + S (fom_value_pfp_division_residual_triminput) = S ((S (fom_index_pfp_division_residual_triminput)) * x3)) /\ exists fom_beta_quotient_pfp_division_residual_triminput_entry. x2 = fom_beta_quotient_pfp_division_residual_triminput_entry * S ((S (fom_index_pfp_division_residual_triminput)) * x3) + (fom_value_pfp_division_residual_triminput))) /\ (exists fom_gap_pfp_division_residual_triminput_value_bound. fom_gap_pfp_division_residual_triminput_value_bound + S (fom_value_pfp_division_residual_triminput) = p))) /\ (((forall pfp_repeat_index_division_residual_trimremoved. (exists pfa_gap_division_residual_trimremovedindex. pfa_gap_division_residual_trimremovedindex + S (pfp_repeat_index_division_residual_trimremoved) = (t)) -> (((exists ff_h_pfp_division_residual_trimremovedentry. ff_h_pfp_division_residual_trimremovedentry + S (0) = S ((S (pfp_repeat_index_division_residual_trimremoved)) * x3)) /\ exists ff_q_pfp_division_residual_trimremovedentry. x2 = ff_q_pfp_division_residual_trimremovedentry * S ((S (pfp_repeat_index_division_residual_trimremoved)) * x3) + (0)))) /\ (((forall pftrim_index_division_residual_trimsuffix pftrim_value_division_residual_trimsuffix. (exists pfa_gap_division_residual_trimsuffixbound. pfa_gap_division_residual_trimsuffixbound + S (pftrim_index_division_residual_trimsuffix) = (R)) -> (((exists ff_h_pfp_division_residual_trimsuffixsource. ff_h_pfp_division_residual_trimsuffixsource + S (pftrim_value_division_residual_trimsuffix) = S ((S ((t)+pftrim_index_division_residual_trimsuffix)) * x3)) /\ exists ff_q_pfp_division_residual_trimsuffixsource. x2 = ff_q_pfp_division_residual_trimsuffixsource * S ((S ((t)+pftrim_index_division_residual_trimsuffix)) * x3) + (pftrim_value_division_residual_trimsuffix))) -> (((exists ff_h_pfp_division_residual_trimsuffixoutput. ff_h_pfp_division_residual_trimsuffixoutput + S (pftrim_value_division_residual_trimsuffix) = S ((S (pftrim_index_division_residual_trimsuffix)) * rc)) /\ exists ff_q_pfp_division_residual_trimsuffixoutput. rb = ff_q_pfp_division_residual_trimsuffixoutput * S ((S (pftrim_index_division_residual_trimsuffix)) * rc) + (pftrim_value_division_residual_trimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_residual_trimnormal. ((((exists ff_h_pfp_division_residual_trimnormalentry. ff_h_pfp_division_residual_trimnormalentry + S (pftrim_leading_division_residual_trimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_residual_trimnormalentry. rb = ff_q_pfp_division_residual_trimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_residual_trimnormal))) /\ ((~(pftrim_leading_division_residual_trimnormal=0)))))))))))))))
  55. 0055specialize prime_field_polynomial_trim_exists (p)
  56. 0056specialize prime_field_polynomial_trim_exists (x2)
  57. 0057specialize prime_field_polynomial_trim_exists (x3)
  58. 0058specialize prime_field_polynomial_trim_exists (L)
  59. 0059apply prime_field_polynomial_trim_exists
  60. 0060have hcanonical : ((forall fom_index_pfp_division_residual_source_bound. (exists fom_gap_pfp_division_residual_source_bound_index_bound. fom_gap_pfp_division_residual_source_bound_index_bound + S (fom_index_pfp_division_residual_source_bound) = L) -> exists fom_value_pfp_division_residual_source_bound. ((((exists fom_beta_height_pfp_division_residual_source_bound_entry. fom_beta_height_pfp_division_residual_source_bound_entry + S (fom_value_pfp_division_residual_source_bound) = S ((S (fom_index_pfp_division_residual_source_bound)) * ac)) /\ exists fom_beta_quotient_pfp_division_residual_source_bound_entry. ab = fom_beta_quotient_pfp_division_residual_source_bound_entry * S ((S (fom_index_pfp_division_residual_source_bound)) * ac) + (fom_value_pfp_division_residual_source_bound))) /\ (exists fom_gap_pfp_division_residual_source_bound_value_bound. fom_gap_pfp_division_residual_source_bound_value_bound + S (fom_value_pfp_division_residual_source_bound) = p))) /\ (((forall fom_index_pfp_division_residual_product_bound. (exists fom_gap_pfp_division_residual_product_bound_index_bound. fom_gap_pfp_division_residual_product_bound_index_bound + S (fom_index_pfp_division_residual_product_bound) = L) -> exists fom_value_pfp_division_residual_product_bound. ((((exists fom_beta_height_pfp_division_residual_product_bound_entry. fom_beta_height_pfp_division_residual_product_bound_entry + S (fom_value_pfp_division_residual_product_bound) = S ((S (fom_index_pfp_division_residual_product_bound)) * x1)) /\ exists fom_beta_quotient_pfp_division_residual_product_bound_entry. x = fom_beta_quotient_pfp_division_residual_product_bound_entry * S ((S (fom_index_pfp_division_residual_product_bound)) * x1) + (fom_value_pfp_division_residual_product_bound))) /\ (exists fom_gap_pfp_division_residual_product_bound_value_bound. fom_gap_pfp_division_residual_product_bound_value_bound + S (fom_value_pfp_division_residual_product_bound) = p))) /\ ((forall fom_index_pfp_division_residual_result_bound. (exists fom_gap_pfp_division_residual_result_bound_index_bound. fom_gap_pfp_division_residual_result_bound_index_bound + S (fom_index_pfp_division_residual_result_bound) = L) -> exists fom_value_pfp_division_residual_result_bound. ((((exists fom_beta_height_pfp_division_residual_result_bound_entry. fom_beta_height_pfp_division_residual_result_bound_entry + S (fom_value_pfp_division_residual_result_bound) = S ((S (fom_index_pfp_division_residual_result_bound)) * x3)) /\ exists fom_beta_quotient_pfp_division_residual_result_bound_entry. x2 = fom_beta_quotient_pfp_division_residual_result_bound_entry * S ((S (fom_index_pfp_division_residual_result_bound)) * x3) + (fom_value_pfp_division_residual_result_bound))) /\ (exists fom_gap_pfp_division_residual_result_bound_value_bound. fom_gap_pfp_division_residual_result_bound_value_bound + S (fom_value_pfp_division_residual_result_bound) = p)))))))
  61. 0061specialize prime_field_polynomial_subtract_bounded (p)
  62. 0062specialize prime_field_polynomial_subtract_bounded (ab)
  63. 0063specialize prime_field_polynomial_subtract_bounded (ac)
  64. 0064specialize prime_field_polynomial_subtract_bounded (x)
  65. 0065specialize prime_field_polynomial_subtract_bounded (x1)
  66. 0066specialize prime_field_polynomial_subtract_bounded (x2)
  67. 0067specialize prime_field_polynomial_subtract_bounded (x3)
  68. 0068specialize prime_field_polynomial_subtract_bounded (L)
  69. 0069apply prime_field_polynomial_subtract_bounded
  70. 0070exact hresidual_witness_witness
  71. 0071cases hcanonical
  72. 0072cases hcanonical_right
  73. 0073exact hcanonical_right_right
  74. 0074cases htrim
  75. 0075cases htrim_witness
  76. 0076cases htrim_witness_witness
  77. 0077cases htrim_witness_witness_witness
  78. 0078exists x
  79. 0079exists x1
  80. 0080exists x2
  81. 0081exists x3
  82. 0082exists x4
  83. 0083exists x5
  84. 0084exists x6
  85. 0085exists x7
  86. 0086split
  87. 0087exact hproduct_witness_witness
  88. 0088split
  89. 0089exact hresidual_witness_witness
  90. 0090exact htrim_witness_witness_witness_witness