PA00FO · theorem

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.

Statement with defined notation

∀ p. ∀ q. ∀ e. ∀ f. ∀ h. ∀ k. p = 2 · h + 1 → q = 2 · k + 1 → (QRes(p,q) → Even(e)) ∧ (Even(e) → QRes(p,q)) ∧ ((¬QRes(p,q) → Odd(e)) ∧ (Odd(e) → ¬QRes(p,q))) → (QRes(q,p) → Even(f)) ∧ (Even(f) → QRes(q,p)) ∧ ((¬QRes(q,p) → Odd(f)) ∧ (Odd(f) → ¬QRes(q,p))) → ModEq(2,e + f,h · k) → Mod4One(p) ∨ Mod4One(q) → QRes(p,q) ∧ QRes(q,p) ∨ ¬QRes(p,q) ∧ ¬QRes(q,p)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq PD0009 Even PD0010 Odd PD0011 Mod4One PD0021 QRes

23 occurrences

In local proof propositions

PD0009 Even PD0011 Mod4One

11 occurrences

Exact expanded native-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))))

Proof neighborhood

Direct theorem prerequisites

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

PA00FP conditional_qres_same_status_from_oriented_gauss_counts

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : Even(h · k)Definitions: Even(h · k)Original native command in the exact edition
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 : (Even(h) → Mod4One(p)) ∧ (Mod4One(p) → Even(h))Definitions: Even(h)Mod4One(p)Original native command in the exact edition
  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
  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 : (Even(k) → Mod4One(q)) ∧ (Mod4One(q) → Even(k))Definitions: Even(k)Mod4One(q)Original native command in the exact edition
  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
  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 defined 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 : Even(h · k)
    Exact native replay linehave hproduct : exists qrp_even_half_product. h * k = 2 * qrp_even_half_product
  14. 0014cases hone
  15. 0015have hbridge : (Even(h) → Mod4One(p)) ∧ (Mod4One(p) → Even(h))
    Exact native replay linehave 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 : Even(h)
    Exact native replay linehave 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 : (Even(k) → Mod4One(q)) ∧ (Mod4One(q) → Even(k))
    Exact native replay linehave 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 : Even(k)
    Exact native replay linehave 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