PA00FP

conditional_qres_same_status_from_oriented_gauss_counts

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

40 script commands · 5 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
gauss count sum mod two from quotient sumsqres same status from mod four one
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro q
  3. L3
    intro e
  4. L4
    intro f
  5. L5
    intro Q
  6. L6
    intro U
  7. L7
    intro h
  8. L8
    intro k
  9. L9
    intro hp
  10. L10
    intro hq
02Fix variables and assumptionsL11–16

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro heclass
  2. L12
    intro hfclass
  3. L13
    intro heq
  4. L14
    intro hfu
  5. L15
    intro hsum
  6. L16
    intro hone
03Establish hcountL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss count sum mod two from quotient sums.

  1. L17
    have hcount : exists qrc_u_count_product qrc_v_count_product. e + f + 2 * qrc_u_count_product = h * k + 2 * qrc_v_count_product
  2. L18
    specialize gauss_count_sum_mod_two_from_quotient_sums e
  3. L19
    specialize gauss_count_sum_mod_two_from_quotient_sums f
  4. L20
    specialize gauss_count_sum_mod_two_from_quotient_sums Q
  5. L21
    specialize gauss_count_sum_mod_two_from_quotient_sums U
  6. L22
    specialize gauss_count_sum_mod_two_from_quotient_sums h
  7. L23
    specialize gauss_count_sum_mod_two_from_quotient_sums k
  8. L24
    apply gauss_count_sum_mod_two_from_quotient_sums
  9. L25
    exact heq
  10. L26
    exact hfu
04Use earlier factsL27–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L27
    exact hsum
  2. L28
    specialize qres_same_status_from_mod_four_one p
  3. L29
    specialize qres_same_status_from_mod_four_one q
  4. L30
    specialize qres_same_status_from_mod_four_one e
  5. L31
    specialize qres_same_status_from_mod_four_one f
  6. L32
    specialize qres_same_status_from_mod_four_one h
  7. L33
    specialize qres_same_status_from_mod_four_one k
  8. L34
    apply qres_same_status_from_mod_four_one
  9. L35
    exact hp
  10. L36
    exact hq
05Use earlier factsL37–40

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L37
    exact heclass
  2. L38
    exact hfclass
  3. L39
    exact hcount
  4. L40
    exact hone

Library-wide reading audit

Original exact command ledger · 40 lines
  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