ZU0007

dirichlet_signed_unit_multiply_cancel_right

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 24 exact native proof lines.

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

Proof neighborhood

Direct dependencies

signed_mul_functional Alpha theorem; checked-use authorized ZU0006 dirichlet_signed_unit_multiply_involution

Direct dependents

ZU0009 dirichlet_signed_unit_affine_unique

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

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.

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