SL0005 · theorem body

quadratic_supplement_minus_one_nonresidue_iff_mod_four_three

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

Statement with defined notation

∀ p. ∀ n. p = S n → Prime(p) → Odd(p) → (¬QRes(p,n) → Mod4Three(p)) ∧ (Mod4Three(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 PD0012 Mod4Three PD0021 QRes

In local proof propositions

PD0009 Even PD0010 Odd PD0012 Mod4Three 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_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)))))

Proof neighborhood

Direct theorem prerequisites

SL0002 odd_predecessor_double_half SL0003 quadratic_supplement_minus_one_half_parity odd_half_odd_iff_mod4_three · 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

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.

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_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 : (Odd(x) → Mod4Three(p)) ∧ (Mod4Three(p) → Odd(x))Definitions: Odd(x)Mod4Three(p)Original native command in the exact edition
  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 defined 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 : (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_right
  24. 0024have hmodfour : (Odd(x) → Mod4Three(p)) ∧ (Mod4Three(p) → Odd(x))
    Exact native replay linehave 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