SL0004

quadratic_supplement_minus_one_residue_iff_mod_four_one

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The first supplementary law: minus one is a quadratic residue modulo an odd prime exactly when that prime is one modulo four.

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. 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)) -> (exists qsm_odd_modulus. p = 2 * qsm_odd_modulus + 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) -> (exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 1)) /\ ((exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 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

The first supplementary law: minus one is a quadratic residue modulo an odd prime exactly when that prime is one modulo four.

The unchanged tactic script uses 3 declared prerequisites and contains 38 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

SL0002 odd_predecessor_double_half SL0003 quadratic_supplement_minus_one_half_parity odd_half_even_iff_mod4_one Alpha theorem; checked-use authorized

Direct dependents

SL0006 quadratic_supplement_minus_one_complete

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

38 script commands · 11 reading checkpoints · 3 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)
odd predecessor double halfquadratic supplement minus one half parity

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–5

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro hpredecessor
  4. L4
    intro hprime
  5. L5
    intro hodd
02Separate the logical casesL6–6

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

  1. L6
    cases hodd
03Establish hdoubleL7–13

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

  1. L7
    have hdouble : n = x + x
  2. L8
    specialize odd_predecessor_double_half p
  3. L9
    specialize odd_predecessor_double_half n
  4. L10
    specialize odd_predecessor_double_half x
  5. L11
    apply odd_predecessor_double_half
  6. L12
    exact hpredecessor
  7. L13
    exact hodd_witness
04Establish hclassificationL14–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply quadratic supplement minus one half parity.

  1. L14
    have hclassification : (QRes(p,n) → Even(x)) ∧ (Even(x) → QRes(p,n)) ∧ ((¬QRes(p,n) → Odd(x)) ∧ (Odd(x) → ¬QRes(p,n)))Definitions: EvenOddQRes
  2. L15
    specialize quadratic_supplement_minus_one_half_parity p
  3. L16
    specialize quadratic_supplement_minus_one_half_parity n
  4. L17
    specialize quadratic_supplement_minus_one_half_parity x
  5. L18
    apply quadratic_supplement_minus_one_half_parity
  6. L19
    exact hpredecessor
  7. L20
    exact hprime
  8. L21
    exact hdouble
05Separate the logical casesL22–23

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

  1. L22
    cases hclassification
  2. L23
    cases hclassification_left
06Establish hmodfourL24–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd half even iff mod4 one.

  1. L24
    have hmodfour : (((exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half) -> (exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 1)) /\ ((exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 1) -> (exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half)))
  2. L25
    specialize odd_half_even_iff_mod4_one p
  3. L26
    specialize odd_half_even_iff_mod4_one x
  4. L27
    apply odd_half_even_iff_mod4_one
  5. L28
    exact hodd_witness
07Separate the logical casesL29–30

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

  1. L29
    cases hmodfour
  2. L30
    split
08Fix variables and assumptionsL31–31

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

  1. L31
    intro hresidue
09Use earlier factsL32–34

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

  1. L32
    apply hmodfour_left
  2. L33
    apply hclassification_left_left
  3. L34
    exact hresidue
10Fix variables and assumptionsL35–35

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

  1. L35
    intro hfourone
11Use earlier factsL36–38

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

  1. L36
    apply hclassification_left_right
  2. L37
    apply hmodfour_right
  3. L38
    exact hfourone

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hpredecessor
  4. 0004intro hprime
  5. 0005intro hodd
  6. 0006cases hodd
  7. 0007have hdouble : n = x + x
  8. 0008specialize odd_predecessor_double_half p
  9. 0009specialize odd_predecessor_double_half n
  10. 0010specialize odd_predecessor_double_half x
  11. 0011apply odd_predecessor_double_half
  12. 0012exact hpredecessor
  13. 0013exact hodd_witness
  14. 0014have hclassification : (((((exists qr_x_qsm_endpoint_predecessor. exists qr_u_qsm_endpoint_predecessor qr_v_qsm_endpoint_predecessor. qr_x_qsm_endpoint_predecessor * qr_x_qsm_endpoint_predecessor + p * qr_u_qsm_endpoint_predecessor = n + p * qr_v_qsm_endpoint_predecessor) -> (exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half)) /\ ((exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half) -> (exists qr_x_qsm_endpoint_predecessor. exists qr_u_qsm_endpoint_predecessor qr_v_qsm_endpoint_predecessor. qr_x_qsm_endpoint_predecessor * qr_x_qsm_endpoint_predecessor + p * qr_u_qsm_endpoint_predecessor = n + p * qr_v_qsm_endpoint_predecessor)))) /\ ((((~(exists qr_x_qsm_endpoint_predecessor. exists qr_u_qsm_endpoint_predecessor qr_v_qsm_endpoint_predecessor. qr_x_qsm_endpoint_predecessor * qr_x_qsm_endpoint_predecessor + p * qr_u_qsm_endpoint_predecessor = n + p * qr_v_qsm_endpoint_predecessor)) -> (exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1)) /\ ((exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1) -> (~(exists qr_x_qsm_endpoint_predecessor. exists qr_u_qsm_endpoint_predecessor qr_v_qsm_endpoint_predecessor. qr_x_qsm_endpoint_predecessor * qr_x_qsm_endpoint_predecessor + p * qr_u_qsm_endpoint_predecessor = n + p * qr_v_qsm_endpoint_predecessor))))))
  15. 0015specialize quadratic_supplement_minus_one_half_parity p
  16. 0016specialize quadratic_supplement_minus_one_half_parity n
  17. 0017specialize quadratic_supplement_minus_one_half_parity x
  18. 0018apply quadratic_supplement_minus_one_half_parity
  19. 0019exact hpredecessor
  20. 0020exact hprime
  21. 0021exact hdouble
  22. 0022cases hclassification
  23. 0023cases hclassification_left
  24. 0024have hmodfour : (((exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half) -> (exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 1)) /\ ((exists qsm_four_one_modulus. p = 4 * qsm_four_one_modulus + 1) -> (exists qsm_even_endpoint_half. x = 2 * qsm_even_endpoint_half)))
  25. 0025specialize odd_half_even_iff_mod4_one p
  26. 0026specialize odd_half_even_iff_mod4_one x
  27. 0027apply odd_half_even_iff_mod4_one
  28. 0028exact hodd_witness
  29. 0029cases hmodfour
  30. 0030split
  31. 0031intro hresidue
  32. 0032apply hmodfour_left
  33. 0033apply hclassification_left_left
  34. 0034exact hresidue
  35. 0035intro hfourone
  36. 0036apply hclassification_left_right
  37. 0037apply hmodfour_right
  38. 0038exact hfourone