PA00FW · theorem

quadratic_reciprocity_combined

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

The exact sign-free two-case quadratic-reciprocity endpoint.

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. Prime(p) → Prime(q) → ¬p = q → Odd(p) → Odd(q) → (Mod4One(p) ∨ Mod4One(q) → QRes(p,q) ∧ QRes(q,p) ∨ ¬QRes(p,q) ∧ ¬QRes(q,p)) ∧ (Mod4Three(p) ∧ Mod4Three(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

PD0004 Prime PD0010 Odd PD0011 Mod4One PD0012 Mod4Three PD0021 QRes

16 occurrences

In local proof propositions

PD0008 ModEq PD0009 Even PD0010 Odd PD0021 QRes

18 occurrences

Exact expanded native-PA statement
forall p q. (~(p = 1) /\ forall qr_factor_a_prime_p qr_factor_b_prime_p. p = qr_factor_a_prime_p * qr_factor_b_prime_p -> qr_factor_a_prime_p = 1 \/ qr_factor_b_prime_p = 1) -> (~(q = 1) /\ forall qr_factor_a_prime_q qr_factor_b_prime_q. q = qr_factor_a_prime_q * qr_factor_b_prime_q -> qr_factor_a_prime_q = 1 \/ qr_factor_b_prime_q = 1) -> ~(p = q) -> (exists qr_half_odd_p. p = 2 * qr_half_odd_p + 1) -> (exists qr_half_odd_q. q = 2 * qr_half_odd_q + 1) -> ((((exists qr_mod4_one_p. p = 4 * qr_mod4_one_p + 1) \/ (exists qr_mod4_one_q. q = 4 * qr_mod4_one_q + 1)) -> (((exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ (exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)) \/ (~(exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ ~(exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)))) /\ ((((exists qr_mod4_three_p. p = 4 * qr_mod4_three_p + 3) /\ (exists qr_mod4_three_q. q = 4 * qr_mod4_three_q + 3)) -> (((exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ ~(exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p)) \/ (~(exists qr_x_p_q. exists qr_u_p_q qr_v_p_q. qr_x_p_q * qr_x_p_q + p * qr_u_p_q = q + p * qr_v_p_q) /\ (exists qr_x_q_p. exists qr_u_q_p qr_v_q_p. qr_x_q_p * qr_x_q_p + q * qr_u_q_p = p + q * qr_v_q_p))))))

Proof neighborhood

Direct theorem prerequisites

PA00FG distinct_odd_primes_gauss_eisenstein_data_exists PA00FP conditional_qres_same_status_from_oriented_gauss_counts PA00FV conditional_qres_opposite_status_from_oriented_gauss_counts

Direct theorem dependents

none

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

65 script commands · 11 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 (3)
distinct odd primes gauss eisenstein data existsconditional qres same status from oriented gauss countsconditional qres opposite status from oriented gauss counts
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 hp
  4. L4
    intro hq
  5. L5
    intro hpq
  6. L6
    intro hpodd
  7. L7
    intro hqodd
02Separate the logical casesL8–9

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

  1. L8
    cases hpodd
  2. L9
    cases hqodd
03Establish hdataL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply distinct odd primes gauss eisenstein data exists.

  1. L10
    have hdata : ∃ e. ∃ f. ∃ Q. ∃ U. (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 = x · x1)Definitions: QRes(p,q)Even(e)Odd(e)QRes(q,p)Even(f)Odd(f)ModEq(2,e,Q)ModEq(2,f,U)Original native command in the exact edition
  2. L11
    specialize distinct_odd_primes_gauss_eisenstein_data_exists p
  3. L12
    specialize distinct_odd_primes_gauss_eisenstein_data_exists q
  4. L13
    specialize distinct_odd_primes_gauss_eisenstein_data_exists x
  5. L14
    specialize distinct_odd_primes_gauss_eisenstein_data_exists x1
  6. L15
    apply distinct_odd_primes_gauss_eisenstein_data_exists
  7. L16
    exact hpodd_witness
  8. L17
    exact hqodd_witness
  9. L18
    exact hp
  10. L19
    exact hq
04Use earlier factsL20–20

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

  1. L20
    exact hpq
05Separate the logical casesL21–29

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

  1. L21
    cases hdata
  2. L22
    cases hdata_witness
  3. L23
    cases hdata_witness_witness
  4. L24
    cases hdata_witness_witness_witness
  5. L25
    cases hdata_witness_witness_witness_witness
  6. L26
    cases hdata_witness_witness_witness_witness_left
  7. L27
    cases hdata_witness_witness_witness_witness_right
  8. L28
    cases hdata_witness_witness_witness_witness_right_left
  9. L29
    split
06Fix variables and assumptionsL30–30

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

  1. L30
    intro hsame
07Use earlier factsL31–40

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

  1. L31
    specialize conditional_qres_same_status_from_oriented_gauss_counts p
  2. L32
    specialize conditional_qres_same_status_from_oriented_gauss_counts q
  3. L33
    specialize conditional_qres_same_status_from_oriented_gauss_counts x2
  4. L34
    specialize conditional_qres_same_status_from_oriented_gauss_counts x3
  5. L35
    specialize conditional_qres_same_status_from_oriented_gauss_counts x4
  6. L36
    specialize conditional_qres_same_status_from_oriented_gauss_counts x5
  7. L37
    specialize conditional_qres_same_status_from_oriented_gauss_counts x
  8. L38
    specialize conditional_qres_same_status_from_oriented_gauss_counts x1
  9. L39
    apply conditional_qres_same_status_from_oriented_gauss_counts
  10. L40
    exact hpodd_witness
08Use earlier factsL41–47

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

  1. L41
    exact hqodd_witness
  2. L42
    exact hdata_witness_witness_witness_witness_left_left
  3. L43
    exact hdata_witness_witness_witness_witness_left_right
  4. L44
    exact hdata_witness_witness_witness_witness_right_left_left
  5. L45
    exact hdata_witness_witness_witness_witness_right_left_right
  6. L46
    exact hdata_witness_witness_witness_witness_right_right
  7. L47
    exact hsame
09Fix variables and assumptionsL48–48

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

  1. L48
    intro hopposite
10Use earlier factsL49–58

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

  1. L49
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts p
  2. L50
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts q
  3. L51
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x2
  4. L52
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x3
  5. L53
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x4
  6. L54
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x5
  7. L55
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x
  8. L56
    specialize conditional_qres_opposite_status_from_oriented_gauss_counts x1
  9. L57
    apply conditional_qres_opposite_status_from_oriented_gauss_counts
  10. L58
    exact hpodd_witness
11Use earlier factsL59–65

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

  1. L59
    exact hqodd_witness
  2. L60
    exact hdata_witness_witness_witness_witness_left_left
  3. L61
    exact hdata_witness_witness_witness_witness_left_right
  4. L62
    exact hdata_witness_witness_witness_witness_right_left_left
  5. L63
    exact hdata_witness_witness_witness_witness_right_left_right
  6. L64
    exact hdata_witness_witness_witness_witness_right_right
  7. L65
    exact hopposite

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro p
  2. 0002intro q
  3. 0003intro hp
  4. 0004intro hq
  5. 0005intro hpq
  6. 0006intro hpodd
  7. 0007intro hqodd
  8. 0008cases hpodd
  9. 0009cases hqodd
  10. 0010have hdata : ∃ e. ∃ f. ∃ Q. ∃ U. (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 = x · x1)
    Exact native replay linehave hdata : exists e f Q U. (((((((exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first) -> (exists qr_even_first_even. e = 2 * qr_even_first_even)) /\ ((exists qr_even_first_even. e = 2 * qr_even_first_even) -> (exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first))) /\ (((~(exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first)) -> (exists qr_odd_first_odd. e = 2 * qr_odd_first_odd + 1)) /\ ((exists qr_odd_first_odd. e = 2 * qr_odd_first_odd + 1) -> ~(exists qr_x_qr_final_first. exists qr_u_qr_final_first qr_v_qr_final_first. qr_x_qr_final_first * qr_x_qr_final_first + p * qr_u_qr_final_first = q + p * qr_v_qr_final_first))))) /\ (((((exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second) -> (exists qr_even_second_even. f = 2 * qr_even_second_even)) /\ ((exists qr_even_second_even. f = 2 * qr_even_second_even) -> (exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second))) /\ (((~(exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second)) -> (exists qr_odd_second_odd. f = 2 * qr_odd_second_odd + 1)) /\ ((exists qr_odd_second_odd. f = 2 * qr_odd_second_odd + 1) -> ~(exists qr_x_qr_final_second. exists qr_u_qr_final_second qr_v_qr_final_second. qr_x_qr_final_second * qr_x_qr_final_second + q * qr_u_qr_final_second = p + q * qr_v_qr_final_second)))))) /\ (((exists qr_mod_u_first qr_mod_v_first. e + 2 * qr_mod_u_first = Q + 2 * qr_mod_v_first) /\ (exists qr_mod_u_second qr_mod_v_second. f + 2 * qr_mod_u_second = U + 2 * qr_mod_v_second)) /\ Q + U = x * x1))
  11. 0011specialize distinct_odd_primes_gauss_eisenstein_data_exists p
  12. 0012specialize distinct_odd_primes_gauss_eisenstein_data_exists q
  13. 0013specialize distinct_odd_primes_gauss_eisenstein_data_exists x
  14. 0014specialize distinct_odd_primes_gauss_eisenstein_data_exists x1
  15. 0015apply distinct_odd_primes_gauss_eisenstein_data_exists
  16. 0016exact hpodd_witness
  17. 0017exact hqodd_witness
  18. 0018exact hp
  19. 0019exact hq
  20. 0020exact hpq
  21. 0021cases hdata
  22. 0022cases hdata_witness
  23. 0023cases hdata_witness_witness
  24. 0024cases hdata_witness_witness_witness
  25. 0025cases hdata_witness_witness_witness_witness
  26. 0026cases hdata_witness_witness_witness_witness_left
  27. 0027cases hdata_witness_witness_witness_witness_right
  28. 0028cases hdata_witness_witness_witness_witness_right_left
  29. 0029split
  30. 0030intro hsame
  31. 0031specialize conditional_qres_same_status_from_oriented_gauss_counts p
  32. 0032specialize conditional_qres_same_status_from_oriented_gauss_counts q
  33. 0033specialize conditional_qres_same_status_from_oriented_gauss_counts x2
  34. 0034specialize conditional_qres_same_status_from_oriented_gauss_counts x3
  35. 0035specialize conditional_qres_same_status_from_oriented_gauss_counts x4
  36. 0036specialize conditional_qres_same_status_from_oriented_gauss_counts x5
  37. 0037specialize conditional_qres_same_status_from_oriented_gauss_counts x
  38. 0038specialize conditional_qres_same_status_from_oriented_gauss_counts x1
  39. 0039apply conditional_qres_same_status_from_oriented_gauss_counts
  40. 0040exact hpodd_witness
  41. 0041exact hqodd_witness
  42. 0042exact hdata_witness_witness_witness_witness_left_left
  43. 0043exact hdata_witness_witness_witness_witness_left_right
  44. 0044exact hdata_witness_witness_witness_witness_right_left_left
  45. 0045exact hdata_witness_witness_witness_witness_right_left_right
  46. 0046exact hdata_witness_witness_witness_witness_right_right
  47. 0047exact hsame
  48. 0048intro hopposite
  49. 0049specialize conditional_qres_opposite_status_from_oriented_gauss_counts p
  50. 0050specialize conditional_qres_opposite_status_from_oriented_gauss_counts q
  51. 0051specialize conditional_qres_opposite_status_from_oriented_gauss_counts x2
  52. 0052specialize conditional_qres_opposite_status_from_oriented_gauss_counts x3
  53. 0053specialize conditional_qres_opposite_status_from_oriented_gauss_counts x4
  54. 0054specialize conditional_qres_opposite_status_from_oriented_gauss_counts x5
  55. 0055specialize conditional_qres_opposite_status_from_oriented_gauss_counts x
  56. 0056specialize conditional_qres_opposite_status_from_oriented_gauss_counts x1
  57. 0057apply conditional_qres_opposite_status_from_oriented_gauss_counts
  58. 0058exact hpodd_witness
  59. 0059exact hqodd_witness
  60. 0060exact hdata_witness_witness_witness_witness_left_left
  61. 0061exact hdata_witness_witness_witness_witness_left_right
  62. 0062exact hdata_witness_witness_witness_witness_right_left_left
  63. 0063exact hdata_witness_witness_witness_witness_right_left_right
  64. 0064exact hdata_witness_witness_witness_witness_right_right
  65. 0065exact hopposite