SL0003 · theorem body

quadratic_supplement_minus_one_half_parity

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

For an odd prime, its predecessor is a quadratic residue exactly when the prime's half is even, and a nonresidue exactly when that half is odd.

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. ∀ n. ∀ h. p = S n → Prime(p) → n = h + h → (QRes(p,n) → Even(h)) ∧ (Even(h) → QRes(p,n)) ∧ ((¬QRes(p,n) → Odd(h)) ∧ (Odd(h) → ¬QRes(p,n)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0004 Prime PD0009 Even PD0010 Odd PD0021 QRes

In local proof propositions

PD0002 Lt PD0008 ModEq PD0009 Even PD0010 Odd PD0020 Pow PD0021 QRes
Exact expanded first-order statement
forall p n h. p = S n -> ((~(p = 1) /\ forall frm_prime_left_qsm_prime frm_prime_right_qsm_prime. p = frm_prime_left_qsm_prime * frm_prime_right_qsm_prime -> frm_prime_left_qsm_prime = 1 \/ frm_prime_right_qsm_prime = 1)) -> n = h + h -> ((((((exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor) -> (exists qsm_even_half. h = 2 * qsm_even_half)) /\ ((exists qsm_even_half. h = 2 * qsm_even_half) -> (exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)))) /\ ((((~(exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)) -> (exists qsm_odd_half. h = 2 * qsm_odd_half + 1)) /\ ((exists qsm_odd_half. h = 2 * qsm_odd_half + 1) -> (~(exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)))))))

Proof neighborhood

Direct theorem prerequisites

SL0001 prime_predecessor_nonzero pow_exists · Stable closed SL0000 bounded_euler_criterion_complete pow_predecessor_parity_mod · Stable closed parity_cases · Stable closed zero_add · Stable closed

Direct theorem dependents

SL0004 quadratic_supplement_minus_one_residue_iff_mod_four_one SL0005 quadratic_supplement_minus_one_nonresidue_iff_mod_four_three

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

91 script commands · 37 reading checkpoints · 6 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)
prime predecessor nonzerobounded euler criterion complete
01Fix variables and assumptionsL1–6

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro h
  4. L4
    intro hpredecessor
  5. L5
    intro hprime
  6. L6
    intro hdouble
02Establish hnonzeroL7–14

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime predecessor nonzero.

  1. L7
    have hnonzero : ~(n = 0)
  2. L8
    intro hzero
  3. L9
    specialize prime_predecessor_nonzero p
  4. L10
    specialize prime_predecessor_nonzero n
  5. L11
    apply prime_predecessor_nonzero
  6. L12
    exact hpredecessor
  7. L13
    exact hprime
  8. L14
    exact hzero
03Establish hboundL15–15

Establish this local claim before using it. It is not an additional assumption.

  1. L15
    have hbound : Lt(n,p)Definitions: Lt(n,p)Original native command in the exact edition
04Construct an explicit witnessL16–16

Supply the displayed value, then prove that it has the required property.

  1. L16
    exists 0
05Calculate and transport equalitiesL17–17

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L17
    trans S n
06Use earlier factsL18–18

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

  1. L18
    apply zero_add
07Calculate and transport equalitiesL19–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L19
    symm
08Use earlier factsL20–20

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

  1. L20
    exact hpredecessor
09Establish hpowerL21–24

Establish this local claim before using it. It is not an additional assumption.

  1. L21
    have hpower : ∃ A. Pow(n,h,A)Definitions: Pow(n,h,A)Original native command in the exact edition
  2. L22
    specialize pow_exists n
  3. L23
    specialize pow_exists h
  4. L24
    exact pow_exists
10Separate the logical casesL25–25

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

  1. L25
    cases hpower
11Establish heulerL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded euler criterion complete.

  1. L26
    have heuler : (QRes(p,n) → ModEq(p,x,1)) ∧ (ModEq(p,x,1) → QRes(p,n)) ∧ ((¬QRes(p,n) → ModEq(p,x,n)) ∧ (ModEq(p,x,n) → ¬QRes(p,n)))Definitions: QRes(p,n)ModEq(p,x,1)ModEq(p,x,n)Original native command in the exact edition
  2. L27
    specialize bounded_euler_criterion_complete p
  3. L28
    specialize bounded_euler_criterion_complete n
  4. L29
    specialize bounded_euler_criterion_complete n
  5. L30
    specialize bounded_euler_criterion_complete h
  6. L31
    specialize bounded_euler_criterion_complete x
  7. L32
    apply bounded_euler_criterion_complete
  8. L33
    exact hpredecessor
  9. L34
    exact hprime
  10. L35
    exact hnonzero
12Use earlier factsL36–38

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

  1. L36
    exact hbound
  2. L37
    exact hdouble
  3. L38
    exact hpower_witness
13Separate the logical casesL39–41

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

  1. L39
    cases heuler
  2. L40
    cases heuler_left
  3. L41
    cases heuler_right
14Establish hsignL42–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow predecessor parity mod.

  1. L42
    have hsign : (Even(h) → ModEq(p,x,1)) ∧ (Odd(h) → ModEq(p,x,n))Definitions: Even(h)ModEq(p,x,1)Odd(h)ModEq(p,x,n)Original native command in the exact edition
  2. L43
    specialize pow_predecessor_parity_mod p
  3. L44
    specialize pow_predecessor_parity_mod n
  4. L45
    specialize pow_predecessor_parity_mod h
  5. L46
    specialize pow_predecessor_parity_mod x
  6. L47
    apply pow_predecessor_parity_mod
  7. L48
    exact hpredecessor
  8. L49
    exact hpower_witness
15Separate the logical casesL50–52

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

  1. L50
    cases hsign
  2. L51
    split
  3. L52
    split
16Fix variables and assumptionsL53–53

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

  1. L53
    intro hresidue
17Use earlier factsL54–54

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

  1. L54
    specialize parity_cases h
18Separate the logical casesL55–56

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

  1. L55
    cases parity_cases
  2. L56
    cases parity_cases_witness
19Construct an explicit witnessL57–57

Supply the displayed value, then prove that it has the required property.

  1. L57
    exists x1
20Use earlier factsL58–58

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

  1. L58
    exact parity_cases_witness_left
21Separate the logical casesL59–59

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

  1. L59
    exfalso
22Establish hnotresidueL60–63

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply heuler right right.

  1. L60
    have hnotresidue : ¬QRes(p,n)Definitions: QRes(p,n)Original native command in the exact edition
  2. L61
    intro hresidue_again
  3. L62
    apply heuler_right_right
  4. L63
    apply hsign_right
23Construct an explicit witnessL64–64

Supply the displayed value, then prove that it has the required property.

  1. L64
    exists x1
24Use earlier factsL65–68

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

  1. L65
    exact parity_cases_witness_right
  2. L66
    exact hresidue_again
  3. L67
    apply hnotresidue
  4. L68
    exact hresidue
25Fix variables and assumptionsL69–69

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

  1. L69
    intro heven
26Use earlier factsL70–72

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

  1. L70
    apply heuler_left_right
  2. L71
    apply hsign_left
  3. L72
    exact heven
27Separate the logical casesL73–73

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

  1. L73
    split
28Fix variables and assumptionsL74–74

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

  1. L74
    intro hnotresidue
29Use earlier factsL75–75

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

  1. L75
    specialize parity_cases h
30Separate the logical casesL76–78

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

  1. L76
    cases parity_cases
  2. L77
    cases parity_cases_witness
  3. L78
    exfalso
31Use earlier factsL79–81

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

  1. L79
    apply hnotresidue
  2. L80
    apply heuler_left_right
  3. L81
    apply hsign_left
32Construct an explicit witnessL82–82

Supply the displayed value, then prove that it has the required property.

  1. L82
    exists x1
33Use earlier factsL83–83

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

  1. L83
    exact parity_cases_witness_left
34Construct an explicit witnessL84–84

Supply the displayed value, then prove that it has the required property.

  1. L84
    exists x1
35Use earlier factsL85–85

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

  1. L85
    exact parity_cases_witness_right
36Fix variables and assumptionsL86–87

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

  1. L86
    intro hodd
  2. L87
    intro hresidue
37Use earlier factsL88–91

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

  1. L88
    apply heuler_right_right
  2. L89
    apply hsign_right
  3. L90
    exact hodd
  4. L91
    exact hresidue

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro h
  4. 0004intro hpredecessor
  5. 0005intro hprime
  6. 0006intro hdouble
  7. 0007have hnonzero : ~(n = 0)
  8. 0008intro hzero
  9. 0009specialize prime_predecessor_nonzero p
  10. 0010specialize prime_predecessor_nonzero n
  11. 0011apply prime_predecessor_nonzero
  12. 0012exact hpredecessor
  13. 0013exact hprime
  14. 0014exact hzero
  15. 0015have hbound : Lt(n,p)
    Exact native replay linehave hbound : exists wpo_gap_qsm_predecessor_bound. wpo_gap_qsm_predecessor_bound + S (n) = p
  16. 0016exists 0
  17. 0017trans S n
  18. 0018apply zero_add
  19. 0019symm
  20. 0020exact hpredecessor
  21. 0021have hpower : ∃ A. Pow(n,h,A)
    Exact native replay linehave hpower : exists A. (exists ff_b_qsm_exists_power ff_c_qsm_exists_power. ((forall ff_i_qsm_exists_power_repeat. (exists ff_lt_qsm_exists_power_repeat_bound. ff_lt_qsm_exists_power_repeat_bound + S ff_i_qsm_exists_power_repeat = h) -> (((exists ff_h_qsm_exists_power_repeat_decoded. ff_h_qsm_exists_power_repeat_decoded + S (n) = S ((S (ff_i_qsm_exists_power_repeat)) * ff_c_qsm_exists_power)) /\ exists ff_q_qsm_exists_power_repeat_decoded. ff_b_qsm_exists_power = ff_q_qsm_exists_power_repeat_decoded * S ((S (ff_i_qsm_exists_power_repeat)) * ff_c_qsm_exists_power) + (n)))) /\ (exists ff_u_qsm_exists_power_product ff_v_qsm_exists_power_product. ((((exists ff_h_qsm_exists_power_product_start. ff_h_qsm_exists_power_product_start + S (1) = S ((S (0)) * ff_v_qsm_exists_power_product)) /\ exists ff_q_qsm_exists_power_product_start. ff_u_qsm_exists_power_product = ff_q_qsm_exists_power_product_start * S ((S (0)) * ff_v_qsm_exists_power_product) + (1))) /\ ((((exists ff_h_qsm_exists_power_product_terminal. ff_h_qsm_exists_power_product_terminal + S (A) = S ((S (h)) * ff_v_qsm_exists_power_product)) /\ exists ff_q_qsm_exists_power_product_terminal. ff_u_qsm_exists_power_product = ff_q_qsm_exists_power_product_terminal * S ((S (h)) * ff_v_qsm_exists_power_product) + (A))) /\ forall ff_i_qsm_exists_power_product. (exists ff_lt_qsm_exists_power_product_bound. ff_lt_qsm_exists_power_product_bound + S ff_i_qsm_exists_power_product = h) -> exists ff_p_qsm_exists_power_product ff_r_qsm_exists_power_product ff_s_qsm_exists_power_product. ((((exists ff_h_qsm_exists_power_product_factor. ff_h_qsm_exists_power_product_factor + S (ff_p_qsm_exists_power_product) = S ((S (ff_i_qsm_exists_power_product)) * ff_c_qsm_exists_power)) /\ exists ff_q_qsm_exists_power_product_factor. ff_b_qsm_exists_power = ff_q_qsm_exists_power_product_factor * S ((S (ff_i_qsm_exists_power_product)) * ff_c_qsm_exists_power) + (ff_p_qsm_exists_power_product))) /\ ((((exists ff_h_qsm_exists_power_product_partial. ff_h_qsm_exists_power_product_partial + S (ff_r_qsm_exists_power_product) = S ((S (ff_i_qsm_exists_power_product)) * ff_v_qsm_exists_power_product)) /\ exists ff_q_qsm_exists_power_product_partial. ff_u_qsm_exists_power_product = ff_q_qsm_exists_power_product_partial * S ((S (ff_i_qsm_exists_power_product)) * ff_v_qsm_exists_power_product) + (ff_r_qsm_exists_power_product))) /\ ((((exists ff_h_qsm_exists_power_product_successor. ff_h_qsm_exists_power_product_successor + S (ff_s_qsm_exists_power_product) = S ((S (S ff_i_qsm_exists_power_product)) * ff_v_qsm_exists_power_product)) /\ exists ff_q_qsm_exists_power_product_successor. ff_u_qsm_exists_power_product = ff_q_qsm_exists_power_product_successor * S ((S (S ff_i_qsm_exists_power_product)) * ff_v_qsm_exists_power_product) + (ff_s_qsm_exists_power_product))) /\ ff_s_qsm_exists_power_product = ff_r_qsm_exists_power_product * ff_p_qsm_exists_power_product))))))))
  22. 0022specialize pow_exists n
  23. 0023specialize pow_exists h
  24. 0024exact pow_exists
  25. 0025cases hpower
  26. 0026have heuler : (QRes(p,n) → ModEq(p,x,1)) ∧ (ModEq(p,x,1) → QRes(p,n)) ∧ ((¬QRes(p,n) → ModEq(p,x,n)) ∧ (ModEq(p,x,n) → ¬QRes(p,n)))
    Exact native replay linehave heuler : (((((exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor) -> (exists wpp_mod_left_qsm_mod_one wpp_mod_right_qsm_mod_one. (x) + p * wpp_mod_left_qsm_mod_one = (1) + p * wpp_mod_right_qsm_mod_one)) /\ ((exists wpp_mod_left_qsm_mod_one wpp_mod_right_qsm_mod_one. (x) + p * wpp_mod_left_qsm_mod_one = (1) + p * wpp_mod_right_qsm_mod_one) -> (exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)))) /\ ((((~(exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)) -> (exists wpp_mod_left_qsm_mod_predecessor wpp_mod_right_qsm_mod_predecessor. (x) + p * wpp_mod_left_qsm_mod_predecessor = (n) + p * wpp_mod_right_qsm_mod_predecessor)) /\ ((exists wpp_mod_left_qsm_mod_predecessor wpp_mod_right_qsm_mod_predecessor. (x) + p * wpp_mod_left_qsm_mod_predecessor = (n) + p * wpp_mod_right_qsm_mod_predecessor) -> (~(exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor))))))
  27. 0027specialize bounded_euler_criterion_complete p
  28. 0028specialize bounded_euler_criterion_complete n
  29. 0029specialize bounded_euler_criterion_complete n
  30. 0030specialize bounded_euler_criterion_complete h
  31. 0031specialize bounded_euler_criterion_complete x
  32. 0032apply bounded_euler_criterion_complete
  33. 0033exact hpredecessor
  34. 0034exact hprime
  35. 0035exact hnonzero
  36. 0036exact hbound
  37. 0037exact hdouble
  38. 0038exact hpower_witness
  39. 0039cases heuler
  40. 0040cases heuler_left
  41. 0041cases heuler_right
  42. 0042have hsign : (Even(h) → ModEq(p,x,1)) ∧ (Odd(h) → ModEq(p,x,n))
    Exact native replay linehave hsign : (((exists qsm_even_half. h = 2 * qsm_even_half) -> (exists wpp_mod_left_qsm_mod_one wpp_mod_right_qsm_mod_one. (x) + p * wpp_mod_left_qsm_mod_one = (1) + p * wpp_mod_right_qsm_mod_one)) /\ ((exists qsm_odd_half. h = 2 * qsm_odd_half + 1) -> (exists wpp_mod_left_qsm_mod_predecessor wpp_mod_right_qsm_mod_predecessor. (x) + p * wpp_mod_left_qsm_mod_predecessor = (n) + p * wpp_mod_right_qsm_mod_predecessor)))
  43. 0043specialize pow_predecessor_parity_mod p
  44. 0044specialize pow_predecessor_parity_mod n
  45. 0045specialize pow_predecessor_parity_mod h
  46. 0046specialize pow_predecessor_parity_mod x
  47. 0047apply pow_predecessor_parity_mod
  48. 0048exact hpredecessor
  49. 0049exact hpower_witness
  50. 0050cases hsign
  51. 0051split
  52. 0052split
  53. 0053intro hresidue
  54. 0054specialize parity_cases h
  55. 0055cases parity_cases
  56. 0056cases parity_cases_witness
  57. 0057exists x1
  58. 0058exact parity_cases_witness_left
  59. 0059exfalso
  60. 0060have hnotresidue : ¬QRes(p,n)
    Exact native replay linehave hnotresidue : ~(exists qr_x_qsm_predecessor. exists qr_u_qsm_predecessor qr_v_qsm_predecessor. qr_x_qsm_predecessor * qr_x_qsm_predecessor + p * qr_u_qsm_predecessor = n + p * qr_v_qsm_predecessor)
  61. 0061intro hresidue_again
  62. 0062apply heuler_right_right
  63. 0063apply hsign_right
  64. 0064exists x1
  65. 0065exact parity_cases_witness_right
  66. 0066exact hresidue_again
  67. 0067apply hnotresidue
  68. 0068exact hresidue
  69. 0069intro heven
  70. 0070apply heuler_left_right
  71. 0071apply hsign_left
  72. 0072exact heven
  73. 0073split
  74. 0074intro hnotresidue
  75. 0075specialize parity_cases h
  76. 0076cases parity_cases
  77. 0077cases parity_cases_witness
  78. 0078exfalso
  79. 0079apply hnotresidue
  80. 0080apply heuler_left_right
  81. 0081apply hsign_left
  82. 0082exists x1
  83. 0083exact parity_cases_witness_left
  84. 0084exists x1
  85. 0085exact parity_cases_witness_right
  86. 0086intro hodd
  87. 0087intro hresidue
  88. 0088apply heuler_right_right
  89. 0089apply hsign_right
  90. 0090exact hodd
  91. 0091exact hresidue