PA00FM · theorem

qres_same_status_from_even_count_sum

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

An even sum of Gauss counts gives 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. (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))) → Even(e + f) → 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

PD0009 Even PD0010 Odd PD0021 QRes

21 occurrences

In local proof propositions

PD0009 Even PD0010 Odd

4 occurrences

Exact expanded native-PA statement
forall p q e f. (((((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_even_count_sum. e + f = 2 * qrp_even_count_sum) -> ((((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

PA00CA even_sum_parity_cases

Direct theorem dependents

PA00FN qres_same_status_from_even_half_product_mod_two

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

37 script commands · 10 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.

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 (1)
even sum parity cases
01Fix variables and assumptionsL1–7

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 heclass
  6. L6
    intro hfclass
  7. L7
    intro hsum
02Separate the logical casesL8–13

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

  1. L8
    cases heclass
  2. L9
    cases heclass_left
  3. L10
    cases heclass_right
  4. L11
    cases hfclass
  5. L12
    cases hfclass_left
  6. L13
    cases hfclass_right
03Establish hcasesL14–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply even sum parity cases.

  1. L14
    have hcases : Even(e) ∧ Even(f) ∨ Odd(e) ∧ Odd(f)Definitions: Even(e)Even(f)Odd(e)Odd(f)Original native command in the exact edition
  2. L15
    specialize even_sum_parity_cases e
  3. L16
    specialize even_sum_parity_cases f
  4. L17
    apply even_sum_parity_cases
  5. L18
    exact hsum
04Separate the logical casesL19–22

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

  1. L19
    cases hcases
  2. L20
    cases hcases_left
  3. L21
    left
  4. L22
    split
05Use earlier factsL23–26

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

  1. L23
    apply heclass_left_right
  2. L24
    exact hcases_left_left
  3. L25
    apply hfclass_left_right
  4. L26
    exact hcases_left_right
06Separate the logical casesL27–29

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

  1. L27
    cases hcases_right
  2. L28
    right
  3. L29
    split
07Fix variables and assumptionsL30–30

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

  1. L30
    intro hpq
08Use earlier factsL31–33

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

  1. L31
    apply heclass_right_right
  2. L32
    exact hcases_right_left
  3. L33
    exact hpq
09Fix variables and assumptionsL34–34

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

  1. L34
    intro hqp
10Use earlier factsL35–37

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

  1. L35
    apply hfclass_right_right
  2. L36
    exact hcases_right_right
  3. L37
    exact hqp

Library-wide reading audit

Original defined command ledger · 37 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro heclass
  6. 0006intro hfclass
  7. 0007intro hsum
  8. 0008cases heclass
  9. 0009cases heclass_left
  10. 0010cases heclass_right
  11. 0011cases hfclass
  12. 0012cases hfclass_left
  13. 0013cases hfclass_right
  14. 0014have hcases : Even(e) ∧ Even(f) ∨ Odd(e) ∧ Odd(f)
    Exact native replay linehave hcases : (((exists qrp_even_e_cases. e = 2 * qrp_even_e_cases) /\ (exists qrp_even_f_cases. f = 2 * qrp_even_f_cases)) \/ ((exists qrp_odd_e_cases. e = 2 * qrp_odd_e_cases + 1) /\ (exists qrp_odd_f_cases. f = 2 * qrp_odd_f_cases + 1)))
  15. 0015specialize even_sum_parity_cases e
  16. 0016specialize even_sum_parity_cases f
  17. 0017apply even_sum_parity_cases
  18. 0018exact hsum
  19. 0019cases hcases
  20. 0020cases hcases_left
  21. 0021left
  22. 0022split
  23. 0023apply heclass_left_right
  24. 0024exact hcases_left_left
  25. 0025apply hfclass_left_right
  26. 0026exact hcases_left_right
  27. 0027cases hcases_right
  28. 0028right
  29. 0029split
  30. 0030intro hpq
  31. 0031apply heclass_right_right
  32. 0032exact hcases_right_left
  33. 0033exact hpq
  34. 0034intro hqp
  35. 0035apply hfclass_right_right
  36. 0036exact hcases_right_right
  37. 0037exact hqp