SL0004 · theorem body

quadratic_supplement_minus_one_residue_iff_mod_four_one

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ p. ∀ n. p = S n → Prime(p) → Odd(p) → (QRes(p,n) → Mod4One(p)) ∧ (Mod4One(p) → 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 PD0010 Odd PD0011 Mod4One PD0021 QRes

In local proof propositions

PD0009 Even PD0010 Odd PD0011 Mod4One PD0021 QRes
Exact expanded first-order 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))))

Proof neighborhood

Direct theorem prerequisites

SL0002 odd_predecessor_double_half SL0003 quadratic_supplement_minus_one_half_parity odd_half_even_iff_mod4_one · Alpha closed

Direct theorem dependents

SL0006 quadratic_supplement_minus_one_complete

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

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.

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)
odd predecessor double halfquadratic supplement minus one half parity
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: QRes(p,n)Even(x)Odd(x)Original native command in the exact edition
  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 : (Even(x) → Mod4One(p)) ∧ (Mod4One(p) → Even(x))Definitions: Even(x)Mod4One(p)Original native command in the exact edition
  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 defined 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 : (QRes(p,n) → Even(x)) ∧ (Even(x) → QRes(p,n)) ∧ ((¬QRes(p,n) → Odd(x)) ∧ (Odd(x) → ¬QRes(p,n)))
    Exact native replay linehave 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 : (Even(x) → Mod4One(p)) ∧ (Mod4One(p) → Even(x))
    Exact native replay linehave 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