PA00FP · theorem

conditional_qres_same_status_from_oriented_gauss_counts

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

Conditional one-mod-four reciprocity: the two cross-residue propositions have the same truth 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. ∀ Q. ∀ U. ∀ 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,Q) → ModEq(2,f,U) → Q + U = 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

24 occurrences

In local proof propositions

PD0008 ModEq

1 occurrences

Exact expanded native-PA statement
forall p q e f Q U h k. p = 2 * h + 1 -> q = 2 * k + 1 -> (((((exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) -> (exists qrc_even_e_even. e = 2 * qrc_even_e_even)) /\ ((exists qrc_even_e_even. e = 2 * qrc_even_e_even) -> (exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq))) /\ (((~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq)) -> (exists qrc_odd_e_odd. e = 2 * qrc_odd_e_odd + 1)) /\ ((exists qrc_odd_e_odd. e = 2 * qrc_odd_e_odd + 1) -> ~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq))))) -> (((((exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp) -> (exists qrc_even_f_even. f = 2 * qrc_even_f_even)) /\ ((exists qrc_even_f_even. f = 2 * qrc_even_f_even) -> (exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))) /\ (((~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp)) -> (exists qrc_odd_f_odd. f = 2 * qrc_odd_f_odd + 1)) /\ ((exists qrc_odd_f_odd. f = 2 * qrc_odd_f_odd + 1) -> ~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))))) -> (exists qrc_u_e_q qrc_v_e_q. e + 2 * qrc_u_e_q = Q + 2 * qrc_v_e_q) -> (exists qrc_u_f_u qrc_v_f_u. f + 2 * qrc_u_f_u = U + 2 * qrc_v_f_u) -> Q + U = h * k -> (((exists qrc_one_p. p = 4 * qrc_one_p + 1) \/ (exists qrc_one_q. q = 4 * qrc_one_q + 1))) -> ((((exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) /\ (exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp)) \/ (~(exists qr_x_qrc_pq. exists qr_u_qrc_pq qr_v_qrc_pq. qr_x_qrc_pq * qr_x_qrc_pq + p * qr_u_qrc_pq = q + p * qr_v_qrc_pq) /\ ~(exists qr_x_qrc_qp. exists qr_u_qrc_qp qr_v_qrc_qp. qr_x_qrc_qp * qr_x_qrc_qp + q * qr_u_qrc_qp = p + q * qr_v_qrc_qp))))

Proof neighborhood

Direct theorem prerequisites

PA00FH gauss_count_sum_mod_two_from_quotient_sums PA00FO qres_same_status_from_mod_four_one

Direct theorem dependents

PA00FW quadratic_reciprocity_combined

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

40 script commands · 5 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 (2)
gauss count sum mod two from quotient sumsqres same status from mod four one
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 Q
  6. L6
    intro U
  7. L7
    intro h
  8. L8
    intro k
  9. L9
    intro hp
  10. L10
    intro hq
02Fix variables and assumptionsL11–16

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

  1. L11
    intro heclass
  2. L12
    intro hfclass
  3. L13
    intro heq
  4. L14
    intro hfu
  5. L15
    intro hsum
  6. L16
    intro hone
03Establish hcountL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gauss count sum mod two from quotient sums.

  1. L17
    have hcount : ModEq(2,e + f,h · k)Definitions: ModEq(2,e + f,h · k)Original native command in the exact edition
  2. L18
    specialize gauss_count_sum_mod_two_from_quotient_sums e
  3. L19
    specialize gauss_count_sum_mod_two_from_quotient_sums f
  4. L20
    specialize gauss_count_sum_mod_two_from_quotient_sums Q
  5. L21
    specialize gauss_count_sum_mod_two_from_quotient_sums U
  6. L22
    specialize gauss_count_sum_mod_two_from_quotient_sums h
  7. L23
    specialize gauss_count_sum_mod_two_from_quotient_sums k
  8. L24
    apply gauss_count_sum_mod_two_from_quotient_sums
  9. L25
    exact heq
  10. L26
    exact hfu
04Use earlier factsL27–36

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

  1. L27
    exact hsum
  2. L28
    specialize qres_same_status_from_mod_four_one p
  3. L29
    specialize qres_same_status_from_mod_four_one q
  4. L30
    specialize qres_same_status_from_mod_four_one e
  5. L31
    specialize qres_same_status_from_mod_four_one f
  6. L32
    specialize qres_same_status_from_mod_four_one h
  7. L33
    specialize qres_same_status_from_mod_four_one k
  8. L34
    apply qres_same_status_from_mod_four_one
  9. L35
    exact hp
  10. L36
    exact hq
05Use earlier factsL37–40

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

  1. L37
    exact heclass
  2. L38
    exact hfclass
  3. L39
    exact hcount
  4. L40
    exact hone

Library-wide reading audit

Original defined command ledger · 40 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro e
  4. 0004intro f
  5. 0005intro Q
  6. 0006intro U
  7. 0007intro h
  8. 0008intro k
  9. 0009intro hp
  10. 0010intro hq
  11. 0011intro heclass
  12. 0012intro hfclass
  13. 0013intro heq
  14. 0014intro hfu
  15. 0015intro hsum
  16. 0016intro hone
  17. 0017have hcount : ModEq(2,e + f,h · k)
    Exact native replay linehave hcount : exists qrc_u_count_product qrc_v_count_product. e + f + 2 * qrc_u_count_product = h * k + 2 * qrc_v_count_product
  18. 0018specialize gauss_count_sum_mod_two_from_quotient_sums e
  19. 0019specialize gauss_count_sum_mod_two_from_quotient_sums f
  20. 0020specialize gauss_count_sum_mod_two_from_quotient_sums Q
  21. 0021specialize gauss_count_sum_mod_two_from_quotient_sums U
  22. 0022specialize gauss_count_sum_mod_two_from_quotient_sums h
  23. 0023specialize gauss_count_sum_mod_two_from_quotient_sums k
  24. 0024apply gauss_count_sum_mod_two_from_quotient_sums
  25. 0025exact heq
  26. 0026exact hfu
  27. 0027exact hsum
  28. 0028specialize qres_same_status_from_mod_four_one p
  29. 0029specialize qres_same_status_from_mod_four_one q
  30. 0030specialize qres_same_status_from_mod_four_one e
  31. 0031specialize qres_same_status_from_mod_four_one f
  32. 0032specialize qres_same_status_from_mod_four_one h
  33. 0033specialize qres_same_status_from_mod_four_one k
  34. 0034apply qres_same_status_from_mod_four_one
  35. 0035exact hp
  36. 0036exact hq
  37. 0037exact heclass
  38. 0038exact hfclass
  39. 0039exact hcount
  40. 0040exact hone