PP002E

prime_field_polynomial_horner_zero

Every actually encoded all-zero coefficient prefix has a genuine zero-result modular execution, including length zero.

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) → Repeat(b,c,0,l) → FpHorner(p,b,c,t,l,0)

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

Definition DAG

FpHorner(p,b,c,x,l,r) · 1Lt(a,b) · 1Prime(p) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_field_polynomial_horner_empty_constructprime_field_polynomial_horner_successor_constructzero_add · checked external prerequisitele_succ · checked external prerequisiteprime_field_multiply_zero_left · checked external prerequisiteprime_field_add_zero_left · checked external prerequisiteprime_field_zero_below_prime · checked external prerequisite
Original expanded first-order statement 
forall p b c t l. (~((p) = 1) /\ forall pfa_factor_left_zero_prime pfa_factor_right_zero_prime. (p) = pfa_factor_left_zero_prime * pfa_factor_right_zero_prime -> pfa_factor_left_zero_prime = 1 \/ pfa_factor_right_zero_prime = 1) -> (exists pfa_gap_zero_base. pfa_gap_zero_base + S (t) = (p)) -> (forall pfp_repeat_index_zero_coefficients. (exists pfa_gap_zero_coefficientsindex. pfa_gap_zero_coefficientsindex + S (pfp_repeat_index_zero_coefficients) = (l)) -> (((exists ff_h_pfp_zero_coefficientsentry. ff_h_pfp_zero_coefficientsentry + S (0) = S ((S (pfp_repeat_index_zero_coefficients)) * c)) /\ exists ff_q_pfp_zero_coefficientsentry. b = ff_q_pfp_zero_coefficientsentry * S ((S (pfp_repeat_index_zero_coefficients)) * c) + (0)))) -> (exists pfh_trace_code_zero_execution pfh_trace_scale_zero_execution. (((exists pfa_gap_zero_executiontracebase. pfa_gap_zero_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_zero_executiontraceinitial. ff_h_pfp_zero_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_zero_execution)) /\ exists ff_q_pfp_zero_executiontraceinitial. pfh_trace_code_zero_execution = ff_q_pfp_zero_executiontraceinitial * S ((S (0)) * pfh_trace_scale_zero_execution) + (0))) /\ (((((exists ff_h_pfp_zero_executiontraceterminal. ff_h_pfp_zero_executiontraceterminal + S (0) = S ((S (l)) * pfh_trace_scale_zero_execution)) /\ exists ff_q_pfp_zero_executiontraceterminal. pfh_trace_code_zero_execution = ff_q_pfp_zero_executiontraceterminal * S ((S (l)) * pfh_trace_scale_zero_execution) + (0))) /\ ((forall pfh_index_zero_executiontracesteps. (exists pfa_gap_zero_executiontracestepsindex. pfa_gap_zero_executiontracestepsindex + S (pfh_index_zero_executiontracesteps) = (l)) -> (exists pfh_coefficient_zero_executiontracestepsstep pfh_before_zero_executiontracestepsstep pfh_after_zero_executiontracestepsstep pfh_product_zero_executiontracestepsstep. ((((exists ff_h_pfp_zero_executiontracestepsstepcoefficient. ff_h_pfp_zero_executiontracestepsstepcoefficient + S (pfh_coefficient_zero_executiontracestepsstep) = S ((S (pfh_index_zero_executiontracesteps)) * c)) /\ exists ff_q_pfp_zero_executiontracestepsstepcoefficient. b = ff_q_pfp_zero_executiontracestepsstepcoefficient * S ((S (pfh_index_zero_executiontracesteps)) * c) + (pfh_coefficient_zero_executiontracestepsstep))) /\ (((((exists ff_h_pfp_zero_executiontracestepsstepbefore. ff_h_pfp_zero_executiontracestepsstepbefore + S (pfh_before_zero_executiontracestepsstep) = S ((S (pfh_index_zero_executiontracesteps)) * pfh_trace_scale_zero_execution)) /\ exists ff_q_pfp_zero_executiontracestepsstepbefore. pfh_trace_code_zero_execution = ff_q_pfp_zero_executiontracestepsstepbefore * S ((S (pfh_index_zero_executiontracesteps)) * pfh_trace_scale_zero_execution) + (pfh_before_zero_executiontracestepsstep))) /\ (((((exists ff_h_pfp_zero_executiontracestepsstepafter. ff_h_pfp_zero_executiontracestepsstepafter + S (pfh_after_zero_executiontracestepsstep) = S ((S (S (pfh_index_zero_executiontracesteps))) * pfh_trace_scale_zero_execution)) /\ exists ff_q_pfp_zero_executiontracestepsstepafter. pfh_trace_code_zero_execution = ff_q_pfp_zero_executiontracestepsstepafter * S ((S (S (pfh_index_zero_executiontracesteps))) * pfh_trace_scale_zero_execution) + (pfh_after_zero_executiontracestepsstep))) /\ (((((exists pfa_gap_zero_executiontracestepsstepmultiplyleft. pfa_gap_zero_executiontracestepsstepmultiplyleft + S (pfh_before_zero_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_zero_executiontracestepsstepmultiplyright. pfa_gap_zero_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_zero_executiontracestepsstepmultiplyresultbound. pfa_gap_zero_executiontracestepsstepmultiplyresultbound + S (pfh_product_zero_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_zero_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_zero_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_zero_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_zero_executiontracestepsstepmultiplyresultcongruence = (pfh_product_zero_executiontracestepsstep) + (p) * pfa_offset_right_zero_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_zero_executiontracestepsstepaddleft. pfa_gap_zero_executiontracestepsstepaddleft + S (pfh_product_zero_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_zero_executiontracestepsstepaddright. pfa_gap_zero_executiontracestepsstepaddright + S (pfh_coefficient_zero_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_zero_executiontracestepsstepaddresultbound. pfa_gap_zero_executiontracestepsstepaddresultbound + S (pfh_after_zero_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_zero_executiontracestepsstepaddresultcongruence pfa_offset_right_zero_executiontracestepsstepaddresultcongruence. ((pfh_product_zero_executiontracestepsstep) + (pfh_coefficient_zero_executiontracestepsstep)) + (p) * pfa_offset_left_zero_executiontracestepsstepaddresultcongruence = (pfh_after_zero_executiontracestepsstep) + (p) * pfa_offset_right_zero_executiontracestepsstepaddresultcongruence)))))))))))))))))))))))))))

Complete tactic proof in conservative notation

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

57 script commands · 11 reading checkpoints · 0 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 (2)
prime field polynomial horner empty constructprime field polynomial horner successor construct
01Fix variables and assumptionsL1–5

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
02Induction on lL6–15

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L6
    induction l
  2. L7
    intro hp
  3. L8
    intro ht
  4. L9
    intro hz
  5. L10
    specialize prime_field_polynomial_horner_empty_construct (p)
  6. L11
    specialize prime_field_polynomial_horner_empty_construct (b)
  7. L12
    specialize prime_field_polynomial_horner_empty_construct (c)
  8. L13
    specialize prime_field_polynomial_horner_empty_construct (t)
  9. L14
    apply prime_field_polynomial_horner_empty_construct
  10. L15
    exact hp
03Use earlier factsL16–16

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

  1. L16
    exact ht
04Fix variables and assumptionsL17–19

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

  1. L17
    intro hp
  2. L18
    intro ht
  3. L19
    intro hz
05Use earlier factsL20–29

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

  1. L20
    specialize prime_field_polynomial_horner_successor_construct (p)
  2. L21
    specialize prime_field_polynomial_horner_successor_construct (b)
  3. L22
    specialize prime_field_polynomial_horner_successor_construct (c)
  4. L23
    specialize prime_field_polynomial_horner_successor_construct (t)
  5. L24
    specialize prime_field_polynomial_horner_successor_construct (l)
  6. L25
    specialize prime_field_polynomial_horner_successor_construct (0)
  7. L26
    specialize prime_field_polynomial_horner_successor_construct (0)
  8. L27
    specialize prime_field_polynomial_horner_successor_construct (0)
  9. L28
    specialize prime_field_polynomial_horner_successor_construct (0)
  10. L29
    apply prime_field_polynomial_horner_successor_construct
06Use earlier factsL30–32

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

  1. L30
    exact hp
  2. L31
    specialize hz (l)
  3. L32
    apply hz
07Construct an explicit witnessL33–33

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

  1. L33
    exists 0
08Use earlier factsL34–37

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

  1. L34
    apply zero_add
  2. L35
    apply IH
  3. L36
    exact hp
  4. L37
    exact ht
09Fix variables and assumptionsL38–39

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

  1. L38
    intro i
  2. L39
    intro hi
10Use earlier factsL40–49

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

  1. L40
    specialize hz (i)
  2. L41
    apply hz
  3. L42
    specialize le_succ (S i)
  4. L43
    specialize le_succ (l)
  5. L44
    apply le_succ
  6. L45
    exact hi
  7. L46
    specialize prime_field_multiply_zero_left (p)
  8. L47
    specialize prime_field_multiply_zero_left (t)
  9. L48
    apply prime_field_multiply_zero_left
  10. L49
    exact hp
11Use earlier factsL50–57

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

  1. L50
    exact ht
  2. L51
    specialize prime_field_add_zero_left (p)
  3. L52
    specialize prime_field_add_zero_left (0)
  4. L53
    apply prime_field_add_zero_left
  5. L54
    exact hp
  6. L55
    specialize prime_field_zero_below_prime (p)
  7. L56
    apply prime_field_zero_below_prime
  8. L57
    exact hp

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro l
  6. 0006induction l
  7. 0007intro hp
  8. 0008intro ht
  9. 0009intro hz
  10. 0010specialize prime_field_polynomial_horner_empty_construct (p)
  11. 0011specialize prime_field_polynomial_horner_empty_construct (b)
  12. 0012specialize prime_field_polynomial_horner_empty_construct (c)
  13. 0013specialize prime_field_polynomial_horner_empty_construct (t)
  14. 0014apply prime_field_polynomial_horner_empty_construct
  15. 0015exact hp
  16. 0016exact ht
  17. 0017intro hp
  18. 0018intro ht
  19. 0019intro hz
  20. 0020specialize prime_field_polynomial_horner_successor_construct (p)
  21. 0021specialize prime_field_polynomial_horner_successor_construct (b)
  22. 0022specialize prime_field_polynomial_horner_successor_construct (c)
  23. 0023specialize prime_field_polynomial_horner_successor_construct (t)
  24. 0024specialize prime_field_polynomial_horner_successor_construct (l)
  25. 0025specialize prime_field_polynomial_horner_successor_construct (0)
  26. 0026specialize prime_field_polynomial_horner_successor_construct (0)
  27. 0027specialize prime_field_polynomial_horner_successor_construct (0)
  28. 0028specialize prime_field_polynomial_horner_successor_construct (0)
  29. 0029apply prime_field_polynomial_horner_successor_construct
  30. 0030exact hp
  31. 0031specialize hz (l)
  32. 0032apply hz
  33. 0033exists 0
  34. 0034apply zero_add
  35. 0035apply IH
  36. 0036exact hp
  37. 0037exact ht
  38. 0038intro i
  39. 0039intro hi
  40. 0040specialize hz (i)
  41. 0041apply hz
  42. 0042specialize le_succ (S i)
  43. 0043specialize le_succ (l)
  44. 0044apply le_succ
  45. 0045exact hi
  46. 0046specialize prime_field_multiply_zero_left (p)
  47. 0047specialize prime_field_multiply_zero_left (t)
  48. 0048apply prime_field_multiply_zero_left
  49. 0049exact hp
  50. 0050exact ht
  51. 0051specialize prime_field_add_zero_left (p)
  52. 0052specialize prime_field_add_zero_left (0)
  53. 0053apply prime_field_add_zero_left
  54. 0054exact hp
  55. 0055specialize prime_field_zero_below_prime (p)
  56. 0056apply prime_field_zero_below_prime
  57. 0057exact hp