PP0022

prime_field_polynomial_horner_exists

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

Every canonical coefficient prefix and canonical base have an actual finite modular Horner history; no trace or norm invariant is supplied.

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 b c t l. (~((p) = 1) /\ forall pfa_factor_left_exists_prime pfa_factor_right_exists_prime. (p) = pfa_factor_left_exists_prime * pfa_factor_right_exists_prime -> pfa_factor_left_exists_prime = 1 \/ pfa_factor_right_exists_prime = 1) -> (forall fom_index_pfp_exists_coefficients. (exists fom_gap_pfp_exists_coefficients_index_bound. fom_gap_pfp_exists_coefficients_index_bound + S (fom_index_pfp_exists_coefficients) = l) -> exists fom_value_pfp_exists_coefficients. ((((exists fom_beta_height_pfp_exists_coefficients_entry. fom_beta_height_pfp_exists_coefficients_entry + S (fom_value_pfp_exists_coefficients) = S ((S (fom_index_pfp_exists_coefficients)) * c)) /\ exists fom_beta_quotient_pfp_exists_coefficients_entry. b = fom_beta_quotient_pfp_exists_coefficients_entry * S ((S (fom_index_pfp_exists_coefficients)) * c) + (fom_value_pfp_exists_coefficients))) /\ (exists fom_gap_pfp_exists_coefficients_value_bound. fom_gap_pfp_exists_coefficients_value_bound + S (fom_value_pfp_exists_coefficients) = p))) -> (exists pfa_gap_exists_base. pfa_gap_exists_base + S (t) = (p)) -> exists r. (exists pfh_trace_code_exists_execution pfh_trace_scale_exists_execution. (((exists pfa_gap_exists_executiontracebase. pfa_gap_exists_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_exists_executiontraceinitial. ff_h_pfp_exists_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontraceinitial. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontraceinitial * S ((S (0)) * pfh_trace_scale_exists_execution) + (0))) /\ (((((exists ff_h_pfp_exists_executiontraceterminal. ff_h_pfp_exists_executiontraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontraceterminal. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontraceterminal * S ((S (l)) * pfh_trace_scale_exists_execution) + (r))) /\ ((forall pfh_index_exists_executiontracesteps. (exists pfa_gap_exists_executiontracestepsindex. pfa_gap_exists_executiontracestepsindex + S (pfh_index_exists_executiontracesteps) = (l)) -> (exists pfh_coefficient_exists_executiontracestepsstep pfh_before_exists_executiontracestepsstep pfh_after_exists_executiontracestepsstep pfh_product_exists_executiontracestepsstep. ((((exists ff_h_pfp_exists_executiontracestepsstepcoefficient. ff_h_pfp_exists_executiontracestepsstepcoefficient + S (pfh_coefficient_exists_executiontracestepsstep) = S ((S (pfh_index_exists_executiontracesteps)) * c)) /\ exists ff_q_pfp_exists_executiontracestepsstepcoefficient. b = ff_q_pfp_exists_executiontracestepsstepcoefficient * S ((S (pfh_index_exists_executiontracesteps)) * c) + (pfh_coefficient_exists_executiontracestepsstep))) /\ (((((exists ff_h_pfp_exists_executiontracestepsstepbefore. ff_h_pfp_exists_executiontracestepsstepbefore + S (pfh_before_exists_executiontracestepsstep) = S ((S (pfh_index_exists_executiontracesteps)) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontracestepsstepbefore. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontracestepsstepbefore * S ((S (pfh_index_exists_executiontracesteps)) * pfh_trace_scale_exists_execution) + (pfh_before_exists_executiontracestepsstep))) /\ (((((exists ff_h_pfp_exists_executiontracestepsstepafter. ff_h_pfp_exists_executiontracestepsstepafter + S (pfh_after_exists_executiontracestepsstep) = S ((S (S (pfh_index_exists_executiontracesteps))) * pfh_trace_scale_exists_execution)) /\ exists ff_q_pfp_exists_executiontracestepsstepafter. pfh_trace_code_exists_execution = ff_q_pfp_exists_executiontracestepsstepafter * S ((S (S (pfh_index_exists_executiontracesteps))) * pfh_trace_scale_exists_execution) + (pfh_after_exists_executiontracestepsstep))) /\ (((((exists pfa_gap_exists_executiontracestepsstepmultiplyleft. pfa_gap_exists_executiontracestepsstepmultiplyleft + S (pfh_before_exists_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_exists_executiontracestepsstepmultiplyright. pfa_gap_exists_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_exists_executiontracestepsstepmultiplyresultbound. pfa_gap_exists_executiontracestepsstepmultiplyresultbound + S (pfh_product_exists_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_exists_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_exists_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_exists_executiontracestepsstepmultiplyresultcongruence = (pfh_product_exists_executiontracestepsstep) + (p) * pfa_offset_right_exists_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_exists_executiontracestepsstepaddleft. pfa_gap_exists_executiontracestepsstepaddleft + S (pfh_product_exists_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_exists_executiontracestepsstepaddright. pfa_gap_exists_executiontracestepsstepaddright + S (pfh_coefficient_exists_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_exists_executiontracestepsstepaddresultbound. pfa_gap_exists_executiontracestepsstepaddresultbound + S (pfh_after_exists_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_executiontracestepsstepaddresultcongruence pfa_offset_right_exists_executiontracestepsstepaddresultcongruence. ((pfh_product_exists_executiontracestepsstep) + (pfh_coefficient_exists_executiontracestepsstep)) + (p) * pfa_offset_left_exists_executiontracestepsstepaddresultcongruence = (pfh_after_exists_executiontracestepsstep) + (p) * pfa_offset_right_exists_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Constructive proof overview

Generated structural guide

Every canonical coefficient prefix and canonical base have an actual finite modular Horner history; no trace or norm invariant is supplied.

The unchanged tactic script uses 4 declared prerequisites and contains 53 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_horner_eval_exists Alpha theorem; checked-use authorized PP0002 prime_field_polynomial_normalization_exists prime_nonzero Stable theorem; checked-use authorized PP0021 prime_field_polynomial_horner_trace_from_normalization

Direct dependents

PP002A prime_field_polynomial_horner_exists_unique PP002B prime_field_polynomial_horner_empty_construct PP002C prime_field_polynomial_horner_successor_construct PP002F prime_field_polynomial_normalized_horner_iff PP0031 prime_field_polynomial_reduce_and_evaluate_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

53 script commands · 11 reading checkpoints · 3 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 normalization existsprime field polynomial horner trace from normalization

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

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

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro l
  6. L6
    intro hp
  7. L7
    intro hc
  8. L8
    intro ht
02Establish hnL9–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta horner eval exists.

  1. L9
    have hn : ∃ n. Horner(b,c,t,l,n)Definitions: Horner
  2. L10
    specialize beta_horner_eval_exists (b)
  3. L11
    specialize beta_horner_eval_exists (c)
  4. L12
    specialize beta_horner_eval_exists (t)
  5. L13
    specialize beta_horner_eval_exists (l)
  6. L14
    apply beta_horner_eval_exists
03Separate the logical casesL15–17

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

  1. L15
    cases hn
  2. L16
    cases hn_witness
  3. L17
    cases hn_witness_witness
04Establish hrL18–27

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

  1. L18
    have hr : ∃ U. ∃ V. FpCoefficientReduction(p,x1,x2,U,V,S l)Definitions: FpCoefficientReduction
  2. L19
    specialize prime_field_polynomial_normalization_exists (p)
  3. L20
    specialize prime_field_polynomial_normalization_exists (x1)
  4. L21
    specialize prime_field_polynomial_normalization_exists (x2)
  5. L22
    specialize prime_field_polynomial_normalization_exists (S l)
  6. L23
    apply prime_field_polynomial_normalization_exists
  7. L24
    intro hz
  8. L25
    specialize prime_nonzero (p)
  9. L26
    apply prime_nonzero
  10. L27
    exact hp
05Use earlier factsL28–28

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

  1. L28
    exact hz
06Separate the logical casesL29–30

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

  1. L29
    cases hr
  2. L30
    cases hr_witness
07Establish heL31–40

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

  1. L31
    have he : ∃ r. FpHornerTrace(p,b,c,t,l,r,x3,x4) ∧ CanonicalModularResidue(p,x,r)Definitions: CanonicalModularResidueFpHornerTrace
  2. L32
    specialize prime_field_polynomial_horner_trace_from_normalization (p)
  3. L33
    specialize prime_field_polynomial_horner_trace_from_normalization (b)
  4. L34
    specialize prime_field_polynomial_horner_trace_from_normalization (c)
  5. L35
    specialize prime_field_polynomial_horner_trace_from_normalization (t)
  6. L36
    specialize prime_field_polynomial_horner_trace_from_normalization (l)
  7. L37
    specialize prime_field_polynomial_horner_trace_from_normalization (x)
  8. L38
    specialize prime_field_polynomial_horner_trace_from_normalization (x1)
  9. L39
    specialize prime_field_polynomial_horner_trace_from_normalization (x2)
  10. L40
    specialize prime_field_polynomial_horner_trace_from_normalization (x3)
08Use earlier factsL41–47

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

  1. L41
    specialize prime_field_polynomial_horner_trace_from_normalization (x4)
  2. L42
    apply prime_field_polynomial_horner_trace_from_normalization
  3. L43
    exact hp
  4. L44
    exact hc
  5. L45
    exact ht
  6. L46
    exact hn_witness_witness_witness
  7. L47
    exact hr_witness_witness
09Separate the logical casesL48–49

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

  1. L48
    cases he
  2. L49
    cases he_witness
10Construct an explicit witnessL50–52

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

  1. L50
    exists x5
  2. L51
    exists x3
  3. L52
    exists x4
11Use earlier factsL53–53

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

  1. L53
    exact he_witness_left

Library-wide reading audit

Original exact command ledger · 53 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro hp
  7. 0007intro hc
  8. 0008intro ht
  9. 0009have hn : exists n. (exists ff_u_ph_pfh_exists_natural ff_v_ph_pfh_exists_natural. ((((exists fs_h_ph_pfh_exists_natural_body_start. fs_h_ph_pfh_exists_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_exists_natural)) /\ exists fs_q_ph_pfh_exists_natural_body_start. ff_u_ph_pfh_exists_natural = fs_q_ph_pfh_exists_natural_body_start * S ((S (0)) * ff_v_ph_pfh_exists_natural) + (0))) /\ ((((exists fs_h_ph_pfh_exists_natural_body_terminal. fs_h_ph_pfh_exists_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_exists_natural)) /\ exists fs_q_ph_pfh_exists_natural_body_terminal. ff_u_ph_pfh_exists_natural = fs_q_ph_pfh_exists_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_exists_natural) + (n))) /\ forall ff_i_ph_pfh_exists_natural_body_steps. (exists ph_bound_pfh_exists_natural_body_steps. ph_bound_pfh_exists_natural_body_steps + S ff_i_ph_pfh_exists_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_exists_natural_body_steps ff_previous_ph_pfh_exists_natural_body_steps ff_current_ph_pfh_exists_natural_body_steps. ((((exists fs_h_ph_pfh_exists_natural_body_steps_coefficient. fs_h_ph_pfh_exists_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_exists_natural_body_steps) = S ((S (ff_i_ph_pfh_exists_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_exists_natural_body_steps_coefficient. b = fs_q_ph_pfh_exists_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_exists_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_exists_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_exists_natural_body_steps_before. fs_h_ph_pfh_exists_natural_body_steps_before + S (ff_previous_ph_pfh_exists_natural_body_steps) = S ((S (ff_i_ph_pfh_exists_natural_body_steps)) * ff_v_ph_pfh_exists_natural)) /\ exists fs_q_ph_pfh_exists_natural_body_steps_before. ff_u_ph_pfh_exists_natural = fs_q_ph_pfh_exists_natural_body_steps_before * S ((S (ff_i_ph_pfh_exists_natural_body_steps)) * ff_v_ph_pfh_exists_natural) + (ff_previous_ph_pfh_exists_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_exists_natural_body_steps_after. fs_h_ph_pfh_exists_natural_body_steps_after + S (ff_current_ph_pfh_exists_natural_body_steps) = S ((S (S ff_i_ph_pfh_exists_natural_body_steps)) * ff_v_ph_pfh_exists_natural)) /\ exists fs_q_ph_pfh_exists_natural_body_steps_after. ff_u_ph_pfh_exists_natural = fs_q_ph_pfh_exists_natural_body_steps_after * S ((S (S ff_i_ph_pfh_exists_natural_body_steps)) * ff_v_ph_pfh_exists_natural) + (ff_current_ph_pfh_exists_natural_body_steps))) /\ ff_current_ph_pfh_exists_natural_body_steps = ff_previous_ph_pfh_exists_natural_body_steps * t + ff_coefficient_ph_pfh_exists_natural_body_steps))))))
  10. 0010specialize beta_horner_eval_exists (b)
  11. 0011specialize beta_horner_eval_exists (c)
  12. 0012specialize beta_horner_eval_exists (t)
  13. 0013specialize beta_horner_eval_exists (l)
  14. 0014apply beta_horner_eval_exists
  15. 0015cases hn
  16. 0016cases hn_witness
  17. 0017cases hn_witness_witness
  18. 0018have hr : exists U V. (forall pfp_index_exists_normalization. (exists pfa_gap_exists_normalizationindex. pfa_gap_exists_normalizationindex + S (pfp_index_exists_normalization) = (S l)) -> exists pfp_source_exists_normalization pfp_residue_exists_normalization. ((((exists ff_h_pfp_exists_normalizationsource. ff_h_pfp_exists_normalizationsource + S (pfp_source_exists_normalization) = S ((S (pfp_index_exists_normalization)) * x2)) /\ exists ff_q_pfp_exists_normalizationsource. x1 = ff_q_pfp_exists_normalizationsource * S ((S (pfp_index_exists_normalization)) * x2) + (pfp_source_exists_normalization))) /\ (((((exists ff_h_pfp_exists_normalizationtarget. ff_h_pfp_exists_normalizationtarget + S (pfp_residue_exists_normalization) = S ((S (pfp_index_exists_normalization)) * V)) /\ exists ff_q_pfp_exists_normalizationtarget. U = ff_q_pfp_exists_normalizationtarget * S ((S (pfp_index_exists_normalization)) * V) + (pfp_residue_exists_normalization))) /\ ((((exists pfa_gap_exists_normalizationresiduebound. pfa_gap_exists_normalizationresiduebound + S (pfp_residue_exists_normalization) = (p)) /\ ((exists pfa_offset_left_exists_normalizationresiduecongruence pfa_offset_right_exists_normalizationresiduecongruence. (pfp_source_exists_normalization) + (p) * pfa_offset_left_exists_normalizationresiduecongruence = (pfp_residue_exists_normalization) + (p) * pfa_offset_right_exists_normalizationresiduecongruence)))))))))
  19. 0019specialize prime_field_polynomial_normalization_exists (p)
  20. 0020specialize prime_field_polynomial_normalization_exists (x1)
  21. 0021specialize prime_field_polynomial_normalization_exists (x2)
  22. 0022specialize prime_field_polynomial_normalization_exists (S l)
  23. 0023apply prime_field_polynomial_normalization_exists
  24. 0024intro hz
  25. 0025specialize prime_nonzero (p)
  26. 0026apply prime_nonzero
  27. 0027exact hp
  28. 0028exact hz
  29. 0029cases hr
  30. 0030cases hr_witness
  31. 0031have he : exists r. ((((exists pfa_gap_exists_chosen_tracebase. pfa_gap_exists_chosen_tracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_exists_chosen_traceinitial. ff_h_pfp_exists_chosen_traceinitial + S (0) = S ((S (0)) * x4)) /\ exists ff_q_pfp_exists_chosen_traceinitial. x3 = ff_q_pfp_exists_chosen_traceinitial * S ((S (0)) * x4) + (0))) /\ (((((exists ff_h_pfp_exists_chosen_traceterminal. ff_h_pfp_exists_chosen_traceterminal + S (r) = S ((S (l)) * x4)) /\ exists ff_q_pfp_exists_chosen_traceterminal. x3 = ff_q_pfp_exists_chosen_traceterminal * S ((S (l)) * x4) + (r))) /\ ((forall pfh_index_exists_chosen_tracesteps. (exists pfa_gap_exists_chosen_tracestepsindex. pfa_gap_exists_chosen_tracestepsindex + S (pfh_index_exists_chosen_tracesteps) = (l)) -> (exists pfh_coefficient_exists_chosen_tracestepsstep pfh_before_exists_chosen_tracestepsstep pfh_after_exists_chosen_tracestepsstep pfh_product_exists_chosen_tracestepsstep. ((((exists ff_h_pfp_exists_chosen_tracestepsstepcoefficient. ff_h_pfp_exists_chosen_tracestepsstepcoefficient + S (pfh_coefficient_exists_chosen_tracestepsstep) = S ((S (pfh_index_exists_chosen_tracesteps)) * c)) /\ exists ff_q_pfp_exists_chosen_tracestepsstepcoefficient. b = ff_q_pfp_exists_chosen_tracestepsstepcoefficient * S ((S (pfh_index_exists_chosen_tracesteps)) * c) + (pfh_coefficient_exists_chosen_tracestepsstep))) /\ (((((exists ff_h_pfp_exists_chosen_tracestepsstepbefore. ff_h_pfp_exists_chosen_tracestepsstepbefore + S (pfh_before_exists_chosen_tracestepsstep) = S ((S (pfh_index_exists_chosen_tracesteps)) * x4)) /\ exists ff_q_pfp_exists_chosen_tracestepsstepbefore. x3 = ff_q_pfp_exists_chosen_tracestepsstepbefore * S ((S (pfh_index_exists_chosen_tracesteps)) * x4) + (pfh_before_exists_chosen_tracestepsstep))) /\ (((((exists ff_h_pfp_exists_chosen_tracestepsstepafter. ff_h_pfp_exists_chosen_tracestepsstepafter + S (pfh_after_exists_chosen_tracestepsstep) = S ((S (S (pfh_index_exists_chosen_tracesteps))) * x4)) /\ exists ff_q_pfp_exists_chosen_tracestepsstepafter. x3 = ff_q_pfp_exists_chosen_tracestepsstepafter * S ((S (S (pfh_index_exists_chosen_tracesteps))) * x4) + (pfh_after_exists_chosen_tracestepsstep))) /\ (((((exists pfa_gap_exists_chosen_tracestepsstepmultiplyleft. pfa_gap_exists_chosen_tracestepsstepmultiplyleft + S (pfh_before_exists_chosen_tracestepsstep) = (p)) /\ (((exists pfa_gap_exists_chosen_tracestepsstepmultiplyright. pfa_gap_exists_chosen_tracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_exists_chosen_tracestepsstepmultiplyresultbound. pfa_gap_exists_chosen_tracestepsstepmultiplyresultbound + S (pfh_product_exists_chosen_tracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_chosen_tracestepsstepmultiplyresultcongruence pfa_offset_right_exists_chosen_tracestepsstepmultiplyresultcongruence. ((pfh_before_exists_chosen_tracestepsstep) * (t)) + (p) * pfa_offset_left_exists_chosen_tracestepsstepmultiplyresultcongruence = (pfh_product_exists_chosen_tracestepsstep) + (p) * pfa_offset_right_exists_chosen_tracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_exists_chosen_tracestepsstepaddleft. pfa_gap_exists_chosen_tracestepsstepaddleft + S (pfh_product_exists_chosen_tracestepsstep) = (p)) /\ (((exists pfa_gap_exists_chosen_tracestepsstepaddright. pfa_gap_exists_chosen_tracestepsstepaddright + S (pfh_coefficient_exists_chosen_tracestepsstep) = (p)) /\ ((((exists pfa_gap_exists_chosen_tracestepsstepaddresultbound. pfa_gap_exists_chosen_tracestepsstepaddresultbound + S (pfh_after_exists_chosen_tracestepsstep) = (p)) /\ ((exists pfa_offset_left_exists_chosen_tracestepsstepaddresultcongruence pfa_offset_right_exists_chosen_tracestepsstepaddresultcongruence. ((pfh_product_exists_chosen_tracestepsstep) + (pfh_coefficient_exists_chosen_tracestepsstep)) + (p) * pfa_offset_left_exists_chosen_tracestepsstepaddresultcongruence = (pfh_after_exists_chosen_tracestepsstep) + (p) * pfa_offset_right_exists_chosen_tracestepsstepaddresultcongruence)))))))))))))))))))))))))) /\ ((((exists pfa_gap_exists_chosen_residuebound. pfa_gap_exists_chosen_residuebound + S (r) = (p)) /\ ((exists pfa_offset_left_exists_chosen_residuecongruence pfa_offset_right_exists_chosen_residuecongruence. (x) + (p) * pfa_offset_left_exists_chosen_residuecongruence = (r) + (p) * pfa_offset_right_exists_chosen_residuecongruence))))))
  32. 0032specialize prime_field_polynomial_horner_trace_from_normalization (p)
  33. 0033specialize prime_field_polynomial_horner_trace_from_normalization (b)
  34. 0034specialize prime_field_polynomial_horner_trace_from_normalization (c)
  35. 0035specialize prime_field_polynomial_horner_trace_from_normalization (t)
  36. 0036specialize prime_field_polynomial_horner_trace_from_normalization (l)
  37. 0037specialize prime_field_polynomial_horner_trace_from_normalization (x)
  38. 0038specialize prime_field_polynomial_horner_trace_from_normalization (x1)
  39. 0039specialize prime_field_polynomial_horner_trace_from_normalization (x2)
  40. 0040specialize prime_field_polynomial_horner_trace_from_normalization (x3)
  41. 0041specialize prime_field_polynomial_horner_trace_from_normalization (x4)
  42. 0042apply prime_field_polynomial_horner_trace_from_normalization
  43. 0043exact hp
  44. 0044exact hc
  45. 0045exact ht
  46. 0046exact hn_witness_witness_witness
  47. 0047exact hr_witness_witness
  48. 0048cases he
  49. 0049cases he_witness
  50. 0050exists x5
  51. 0051exists x3
  52. 0052exists x4
  53. 0053exact he_witness_left