ZU0007

dirichlet_signed_unit_multiply_cancel_right

An actual signed unit can be cancelled from a common right factor without cancelling arbitrary zero or nonunit factors.

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. ∀ a. ∀ b. ∀ z. SignedUnit(u) → SignedMul(a,u,z) → SignedMul(b,u,z) → a = b

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

Definition DAG

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

Actual proof prerequisites

signed_mul_functional · checked external prerequisitedirichlet_signed_unit_multiply_involution
Original expanded first-order statement 
forall u a b z. (((u) = 2 \/ (u) = 1)) -> (exists sto_ap_multiply_cancel_first sto_an_multiply_cancel_first sto_bp_multiply_cancel_first sto_bn_multiply_cancel_first sto_cp_multiply_cancel_first sto_cn_multiply_cancel_first. (((((a) = 2 * (sto_ap_multiply_cancel_first) /\ (sto_an_multiply_cancel_first) = 0) \/ exists ge_signed_half_multiply_cancel_firstleft. (((a) = 2 * ge_signed_half_multiply_cancel_firstleft + 1 /\ (sto_ap_multiply_cancel_first) = 0) /\ (sto_an_multiply_cancel_first) = S ge_signed_half_multiply_cancel_firstleft))) /\ ((((((u) = 2 * (sto_bp_multiply_cancel_first) /\ (sto_bn_multiply_cancel_first) = 0) \/ exists ge_signed_half_multiply_cancel_firstright. (((u) = 2 * ge_signed_half_multiply_cancel_firstright + 1 /\ (sto_bp_multiply_cancel_first) = 0) /\ (sto_bn_multiply_cancel_first) = S ge_signed_half_multiply_cancel_firstright))) /\ ((((((z) = 2 * (sto_cp_multiply_cancel_first) /\ (sto_cn_multiply_cancel_first) = 0) \/ exists ge_signed_half_multiply_cancel_firstoutput. (((z) = 2 * ge_signed_half_multiply_cancel_firstoutput + 1 /\ (sto_cp_multiply_cancel_first) = 0) /\ (sto_cn_multiply_cancel_first) = S ge_signed_half_multiply_cancel_firstoutput))) /\ ((sto_ap_multiply_cancel_first * sto_bp_multiply_cancel_first + sto_an_multiply_cancel_first * sto_bn_multiply_cancel_first) + sto_cn_multiply_cancel_first = (sto_ap_multiply_cancel_first * sto_bn_multiply_cancel_first + sto_an_multiply_cancel_first * sto_bp_multiply_cancel_first) + sto_cp_multiply_cancel_first))))))) -> (exists sto_ap_multiply_cancel_second sto_an_multiply_cancel_second sto_bp_multiply_cancel_second sto_bn_multiply_cancel_second sto_cp_multiply_cancel_second sto_cn_multiply_cancel_second. (((((b) = 2 * (sto_ap_multiply_cancel_second) /\ (sto_an_multiply_cancel_second) = 0) \/ exists ge_signed_half_multiply_cancel_secondleft. (((b) = 2 * ge_signed_half_multiply_cancel_secondleft + 1 /\ (sto_ap_multiply_cancel_second) = 0) /\ (sto_an_multiply_cancel_second) = S ge_signed_half_multiply_cancel_secondleft))) /\ ((((((u) = 2 * (sto_bp_multiply_cancel_second) /\ (sto_bn_multiply_cancel_second) = 0) \/ exists ge_signed_half_multiply_cancel_secondright. (((u) = 2 * ge_signed_half_multiply_cancel_secondright + 1 /\ (sto_bp_multiply_cancel_second) = 0) /\ (sto_bn_multiply_cancel_second) = S ge_signed_half_multiply_cancel_secondright))) /\ ((((((z) = 2 * (sto_cp_multiply_cancel_second) /\ (sto_cn_multiply_cancel_second) = 0) \/ exists ge_signed_half_multiply_cancel_secondoutput. (((z) = 2 * ge_signed_half_multiply_cancel_secondoutput + 1 /\ (sto_cp_multiply_cancel_second) = 0) /\ (sto_cn_multiply_cancel_second) = S ge_signed_half_multiply_cancel_secondoutput))) /\ ((sto_ap_multiply_cancel_second * sto_bp_multiply_cancel_second + sto_an_multiply_cancel_second * sto_bn_multiply_cancel_second) + sto_cn_multiply_cancel_second = (sto_ap_multiply_cancel_second * sto_bn_multiply_cancel_second + sto_an_multiply_cancel_second * sto_bp_multiply_cancel_second) + sto_cp_multiply_cancel_second))))))) -> a=b

Complete tactic proof in conservative notation

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

24 script commands · 3 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.

Named ingredients (1)
dirichlet signed unit multiply involution
01Fix variables and assumptionsL1–7

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

  1. L1
    intro u
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro z
  5. L5
    intro hu
  6. L6
    intro ha
  7. L7
    intro hb
02Use earlier factsL8–17

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

  1. L8
    specialize signed_mul_functional (z)
  2. L9
    specialize signed_mul_functional (u)
  3. L10
    specialize signed_mul_functional (a)
  4. L11
    specialize signed_mul_functional (b)
  5. L12
    apply signed_mul_functional
  6. L13
    specialize dirichlet_signed_unit_multiply_involution (u)
  7. L14
    specialize dirichlet_signed_unit_multiply_involution (a)
  8. L15
    specialize dirichlet_signed_unit_multiply_involution (z)
  9. L16
    apply dirichlet_signed_unit_multiply_involution
  10. L17
    exact hu
03Use earlier factsL18–24

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

  1. L18
    exact ha
  2. L19
    specialize dirichlet_signed_unit_multiply_involution (u)
  3. L20
    specialize dirichlet_signed_unit_multiply_involution (b)
  4. L21
    specialize dirichlet_signed_unit_multiply_involution (z)
  5. L22
    apply dirichlet_signed_unit_multiply_involution
  6. L23
    exact hu
  7. L24
    exact hb

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro u
  2. 0002intro a
  3. 0003intro b
  4. 0004intro z
  5. 0005intro hu
  6. 0006intro ha
  7. 0007intro hb
  8. 0008specialize signed_mul_functional (z)
  9. 0009specialize signed_mul_functional (u)
  10. 0010specialize signed_mul_functional (a)
  11. 0011specialize signed_mul_functional (b)
  12. 0012apply signed_mul_functional
  13. 0013specialize dirichlet_signed_unit_multiply_involution (u)
  14. 0014specialize dirichlet_signed_unit_multiply_involution (a)
  15. 0015specialize dirichlet_signed_unit_multiply_involution (z)
  16. 0016apply dirichlet_signed_unit_multiply_involution
  17. 0017exact hu
  18. 0018exact ha
  19. 0019specialize dirichlet_signed_unit_multiply_involution (u)
  20. 0020specialize dirichlet_signed_unit_multiply_involution (b)
  21. 0021specialize dirichlet_signed_unit_multiply_involution (z)
  22. 0022apply dirichlet_signed_unit_multiply_involution
  23. 0023exact hu
  24. 0024exact hb