PA00FW

quadratic_reciprocity_combined

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

The exact sign-free two-case quadratic-reciprocity endpoint.

Exact expanded PA statement

forall p q. (~(p = 1) /\ forall qr_factor_a_prime_p qr_factor_b_prime_p. p = qr_factor_a_prime_p * qr_factor_b_prime_p -> qr_factor_a_prime_p = 1 \/ qr_factor_b_prime_p = 1) -> (~(q = 1) /\ forall qr_factor_a_prime_q qr_factor_b_prime_q. q = qr_factor_a_prime_q * qr_factor_b_prime_q -> qr_factor_a_prime_q = 1 \/ qr_factor_b_prime_q = 1) -> ~(p = q) -> (exists qr_half_odd_p. p = 2 * qr_half_odd_p + 1) -> (exists qr_half_odd_q. q = 2 * qr_half_odd_q + 1) -> ((((exists qr_mod4_one_p. p = 4 * qr_mod4_one_p + 1) \/ (exists qr_mod4_one_q. q = 4 * qr_mod4_one_q + 1)) -> (((exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ (exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)) \/ (~(exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ ~(exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)))) /\ ((((exists qr_mod4_three_p. p = 4 * qr_mod4_three_p + 3) /\ (exists qr_mod4_three_q. q = 4 * qr_mod4_three_q + 3)) -> (((exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ ~(exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)) \/ (~(exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ (exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p))))))

Combine the two sign-free reciprocity cases

Curated informal proof

Write the two odd primes as successors of twice their half-prime parameters. Construct the common Gauss–Eisenstein data package once and unpack its two residue classifications, two parity transports, and the lattice-count identity.

For the same-status implication, feed the hypothesis that one half-prime parameter is even into the constructive same-parity endpoint. For the opposite-status implication, feed the hypothesis that both half-prime parameters are odd into the opposite-parity endpoint. Pair the two implications under the original quantifiers.

Referenced ingredients

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

Proof neighborhood

Direct dependencies

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

Direct dependents

none

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 hp
  4. 0004intro hq
  5. 0005intro hpq
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008cases hpodd
  9. 0009cases hqodd
  10. 0010have hdata : exists e f Q U. (((((((exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first) -> (exists qr_even_first_even. e = 2 * qr_even_first_even)) /\ ((exists qr_even_first_even. e = 2 * qr_even_first_even) -> (exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first))) /\ (((~(exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first)) -> (exists qr_odd_first_odd. e = 2 * qr_odd_first_odd + 1)) /\ ((exists qr_odd_first_odd. e = 2 * qr_odd_first_odd + 1) -> ~(exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first))))) /\ (((((exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second) -> (exists qr_even_second_even. f = 2 * qr_even_second_even)) /\ ((exists qr_even_second_even. f = 2 * qr_even_second_even) -> (exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second))) /\ (((~(exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second)) -> (exists qr_odd_second_odd. f = 2 * qr_odd_second_odd + 1)) /\ ((exists qr_odd_second_odd. f = 2 * qr_odd_second_odd + 1) -> ~(exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second)))))) /\ (((exists qr_mod_u_first qr_mod_v_first. e + 2 * qr_mod_u_first = Q + 2 * qr_mod_v_first) /\ (exists qr_mod_u_second qr_mod_v_second. f + 2 * qr_mod_u_second = U + 2 * qr_mod_v_second)) /\ Q + U = x * x1))
  11. 0011specialize distinct_odd_primes_gauss_eisenstein_data_exists p
  12. 0012specialize distinct_odd_primes_gauss_eisenstein_data_exists q
  13. 0013specialize distinct_odd_primes_gauss_eisenstein_data_exists x
  14. 0014specialize distinct_odd_primes_gauss_eisenstein_data_exists x1
  15. 0015apply distinct_odd_primes_gauss_eisenstein_data_exists
  16. 0016exact hpodd_witness
  17. 0017exact hqodd_witness
  18. 0018exact hp
  19. 0019exact hq
  20. 0020exact hpq
  21. 0021cases hdata
  22. 0022cases hdata_witness
  23. 0023cases hdata_witness_witness
  24. 0024cases hdata_witness_witness_witness
  25. 0025cases hdata_witness_witness_witness_witness
  26. 0026cases hdata_witness_witness_witness_witness_left
  27. 0027cases hdata_witness_witness_witness_witness_right
  28. 0028cases hdata_witness_witness_witness_witness_right_left
  29. 0029split
  30. 0030intro hsame
  31. 0031specialize conditional_qres_same_status_from_oriented_gauss_counts p
  32. 0032specialize conditional_qres_same_status_from_oriented_gauss_counts q
  33. 0033specialize conditional_qres_same_status_from_oriented_gauss_counts x2
  34. 0034specialize conditional_qres_same_status_from_oriented_gauss_counts x3
  35. 0035specialize conditional_qres_same_status_from_oriented_gauss_counts x4
  36. 0036specialize conditional_qres_same_status_from_oriented_gauss_counts x5
  37. 0037specialize conditional_qres_same_status_from_oriented_gauss_counts x
  38. 0038specialize conditional_qres_same_status_from_oriented_gauss_counts x1
  39. 0039apply conditional_qres_same_status_from_oriented_gauss_counts
  40. 0040exact hpodd_witness
  41. 0041exact hqodd_witness
  42. 0042exact hdata_witness_witness_witness_witness_left_left
  43. 0043exact hdata_witness_witness_witness_witness_left_right
  44. 0044exact hdata_witness_witness_witness_witness_right_left_left
  45. 0045exact hdata_witness_witness_witness_witness_right_left_right
  46. 0046exact hdata_witness_witness_witness_witness_right_right
  47. 0047exact hsame
  48. 0048intro hopposite
  49. 0049specialize conditional_qres_opposite_status_from_oriented_gauss_counts p
  50. 0050specialize conditional_qres_opposite_status_from_oriented_gauss_counts q
  51. 0051specialize conditional_qres_opposite_status_from_oriented_gauss_counts x2
  52. 0052specialize conditional_qres_opposite_status_from_oriented_gauss_counts x3
  53. 0053specialize conditional_qres_opposite_status_from_oriented_gauss_counts x4
  54. 0054specialize conditional_qres_opposite_status_from_oriented_gauss_counts x5
  55. 0055specialize conditional_qres_opposite_status_from_oriented_gauss_counts x
  56. 0056specialize conditional_qres_opposite_status_from_oriented_gauss_counts x1
  57. 0057apply conditional_qres_opposite_status_from_oriented_gauss_counts
  58. 0058exact hpodd_witness
  59. 0059exact hqodd_witness
  60. 0060exact hdata_witness_witness_witness_witness_left_left
  61. 0061exact hdata_witness_witness_witness_witness_left_right
  62. 0062exact hdata_witness_witness_witness_witness_right_left_left
  63. 0063exact hdata_witness_witness_witness_witness_right_left_right
  64. 0064exact hdata_witness_witness_witness_witness_right_right
  65. 0065exact hopposite