PA00FV

conditional_qres_opposite_status_from_oriented_gauss_counts

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

Conditional three-mod-four reciprocity: exactly one cross-residue proposition holds.

Exact expanded PA statement

forall p q e f Q U h k. p = 2 * h + 1 -> q = 2 * k + 1 -> (((((exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) -> (exists qrc_even_e_even. e = 2 * qrc_even_e_even)) /\ ((exists qrc_even_e_even. e = 2 * qrc_even_e_even) -> (exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq))) /\ (((~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq)) -> (exists qrc_odd_e_odd. e = 2 * qrc_odd_e_odd + 1)) /\ ((exists qrc_odd_e_odd. e = 2 * qrc_odd_e_odd + 1) -> ~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq))))) -> (((((exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp) -> (exists qrc_even_f_even. f = 2 * qrc_even_f_even)) /\ ((exists qrc_even_f_even. f = 2 * qrc_even_f_even) -> (exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))) /\ (((~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp)) -> (exists qrc_odd_f_odd. f = 2 * qrc_odd_f_odd + 1)) /\ ((exists qrc_odd_f_odd. f = 2 * qrc_odd_f_odd + 1) -> ~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))))) -> (exists qrc_u_e_q qrc_v_e_q. e + 2 * qrc_u_e_q = Q + 2 * qrc_v_e_q) -> (exists qrc_u_f_u qrc_v_f_u. f + 2 * qrc_u_f_u = U + 2 * qrc_v_f_u) -> Q + U = h * k -> (((exists qrc_three_p. p = 4 * qrc_three_p + 3) /\ (exists qrc_three_q. q = 4 * qrc_three_q + 3))) -> ((((exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) /\ ~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp)) \/ (~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) /\ (exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))))

Derive opposite residue status in the three-mod-four case

Curated informal proof

Construct and unpack the shared oriented Gauss–Eisenstein counts. When both half-prime parameters are odd, their product is odd, so the Eisenstein identity forces the two Gauss counts to have opposite parity.

The two count classifications then say that exactly one of the cross-residue propositions holds. This is the three-mod-four case of quadratic reciprocity, expressed without a sign or Legendre-symbol primitive.

Referenced ingredients

PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FU qres_opposite_status_from_mod_four_three

Proof neighborhood

Direct dependencies

PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FU qres_opposite_status_from_mod_four_three

Direct dependents

PA00FW quadratic_reciprocity_combined

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 Q
  6. 0006intro U
  7. 0007intro h
  8. 0008intro k
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro heclass
  12. 0012intro hfclass
  13. 0013intro heq
  14. 0014intro hfu
  15. 0015intro hsum
  16. 0016intro hthree
  17. 0017have hcount : exists qrc_u_count_product qrc_v_count_product. e + f + 2 * qrc_u_count_product = h * k + 2 * qrc_v_count_product
  18. 0018specialize gauss_count_sum_mod_two_from_quotient_sums e
  19. 0019specialize gauss_count_sum_mod_two_from_quotient_sums f
  20. 0020specialize gauss_count_sum_mod_two_from_quotient_sums Q
  21. 0021specialize gauss_count_sum_mod_two_from_quotient_sums U
  22. 0022specialize gauss_count_sum_mod_two_from_quotient_sums h
  23. 0023specialize gauss_count_sum_mod_two_from_quotient_sums k
  24. 0024apply gauss_count_sum_mod_two_from_quotient_sums
  25. 0025exact heq
  26. 0026exact hfu
  27. 0027exact hsum
  28. 0028specialize qres_opposite_status_from_mod_four_three p
  29. 0029specialize qres_opposite_status_from_mod_four_three q
  30. 0030specialize qres_opposite_status_from_mod_four_three e
  31. 0031specialize qres_opposite_status_from_mod_four_three f
  32. 0032specialize qres_opposite_status_from_mod_four_three h
  33. 0033specialize qres_opposite_status_from_mod_four_three k
  34. 0034apply qres_opposite_status_from_mod_four_three
  35. 0035exact hp
  36. 0036exact hq
  37. 0037exact heclass
  38. 0038exact hfclass
  39. 0039exact hcount
  40. 0040exact hthree