SL000E · theorem body

doubling_gauss_odd_count_implies_bad_mod_eight

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

An odd doubling reflection count forces the prime to be three or five 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. ∀ h. ∀ e. p = 2 · h + 1 → h = 2 · e ∨ (∃ x. h = 2 · x + 1 ∧ e = S x) → Odd(e) → (∃ x. p = 8 · x + 3) ∨ (∃ x. p = 8 · x + 5)

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

PD0009 Even
Exact expanded first-order statement
forall p h e. p = 2 * h + 1 -> (((h = 2 * e) \/ (exists qst_count_half_shape. h = 2 * qst_count_half_shape + 1 /\ e = S qst_count_half_shape))) -> (exists qst_odd_count. e = 2 * qst_odd_count + 1) -> (((exists qst_mod_eight_modulus_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5)))

Proof neighborhood

Direct theorem prerequisites

odd_successor_to_even · Stable closed mul_add · Stable closed four_mul_eq_double_double · Stable closed SL0008 eight_mul_eq_double_four

Direct theorem dependents

SL000F doubling_gauss_count_parity_mod_eight_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

32 script commands · 12 reading checkpoints · 1 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–6

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro e
  4. L4
    intro hpodd
  5. L5
    intro hshape
  6. L6
    intro hodd
02Separate the logical casesL7–9

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

  1. L7
    cases hshape
  2. L8
    cases hodd
  3. L9
    right
03Construct an explicit witnessL10–10

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

  1. L10
    exists x
04Calculate and transport equalitiesL11–14

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

  1. L11
    rewrite hpodd
  2. L12
    rewrite hshape_left
  3. L13
    rewrite hodd_witness
  4. L14
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
05Separate the logical casesL15–17

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

  1. L15
    cases hshape_right
  2. L16
    cases hshape_right_witness
  3. L17
    cases hodd
06Establish heven_halfL18–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply odd successor to even.

  1. L18
    have heven_half : Even(x)Definitions: Even(x)Original native command in the exact edition
  2. L19
    specialize odd_successor_to_even x
  3. L20
    apply odd_successor_to_even
07Construct an explicit witnessL21–21

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

  1. L21
    exists x1
08Calculate and transport equalitiesL22–23

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

  1. L22
    trans e
  2. L23
    symm
09Use earlier factsL24–25

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

  1. L24
    exact hshape_right_witness_right
  2. L25
    exact hodd_witness
10Separate the logical casesL26–27

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

  1. L26
    cases heven_half
  2. L27
    left
11Construct an explicit witnessL28–28

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

  1. L28
    exists x2
12Calculate and transport equalitiesL29–32

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

  1. L29
    rewrite hpodd
  2. L30
    rewrite hshape_right_witness_left
  3. L31
    rewrite heven_half_witness
  4. L32
    simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro e
  4. 0004intro hpodd
  5. 0005intro hshape
  6. 0006intro hodd
  7. 0007cases hshape
  8. 0008cases hodd
  9. 0009right
  10. 0010exists x
  11. 0011rewrite hpodd
  12. 0012rewrite hshape_left
  13. 0013rewrite hodd_witness
  14. 0014simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]
  15. 0015cases hshape_right
  16. 0016cases hshape_right_witness
  17. 0017cases hodd
  18. 0018have heven_half : Even(x)
    Exact native replay linehave heven_half : exists a. x = 2 * a
  19. 0019specialize odd_successor_to_even x
  20. 0020apply odd_successor_to_even
  21. 0021exists x1
  22. 0022trans e
  23. 0023symm
  24. 0024exact hshape_right_witness_right
  25. 0025exact hodd_witness
  26. 0026cases heven_half
  27. 0027left
  28. 0028exists x2
  29. 0029rewrite hpodd
  30. 0030rewrite hshape_right_witness_left
  31. 0031rewrite heven_half_witness
  32. 0032simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]