PP0029

prime_field_polynomial_horner_functional

Every actual modular execution of the same coefficient prefix and base has the same canonical result.

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. ∀ r. ∀ s. Prime(p) → FpHorner(p,b,c,t,l,r) → FpHorner(p,b,c,t,l,s) → r = s

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

Definition DAG

Horner(b,c,x,ell,z) · 1FpHorner(p,b,c,x,l,r) · 2Prime(p) · 1

Actual proof prerequisites

beta_horner_eval_exists · checked external prerequisiteprime_field_polynomial_horner_residuebinary_canonical_residue_functional · checked external prerequisite
Original expanded first-order statement 
forall p b c t l r s. (~((p) = 1) /\ forall pfa_factor_left_functional_prime pfa_factor_right_functional_prime. (p) = pfa_factor_left_functional_prime * pfa_factor_right_functional_prime -> pfa_factor_left_functional_prime = 1 \/ pfa_factor_right_functional_prime = 1) -> (exists pfh_trace_code_functional_first pfh_trace_scale_functional_first. (((exists pfa_gap_functional_firsttracebase. pfa_gap_functional_firsttracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_functional_firsttraceinitial. ff_h_pfp_functional_firsttraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceinitial. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttraceinitial * S ((S (0)) * pfh_trace_scale_functional_first) + (0))) /\ (((((exists ff_h_pfp_functional_firsttraceterminal. ff_h_pfp_functional_firsttraceterminal + S (r) = S ((S (l)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttraceterminal. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttraceterminal * S ((S (l)) * pfh_trace_scale_functional_first) + (r))) /\ ((forall pfh_index_functional_firsttracesteps. (exists pfa_gap_functional_firsttracestepsindex. pfa_gap_functional_firsttracestepsindex + S (pfh_index_functional_firsttracesteps) = (l)) -> (exists pfh_coefficient_functional_firsttracestepsstep pfh_before_functional_firsttracestepsstep pfh_after_functional_firsttracestepsstep pfh_product_functional_firsttracestepsstep. ((((exists ff_h_pfp_functional_firsttracestepsstepcoefficient. ff_h_pfp_functional_firsttracestepsstepcoefficient + S (pfh_coefficient_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * c)) /\ exists ff_q_pfp_functional_firsttracestepsstepcoefficient. b = ff_q_pfp_functional_firsttracestepsstepcoefficient * S ((S (pfh_index_functional_firsttracesteps)) * c) + (pfh_coefficient_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepbefore. ff_h_pfp_functional_firsttracestepsstepbefore + S (pfh_before_functional_firsttracestepsstep) = S ((S (pfh_index_functional_firsttracesteps)) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepbefore. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttracestepsstepbefore * S ((S (pfh_index_functional_firsttracesteps)) * pfh_trace_scale_functional_first) + (pfh_before_functional_firsttracestepsstep))) /\ (((((exists ff_h_pfp_functional_firsttracestepsstepafter. ff_h_pfp_functional_firsttracestepsstepafter + S (pfh_after_functional_firsttracestepsstep) = S ((S (S (pfh_index_functional_firsttracesteps))) * pfh_trace_scale_functional_first)) /\ exists ff_q_pfp_functional_firsttracestepsstepafter. pfh_trace_code_functional_first = ff_q_pfp_functional_firsttracestepsstepafter * S ((S (S (pfh_index_functional_firsttracesteps))) * pfh_trace_scale_functional_first) + (pfh_after_functional_firsttracestepsstep))) /\ (((((exists pfa_gap_functional_firsttracestepsstepmultiplyleft. pfa_gap_functional_firsttracestepsstepmultiplyleft + S (pfh_before_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepmultiplyright. pfa_gap_functional_firsttracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepmultiplyresultbound. pfa_gap_functional_firsttracestepsstepmultiplyresultbound + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence. ((pfh_before_functional_firsttracestepsstep) * (t)) + (p) * pfa_offset_left_functional_firsttracestepsstepmultiplyresultcongruence = (pfh_product_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddleft. pfa_gap_functional_firsttracestepsstepaddleft + S (pfh_product_functional_firsttracestepsstep) = (p)) /\ (((exists pfa_gap_functional_firsttracestepsstepaddright. pfa_gap_functional_firsttracestepsstepaddright + S (pfh_coefficient_functional_firsttracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_firsttracestepsstepaddresultbound. pfa_gap_functional_firsttracestepsstepaddresultbound + S (pfh_after_functional_firsttracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_firsttracestepsstepaddresultcongruence pfa_offset_right_functional_firsttracestepsstepaddresultcongruence. ((pfh_product_functional_firsttracestepsstep) + (pfh_coefficient_functional_firsttracestepsstep)) + (p) * pfa_offset_left_functional_firsttracestepsstepaddresultcongruence = (pfh_after_functional_firsttracestepsstep) + (p) * pfa_offset_right_functional_firsttracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> (exists pfh_trace_code_functional_second pfh_trace_scale_functional_second. (((exists pfa_gap_functional_secondtracebase. pfa_gap_functional_secondtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_functional_secondtraceinitial. ff_h_pfp_functional_secondtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceinitial. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtraceinitial * S ((S (0)) * pfh_trace_scale_functional_second) + (0))) /\ (((((exists ff_h_pfp_functional_secondtraceterminal. ff_h_pfp_functional_secondtraceterminal + S (s) = S ((S (l)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtraceterminal. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtraceterminal * S ((S (l)) * pfh_trace_scale_functional_second) + (s))) /\ ((forall pfh_index_functional_secondtracesteps. (exists pfa_gap_functional_secondtracestepsindex. pfa_gap_functional_secondtracestepsindex + S (pfh_index_functional_secondtracesteps) = (l)) -> (exists pfh_coefficient_functional_secondtracestepsstep pfh_before_functional_secondtracestepsstep pfh_after_functional_secondtracestepsstep pfh_product_functional_secondtracestepsstep. ((((exists ff_h_pfp_functional_secondtracestepsstepcoefficient. ff_h_pfp_functional_secondtracestepsstepcoefficient + S (pfh_coefficient_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * c)) /\ exists ff_q_pfp_functional_secondtracestepsstepcoefficient. b = ff_q_pfp_functional_secondtracestepsstepcoefficient * S ((S (pfh_index_functional_secondtracesteps)) * c) + (pfh_coefficient_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepbefore. ff_h_pfp_functional_secondtracestepsstepbefore + S (pfh_before_functional_secondtracestepsstep) = S ((S (pfh_index_functional_secondtracesteps)) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepbefore. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtracestepsstepbefore * S ((S (pfh_index_functional_secondtracesteps)) * pfh_trace_scale_functional_second) + (pfh_before_functional_secondtracestepsstep))) /\ (((((exists ff_h_pfp_functional_secondtracestepsstepafter. ff_h_pfp_functional_secondtracestepsstepafter + S (pfh_after_functional_secondtracestepsstep) = S ((S (S (pfh_index_functional_secondtracesteps))) * pfh_trace_scale_functional_second)) /\ exists ff_q_pfp_functional_secondtracestepsstepafter. pfh_trace_code_functional_second = ff_q_pfp_functional_secondtracestepsstepafter * S ((S (S (pfh_index_functional_secondtracesteps))) * pfh_trace_scale_functional_second) + (pfh_after_functional_secondtracestepsstep))) /\ (((((exists pfa_gap_functional_secondtracestepsstepmultiplyleft. pfa_gap_functional_secondtracestepsstepmultiplyleft + S (pfh_before_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepmultiplyright. pfa_gap_functional_secondtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepmultiplyresultbound. pfa_gap_functional_secondtracestepsstepmultiplyresultbound + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence. ((pfh_before_functional_secondtracestepsstep) * (t)) + (p) * pfa_offset_left_functional_secondtracestepsstepmultiplyresultcongruence = (pfh_product_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddleft. pfa_gap_functional_secondtracestepsstepaddleft + S (pfh_product_functional_secondtracestepsstep) = (p)) /\ (((exists pfa_gap_functional_secondtracestepsstepaddright. pfa_gap_functional_secondtracestepsstepaddright + S (pfh_coefficient_functional_secondtracestepsstep) = (p)) /\ ((((exists pfa_gap_functional_secondtracestepsstepaddresultbound. pfa_gap_functional_secondtracestepsstepaddresultbound + S (pfh_after_functional_secondtracestepsstep) = (p)) /\ ((exists pfa_offset_left_functional_secondtracestepsstepaddresultcongruence pfa_offset_right_functional_secondtracestepsstepaddresultcongruence. ((pfh_product_functional_secondtracestepsstep) + (pfh_coefficient_functional_secondtracestepsstep)) + (p) * pfa_offset_left_functional_secondtracestepsstepaddresultcongruence = (pfh_after_functional_secondtracestepsstep) + (p) * pfa_offset_right_functional_secondtracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> r=s

Complete tactic proof in conservative notation

All 44 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

44 script commands · 6 reading checkpoints · 1 local claims

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

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 (1)
prime field polynomial horner residue
01Fix variables and assumptionsL1–10

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 r
  7. L7
    intro s
  8. L8
    intro hp
  9. L9
    intro hr
  10. L10
    intro hs
02Establish hnL11–16

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

  1. L11
    have hn : ∃ n. Horner(b,c,t,l,n)Definitions: Horner(b,c,t,l,n)Original native command in the exact edition
  2. L12
    specialize beta_horner_eval_exists (b)
  3. L13
    specialize beta_horner_eval_exists (c)
  4. L14
    specialize beta_horner_eval_exists (t)
  5. L15
    specialize beta_horner_eval_exists (l)
  6. L16
    apply beta_horner_eval_exists
03Separate the logical casesL17–17

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

  1. L17
    cases hn
04Use earlier factsL18–27

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

  1. L18
    specialize binary_canonical_residue_functional (p)
  2. L19
    specialize binary_canonical_residue_functional (x)
  3. L20
    specialize binary_canonical_residue_functional (r)
  4. L21
    specialize binary_canonical_residue_functional (s)
  5. L22
    apply binary_canonical_residue_functional
  6. L23
    specialize prime_field_polynomial_horner_residue (p)
  7. L24
    specialize prime_field_polynomial_horner_residue (b)
  8. L25
    specialize prime_field_polynomial_horner_residue (c)
  9. L26
    specialize prime_field_polynomial_horner_residue (t)
  10. L27
    specialize prime_field_polynomial_horner_residue (l)
05Use earlier factsL28–37

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

  1. L28
    specialize prime_field_polynomial_horner_residue (x)
  2. L29
    specialize prime_field_polynomial_horner_residue (r)
  3. L30
    apply prime_field_polynomial_horner_residue
  4. L31
    exact hp
  5. L32
    exact hn_witness
  6. L33
    exact hr
  7. L34
    specialize prime_field_polynomial_horner_residue (p)
  8. L35
    specialize prime_field_polynomial_horner_residue (b)
  9. L36
    specialize prime_field_polynomial_horner_residue (c)
  10. L37
    specialize prime_field_polynomial_horner_residue (t)
06Use earlier factsL38–44

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

  1. L38
    specialize prime_field_polynomial_horner_residue (l)
  2. L39
    specialize prime_field_polynomial_horner_residue (x)
  3. L40
    specialize prime_field_polynomial_horner_residue (s)
  4. L41
    apply prime_field_polynomial_horner_residue
  5. L42
    exact hp
  6. L43
    exact hn_witness
  7. L44
    exact hs

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006intro r
  7. 0007intro s
  8. 0008intro hp
  9. 0009intro hr
  10. 0010intro hs
  11. 0011have hn : ∃ n. Horner(b,c,t,l,n)
  12. 0012specialize beta_horner_eval_exists (b)
  13. 0013specialize beta_horner_eval_exists (c)
  14. 0014specialize beta_horner_eval_exists (t)
  15. 0015specialize beta_horner_eval_exists (l)
  16. 0016apply beta_horner_eval_exists
  17. 0017cases hn
  18. 0018specialize binary_canonical_residue_functional (p)
  19. 0019specialize binary_canonical_residue_functional (x)
  20. 0020specialize binary_canonical_residue_functional (r)
  21. 0021specialize binary_canonical_residue_functional (s)
  22. 0022apply binary_canonical_residue_functional
  23. 0023specialize prime_field_polynomial_horner_residue (p)
  24. 0024specialize prime_field_polynomial_horner_residue (b)
  25. 0025specialize prime_field_polynomial_horner_residue (c)
  26. 0026specialize prime_field_polynomial_horner_residue (t)
  27. 0027specialize prime_field_polynomial_horner_residue (l)
  28. 0028specialize prime_field_polynomial_horner_residue (x)
  29. 0029specialize prime_field_polynomial_horner_residue (r)
  30. 0030apply prime_field_polynomial_horner_residue
  31. 0031exact hp
  32. 0032exact hn_witness
  33. 0033exact hr
  34. 0034specialize prime_field_polynomial_horner_residue (p)
  35. 0035specialize prime_field_polynomial_horner_residue (b)
  36. 0036specialize prime_field_polynomial_horner_residue (c)
  37. 0037specialize prime_field_polynomial_horner_residue (t)
  38. 0038specialize prime_field_polynomial_horner_residue (l)
  39. 0039specialize prime_field_polynomial_horner_residue (x)
  40. 0040specialize prime_field_polynomial_horner_residue (s)
  41. 0041apply prime_field_polynomial_horner_residue
  42. 0042exact hp
  43. 0043exact hn_witness
  44. 0044exact hs