PX0069

prime_field_convolution_coefficient_before_left_padding_right

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

Every actual convolution coefficient before the added leading block is zero at a nonzero modulus.

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 ab ac L bb bc M BB BC t i r. (~(p=0)) -> (((forall pfp_repeat_index_before_coefficient_pad_rightzeros. (exists pfa_gap_before_coefficient_pad_rightzerosindex. pfa_gap_before_coefficient_pad_rightzerosindex + S (pfp_repeat_index_before_coefficient_pad_rightzeros) = (t)) -> (((exists ff_h_pfp_before_coefficient_pad_rightzerosentry. ff_h_pfp_before_coefficient_pad_rightzerosentry + S (0) = S ((S (pfp_repeat_index_before_coefficient_pad_rightzeros)) * BC)) /\ exists ff_q_pfp_before_coefficient_pad_rightzerosentry. BB = ff_q_pfp_before_coefficient_pad_rightzerosentry * S ((S (pfp_repeat_index_before_coefficient_pad_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_before_coefficient_pad_right pfrep_value_before_coefficient_pad_right. (exists pfa_gap_before_coefficient_pad_rightbound. pfa_gap_before_coefficient_pad_rightbound + S (pfrep_index_before_coefficient_pad_right) = (M)) -> (((exists ff_h_pfp_before_coefficient_pad_rightinput. ff_h_pfp_before_coefficient_pad_rightinput + S (pfrep_value_before_coefficient_pad_right) = S ((S (pfrep_index_before_coefficient_pad_right)) * bc)) /\ exists ff_q_pfp_before_coefficient_pad_rightinput. bb = ff_q_pfp_before_coefficient_pad_rightinput * S ((S (pfrep_index_before_coefficient_pad_right)) * bc) + (pfrep_value_before_coefficient_pad_right))) -> (((exists ff_h_pfp_before_coefficient_pad_rightoutput. ff_h_pfp_before_coefficient_pad_rightoutput + S (pfrep_value_before_coefficient_pad_right) = S ((S ((t)+pfrep_index_before_coefficient_pad_right)) * BC)) /\ exists ff_q_pfp_before_coefficient_pad_rightoutput. BB = ff_q_pfp_before_coefficient_pad_rightoutput * S ((S ((t)+pfrep_index_before_coefficient_pad_right)) * BC) + (pfrep_value_before_coefficient_pad_right))))))) -> (exists pfa_gap_before_coefficient_index_right. pfa_gap_before_coefficient_index_right + S (i) = (t)) -> (exists pfc_terms_code_before_coefficient_actual_right pfc_terms_scale_before_coefficient_actual_right pfc_natural_sum_before_coefficient_actual_right. ((forall pfc_index_before_coefficient_actual_rightdiagonal. (exists pfa_gap_before_coefficient_actual_rightdiagonalbound. pfa_gap_before_coefficient_actual_rightdiagonalbound + S (pfc_index_before_coefficient_actual_rightdiagonal) = (S (i))) -> exists pfc_value_before_coefficient_actual_rightdiagonal. ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonalentry. ff_h_pfp_before_coefficient_actual_rightdiagonalentry + S (pfc_value_before_coefficient_actual_rightdiagonal) = S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * pfc_terms_scale_before_coefficient_actual_right)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonalentry. pfc_terms_code_before_coefficient_actual_right = ff_q_pfp_before_coefficient_actual_rightdiagonalentry * S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * pfc_terms_scale_before_coefficient_actual_right) + (pfc_value_before_coefficient_actual_rightdiagonal))) /\ ((exists pfc_complement_before_coefficient_actual_rightdiagonalterm pfc_left_before_coefficient_actual_rightdiagonalterm pfc_right_before_coefficient_actual_rightdiagonalterm. (((pfc_index_before_coefficient_actual_rightdiagonal)+pfc_complement_before_coefficient_actual_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_before_coefficient_actual_rightdiagonaltermleftinside. pfa_gap_before_coefficient_actual_rightdiagonaltermleftinside + S (pfc_index_before_coefficient_actual_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonaltermleftentry. ff_h_pfp_before_coefficient_actual_rightdiagonaltermleftentry + S (pfc_left_before_coefficient_actual_rightdiagonalterm) = S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * ac)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonaltermleftentry. ab = ff_q_pfp_before_coefficient_actual_rightdiagonaltermleftentry * S ((S (pfc_index_before_coefficient_actual_rightdiagonal)) * ac) + (pfc_left_before_coefficient_actual_rightdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_rightdiagonaltermleftoutside. pfc_gap_before_coefficient_actual_rightdiagonaltermleftoutside+(L)=(pfc_index_before_coefficient_actual_rightdiagonal)) /\ (((pfc_left_before_coefficient_actual_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_before_coefficient_actual_rightdiagonaltermrightinside. pfa_gap_before_coefficient_actual_rightdiagonaltermrightinside + S (pfc_complement_before_coefficient_actual_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_before_coefficient_actual_rightdiagonaltermrightentry. ff_h_pfp_before_coefficient_actual_rightdiagonaltermrightentry + S (pfc_right_before_coefficient_actual_rightdiagonalterm) = S ((S (pfc_complement_before_coefficient_actual_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_before_coefficient_actual_rightdiagonaltermrightentry. BB = ff_q_pfp_before_coefficient_actual_rightdiagonaltermrightentry * S ((S (pfc_complement_before_coefficient_actual_rightdiagonalterm)) * BC) + (pfc_right_before_coefficient_actual_rightdiagonalterm)))))) \/ (((exists pfc_gap_before_coefficient_actual_rightdiagonaltermrightoutside. pfc_gap_before_coefficient_actual_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_before_coefficient_actual_rightdiagonalterm)) /\ (((pfc_right_before_coefficient_actual_rightdiagonalterm)=0))))) /\ (((pfc_value_before_coefficient_actual_rightdiagonal)=pfc_left_before_coefficient_actual_rightdiagonalterm*pfc_right_before_coefficient_actual_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_before_coefficient_actual_rightsum fs_v_pfc_before_coefficient_actual_rightsum. ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_start. fs_h_pfc_before_coefficient_actual_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_start. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_start * S ((S (0)) * fs_v_pfc_before_coefficient_actual_rightsum) + (0))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_terminal. fs_h_pfc_before_coefficient_actual_rightsum_body_terminal + S (pfc_natural_sum_before_coefficient_actual_right) = S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_terminal. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_before_coefficient_actual_rightsum) + (pfc_natural_sum_before_coefficient_actual_right))) /\ forall fs_i_pfc_before_coefficient_actual_rightsum_body_steps. (exists fs_lt_pfc_before_coefficient_actual_rightsum_body_steps_bound. fs_lt_pfc_before_coefficient_actual_rightsum_body_steps_bound + S fs_i_pfc_before_coefficient_actual_rightsum_body_steps = S (i)) -> exists fs_a_pfc_before_coefficient_actual_rightsum_body_steps fs_r_pfc_before_coefficient_actual_rightsum_body_steps fs_s_pfc_before_coefficient_actual_rightsum_body_steps. ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_summand. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_summand + S (fs_a_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_right)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_summand. pfc_terms_code_before_coefficient_actual_right = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_summand * S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * pfc_terms_scale_before_coefficient_actual_right) + (fs_a_pfc_before_coefficient_actual_rightsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_partial. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_partial + S (fs_r_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_partial. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_partial * S ((S (fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum) + (fs_r_pfc_before_coefficient_actual_rightsum_body_steps))) /\ ((((exists fs_h_pfc_before_coefficient_actual_rightsum_body_steps_successor. fs_h_pfc_before_coefficient_actual_rightsum_body_steps_successor + S (fs_s_pfc_before_coefficient_actual_rightsum_body_steps) = S ((S (S fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum)) /\ exists fs_q_pfc_before_coefficient_actual_rightsum_body_steps_successor. fs_u_pfc_before_coefficient_actual_rightsum = fs_q_pfc_before_coefficient_actual_rightsum_body_steps_successor * S ((S (S fs_i_pfc_before_coefficient_actual_rightsum_body_steps)) * fs_v_pfc_before_coefficient_actual_rightsum) + (fs_s_pfc_before_coefficient_actual_rightsum_body_steps))) /\ fs_s_pfc_before_coefficient_actual_rightsum_body_steps = fs_r_pfc_before_coefficient_actual_rightsum_body_steps + fs_a_pfc_before_coefficient_actual_rightsum_body_steps)))))) /\ ((((exists pfa_gap_before_coefficient_actual_rightresiduebound. pfa_gap_before_coefficient_actual_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_before_coefficient_actual_rightresiduecongruence pfa_offset_right_before_coefficient_actual_rightresiduecongruence. (pfc_natural_sum_before_coefficient_actual_right) + (p) * pfa_offset_left_before_coefficient_actual_rightresiduecongruence = (r) + (p) * pfa_offset_right_before_coefficient_actual_rightresiduecongruence))))))))) -> (r=0)

Constructive proof overview

Generated structural guide

Every actual convolution coefficient before the added leading block is zero at a nonzero modulus.

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

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

Proof neighborhood

Direct dependencies

PX0063 polynomial_diagonal_term_left_padding_zero_right le_trans Alpha theorem; checked-use authorized beta_repeat_sum_exact Alpha theorem; checked-use authorized prime_field_residue_bounded_value Alpha theorem; checked-use authorized one_le_of_ne_zero Alpha theorem; checked-use authorized le_add_right Alpha theorem; checked-use authorized

Direct dependents

PX006D prime_field_polynomial_convolution_left_padding_nonempty_right

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

77 script commands · 14 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.

Named ingredients (1)
polynomial diagonal term left padding zero right

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 ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro BB
  9. L9
    intro BC
  10. L10
    intro t
02Fix variables and assumptionsL11–16

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

  1. L11
    intro i
  2. L12
    intro r
  3. L13
    intro hp
  4. L14
    intro hpad
  5. L15
    intro hi
  6. L16
    intro hc
03Separate the logical casesL17–21

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

  1. L17
    cases hc
  2. L18
    cases hc_witness
  3. L19
    cases hc_witness_witness
  4. L20
    cases hc_witness_witness_witness
  5. L21
    cases hc_witness_witness_witness_right
04Establish hzL22–24

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

  1. L22
    have hz : Repeat(x,x1,0,S i)Definitions: Repeat
  2. L23
    intro j
  3. L24
    intro hj
05Establish htL25–28

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

  1. L25
    have ht : ∃ z. BetaAt(x,x1,j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,i,j,z)Definitions: PolynomialDiagonalTermBetaAt
  2. L26
    specialize hc_witness_witness_witness_left (j)
  3. L27
    apply hc_witness_witness_witness_left
  4. L28
    exact hj
06Separate the logical casesL29–30

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

  1. L29
    cases ht
  2. L30
    cases ht_witness
07Establish heqL31–40

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

  1. L31
    have heq : x3=0
  2. L32
    specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  3. L33
    specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  4. L34
    specialize polynomial_diagonal_term_left_padding_zero_right (L)
  5. L35
    specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  6. L36
    specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  7. L37
    specialize polynomial_diagonal_term_left_padding_zero_right (M)
  8. L38
    specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  9. L39
    specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  10. L40
    specialize polynomial_diagonal_term_left_padding_zero_right (t)
08Use earlier factsL41–50

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

  1. L41
    specialize polynomial_diagonal_term_left_padding_zero_right (i)
  2. L42
    specialize polynomial_diagonal_term_left_padding_zero_right (j)
  3. L43
    specialize polynomial_diagonal_term_left_padding_zero_right (x3)
  4. L44
    apply polynomial_diagonal_term_left_padding_zero_right
  5. L45
    exact hpad
  6. L46
    specialize le_trans (S i)
  7. L47
    specialize le_trans (t)
  8. L48
    specialize le_trans (t+j)
  9. L49
    apply le_trans
  10. L50
    exact hi
09Use earlier factsL51–54

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

  1. L51
    specialize le_add_right (t)
  2. L52
    specialize le_add_right (j)
  3. L53
    apply le_add_right
  4. L54
    exact ht_witness_right
10Calculate and transport equalitiesL55–56

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

  1. L55
    rewrite heq at ht_witness_left
  2. L56
    rewrite heq at ht_witness_left
11Use earlier factsL57–57

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

  1. L57
    exact ht_witness_left
12Establish hsumL58–67

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

  1. L58
    have hsum : x2=0
  2. L59
    trans (S i)*0
  3. L60
    specialize beta_repeat_sum_exact (x)
  4. L61
    specialize beta_repeat_sum_exact (x1)
  5. L62
    specialize beta_repeat_sum_exact (0)
  6. L63
    specialize beta_repeat_sum_exact (S i)
  7. L64
    specialize beta_repeat_sum_exact (x2)
  8. L65
    apply beta_repeat_sum_exact
  9. L66
    exact hz
  10. L67
    exact hc_witness_witness_witness_right_left
13Calculate and transport equalitiesL68–69

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

  1. L68
    simp
  2. L69
    rewrite hsum at hc_witness_witness_witness_right_right
14Use earlier factsL70–77

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

  1. L70
    specialize prime_field_residue_bounded_value (p)
  2. L71
    specialize prime_field_residue_bounded_value (0)
  3. L72
    specialize prime_field_residue_bounded_value (r)
  4. L73
    apply prime_field_residue_bounded_value
  5. L74
    specialize one_le_of_ne_zero (p)
  6. L75
    apply one_le_of_ne_zero
  7. L76
    exact hp
  8. L77
    exact hc_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 77 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro BB
  9. 0009intro BC
  10. 0010intro t
  11. 0011intro i
  12. 0012intro r
  13. 0013intro hp
  14. 0014intro hpad
  15. 0015intro hi
  16. 0016intro hc
  17. 0017cases hc
  18. 0018cases hc_witness
  19. 0019cases hc_witness_witness
  20. 0020cases hc_witness_witness_witness
  21. 0021cases hc_witness_witness_witness_right
  22. 0022have hz : forall pfp_repeat_index_before_coefficient_zero_diagonal_right. (exists pfa_gap_before_coefficient_zero_diagonal_rightindex. pfa_gap_before_coefficient_zero_diagonal_rightindex + S (pfp_repeat_index_before_coefficient_zero_diagonal_right) = (S i)) -> (((exists ff_h_pfp_before_coefficient_zero_diagonal_rightentry. ff_h_pfp_before_coefficient_zero_diagonal_rightentry + S (0) = S ((S (pfp_repeat_index_before_coefficient_zero_diagonal_right)) * x1)) /\ exists ff_q_pfp_before_coefficient_zero_diagonal_rightentry. x = ff_q_pfp_before_coefficient_zero_diagonal_rightentry * S ((S (pfp_repeat_index_before_coefficient_zero_diagonal_right)) * x1) + (0)))
  23. 0023intro j
  24. 0024intro hj
  25. 0025have ht : exists z. ((((exists ff_h_pfp_before_coefficient_entry_right. ff_h_pfp_before_coefficient_entry_right + S (z) = S ((S (j)) * x1)) /\ exists ff_q_pfp_before_coefficient_entry_right. x = ff_q_pfp_before_coefficient_entry_right * S ((S (j)) * x1) + (z))) /\ ((exists pfc_complement_before_coefficient_term_right pfc_left_before_coefficient_term_right pfc_right_before_coefficient_term_right. (((j)+pfc_complement_before_coefficient_term_right=(i)) /\ ((((((exists pfa_gap_before_coefficient_term_rightleftinside. pfa_gap_before_coefficient_term_rightleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_before_coefficient_term_rightleftentry. ff_h_pfp_before_coefficient_term_rightleftentry + S (pfc_left_before_coefficient_term_right) = S ((S (j)) * ac)) /\ exists ff_q_pfp_before_coefficient_term_rightleftentry. ab = ff_q_pfp_before_coefficient_term_rightleftentry * S ((S (j)) * ac) + (pfc_left_before_coefficient_term_right)))))) \/ (((exists pfc_gap_before_coefficient_term_rightleftoutside. pfc_gap_before_coefficient_term_rightleftoutside+(L)=(j)) /\ (((pfc_left_before_coefficient_term_right)=0))))) /\ ((((((exists pfa_gap_before_coefficient_term_rightrightinside. pfa_gap_before_coefficient_term_rightrightinside + S (pfc_complement_before_coefficient_term_right) = (t+M)) /\ ((((exists ff_h_pfp_before_coefficient_term_rightrightentry. ff_h_pfp_before_coefficient_term_rightrightentry + S (pfc_right_before_coefficient_term_right) = S ((S (pfc_complement_before_coefficient_term_right)) * BC)) /\ exists ff_q_pfp_before_coefficient_term_rightrightentry. BB = ff_q_pfp_before_coefficient_term_rightrightentry * S ((S (pfc_complement_before_coefficient_term_right)) * BC) + (pfc_right_before_coefficient_term_right)))))) \/ (((exists pfc_gap_before_coefficient_term_rightrightoutside. pfc_gap_before_coefficient_term_rightrightoutside+(t+M)=(pfc_complement_before_coefficient_term_right)) /\ (((pfc_right_before_coefficient_term_right)=0))))) /\ (((z)=pfc_left_before_coefficient_term_right*pfc_right_before_coefficient_term_right))))))))))
  26. 0026specialize hc_witness_witness_witness_left (j)
  27. 0027apply hc_witness_witness_witness_left
  28. 0028exact hj
  29. 0029cases ht
  30. 0030cases ht_witness
  31. 0031have heq : x3=0
  32. 0032specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  33. 0033specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  34. 0034specialize polynomial_diagonal_term_left_padding_zero_right (L)
  35. 0035specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  36. 0036specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  37. 0037specialize polynomial_diagonal_term_left_padding_zero_right (M)
  38. 0038specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  39. 0039specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  40. 0040specialize polynomial_diagonal_term_left_padding_zero_right (t)
  41. 0041specialize polynomial_diagonal_term_left_padding_zero_right (i)
  42. 0042specialize polynomial_diagonal_term_left_padding_zero_right (j)
  43. 0043specialize polynomial_diagonal_term_left_padding_zero_right (x3)
  44. 0044apply polynomial_diagonal_term_left_padding_zero_right
  45. 0045exact hpad
  46. 0046specialize le_trans (S i)
  47. 0047specialize le_trans (t)
  48. 0048specialize le_trans (t+j)
  49. 0049apply le_trans
  50. 0050exact hi
  51. 0051specialize le_add_right (t)
  52. 0052specialize le_add_right (j)
  53. 0053apply le_add_right
  54. 0054exact ht_witness_right
  55. 0055rewrite heq at ht_witness_left
  56. 0056rewrite heq at ht_witness_left
  57. 0057exact ht_witness_left
  58. 0058have hsum : x2=0
  59. 0059trans (S i)*0
  60. 0060specialize beta_repeat_sum_exact (x)
  61. 0061specialize beta_repeat_sum_exact (x1)
  62. 0062specialize beta_repeat_sum_exact (0)
  63. 0063specialize beta_repeat_sum_exact (S i)
  64. 0064specialize beta_repeat_sum_exact (x2)
  65. 0065apply beta_repeat_sum_exact
  66. 0066exact hz
  67. 0067exact hc_witness_witness_witness_right_left
  68. 0068simp
  69. 0069rewrite hsum at hc_witness_witness_witness_right_right
  70. 0070specialize prime_field_residue_bounded_value (p)
  71. 0071specialize prime_field_residue_bounded_value (0)
  72. 0072specialize prime_field_residue_bounded_value (r)
  73. 0073apply prime_field_residue_bounded_value
  74. 0074specialize one_le_of_ne_zero (p)
  75. 0075apply one_le_of_ne_zero
  76. 0076exact hp
  77. 0077exact hc_witness_witness_witness_right_right