PP0020

prime_field_polynomial_horner_canonical_step

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

Construct an actual canonical multiply-then-add step from proved residues of the corresponding natural step.

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 n t a r s. (~((p) = 1) /\ forall pfa_factor_left_step_prime pfa_factor_right_step_prime. (p) = pfa_factor_left_step_prime * pfa_factor_right_step_prime -> pfa_factor_left_step_prime = 1 \/ pfa_factor_right_step_prime = 1) -> (exists pfa_gap_step_base. pfa_gap_step_base + S (t) = (p)) -> (exists pfa_gap_step_coefficient. pfa_gap_step_coefficient + S (a) = (p)) -> (((exists pfa_gap_step_previousbound. pfa_gap_step_previousbound + S (r) = (p)) /\ ((exists pfa_offset_left_step_previouscongruence pfa_offset_right_step_previouscongruence. (n) + (p) * pfa_offset_left_step_previouscongruence = (r) + (p) * pfa_offset_right_step_previouscongruence)))) -> (((exists pfa_gap_step_nextbound. pfa_gap_step_nextbound + S (s) = (p)) /\ ((exists pfa_offset_left_step_nextcongruence pfa_offset_right_step_nextcongruence. (n*t+a) + (p) * pfa_offset_left_step_nextcongruence = (s) + (p) * pfa_offset_right_step_nextcongruence)))) -> exists k. ((((exists pfa_gap_step_productleft. pfa_gap_step_productleft + S (r) = (p)) /\ (((exists pfa_gap_step_productright. pfa_gap_step_productright + S (t) = (p)) /\ ((((exists pfa_gap_step_productresultbound. pfa_gap_step_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_step_productresultcongruence pfa_offset_right_step_productresultcongruence. ((r) * (t)) + (p) * pfa_offset_left_step_productresultcongruence = (k) + (p) * pfa_offset_right_step_productresultcongruence))))))))) /\ ((((exists pfa_gap_step_sumleft. pfa_gap_step_sumleft + S (k) = (p)) /\ (((exists pfa_gap_step_sumright. pfa_gap_step_sumright + S (a) = (p)) /\ ((((exists pfa_gap_step_sumresultbound. pfa_gap_step_sumresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_step_sumresultcongruence pfa_offset_right_step_sumresultcongruence. ((k) + (a)) + (p) * pfa_offset_left_step_sumresultcongruence = (s) + (p) * pfa_offset_right_step_sumresultcongruence)))))))))))

Constructive proof overview

Generated structural guide

Construct an actual canonical multiply-then-add step from proved residues of the corresponding natural step.

The unchanged tactic script uses 6 declared prerequisites and contains 79 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_multiply_exists Alpha theorem; checked-use authorized prime_field_add_exists Alpha theorem; checked-use authorized prime_field_residue_multiply Alpha theorem; checked-use authorized prime_field_residue_add Alpha theorem; checked-use authorized prime_field_residue_reflexive Alpha theorem; checked-use authorized binary_canonical_residue_functional Alpha theorem; checked-use authorized

Direct dependents

PP0021 prime_field_polynomial_horner_trace_from_normalization

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

79 script commands · 20 reading checkpoints · 7 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro t
  4. L4
    intro a
  5. L5
    intro r
  6. L6
    intro s
  7. L7
    intro hp
  8. L8
    intro ht
  9. L9
    intro ha
  10. L10
    intro hr
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hs
03Establish hrcopyL12–13

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

  1. L12
    have hrcopy : ((exists pfa_gap_step_previous_copybound. pfa_gap_step_previous_copybound + S (r) = (p)) /\ ((exists pfa_offset_left_step_previous_copycongruence pfa_offset_right_step_previous_copycongruence. (n) + (p) * pfa_offset_left_step_previous_copycongruence = (r) + (p) * pfa_offset_right_step_previous_copycongruence)))
  2. L13
    exact hr
04Separate the logical casesL14–14

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

  1. L14
    cases hrcopy
05Establish hmL15–22

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

  1. L15
    have hm : exists k. (((exists pfa_gap_step_chosen_productleft. pfa_gap_step_chosen_productleft + S (r) = (p)) /\ (((exists pfa_gap_step_chosen_productright. pfa_gap_step_chosen_productright + S (t) = (p)) /\ ((((exists pfa_gap_step_chosen_productresultbound. pfa_gap_step_chosen_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_step_chosen_productresultcongruence pfa_offset_right_step_chosen_productresultcongruence. ((r) * (t)) + (p) * pfa_offset_left_step_chosen_productresultcongruence = (k) + (p) * pfa_offset_right_step_chosen_productresultcongruence)))))))))
  2. L16
    specialize prime_field_multiply_exists (p)
  3. L17
    specialize prime_field_multiply_exists (r)
  4. L18
    specialize prime_field_multiply_exists (t)
  5. L19
    apply prime_field_multiply_exists
  6. L20
    exact hp
  7. L21
    exact hrcopy_left
  8. L22
    exact ht
06Separate the logical casesL23–23

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

  1. L23
    cases hm
07Establish hmcopyL24–25

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

  1. L24
    have hmcopy : ((exists pfa_gap_step_product_copyleft. pfa_gap_step_product_copyleft + S (r) = (p)) /\ (((exists pfa_gap_step_product_copyright. pfa_gap_step_product_copyright + S (t) = (p)) /\ ((((exists pfa_gap_step_product_copyresultbound. pfa_gap_step_product_copyresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_step_product_copyresultcongruence pfa_offset_right_step_product_copyresultcongruence. ((r) * (t)) + (p) * pfa_offset_left_step_product_copyresultcongruence = (x) + (p) * pfa_offset_right_step_product_copyresultcongruence))))))))
  2. L25
    exact hm_witness
08Separate the logical casesL26–28

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

  1. L26
    cases hmcopy
  2. L27
    cases hmcopy_right
  3. L28
    cases hmcopy_right_right
09Establish haddL29–36

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

  1. L29
    have hadd : exists z. (((exists pfa_gap_step_chosen_sumleft. pfa_gap_step_chosen_sumleft + S (x) = (p)) /\ (((exists pfa_gap_step_chosen_sumright. pfa_gap_step_chosen_sumright + S (a) = (p)) /\ ((((exists pfa_gap_step_chosen_sumresultbound. pfa_gap_step_chosen_sumresultbound + S (z) = (p)) /\ ((exists pfa_offset_left_step_chosen_sumresultcongruence pfa_offset_right_step_chosen_sumresultcongruence. ((x) + (a)) + (p) * pfa_offset_left_step_chosen_sumresultcongruence = (z) + (p) * pfa_offset_right_step_chosen_sumresultcongruence)))))))))
  2. L30
    specialize prime_field_add_exists (p)
  3. L31
    specialize prime_field_add_exists (x)
  4. L32
    specialize prime_field_add_exists (a)
  5. L33
    apply prime_field_add_exists
  6. L34
    exact hp
  7. L35
    exact hmcopy_right_right_left
  8. L36
    exact ha
10Separate the logical casesL37–37

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

  1. L37
    cases hadd
11Establish hmulresL38–47

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

  1. L38
    have hmulres : ((exists pfa_gap_step_product_residuebound. pfa_gap_step_product_residuebound + S (x) = (p)) /\ ((exists pfa_offset_left_step_product_residuecongruence pfa_offset_right_step_product_residuecongruence. (n*t) + (p) * pfa_offset_left_step_product_residuecongruence = (x) + (p) * pfa_offset_right_step_product_residuecongruence)))
  2. L39
    specialize prime_field_residue_multiply (p)
  3. L40
    specialize prime_field_residue_multiply (n)
  4. L41
    specialize prime_field_residue_multiply (t)
  5. L42
    specialize prime_field_residue_multiply (r)
  6. L43
    specialize prime_field_residue_multiply (t)
  7. L44
    specialize prime_field_residue_multiply (x)
  8. L45
    apply prime_field_residue_multiply
  9. L46
    exact hr
  10. L47
    specialize prime_field_residue_reflexive (p)
12Use earlier factsL48–51

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

  1. L48
    specialize prime_field_residue_reflexive (t)
  2. L49
    apply prime_field_residue_reflexive
  3. L50
    exact ht
  4. L51
    exact hm_witness
13Establish hsumresL52–61

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

  1. L52
    have hsumres : ((exists pfa_gap_step_sum_residuebound. pfa_gap_step_sum_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_step_sum_residuecongruence pfa_offset_right_step_sum_residuecongruence. (n*t+a) + (p) * pfa_offset_left_step_sum_residuecongruence = (x1) + (p) * pfa_offset_right_step_sum_residuecongruence)))
  2. L53
    specialize prime_field_residue_add (p)
  3. L54
    specialize prime_field_residue_add (n*t)
  4. L55
    specialize prime_field_residue_add (a)
  5. L56
    specialize prime_field_residue_add (x)
  6. L57
    specialize prime_field_residue_add (a)
  7. L58
    specialize prime_field_residue_add (x1)
  8. L59
    apply prime_field_residue_add
  9. L60
    exact hmulres
  10. L61
    specialize prime_field_residue_reflexive (p)
14Use earlier factsL62–65

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

  1. L62
    specialize prime_field_residue_reflexive (a)
  2. L63
    apply prime_field_residue_reflexive
  3. L64
    exact ha
  4. L65
    exact hadd_witness
15Establish heqL66–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary canonical residue functional.

  1. L66
    have heq : x1=s
  2. L67
    specialize binary_canonical_residue_functional (p)
  3. L68
    specialize binary_canonical_residue_functional (n*t+a)
  4. L69
    specialize binary_canonical_residue_functional (x1)
  5. L70
    specialize binary_canonical_residue_functional (s)
  6. L71
    apply binary_canonical_residue_functional
  7. L72
    exact hsumres
  8. L73
    exact hs
16Construct an explicit witnessL74–74

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

  1. L74
    exists x
17Separate the logical casesL75–75

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

  1. L75
    split
18Use earlier factsL76–76

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

  1. L76
    exact hm_witness
19Calculate and transport equalitiesL77–78

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

  1. L77
    rewrite heq at hadd_witness
  2. L78
    rewrite heq at hadd_witness
20Use earlier factsL79–79

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

  1. L79
    exact hadd_witness

Library-wide reading audit

Original exact command ledger · 79 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro t
  4. 0004intro a
  5. 0005intro r
  6. 0006intro s
  7. 0007intro hp
  8. 0008intro ht
  9. 0009intro ha
  10. 0010intro hr
  11. 0011intro hs
  12. 0012have hrcopy : ((exists pfa_gap_step_previous_copybound. pfa_gap_step_previous_copybound + S (r) = (p)) /\ ((exists pfa_offset_left_step_previous_copycongruence pfa_offset_right_step_previous_copycongruence. (n) + (p) * pfa_offset_left_step_previous_copycongruence = (r) + (p) * pfa_offset_right_step_previous_copycongruence)))
  13. 0013exact hr
  14. 0014cases hrcopy
  15. 0015have hm : exists k. (((exists pfa_gap_step_chosen_productleft. pfa_gap_step_chosen_productleft + S (r) = (p)) /\ (((exists pfa_gap_step_chosen_productright. pfa_gap_step_chosen_productright + S (t) = (p)) /\ ((((exists pfa_gap_step_chosen_productresultbound. pfa_gap_step_chosen_productresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_step_chosen_productresultcongruence pfa_offset_right_step_chosen_productresultcongruence. ((r) * (t)) + (p) * pfa_offset_left_step_chosen_productresultcongruence = (k) + (p) * pfa_offset_right_step_chosen_productresultcongruence)))))))))
  16. 0016specialize prime_field_multiply_exists (p)
  17. 0017specialize prime_field_multiply_exists (r)
  18. 0018specialize prime_field_multiply_exists (t)
  19. 0019apply prime_field_multiply_exists
  20. 0020exact hp
  21. 0021exact hrcopy_left
  22. 0022exact ht
  23. 0023cases hm
  24. 0024have hmcopy : ((exists pfa_gap_step_product_copyleft. pfa_gap_step_product_copyleft + S (r) = (p)) /\ (((exists pfa_gap_step_product_copyright. pfa_gap_step_product_copyright + S (t) = (p)) /\ ((((exists pfa_gap_step_product_copyresultbound. pfa_gap_step_product_copyresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_step_product_copyresultcongruence pfa_offset_right_step_product_copyresultcongruence. ((r) * (t)) + (p) * pfa_offset_left_step_product_copyresultcongruence = (x) + (p) * pfa_offset_right_step_product_copyresultcongruence))))))))
  25. 0025exact hm_witness
  26. 0026cases hmcopy
  27. 0027cases hmcopy_right
  28. 0028cases hmcopy_right_right
  29. 0029have hadd : exists z. (((exists pfa_gap_step_chosen_sumleft. pfa_gap_step_chosen_sumleft + S (x) = (p)) /\ (((exists pfa_gap_step_chosen_sumright. pfa_gap_step_chosen_sumright + S (a) = (p)) /\ ((((exists pfa_gap_step_chosen_sumresultbound. pfa_gap_step_chosen_sumresultbound + S (z) = (p)) /\ ((exists pfa_offset_left_step_chosen_sumresultcongruence pfa_offset_right_step_chosen_sumresultcongruence. ((x) + (a)) + (p) * pfa_offset_left_step_chosen_sumresultcongruence = (z) + (p) * pfa_offset_right_step_chosen_sumresultcongruence)))))))))
  30. 0030specialize prime_field_add_exists (p)
  31. 0031specialize prime_field_add_exists (x)
  32. 0032specialize prime_field_add_exists (a)
  33. 0033apply prime_field_add_exists
  34. 0034exact hp
  35. 0035exact hmcopy_right_right_left
  36. 0036exact ha
  37. 0037cases hadd
  38. 0038have hmulres : ((exists pfa_gap_step_product_residuebound. pfa_gap_step_product_residuebound + S (x) = (p)) /\ ((exists pfa_offset_left_step_product_residuecongruence pfa_offset_right_step_product_residuecongruence. (n*t) + (p) * pfa_offset_left_step_product_residuecongruence = (x) + (p) * pfa_offset_right_step_product_residuecongruence)))
  39. 0039specialize prime_field_residue_multiply (p)
  40. 0040specialize prime_field_residue_multiply (n)
  41. 0041specialize prime_field_residue_multiply (t)
  42. 0042specialize prime_field_residue_multiply (r)
  43. 0043specialize prime_field_residue_multiply (t)
  44. 0044specialize prime_field_residue_multiply (x)
  45. 0045apply prime_field_residue_multiply
  46. 0046exact hr
  47. 0047specialize prime_field_residue_reflexive (p)
  48. 0048specialize prime_field_residue_reflexive (t)
  49. 0049apply prime_field_residue_reflexive
  50. 0050exact ht
  51. 0051exact hm_witness
  52. 0052have hsumres : ((exists pfa_gap_step_sum_residuebound. pfa_gap_step_sum_residuebound + S (x1) = (p)) /\ ((exists pfa_offset_left_step_sum_residuecongruence pfa_offset_right_step_sum_residuecongruence. (n*t+a) + (p) * pfa_offset_left_step_sum_residuecongruence = (x1) + (p) * pfa_offset_right_step_sum_residuecongruence)))
  53. 0053specialize prime_field_residue_add (p)
  54. 0054specialize prime_field_residue_add (n*t)
  55. 0055specialize prime_field_residue_add (a)
  56. 0056specialize prime_field_residue_add (x)
  57. 0057specialize prime_field_residue_add (a)
  58. 0058specialize prime_field_residue_add (x1)
  59. 0059apply prime_field_residue_add
  60. 0060exact hmulres
  61. 0061specialize prime_field_residue_reflexive (p)
  62. 0062specialize prime_field_residue_reflexive (a)
  63. 0063apply prime_field_residue_reflexive
  64. 0064exact ha
  65. 0065exact hadd_witness
  66. 0066have heq : x1=s
  67. 0067specialize binary_canonical_residue_functional (p)
  68. 0068specialize binary_canonical_residue_functional (n*t+a)
  69. 0069specialize binary_canonical_residue_functional (x1)
  70. 0070specialize binary_canonical_residue_functional (s)
  71. 0071apply binary_canonical_residue_functional
  72. 0072exact hsumres
  73. 0073exact hs
  74. 0074exists x
  75. 0075split
  76. 0076exact hm_witness
  77. 0077rewrite heq at hadd_witness
  78. 0078rewrite heq at hadd_witness
  79. 0079exact hadd_witness