PP0025

prime_field_polynomial_horner_successor_decompose

An actual successor execution decomposes into its actual prefix and final multiply-then-add step in highest-degree-first order.

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. FpHorner(p,b,c,t,S l,r) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,l,x) ∧ (FpHorner(p,b,c,t,l,y) ∧ (FpMul(p,y,t,z) ∧ FpAdd(p,z,x,r)))

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

Definition DAG

FpAdd(p,a,b,c) · 1FpMul(p,a,b,c) · 1FpHornerStep(p,b,c,x,u,v,i) · 1FpHorner(p,b,c,x,l,r) · 2BetaAt(b,c,i,x) · 1

Actual proof prerequisites

zero_add · checked external prerequisitebeta_at_unique · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall p b c t l r. (exists pfh_trace_code_successor_execution pfh_trace_scale_successor_execution. (((exists pfa_gap_successor_executiontracebase. pfa_gap_successor_executiontracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_executiontraceinitial. ff_h_pfp_successor_executiontraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontraceinitial. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontraceinitial * S ((S (0)) * pfh_trace_scale_successor_execution) + (0))) /\ (((((exists ff_h_pfp_successor_executiontraceterminal. ff_h_pfp_successor_executiontraceterminal + S (r) = S ((S (S l)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontraceterminal. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontraceterminal * S ((S (S l)) * pfh_trace_scale_successor_execution) + (r))) /\ ((forall pfh_index_successor_executiontracesteps. (exists pfa_gap_successor_executiontracestepsindex. pfa_gap_successor_executiontracestepsindex + S (pfh_index_successor_executiontracesteps) = (S l)) -> (exists pfh_coefficient_successor_executiontracestepsstep pfh_before_successor_executiontracestepsstep pfh_after_successor_executiontracestepsstep pfh_product_successor_executiontracestepsstep. ((((exists ff_h_pfp_successor_executiontracestepsstepcoefficient. ff_h_pfp_successor_executiontracestepsstepcoefficient + S (pfh_coefficient_successor_executiontracestepsstep) = S ((S (pfh_index_successor_executiontracesteps)) * c)) /\ exists ff_q_pfp_successor_executiontracestepsstepcoefficient. b = ff_q_pfp_successor_executiontracestepsstepcoefficient * S ((S (pfh_index_successor_executiontracesteps)) * c) + (pfh_coefficient_successor_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_executiontracestepsstepbefore. ff_h_pfp_successor_executiontracestepsstepbefore + S (pfh_before_successor_executiontracestepsstep) = S ((S (pfh_index_successor_executiontracesteps)) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontracestepsstepbefore. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontracestepsstepbefore * S ((S (pfh_index_successor_executiontracesteps)) * pfh_trace_scale_successor_execution) + (pfh_before_successor_executiontracestepsstep))) /\ (((((exists ff_h_pfp_successor_executiontracestepsstepafter. ff_h_pfp_successor_executiontracestepsstepafter + S (pfh_after_successor_executiontracestepsstep) = S ((S (S (pfh_index_successor_executiontracesteps))) * pfh_trace_scale_successor_execution)) /\ exists ff_q_pfp_successor_executiontracestepsstepafter. pfh_trace_code_successor_execution = ff_q_pfp_successor_executiontracestepsstepafter * S ((S (S (pfh_index_successor_executiontracesteps))) * pfh_trace_scale_successor_execution) + (pfh_after_successor_executiontracestepsstep))) /\ (((((exists pfa_gap_successor_executiontracestepsstepmultiplyleft. pfa_gap_successor_executiontracestepsstepmultiplyleft + S (pfh_before_successor_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_executiontracestepsstepmultiplyright. pfa_gap_successor_executiontracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_executiontracestepsstepmultiplyresultbound. pfa_gap_successor_executiontracestepsstepmultiplyresultbound + S (pfh_product_successor_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_executiontracestepsstepmultiplyresultcongruence pfa_offset_right_successor_executiontracestepsstepmultiplyresultcongruence. ((pfh_before_successor_executiontracestepsstep) * (t)) + (p) * pfa_offset_left_successor_executiontracestepsstepmultiplyresultcongruence = (pfh_product_successor_executiontracestepsstep) + (p) * pfa_offset_right_successor_executiontracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_executiontracestepsstepaddleft. pfa_gap_successor_executiontracestepsstepaddleft + S (pfh_product_successor_executiontracestepsstep) = (p)) /\ (((exists pfa_gap_successor_executiontracestepsstepaddright. pfa_gap_successor_executiontracestepsstepaddright + S (pfh_coefficient_successor_executiontracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_executiontracestepsstepaddresultbound. pfa_gap_successor_executiontracestepsstepaddresultbound + S (pfh_after_successor_executiontracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_executiontracestepsstepaddresultcongruence pfa_offset_right_successor_executiontracestepsstepaddresultcongruence. ((pfh_product_successor_executiontracestepsstep) + (pfh_coefficient_successor_executiontracestepsstep)) + (p) * pfa_offset_left_successor_executiontracestepsstepaddresultcongruence = (pfh_after_successor_executiontracestepsstep) + (p) * pfa_offset_right_successor_executiontracestepsstepaddresultcongruence))))))))))))))))))))))))))) -> exists a h k. ((((exists ff_h_pfp_successor_coefficient. ff_h_pfp_successor_coefficient + S (a) = S ((S (l)) * c)) /\ exists ff_q_pfp_successor_coefficient. b = ff_q_pfp_successor_coefficient * S ((S (l)) * c) + (a))) /\ (((exists pfh_trace_code_successor_prefix pfh_trace_scale_successor_prefix. (((exists pfa_gap_successor_prefixtracebase. pfa_gap_successor_prefixtracebase + S (t) = (p)) /\ (((((exists ff_h_pfp_successor_prefixtraceinitial. ff_h_pfp_successor_prefixtraceinitial + S (0) = S ((S (0)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtraceinitial. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtraceinitial * S ((S (0)) * pfh_trace_scale_successor_prefix) + (0))) /\ (((((exists ff_h_pfp_successor_prefixtraceterminal. ff_h_pfp_successor_prefixtraceterminal + S (h) = S ((S (l)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtraceterminal. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtraceterminal * S ((S (l)) * pfh_trace_scale_successor_prefix) + (h))) /\ ((forall pfh_index_successor_prefixtracesteps. (exists pfa_gap_successor_prefixtracestepsindex. pfa_gap_successor_prefixtracestepsindex + S (pfh_index_successor_prefixtracesteps) = (l)) -> (exists pfh_coefficient_successor_prefixtracestepsstep pfh_before_successor_prefixtracestepsstep pfh_after_successor_prefixtracestepsstep pfh_product_successor_prefixtracestepsstep. ((((exists ff_h_pfp_successor_prefixtracestepsstepcoefficient. ff_h_pfp_successor_prefixtracestepsstepcoefficient + S (pfh_coefficient_successor_prefixtracestepsstep) = S ((S (pfh_index_successor_prefixtracesteps)) * c)) /\ exists ff_q_pfp_successor_prefixtracestepsstepcoefficient. b = ff_q_pfp_successor_prefixtracestepsstepcoefficient * S ((S (pfh_index_successor_prefixtracesteps)) * c) + (pfh_coefficient_successor_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_prefixtracestepsstepbefore. ff_h_pfp_successor_prefixtracestepsstepbefore + S (pfh_before_successor_prefixtracestepsstep) = S ((S (pfh_index_successor_prefixtracesteps)) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtracestepsstepbefore. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtracestepsstepbefore * S ((S (pfh_index_successor_prefixtracesteps)) * pfh_trace_scale_successor_prefix) + (pfh_before_successor_prefixtracestepsstep))) /\ (((((exists ff_h_pfp_successor_prefixtracestepsstepafter. ff_h_pfp_successor_prefixtracestepsstepafter + S (pfh_after_successor_prefixtracestepsstep) = S ((S (S (pfh_index_successor_prefixtracesteps))) * pfh_trace_scale_successor_prefix)) /\ exists ff_q_pfp_successor_prefixtracestepsstepafter. pfh_trace_code_successor_prefix = ff_q_pfp_successor_prefixtracestepsstepafter * S ((S (S (pfh_index_successor_prefixtracesteps))) * pfh_trace_scale_successor_prefix) + (pfh_after_successor_prefixtracestepsstep))) /\ (((((exists pfa_gap_successor_prefixtracestepsstepmultiplyleft. pfa_gap_successor_prefixtracestepsstepmultiplyleft + S (pfh_before_successor_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_prefixtracestepsstepmultiplyright. pfa_gap_successor_prefixtracestepsstepmultiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_prefixtracestepsstepmultiplyresultbound. pfa_gap_successor_prefixtracestepsstepmultiplyresultbound + S (pfh_product_successor_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_prefixtracestepsstepmultiplyresultcongruence pfa_offset_right_successor_prefixtracestepsstepmultiplyresultcongruence. ((pfh_before_successor_prefixtracestepsstep) * (t)) + (p) * pfa_offset_left_successor_prefixtracestepsstepmultiplyresultcongruence = (pfh_product_successor_prefixtracestepsstep) + (p) * pfa_offset_right_successor_prefixtracestepsstepmultiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_prefixtracestepsstepaddleft. pfa_gap_successor_prefixtracestepsstepaddleft + S (pfh_product_successor_prefixtracestepsstep) = (p)) /\ (((exists pfa_gap_successor_prefixtracestepsstepaddright. pfa_gap_successor_prefixtracestepsstepaddright + S (pfh_coefficient_successor_prefixtracestepsstep) = (p)) /\ ((((exists pfa_gap_successor_prefixtracestepsstepaddresultbound. pfa_gap_successor_prefixtracestepsstepaddresultbound + S (pfh_after_successor_prefixtracestepsstep) = (p)) /\ ((exists pfa_offset_left_successor_prefixtracestepsstepaddresultcongruence pfa_offset_right_successor_prefixtracestepsstepaddresultcongruence. ((pfh_product_successor_prefixtracestepsstep) + (pfh_coefficient_successor_prefixtracestepsstep)) + (p) * pfa_offset_left_successor_prefixtracestepsstepaddresultcongruence = (pfh_after_successor_prefixtracestepsstep) + (p) * pfa_offset_right_successor_prefixtracestepsstepaddresultcongruence))))))))))))))))))))))))))) /\ (((((exists pfa_gap_successor_multiplyleft. pfa_gap_successor_multiplyleft + S (h) = (p)) /\ (((exists pfa_gap_successor_multiplyright. pfa_gap_successor_multiplyright + S (t) = (p)) /\ ((((exists pfa_gap_successor_multiplyresultbound. pfa_gap_successor_multiplyresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_successor_multiplyresultcongruence pfa_offset_right_successor_multiplyresultcongruence. ((h) * (t)) + (p) * pfa_offset_left_successor_multiplyresultcongruence = (k) + (p) * pfa_offset_right_successor_multiplyresultcongruence))))))))) /\ ((((exists pfa_gap_successor_addleft. pfa_gap_successor_addleft + S (k) = (p)) /\ (((exists pfa_gap_successor_addright. pfa_gap_successor_addright + S (a) = (p)) /\ ((((exists pfa_gap_successor_addresultbound. pfa_gap_successor_addresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_successor_addresultcongruence pfa_offset_right_successor_addresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_successor_addresultcongruence = (r) + (p) * pfa_offset_right_successor_addresultcongruence)))))))))))))))

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 · 23 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.

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 r
  7. L7
    intro h
02Separate the logical casesL8–12

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

  1. L8
    cases h
  2. L9
    cases h_witness
  3. L10
    cases h_witness_witness
  4. L11
    cases h_witness_witness_right
  5. L12
    cases h_witness_witness_right_right
03Establish hsL13–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h witness witness right right right.

  1. L13
    have hs : FpHornerStep(p,b,c,t,x,x1,l)Definitions: FpHornerStep(p,b,c,t,x,x1,l)Original native command in the exact edition
  2. L14
    specialize h_witness_witness_right_right_right (l)
  3. L15
    apply h_witness_witness_right_right_right
04Construct an explicit witnessL16–16

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

  1. L16
    exists 0
05Use earlier factsL17–17

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

  1. L17
    apply zero_add
06Separate the logical casesL18–25

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

  1. L18
    cases hs
  2. L19
    cases hs_witness
  3. L20
    cases hs_witness_witness
  4. L21
    cases hs_witness_witness_witness
  5. L22
    cases hs_witness_witness_witness_witness
  6. L23
    cases hs_witness_witness_witness_witness_right
  7. L24
    cases hs_witness_witness_witness_witness_right_right
  8. L25
    cases hs_witness_witness_witness_witness_right_right_right
07Establish heqL26–35

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

  1. L26
    have heq : x4=r
  2. L27
    specialize beta_at_unique (x)
  3. L28
    specialize beta_at_unique (x1)
  4. L29
    specialize beta_at_unique (S l)
  5. L30
    specialize beta_at_unique (x4)
  6. L31
    specialize beta_at_unique (r)
  7. L32
    apply beta_at_unique
  8. L33
    exact hs_witness_witness_witness_witness_right_right_left
  9. L34
    exact h_witness_witness_right_right_left
  10. L35
    rewrite heq at hs_witness_witness_witness_witness_right_right_right_right
08Calculate and transport equalitiesL36–36

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite heq at hs_witness_witness_witness_witness_right_right_right_right
09Construct an explicit witnessL37–39

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

  1. L37
    exists x2
  2. L38
    exists x3
  3. L39
    exists x5
10Separate the logical casesL40–40

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

  1. L40
    split
11Use earlier factsL41–41

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

  1. L41
    exact hs_witness_witness_witness_witness_left
12Separate the logical casesL42–42

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

  1. L42
    split
13Construct an explicit witnessL43–44

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

  1. L43
    exists x
  2. L44
    exists x1
14Separate the logical casesL45–45

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

  1. L45
    split
15Use earlier factsL46–46

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

  1. L46
    exact h_witness_witness_left
16Separate the logical casesL47–47

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

  1. L47
    split
17Use earlier factsL48–48

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

  1. L48
    exact h_witness_witness_right_left
18Separate the logical casesL49–49

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

  1. L49
    split
19Use earlier factsL50–50

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

  1. L50
    exact hs_witness_witness_witness_witness_right_left
20Fix variables and assumptionsL51–52

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

  1. L51
    intro i
  2. L52
    intro hi
21Use earlier factsL53–58

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

  1. L53
    specialize h_witness_witness_right_right_right (i)
  2. L54
    apply h_witness_witness_right_right_right
  3. L55
    specialize le_succ (S i)
  4. L56
    specialize le_succ (l)
  5. L57
    apply le_succ
  6. L58
    exact hi
22Separate the logical casesL59–59

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

  1. L59
    split
23Use earlier factsL60–61

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

  1. L60
    exact hs_witness_witness_witness_witness_right_right_right_left
  2. L61
    exact hs_witness_witness_witness_witness_right_right_right_right

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 r
  7. 0007intro h
  8. 0008cases h
  9. 0009cases h_witness
  10. 0010cases h_witness_witness
  11. 0011cases h_witness_witness_right
  12. 0012cases h_witness_witness_right_right
  13. 0013have hs : FpHornerStep(p,b,c,t,x,x1,l)
  14. 0014specialize h_witness_witness_right_right_right (l)
  15. 0015apply h_witness_witness_right_right_right
  16. 0016exists 0
  17. 0017apply zero_add
  18. 0018cases hs
  19. 0019cases hs_witness
  20. 0020cases hs_witness_witness
  21. 0021cases hs_witness_witness_witness
  22. 0022cases hs_witness_witness_witness_witness
  23. 0023cases hs_witness_witness_witness_witness_right
  24. 0024cases hs_witness_witness_witness_witness_right_right
  25. 0025cases hs_witness_witness_witness_witness_right_right_right
  26. 0026have heq : x4=r
  27. 0027specialize beta_at_unique (x)
  28. 0028specialize beta_at_unique (x1)
  29. 0029specialize beta_at_unique (S l)
  30. 0030specialize beta_at_unique (x4)
  31. 0031specialize beta_at_unique (r)
  32. 0032apply beta_at_unique
  33. 0033exact hs_witness_witness_witness_witness_right_right_left
  34. 0034exact h_witness_witness_right_right_left
  35. 0035rewrite heq at hs_witness_witness_witness_witness_right_right_right_right
  36. 0036rewrite heq at hs_witness_witness_witness_witness_right_right_right_right
  37. 0037exists x2
  38. 0038exists x3
  39. 0039exists x5
  40. 0040split
  41. 0041exact hs_witness_witness_witness_witness_left
  42. 0042split
  43. 0043exists x
  44. 0044exists x1
  45. 0045split
  46. 0046exact h_witness_witness_left
  47. 0047split
  48. 0048exact h_witness_witness_right_left
  49. 0049split
  50. 0050exact hs_witness_witness_witness_witness_right_left
  51. 0051intro i
  52. 0052intro hi
  53. 0053specialize h_witness_witness_right_right_right (i)
  54. 0054apply h_witness_witness_right_right_right
  55. 0055specialize le_succ (S i)
  56. 0056specialize le_succ (l)
  57. 0057apply le_succ
  58. 0058exact hi
  59. 0059split
  60. 0060exact hs_witness_witness_witness_witness_right_right_right_left
  61. 0061exact hs_witness_witness_witness_witness_right_right_right_right