PP001F

prime_field_polynomial_scalar_add_distributes

Acting by an actual sum of scalars agrees with adding their separately constructed coefficient actions.

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. ∀ xb. ∀ xc. ∀ yb. ∀ yc. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ l. FpAdd(p,a,b,k) → FpPolyScale(p,k,ab,ac,ub,uc,l) → FpPolyScale(p,a,ab,ac,xb,xc,l) → FpPolyScale(p,b,ab,ac,yb,yc,l) → FpPolyAdd(p,xb,xc,yb,yc,vb,vc,l) → BetaPrefixEqual(ub,uc,vb,vc,l)

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

Definition DAG

FpAdd(p,a,b,c) · 1BetaPrefixEqual(b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 1FpPolyScale(p,k,ab,ac,bb,bc,l) · 3BetaAt(b,c,i,x) · 4

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_right_distributive · checked external prerequisiteprime_field_polynomial_scale_entryprime_field_polynomial_add_entry
Original expanded first-order statement 
forall p a b k ab ac xb xc yb yc ub uc vb vc l. (((exists pfa_gap_scalar_distribute_sumleft. pfa_gap_scalar_distribute_sumleft + S (a) = (p)) /\ (((exists pfa_gap_scalar_distribute_sumright. pfa_gap_scalar_distribute_sumright + S (b) = (p)) /\ ((((exists pfa_gap_scalar_distribute_sumresultbound. pfa_gap_scalar_distribute_sumresultbound + S (k) = (p)) /\ ((exists pfa_offset_left_scalar_distribute_sumresultcongruence pfa_offset_right_scalar_distribute_sumresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_scalar_distribute_sumresultcongruence = (k) + (p) * pfa_offset_right_scalar_distribute_sumresultcongruence))))))))) -> (((exists pfa_gap_scalar_distribute_leftscalar. pfa_gap_scalar_distribute_leftscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_distribute_left. (exists pfa_gap_scalar_distribute_leftindex. pfa_gap_scalar_distribute_leftindex + S (pfp_index_scalar_distribute_left) = (l)) -> exists pfp_source_scalar_distribute_left pfp_value_scalar_distribute_left. ((((exists ff_h_pfp_scalar_distribute_leftsource. ff_h_pfp_scalar_distribute_leftsource + S (pfp_source_scalar_distribute_left) = S ((S (pfp_index_scalar_distribute_left)) * ac)) /\ exists ff_q_pfp_scalar_distribute_leftsource. ab = ff_q_pfp_scalar_distribute_leftsource * S ((S (pfp_index_scalar_distribute_left)) * ac) + (pfp_source_scalar_distribute_left))) /\ (((((exists ff_h_pfp_scalar_distribute_lefttarget. ff_h_pfp_scalar_distribute_lefttarget + S (pfp_value_scalar_distribute_left) = S ((S (pfp_index_scalar_distribute_left)) * uc)) /\ exists ff_q_pfp_scalar_distribute_lefttarget. ub = ff_q_pfp_scalar_distribute_lefttarget * S ((S (pfp_index_scalar_distribute_left)) * uc) + (pfp_value_scalar_distribute_left))) /\ ((((exists pfa_gap_scalar_distribute_leftoperationleft. pfa_gap_scalar_distribute_leftoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_distribute_leftoperationright. pfa_gap_scalar_distribute_leftoperationright + S (pfp_source_scalar_distribute_left) = (p)) /\ ((((exists pfa_gap_scalar_distribute_leftoperationresultbound. pfa_gap_scalar_distribute_leftoperationresultbound + S (pfp_value_scalar_distribute_left) = (p)) /\ ((exists pfa_offset_left_scalar_distribute_leftoperationresultcongruence pfa_offset_right_scalar_distribute_leftoperationresultcongruence. ((k) * (pfp_source_scalar_distribute_left)) + (p) * pfa_offset_left_scalar_distribute_leftoperationresultcongruence = (pfp_value_scalar_distribute_left) + (p) * pfa_offset_right_scalar_distribute_leftoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scalar_distribute_ascalar. pfa_gap_scalar_distribute_ascalar + S (a) = (p)) /\ ((forall pfp_index_scalar_distribute_a. (exists pfa_gap_scalar_distribute_aindex. pfa_gap_scalar_distribute_aindex + S (pfp_index_scalar_distribute_a) = (l)) -> exists pfp_source_scalar_distribute_a pfp_value_scalar_distribute_a. ((((exists ff_h_pfp_scalar_distribute_asource. ff_h_pfp_scalar_distribute_asource + S (pfp_source_scalar_distribute_a) = S ((S (pfp_index_scalar_distribute_a)) * ac)) /\ exists ff_q_pfp_scalar_distribute_asource. ab = ff_q_pfp_scalar_distribute_asource * S ((S (pfp_index_scalar_distribute_a)) * ac) + (pfp_source_scalar_distribute_a))) /\ (((((exists ff_h_pfp_scalar_distribute_atarget. ff_h_pfp_scalar_distribute_atarget + S (pfp_value_scalar_distribute_a) = S ((S (pfp_index_scalar_distribute_a)) * xc)) /\ exists ff_q_pfp_scalar_distribute_atarget. xb = ff_q_pfp_scalar_distribute_atarget * S ((S (pfp_index_scalar_distribute_a)) * xc) + (pfp_value_scalar_distribute_a))) /\ ((((exists pfa_gap_scalar_distribute_aoperationleft. pfa_gap_scalar_distribute_aoperationleft + S (a) = (p)) /\ (((exists pfa_gap_scalar_distribute_aoperationright. pfa_gap_scalar_distribute_aoperationright + S (pfp_source_scalar_distribute_a) = (p)) /\ ((((exists pfa_gap_scalar_distribute_aoperationresultbound. pfa_gap_scalar_distribute_aoperationresultbound + S (pfp_value_scalar_distribute_a) = (p)) /\ ((exists pfa_offset_left_scalar_distribute_aoperationresultcongruence pfa_offset_right_scalar_distribute_aoperationresultcongruence. ((a) * (pfp_source_scalar_distribute_a)) + (p) * pfa_offset_left_scalar_distribute_aoperationresultcongruence = (pfp_value_scalar_distribute_a) + (p) * pfa_offset_right_scalar_distribute_aoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_scalar_distribute_bscalar. pfa_gap_scalar_distribute_bscalar + S (b) = (p)) /\ ((forall pfp_index_scalar_distribute_b. (exists pfa_gap_scalar_distribute_bindex. pfa_gap_scalar_distribute_bindex + S (pfp_index_scalar_distribute_b) = (l)) -> exists pfp_source_scalar_distribute_b pfp_value_scalar_distribute_b. ((((exists ff_h_pfp_scalar_distribute_bsource. ff_h_pfp_scalar_distribute_bsource + S (pfp_source_scalar_distribute_b) = S ((S (pfp_index_scalar_distribute_b)) * ac)) /\ exists ff_q_pfp_scalar_distribute_bsource. ab = ff_q_pfp_scalar_distribute_bsource * S ((S (pfp_index_scalar_distribute_b)) * ac) + (pfp_source_scalar_distribute_b))) /\ (((((exists ff_h_pfp_scalar_distribute_btarget. ff_h_pfp_scalar_distribute_btarget + S (pfp_value_scalar_distribute_b) = S ((S (pfp_index_scalar_distribute_b)) * yc)) /\ exists ff_q_pfp_scalar_distribute_btarget. yb = ff_q_pfp_scalar_distribute_btarget * S ((S (pfp_index_scalar_distribute_b)) * yc) + (pfp_value_scalar_distribute_b))) /\ ((((exists pfa_gap_scalar_distribute_boperationleft. pfa_gap_scalar_distribute_boperationleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_distribute_boperationright. pfa_gap_scalar_distribute_boperationright + S (pfp_source_scalar_distribute_b) = (p)) /\ ((((exists pfa_gap_scalar_distribute_boperationresultbound. pfa_gap_scalar_distribute_boperationresultbound + S (pfp_value_scalar_distribute_b) = (p)) /\ ((exists pfa_offset_left_scalar_distribute_boperationresultcongruence pfa_offset_right_scalar_distribute_boperationresultcongruence. ((b) * (pfp_source_scalar_distribute_b)) + (p) * pfa_offset_left_scalar_distribute_boperationresultcongruence = (pfp_value_scalar_distribute_b) + (p) * pfa_offset_right_scalar_distribute_boperationresultcongruence))))))))))))))))) -> (forall pfp_index_scalar_distribute_right. (exists pfa_gap_scalar_distribute_rightindex. pfa_gap_scalar_distribute_rightindex + S (pfp_index_scalar_distribute_right) = (l)) -> exists pfp_left_scalar_distribute_right pfp_right_scalar_distribute_right pfp_value_scalar_distribute_right. ((((exists ff_h_pfp_scalar_distribute_rightleft. ff_h_pfp_scalar_distribute_rightleft + S (pfp_left_scalar_distribute_right) = S ((S (pfp_index_scalar_distribute_right)) * xc)) /\ exists ff_q_pfp_scalar_distribute_rightleft. xb = ff_q_pfp_scalar_distribute_rightleft * S ((S (pfp_index_scalar_distribute_right)) * xc) + (pfp_left_scalar_distribute_right))) /\ (((((exists ff_h_pfp_scalar_distribute_rightright. ff_h_pfp_scalar_distribute_rightright + S (pfp_right_scalar_distribute_right) = S ((S (pfp_index_scalar_distribute_right)) * yc)) /\ exists ff_q_pfp_scalar_distribute_rightright. yb = ff_q_pfp_scalar_distribute_rightright * S ((S (pfp_index_scalar_distribute_right)) * yc) + (pfp_right_scalar_distribute_right))) /\ (((((exists ff_h_pfp_scalar_distribute_righttarget. ff_h_pfp_scalar_distribute_righttarget + S (pfp_value_scalar_distribute_right) = S ((S (pfp_index_scalar_distribute_right)) * vc)) /\ exists ff_q_pfp_scalar_distribute_righttarget. vb = ff_q_pfp_scalar_distribute_righttarget * S ((S (pfp_index_scalar_distribute_right)) * vc) + (pfp_value_scalar_distribute_right))) /\ ((((exists pfa_gap_scalar_distribute_rightoperationleft. pfa_gap_scalar_distribute_rightoperationleft + S (pfp_left_scalar_distribute_right) = (p)) /\ (((exists pfa_gap_scalar_distribute_rightoperationright. pfa_gap_scalar_distribute_rightoperationright + S (pfp_right_scalar_distribute_right) = (p)) /\ ((((exists pfa_gap_scalar_distribute_rightoperationresultbound. pfa_gap_scalar_distribute_rightoperationresultbound + S (pfp_value_scalar_distribute_right) = (p)) /\ ((exists pfa_offset_left_scalar_distribute_rightoperationresultcongruence pfa_offset_right_scalar_distribute_rightoperationresultcongruence. ((pfp_left_scalar_distribute_right) + (pfp_right_scalar_distribute_right)) + (p) * pfa_offset_left_scalar_distribute_rightoperationresultcongruence = (pfp_value_scalar_distribute_right) + (p) * pfa_offset_right_scalar_distribute_rightoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_scalar_distribute_result mdr_a_pfp_scalar_distribute_result. (exists mdr_gap_pfp_scalar_distribute_resultb. mdr_gap_pfp_scalar_distribute_resultb + S (mdr_i_pfp_scalar_distribute_result) = (l)) -> (((exists ff_h_mdr_pfp_scalar_distribute_resulto. ff_h_mdr_pfp_scalar_distribute_resulto + S (mdr_a_pfp_scalar_distribute_result) = S ((S (mdr_i_pfp_scalar_distribute_result)) * uc)) /\ exists ff_q_mdr_pfp_scalar_distribute_resulto. ub = ff_q_mdr_pfp_scalar_distribute_resulto * S ((S (mdr_i_pfp_scalar_distribute_result)) * uc) + (mdr_a_pfp_scalar_distribute_result))) -> (((exists ff_h_mdr_pfp_scalar_distribute_resultn. ff_h_mdr_pfp_scalar_distribute_resultn + S (mdr_a_pfp_scalar_distribute_result) = S ((S (mdr_i_pfp_scalar_distribute_result)) * vc)) /\ exists ff_q_mdr_pfp_scalar_distribute_resultn. vb = ff_q_mdr_pfp_scalar_distribute_resultn * S ((S (mdr_i_pfp_scalar_distribute_result)) * vc) + (mdr_a_pfp_scalar_distribute_result))))

Complete tactic proof in conservative notation

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

126 script commands · 21 reading checkpoints · 5 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 scale entryprime field polynomial add 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 xb
  8. L8
    intro xc
  9. L9
    intro yb
  10. L10
    intro yc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro ub
  2. L12
    intro uc
  3. L13
    intro vb
  4. L14
    intro vc
  5. L15
    intro l
  6. L16
    intro hsum
  7. L17
    intro hleft
  8. L18
    intro hfirst
  9. L19
    intro hsecond
  10. L20
    intro hright
03Fix variables and assumptionsL21–24

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

  1. L21
    intro i
  2. L22
    intro r
  3. L23
    intro hi
  4. L24
    intro hr
04Establish entry_aL25–29

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

  1. L25
    have entry_a : ∃ z. BetaAt(ab,ac,i,z)Definitions: BetaAt(ab,ac,i,z)Original native command in the exact edition
  2. L26
    specialize beta_at_exists (ab)
  3. L27
    specialize beta_at_exists (ac)
  4. L28
    specialize beta_at_exists (i)
  5. L29
    apply beta_at_exists
05Separate the logical casesL30–30

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

  1. L30
    cases entry_a
06Establish entry_xL31–35

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

  1. L31
    have entry_x : ∃ z. BetaAt(xb,xc,i,z)Definitions: BetaAt(xb,xc,i,z)Original native command in the exact edition
  2. L32
    specialize beta_at_exists (xb)
  3. L33
    specialize beta_at_exists (xc)
  4. L34
    specialize beta_at_exists (i)
  5. L35
    apply beta_at_exists
07Separate the logical casesL36–36

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

  1. L36
    cases entry_x
08Establish entry_yL37–41

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

  1. L37
    have entry_y : ∃ z. BetaAt(yb,yc,i,z)Definitions: BetaAt(yb,yc,i,z)Original native command in the exact edition
  2. L38
    specialize beta_at_exists (yb)
  3. L39
    specialize beta_at_exists (yc)
  4. L40
    specialize beta_at_exists (i)
  5. L41
    apply beta_at_exists
09Separate the logical casesL42–42

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

  1. L42
    cases entry_y
10Establish entry_vL43–47

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

  1. L43
    have entry_v : ∃ z. BetaAt(vb,vc,i,z)Definitions: BetaAt(vb,vc,i,z)Original native command in the exact edition
  2. L44
    specialize beta_at_exists (vb)
  3. L45
    specialize beta_at_exists (vc)
  4. L46
    specialize beta_at_exists (i)
  5. L47
    apply beta_at_exists
11Separate the logical casesL48–48

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

  1. L48
    cases entry_v
12Establish heqL49–58

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

  1. L49
    have heq : r=x3
  2. L50
    specialize prime_field_right_distributive (p)
  3. L51
    specialize prime_field_right_distributive (x)
  4. L52
    specialize prime_field_right_distributive (a)
  5. L53
    specialize prime_field_right_distributive (b)
  6. L54
    specialize prime_field_right_distributive (k)
  7. L55
    specialize prime_field_right_distributive (x1)
  8. L56
    specialize prime_field_right_distributive (x2)
  9. L57
    specialize prime_field_right_distributive (r)
  10. L58
    specialize prime_field_right_distributive (x3)
13Use earlier factsL59–68

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

  1. L59
    apply prime_field_right_distributive
  2. L60
    exact hsum
  3. L61
    specialize prime_field_polynomial_scale_entry (p)
  4. L62
    specialize prime_field_polynomial_scale_entry (k)
  5. L63
    specialize prime_field_polynomial_scale_entry (ab)
  6. L64
    specialize prime_field_polynomial_scale_entry (ac)
  7. L65
    specialize prime_field_polynomial_scale_entry (ub)
  8. L66
    specialize prime_field_polynomial_scale_entry (uc)
  9. L67
    specialize prime_field_polynomial_scale_entry (l)
  10. L68
    specialize prime_field_polynomial_scale_entry (i)
14Use earlier factsL69–78

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

  1. L69
    specialize prime_field_polynomial_scale_entry (x)
  2. L70
    specialize prime_field_polynomial_scale_entry (r)
  3. L71
    apply prime_field_polynomial_scale_entry
  4. L72
    exact hleft
  5. L73
    exact hi
  6. L74
    exact entry_a_witness
  7. L75
    exact hr
  8. L76
    specialize prime_field_polynomial_scale_entry (p)
  9. L77
    specialize prime_field_polynomial_scale_entry (a)
  10. L78
    specialize prime_field_polynomial_scale_entry (ab)
15Use earlier factsL79–88

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

  1. L79
    specialize prime_field_polynomial_scale_entry (ac)
  2. L80
    specialize prime_field_polynomial_scale_entry (xb)
  3. L81
    specialize prime_field_polynomial_scale_entry (xc)
  4. L82
    specialize prime_field_polynomial_scale_entry (l)
  5. L83
    specialize prime_field_polynomial_scale_entry (i)
  6. L84
    specialize prime_field_polynomial_scale_entry (x)
  7. L85
    specialize prime_field_polynomial_scale_entry (x1)
  8. L86
    apply prime_field_polynomial_scale_entry
  9. L87
    exact hfirst
  10. L88
    exact hi
16Use earlier factsL89–98

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

  1. L89
    exact entry_a_witness
  2. L90
    exact entry_x_witness
  3. L91
    specialize prime_field_polynomial_scale_entry (p)
  4. L92
    specialize prime_field_polynomial_scale_entry (b)
  5. L93
    specialize prime_field_polynomial_scale_entry (ab)
  6. L94
    specialize prime_field_polynomial_scale_entry (ac)
  7. L95
    specialize prime_field_polynomial_scale_entry (yb)
  8. L96
    specialize prime_field_polynomial_scale_entry (yc)
  9. L97
    specialize prime_field_polynomial_scale_entry (l)
  10. L98
    specialize prime_field_polynomial_scale_entry (i)
17Use earlier factsL99–108

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

  1. L99
    specialize prime_field_polynomial_scale_entry (x)
  2. L100
    specialize prime_field_polynomial_scale_entry (x2)
  3. L101
    apply prime_field_polynomial_scale_entry
  4. L102
    exact hsecond
  5. L103
    exact hi
  6. L104
    exact entry_a_witness
  7. L105
    exact entry_y_witness
  8. L106
    specialize prime_field_polynomial_add_entry (p)
  9. L107
    specialize prime_field_polynomial_add_entry (xb)
  10. L108
    specialize prime_field_polynomial_add_entry (xc)
18Use earlier factsL109–118

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

  1. L109
    specialize prime_field_polynomial_add_entry (yb)
  2. L110
    specialize prime_field_polynomial_add_entry (yc)
  3. L111
    specialize prime_field_polynomial_add_entry (vb)
  4. L112
    specialize prime_field_polynomial_add_entry (vc)
  5. L113
    specialize prime_field_polynomial_add_entry (l)
  6. L114
    specialize prime_field_polynomial_add_entry (i)
  7. L115
    specialize prime_field_polynomial_add_entry (x1)
  8. L116
    specialize prime_field_polynomial_add_entry (x2)
  9. L117
    specialize prime_field_polynomial_add_entry (x3)
  10. L118
    apply prime_field_polynomial_add_entry
19Use earlier factsL119–123

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

  1. L119
    exact hright
  2. L120
    exact hi
  3. L121
    exact entry_x_witness
  4. L122
    exact entry_y_witness
  5. L123
    exact entry_v_witness
20Calculate and transport equalitiesL124–125

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

  1. L124
    rewrite heq
  2. L125
    rewrite heq
21Use earlier factsL126–126

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

  1. L126
    exact entry_v_witness

Library-wide reading audit

Original defined command ledger · 126 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro k
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro xb
  8. 0008intro xc
  9. 0009intro yb
  10. 0010intro yc
  11. 0011intro ub
  12. 0012intro uc
  13. 0013intro vb
  14. 0014intro vc
  15. 0015intro l
  16. 0016intro hsum
  17. 0017intro hleft
  18. 0018intro hfirst
  19. 0019intro hsecond
  20. 0020intro hright
  21. 0021intro i
  22. 0022intro r
  23. 0023intro hi
  24. 0024intro hr
  25. 0025have entry_a : ∃ z. BetaAt(ab,ac,i,z)
  26. 0026specialize beta_at_exists (ab)
  27. 0027specialize beta_at_exists (ac)
  28. 0028specialize beta_at_exists (i)
  29. 0029apply beta_at_exists
  30. 0030cases entry_a
  31. 0031have entry_x : ∃ z. BetaAt(xb,xc,i,z)
  32. 0032specialize beta_at_exists (xb)
  33. 0033specialize beta_at_exists (xc)
  34. 0034specialize beta_at_exists (i)
  35. 0035apply beta_at_exists
  36. 0036cases entry_x
  37. 0037have entry_y : ∃ z. BetaAt(yb,yc,i,z)
  38. 0038specialize beta_at_exists (yb)
  39. 0039specialize beta_at_exists (yc)
  40. 0040specialize beta_at_exists (i)
  41. 0041apply beta_at_exists
  42. 0042cases entry_y
  43. 0043have entry_v : ∃ z. BetaAt(vb,vc,i,z)
  44. 0044specialize beta_at_exists (vb)
  45. 0045specialize beta_at_exists (vc)
  46. 0046specialize beta_at_exists (i)
  47. 0047apply beta_at_exists
  48. 0048cases entry_v
  49. 0049have heq : r=x3
  50. 0050specialize prime_field_right_distributive (p)
  51. 0051specialize prime_field_right_distributive (x)
  52. 0052specialize prime_field_right_distributive (a)
  53. 0053specialize prime_field_right_distributive (b)
  54. 0054specialize prime_field_right_distributive (k)
  55. 0055specialize prime_field_right_distributive (x1)
  56. 0056specialize prime_field_right_distributive (x2)
  57. 0057specialize prime_field_right_distributive (r)
  58. 0058specialize prime_field_right_distributive (x3)
  59. 0059apply prime_field_right_distributive
  60. 0060exact hsum
  61. 0061specialize prime_field_polynomial_scale_entry (p)
  62. 0062specialize prime_field_polynomial_scale_entry (k)
  63. 0063specialize prime_field_polynomial_scale_entry (ab)
  64. 0064specialize prime_field_polynomial_scale_entry (ac)
  65. 0065specialize prime_field_polynomial_scale_entry (ub)
  66. 0066specialize prime_field_polynomial_scale_entry (uc)
  67. 0067specialize prime_field_polynomial_scale_entry (l)
  68. 0068specialize prime_field_polynomial_scale_entry (i)
  69. 0069specialize prime_field_polynomial_scale_entry (x)
  70. 0070specialize prime_field_polynomial_scale_entry (r)
  71. 0071apply prime_field_polynomial_scale_entry
  72. 0072exact hleft
  73. 0073exact hi
  74. 0074exact entry_a_witness
  75. 0075exact hr
  76. 0076specialize prime_field_polynomial_scale_entry (p)
  77. 0077specialize prime_field_polynomial_scale_entry (a)
  78. 0078specialize prime_field_polynomial_scale_entry (ab)
  79. 0079specialize prime_field_polynomial_scale_entry (ac)
  80. 0080specialize prime_field_polynomial_scale_entry (xb)
  81. 0081specialize prime_field_polynomial_scale_entry (xc)
  82. 0082specialize prime_field_polynomial_scale_entry (l)
  83. 0083specialize prime_field_polynomial_scale_entry (i)
  84. 0084specialize prime_field_polynomial_scale_entry (x)
  85. 0085specialize prime_field_polynomial_scale_entry (x1)
  86. 0086apply prime_field_polynomial_scale_entry
  87. 0087exact hfirst
  88. 0088exact hi
  89. 0089exact entry_a_witness
  90. 0090exact entry_x_witness
  91. 0091specialize prime_field_polynomial_scale_entry (p)
  92. 0092specialize prime_field_polynomial_scale_entry (b)
  93. 0093specialize prime_field_polynomial_scale_entry (ab)
  94. 0094specialize prime_field_polynomial_scale_entry (ac)
  95. 0095specialize prime_field_polynomial_scale_entry (yb)
  96. 0096specialize prime_field_polynomial_scale_entry (yc)
  97. 0097specialize prime_field_polynomial_scale_entry (l)
  98. 0098specialize prime_field_polynomial_scale_entry (i)
  99. 0099specialize prime_field_polynomial_scale_entry (x)
  100. 0100specialize prime_field_polynomial_scale_entry (x2)
  101. 0101apply prime_field_polynomial_scale_entry
  102. 0102exact hsecond
  103. 0103exact hi
  104. 0104exact entry_a_witness
  105. 0105exact entry_y_witness
  106. 0106specialize prime_field_polynomial_add_entry (p)
  107. 0107specialize prime_field_polynomial_add_entry (xb)
  108. 0108specialize prime_field_polynomial_add_entry (xc)
  109. 0109specialize prime_field_polynomial_add_entry (yb)
  110. 0110specialize prime_field_polynomial_add_entry (yc)
  111. 0111specialize prime_field_polynomial_add_entry (vb)
  112. 0112specialize prime_field_polynomial_add_entry (vc)
  113. 0113specialize prime_field_polynomial_add_entry (l)
  114. 0114specialize prime_field_polynomial_add_entry (i)
  115. 0115specialize prime_field_polynomial_add_entry (x1)
  116. 0116specialize prime_field_polynomial_add_entry (x2)
  117. 0117specialize prime_field_polynomial_add_entry (x3)
  118. 0118apply prime_field_polynomial_add_entry
  119. 0119exact hright
  120. 0120exact hi
  121. 0121exact entry_x_witness
  122. 0122exact entry_y_witness
  123. 0123exact entry_v_witness
  124. 0124rewrite heq
  125. 0125rewrite heq
  126. 0126exact entry_v_witness