PP0031

prime_field_polynomial_reduce_and_evaluate_exists

For arbitrary finite natural coefficients construct their canonical prime-field table and an actual Horner execution, and prove agreement with every natural T12 evaluation.

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

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

Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ t. ∀ l. Prime(p) → Lt(t,p) → ∃ x. ∃ y. ∃ z. FpCoefficientReduction(p,b,c,x,y,l) ∧ (FpHorner(p,x,y,t,l,z) ∧ (∀ n. Horner(b,c,t,l,n) → CanonicalModularResidue(p,n,z)))

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

Definition DAG

Horner(b,c,x,ell,z) · 1CanonicalModularResidue(m,a,r) · 1FpCoefficientReduction(p,b,c,d,e,l) · 2FpHorner(p,b,c,x,l,r) · 2Lt(a,b) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_normalization_existsprime_nonzero · checked external prerequisiteprime_field_polynomial_horner_existsprime_field_polynomial_normalization_boundedprime_field_polynomial_horner_normalization_residue
Original expanded first-order statement 
forall p b c t l. (~((p) = 1) /\ forall pfa_factor_left_complete_prime pfa_factor_right_complete_prime. (p) = pfa_factor_left_complete_prime * pfa_factor_right_complete_prime -> pfa_factor_left_complete_prime = 1 \/ pfa_factor_right_complete_prime = 1) -> (exists pfa_gap_complete_base. pfa_gap_complete_base + S (t) = (p)) -> exists d e r. ((forall pfp_index_complete_reduction_result. (exists pfa_gap_complete_reduction_resultindex. pfa_gap_complete_reduction_resultindex + S (pfp_index_complete_reduction_result) = (l)) -> exists pfp_source_complete_reduction_result pfp_residue_complete_reduction_result. ((((exists ff_h_pfp_complete_reduction_resultsource. ff_h_pfp_complete_reduction_resultsource + S (pfp_source_complete_reduction_result) = S ((S (pfp_index_complete_reduction_result)) * c)) /\ exists ff_q_pfp_complete_reduction_resultsource. b = ff_q_pfp_complete_reduction_resultsource * S ((S (pfp_index_complete_reduction_result)) * c) + (pfp_source_complete_reduction_result))) /\ (((((exists ff_h_pfp_complete_reduction_resulttarget. ff_h_pfp_complete_reduction_resulttarget + S (pfp_residue_complete_reduction_result) = S ((S (pfp_index_complete_reduction_result)) * e)) /\ exists ff_q_pfp_complete_reduction_resulttarget. d = ff_q_pfp_complete_reduction_resulttarget * S ((S (pfp_index_complete_reduction_result)) * e) + (pfp_residue_complete_reduction_result))) /\ ((((exists pfa_gap_complete_reduction_resultresiduebound. pfa_gap_complete_reduction_resultresiduebound + S (pfp_residue_complete_reduction_result) = (p)) /\ ((exists pfa_offset_left_complete_reduction_resultresiduecongruence pfa_offset_right_complete_reduction_resultresiduecongruence. (pfp_source_complete_reduction_result) + (p) * pfa_offset_left_complete_reduction_resultresiduecongruence = (pfp_residue_complete_reduction_result) + (p) * pfa_offset_right_complete_reduction_resultresiduecongruence))))))))) /\ (((exists pfh_trace_code_complete_execution_result pfh_trace_scale_complete_execution_result. (((exists pfa_gap_complete_execution_resulttracebase. pfa_gap_complete_execution_resulttracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_complete_execution_resulttraceinitial. ff_h_pfp_complete_execution_resulttraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttraceinitial. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttraceinitial * S ((S (0)) * pfh_trace_scale_complete_execution_result) + (0))) /\ (((((exists ff_h_pfp_complete_execution_resulttraceterminal. ff_h_pfp_complete_execution_resulttraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttraceterminal. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttraceterminal * S ((S (l)) * pfh_trace_scale_complete_execution_result) + (r))) /\ ((forall pfh_index_complete_execution_resulttracesteps. (exists pfa_gap_complete_execution_resulttracestepsindex. pfa_gap_complete_execution_resulttracestepsindex + S (pfh_index_complete_execution_resulttracesteps) = (l)) -> (exists pfh_coefficient_complete_execution_resulttracestepsstep pfh_before_complete_execution_resulttracestepsstep pfh_after_complete_execution_resulttracestepsstep pfh_product_complete_execution_resulttracestepsstep. ((((exists ff_h_pfp_complete_execution_resulttracestepsstepcoefficient. ff_h_pfp_complete_execution_resulttracestepsstepcoefficient + S (pfh_coefficient_complete_execution_resulttracestepsstep) = S ((S (pfh_index_complete_execution_resulttracesteps)) * e)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepcoefficient. d = ff_q_pfp_complete_execution_resulttracestepsstepcoefficient * S ((S (pfh_index_complete_execution_resulttracesteps)) * e) + (pfh_coefficient_complete_execution_resulttracestepsstep))) /\ (((((exists ff_h_pfp_complete_execution_resulttracestepsstepbefore. ff_h_pfp_complete_execution_resulttracestepsstepbefore + S (pfh_before_complete_execution_resulttracestepsstep) = S ((S (pfh_index_complete_execution_resulttracesteps)) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepbefore. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttracestepsstepbefore * S ((S (pfh_index_complete_execution_resulttracesteps)) * pfh_trace_scale_complete_execution_result) + (pfh_before_complete_execution_resulttracestepsstep))) /\ (((((exists ff_h_pfp_complete_execution_resulttracestepsstepafter. ff_h_pfp_complete_execution_resulttracestepsstepafter + S (pfh_after_complete_execution_resulttracestepsstep) = S ((S (S (pfh_index_complete_execution_resulttracesteps))) * pfh_trace_scale_complete_execution_result)) /\ exists ff_q_pfp_complete_execution_resulttracestepsstepafter. pfh_trace_code_complete_execution_result = ff_q_pfp_complete_execution_resulttracestepsstepafter * S ((S (S (pfh_index_complete_execution_resulttracesteps))) * pfh_trace_scale_complete_execution_result) + (pfh_after_complete_execution_resulttracestepsstep))) /\ (((((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyleft. pfa_gap_complete_execution_resulttracestepsstepmultiplyleft + S (pfh_before_complete_execution_resulttracestepsstep) = (p)) /\ (((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyright. pfa_gap_complete_execution_resulttracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepmultiplyresultbound. pfa_gap_complete_execution_resulttracestepsstepmultiplyresultbound + S (pfh_product_complete_execution_resulttracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_execution_resulttracestepsstepmultiplyresultcongruence pfa_offset_right_complete_execution_resulttracestepsstepmultiplyresultcongruence. ((pfh_before_complete_execution_resulttracestepsstep) * (t)) + (p) * pfa_offset_left_complete_execution_resulttracestepsstepmultiplyresultcongruence = (pfh_product_complete_execution_resulttracestepsstep) + (p) * pfa_offset_right_complete_execution_resulttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepaddleft. pfa_gap_complete_execution_resulttracestepsstepaddleft + S (pfh_product_complete_execution_resulttracestepsstep) = (p)) /\ (((exists pfa_gap_complete_execution_resulttracestepsstepaddright. pfa_gap_complete_execution_resulttracestepsstepaddright + S (pfh_coefficient_complete_execution_resulttracestepsstep) = (p)) /\ ((((exists pfa_gap_complete_execution_resulttracestepsstepaddresultbound. pfa_gap_complete_execution_resulttracestepsstepaddresultbound + S (pfh_after_complete_execution_resulttracestepsstep) = (p)) /\ ((exists pfa_offset_left_complete_execution_resulttracestepsstepaddresultcongruence pfa_offset_right_complete_execution_resulttracestepsstepaddresultcongruence. ((pfh_product_complete_execution_resulttracestepsstep) + (pfh_coefficient_complete_execution_resulttracestepsstep)) + (p) * pfa_offset_left_complete_execution_resulttracestepsstepaddresultcongruence = (pfh_after_complete_execution_resulttracestepsstep) + (p) * pfa_offset_right_complete_execution_resulttracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ ((forall n. (exists ff_u_ph_pfh_complete_natural ff_v_ph_pfh_complete_natural. ((((exists fs_h_ph_pfh_complete_natural_body_start. fs_h_ph_pfh_complete_natural_body_start + S (0) = S ((S (0)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_start. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_start * S ((S (0)) * ff_v_ph_pfh_complete_natural) + (0))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_terminal. fs_h_ph_pfh_complete_natural_body_terminal + S (n) = S ((S (l)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_terminal. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_terminal * S ((S (l)) * ff_v_ph_pfh_complete_natural) + (n))) /\ forall ff_i_ph_pfh_complete_natural_body_steps. (exists ph_bound_pfh_complete_natural_body_steps. ph_bound_pfh_complete_natural_body_steps + S ff_i_ph_pfh_complete_natural_body_steps = l) -> exists ff_coefficient_ph_pfh_complete_natural_body_steps ff_previous_ph_pfh_complete_natural_body_steps ff_current_ph_pfh_complete_natural_body_steps. ((((exists fs_h_ph_pfh_complete_natural_body_steps_coefficient. fs_h_ph_pfh_complete_natural_body_steps_coefficient + S (ff_coefficient_ph_pfh_complete_natural_body_steps) = S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * c)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_coefficient. b = fs_q_ph_pfh_complete_natural_body_steps_coefficient * S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * c) + (ff_coefficient_ph_pfh_complete_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_steps_before. fs_h_ph_pfh_complete_natural_body_steps_before + S (ff_previous_ph_pfh_complete_natural_body_steps) = S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_before. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_steps_before * S ((S (ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural) + (ff_previous_ph_pfh_complete_natural_body_steps))) /\ ((((exists fs_h_ph_pfh_complete_natural_body_steps_after. fs_h_ph_pfh_complete_natural_body_steps_after + S (ff_current_ph_pfh_complete_natural_body_steps) = S ((S (S ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural)) /\ exists fs_q_ph_pfh_complete_natural_body_steps_after. ff_u_ph_pfh_complete_natural = fs_q_ph_pfh_complete_natural_body_steps_after * S ((S (S ff_i_ph_pfh_complete_natural_body_steps)) * ff_v_ph_pfh_complete_natural) + (ff_current_ph_pfh_complete_natural_body_steps))) /\ ff_current_ph_pfh_complete_natural_body_steps = ff_previous_ph_pfh_complete_natural_body_steps * t + ff_coefficient_ph_pfh_complete_natural_body_steps)))))) -> (((exists pfa_gap_complete_residuebound. pfa_gap_complete_residuebound + S (r) = (p)) /\ ((exists pfa_offset_left_complete_residuecongruence pfa_offset_right_complete_residuecongruence. (n) + (p) * pfa_offset_left_complete_residuecongruence = (r) + (p) * pfa_offset_right_complete_residuecongruence)))))))))

Complete tactic proof in conservative notation

All 61 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

61 script commands · 15 reading checkpoints · 2 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
prime field polynomial normalization existsprime field polynomial horner existsprime field polynomial normalization boundedprime field polynomial horner normalization residue
01Fix variables and assumptionsL1–7

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 ht
02Establish hredL8–17

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

  1. L8
    have hred : ∃ d. ∃ e. FpCoefficientReduction(p,b,c,d,e,l)Definitions: FpCoefficientReduction(p,b,c,d,e,l)Original native command in the exact edition
  2. L9
    specialize prime_field_polynomial_normalization_exists (p)
  3. L10
    specialize prime_field_polynomial_normalization_exists (b)
  4. L11
    specialize prime_field_polynomial_normalization_exists (c)
  5. L12
    specialize prime_field_polynomial_normalization_exists (l)
  6. L13
    apply prime_field_polynomial_normalization_exists
  7. L14
    intro hz
  8. L15
    specialize prime_nonzero (p)
  9. L16
    apply prime_nonzero
  10. L17
    exact hp
03Use earlier factsL18–18

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

  1. L18
    exact hz
04Separate the logical casesL19–20

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

  1. L19
    cases hred
  2. L20
    cases hred_witness
05Establish heL21–30

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

  1. L21
    have he : ∃ r. FpHorner(p,x,x1,t,l,r)Definitions: FpHorner(p,x,x1,t,l,r)Original native command in the exact edition
  2. L22
    specialize prime_field_polynomial_horner_exists (p)
  3. L23
    specialize prime_field_polynomial_horner_exists (x)
  4. L24
    specialize prime_field_polynomial_horner_exists (x1)
  5. L25
    specialize prime_field_polynomial_horner_exists (t)
  6. L26
    specialize prime_field_polynomial_horner_exists (l)
  7. L27
    apply prime_field_polynomial_horner_exists
  8. L28
    exact hp
  9. L29
    specialize prime_field_polynomial_normalization_bounded (p)
  10. L30
    specialize prime_field_polynomial_normalization_bounded (b)
06Use earlier factsL31–37

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

  1. L31
    specialize prime_field_polynomial_normalization_bounded (c)
  2. L32
    specialize prime_field_polynomial_normalization_bounded (x)
  3. L33
    specialize prime_field_polynomial_normalization_bounded (x1)
  4. L34
    specialize prime_field_polynomial_normalization_bounded (l)
  5. L35
    apply prime_field_polynomial_normalization_bounded
  6. L36
    exact hred_witness_witness
  7. L37
    exact ht
07Separate the logical casesL38–38

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

  1. L38
    cases he
08Construct an explicit witnessL39–41

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

  1. L39
    exists x
  2. L40
    exists x1
  3. L41
    exists x2
09Separate the logical casesL42–42

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

  1. L42
    split
10Use earlier factsL43–43

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

  1. L43
    exact hred_witness_witness
11Separate the logical casesL44–44

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

  1. L44
    split
12Use earlier factsL45–45

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

  1. L45
    exact he_witness
13Fix variables and assumptionsL46–47

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

  1. L46
    intro n
  2. L47
    intro hn
14Use earlier factsL48–57

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

  1. L48
    specialize prime_field_polynomial_horner_normalization_residue (p)
  2. L49
    specialize prime_field_polynomial_horner_normalization_residue (b)
  3. L50
    specialize prime_field_polynomial_horner_normalization_residue (c)
  4. L51
    specialize prime_field_polynomial_horner_normalization_residue (x)
  5. L52
    specialize prime_field_polynomial_horner_normalization_residue (x1)
  6. L53
    specialize prime_field_polynomial_horner_normalization_residue (t)
  7. L54
    specialize prime_field_polynomial_horner_normalization_residue (l)
  8. L55
    specialize prime_field_polynomial_horner_normalization_residue (n)
  9. L56
    specialize prime_field_polynomial_horner_normalization_residue (x2)
  10. L57
    apply prime_field_polynomial_horner_normalization_residue
15Use earlier factsL58–61

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

  1. L58
    exact hp
  2. L59
    exact hred_witness_witness
  3. L60
    exact hn
  4. L61
    exact he_witness

Library-wide reading audit

Original defined command ledger · 61 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro hp
  7. 0007intro ht
  8. 0008have hred : ∃ d. ∃ e. FpCoefficientReduction(p,b,c,d,e,l)
  9. 0009specialize prime_field_polynomial_normalization_exists (p)
  10. 0010specialize prime_field_polynomial_normalization_exists (b)
  11. 0011specialize prime_field_polynomial_normalization_exists (c)
  12. 0012specialize prime_field_polynomial_normalization_exists (l)
  13. 0013apply prime_field_polynomial_normalization_exists
  14. 0014intro hz
  15. 0015specialize prime_nonzero (p)
  16. 0016apply prime_nonzero
  17. 0017exact hp
  18. 0018exact hz
  19. 0019cases hred
  20. 0020cases hred_witness
  21. 0021have he : ∃ r. FpHorner(p,x,x1,t,l,r)
  22. 0022specialize prime_field_polynomial_horner_exists (p)
  23. 0023specialize prime_field_polynomial_horner_exists (x)
  24. 0024specialize prime_field_polynomial_horner_exists (x1)
  25. 0025specialize prime_field_polynomial_horner_exists (t)
  26. 0026specialize prime_field_polynomial_horner_exists (l)
  27. 0027apply prime_field_polynomial_horner_exists
  28. 0028exact hp
  29. 0029specialize prime_field_polynomial_normalization_bounded (p)
  30. 0030specialize prime_field_polynomial_normalization_bounded (b)
  31. 0031specialize prime_field_polynomial_normalization_bounded (c)
  32. 0032specialize prime_field_polynomial_normalization_bounded (x)
  33. 0033specialize prime_field_polynomial_normalization_bounded (x1)
  34. 0034specialize prime_field_polynomial_normalization_bounded (l)
  35. 0035apply prime_field_polynomial_normalization_bounded
  36. 0036exact hred_witness_witness
  37. 0037exact ht
  38. 0038cases he
  39. 0039exists x
  40. 0040exists x1
  41. 0041exists x2
  42. 0042split
  43. 0043exact hred_witness_witness
  44. 0044split
  45. 0045exact he_witness
  46. 0046intro n
  47. 0047intro hn
  48. 0048specialize prime_field_polynomial_horner_normalization_residue (p)
  49. 0049specialize prime_field_polynomial_horner_normalization_residue (b)
  50. 0050specialize prime_field_polynomial_horner_normalization_residue (c)
  51. 0051specialize prime_field_polynomial_horner_normalization_residue (x)
  52. 0052specialize prime_field_polynomial_horner_normalization_residue (x1)
  53. 0053specialize prime_field_polynomial_horner_normalization_residue (t)
  54. 0054specialize prime_field_polynomial_horner_normalization_residue (l)
  55. 0055specialize prime_field_polynomial_horner_normalization_residue (n)
  56. 0056specialize prime_field_polynomial_horner_normalization_residue (x2)
  57. 0057apply prime_field_polynomial_horner_normalization_residue
  58. 0058exact hp
  59. 0059exact hred_witness_witness
  60. 0060exact hn
  61. 0061exact he_witness