PA00FS · theorem

qres_opposite_status_from_odd_count_sum

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

An odd sum of Gauss counts gives 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.

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))) → Odd(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_odd_count_sum. e + f = 2 * qrp_odd_count_sum + 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

PA00CD odd_sum_parity_cases

Direct theorem dependents

PA00FT qres_opposite_status_from_odd_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)
odd 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 odd sum parity cases.

  1. L14
    have hcases : Even(e) ∧ Odd(f) ∨ Odd(e) ∧ Even(f)Definitions: Even(e)Odd(f)Odd(e)Even(f)Original native command in the exact edition
  2. L15
    specialize odd_sum_parity_cases e
  3. L16
    specialize odd_sum_parity_cases f
  4. L17
    apply odd_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–24

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

  1. L23
    apply heclass_left_right
  2. L24
    exact hcases_left_left
06Fix variables and assumptionsL25–25

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

  1. L25
    intro hqp
07Use earlier factsL26–28

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

  1. L26
    apply hfclass_right_right
  2. L27
    exact hcases_left_right
  3. L28
    exact hqp
08Separate the logical casesL29–31

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

  1. L29
    cases hcases_right
  2. L30
    right
  3. L31
    split
09Fix variables and assumptionsL32–32

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

  1. L32
    intro hpq
10Use earlier factsL33–37

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

  1. L33
    apply heclass_right_right
  2. L34
    exact hcases_right_left
  3. L35
    exact hpq
  4. L36
    apply hfclass_left_right
  5. L37
    exact hcases_right_right

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) ∧ Odd(f) ∨ Odd(e) ∧ Even(f)
    Exact native replay linehave hcases : (((exists qrp_even_e_cases. e = 2 * qrp_even_e_cases) /\ (exists qrp_odd_f_cases. f = 2 * qrp_odd_f_cases + 1)) \/ ((exists qrp_odd_e_cases. e = 2 * qrp_odd_e_cases + 1) /\ (exists qrp_even_f_cases. f = 2 * qrp_even_f_cases)))
  15. 0015specialize odd_sum_parity_cases e
  16. 0016specialize odd_sum_parity_cases f
  17. 0017apply odd_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. 0025intro hqp
  26. 0026apply hfclass_right_right
  27. 0027exact hcases_left_right
  28. 0028exact hqp
  29. 0029cases hcases_right
  30. 0030right
  31. 0031split
  32. 0032intro hpq
  33. 0033apply heclass_right_right
  34. 0034exact hcases_right_left
  35. 0035exact hpq
  36. 0036apply hfclass_left_right
  37. 0037exact hcases_right_right