PA00BQ

bounded_euler_criterion_residue_iff

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

For bounded nonzero inputs, quadratic residuosity is equivalent to the half-power residue one.

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_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))))

Structural proof guide

Generated structural guide

For bounded nonzero inputs, quadratic residuosity is equivalent to the half-power residue one.

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

The proof proceeds by case analysis (6), intermediate claims (3).

Referenced ingredients

PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Proof neighborhood

Direct dependencies

PA00BN bounded_euler_criterion_dichotomy PA00BP odd_prime_one_not_mod_predecessor PA003L mod_eq_symm PA0024 mod_eq_trans

Direct dependents

PA00BR arbitrary_euler_criterion_residue_iff PA00BS bounded_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 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)
  26. 0026intro hcollision
  27. 0027specialize odd_prime_one_not_mod_predecessor p
  28. 0028specialize odd_prime_one_not_mod_predecessor n
  29. 0029specialize odd_prime_one_not_mod_predecessor h
  30. 0030apply odd_prime_one_not_mod_predecessor
  31. 0031exact hpn
  32. 0032exact hp
  33. 0033exact heven
  34. 0034exact hcollision
  35. 0035split
  36. 0036intro hqres
  37. 0037cases hdichotomy
  38. 0038cases hdichotomy_left
  39. 0039exact hdichotomy_left_right
  40. 0040cases hdichotomy_right
  41. 0041exfalso
  42. 0042apply hdichotomy_right_left
  43. 0043exact hqres
  44. 0044intro hone
  45. 0045cases hdichotomy
  46. 0046cases hdichotomy_left
  47. 0047exact hdichotomy_left_left
  48. 0048cases hdichotomy_right
  49. 0049exfalso
  50. 0050apply hdistinct
  51. 0051have hone_back : exists wpp_mod_left_ecb_one_back wpp_mod_right_ecb_one_back. (1) + p * wpp_mod_left_ecb_one_back = (A) + p * wpp_mod_right_ecb_one_back
  52. 0052specialize mod_eq_symm p
  53. 0053specialize mod_eq_symm A
  54. 0054specialize mod_eq_symm 1
  55. 0055apply mod_eq_symm
  56. 0056exact hone
  57. 0057specialize mod_eq_trans p
  58. 0058specialize mod_eq_trans 1
  59. 0059specialize mod_eq_trans A
  60. 0060specialize mod_eq_trans n
  61. 0061apply mod_eq_trans
  62. 0062exact hone_back
  63. 0063exact hdichotomy_right_right