PP001D

prime_field_polynomial_scale_associative

Two successive canonical scalar actions agree coefficientwise with the actual canonical product scalar.

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. ∀ a. ∀ b. ∀ k. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ l. FpMul(p,a,b,k) → FpPolyScale(p,b,ab,ac,bb,bc,l) → FpPolyScale(p,a,bb,bc,ub,uc,l) → FpPolyScale(p,k,ab,ac,vb,vc,l) → BetaPrefixEqual(ub,uc,vb,vc,l)

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

Definition DAG

FpMul(p,a,b,c) · 1BetaPrefixEqual(b,c,d,e,l) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 3BetaAt(b,c,i,x) · 3

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_multiply_associative · checked external prerequisiteprime_field_polynomial_scale_entry
Original expanded first-order statement 
forall p a b k ab ac bb bc ub uc vb vc l. (((exists pfa_gap_scale_assoc_scalarsleft. pfa_gap_scale_assoc_scalarsleft + S (a) = (p)) /\ (((exists pfa_gap_scale_assoc_scalarsright. pfa_gap_scale_assoc_scalarsright + S (b) = (p)) /\ ((((exists pfa_gap_scale_assoc_scalarsresultbound. pfa_gap_scale_assoc_scalarsresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_scale_assoc_scalarsresultcongruence pfa_offset_right_scale_assoc_scalarsresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_scale_assoc_scalarsresultcongruence = (k) + (p) * pfa_offset_right_scale_assoc_scalarsresultcongruence))))))))) -> (((exists pfa_gap_scale_assoc_firstscalar. pfa_gap_scale_assoc_firstscalar + S (b) = (p)) /\ ((forall pfp_index_scale_assoc_first. (exists pfa_gap_scale_assoc_firstindex. pfa_gap_scale_assoc_firstindex + S (pfp_index_scale_assoc_first) = (l)) -> exists pfp_source_scale_assoc_first pfp_value_scale_assoc_first. ((((exists ff_h_pfp_scale_assoc_firstsource. ff_h_pfp_scale_assoc_firstsource + S (pfp_source_scale_assoc_first) = S ((S (pfp_index_scale_assoc_first)) * ac)) /\ exists ff_q_pfp_scale_assoc_firstsource. ab = ff_q_pfp_scale_assoc_firstsource * S ((S (pfp_index_scale_assoc_first)) * ac) + (pfp_source_scale_assoc_first))) /\ (((((exists ff_h_pfp_scale_assoc_firsttarget. ff_h_pfp_scale_assoc_firsttarget + S (pfp_value_scale_assoc_first) = S ((S (pfp_index_scale_assoc_first)) * bc)) /\ exists ff_q_pfp_scale_assoc_firsttarget. bb = ff_q_pfp_scale_assoc_firsttarget * S ((S (pfp_index_scale_assoc_first)) * bc) + (pfp_value_scale_assoc_first))) /\ ((((exists pfa_gap_scale_assoc_firstoperationleft. pfa_gap_scale_assoc_firstoperationleft + S (b) = (p)) /\ (((exists pfa_gap_scale_assoc_firstoperationright. pfa_gap_scale_assoc_firstoperationright + S (pfp_source_scale_assoc_first) = (p)) /\ ((((exists pfa_gap_scale_assoc_firstoperationresultbound. pfa_gap_scale_assoc_firstoperationresultbound + S (pfp_value_scale_assoc_first) = (p)) /\ ((exists pfa_offset_left_scale_assoc_firstoperationresultcongruence pfa_offset_right_scale_assoc_firstoperationresultcongruence. ((b) * (pfp_source_scale_assoc_first)) + (p) * pfa_offset_left_scale_assoc_firstoperationresultcongruence = (pfp_value_scale_assoc_first) + (p) * pfa_offset_right_scale_assoc_firstoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scale_assoc_secondscalar. pfa_gap_scale_assoc_secondscalar + S (a) = (p)) /\ ((forall pfp_index_scale_assoc_second. (exists pfa_gap_scale_assoc_secondindex. pfa_gap_scale_assoc_secondindex + S (pfp_index_scale_assoc_second) = (l)) -> exists pfp_source_scale_assoc_second pfp_value_scale_assoc_second. ((((exists ff_h_pfp_scale_assoc_secondsource. ff_h_pfp_scale_assoc_secondsource + S (pfp_source_scale_assoc_second) = S ((S (pfp_index_scale_assoc_second)) * bc)) /\ exists ff_q_pfp_scale_assoc_secondsource. bb = ff_q_pfp_scale_assoc_secondsource * S ((S (pfp_index_scale_assoc_second)) * bc) + (pfp_source_scale_assoc_second))) /\ (((((exists ff_h_pfp_scale_assoc_secondtarget. ff_h_pfp_scale_assoc_secondtarget + S (pfp_value_scale_assoc_second) = S ((S (pfp_index_scale_assoc_second)) * uc)) /\ exists ff_q_pfp_scale_assoc_secondtarget. ub = ff_q_pfp_scale_assoc_secondtarget * S ((S (pfp_index_scale_assoc_second)) * uc) + (pfp_value_scale_assoc_second))) /\ ((((exists pfa_gap_scale_assoc_secondoperationleft. pfa_gap_scale_assoc_secondoperationleft + S (a) = (p)) /\ (((exists pfa_gap_scale_assoc_secondoperationright. pfa_gap_scale_assoc_secondoperationright + S (pfp_source_scale_assoc_second) = (p)) /\ ((((exists pfa_gap_scale_assoc_secondoperationresultbound. pfa_gap_scale_assoc_secondoperationresultbound + S (pfp_value_scale_assoc_second) = (p)) /\ ((exists pfa_offset_left_scale_assoc_secondoperationresultcongruence pfa_offset_right_scale_assoc_secondoperationresultcongruence. ((a) * (pfp_source_scale_assoc_second)) + (p) * pfa_offset_left_scale_assoc_secondoperationresultcongruence = (pfp_value_scale_assoc_second) + (p) * pfa_offset_right_scale_assoc_secondoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scale_assoc_productscalar. pfa_gap_scale_assoc_productscalar + S (k) = (p)) /\ ((forall pfp_index_scale_assoc_product. (exists pfa_gap_scale_assoc_productindex. pfa_gap_scale_assoc_productindex + S (pfp_index_scale_assoc_product) = (l)) -> exists pfp_source_scale_assoc_product pfp_value_scale_assoc_product. ((((exists ff_h_pfp_scale_assoc_productsource. ff_h_pfp_scale_assoc_productsource + S (pfp_source_scale_assoc_product) = S ((S (pfp_index_scale_assoc_product)) * ac)) /\ exists ff_q_pfp_scale_assoc_productsource. ab = ff_q_pfp_scale_assoc_productsource * S ((S (pfp_index_scale_assoc_product)) * ac) + (pfp_source_scale_assoc_product))) /\ (((((exists ff_h_pfp_scale_assoc_producttarget. ff_h_pfp_scale_assoc_producttarget + S (pfp_value_scale_assoc_product) = S ((S (pfp_index_scale_assoc_product)) * vc)) /\ exists ff_q_pfp_scale_assoc_producttarget. vb = ff_q_pfp_scale_assoc_producttarget * S ((S (pfp_index_scale_assoc_product)) * vc) + (pfp_value_scale_assoc_product))) /\ ((((exists pfa_gap_scale_assoc_productoperationleft. pfa_gap_scale_assoc_productoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scale_assoc_productoperationright. pfa_gap_scale_assoc_productoperationright + S (pfp_source_scale_assoc_product) = (p)) /\ ((((exists pfa_gap_scale_assoc_productoperationresultbound. pfa_gap_scale_assoc_productoperationresultbound + S (pfp_value_scale_assoc_product) = (p)) /\ ((exists pfa_offset_left_scale_assoc_productoperationresultcongruence pfa_offset_right_scale_assoc_productoperationresultcongruence. ((k) * (pfp_source_scale_assoc_product)) + (p) * pfa_offset_left_scale_assoc_productoperationresultcongruence = (pfp_value_scale_assoc_product) + (p) * pfa_offset_right_scale_assoc_productoperationresultcongruence))))))))))))))))) -> (forall mdr_i_pfp_scale_assoc_result mdr_a_pfp_scale_assoc_result. (exists mdr_gap_pfp_scale_assoc_resultb. mdr_gap_pfp_scale_assoc_resultb + S (mdr_i_pfp_scale_assoc_result) = (l)) -> (((exists ff_h_mdr_pfp_scale_assoc_resulto. ff_h_mdr_pfp_scale_assoc_resulto + S (mdr_a_pfp_scale_assoc_result) = S ((S (mdr_i_pfp_scale_assoc_result)) * uc)) /\ exists ff_q_mdr_pfp_scale_assoc_resulto. ub = ff_q_mdr_pfp_scale_assoc_resulto * S ((S (mdr_i_pfp_scale_assoc_result)) * uc) + (mdr_a_pfp_scale_assoc_result))) -> (((exists ff_h_mdr_pfp_scale_assoc_resultn. ff_h_mdr_pfp_scale_assoc_resultn + S (mdr_a_pfp_scale_assoc_result) = S ((S (mdr_i_pfp_scale_assoc_result)) * vc)) /\ exists ff_q_mdr_pfp_scale_assoc_resultn. vb = ff_q_mdr_pfp_scale_assoc_resultn * S ((S (mdr_i_pfp_scale_assoc_result)) * vc) + (mdr_a_pfp_scale_assoc_result))))

Complete tactic proof in conservative notation

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

99 script commands · 17 reading checkpoints · 4 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 scale entry
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro k
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro ub
  10. L10
    intro uc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro vb
  2. L12
    intro vc
  3. L13
    intro l
  4. L14
    intro hk
  5. L15
    intro hfirst
  6. L16
    intro hsecond
  7. L17
    intro hproduct
  8. L18
    intro i
  9. L19
    intro r
  10. L20
    intro hi
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hr
04Establish entry_aL22–26

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

  1. L22
    have entry_a : ∃ z. BetaAt(ab,ac,i,z)Definitions: BetaAt(ab,ac,i,z)Original native command in the exact edition
  2. L23
    specialize beta_at_exists (ab)
  3. L24
    specialize beta_at_exists (ac)
  4. L25
    specialize beta_at_exists (i)
  5. L26
    apply beta_at_exists
05Separate the logical casesL27–27

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

  1. L27
    cases entry_a
06Establish entry_bL28–32

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

  1. L28
    have entry_b : ∃ z. BetaAt(bb,bc,i,z)Definitions: BetaAt(bb,bc,i,z)Original native command in the exact edition
  2. L29
    specialize beta_at_exists (bb)
  3. L30
    specialize beta_at_exists (bc)
  4. L31
    specialize beta_at_exists (i)
  5. L32
    apply beta_at_exists
07Separate the logical casesL33–33

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

  1. L33
    cases entry_b
08Establish entry_vL34–38

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

  1. L34
    have entry_v : ∃ z. BetaAt(vb,vc,i,z)Definitions: BetaAt(vb,vc,i,z)Original native command in the exact edition
  2. L35
    specialize beta_at_exists (vb)
  3. L36
    specialize beta_at_exists (vc)
  4. L37
    specialize beta_at_exists (i)
  5. L38
    apply beta_at_exists
09Separate the logical casesL39–39

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

  1. L39
    cases entry_v
10Establish heqL40–49

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

  1. L40
    have heq : r=x2
  2. L41
    symm
  3. L42
    specialize prime_field_multiply_associative (p)
  4. L43
    specialize prime_field_multiply_associative (a)
  5. L44
    specialize prime_field_multiply_associative (b)
  6. L45
    specialize prime_field_multiply_associative (x)
  7. L46
    specialize prime_field_multiply_associative (k)
  8. L47
    specialize prime_field_multiply_associative (x1)
  9. L48
    specialize prime_field_multiply_associative (x2)
  10. L49
    specialize prime_field_multiply_associative (r)
11Use earlier factsL50–59

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

  1. L50
    apply prime_field_multiply_associative
  2. L51
    exact hk
  3. L52
    specialize prime_field_polynomial_scale_entry (p)
  4. L53
    specialize prime_field_polynomial_scale_entry (k)
  5. L54
    specialize prime_field_polynomial_scale_entry (ab)
  6. L55
    specialize prime_field_polynomial_scale_entry (ac)
  7. L56
    specialize prime_field_polynomial_scale_entry (vb)
  8. L57
    specialize prime_field_polynomial_scale_entry (vc)
  9. L58
    specialize prime_field_polynomial_scale_entry (l)
  10. L59
    specialize prime_field_polynomial_scale_entry (i)
12Use earlier factsL60–69

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

  1. L60
    specialize prime_field_polynomial_scale_entry (x)
  2. L61
    specialize prime_field_polynomial_scale_entry (x2)
  3. L62
    apply prime_field_polynomial_scale_entry
  4. L63
    exact hproduct
  5. L64
    exact hi
  6. L65
    exact entry_a_witness
  7. L66
    exact entry_v_witness
  8. L67
    specialize prime_field_polynomial_scale_entry (p)
  9. L68
    specialize prime_field_polynomial_scale_entry (b)
  10. L69
    specialize prime_field_polynomial_scale_entry (ab)
13Use earlier factsL70–79

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

  1. L70
    specialize prime_field_polynomial_scale_entry (ac)
  2. L71
    specialize prime_field_polynomial_scale_entry (bb)
  3. L72
    specialize prime_field_polynomial_scale_entry (bc)
  4. L73
    specialize prime_field_polynomial_scale_entry (l)
  5. L74
    specialize prime_field_polynomial_scale_entry (i)
  6. L75
    specialize prime_field_polynomial_scale_entry (x)
  7. L76
    specialize prime_field_polynomial_scale_entry (x1)
  8. L77
    apply prime_field_polynomial_scale_entry
  9. L78
    exact hfirst
  10. L79
    exact hi
14Use earlier factsL80–89

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

  1. L80
    exact entry_a_witness
  2. L81
    exact entry_b_witness
  3. L82
    specialize prime_field_polynomial_scale_entry (p)
  4. L83
    specialize prime_field_polynomial_scale_entry (a)
  5. L84
    specialize prime_field_polynomial_scale_entry (bb)
  6. L85
    specialize prime_field_polynomial_scale_entry (bc)
  7. L86
    specialize prime_field_polynomial_scale_entry (ub)
  8. L87
    specialize prime_field_polynomial_scale_entry (uc)
  9. L88
    specialize prime_field_polynomial_scale_entry (l)
  10. L89
    specialize prime_field_polynomial_scale_entry (i)
15Use earlier factsL90–96

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

  1. L90
    specialize prime_field_polynomial_scale_entry (x1)
  2. L91
    specialize prime_field_polynomial_scale_entry (r)
  3. L92
    apply prime_field_polynomial_scale_entry
  4. L93
    exact hsecond
  5. L94
    exact hi
  6. L95
    exact entry_b_witness
  7. L96
    exact hr
16Calculate and transport equalitiesL97–98

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

  1. L97
    rewrite heq
  2. L98
    rewrite heq
17Use earlier factsL99–99

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

  1. L99
    exact entry_v_witness

Library-wide reading audit

Original defined command ledger · 99 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro k
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro ub
  10. 0010intro uc
  11. 0011intro vb
  12. 0012intro vc
  13. 0013intro l
  14. 0014intro hk
  15. 0015intro hfirst
  16. 0016intro hsecond
  17. 0017intro hproduct
  18. 0018intro i
  19. 0019intro r
  20. 0020intro hi
  21. 0021intro hr
  22. 0022have entry_a : ∃ z. BetaAt(ab,ac,i,z)
  23. 0023specialize beta_at_exists (ab)
  24. 0024specialize beta_at_exists (ac)
  25. 0025specialize beta_at_exists (i)
  26. 0026apply beta_at_exists
  27. 0027cases entry_a
  28. 0028have entry_b : ∃ z. BetaAt(bb,bc,i,z)
  29. 0029specialize beta_at_exists (bb)
  30. 0030specialize beta_at_exists (bc)
  31. 0031specialize beta_at_exists (i)
  32. 0032apply beta_at_exists
  33. 0033cases entry_b
  34. 0034have entry_v : ∃ z. BetaAt(vb,vc,i,z)
  35. 0035specialize beta_at_exists (vb)
  36. 0036specialize beta_at_exists (vc)
  37. 0037specialize beta_at_exists (i)
  38. 0038apply beta_at_exists
  39. 0039cases entry_v
  40. 0040have heq : r=x2
  41. 0041symm
  42. 0042specialize prime_field_multiply_associative (p)
  43. 0043specialize prime_field_multiply_associative (a)
  44. 0044specialize prime_field_multiply_associative (b)
  45. 0045specialize prime_field_multiply_associative (x)
  46. 0046specialize prime_field_multiply_associative (k)
  47. 0047specialize prime_field_multiply_associative (x1)
  48. 0048specialize prime_field_multiply_associative (x2)
  49. 0049specialize prime_field_multiply_associative (r)
  50. 0050apply prime_field_multiply_associative
  51. 0051exact hk
  52. 0052specialize prime_field_polynomial_scale_entry (p)
  53. 0053specialize prime_field_polynomial_scale_entry (k)
  54. 0054specialize prime_field_polynomial_scale_entry (ab)
  55. 0055specialize prime_field_polynomial_scale_entry (ac)
  56. 0056specialize prime_field_polynomial_scale_entry (vb)
  57. 0057specialize prime_field_polynomial_scale_entry (vc)
  58. 0058specialize prime_field_polynomial_scale_entry (l)
  59. 0059specialize prime_field_polynomial_scale_entry (i)
  60. 0060specialize prime_field_polynomial_scale_entry (x)
  61. 0061specialize prime_field_polynomial_scale_entry (x2)
  62. 0062apply prime_field_polynomial_scale_entry
  63. 0063exact hproduct
  64. 0064exact hi
  65. 0065exact entry_a_witness
  66. 0066exact entry_v_witness
  67. 0067specialize prime_field_polynomial_scale_entry (p)
  68. 0068specialize prime_field_polynomial_scale_entry (b)
  69. 0069specialize prime_field_polynomial_scale_entry (ab)
  70. 0070specialize prime_field_polynomial_scale_entry (ac)
  71. 0071specialize prime_field_polynomial_scale_entry (bb)
  72. 0072specialize prime_field_polynomial_scale_entry (bc)
  73. 0073specialize prime_field_polynomial_scale_entry (l)
  74. 0074specialize prime_field_polynomial_scale_entry (i)
  75. 0075specialize prime_field_polynomial_scale_entry (x)
  76. 0076specialize prime_field_polynomial_scale_entry (x1)
  77. 0077apply prime_field_polynomial_scale_entry
  78. 0078exact hfirst
  79. 0079exact hi
  80. 0080exact entry_a_witness
  81. 0081exact entry_b_witness
  82. 0082specialize prime_field_polynomial_scale_entry (p)
  83. 0083specialize prime_field_polynomial_scale_entry (a)
  84. 0084specialize prime_field_polynomial_scale_entry (bb)
  85. 0085specialize prime_field_polynomial_scale_entry (bc)
  86. 0086specialize prime_field_polynomial_scale_entry (ub)
  87. 0087specialize prime_field_polynomial_scale_entry (uc)
  88. 0088specialize prime_field_polynomial_scale_entry (l)
  89. 0089specialize prime_field_polynomial_scale_entry (i)
  90. 0090specialize prime_field_polynomial_scale_entry (x1)
  91. 0091specialize prime_field_polynomial_scale_entry (r)
  92. 0092apply prime_field_polynomial_scale_entry
  93. 0093exact hsecond
  94. 0094exact hi
  95. 0095exact entry_b_witness
  96. 0096exact hr
  97. 0097rewrite heq
  98. 0098rewrite heq
  99. 0099exact entry_v_witness