PA00FO

qres_same_status_from_mod_four_one

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

A one-mod-four input forces equal 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_one_p. p = 4 * qrp_one_p + 1) \/ (exists qrp_one_q. q = 4 * qrp_one_q + 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 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

A one-mod-four input forces equal cross-residue status.

Use the direct prerequisites odd_half_even_iff_mod4_one, even_mul_left, even_mul_right, qres_same_status_from_even_half_product_mod_two as previously established PA formulas.

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

Referenced ingredients

PA00FJ odd_half_even_iff_mod4_one PA006U even_mul_left PA006E even_mul_right PA00FN qres_same_status_from_even_half_product_mod_two

Proof neighborhood

Direct dependencies

PA00FJ odd_half_even_iff_mod4_one PA006U even_mul_left PA006E even_mul_right PA00FN qres_same_status_from_even_half_product_mod_two

Direct dependents

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

51 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 (4)
odd half even iff mod4 oneeven mul lefteven mul rightqres same status from even 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 hone
03Establish hproductL13–13

Establish this local claim before using it. It is not an additional assumption.

  1. L13
    have hproduct : exists qrp_even_half_product. h * k = 2 * qrp_even_half_product
04Separate the logical casesL14–14

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

  1. L14
    cases hone
05Establish hbridgeL15–19

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

  1. L15
    have hbridge : (((exists qrp_even_h. h = 2 * qrp_even_h) -> (exists qrp_one_p. p = 4 * qrp_one_p + 1)) /\ ((exists qrp_one_p. p = 4 * qrp_one_p + 1) -> (exists qrp_even_h. h = 2 * qrp_even_h)))
  2. L16
    specialize odd_half_even_iff_mod4_one p
  3. L17
    specialize odd_half_even_iff_mod4_one h
  4. L18
    apply odd_half_even_iff_mod4_one
  5. L19
    exact hp
06Separate the logical casesL20–20

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

  1. L20
    cases hbridge
07Establish hhalfL21–27

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

  1. L21
    have hhalf : exists qrp_even_h. h = 2 * qrp_even_h
  2. L22
    apply hbridge_right
  3. L23
    exact hone_left
  4. L24
    specialize even_mul_left h
  5. L25
    specialize even_mul_left k
  6. L26
    apply even_mul_left
  7. L27
    exact hhalf
08Establish hbridgeL28–32

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

  1. L28
    have hbridge : (((exists qrp_even_k. k = 2 * qrp_even_k) -> (exists qrp_one_q. q = 4 * qrp_one_q + 1)) /\ ((exists qrp_one_q. q = 4 * qrp_one_q + 1) -> (exists qrp_even_k. k = 2 * qrp_even_k)))
  2. L29
    specialize odd_half_even_iff_mod4_one q
  3. L30
    specialize odd_half_even_iff_mod4_one k
  4. L31
    apply odd_half_even_iff_mod4_one
  5. L32
    exact hq
09Separate the logical casesL33–33

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

  1. L33
    cases hbridge
10Establish hhalfL34–43

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

  1. L34
    have hhalf : exists qrp_even_k. k = 2 * qrp_even_k
  2. L35
    apply hbridge_right
  3. L36
    exact hone_right
  4. L37
    specialize even_mul_right h
  5. L38
    specialize even_mul_right k
  6. L39
    apply even_mul_right
  7. L40
    exact hhalf
  8. L41
    specialize qres_same_status_from_even_half_product_mod_two p
  9. L42
    specialize qres_same_status_from_even_half_product_mod_two q
  10. L43
    specialize qres_same_status_from_even_half_product_mod_two e
11Use earlier factsL44–51

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

  1. L44
    specialize qres_same_status_from_even_half_product_mod_two f
  2. L45
    specialize qres_same_status_from_even_half_product_mod_two h
  3. L46
    specialize qres_same_status_from_even_half_product_mod_two k
  4. L47
    apply qres_same_status_from_even_half_product_mod_two
  5. L48
    exact heclass
  6. L49
    exact hfclass
  7. L50
    exact hmod
  8. L51
    exact hproduct

Library-wide reading audit

Original exact command ledger · 51 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 hone
  13. 0013have hproduct : exists qrp_even_half_product. h * k = 2 * qrp_even_half_product
  14. 0014cases hone
  15. 0015have hbridge : (((exists qrp_even_h. h = 2 * qrp_even_h) -> (exists qrp_one_p. p = 4 * qrp_one_p + 1)) /\ ((exists qrp_one_p. p = 4 * qrp_one_p + 1) -> (exists qrp_even_h. h = 2 * qrp_even_h)))
  16. 0016specialize odd_half_even_iff_mod4_one p
  17. 0017specialize odd_half_even_iff_mod4_one h
  18. 0018apply odd_half_even_iff_mod4_one
  19. 0019exact hp
  20. 0020cases hbridge
  21. 0021have hhalf : exists qrp_even_h. h = 2 * qrp_even_h
  22. 0022apply hbridge_right
  23. 0023exact hone_left
  24. 0024specialize even_mul_left h
  25. 0025specialize even_mul_left k
  26. 0026apply even_mul_left
  27. 0027exact hhalf
  28. 0028have hbridge : (((exists qrp_even_k. k = 2 * qrp_even_k) -> (exists qrp_one_q. q = 4 * qrp_one_q + 1)) /\ ((exists qrp_one_q. q = 4 * qrp_one_q + 1) -> (exists qrp_even_k. k = 2 * qrp_even_k)))
  29. 0029specialize odd_half_even_iff_mod4_one q
  30. 0030specialize odd_half_even_iff_mod4_one k
  31. 0031apply odd_half_even_iff_mod4_one
  32. 0032exact hq
  33. 0033cases hbridge
  34. 0034have hhalf : exists qrp_even_k. k = 2 * qrp_even_k
  35. 0035apply hbridge_right
  36. 0036exact hone_right
  37. 0037specialize even_mul_right h
  38. 0038specialize even_mul_right k
  39. 0039apply even_mul_right
  40. 0040exact hhalf
  41. 0041specialize qres_same_status_from_even_half_product_mod_two p
  42. 0042specialize qres_same_status_from_even_half_product_mod_two q
  43. 0043specialize qres_same_status_from_even_half_product_mod_two e
  44. 0044specialize qres_same_status_from_even_half_product_mod_two f
  45. 0045specialize qres_same_status_from_even_half_product_mod_two h
  46. 0046specialize qres_same_status_from_even_half_product_mod_two k
  47. 0047apply qres_same_status_from_even_half_product_mod_two
  48. 0048exact heclass
  49. 0049exact hfclass
  50. 0050exact hmod
  51. 0051exact hproduct