PA00FU

qres_opposite_status_from_mod_four_three

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

Two three-mod-four inputs force opposite 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_three_p. p = 4 * qrp_three_p + 3) /\ (exists qrp_three_q. q = 4 * qrp_three_q + 3)) -> ((((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

Two three-mod-four inputs force opposite cross-residue status.

Use the direct prerequisites odd_half_odd_iff_mod4_three, odd_mul_odd, qres_opposite_status_from_odd_half_product_mod_two as previously established PA formulas.

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

Referenced ingredients

PA00FR odd_half_odd_iff_mod4_three PA006D odd_mul_odd PA00FT qres_opposite_status_from_odd_half_product_mod_two

Proof neighborhood

Direct dependencies

PA00FR odd_half_odd_iff_mod4_three PA006D odd_mul_odd PA00FT qres_opposite_status_from_odd_half_product_mod_two

Direct dependents

PA00FV conditional_qres_opposite_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 hthree
  13. 0013cases hthree
  14. 0014have hpbridge : (((exists qrp_odd_h. h = 2 * qrp_odd_h + 1) -> (exists qrp_three_p. p = 4 * qrp_three_p + 3)) /\ ((exists qrp_three_p. p = 4 * qrp_three_p + 3) -> (exists qrp_odd_h. h = 2 * qrp_odd_h + 1)))
  15. 0015specialize odd_half_odd_iff_mod4_three p
  16. 0016specialize odd_half_odd_iff_mod4_three h
  17. 0017apply odd_half_odd_iff_mod4_three
  18. 0018exact hp
  19. 0019cases hpbridge
  20. 0020have hpodd : exists qrp_odd_h. h = 2 * qrp_odd_h + 1
  21. 0021apply hpbridge_right
  22. 0022exact hthree_left
  23. 0023have hqbridge : (((exists qrp_odd_k. k = 2 * qrp_odd_k + 1) -> (exists qrp_three_q. q = 4 * qrp_three_q + 3)) /\ ((exists qrp_three_q. q = 4 * qrp_three_q + 3) -> (exists qrp_odd_k. k = 2 * qrp_odd_k + 1)))
  24. 0024specialize odd_half_odd_iff_mod4_three q
  25. 0025specialize odd_half_odd_iff_mod4_three k
  26. 0026apply odd_half_odd_iff_mod4_three
  27. 0027exact hq
  28. 0028cases hqbridge
  29. 0029have hqodd : exists qrp_odd_k. k = 2 * qrp_odd_k + 1
  30. 0030apply hqbridge_right
  31. 0031exact hthree_right
  32. 0032have hproduct : exists qrp_odd_half_product. h * k = 2 * qrp_odd_half_product + 1
  33. 0033specialize odd_mul_odd h
  34. 0034specialize odd_mul_odd k
  35. 0035apply odd_mul_odd
  36. 0036exact hpodd
  37. 0037exact hqodd
  38. 0038specialize qres_opposite_status_from_odd_half_product_mod_two p
  39. 0039specialize qres_opposite_status_from_odd_half_product_mod_two q
  40. 0040specialize qres_opposite_status_from_odd_half_product_mod_two e
  41. 0041specialize qres_opposite_status_from_odd_half_product_mod_two f
  42. 0042specialize qres_opposite_status_from_odd_half_product_mod_two h
  43. 0043specialize qres_opposite_status_from_odd_half_product_mod_two k
  44. 0044apply qres_opposite_status_from_odd_half_product_mod_two
  45. 0045exact heclass
  46. 0046exact hfclass
  47. 0047exact hmod
  48. 0048exact hproduct