PP0020

prime_field_polynomial_horner_canonical_step

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

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. ∀ n. ∀ t. ∀ a. ∀ r. ∀ s. Prime(p) → Lt(t,p) → Lt(a,p) → CanonicalModularResidue(p,n,r) → CanonicalModularResidue(p,n · t + a,s) → ∃ x. FpMul(p,r,t,x) ∧ FpAdd(p,x,a,s)

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

Definition DAG

CanonicalModularResidue(m,a,r) · 5FpAdd(p,a,b,c) · 2FpMul(p,a,b,c) · 3Lt(a,b) · 2Prime(p) · 1

Actual proof prerequisites

prime_field_multiply_exists · checked external prerequisiteprime_field_add_exists · checked external prerequisiteprime_field_residue_multiply · checked external prerequisiteprime_field_residue_add · checked external prerequisiteprime_field_residue_reflexive · checked external prerequisitebinary_canonical_residue_functional · checked external prerequisite
Original expanded first-order 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)))))))))))

Complete tactic proof in conservative notation

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

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.

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–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 : CanonicalModularResidue(p,n,r)Definitions: CanonicalModularResidue(p,n,r)Original native command in the exact edition
  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 : ∃ k. FpMul(p,r,t,k)Definitions: FpMul(p,r,t,k)Original native command in the exact edition
  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 : FpMul(p,r,t,x)Definitions: FpMul(p,r,t,x)Original native command in the exact edition
  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 : ∃ z. FpAdd(p,x,a,z)Definitions: FpAdd(p,x,a,z)Original native command in the exact edition
  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 : CanonicalModularResidue(p,n · t,x)Definitions: CanonicalModularResidue(p,n · t,x)Original native command in the exact edition
  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 : CanonicalModularResidue(p,n · t + a,x1)Definitions: CanonicalModularResidue(p,n · t + a,x1)Original native command in the exact edition
  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 defined 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 : CanonicalModularResidue(p,n,r)
  13. 0013exact hr
  14. 0014cases hrcopy
  15. 0015have hm : ∃ k. FpMul(p,r,t,k)
  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 : FpMul(p,r,t,x)
  25. 0025exact hm_witness
  26. 0026cases hmcopy
  27. 0027cases hmcopy_right
  28. 0028cases hmcopy_right_right
  29. 0029have hadd : ∃ z. FpAdd(p,x,a,z)
  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 : CanonicalModularResidue(p,n · t,x)
  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 : CanonicalModularResidue(p,n · t + a,x1)
  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