PG0020

prime_field_polynomial_shift_equivalent_congruent

Two actual trailing-zero shifts preserve formal coefficient equivalence across arbitrary represented lengths, including empty prefixes. The proof obtains actual predecessor-power coefficients and compares decoded values, without any modulus, primality, coefficient-bound, raw-code identity, or evaluation-equality assumption.

Alpha v34 checked-use · first admitted v34 · 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.

All products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ L. ∀ d. ∀ e. ∀ M. ∀ ub. ∀ uc. ∀ vb. ∀ vc. PolynomialEquivalent(b,c,L,d,e,M) → PolynomialShift(b,c,L,ub,uc) → PolynomialShift(d,e,M,vb,vc) → PolynomialEquivalent(ub,uc,S L,vb,vc,S M)

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

Definition DAG

PolynomialPowerCoefficient(b,c,L,k,a) · 6PolynomialEquivalent(b,c,L,d,e,M) · 2PolynomialShift(b,c,L,d,e) · 2

Actual proof prerequisites

zero_or_succ · checked external prerequisiteprime_field_polynomial_shift_power_zeroprime_field_polynomial_shift_power_successorprime_field_polynomial_power_coefficient_exists · checked external prerequisiteprime_field_polynomial_power_coefficient_functional · checked external prerequisite
Original expanded first-order statement 
forall b c L d e M ub uc vb vc. (forall pfrep_power_shift_congruent_input pfrep_left_shift_congruent_input pfrep_right_shift_congruent_input. ((exists pfrep_position_shift_congruent_inputfirst. ((pfrep_position_shift_congruent_inputfirst+S (pfrep_power_shift_congruent_input)=(L)) /\ ((((exists ff_h_pfp_shift_congruent_inputfirstentry. ff_h_pfp_shift_congruent_inputfirstentry + S (pfrep_left_shift_congruent_input) = S ((S (pfrep_position_shift_congruent_inputfirst)) * c)) /\ exists ff_q_pfp_shift_congruent_inputfirstentry. b = ff_q_pfp_shift_congruent_inputfirstentry * S ((S (pfrep_position_shift_congruent_inputfirst)) * c) + (pfrep_left_shift_congruent_input)))))) \/ (((exists pfrep_gap_shift_congruent_inputfirstoutside. pfrep_gap_shift_congruent_inputfirstoutside+(L)=(pfrep_power_shift_congruent_input)) /\ (((pfrep_left_shift_congruent_input)=0))))) -> ((exists pfrep_position_shift_congruent_inputsecond. ((pfrep_position_shift_congruent_inputsecond+S (pfrep_power_shift_congruent_input)=(M)) /\ ((((exists ff_h_pfp_shift_congruent_inputsecondentry. ff_h_pfp_shift_congruent_inputsecondentry + S (pfrep_right_shift_congruent_input) = S ((S (pfrep_position_shift_congruent_inputsecond)) * e)) /\ exists ff_q_pfp_shift_congruent_inputsecondentry. d = ff_q_pfp_shift_congruent_inputsecondentry * S ((S (pfrep_position_shift_congruent_inputsecond)) * e) + (pfrep_right_shift_congruent_input)))))) \/ (((exists pfrep_gap_shift_congruent_inputsecondoutside. pfrep_gap_shift_congruent_inputsecondoutside+(M)=(pfrep_power_shift_congruent_input)) /\ (((pfrep_right_shift_congruent_input)=0))))) -> pfrep_left_shift_congruent_input=pfrep_right_shift_congruent_input) -> (((forall mdr_i_pfp_shift_congruent_leftprefix mdr_a_pfp_shift_congruent_leftprefix. (exists mdr_gap_pfp_shift_congruent_leftprefixb. mdr_gap_pfp_shift_congruent_leftprefixb + S (mdr_i_pfp_shift_congruent_leftprefix) = (L)) -> (((exists ff_h_mdr_pfp_shift_congruent_leftprefixo. ff_h_mdr_pfp_shift_congruent_leftprefixo + S (mdr_a_pfp_shift_congruent_leftprefix) = S ((S (mdr_i_pfp_shift_congruent_leftprefix)) * c)) /\ exists ff_q_mdr_pfp_shift_congruent_leftprefixo. b = ff_q_mdr_pfp_shift_congruent_leftprefixo * S ((S (mdr_i_pfp_shift_congruent_leftprefix)) * c) + (mdr_a_pfp_shift_congruent_leftprefix))) -> (((exists ff_h_mdr_pfp_shift_congruent_leftprefixn. ff_h_mdr_pfp_shift_congruent_leftprefixn + S (mdr_a_pfp_shift_congruent_leftprefix) = S ((S (mdr_i_pfp_shift_congruent_leftprefix)) * uc)) /\ exists ff_q_mdr_pfp_shift_congruent_leftprefixn. ub = ff_q_mdr_pfp_shift_congruent_leftprefixn * S ((S (mdr_i_pfp_shift_congruent_leftprefix)) * uc) + (mdr_a_pfp_shift_congruent_leftprefix)))) /\ ((((exists ff_h_pfp_shift_congruent_leftlast. ff_h_pfp_shift_congruent_leftlast + S (0) = S ((S (L)) * uc)) /\ exists ff_q_pfp_shift_congruent_leftlast. ub = ff_q_pfp_shift_congruent_leftlast * S ((S (L)) * uc) + (0)))))) -> (((forall mdr_i_pfp_shift_congruent_rightprefix mdr_a_pfp_shift_congruent_rightprefix. (exists mdr_gap_pfp_shift_congruent_rightprefixb. mdr_gap_pfp_shift_congruent_rightprefixb + S (mdr_i_pfp_shift_congruent_rightprefix) = (M)) -> (((exists ff_h_mdr_pfp_shift_congruent_rightprefixo. ff_h_mdr_pfp_shift_congruent_rightprefixo + S (mdr_a_pfp_shift_congruent_rightprefix) = S ((S (mdr_i_pfp_shift_congruent_rightprefix)) * e)) /\ exists ff_q_mdr_pfp_shift_congruent_rightprefixo. d = ff_q_mdr_pfp_shift_congruent_rightprefixo * S ((S (mdr_i_pfp_shift_congruent_rightprefix)) * e) + (mdr_a_pfp_shift_congruent_rightprefix))) -> (((exists ff_h_mdr_pfp_shift_congruent_rightprefixn. ff_h_mdr_pfp_shift_congruent_rightprefixn + S (mdr_a_pfp_shift_congruent_rightprefix) = S ((S (mdr_i_pfp_shift_congruent_rightprefix)) * vc)) /\ exists ff_q_mdr_pfp_shift_congruent_rightprefixn. vb = ff_q_mdr_pfp_shift_congruent_rightprefixn * S ((S (mdr_i_pfp_shift_congruent_rightprefix)) * vc) + (mdr_a_pfp_shift_congruent_rightprefix)))) /\ ((((exists ff_h_pfp_shift_congruent_rightlast. ff_h_pfp_shift_congruent_rightlast + S (0) = S ((S (M)) * vc)) /\ exists ff_q_pfp_shift_congruent_rightlast. vb = ff_q_pfp_shift_congruent_rightlast * S ((S (M)) * vc) + (0)))))) -> (forall pfrep_power_shift_congruent_result pfrep_left_shift_congruent_result pfrep_right_shift_congruent_result. ((exists pfrep_position_shift_congruent_resultfirst. ((pfrep_position_shift_congruent_resultfirst+S (pfrep_power_shift_congruent_result)=(S L)) /\ ((((exists ff_h_pfp_shift_congruent_resultfirstentry. ff_h_pfp_shift_congruent_resultfirstentry + S (pfrep_left_shift_congruent_result) = S ((S (pfrep_position_shift_congruent_resultfirst)) * uc)) /\ exists ff_q_pfp_shift_congruent_resultfirstentry. ub = ff_q_pfp_shift_congruent_resultfirstentry * S ((S (pfrep_position_shift_congruent_resultfirst)) * uc) + (pfrep_left_shift_congruent_result)))))) \/ (((exists pfrep_gap_shift_congruent_resultfirstoutside. pfrep_gap_shift_congruent_resultfirstoutside+(S L)=(pfrep_power_shift_congruent_result)) /\ (((pfrep_left_shift_congruent_result)=0))))) -> ((exists pfrep_position_shift_congruent_resultsecond. ((pfrep_position_shift_congruent_resultsecond+S (pfrep_power_shift_congruent_result)=(S M)) /\ ((((exists ff_h_pfp_shift_congruent_resultsecondentry. ff_h_pfp_shift_congruent_resultsecondentry + S (pfrep_right_shift_congruent_result) = S ((S (pfrep_position_shift_congruent_resultsecond)) * vc)) /\ exists ff_q_pfp_shift_congruent_resultsecondentry. vb = ff_q_pfp_shift_congruent_resultsecondentry * S ((S (pfrep_position_shift_congruent_resultsecond)) * vc) + (pfrep_right_shift_congruent_result)))))) \/ (((exists pfrep_gap_shift_congruent_resultsecondoutside. pfrep_gap_shift_congruent_resultsecondoutside+(S M)=(pfrep_power_shift_congruent_result)) /\ (((pfrep_right_shift_congruent_result)=0))))) -> pfrep_left_shift_congruent_result=pfrep_right_shift_congruent_result)

Complete tactic proof in conservative notation

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

138 script commands · 25 reading checkpoints · 12 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 shift power zeroprime field polynomial shift power successor
01Fix variables and assumptionsL1–10

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro L
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro M
  7. L7
    intro ub
  8. L8
    intro uc
  9. L9
    intro vb
  10. L10
    intro vc
02Fix variables and assumptionsL11–18

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

  1. L11
    intro he
  2. L12
    intro hu
  3. L13
    intro hv
  4. L14
    intro k
  5. L15
    intro a
  6. L16
    intro r
  7. L17
    intro hleft
  8. L18
    intro hright
03Establish hcasesL19–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply zero or succ.

  1. L19
    have hcases : k=0 \/ exists j. k=S j
  2. L20
    specialize zero_or_succ (k)
  3. L21
    apply zero_or_succ
04Separate the logical casesL22–22

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

  1. L22
    cases hcases
05Calculate and transport equalitiesL23–26

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

  1. L23
    rewrite hcases_left at hleft
  2. L24
    rewrite hcases_left at hleft
  3. L25
    rewrite hcases_left at hright
  4. L26
    rewrite hcases_left at hright
06Establish hleft_zeroL27–34

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

  1. L27
    have hleft_zero : PolynomialPowerCoefficient(ub,uc,S L,0,0)Definitions: PolynomialPowerCoefficient(ub,uc,S L,0,0)Original native command in the exact edition
  2. L28
    specialize prime_field_polynomial_shift_power_zero (b)
  3. L29
    specialize prime_field_polynomial_shift_power_zero (c)
  4. L30
    specialize prime_field_polynomial_shift_power_zero (L)
  5. L31
    specialize prime_field_polynomial_shift_power_zero (ub)
  6. L32
    specialize prime_field_polynomial_shift_power_zero (uc)
  7. L33
    apply prime_field_polynomial_shift_power_zero
  8. L34
    exact hu
07Establish hright_zeroL35–42

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

  1. L35
    have hright_zero : PolynomialPowerCoefficient(vb,vc,S M,0,0)Definitions: PolynomialPowerCoefficient(vb,vc,S M,0,0)Original native command in the exact edition
  2. L36
    specialize prime_field_polynomial_shift_power_zero (d)
  3. L37
    specialize prime_field_polynomial_shift_power_zero (e)
  4. L38
    specialize prime_field_polynomial_shift_power_zero (M)
  5. L39
    specialize prime_field_polynomial_shift_power_zero (vb)
  6. L40
    specialize prime_field_polynomial_shift_power_zero (vc)
  7. L41
    apply prime_field_polynomial_shift_power_zero
  8. L42
    exact hv
08Establish hleft_valueL43–52

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

  1. L43
    have hleft_value : a=0
  2. L44
    specialize prime_field_polynomial_power_coefficient_functional (ub)
  3. L45
    specialize prime_field_polynomial_power_coefficient_functional (uc)
  4. L46
    specialize prime_field_polynomial_power_coefficient_functional (S L)
  5. L47
    specialize prime_field_polynomial_power_coefficient_functional (0)
  6. L48
    specialize prime_field_polynomial_power_coefficient_functional (a)
  7. L49
    specialize prime_field_polynomial_power_coefficient_functional (0)
  8. L50
    apply prime_field_polynomial_power_coefficient_functional
  9. L51
    exact hleft
  10. L52
    exact hleft_zero
09Establish hright_valueL53–62

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

  1. L53
    have hright_value : 0=r
  2. L54
    specialize prime_field_polynomial_power_coefficient_functional (vb)
  3. L55
    specialize prime_field_polynomial_power_coefficient_functional (vc)
  4. L56
    specialize prime_field_polynomial_power_coefficient_functional (S M)
  5. L57
    specialize prime_field_polynomial_power_coefficient_functional (0)
  6. L58
    specialize prime_field_polynomial_power_coefficient_functional (0)
  7. L59
    specialize prime_field_polynomial_power_coefficient_functional (r)
  8. L60
    apply prime_field_polynomial_power_coefficient_functional
  9. L61
    exact hright_zero
  10. L62
    exact hright
10Calculate and transport equalitiesL63–63

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

  1. L63
    trans 0
11Use earlier factsL64–65

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

  1. L64
    exact hleft_value
  2. L65
    exact hright_value
12Separate the logical casesL66–66

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

  1. L66
    cases hcases_right
13Calculate and transport equalitiesL67–70

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

  1. L67
    rewrite hcases_right_witness at hleft
  2. L68
    rewrite hcases_right_witness at hleft
  3. L69
    rewrite hcases_right_witness at hright
  4. L70
    rewrite hcases_right_witness at hright
14Establish hleft_previousL71–76

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

  1. L71
    have hleft_previous : ∃ s. PolynomialPowerCoefficient(b,c,L,x,s)Definitions: PolynomialPowerCoefficient(b,c,L,x,s)Original native command in the exact edition
  2. L72
    specialize prime_field_polynomial_power_coefficient_exists (b)
  3. L73
    specialize prime_field_polynomial_power_coefficient_exists (c)
  4. L74
    specialize prime_field_polynomial_power_coefficient_exists (L)
  5. L75
    specialize prime_field_polynomial_power_coefficient_exists (x)
  6. L76
    apply prime_field_polynomial_power_coefficient_exists
15Separate the logical casesL77–77

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

  1. L77
    cases hleft_previous
16Establish hright_previousL78–83

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

  1. L78
    have hright_previous : ∃ s. PolynomialPowerCoefficient(d,e,M,x,s)Definitions: PolynomialPowerCoefficient(d,e,M,x,s)Original native command in the exact edition
  2. L79
    specialize prime_field_polynomial_power_coefficient_exists (d)
  3. L80
    specialize prime_field_polynomial_power_coefficient_exists (e)
  4. L81
    specialize prime_field_polynomial_power_coefficient_exists (M)
  5. L82
    specialize prime_field_polynomial_power_coefficient_exists (x)
  6. L83
    apply prime_field_polynomial_power_coefficient_exists
17Separate the logical casesL84–84

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

  1. L84
    cases hright_previous
18Establish hleft_shiftedL85–94

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

  1. L85
    have hleft_shifted : PolynomialPowerCoefficient(ub,uc,S L,S x,x1)Definitions: PolynomialPowerCoefficient(ub,uc,S L,S x,x1)Original native command in the exact edition
  2. L86
    specialize prime_field_polynomial_shift_power_successor (b)
  3. L87
    specialize prime_field_polynomial_shift_power_successor (c)
  4. L88
    specialize prime_field_polynomial_shift_power_successor (L)
  5. L89
    specialize prime_field_polynomial_shift_power_successor (ub)
  6. L90
    specialize prime_field_polynomial_shift_power_successor (uc)
  7. L91
    specialize prime_field_polynomial_shift_power_successor (x)
  8. L92
    specialize prime_field_polynomial_shift_power_successor (x1)
  9. L93
    apply prime_field_polynomial_shift_power_successor
  10. L94
    exact hu
19Use earlier factsL95–95

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

  1. L95
    exact hleft_previous_witness
20Establish hright_shiftedL96–105

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

  1. L96
    have hright_shifted : PolynomialPowerCoefficient(vb,vc,S M,S x,x2)Definitions: PolynomialPowerCoefficient(vb,vc,S M,S x,x2)Original native command in the exact edition
  2. L97
    specialize prime_field_polynomial_shift_power_successor (d)
  3. L98
    specialize prime_field_polynomial_shift_power_successor (e)
  4. L99
    specialize prime_field_polynomial_shift_power_successor (M)
  5. L100
    specialize prime_field_polynomial_shift_power_successor (vb)
  6. L101
    specialize prime_field_polynomial_shift_power_successor (vc)
  7. L102
    specialize prime_field_polynomial_shift_power_successor (x)
  8. L103
    specialize prime_field_polynomial_shift_power_successor (x2)
  9. L104
    apply prime_field_polynomial_shift_power_successor
  10. L105
    exact hv
21Use earlier factsL106–106

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

  1. L106
    exact hright_previous_witness
22Establish hleft_valueL107–116

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

  1. L107
    have hleft_value : a=x1
  2. L108
    specialize prime_field_polynomial_power_coefficient_functional (ub)
  3. L109
    specialize prime_field_polynomial_power_coefficient_functional (uc)
  4. L110
    specialize prime_field_polynomial_power_coefficient_functional (S L)
  5. L111
    specialize prime_field_polynomial_power_coefficient_functional (S x)
  6. L112
    specialize prime_field_polynomial_power_coefficient_functional (a)
  7. L113
    specialize prime_field_polynomial_power_coefficient_functional (x1)
  8. L114
    apply prime_field_polynomial_power_coefficient_functional
  9. L115
    exact hleft
  10. L116
    exact hleft_shifted
23Establish hright_valueL117–126

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

  1. L117
    have hright_value : x2=r
  2. L118
    specialize prime_field_polynomial_power_coefficient_functional (vb)
  3. L119
    specialize prime_field_polynomial_power_coefficient_functional (vc)
  4. L120
    specialize prime_field_polynomial_power_coefficient_functional (S M)
  5. L121
    specialize prime_field_polynomial_power_coefficient_functional (S x)
  6. L122
    specialize prime_field_polynomial_power_coefficient_functional (x2)
  7. L123
    specialize prime_field_polynomial_power_coefficient_functional (r)
  8. L124
    apply prime_field_polynomial_power_coefficient_functional
  9. L125
    exact hright_shifted
  10. L126
    exact hright
24Establish hprevious_equalL127–136

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

  1. L127
    have hprevious_equal : x1=x2
  2. L128
    specialize he (x)
  3. L129
    specialize he (x1)
  4. L130
    specialize he (x2)
  5. L131
    apply he
  6. L132
    exact hleft_previous_witness
  7. L133
    exact hright_previous_witness
  8. L134
    trans x1
  9. L135
    exact hleft_value
  10. L136
    trans x2
25Use earlier factsL137–138

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

  1. L137
    exact hprevious_equal
  2. L138
    exact hright_value

Library-wide reading audit

Original defined command ledger · 138 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro L
  4. 0004intro d
  5. 0005intro e
  6. 0006intro M
  7. 0007intro ub
  8. 0008intro uc
  9. 0009intro vb
  10. 0010intro vc
  11. 0011intro he
  12. 0012intro hu
  13. 0013intro hv
  14. 0014intro k
  15. 0015intro a
  16. 0016intro r
  17. 0017intro hleft
  18. 0018intro hright
  19. 0019have hcases : k=0 \/ exists j. k=S j
  20. 0020specialize zero_or_succ (k)
  21. 0021apply zero_or_succ
  22. 0022cases hcases
  23. 0023rewrite hcases_left at hleft
  24. 0024rewrite hcases_left at hleft
  25. 0025rewrite hcases_left at hright
  26. 0026rewrite hcases_left at hright
  27. 0027have hleft_zero : PolynomialPowerCoefficient(ub,uc,S L,0,0)
  28. 0028specialize prime_field_polynomial_shift_power_zero (b)
  29. 0029specialize prime_field_polynomial_shift_power_zero (c)
  30. 0030specialize prime_field_polynomial_shift_power_zero (L)
  31. 0031specialize prime_field_polynomial_shift_power_zero (ub)
  32. 0032specialize prime_field_polynomial_shift_power_zero (uc)
  33. 0033apply prime_field_polynomial_shift_power_zero
  34. 0034exact hu
  35. 0035have hright_zero : PolynomialPowerCoefficient(vb,vc,S M,0,0)
  36. 0036specialize prime_field_polynomial_shift_power_zero (d)
  37. 0037specialize prime_field_polynomial_shift_power_zero (e)
  38. 0038specialize prime_field_polynomial_shift_power_zero (M)
  39. 0039specialize prime_field_polynomial_shift_power_zero (vb)
  40. 0040specialize prime_field_polynomial_shift_power_zero (vc)
  41. 0041apply prime_field_polynomial_shift_power_zero
  42. 0042exact hv
  43. 0043have hleft_value : a=0
  44. 0044specialize prime_field_polynomial_power_coefficient_functional (ub)
  45. 0045specialize prime_field_polynomial_power_coefficient_functional (uc)
  46. 0046specialize prime_field_polynomial_power_coefficient_functional (S L)
  47. 0047specialize prime_field_polynomial_power_coefficient_functional (0)
  48. 0048specialize prime_field_polynomial_power_coefficient_functional (a)
  49. 0049specialize prime_field_polynomial_power_coefficient_functional (0)
  50. 0050apply prime_field_polynomial_power_coefficient_functional
  51. 0051exact hleft
  52. 0052exact hleft_zero
  53. 0053have hright_value : 0=r
  54. 0054specialize prime_field_polynomial_power_coefficient_functional (vb)
  55. 0055specialize prime_field_polynomial_power_coefficient_functional (vc)
  56. 0056specialize prime_field_polynomial_power_coefficient_functional (S M)
  57. 0057specialize prime_field_polynomial_power_coefficient_functional (0)
  58. 0058specialize prime_field_polynomial_power_coefficient_functional (0)
  59. 0059specialize prime_field_polynomial_power_coefficient_functional (r)
  60. 0060apply prime_field_polynomial_power_coefficient_functional
  61. 0061exact hright_zero
  62. 0062exact hright
  63. 0063trans 0
  64. 0064exact hleft_value
  65. 0065exact hright_value
  66. 0066cases hcases_right
  67. 0067rewrite hcases_right_witness at hleft
  68. 0068rewrite hcases_right_witness at hleft
  69. 0069rewrite hcases_right_witness at hright
  70. 0070rewrite hcases_right_witness at hright
  71. 0071have hleft_previous : ∃ s. PolynomialPowerCoefficient(b,c,L,x,s)
  72. 0072specialize prime_field_polynomial_power_coefficient_exists (b)
  73. 0073specialize prime_field_polynomial_power_coefficient_exists (c)
  74. 0074specialize prime_field_polynomial_power_coefficient_exists (L)
  75. 0075specialize prime_field_polynomial_power_coefficient_exists (x)
  76. 0076apply prime_field_polynomial_power_coefficient_exists
  77. 0077cases hleft_previous
  78. 0078have hright_previous : ∃ s. PolynomialPowerCoefficient(d,e,M,x,s)
  79. 0079specialize prime_field_polynomial_power_coefficient_exists (d)
  80. 0080specialize prime_field_polynomial_power_coefficient_exists (e)
  81. 0081specialize prime_field_polynomial_power_coefficient_exists (M)
  82. 0082specialize prime_field_polynomial_power_coefficient_exists (x)
  83. 0083apply prime_field_polynomial_power_coefficient_exists
  84. 0084cases hright_previous
  85. 0085have hleft_shifted : PolynomialPowerCoefficient(ub,uc,S L,S x,x1)
  86. 0086specialize prime_field_polynomial_shift_power_successor (b)
  87. 0087specialize prime_field_polynomial_shift_power_successor (c)
  88. 0088specialize prime_field_polynomial_shift_power_successor (L)
  89. 0089specialize prime_field_polynomial_shift_power_successor (ub)
  90. 0090specialize prime_field_polynomial_shift_power_successor (uc)
  91. 0091specialize prime_field_polynomial_shift_power_successor (x)
  92. 0092specialize prime_field_polynomial_shift_power_successor (x1)
  93. 0093apply prime_field_polynomial_shift_power_successor
  94. 0094exact hu
  95. 0095exact hleft_previous_witness
  96. 0096have hright_shifted : PolynomialPowerCoefficient(vb,vc,S M,S x,x2)
  97. 0097specialize prime_field_polynomial_shift_power_successor (d)
  98. 0098specialize prime_field_polynomial_shift_power_successor (e)
  99. 0099specialize prime_field_polynomial_shift_power_successor (M)
  100. 0100specialize prime_field_polynomial_shift_power_successor (vb)
  101. 0101specialize prime_field_polynomial_shift_power_successor (vc)
  102. 0102specialize prime_field_polynomial_shift_power_successor (x)
  103. 0103specialize prime_field_polynomial_shift_power_successor (x2)
  104. 0104apply prime_field_polynomial_shift_power_successor
  105. 0105exact hv
  106. 0106exact hright_previous_witness
  107. 0107have hleft_value : a=x1
  108. 0108specialize prime_field_polynomial_power_coefficient_functional (ub)
  109. 0109specialize prime_field_polynomial_power_coefficient_functional (uc)
  110. 0110specialize prime_field_polynomial_power_coefficient_functional (S L)
  111. 0111specialize prime_field_polynomial_power_coefficient_functional (S x)
  112. 0112specialize prime_field_polynomial_power_coefficient_functional (a)
  113. 0113specialize prime_field_polynomial_power_coefficient_functional (x1)
  114. 0114apply prime_field_polynomial_power_coefficient_functional
  115. 0115exact hleft
  116. 0116exact hleft_shifted
  117. 0117have hright_value : x2=r
  118. 0118specialize prime_field_polynomial_power_coefficient_functional (vb)
  119. 0119specialize prime_field_polynomial_power_coefficient_functional (vc)
  120. 0120specialize prime_field_polynomial_power_coefficient_functional (S M)
  121. 0121specialize prime_field_polynomial_power_coefficient_functional (S x)
  122. 0122specialize prime_field_polynomial_power_coefficient_functional (x2)
  123. 0123specialize prime_field_polynomial_power_coefficient_functional (r)
  124. 0124apply prime_field_polynomial_power_coefficient_functional
  125. 0125exact hright_shifted
  126. 0126exact hright
  127. 0127have hprevious_equal : x1=x2
  128. 0128specialize he (x)
  129. 0129specialize he (x1)
  130. 0130specialize he (x2)
  131. 0131apply he
  132. 0132exact hleft_previous_witness
  133. 0133exact hright_previous_witness
  134. 0134trans x1
  135. 0135exact hleft_value
  136. 0136trans x2
  137. 0137exact hprevious_equal
  138. 0138exact hright_value