PA00FP

conditional_qres_same_status_from_oriented_gauss_counts

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

Conditional one-mod-four reciprocity: the two cross-residue propositions have the same truth status.

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_one_p. p = 4 * qrc_one_p + 1) \/ (exists qrc_one_q. q = 4 * qrc_one_q + 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 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 equal residue status when one prime is one modulo four

Curated informal proof

Construct and unpack the shared oriented Gauss–Eisenstein counts. If one half-prime parameter is even, their product is even; the Eisenstein identity and the two modulo-two transports therefore force the Gauss counts to have the same parity.

Each count's parity is already equivalent to the truth status of its cross-residue proposition, so the two propositions are equivalent. This is the one-mod-four case of quadratic reciprocity.

Referenced ingredients

PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FO qres_same_status_from_mod_four_one

Proof neighborhood

Direct dependencies

PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FO qres_same_status_from_mod_four_one

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 hone
  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_same_status_from_mod_four_one p
  29. 0029specialize qres_same_status_from_mod_four_one q
  30. 0030specialize qres_same_status_from_mod_four_one e
  31. 0031specialize qres_same_status_from_mod_four_one f
  32. 0032specialize qres_same_status_from_mod_four_one h
  33. 0033specialize qres_same_status_from_mod_four_one k
  34. 0034apply qres_same_status_from_mod_four_one
  35. 0035exact hp
  36. 0036exact hq
  37. 0037exact heclass
  38. 0038exact hfclass
  39. 0039exact hcount
  40. 0040exact hone