SL000F

doubling_gauss_count_parity_mod_eight_complete

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

For the exact doubling reflection-count shape, evenness is equivalent to classes one/seven and oddness to three/five.

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.

Exact expanded first-order arithmetic 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)))) /\ ((((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))) -> (exists qst_even_count. e = 2 * qst_even_count)))) /\ ((((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)))) /\ ((((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))) -> (exists qst_odd_count. e = 2 * qst_odd_count + 1))))))

Constructive proof overview

Generated structural guide

For the exact doubling reflection-count shape, evenness is equivalent to classes one/seven and oddness to three/five.

The unchanged tactic script uses 4 declared prerequisites and contains 60 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

SL000D doubling_gauss_even_count_implies_good_mod_eight SL000E doubling_gauss_odd_count_implies_bad_mod_eight SL000C mod_eight_good_bad_exclusive parity_cases Stable theorem; checked-use authorized

Direct dependents

SL000O quadratic_supplement_two_conditional_on_gauss_count_shape

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

60 script commands · 24 reading checkpoints · 0 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.

Named ingredients (3)
doubling gauss even count implies good mod eightdoubling gauss odd count implies bad mod eightmod eight good bad exclusive
01Fix variables and assumptionsL1–5

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
02Separate the logical casesL6–7

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

  1. L6
    split
  2. L7
    split
03Fix variables and assumptionsL8–8

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

  1. L8
    intro heven
04Use earlier factsL9–15

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

  1. L9
    specialize doubling_gauss_even_count_implies_good_mod_eight p
  2. L10
    specialize doubling_gauss_even_count_implies_good_mod_eight h
  3. L11
    specialize doubling_gauss_even_count_implies_good_mod_eight e
  4. L12
    apply doubling_gauss_even_count_implies_good_mod_eight
  5. L13
    exact hpodd
  6. L14
    exact hshape
  7. L15
    exact heven
05Fix variables and assumptionsL16–16

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

  1. L16
    intro hgood
06Use earlier factsL17–17

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

  1. L17
    specialize parity_cases e
07Separate the logical casesL18–19

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

  1. L18
    cases parity_cases
  2. L19
    cases parity_cases_witness
08Construct an explicit witnessL20–20

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

  1. L20
    exists x
09Use earlier factsL21–21

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

  1. L21
    exact parity_cases_witness_left
10Separate the logical casesL22–22

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

  1. L22
    exfalso
11Use earlier factsL23–31

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

  1. L23
    specialize mod_eight_good_bad_exclusive p
  2. L24
    apply mod_eight_good_bad_exclusive
  3. L25
    exact hgood
  4. L26
    specialize doubling_gauss_odd_count_implies_bad_mod_eight p
  5. L27
    specialize doubling_gauss_odd_count_implies_bad_mod_eight h
  6. L28
    specialize doubling_gauss_odd_count_implies_bad_mod_eight e
  7. L29
    apply doubling_gauss_odd_count_implies_bad_mod_eight
  8. L30
    exact hpodd
  9. L31
    exact hshape
12Construct an explicit witnessL32–32

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

  1. L32
    exists x
13Use earlier factsL33–33

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

  1. L33
    exact parity_cases_witness_right
14Separate the logical casesL34–34

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

  1. L34
    split
15Fix variables and assumptionsL35–35

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

  1. L35
    intro hodd
16Use earlier factsL36–42

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

  1. L36
    specialize doubling_gauss_odd_count_implies_bad_mod_eight p
  2. L37
    specialize doubling_gauss_odd_count_implies_bad_mod_eight h
  3. L38
    specialize doubling_gauss_odd_count_implies_bad_mod_eight e
  4. L39
    apply doubling_gauss_odd_count_implies_bad_mod_eight
  5. L40
    exact hpodd
  6. L41
    exact hshape
  7. L42
    exact hodd
17Fix variables and assumptionsL43–43

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

  1. L43
    intro hbad
18Use earlier factsL44–44

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

  1. L44
    specialize parity_cases e
19Separate the logical casesL45–47

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

  1. L45
    cases parity_cases
  2. L46
    cases parity_cases_witness
  3. L47
    exfalso
20Use earlier factsL48–55

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

  1. L48
    specialize mod_eight_good_bad_exclusive p
  2. L49
    apply mod_eight_good_bad_exclusive
  3. L50
    specialize doubling_gauss_even_count_implies_good_mod_eight p
  4. L51
    specialize doubling_gauss_even_count_implies_good_mod_eight h
  5. L52
    specialize doubling_gauss_even_count_implies_good_mod_eight e
  6. L53
    apply doubling_gauss_even_count_implies_good_mod_eight
  7. L54
    exact hpodd
  8. L55
    exact hshape
21Construct an explicit witnessL56–56

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

  1. L56
    exists x
22Use earlier factsL57–58

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

  1. L57
    exact parity_cases_witness_left
  2. L58
    exact hbad
23Construct an explicit witnessL59–59

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

  1. L59
    exists x
24Use earlier factsL60–60

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

  1. L60
    exact parity_cases_witness_right

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro e
  4. 0004intro hpodd
  5. 0005intro hshape
  6. 0006split
  7. 0007split
  8. 0008intro heven
  9. 0009specialize doubling_gauss_even_count_implies_good_mod_eight p
  10. 0010specialize doubling_gauss_even_count_implies_good_mod_eight h
  11. 0011specialize doubling_gauss_even_count_implies_good_mod_eight e
  12. 0012apply doubling_gauss_even_count_implies_good_mod_eight
  13. 0013exact hpodd
  14. 0014exact hshape
  15. 0015exact heven
  16. 0016intro hgood
  17. 0017specialize parity_cases e
  18. 0018cases parity_cases
  19. 0019cases parity_cases_witness
  20. 0020exists x
  21. 0021exact parity_cases_witness_left
  22. 0022exfalso
  23. 0023specialize mod_eight_good_bad_exclusive p
  24. 0024apply mod_eight_good_bad_exclusive
  25. 0025exact hgood
  26. 0026specialize doubling_gauss_odd_count_implies_bad_mod_eight p
  27. 0027specialize doubling_gauss_odd_count_implies_bad_mod_eight h
  28. 0028specialize doubling_gauss_odd_count_implies_bad_mod_eight e
  29. 0029apply doubling_gauss_odd_count_implies_bad_mod_eight
  30. 0030exact hpodd
  31. 0031exact hshape
  32. 0032exists x
  33. 0033exact parity_cases_witness_right
  34. 0034split
  35. 0035intro hodd
  36. 0036specialize doubling_gauss_odd_count_implies_bad_mod_eight p
  37. 0037specialize doubling_gauss_odd_count_implies_bad_mod_eight h
  38. 0038specialize doubling_gauss_odd_count_implies_bad_mod_eight e
  39. 0039apply doubling_gauss_odd_count_implies_bad_mod_eight
  40. 0040exact hpodd
  41. 0041exact hshape
  42. 0042exact hodd
  43. 0043intro hbad
  44. 0044specialize parity_cases e
  45. 0045cases parity_cases
  46. 0046cases parity_cases_witness
  47. 0047exfalso
  48. 0048specialize mod_eight_good_bad_exclusive p
  49. 0049apply mod_eight_good_bad_exclusive
  50. 0050specialize doubling_gauss_even_count_implies_good_mod_eight p
  51. 0051specialize doubling_gauss_even_count_implies_good_mod_eight h
  52. 0052specialize doubling_gauss_even_count_implies_good_mod_eight e
  53. 0053apply doubling_gauss_even_count_implies_good_mod_eight
  54. 0054exact hpodd
  55. 0055exact hshape
  56. 0056exists x
  57. 0057exact parity_cases_witness_left
  58. 0058exact hbad
  59. 0059exists x
  60. 0060exact parity_cases_witness_right