SL0005

quadratic_supplement_minus_one_nonresidue_iff_mod_four_three

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

The first supplementary law's complementary branch: minus one is a nonresidue exactly for odd primes that are three 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_three_modulus. p = 4 * qsm_four_three_modulus + 3)) /\ ((exists qsm_four_three_modulus. p = 4 * qsm_four_three_modulus + 3) -> (~(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's complementary branch: minus one is a nonresidue exactly for odd primes that are three modulo four.

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

40 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_right
06Establish hmodfourL24–28

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

  1. L24
    have hmodfour : (((exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1) -> (exists qsm_four_three_modulus. p = 4 * qsm_four_three_modulus + 3)) /\ ((exists qsm_four_three_modulus. p = 4 * qsm_four_three_modulus + 3) -> (exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1)))
  2. L25
    specialize odd_half_odd_iff_mod4_three p
  3. L26
    specialize odd_half_odd_iff_mod4_three x
  4. L27
    apply odd_half_odd_iff_mod4_three
  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 hnonresidue
09Use earlier factsL32–34

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

  1. L32
    apply hmodfour_left
  2. L33
    apply hclassification_right_left
  3. L34
    exact hnonresidue
10Fix variables and assumptionsL35–36

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

  1. L35
    intro hfourthree
  2. L36
    intro hresidue
11Use earlier factsL37–40

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

  1. L37
    apply hclassification_right_right
  2. L38
    apply hmodfour_right
  3. L39
    exact hfourthree
  4. L40
    exact hresidue

Library-wide reading audit

Original exact command ledger · 40 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_right
  24. 0024have hmodfour : (((exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1) -> (exists qsm_four_three_modulus. p = 4 * qsm_four_three_modulus + 3)) /\ ((exists qsm_four_three_modulus. p = 4 * qsm_four_three_modulus + 3) -> (exists qsm_odd_endpoint_half. x = 2 * qsm_odd_endpoint_half + 1)))
  25. 0025specialize odd_half_odd_iff_mod4_three p
  26. 0026specialize odd_half_odd_iff_mod4_three x
  27. 0027apply odd_half_odd_iff_mod4_three
  28. 0028exact hodd_witness
  29. 0029cases hmodfour
  30. 0030split
  31. 0031intro hnonresidue
  32. 0032apply hmodfour_left
  33. 0033apply hclassification_right_left
  34. 0034exact hnonresidue
  35. 0035intro hfourthree
  36. 0036intro hresidue
  37. 0037apply hclassification_right_right
  38. 0038apply hmodfour_right
  39. 0039exact hfourthree
  40. 0040exact hresidue