ZU0002

dirichlet_signed_unit_product_classification

An actual signed product is positive one only for the two equal canonical units; mixed signs are constructively impossible.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Canonical signed +1 is code 2 and -1 is code 1. The two-case unit graph does not assume an inverse or cancellation law: its actual product characterization and affine existence and uniqueness are proved. These scalar lemmas support the separately checked finite inverse criterion; full G009 remains broader.

Exact theorem in conservative defined notation

∀ a. ∀ b. SignedMul(a,b,2) → a = 2 ∧ b = 2 ∨ a = 1 ∧ b = 1

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedDecode(z,p,n) · 4SignedMul(a,b,c) · 1

Actual proof prerequisites

signed_decode_total · checked external prerequisitemul_one · checked external prerequisitezero_add · checked external prerequisitesigned_mul_to_decoded_equation · checked external prerequisitesigned_decode_normal · checked external prerequisitemul_zero_left · checked external prerequisitemul_eq_one_components · checked external prerequisitesigned_decoded_balance_implies_code_eq · checked external prerequisite
Original expanded first-order statement 
forall a b. (exists sto_ap_classify sto_an_classify sto_bp_classify sto_bn_classify sto_cp_classify sto_cn_classify. (((((a) = 2 * (sto_ap_classify) /\ (sto_an_classify) = 0) \/ exists ge_signed_half_classifyleft. (((a) = 2 * ge_signed_half_classifyleft + 1 /\ (sto_ap_classify) = 0) /\ (sto_an_classify) = S ge_signed_half_classifyleft))) /\ ((((((b) = 2 * (sto_bp_classify) /\ (sto_bn_classify) = 0) \/ exists ge_signed_half_classifyright. (((b) = 2 * ge_signed_half_classifyright + 1 /\ (sto_bp_classify) = 0) /\ (sto_bn_classify) = S ge_signed_half_classifyright))) /\ ((((((2) = 2 * (sto_cp_classify) /\ (sto_cn_classify) = 0) \/ exists ge_signed_half_classifyoutput. (((2) = 2 * ge_signed_half_classifyoutput + 1 /\ (sto_cp_classify) = 0) /\ (sto_cn_classify) = S ge_signed_half_classifyoutput))) /\ ((sto_ap_classify * sto_bp_classify + sto_an_classify * sto_bn_classify) + sto_cn_classify = (sto_ap_classify * sto_bn_classify + sto_an_classify * sto_bp_classify) + sto_cp_classify))))))) -> ((a=2 /\ b=2) \/ (a=1 /\ b=1))

Complete tactic proof in conservative notation

All 151 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

151 script commands · 47 reading checkpoints · 13 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–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hmul
02Establish haL4–6

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

  1. L4
    have ha : ∃ p. ∃ n. SignedDecode(a,p,n)Definitions: SignedDecode(a,p,n)Original native command in the exact edition
  2. L5
    specialize signed_decode_total (a)
  3. L6
    apply signed_decode_total
03Separate the logical casesL7–8

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

  1. L7
    cases ha
  2. L8
    cases ha_witness
04Establish hbL9–11

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

  1. L9
    have hb : ∃ p. ∃ n. SignedDecode(b,p,n)Definitions: SignedDecode(b,p,n)Original native command in the exact edition
  2. L10
    specialize signed_decode_total (b)
  3. L11
    apply signed_decode_total
05Separate the logical casesL12–13

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

  1. L12
    cases hb
  2. L13
    cases hb_witness
06Establish hplusL14–14

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

  1. L14
    have hplus : SignedDecode(2,1,0)Definitions: SignedDecode(2,1,0)Original native command in the exact edition
07Separate the logical casesL15–16

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

  1. L15
    left
  2. L16
    split
08Calculate and transport equalitiesL17–17

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

  1. L17
    symm
09Use earlier factsL18–18

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

  1. L18
    apply mul_one
10Calculate and transport equalitiesL19–19

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

  1. L19
    refl
11Establish hminusL20–20

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

  1. L20
    have hminus : SignedDecode(1,0,1)Definitions: SignedDecode(1,0,1)Original native command in the exact edition
12Separate the logical casesL21–21

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

  1. L21
    right
13Construct an explicit witnessL22–22

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

  1. L22
    exists 0
14Separate the logical casesL23–24

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

  1. L23
    split
  2. L24
    split
15Calculate and transport equalitiesL25–26

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

  1. L25
    rewrite PA5
  2. L26
    symm
16Use earlier factsL27–27

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

  1. L27
    apply zero_add
17Calculate and transport equalitiesL28–29

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

  1. L28
    refl
  2. L29
    refl
18Establish heL30–39

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

  1. L30
    have he : (x*x2 + x1*x3)+0 = (x*x3 + x1*x2)+1
  2. L31
    specialize signed_mul_to_decoded_equation (a)
  3. L32
    specialize signed_mul_to_decoded_equation (b)
  4. L33
    specialize signed_mul_to_decoded_equation (2)
  5. L34
    specialize signed_mul_to_decoded_equation (x)
  6. L35
    specialize signed_mul_to_decoded_equation (x1)
  7. L36
    specialize signed_mul_to_decoded_equation (x2)
  8. L37
    specialize signed_mul_to_decoded_equation (x3)
  9. L38
    specialize signed_mul_to_decoded_equation (1)
  10. L39
    specialize signed_mul_to_decoded_equation (0)
19Use earlier factsL40–44

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

  1. L40
    apply signed_mul_to_decoded_equation
  2. L41
    exact ha_witness_witness
  3. L42
    exact hb_witness_witness
  4. L43
    exact hplus
  5. L44
    exact hmul
20Establish hnaL45–50

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

  1. L45
    have hna : x=0 \/ x1=0
  2. L46
    specialize signed_decode_normal (a)
  3. L47
    specialize signed_decode_normal (x)
  4. L48
    specialize signed_decode_normal (x1)
  5. L49
    apply signed_decode_normal
  6. L50
    exact ha_witness_witness
21Establish hnbL51–56

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

  1. L51
    have hnb : x2=0 \/ x3=0
  2. L52
    specialize signed_decode_normal (b)
  3. L53
    specialize signed_decode_normal (x2)
  4. L54
    specialize signed_decode_normal (x3)
  5. L55
    apply signed_decode_normal
  6. L56
    exact hb_witness_witness
22Separate the logical casesL57–58

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

  1. L57
    cases hna
  2. L58
    cases hnb
23Establish hmL59–65

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

  1. L59
    have hm : x1*x3=1
  2. L60
    trans (x*x2+x1*x3)+0
  3. L61
    symm
  4. L62
    simp [hna_left, hnb_left, mul_zero_left, zero_add]
  5. L63
    trans (x*x3+x1*x2)+1
  6. L64
    exact he
  7. L65
    simp [hna_left, hnb_left, mul_zero_left, zero_add]
24Establish hpartsL66–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq one components.

  1. L66
    have hparts : x1=1 /\ x3=1
  2. L67
    specialize mul_eq_one_components (x1)
  3. L68
    specialize mul_eq_one_components (x3)
  4. L69
    apply mul_eq_one_components
  5. L70
    exact hm
25Separate the logical casesL71–73

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

  1. L71
    cases hparts
  2. L72
    right
  3. L73
    split
26Use earlier factsL74–82

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

  1. L74
    specialize signed_decoded_balance_implies_code_eq (a)
  2. L75
    specialize signed_decoded_balance_implies_code_eq (x)
  3. L76
    specialize signed_decoded_balance_implies_code_eq (x1)
  4. L77
    specialize signed_decoded_balance_implies_code_eq (1)
  5. L78
    specialize signed_decoded_balance_implies_code_eq (0)
  6. L79
    specialize signed_decoded_balance_implies_code_eq (1)
  7. L80
    apply signed_decoded_balance_implies_code_eq
  8. L81
    exact ha_witness_witness
  9. L82
    exact hminus
27Calculate and transport equalitiesL83–83

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

  1. L83
    simp [hna_left, hparts_left, zero_add]
28Use earlier factsL84–92

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

  1. L84
    specialize signed_decoded_balance_implies_code_eq (b)
  2. L85
    specialize signed_decoded_balance_implies_code_eq (x2)
  3. L86
    specialize signed_decoded_balance_implies_code_eq (x3)
  4. L87
    specialize signed_decoded_balance_implies_code_eq (1)
  5. L88
    specialize signed_decoded_balance_implies_code_eq (0)
  6. L89
    specialize signed_decoded_balance_implies_code_eq (1)
  7. L90
    apply signed_decoded_balance_implies_code_eq
  8. L91
    exact hb_witness_witness
  9. L92
    exact hminus
29Calculate and transport equalitiesL93–93

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

  1. L93
    simp [hnb_left, hparts_right, zero_add]
30Establish hmL94–100

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

  1. L94
    have hm : 0=S(x1*x2)
  2. L95
    trans (x*x2+x1*x3)+0
  3. L96
    symm
  4. L97
    simp [hna_left, hnb_right, mul_zero_left, zero_add]
  5. L98
    trans (x*x3+x1*x2)+1
  6. L99
    exact he
  7. L100
    simp [hna_left, hnb_right, mul_zero_left, zero_add]
31Separate the logical casesL101–101

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

  1. L101
    exfalso
32Use earlier factsL102–102

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

  1. L102
    apply PA1
33Calculate and transport equalitiesL103–103

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

  1. L103
    symm
34Use earlier factsL104–104

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

  1. L104
    exact hm
35Separate the logical casesL105–105

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

  1. L105
    cases hnb
36Establish hmL106–112

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

  1. L106
    have hm : 0=S(x*x3)
  2. L107
    trans (x*x2+x1*x3)+0
  3. L108
    symm
  4. L109
    simp [hna_right, hnb_left, mul_zero_left, zero_add]
  5. L110
    trans (x*x3+x1*x2)+1
  6. L111
    exact he
  7. L112
    simp [hna_right, hnb_left, mul_zero_left, zero_add]
37Separate the logical casesL113–113

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

  1. L113
    exfalso
38Use earlier factsL114–114

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

  1. L114
    apply PA1
39Calculate and transport equalitiesL115–115

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

  1. L115
    symm
40Use earlier factsL116–116

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

  1. L116
    exact hm
41Establish hmL117–123

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

  1. L117
    have hm : x*x2=1
  2. L118
    trans (x*x2+x1*x3)+0
  3. L119
    symm
  4. L120
    simp [hna_right, hnb_right, mul_zero_left, zero_add]
  5. L121
    trans (x*x3+x1*x2)+1
  6. L122
    exact he
  7. L123
    simp [hna_right, hnb_right, mul_zero_left, zero_add]
42Establish hpartsL124–128

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul eq one components.

  1. L124
    have hparts : x=1 /\ x2=1
  2. L125
    specialize mul_eq_one_components (x)
  3. L126
    specialize mul_eq_one_components (x2)
  4. L127
    apply mul_eq_one_components
  5. L128
    exact hm
43Separate the logical casesL129–131

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

  1. L129
    cases hparts
  2. L130
    left
  3. L131
    split
44Use earlier factsL132–140

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

  1. L132
    specialize signed_decoded_balance_implies_code_eq (a)
  2. L133
    specialize signed_decoded_balance_implies_code_eq (x)
  3. L134
    specialize signed_decoded_balance_implies_code_eq (x1)
  4. L135
    specialize signed_decoded_balance_implies_code_eq (2)
  5. L136
    specialize signed_decoded_balance_implies_code_eq (1)
  6. L137
    specialize signed_decoded_balance_implies_code_eq (0)
  7. L138
    apply signed_decoded_balance_implies_code_eq
  8. L139
    exact ha_witness_witness
  9. L140
    exact hplus
45Calculate and transport equalitiesL141–141

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

  1. L141
    simp [hparts_left, hna_right, zero_add]
46Use earlier factsL142–150

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

  1. L142
    specialize signed_decoded_balance_implies_code_eq (b)
  2. L143
    specialize signed_decoded_balance_implies_code_eq (x2)
  3. L144
    specialize signed_decoded_balance_implies_code_eq (x3)
  4. L145
    specialize signed_decoded_balance_implies_code_eq (2)
  5. L146
    specialize signed_decoded_balance_implies_code_eq (1)
  6. L147
    specialize signed_decoded_balance_implies_code_eq (0)
  7. L148
    apply signed_decoded_balance_implies_code_eq
  8. L149
    exact hb_witness_witness
  9. L150
    exact hplus
47Calculate and transport equalitiesL151–151

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

  1. L151
    simp [hparts_right, hnb_right, zero_add]

Library-wide reading audit

Original defined command ledger · 151 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hmul
  4. 0004have ha : ∃ p. ∃ n. SignedDecode(a,p,n)
  5. 0005specialize signed_decode_total (a)
  6. 0006apply signed_decode_total
  7. 0007cases ha
  8. 0008cases ha_witness
  9. 0009have hb : ∃ p. ∃ n. SignedDecode(b,p,n)
  10. 0010specialize signed_decode_total (b)
  11. 0011apply signed_decode_total
  12. 0012cases hb
  13. 0013cases hb_witness
  14. 0014have hplus : SignedDecode(2,1,0)
  15. 0015left
  16. 0016split
  17. 0017symm
  18. 0018apply mul_one
  19. 0019refl
  20. 0020have hminus : SignedDecode(1,0,1)
  21. 0021right
  22. 0022exists 0
  23. 0023split
  24. 0024split
  25. 0025rewrite PA5
  26. 0026symm
  27. 0027apply zero_add
  28. 0028refl
  29. 0029refl
  30. 0030have he : (x*x2 + x1*x3)+0 = (x*x3 + x1*x2)+1
  31. 0031specialize signed_mul_to_decoded_equation (a)
  32. 0032specialize signed_mul_to_decoded_equation (b)
  33. 0033specialize signed_mul_to_decoded_equation (2)
  34. 0034specialize signed_mul_to_decoded_equation (x)
  35. 0035specialize signed_mul_to_decoded_equation (x1)
  36. 0036specialize signed_mul_to_decoded_equation (x2)
  37. 0037specialize signed_mul_to_decoded_equation (x3)
  38. 0038specialize signed_mul_to_decoded_equation (1)
  39. 0039specialize signed_mul_to_decoded_equation (0)
  40. 0040apply signed_mul_to_decoded_equation
  41. 0041exact ha_witness_witness
  42. 0042exact hb_witness_witness
  43. 0043exact hplus
  44. 0044exact hmul
  45. 0045have hna : x=0 \/ x1=0
  46. 0046specialize signed_decode_normal (a)
  47. 0047specialize signed_decode_normal (x)
  48. 0048specialize signed_decode_normal (x1)
  49. 0049apply signed_decode_normal
  50. 0050exact ha_witness_witness
  51. 0051have hnb : x2=0 \/ x3=0
  52. 0052specialize signed_decode_normal (b)
  53. 0053specialize signed_decode_normal (x2)
  54. 0054specialize signed_decode_normal (x3)
  55. 0055apply signed_decode_normal
  56. 0056exact hb_witness_witness
  57. 0057cases hna
  58. 0058cases hnb
  59. 0059have hm : x1*x3=1
  60. 0060trans (x*x2+x1*x3)+0
  61. 0061symm
  62. 0062simp [hna_left, hnb_left, mul_zero_left, zero_add]
  63. 0063trans (x*x3+x1*x2)+1
  64. 0064exact he
  65. 0065simp [hna_left, hnb_left, mul_zero_left, zero_add]
  66. 0066have hparts : x1=1 /\ x3=1
  67. 0067specialize mul_eq_one_components (x1)
  68. 0068specialize mul_eq_one_components (x3)
  69. 0069apply mul_eq_one_components
  70. 0070exact hm
  71. 0071cases hparts
  72. 0072right
  73. 0073split
  74. 0074specialize signed_decoded_balance_implies_code_eq (a)
  75. 0075specialize signed_decoded_balance_implies_code_eq (x)
  76. 0076specialize signed_decoded_balance_implies_code_eq (x1)
  77. 0077specialize signed_decoded_balance_implies_code_eq (1)
  78. 0078specialize signed_decoded_balance_implies_code_eq (0)
  79. 0079specialize signed_decoded_balance_implies_code_eq (1)
  80. 0080apply signed_decoded_balance_implies_code_eq
  81. 0081exact ha_witness_witness
  82. 0082exact hminus
  83. 0083simp [hna_left, hparts_left, zero_add]
  84. 0084specialize signed_decoded_balance_implies_code_eq (b)
  85. 0085specialize signed_decoded_balance_implies_code_eq (x2)
  86. 0086specialize signed_decoded_balance_implies_code_eq (x3)
  87. 0087specialize signed_decoded_balance_implies_code_eq (1)
  88. 0088specialize signed_decoded_balance_implies_code_eq (0)
  89. 0089specialize signed_decoded_balance_implies_code_eq (1)
  90. 0090apply signed_decoded_balance_implies_code_eq
  91. 0091exact hb_witness_witness
  92. 0092exact hminus
  93. 0093simp [hnb_left, hparts_right, zero_add]
  94. 0094have hm : 0=S(x1*x2)
  95. 0095trans (x*x2+x1*x3)+0
  96. 0096symm
  97. 0097simp [hna_left, hnb_right, mul_zero_left, zero_add]
  98. 0098trans (x*x3+x1*x2)+1
  99. 0099exact he
  100. 0100simp [hna_left, hnb_right, mul_zero_left, zero_add]
  101. 0101exfalso
  102. 0102apply PA1
  103. 0103symm
  104. 0104exact hm
  105. 0105cases hnb
  106. 0106have hm : 0=S(x*x3)
  107. 0107trans (x*x2+x1*x3)+0
  108. 0108symm
  109. 0109simp [hna_right, hnb_left, mul_zero_left, zero_add]
  110. 0110trans (x*x3+x1*x2)+1
  111. 0111exact he
  112. 0112simp [hna_right, hnb_left, mul_zero_left, zero_add]
  113. 0113exfalso
  114. 0114apply PA1
  115. 0115symm
  116. 0116exact hm
  117. 0117have hm : x*x2=1
  118. 0118trans (x*x2+x1*x3)+0
  119. 0119symm
  120. 0120simp [hna_right, hnb_right, mul_zero_left, zero_add]
  121. 0121trans (x*x3+x1*x2)+1
  122. 0122exact he
  123. 0123simp [hna_right, hnb_right, mul_zero_left, zero_add]
  124. 0124have hparts : x=1 /\ x2=1
  125. 0125specialize mul_eq_one_components (x)
  126. 0126specialize mul_eq_one_components (x2)
  127. 0127apply mul_eq_one_components
  128. 0128exact hm
  129. 0129cases hparts
  130. 0130left
  131. 0131split
  132. 0132specialize signed_decoded_balance_implies_code_eq (a)
  133. 0133specialize signed_decoded_balance_implies_code_eq (x)
  134. 0134specialize signed_decoded_balance_implies_code_eq (x1)
  135. 0135specialize signed_decoded_balance_implies_code_eq (2)
  136. 0136specialize signed_decoded_balance_implies_code_eq (1)
  137. 0137specialize signed_decoded_balance_implies_code_eq (0)
  138. 0138apply signed_decoded_balance_implies_code_eq
  139. 0139exact ha_witness_witness
  140. 0140exact hplus
  141. 0141simp [hparts_left, hna_right, zero_add]
  142. 0142specialize signed_decoded_balance_implies_code_eq (b)
  143. 0143specialize signed_decoded_balance_implies_code_eq (x2)
  144. 0144specialize signed_decoded_balance_implies_code_eq (x3)
  145. 0145specialize signed_decoded_balance_implies_code_eq (2)
  146. 0146specialize signed_decoded_balance_implies_code_eq (1)
  147. 0147specialize signed_decoded_balance_implies_code_eq (0)
  148. 0148apply signed_decoded_balance_implies_code_eq
  149. 0149exact hb_witness_witness
  150. 0150exact hplus
  151. 0151simp [hparts_right, hnb_right, zero_add]