PA00FV

conditional_qres_opposite_status_from_oriented_gauss_counts

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

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

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_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-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 opposite status from mod four three
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 hthree
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_opposite_status_from_mod_four_three p
  3. L29
    specialize qres_opposite_status_from_mod_four_three q
  4. L30
    specialize qres_opposite_status_from_mod_four_three e
  5. L31
    specialize qres_opposite_status_from_mod_four_three f
  6. L32
    specialize qres_opposite_status_from_mod_four_three h
  7. L33
    specialize qres_opposite_status_from_mod_four_three k
  8. L34
    apply qres_opposite_status_from_mod_four_three
  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 hthree

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 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