PA00FO

qres_same_status_from_mod_four_one

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

A one-mod-four input forces equal cross-residue status.

Exact expanded PA statement

forall p q e f h k. p = 2 * h + 1 -> q = 2 * k + 1 -> (((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) -> (exists qrp_even_e_even. e = 2 * qrp_even_e_even)) /\ ((exists qrp_even_e_even. e = 2 * qrp_even_e_even) -> (exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))) /\ (((~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq)) -> (exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1)) /\ ((exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1) -> ~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))))) -> (((((exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp) -> (exists qrp_even_f_even. f = 2 * qrp_even_f_even)) /\ ((exists qrp_even_f_even. f = 2 * qrp_even_f_even) -> (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))) /\ (((~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) -> (exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1)) /\ ((exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1) -> ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))) -> (exists qrp_u_count_product qrp_v_count_product. e + f + 2 * qrp_u_count_product = h * k + 2 * qrp_v_count_product) -> ((exists qrp_one_p. p = 4 * qrp_one_p + 1) \/ (exists qrp_one_q. q = 4 * qrp_one_q + 1)) -> ((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) \/ (~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))

Structural proof guide

Generated structural guide

A one-mod-four input forces equal cross-residue status.

Use the direct prerequisites odd_half_even_iff_mod4_one, even_mul_left, even_mul_right, qres_same_status_from_even_half_product_mod_two as previously established PA formulas.

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

Referenced ingredients

PA00FJ odd_half_even_iff_mod4_one PA006U even_mul_left PA006E even_mul_right PA00FN qres_same_status_from_even_half_product_mod_two

Proof neighborhood

Direct dependencies

PA00FJ odd_half_even_iff_mod4_one PA006U even_mul_left PA006E even_mul_right PA00FN qres_same_status_from_even_half_product_mod_two

Direct dependents

PA00FP conditional_qres_same_status_from_oriented_gauss_counts

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 q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro h
  6. 0006intro k
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro heclass
  10. 0010intro hfclass
  11. 0011intro hmod
  12. 0012intro hone
  13. 0013have hproduct : exists qrp_even_half_product. h * k = 2 * qrp_even_half_product
  14. 0014cases hone
  15. 0015have hbridge : (((exists qrp_even_h. h = 2 * qrp_even_h) -> (exists qrp_one_p. p = 4 * qrp_one_p + 1)) /\ ((exists qrp_one_p. p = 4 * qrp_one_p + 1) -> (exists qrp_even_h. h = 2 * qrp_even_h)))
  16. 0016specialize odd_half_even_iff_mod4_one p
  17. 0017specialize odd_half_even_iff_mod4_one h
  18. 0018apply odd_half_even_iff_mod4_one
  19. 0019exact hp
  20. 0020cases hbridge
  21. 0021have hhalf : exists qrp_even_h. h = 2 * qrp_even_h
  22. 0022apply hbridge_right
  23. 0023exact hone_left
  24. 0024specialize even_mul_left h
  25. 0025specialize even_mul_left k
  26. 0026apply even_mul_left
  27. 0027exact hhalf
  28. 0028have hbridge : (((exists qrp_even_k. k = 2 * qrp_even_k) -> (exists qrp_one_q. q = 4 * qrp_one_q + 1)) /\ ((exists qrp_one_q. q = 4 * qrp_one_q + 1) -> (exists qrp_even_k. k = 2 * qrp_even_k)))
  29. 0029specialize odd_half_even_iff_mod4_one q
  30. 0030specialize odd_half_even_iff_mod4_one k
  31. 0031apply odd_half_even_iff_mod4_one
  32. 0032exact hq
  33. 0033cases hbridge
  34. 0034have hhalf : exists qrp_even_k. k = 2 * qrp_even_k
  35. 0035apply hbridge_right
  36. 0036exact hone_right
  37. 0037specialize even_mul_right h
  38. 0038specialize even_mul_right k
  39. 0039apply even_mul_right
  40. 0040exact hhalf
  41. 0041specialize qres_same_status_from_even_half_product_mod_two p
  42. 0042specialize qres_same_status_from_even_half_product_mod_two q
  43. 0043specialize qres_same_status_from_even_half_product_mod_two e
  44. 0044specialize qres_same_status_from_even_half_product_mod_two f
  45. 0045specialize qres_same_status_from_even_half_product_mod_two h
  46. 0046specialize qres_same_status_from_even_half_product_mod_two k
  47. 0047apply qres_same_status_from_even_half_product_mod_two
  48. 0048exact heclass
  49. 0049exact hfclass
  50. 0050exact hmod
  51. 0051exact hproduct