SL000C

mod_eight_good_bad_exclusive

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

The favorable modulo-eight classes one and seven cannot equal the unfavorable classes three and 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. (((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_three. p = 8 * qst_mod_eight_modulus_three + 3) \/ (exists qst_mod_eight_modulus_five. p = 8 * qst_mod_eight_modulus_five + 5))) -> false

Constructive proof overview

Generated structural guide

The favorable modulo-eight classes one and seven cannot equal the unfavorable classes three and five.

The unchanged tactic script uses 1 declared prerequisite and contains 104 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

SL000B mod_eight_remainder_unique

Direct dependents

SL000F doubling_gauss_count_parity_mod_eight_complete

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

104 script commands · 39 reading checkpoints · 14 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 (1)
mod eight remainder unique
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro hgood
  3. L3
    intro hbad
02Separate the logical casesL4–7

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

  1. L4
    cases hgood
  2. L5
    cases hgood_left
  3. L6
    cases hbad
  4. L7
    cases hbad_left
03Establish hremaindersL8–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eight remainder unique.

  1. L8
    have hremainders : 1 = 3
  2. L9
    specialize mod_eight_remainder_unique p
  3. L10
    specialize mod_eight_remainder_unique x
  4. L11
    specialize mod_eight_remainder_unique 1
  5. L12
    specialize mod_eight_remainder_unique x1
  6. L13
    specialize mod_eight_remainder_unique 3
  7. L14
    apply mod_eight_remainder_unique
  8. L15
    exact hgood_left_witness
04Construct an explicit witnessL16–16

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

  1. L16
    exists 6
05Calculate and transport equalitiesL17–17

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

  1. L17
    norm_num
06Use earlier factsL18–18

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

  1. L18
    exact hbad_left_witness
07Construct an explicit witnessL19–19

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

  1. L19
    exists 4
08Calculate and transport equalitiesL20–20

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

  1. L20
    norm_num
09Establish hzeroL21–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L21
    have hzero : 0 = 2
  2. L22
    apply PA2
  3. L23
    exact hremainders
  4. L24
    apply PA1
  5. L25
    symm
  6. L26
    exact hzero
10Separate the logical casesL27–27

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

  1. L27
    cases hbad_right
11Establish hremaindersL28–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eight remainder unique.

  1. L28
    have hremainders : 1 = 5
  2. L29
    specialize mod_eight_remainder_unique p
  3. L30
    specialize mod_eight_remainder_unique x
  4. L31
    specialize mod_eight_remainder_unique 1
  5. L32
    specialize mod_eight_remainder_unique x1
  6. L33
    specialize mod_eight_remainder_unique 5
  7. L34
    apply mod_eight_remainder_unique
  8. L35
    exact hgood_left_witness
12Construct an explicit witnessL36–36

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

  1. L36
    exists 6
13Calculate and transport equalitiesL37–37

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

  1. L37
    norm_num
14Use earlier factsL38–38

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

  1. L38
    exact hbad_right_witness
15Construct an explicit witnessL39–39

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

  1. L39
    exists 2
16Calculate and transport equalitiesL40–40

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

  1. L40
    norm_num
17Establish hzeroL41–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L41
    have hzero : 0 = 4
  2. L42
    apply PA2
  3. L43
    exact hremainders
  4. L44
    apply PA1
  5. L45
    symm
  6. L46
    exact hzero
18Separate the logical casesL47–49

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

  1. L47
    cases hgood_right
  2. L48
    cases hbad
  3. L49
    cases hbad_left
19Establish hremaindersL50–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eight remainder unique.

  1. L50
    have hremainders : 7 = 3
  2. L51
    specialize mod_eight_remainder_unique p
  3. L52
    specialize mod_eight_remainder_unique x
  4. L53
    specialize mod_eight_remainder_unique 7
  5. L54
    specialize mod_eight_remainder_unique x1
  6. L55
    specialize mod_eight_remainder_unique 3
  7. L56
    apply mod_eight_remainder_unique
  8. L57
    exact hgood_right_witness
20Construct an explicit witnessL58–58

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

  1. L58
    exists 0
21Calculate and transport equalitiesL59–59

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

  1. L59
    norm_num
22Use earlier factsL60–60

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

  1. L60
    exact hbad_left_witness
23Construct an explicit witnessL61–61

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

  1. L61
    exists 4
24Calculate and transport equalitiesL62–62

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

  1. L62
    norm_num
25Establish hfirstL63–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L63
    have hfirst : 6 = 2
  2. L64
    apply PA2
  3. L65
    exact hremainders
26Establish hsecondL66–68

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L66
    have hsecond : 5 = 1
  2. L67
    apply PA2
  3. L68
    exact hfirst
27Establish hzeroL69–73

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L69
    have hzero : 4 = 0
  2. L70
    apply PA2
  3. L71
    exact hsecond
  4. L72
    apply PA1
  5. L73
    exact hzero
28Separate the logical casesL74–74

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

  1. L74
    cases hbad_right
29Establish hremaindersL75–82

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eight remainder unique.

  1. L75
    have hremainders : 7 = 5
  2. L76
    specialize mod_eight_remainder_unique p
  3. L77
    specialize mod_eight_remainder_unique x
  4. L78
    specialize mod_eight_remainder_unique 7
  5. L79
    specialize mod_eight_remainder_unique x1
  6. L80
    specialize mod_eight_remainder_unique 5
  7. L81
    apply mod_eight_remainder_unique
  8. L82
    exact hgood_right_witness
30Construct an explicit witnessL83–83

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

  1. L83
    exists 0
31Calculate and transport equalitiesL84–84

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

  1. L84
    norm_num
32Use earlier factsL85–85

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

  1. L85
    exact hbad_right_witness
33Construct an explicit witnessL86–86

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

  1. L86
    exists 2
34Calculate and transport equalitiesL87–87

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

  1. L87
    norm_num
35Establish hfirstL88–90

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L88
    have hfirst : 6 = 4
  2. L89
    apply PA2
  3. L90
    exact hremainders
36Establish hsecondL91–93

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L91
    have hsecond : 5 = 3
  2. L92
    apply PA2
  3. L93
    exact hfirst
37Establish hthirdL94–96

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L94
    have hthird : 4 = 2
  2. L95
    apply PA2
  3. L96
    exact hsecond
38Establish hfourthL97–99

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L97
    have hfourth : 3 = 1
  2. L98
    apply PA2
  3. L99
    exact hthird
39Establish hzeroL100–104

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L100
    have hzero : 2 = 0
  2. L101
    apply PA2
  3. L102
    exact hfourth
  4. L103
    apply PA1
  5. L104
    exact hzero

Library-wide reading audit

Original exact command ledger · 104 lines
  1. 0001intro p
  2. 0002intro hgood
  3. 0003intro hbad
  4. 0004cases hgood
  5. 0005cases hgood_left
  6. 0006cases hbad
  7. 0007cases hbad_left
  8. 0008have hremainders : 1 = 3
  9. 0009specialize mod_eight_remainder_unique p
  10. 0010specialize mod_eight_remainder_unique x
  11. 0011specialize mod_eight_remainder_unique 1
  12. 0012specialize mod_eight_remainder_unique x1
  13. 0013specialize mod_eight_remainder_unique 3
  14. 0014apply mod_eight_remainder_unique
  15. 0015exact hgood_left_witness
  16. 0016exists 6
  17. 0017norm_num
  18. 0018exact hbad_left_witness
  19. 0019exists 4
  20. 0020norm_num
  21. 0021have hzero : 0 = 2
  22. 0022apply PA2
  23. 0023exact hremainders
  24. 0024apply PA1
  25. 0025symm
  26. 0026exact hzero
  27. 0027cases hbad_right
  28. 0028have hremainders : 1 = 5
  29. 0029specialize mod_eight_remainder_unique p
  30. 0030specialize mod_eight_remainder_unique x
  31. 0031specialize mod_eight_remainder_unique 1
  32. 0032specialize mod_eight_remainder_unique x1
  33. 0033specialize mod_eight_remainder_unique 5
  34. 0034apply mod_eight_remainder_unique
  35. 0035exact hgood_left_witness
  36. 0036exists 6
  37. 0037norm_num
  38. 0038exact hbad_right_witness
  39. 0039exists 2
  40. 0040norm_num
  41. 0041have hzero : 0 = 4
  42. 0042apply PA2
  43. 0043exact hremainders
  44. 0044apply PA1
  45. 0045symm
  46. 0046exact hzero
  47. 0047cases hgood_right
  48. 0048cases hbad
  49. 0049cases hbad_left
  50. 0050have hremainders : 7 = 3
  51. 0051specialize mod_eight_remainder_unique p
  52. 0052specialize mod_eight_remainder_unique x
  53. 0053specialize mod_eight_remainder_unique 7
  54. 0054specialize mod_eight_remainder_unique x1
  55. 0055specialize mod_eight_remainder_unique 3
  56. 0056apply mod_eight_remainder_unique
  57. 0057exact hgood_right_witness
  58. 0058exists 0
  59. 0059norm_num
  60. 0060exact hbad_left_witness
  61. 0061exists 4
  62. 0062norm_num
  63. 0063have hfirst : 6 = 2
  64. 0064apply PA2
  65. 0065exact hremainders
  66. 0066have hsecond : 5 = 1
  67. 0067apply PA2
  68. 0068exact hfirst
  69. 0069have hzero : 4 = 0
  70. 0070apply PA2
  71. 0071exact hsecond
  72. 0072apply PA1
  73. 0073exact hzero
  74. 0074cases hbad_right
  75. 0075have hremainders : 7 = 5
  76. 0076specialize mod_eight_remainder_unique p
  77. 0077specialize mod_eight_remainder_unique x
  78. 0078specialize mod_eight_remainder_unique 7
  79. 0079specialize mod_eight_remainder_unique x1
  80. 0080specialize mod_eight_remainder_unique 5
  81. 0081apply mod_eight_remainder_unique
  82. 0082exact hgood_right_witness
  83. 0083exists 0
  84. 0084norm_num
  85. 0085exact hbad_right_witness
  86. 0086exists 2
  87. 0087norm_num
  88. 0088have hfirst : 6 = 4
  89. 0089apply PA2
  90. 0090exact hremainders
  91. 0091have hsecond : 5 = 3
  92. 0092apply PA2
  93. 0093exact hfirst
  94. 0094have hthird : 4 = 2
  95. 0095apply PA2
  96. 0096exact hsecond
  97. 0097have hfourth : 3 = 1
  98. 0098apply PA2
  99. 0099exact hthird
  100. 0100have hzero : 2 = 0
  101. 0101apply PA2
  102. 0102exact hfourth
  103. 0103apply PA1
  104. 0104exact hzero