SL0009 · theorem body

odd_mod_eight_cases

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

Every odd natural constructively belongs to one of the four residue classes one, three, five or seven modulo eight.

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. Odd(p) → (∃ x. p = 8 · x + 1) ∨ ((∃ x. p = 8 · x + 3) ∨ ((∃ x. p = 8 · x + 5) ∨ (∃ x. p = 8 · x + 7)))

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

PD0010 Odd

In local proof propositions

none
Exact expanded first-order statement
forall p. (exists qst_odd_modulus. p = 2 * qst_odd_modulus + 1) -> (((exists qst_mod_eight_one. p = 8 * qst_mod_eight_one + 1) \/ ((exists qst_mod_eight_three. p = 8 * qst_mod_eight_three + 3) \/ ((exists qst_mod_eight_five. p = 8 * qst_mod_eight_five + 5) \/ (exists qst_mod_eight_seven. p = 8 * qst_mod_eight_seven + 7)))))

Proof neighborhood

Direct theorem prerequisites

parity_cases · Stable closed mul_add · Stable closed four_mul_eq_double_double · Stable closed SL0008 eight_mul_eq_double_four

Direct theorem dependents

none

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

47 script commands · 18 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.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hodd
02Separate the logical casesL3–3

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

  1. L3
    cases hodd
03Establish hhalf_parityL4–6

Establish this local claim before using it. It is not an additional assumption.

  1. L4
    have hhalf_parity : exists a. x = 2 * a \/ x = 2 * a + 1
  2. L5
    specialize parity_cases x
  3. L6
    exact parity_cases
04Separate the logical casesL7–8

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

  1. L7
    cases hhalf_parity
  2. L8
    cases hhalf_parity_witness
05Establish hquarter_parityL9–11

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hquarter_parity : exists b. x1 = 2 * b \/ x1 = 2 * b + 1
  2. L10
    specialize parity_cases x1
  3. L11
    exact parity_cases
06Separate the logical casesL12–14

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

  1. L12
    cases hquarter_parity
  2. L13
    cases hquarter_parity_witness
  3. L14
    left
07Construct an explicit witnessL15–15

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists x2
08Calculate and transport equalitiesL16–19

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L16
    rewrite hodd_witness
  2. L17
    rewrite hhalf_parity_witness_left
  3. L18
    rewrite hquarter_parity_witness_left
  4. L19
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
09Separate the logical casesL20–22

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

  1. L20
    right
  2. L21
    right
  3. L22
    left
10Construct an explicit witnessL23–23

Supply the displayed value, then prove that it has the required property.

  1. L23
    exists x2
11Calculate and transport equalitiesL24–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L24
    rewrite hodd_witness
  2. L25
    rewrite hhalf_parity_witness_left
  3. L26
    rewrite hquarter_parity_witness_right
  4. L27
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
12Establish hquarter_parityL28–30

Establish this local claim before using it. It is not an additional assumption.

  1. L28
    have hquarter_parity : exists b. x1 = 2 * b \/ x1 = 2 * b + 1
  2. L29
    specialize parity_cases x1
  3. L30
    exact parity_cases
13Separate the logical casesL31–34

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

  1. L31
    cases hquarter_parity
  2. L32
    cases hquarter_parity_witness
  3. L33
    right
  4. L34
    left
14Construct an explicit witnessL35–35

Supply the displayed value, then prove that it has the required property.

  1. L35
    exists x2
15Calculate and transport equalitiesL36–39

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L36
    rewrite hodd_witness
  2. L37
    rewrite hhalf_parity_witness_right
  3. L38
    rewrite hquarter_parity_witness_left
  4. L39
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
16Separate the logical casesL40–42

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

  1. L40
    right
  2. L41
    right
  3. L42
    right
17Construct an explicit witnessL43–43

Supply the displayed value, then prove that it has the required property.

  1. L43
    exists x2
18Calculate and transport equalitiesL44–47

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L44
    rewrite hodd_witness
  2. L45
    rewrite hhalf_parity_witness_right
  3. L46
    rewrite hquarter_parity_witness_right
  4. L47
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro p
  2. 0002intro hodd
  3. 0003cases hodd
  4. 0004have hhalf_parity : exists a. x = 2 * a \/ x = 2 * a + 1
  5. 0005specialize parity_cases x
  6. 0006exact parity_cases
  7. 0007cases hhalf_parity
  8. 0008cases hhalf_parity_witness
  9. 0009have hquarter_parity : exists b. x1 = 2 * b \/ x1 = 2 * b + 1
  10. 0010specialize parity_cases x1
  11. 0011exact parity_cases
  12. 0012cases hquarter_parity
  13. 0013cases hquarter_parity_witness
  14. 0014left
  15. 0015exists x2
  16. 0016rewrite hodd_witness
  17. 0017rewrite hhalf_parity_witness_left
  18. 0018rewrite hquarter_parity_witness_left
  19. 0019simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
  20. 0020right
  21. 0021right
  22. 0022left
  23. 0023exists x2
  24. 0024rewrite hodd_witness
  25. 0025rewrite hhalf_parity_witness_left
  26. 0026rewrite hquarter_parity_witness_right
  27. 0027simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
  28. 0028have hquarter_parity : exists b. x1 = 2 * b \/ x1 = 2 * b + 1
  29. 0029specialize parity_cases x1
  30. 0030exact parity_cases
  31. 0031cases hquarter_parity
  32. 0032cases hquarter_parity_witness
  33. 0033right
  34. 0034left
  35. 0035exists x2
  36. 0036rewrite hodd_witness
  37. 0037rewrite hhalf_parity_witness_right
  38. 0038rewrite hquarter_parity_witness_left
  39. 0039simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
  40. 0040right
  41. 0041right
  42. 0042right
  43. 0043exists x2
  44. 0044rewrite hodd_witness
  45. 0045rewrite hhalf_parity_witness_right
  46. 0046rewrite hquarter_parity_witness_right
  47. 0047simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]