PX0026

prime_field_polynomial_inverse_scale

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

An actual inverse scalar gives the reverse coefficient action, with a constructed intermediate table and exact decoded transport; no unit-associate law is assumed.

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 a k ab ac bb bc L. (~((p) = 1) /\ forall pfa_factor_left_inverse_scale_prime pfa_factor_right_inverse_scale_prime. (p) = pfa_factor_left_inverse_scale_prime * pfa_factor_right_inverse_scale_prime -> pfa_factor_left_inverse_scale_prime = 1 \/ pfa_factor_right_inverse_scale_prime = 1) -> (((~((a) = 0)) /\ ((((exists pfa_gap_inverse_scale_inversemultiplicationleft. pfa_gap_inverse_scale_inversemultiplicationleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_inversemultiplicationright. pfa_gap_inverse_scale_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_inverse_scale_inversemultiplicationresultbound. pfa_gap_inverse_scale_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverse_scale_inversemultiplicationresultcongruence pfa_offset_right_inverse_scale_inversemultiplicationresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_inverse_scale_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_inverse_scale_inversemultiplicationresultcongruence)))))))))))) -> (((exists pfa_gap_inverse_scale_forwardscalar. pfa_gap_inverse_scale_forwardscalar + S (k) = (p)) /\ ((forall pfp_index_inverse_scale_forward. (exists pfa_gap_inverse_scale_forwardindex. pfa_gap_inverse_scale_forwardindex + S (pfp_index_inverse_scale_forward) = (L)) -> exists pfp_source_inverse_scale_forward pfp_value_inverse_scale_forward. ((((exists ff_h_pfp_inverse_scale_forwardsource. ff_h_pfp_inverse_scale_forwardsource + S (pfp_source_inverse_scale_forward) = S ((S (pfp_index_inverse_scale_forward)) * ac)) /\ exists ff_q_pfp_inverse_scale_forwardsource. ab = ff_q_pfp_inverse_scale_forwardsource * S ((S (pfp_index_inverse_scale_forward)) * ac) + (pfp_source_inverse_scale_forward))) /\ (((((exists ff_h_pfp_inverse_scale_forwardtarget. ff_h_pfp_inverse_scale_forwardtarget + S (pfp_value_inverse_scale_forward) = S ((S (pfp_index_inverse_scale_forward)) * bc)) /\ exists ff_q_pfp_inverse_scale_forwardtarget. bb = ff_q_pfp_inverse_scale_forwardtarget * S ((S (pfp_index_inverse_scale_forward)) * bc) + (pfp_value_inverse_scale_forward))) /\ ((((exists pfa_gap_inverse_scale_forwardoperationleft. pfa_gap_inverse_scale_forwardoperationleft + S (k) = (p)) /\ (((exists pfa_gap_inverse_scale_forwardoperationright. pfa_gap_inverse_scale_forwardoperationright + S (pfp_source_inverse_scale_forward) = (p)) /\ ((((exists pfa_gap_inverse_scale_forwardoperationresultbound. pfa_gap_inverse_scale_forwardoperationresultbound + S (pfp_value_inverse_scale_forward) = (p)) /\ ((exists pfa_offset_left_inverse_scale_forwardoperationresultcongruence pfa_offset_right_inverse_scale_forwardoperationresultcongruence. ((k) * (pfp_source_inverse_scale_forward)) + (p) * pfa_offset_left_inverse_scale_forwardoperationresultcongruence = (pfp_value_inverse_scale_forward) + (p) * pfa_offset_right_inverse_scale_forwardoperationresultcongruence))))))))))))))))) -> (((exists pfa_gap_inverse_scale_backwardscalar. pfa_gap_inverse_scale_backwardscalar + S (a) = (p)) /\ ((forall pfp_index_inverse_scale_backward. (exists pfa_gap_inverse_scale_backwardindex. pfa_gap_inverse_scale_backwardindex + S (pfp_index_inverse_scale_backward) = (L)) -> exists pfp_source_inverse_scale_backward pfp_value_inverse_scale_backward. ((((exists ff_h_pfp_inverse_scale_backwardsource. ff_h_pfp_inverse_scale_backwardsource + S (pfp_source_inverse_scale_backward) = S ((S (pfp_index_inverse_scale_backward)) * bc)) /\ exists ff_q_pfp_inverse_scale_backwardsource. bb = ff_q_pfp_inverse_scale_backwardsource * S ((S (pfp_index_inverse_scale_backward)) * bc) + (pfp_source_inverse_scale_backward))) /\ (((((exists ff_h_pfp_inverse_scale_backwardtarget. ff_h_pfp_inverse_scale_backwardtarget + S (pfp_value_inverse_scale_backward) = S ((S (pfp_index_inverse_scale_backward)) * ac)) /\ exists ff_q_pfp_inverse_scale_backwardtarget. ab = ff_q_pfp_inverse_scale_backwardtarget * S ((S (pfp_index_inverse_scale_backward)) * ac) + (pfp_value_inverse_scale_backward))) /\ ((((exists pfa_gap_inverse_scale_backwardoperationleft. pfa_gap_inverse_scale_backwardoperationleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_backwardoperationright. pfa_gap_inverse_scale_backwardoperationright + S (pfp_source_inverse_scale_backward) = (p)) /\ ((((exists pfa_gap_inverse_scale_backwardoperationresultbound. pfa_gap_inverse_scale_backwardoperationresultbound + S (pfp_value_inverse_scale_backward) = (p)) /\ ((exists pfa_offset_left_inverse_scale_backwardoperationresultcongruence pfa_offset_right_inverse_scale_backwardoperationresultcongruence. ((a) * (pfp_source_inverse_scale_backward)) + (p) * pfa_offset_left_inverse_scale_backwardoperationresultcongruence = (pfp_value_inverse_scale_backward) + (p) * pfa_offset_right_inverse_scale_backwardoperationresultcongruence)))))))))))))))))

Constructive proof overview

Generated structural guide

An actual inverse scalar gives the reverse coefficient action, with a constructed intermediate table and exact decoded transport; no unit-associate law is assumed.

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

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

Proof neighborhood

Direct dependencies

prime_field_polynomial_scale_bounded Alpha theorem; checked-use authorized prime_field_polynomial_scale_exists Alpha theorem; checked-use authorized prime_nonzero Alpha theorem; checked-use authorized prime_field_polynomial_scale_associative Alpha theorem; checked-use authorized prime_field_polynomial_scale_one Alpha theorem; checked-use authorized prime_field_polynomial_scale_transport Alpha theorem; checked-use authorized

Direct dependents

none

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

88 script commands · 15 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.

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 k
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro bb
  7. L7
    intro bc
  8. L8
    intro L
  9. L9
    intro hp
  10. L10
    intro hinv
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hs
03Establish hboundL12–21

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

  1. L12
    have hbound : BetaPrefixInto(ab,ac,L,p) ∧ BetaPrefixInto(bb,bc,L,p)Definitions: BetaPrefixInto
  2. L13
    specialize prime_field_polynomial_scale_bounded (p)
  3. L14
    specialize prime_field_polynomial_scale_bounded (k)
  4. L15
    specialize prime_field_polynomial_scale_bounded (ab)
  5. L16
    specialize prime_field_polynomial_scale_bounded (ac)
  6. L17
    specialize prime_field_polynomial_scale_bounded (bb)
  7. L18
    specialize prime_field_polynomial_scale_bounded (bc)
  8. L19
    specialize prime_field_polynomial_scale_bounded (L)
  9. L20
    apply prime_field_polynomial_scale_bounded
  10. L21
    exact hs
04Separate the logical casesL22–23

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

  1. L22
    cases hbound
  2. L23
    cases hinv
05Establish hmL24–25

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

  1. L24
    have hm : ((exists pfa_gap_inverse_scale_productleft. pfa_gap_inverse_scale_productleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_productright. pfa_gap_inverse_scale_productright + S (k) = (p)) /\ ((((exists pfa_gap_inverse_scale_productresultbound. pfa_gap_inverse_scale_productresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverse_scale_productresultcongruence pfa_offset_right_inverse_scale_productresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_inverse_scale_productresultcongruence = (1) + (p) * pfa_offset_right_inverse_scale_productresultcongruence))))))))
  2. L25
    exact hinv_right
06Separate the logical casesL26–28

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

  1. L26
    cases hinv_right
  2. L27
    cases hinv_right_right
  3. L28
    cases hinv_right_right_right
07Establish hrL29–38

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

  1. L29
    have hr : ∃ cb. ∃ cc. FpPolyScale(p,a,bb,bc,cb,cc,L)Definitions: FpPolyScale
  2. L30
    specialize prime_field_polynomial_scale_exists (p)
  3. L31
    specialize prime_field_polynomial_scale_exists (a)
  4. L32
    specialize prime_field_polynomial_scale_exists (bb)
  5. L33
    specialize prime_field_polynomial_scale_exists (bc)
  6. L34
    specialize prime_field_polynomial_scale_exists (L)
  7. L35
    apply prime_field_polynomial_scale_exists
  8. L36
    intro hpzero
  9. L37
    specialize prime_nonzero (p)
  10. L38
    apply prime_nonzero
08Use earlier factsL39–42

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

  1. L39
    exact hp
  2. L40
    exact hpzero
  3. L41
    exact hinv_right_left
  4. L42
    exact hbound_right
09Separate the logical casesL43–44

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

  1. L43
    cases hr
  2. L44
    cases hr_witness
10Establish heL45–54

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

  1. L45
    have he : BetaPrefixEqual(x,x1,ab,ac,L)Definitions: BetaPrefixEqual
  2. L46
    specialize prime_field_polynomial_scale_associative (p)
  3. L47
    specialize prime_field_polynomial_scale_associative (a)
  4. L48
    specialize prime_field_polynomial_scale_associative (k)
  5. L49
    specialize prime_field_polynomial_scale_associative (1)
  6. L50
    specialize prime_field_polynomial_scale_associative (ab)
  7. L51
    specialize prime_field_polynomial_scale_associative (ac)
  8. L52
    specialize prime_field_polynomial_scale_associative (bb)
  9. L53
    specialize prime_field_polynomial_scale_associative (bc)
  10. L54
    specialize prime_field_polynomial_scale_associative (x)
11Use earlier factsL55–64

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

  1. L55
    specialize prime_field_polynomial_scale_associative (x1)
  2. L56
    specialize prime_field_polynomial_scale_associative (ab)
  3. L57
    specialize prime_field_polynomial_scale_associative (ac)
  4. L58
    specialize prime_field_polynomial_scale_associative (L)
  5. L59
    apply prime_field_polynomial_scale_associative
  6. L60
    exact hm
  7. L61
    exact hs
  8. L62
    exact hr_witness_witness
  9. L63
    specialize prime_field_polynomial_scale_one (p)
  10. L64
    specialize prime_field_polynomial_scale_one (ab)
12Use earlier factsL65–74

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

  1. L65
    specialize prime_field_polynomial_scale_one (ac)
  2. L66
    specialize prime_field_polynomial_scale_one (L)
  3. L67
    apply prime_field_polynomial_scale_one
  4. L68
    exact hp
  5. L69
    exact hbound_left
  6. L70
    specialize prime_field_polynomial_scale_transport (p)
  7. L71
    specialize prime_field_polynomial_scale_transport (a)
  8. L72
    specialize prime_field_polynomial_scale_transport (bb)
  9. L73
    specialize prime_field_polynomial_scale_transport (bc)
  10. L74
    specialize prime_field_polynomial_scale_transport (x)
13Use earlier factsL75–81

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

  1. L75
    specialize prime_field_polynomial_scale_transport (x1)
  2. L76
    specialize prime_field_polynomial_scale_transport (bb)
  3. L77
    specialize prime_field_polynomial_scale_transport (bc)
  4. L78
    specialize prime_field_polynomial_scale_transport (ab)
  5. L79
    specialize prime_field_polynomial_scale_transport (ac)
  6. L80
    specialize prime_field_polynomial_scale_transport (L)
  7. L81
    apply prime_field_polynomial_scale_transport
14Fix variables and assumptionsL82–85

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

  1. L82
    intro i
  2. L83
    intro r
  3. L84
    intro hi
  4. L85
    intro hat
15Use earlier factsL86–88

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

  1. L86
    exact hat
  2. L87
    exact he
  3. L88
    exact hr_witness_witness

Library-wide reading audit

Original exact command ledger · 88 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro k
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro bb
  7. 0007intro bc
  8. 0008intro L
  9. 0009intro hp
  10. 0010intro hinv
  11. 0011intro hs
  12. 0012have hbound : ((forall fom_index_pfp_inverse_scale_A. (exists fom_gap_pfp_inverse_scale_A_index_bound. fom_gap_pfp_inverse_scale_A_index_bound + S (fom_index_pfp_inverse_scale_A) = L) -> exists fom_value_pfp_inverse_scale_A. ((((exists fom_beta_height_pfp_inverse_scale_A_entry. fom_beta_height_pfp_inverse_scale_A_entry + S (fom_value_pfp_inverse_scale_A) = S ((S (fom_index_pfp_inverse_scale_A)) * ac)) /\ exists fom_beta_quotient_pfp_inverse_scale_A_entry. ab = fom_beta_quotient_pfp_inverse_scale_A_entry * S ((S (fom_index_pfp_inverse_scale_A)) * ac) + (fom_value_pfp_inverse_scale_A))) /\ (exists fom_gap_pfp_inverse_scale_A_value_bound. fom_gap_pfp_inverse_scale_A_value_bound + S (fom_value_pfp_inverse_scale_A) = p))) /\ ((forall fom_index_pfp_inverse_scale_B. (exists fom_gap_pfp_inverse_scale_B_index_bound. fom_gap_pfp_inverse_scale_B_index_bound + S (fom_index_pfp_inverse_scale_B) = L) -> exists fom_value_pfp_inverse_scale_B. ((((exists fom_beta_height_pfp_inverse_scale_B_entry. fom_beta_height_pfp_inverse_scale_B_entry + S (fom_value_pfp_inverse_scale_B) = S ((S (fom_index_pfp_inverse_scale_B)) * bc)) /\ exists fom_beta_quotient_pfp_inverse_scale_B_entry. bb = fom_beta_quotient_pfp_inverse_scale_B_entry * S ((S (fom_index_pfp_inverse_scale_B)) * bc) + (fom_value_pfp_inverse_scale_B))) /\ (exists fom_gap_pfp_inverse_scale_B_value_bound. fom_gap_pfp_inverse_scale_B_value_bound + S (fom_value_pfp_inverse_scale_B) = p)))))
  13. 0013specialize prime_field_polynomial_scale_bounded (p)
  14. 0014specialize prime_field_polynomial_scale_bounded (k)
  15. 0015specialize prime_field_polynomial_scale_bounded (ab)
  16. 0016specialize prime_field_polynomial_scale_bounded (ac)
  17. 0017specialize prime_field_polynomial_scale_bounded (bb)
  18. 0018specialize prime_field_polynomial_scale_bounded (bc)
  19. 0019specialize prime_field_polynomial_scale_bounded (L)
  20. 0020apply prime_field_polynomial_scale_bounded
  21. 0021exact hs
  22. 0022cases hbound
  23. 0023cases hinv
  24. 0024have hm : ((exists pfa_gap_inverse_scale_productleft. pfa_gap_inverse_scale_productleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_productright. pfa_gap_inverse_scale_productright + S (k) = (p)) /\ ((((exists pfa_gap_inverse_scale_productresultbound. pfa_gap_inverse_scale_productresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverse_scale_productresultcongruence pfa_offset_right_inverse_scale_productresultcongruence. ((a) * (k)) + (p) * pfa_offset_left_inverse_scale_productresultcongruence = (1) + (p) * pfa_offset_right_inverse_scale_productresultcongruence))))))))
  25. 0025exact hinv_right
  26. 0026cases hinv_right
  27. 0027cases hinv_right_right
  28. 0028cases hinv_right_right_right
  29. 0029have hr : exists cb cc. (((exists pfa_gap_inverse_scale_actualscalar. pfa_gap_inverse_scale_actualscalar + S (a) = (p)) /\ ((forall pfp_index_inverse_scale_actual. (exists pfa_gap_inverse_scale_actualindex. pfa_gap_inverse_scale_actualindex + S (pfp_index_inverse_scale_actual) = (L)) -> exists pfp_source_inverse_scale_actual pfp_value_inverse_scale_actual. ((((exists ff_h_pfp_inverse_scale_actualsource. ff_h_pfp_inverse_scale_actualsource + S (pfp_source_inverse_scale_actual) = S ((S (pfp_index_inverse_scale_actual)) * bc)) /\ exists ff_q_pfp_inverse_scale_actualsource. bb = ff_q_pfp_inverse_scale_actualsource * S ((S (pfp_index_inverse_scale_actual)) * bc) + (pfp_source_inverse_scale_actual))) /\ (((((exists ff_h_pfp_inverse_scale_actualtarget. ff_h_pfp_inverse_scale_actualtarget + S (pfp_value_inverse_scale_actual) = S ((S (pfp_index_inverse_scale_actual)) * cc)) /\ exists ff_q_pfp_inverse_scale_actualtarget. cb = ff_q_pfp_inverse_scale_actualtarget * S ((S (pfp_index_inverse_scale_actual)) * cc) + (pfp_value_inverse_scale_actual))) /\ ((((exists pfa_gap_inverse_scale_actualoperationleft. pfa_gap_inverse_scale_actualoperationleft + S (a) = (p)) /\ (((exists pfa_gap_inverse_scale_actualoperationright. pfa_gap_inverse_scale_actualoperationright + S (pfp_source_inverse_scale_actual) = (p)) /\ ((((exists pfa_gap_inverse_scale_actualoperationresultbound. pfa_gap_inverse_scale_actualoperationresultbound + S (pfp_value_inverse_scale_actual) = (p)) /\ ((exists pfa_offset_left_inverse_scale_actualoperationresultcongruence pfa_offset_right_inverse_scale_actualoperationresultcongruence. ((a) * (pfp_source_inverse_scale_actual)) + (p) * pfa_offset_left_inverse_scale_actualoperationresultcongruence = (pfp_value_inverse_scale_actual) + (p) * pfa_offset_right_inverse_scale_actualoperationresultcongruence)))))))))))))))))
  30. 0030specialize prime_field_polynomial_scale_exists (p)
  31. 0031specialize prime_field_polynomial_scale_exists (a)
  32. 0032specialize prime_field_polynomial_scale_exists (bb)
  33. 0033specialize prime_field_polynomial_scale_exists (bc)
  34. 0034specialize prime_field_polynomial_scale_exists (L)
  35. 0035apply prime_field_polynomial_scale_exists
  36. 0036intro hpzero
  37. 0037specialize prime_nonzero (p)
  38. 0038apply prime_nonzero
  39. 0039exact hp
  40. 0040exact hpzero
  41. 0041exact hinv_right_left
  42. 0042exact hbound_right
  43. 0043cases hr
  44. 0044cases hr_witness
  45. 0045have he : forall mdr_i_pfp_inverse_scale_result_equal mdr_a_pfp_inverse_scale_result_equal. (exists mdr_gap_pfp_inverse_scale_result_equalb. mdr_gap_pfp_inverse_scale_result_equalb + S (mdr_i_pfp_inverse_scale_result_equal) = (L)) -> (((exists ff_h_mdr_pfp_inverse_scale_result_equalo. ff_h_mdr_pfp_inverse_scale_result_equalo + S (mdr_a_pfp_inverse_scale_result_equal) = S ((S (mdr_i_pfp_inverse_scale_result_equal)) * x1)) /\ exists ff_q_mdr_pfp_inverse_scale_result_equalo. x = ff_q_mdr_pfp_inverse_scale_result_equalo * S ((S (mdr_i_pfp_inverse_scale_result_equal)) * x1) + (mdr_a_pfp_inverse_scale_result_equal))) -> (((exists ff_h_mdr_pfp_inverse_scale_result_equaln. ff_h_mdr_pfp_inverse_scale_result_equaln + S (mdr_a_pfp_inverse_scale_result_equal) = S ((S (mdr_i_pfp_inverse_scale_result_equal)) * ac)) /\ exists ff_q_mdr_pfp_inverse_scale_result_equaln. ab = ff_q_mdr_pfp_inverse_scale_result_equaln * S ((S (mdr_i_pfp_inverse_scale_result_equal)) * ac) + (mdr_a_pfp_inverse_scale_result_equal)))
  46. 0046specialize prime_field_polynomial_scale_associative (p)
  47. 0047specialize prime_field_polynomial_scale_associative (a)
  48. 0048specialize prime_field_polynomial_scale_associative (k)
  49. 0049specialize prime_field_polynomial_scale_associative (1)
  50. 0050specialize prime_field_polynomial_scale_associative (ab)
  51. 0051specialize prime_field_polynomial_scale_associative (ac)
  52. 0052specialize prime_field_polynomial_scale_associative (bb)
  53. 0053specialize prime_field_polynomial_scale_associative (bc)
  54. 0054specialize prime_field_polynomial_scale_associative (x)
  55. 0055specialize prime_field_polynomial_scale_associative (x1)
  56. 0056specialize prime_field_polynomial_scale_associative (ab)
  57. 0057specialize prime_field_polynomial_scale_associative (ac)
  58. 0058specialize prime_field_polynomial_scale_associative (L)
  59. 0059apply prime_field_polynomial_scale_associative
  60. 0060exact hm
  61. 0061exact hs
  62. 0062exact hr_witness_witness
  63. 0063specialize prime_field_polynomial_scale_one (p)
  64. 0064specialize prime_field_polynomial_scale_one (ab)
  65. 0065specialize prime_field_polynomial_scale_one (ac)
  66. 0066specialize prime_field_polynomial_scale_one (L)
  67. 0067apply prime_field_polynomial_scale_one
  68. 0068exact hp
  69. 0069exact hbound_left
  70. 0070specialize prime_field_polynomial_scale_transport (p)
  71. 0071specialize prime_field_polynomial_scale_transport (a)
  72. 0072specialize prime_field_polynomial_scale_transport (bb)
  73. 0073specialize prime_field_polynomial_scale_transport (bc)
  74. 0074specialize prime_field_polynomial_scale_transport (x)
  75. 0075specialize prime_field_polynomial_scale_transport (x1)
  76. 0076specialize prime_field_polynomial_scale_transport (bb)
  77. 0077specialize prime_field_polynomial_scale_transport (bc)
  78. 0078specialize prime_field_polynomial_scale_transport (ab)
  79. 0079specialize prime_field_polynomial_scale_transport (ac)
  80. 0080specialize prime_field_polynomial_scale_transport (L)
  81. 0081apply prime_field_polynomial_scale_transport
  82. 0082intro i
  83. 0083intro r
  84. 0084intro hi
  85. 0085intro hat
  86. 0086exact hat
  87. 0087exact he
  88. 0088exact hr_witness_witness