ZU0001

dirichlet_signed_unit_self_product

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

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

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 expanded first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

signed_mul_one_right Alpha theorem; checked-use authorized signed_mul_of_decoded_equation Alpha theorem; checked-use authorized mul_one Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized

Direct dependents

ZU0003 dirichlet_signed_unit_inverse_iff ZU0006 dirichlet_signed_unit_multiply_involution

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

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.

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 exact 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