ZU0001

dirichlet_signed_unit_self_product

Each of the two canonical signed units has an actual signed square equal to positive one.

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

∀ u. SignedUnit(u) → SignedMul(u,u,2)

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

Definition DAG

SignedMul(a,b,c) · 1SignedUnit(u) · 1

Actual proof prerequisites

signed_mul_one_right · checked external prerequisitesigned_mul_of_decoded_equation · checked external prerequisitemul_one · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall u. (((u) = 2 \/ (u) = 1)) -> (exists sto_ap_self_product sto_an_self_product sto_bp_self_product sto_bn_self_product sto_cp_self_product sto_cn_self_product. (((((u) = 2 * (sto_ap_self_product) /\ (sto_an_self_product) = 0) \/ exists ge_signed_half_self_productleft. (((u) = 2 * ge_signed_half_self_productleft + 1 /\ (sto_ap_self_product) = 0) /\ (sto_an_self_product) = S ge_signed_half_self_productleft))) /\ ((((((u) = 2 * (sto_bp_self_product) /\ (sto_bn_self_product) = 0) \/ exists ge_signed_half_self_productright. (((u) = 2 * ge_signed_half_self_productright + 1 /\ (sto_bp_self_product) = 0) /\ (sto_bn_self_product) = S ge_signed_half_self_productright))) /\ ((((((2) = 2 * (sto_cp_self_product) /\ (sto_cn_self_product) = 0) \/ exists ge_signed_half_self_productoutput. (((2) = 2 * ge_signed_half_self_productoutput + 1 /\ (sto_cp_self_product) = 0) /\ (sto_cn_self_product) = S ge_signed_half_self_productoutput))) /\ ((sto_ap_self_product * sto_bp_self_product + sto_an_self_product * sto_bn_self_product) + sto_cn_self_product = (sto_ap_self_product * sto_bn_self_product + sto_an_self_product * sto_bp_self_product) + sto_cp_self_product)))))))

Complete tactic proof in conservative notation

All 47 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

47 script commands · 22 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.

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–2

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

  1. L1
    intro u
  2. L2
    intro hu
02Separate the logical casesL3–3

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

  1. L3
    cases hu
03Calculate and transport equalitiesL4–7

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

  1. L4
    rewrite hu_left
  2. L5
    rewrite hu_left
  3. L6
    rewrite hu_left
  4. L7
    rewrite hu_left
04Use earlier factsL8–9

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

  1. L8
    specialize signed_mul_one_right (2)
  2. L9
    apply signed_mul_one_right
05Calculate and transport equalitiesL10–13

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

  1. L10
    rewrite hu_right
  2. L11
    rewrite hu_right
  3. L12
    rewrite hu_right
  4. L13
    rewrite hu_right
06Use earlier factsL14–23

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

  1. L14
    specialize signed_mul_of_decoded_equation (1)
  2. L15
    specialize signed_mul_of_decoded_equation (1)
  3. L16
    specialize signed_mul_of_decoded_equation (2)
  4. L17
    specialize signed_mul_of_decoded_equation (0)
  5. L18
    specialize signed_mul_of_decoded_equation (1)
  6. L19
    specialize signed_mul_of_decoded_equation (0)
  7. L20
    specialize signed_mul_of_decoded_equation (1)
  8. L21
    specialize signed_mul_of_decoded_equation (1)
  9. L22
    specialize signed_mul_of_decoded_equation (0)
  10. L23
    apply signed_mul_of_decoded_equation
07Separate the logical casesL24–24

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

  1. L24
    right
08Construct an explicit witnessL25–25

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

  1. L25
    exists 0
09Separate the logical casesL26–27

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

  1. L26
    split
  2. L27
    split
10Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite PA5
  2. L29
    symm
11Use earlier factsL30–30

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

  1. L30
    apply zero_add
12Calculate and transport equalitiesL31–32

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

  1. L31
    refl
  2. L32
    refl
13Separate the logical casesL33–33

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

  1. L33
    right
14Construct an explicit witnessL34–34

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

  1. L34
    exists 0
15Separate the logical casesL35–36

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

  1. L35
    split
  2. L36
    split
16Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite PA5
  2. L38
    symm
17Use earlier factsL39–39

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

  1. L39
    apply zero_add
18Calculate and transport equalitiesL40–41

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

  1. L40
    refl
  2. L41
    refl
19Separate the logical casesL42–43

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

  1. L42
    left
  2. L43
    split
20Calculate and transport equalitiesL44–44

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

  1. L44
    symm
21Use earlier factsL45–45

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

  1. L45
    apply mul_one
22Calculate and transport equalitiesL46–47

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

  1. L46
    refl
  2. L47
    simp

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro u
  2. 0002intro hu
  3. 0003cases hu
  4. 0004rewrite hu_left
  5. 0005rewrite hu_left
  6. 0006rewrite hu_left
  7. 0007rewrite hu_left
  8. 0008specialize signed_mul_one_right (2)
  9. 0009apply signed_mul_one_right
  10. 0010rewrite hu_right
  11. 0011rewrite hu_right
  12. 0012rewrite hu_right
  13. 0013rewrite hu_right
  14. 0014specialize signed_mul_of_decoded_equation (1)
  15. 0015specialize signed_mul_of_decoded_equation (1)
  16. 0016specialize signed_mul_of_decoded_equation (2)
  17. 0017specialize signed_mul_of_decoded_equation (0)
  18. 0018specialize signed_mul_of_decoded_equation (1)
  19. 0019specialize signed_mul_of_decoded_equation (0)
  20. 0020specialize signed_mul_of_decoded_equation (1)
  21. 0021specialize signed_mul_of_decoded_equation (1)
  22. 0022specialize signed_mul_of_decoded_equation (0)
  23. 0023apply signed_mul_of_decoded_equation
  24. 0024right
  25. 0025exists 0
  26. 0026split
  27. 0027split
  28. 0028rewrite PA5
  29. 0029symm
  30. 0030apply zero_add
  31. 0031refl
  32. 0032refl
  33. 0033right
  34. 0034exists 0
  35. 0035split
  36. 0036split
  37. 0037rewrite PA5
  38. 0038symm
  39. 0039apply zero_add
  40. 0040refl
  41. 0041refl
  42. 0042left
  43. 0043split
  44. 0044symm
  45. 0045apply mul_one
  46. 0046refl
  47. 0047simp