PA00BS

bounded_euler_criterion_nonresidue_iff

Alpha v16 checked-use theorem · independently closed; not Stable

For bounded nonzero inputs, nonresiduosity is equivalent to the half-power residue p-1.

Exact expanded PA statement

forall p a n h A. p = S n -> ((~(p = 1) /\ forall esi_prime_left_ecb_prime esi_prime_right_ecb_prime. p = esi_prime_left_ecb_prime * esi_prime_right_ecb_prime -> esi_prime_left_ecb_prime = 1 \/ esi_prime_right_ecb_prime = 1)) -> ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> n = h + h -> (exists ff_b_ecb_power ff_c_ecb_power. ((forall ff_i_ecb_power_repeat. (exists ff_lt_ecb_power_repeat_bound. ff_lt_ecb_power_repeat_bound + S ff_i_ecb_power_repeat = h) -> (((exists ff_h_ecb_power_repeat_decoded. ff_h_ecb_power_repeat_decoded + S (a) = S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_repeat_decoded. ff_b_ecb_power = ff_q_ecb_power_repeat_decoded * S ((S (ff_i_ecb_power_repeat)) * ff_c_ecb_power) + (a)))) /\ (exists ff_u_ecb_power_product ff_v_ecb_power_product. ((((exists ff_h_ecb_power_product_start. ff_h_ecb_power_product_start + S (1) = S ((S (0)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_start. ff_u_ecb_power_product = ff_q_ecb_power_product_start * S ((S (0)) * ff_v_ecb_power_product) + (1))) /\ ((((exists ff_h_ecb_power_product_terminal. ff_h_ecb_power_product_terminal + S (A) = S ((S (h)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_terminal. ff_u_ecb_power_product = ff_q_ecb_power_product_terminal * S ((S (h)) * ff_v_ecb_power_product) + (A))) /\ forall ff_i_ecb_power_product. (exists ff_lt_ecb_power_product_bound. ff_lt_ecb_power_product_bound + S ff_i_ecb_power_product = h) -> exists ff_p_ecb_power_product ff_r_ecb_power_product ff_s_ecb_power_product. ((((exists ff_h_ecb_power_product_factor. ff_h_ecb_power_product_factor + S (ff_p_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power)) /\ exists ff_q_ecb_power_product_factor. ff_b_ecb_power = ff_q_ecb_power_product_factor * S ((S (ff_i_ecb_power_product)) * ff_c_ecb_power) + (ff_p_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_partial. ff_h_ecb_power_product_partial + S (ff_r_ecb_power_product) = S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_partial. ff_u_ecb_power_product = ff_q_ecb_power_product_partial * S ((S (ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_r_ecb_power_product))) /\ ((((exists ff_h_ecb_power_product_successor. ff_h_ecb_power_product_successor + S (ff_s_ecb_power_product) = S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product)) /\ exists ff_q_ecb_power_product_successor. ff_u_ecb_power_product = ff_q_ecb_power_product_successor * S ((S (S ff_i_ecb_power_product)) * ff_v_ecb_power_product) + (ff_s_ecb_power_product))) /\ ff_s_ecb_power_product = ff_r_ecb_power_product * ff_p_ecb_power_product)))))))) -> (((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) -> (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor)) /\ ((exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor) -> ~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres))))

Structural proof guide

Generated structural guide

For bounded nonzero inputs, nonresiduosity is equivalent to the half-power residue p-1.

Use the direct prerequisites bounded_euler_criterion_dichotomy, bounded_euler_criterion_residue_iff, odd_prime_one_not_mod_predecessor, mod_eq_symm, mod_eq_trans as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (5).

Referenced ingredients

PA00BN bounded_euler_criterion_dichotomy PA00BQ bounded_euler_criterion_residue_iff PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00BN bounded_euler_criterion_dichotomy PA00BQ bounded_euler_criterion_residue_iff PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00BT arbitrary_euler_criterion_nonresidue_iff

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro h
  5. 0005intro A
  6. 0006intro hpn
  7. 0007intro hp
  8. 0008intro ha0
  9. 0009intro hap
  10. 0010intro heven
  11. 0011intro hpower
  12. 0012have hdichotomy : (((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) /\ (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) \/ ((~(exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)) /\ (exists wpp_mod_left_ecb_mod_predecessor wpp_mod_right_ecb_mod_predecessor. (A) + p * wpp_mod_left_ecb_mod_predecessor = (n) + p * wpp_mod_right_ecb_mod_predecessor)))
  13. 0013specialize bounded_euler_criterion_dichotomy p
  14. 0014specialize bounded_euler_criterion_dichotomy a
  15. 0015specialize bounded_euler_criterion_dichotomy n
  16. 0016specialize bounded_euler_criterion_dichotomy h
  17. 0017specialize bounded_euler_criterion_dichotomy A
  18. 0018apply bounded_euler_criterion_dichotomy
  19. 0019exact hpn
  20. 0020exact hp
  21. 0021exact ha0
  22. 0022exact hap
  23. 0023exact heven
  24. 0024exact hpower
  25. 0025have hresidue_iff : (((exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres) -> (exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one)) /\ ((exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one) -> (exists qr_x_ecb_qres. exists qr_u_ecb_qres qr_v_ecb_qres. qr_x_ecb_qres * qr_x_ecb_qres + p * qr_u_ecb_qres = a + p * qr_v_ecb_qres)))
  26. 0026specialize bounded_euler_criterion_residue_iff p
  27. 0027specialize bounded_euler_criterion_residue_iff a
  28. 0028specialize bounded_euler_criterion_residue_iff n
  29. 0029specialize bounded_euler_criterion_residue_iff h
  30. 0030specialize bounded_euler_criterion_residue_iff A
  31. 0031apply bounded_euler_criterion_residue_iff
  32. 0032exact hpn
  33. 0033exact hp
  34. 0034exact ha0
  35. 0035exact hap
  36. 0036exact heven
  37. 0037exact hpower
  38. 0038have hdistinct : ~(exists wpp_mod_left_ecb_one_mod_predecessor wpp_mod_right_ecb_one_mod_predecessor. (1) + p * wpp_mod_left_ecb_one_mod_predecessor = (n) + p * wpp_mod_right_ecb_one_mod_predecessor)
  39. 0039intro hcollision
  40. 0040specialize odd_prime_one_not_mod_predecessor p
  41. 0041specialize odd_prime_one_not_mod_predecessor n
  42. 0042specialize odd_prime_one_not_mod_predecessor h
  43. 0043apply odd_prime_one_not_mod_predecessor
  44. 0044exact hpn
  45. 0045exact hp
  46. 0046exact heven
  47. 0047exact hcollision
  48. 0048split
  49. 0049intro hnonresidue
  50. 0050cases hdichotomy
  51. 0051cases hdichotomy_left
  52. 0052exfalso
  53. 0053apply hnonresidue
  54. 0054exact hdichotomy_left_left
  55. 0055cases hdichotomy_right
  56. 0056exact hdichotomy_right_right
  57. 0057intro hminus
  58. 0058intro hqres
  59. 0059cases hresidue_iff
  60. 0060have hone : exists wpp_mod_left_ecb_mod_one wpp_mod_right_ecb_mod_one. (A) + p * wpp_mod_left_ecb_mod_one = (1) + p * wpp_mod_right_ecb_mod_one
  61. 0061apply hresidue_iff_left
  62. 0062exact hqres
  63. 0063apply hdistinct
  64. 0064have hone_back : exists wpp_mod_left_ecb_nonresidue_one_back wpp_mod_right_ecb_nonresidue_one_back. (1) + p * wpp_mod_left_ecb_nonresidue_one_back = (A) + p * wpp_mod_right_ecb_nonresidue_one_back
  65. 0065specialize mod_eq_symm p
  66. 0066specialize mod_eq_symm A
  67. 0067specialize mod_eq_symm 1
  68. 0068apply mod_eq_symm
  69. 0069exact hone
  70. 0070specialize mod_eq_trans p
  71. 0071specialize mod_eq_trans 1
  72. 0072specialize mod_eq_trans A
  73. 0073specialize mod_eq_trans n
  74. 0074apply mod_eq_trans
  75. 0075exact hone_back
  76. 0076exact hminus