PA00FU

qres_opposite_status_from_mod_four_three

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

Two three-mod-four inputs force opposite cross-residue 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 h k. p = 2 * h + 1 -> q = 2 * k + 1 -> (((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) -> (exists qrp_even_e_even. e = 2 * qrp_even_e_even)) /\ ((exists qrp_even_e_even. e = 2 * qrp_even_e_even) -> (exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))) /\ (((~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq)) -> (exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1)) /\ ((exists qrp_odd_e_odd. e = 2 * qrp_odd_e_odd + 1) -> ~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq))))) -> (((((exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp) -> (exists qrp_even_f_even. f = 2 * qrp_even_f_even)) /\ ((exists qrp_even_f_even. f = 2 * qrp_even_f_even) -> (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))) /\ (((~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) -> (exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1)) /\ ((exists qrp_odd_f_odd. f = 2 * qrp_odd_f_odd + 1) -> ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))) -> (exists qrp_u_count_product qrp_v_count_product. e + f + 2 * qrp_u_count_product = h * k + 2 * qrp_v_count_product) -> ((exists qrp_three_p. p = 4 * qrp_three_p + 3) /\ (exists qrp_three_q. q = 4 * qrp_three_q + 3)) -> ((((exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ ~(exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp)) \/ (~(exists qr_x_qrp_pq. exists qr_u_qrp_pq qr_v_qrp_pq. qr_x_qrp_pq * qr_x_qrp_pq + p * qr_u_qrp_pq = q + p * qr_v_qrp_pq) /\ (exists qr_x_qrp_qp. exists qr_u_qrp_qp qr_v_qrp_qp. qr_x_qrp_qp * qr_x_qrp_qp + q * qr_u_qrp_qp = p + q * qr_v_qrp_qp))))

Structural proof guide

Generated structural guide

Two three-mod-four inputs force opposite cross-residue status.

Use the direct prerequisites odd_half_odd_iff_mod4_three, odd_mul_odd, qres_opposite_status_from_odd_half_product_mod_two as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (5).

Referenced ingredients

PA00FR odd_half_odd_iff_mod4_three PA006D odd_mul_odd PA00FT qres_opposite_status_from_odd_half_product_mod_two

Proof neighborhood

Direct dependencies

PA00FR odd_half_odd_iff_mod4_three PA006D odd_mul_odd PA00FT qres_opposite_status_from_odd_half_product_mod_two

Direct dependents

PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

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

48 script commands · 11 reading checkpoints · 5 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 (3)
odd half odd iff mod4 threeodd mul oddqres opposite status from odd half product mod two
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 h
  6. L6
    intro k
  7. L7
    intro hp
  8. L8
    intro hq
  9. L9
    intro heclass
  10. L10
    intro hfclass
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hmod
  2. L12
    intro hthree
03Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases hthree
04Establish hpbridgeL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half odd iff mod4 three.

  1. L14
    have hpbridge : (((exists qrp_odd_h. h = 2 * qrp_odd_h + 1) -> (exists qrp_three_p. p = 4 * qrp_three_p + 3)) /\ ((exists qrp_three_p. p = 4 * qrp_three_p + 3) -> (exists qrp_odd_h. h = 2 * qrp_odd_h + 1)))
  2. L15
    specialize odd_half_odd_iff_mod4_three p
  3. L16
    specialize odd_half_odd_iff_mod4_three h
  4. L17
    apply odd_half_odd_iff_mod4_three
  5. L18
    exact hp
05Separate the logical casesL19–19

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hpbridge
06Establish hpoddL20–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hpbridge right.

  1. L20
    have hpodd : exists qrp_odd_h. h = 2 * qrp_odd_h + 1
  2. L21
    apply hpbridge_right
  3. L22
    exact hthree_left
07Establish hqbridgeL23–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half odd iff mod4 three.

  1. L23
    have hqbridge : (((exists qrp_odd_k. k = 2 * qrp_odd_k + 1) -> (exists qrp_three_q. q = 4 * qrp_three_q + 3)) /\ ((exists qrp_three_q. q = 4 * qrp_three_q + 3) -> (exists qrp_odd_k. k = 2 * qrp_odd_k + 1)))
  2. L24
    specialize odd_half_odd_iff_mod4_three q
  3. L25
    specialize odd_half_odd_iff_mod4_three k
  4. L26
    apply odd_half_odd_iff_mod4_three
  5. L27
    exact hq
08Separate the logical casesL28–28

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L28
    cases hqbridge
09Establish hqoddL29–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hqbridge right.

  1. L29
    have hqodd : exists qrp_odd_k. k = 2 * qrp_odd_k + 1
  2. L30
    apply hqbridge_right
  3. L31
    exact hthree_right
10Establish hproductL32–41

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd mul odd.

  1. L32
    have hproduct : exists qrp_odd_half_product. h * k = 2 * qrp_odd_half_product + 1
  2. L33
    specialize odd_mul_odd h
  3. L34
    specialize odd_mul_odd k
  4. L35
    apply odd_mul_odd
  5. L36
    exact hpodd
  6. L37
    exact hqodd
  7. L38
    specialize qres_opposite_status_from_odd_half_product_mod_two p
  8. L39
    specialize qres_opposite_status_from_odd_half_product_mod_two q
  9. L40
    specialize qres_opposite_status_from_odd_half_product_mod_two e
  10. L41
    specialize qres_opposite_status_from_odd_half_product_mod_two f
11Use earlier factsL42–48

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

  1. L42
    specialize qres_opposite_status_from_odd_half_product_mod_two h
  2. L43
    specialize qres_opposite_status_from_odd_half_product_mod_two k
  3. L44
    apply qres_opposite_status_from_odd_half_product_mod_two
  4. L45
    exact heclass
  5. L46
    exact hfclass
  6. L47
    exact hmod
  7. L48
    exact hproduct

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro h
  6. 0006intro k
  7. 0007intro hp
  8. 0008intro hq
  9. 0009intro heclass
  10. 0010intro hfclass
  11. 0011intro hmod
  12. 0012intro hthree
  13. 0013cases hthree
  14. 0014have hpbridge : (((exists qrp_odd_h. h = 2 * qrp_odd_h + 1) -> (exists qrp_three_p. p = 4 * qrp_three_p + 3)) /\ ((exists qrp_three_p. p = 4 * qrp_three_p + 3) -> (exists qrp_odd_h. h = 2 * qrp_odd_h + 1)))
  15. 0015specialize odd_half_odd_iff_mod4_three p
  16. 0016specialize odd_half_odd_iff_mod4_three h
  17. 0017apply odd_half_odd_iff_mod4_three
  18. 0018exact hp
  19. 0019cases hpbridge
  20. 0020have hpodd : exists qrp_odd_h. h = 2 * qrp_odd_h + 1
  21. 0021apply hpbridge_right
  22. 0022exact hthree_left
  23. 0023have hqbridge : (((exists qrp_odd_k. k = 2 * qrp_odd_k + 1) -> (exists qrp_three_q. q = 4 * qrp_three_q + 3)) /\ ((exists qrp_three_q. q = 4 * qrp_three_q + 3) -> (exists qrp_odd_k. k = 2 * qrp_odd_k + 1)))
  24. 0024specialize odd_half_odd_iff_mod4_three q
  25. 0025specialize odd_half_odd_iff_mod4_three k
  26. 0026apply odd_half_odd_iff_mod4_three
  27. 0027exact hq
  28. 0028cases hqbridge
  29. 0029have hqodd : exists qrp_odd_k. k = 2 * qrp_odd_k + 1
  30. 0030apply hqbridge_right
  31. 0031exact hthree_right
  32. 0032have hproduct : exists qrp_odd_half_product. h * k = 2 * qrp_odd_half_product + 1
  33. 0033specialize odd_mul_odd h
  34. 0034specialize odd_mul_odd k
  35. 0035apply odd_mul_odd
  36. 0036exact hpodd
  37. 0037exact hqodd
  38. 0038specialize qres_opposite_status_from_odd_half_product_mod_two p
  39. 0039specialize qres_opposite_status_from_odd_half_product_mod_two q
  40. 0040specialize qres_opposite_status_from_odd_half_product_mod_two e
  41. 0041specialize qres_opposite_status_from_odd_half_product_mod_two f
  42. 0042specialize qres_opposite_status_from_odd_half_product_mod_two h
  43. 0043specialize qres_opposite_status_from_odd_half_product_mod_two k
  44. 0044apply qres_opposite_status_from_odd_half_product_mod_two
  45. 0045exact heclass
  46. 0046exact hfclass
  47. 0047exact hmod
  48. 0048exact hproduct