SL000D · theorem body

doubling_gauss_even_count_implies_good_mod_eight

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

An even doubling reflection count forces the prime to be one 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. ∀ h. ∀ e. p = 2 · h + 1 → h = 2 · e ∨ (∃ x. h = 2 · x + 1 ∧ e = S x) → Even(e) → (∃ x. p = 8 · x + 1) ∨ (∃ 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

PD0009 Even

In local proof propositions

PD0010 Odd
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_even_count. e = 2 * qst_even_count) -> (((exists qst_mod_eight_modulus_one. p = 8 * qst_mod_eight_modulus_one + 1) \/ (exists qst_mod_eight_modulus_seven. p = 8 * qst_mod_eight_modulus_seven + 7)))

Proof neighborhood

Direct theorem prerequisites

even_successor_to_odd · 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 hodd
  5. L5
    intro hshape
  6. L6
    intro heven
02Separate the logical casesL7–9

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

  1. L7
    cases hshape
  2. L8
    cases heven
  3. L9
    left
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 hodd
  2. L12
    rewrite hshape_left
  3. L13
    rewrite heven_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 heven
06Establish hodd_halfL18–20

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

  1. L18
    have hodd_half : Odd(x)Definitions: Odd(x)Original native command in the exact edition
  2. L19
    specialize even_successor_to_odd x
  3. L20
    apply even_successor_to_odd
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 heven_witness
10Separate the logical casesL26–27

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

  1. L26
    cases hodd_half
  2. L27
    right
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 hodd
  2. L30
    rewrite hshape_right_witness_left
  3. L31
    rewrite hodd_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 hodd
  5. 0005intro hshape
  6. 0006intro heven
  7. 0007cases hshape
  8. 0008cases heven
  9. 0009left
  10. 0010exists x
  11. 0011rewrite hodd
  12. 0012rewrite hshape_left
  13. 0013rewrite heven_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 heven
  18. 0018have hodd_half : Odd(x)
    Exact native replay linehave hodd_half : exists a. x = 2 * a + 1
  19. 0019specialize even_successor_to_odd x
  20. 0020apply even_successor_to_odd
  21. 0021exists x1
  22. 0022trans e
  23. 0023symm
  24. 0024exact hshape_right_witness_right
  25. 0025exact heven_witness
  26. 0026cases hodd_half
  27. 0027right
  28. 0028exists x2
  29. 0029rewrite hodd
  30. 0030rewrite hshape_right_witness_left
  31. 0031rewrite hodd_half_witness
  32. 0032simp [mul_add, four_mul_eq_double_double, eight_mul_eq_double_four]