SL0003

quadratic_supplement_minus_one_half_parity

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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.

The unchanged tactic script uses 6 declared prerequisites and contains 91 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

SL0001 prime_predecessor_nonzero pow_exists Stable theorem; checked-use authorized SL0000 bounded_euler_criterion_complete pow_predecessor_parity_mod Stable theorem; checked-use authorized parity_cases Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

SL0004 quadratic_supplement_minus_one_residue_iff_mod_four_one SL0005 quadratic_supplement_minus_one_nonresidue_iff_mod_four_three

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (2)
prime predecessor nonzerobounded euler criterion complete

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 : exists wpo_gap_qsm_predecessor_bound. wpo_gap_qsm_predecessor_bound + S (n) = p
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
  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: ModEqQRes
  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 : (((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)))
  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 : ~(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)
  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 exact 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 : 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 : 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 : (((((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 : (((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 : ~(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