ZU0009

dirichlet_signed_unit_affine_unique

Any two witnessed solutions of the same unit-affine equation have equal canonical inputs and equal actual product outputs.

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

∀ r. ∀ u. ∀ e. ∀ a. ∀ b. ∀ c. ∀ d. SignedUnit(u) → SignedMul(a,u,b) → SignedAdd(r,b,e) → SignedMul(c,u,d) → SignedAdd(r,d,e) → a = c ∧ b = d

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

Definition DAG

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

Actual proof prerequisites

dirichlet_signed_add_cancel_leftdirichlet_signed_unit_multiply_cancel_right
Original expanded first-order statement 
forall r u e a b c d. (((u) = 2 \/ (u) = 1)) -> (exists sto_ap_affine_unique_first_product sto_an_affine_unique_first_product sto_bp_affine_unique_first_product sto_bn_affine_unique_first_product sto_cp_affine_unique_first_product sto_cn_affine_unique_first_product. (((((a) = 2 * (sto_ap_affine_unique_first_product) /\ (sto_an_affine_unique_first_product) = 0) \/ exists ge_signed_half_affine_unique_first_productleft. (((a) = 2 * ge_signed_half_affine_unique_first_productleft + 1 /\ (sto_ap_affine_unique_first_product) = 0) /\ (sto_an_affine_unique_first_product) = S ge_signed_half_affine_unique_first_productleft))) /\ ((((((u) = 2 * (sto_bp_affine_unique_first_product) /\ (sto_bn_affine_unique_first_product) = 0) \/ exists ge_signed_half_affine_unique_first_productright. (((u) = 2 * ge_signed_half_affine_unique_first_productright + 1 /\ (sto_bp_affine_unique_first_product) = 0) /\ (sto_bn_affine_unique_first_product) = S ge_signed_half_affine_unique_first_productright))) /\ ((((((b) = 2 * (sto_cp_affine_unique_first_product) /\ (sto_cn_affine_unique_first_product) = 0) \/ exists ge_signed_half_affine_unique_first_productoutput. (((b) = 2 * ge_signed_half_affine_unique_first_productoutput + 1 /\ (sto_cp_affine_unique_first_product) = 0) /\ (sto_cn_affine_unique_first_product) = S ge_signed_half_affine_unique_first_productoutput))) /\ ((sto_ap_affine_unique_first_product * sto_bp_affine_unique_first_product + sto_an_affine_unique_first_product * sto_bn_affine_unique_first_product) + sto_cn_affine_unique_first_product = (sto_ap_affine_unique_first_product * sto_bn_affine_unique_first_product + sto_an_affine_unique_first_product * sto_bp_affine_unique_first_product) + sto_cp_affine_unique_first_product))))))) -> (exists dsa_ap_affine_unique_first_sum dsa_an_affine_unique_first_sum dsa_bp_affine_unique_first_sum dsa_bn_affine_unique_first_sum dsa_cp_affine_unique_first_sum dsa_cn_affine_unique_first_sum. (((((r) = 2 * (dsa_ap_affine_unique_first_sum) /\ (dsa_an_affine_unique_first_sum) = 0) \/ exists ge_signed_half_affine_unique_first_sumleft. (((r) = 2 * ge_signed_half_affine_unique_first_sumleft + 1 /\ (dsa_ap_affine_unique_first_sum) = 0) /\ (dsa_an_affine_unique_first_sum) = S ge_signed_half_affine_unique_first_sumleft))) /\ ((((((b) = 2 * (dsa_bp_affine_unique_first_sum) /\ (dsa_bn_affine_unique_first_sum) = 0) \/ exists ge_signed_half_affine_unique_first_sumright. (((b) = 2 * ge_signed_half_affine_unique_first_sumright + 1 /\ (dsa_bp_affine_unique_first_sum) = 0) /\ (dsa_bn_affine_unique_first_sum) = S ge_signed_half_affine_unique_first_sumright))) /\ ((((((e) = 2 * (dsa_cp_affine_unique_first_sum) /\ (dsa_cn_affine_unique_first_sum) = 0) \/ exists ge_signed_half_affine_unique_first_sumoutput. (((e) = 2 * ge_signed_half_affine_unique_first_sumoutput + 1 /\ (dsa_cp_affine_unique_first_sum) = 0) /\ (dsa_cn_affine_unique_first_sum) = S ge_signed_half_affine_unique_first_sumoutput))) /\ ((dsa_ap_affine_unique_first_sum + dsa_bp_affine_unique_first_sum) + dsa_cn_affine_unique_first_sum = (dsa_an_affine_unique_first_sum + dsa_bn_affine_unique_first_sum) + dsa_cp_affine_unique_first_sum))))))) -> (exists sto_ap_affine_unique_second_product sto_an_affine_unique_second_product sto_bp_affine_unique_second_product sto_bn_affine_unique_second_product sto_cp_affine_unique_second_product sto_cn_affine_unique_second_product. (((((c) = 2 * (sto_ap_affine_unique_second_product) /\ (sto_an_affine_unique_second_product) = 0) \/ exists ge_signed_half_affine_unique_second_productleft. (((c) = 2 * ge_signed_half_affine_unique_second_productleft + 1 /\ (sto_ap_affine_unique_second_product) = 0) /\ (sto_an_affine_unique_second_product) = S ge_signed_half_affine_unique_second_productleft))) /\ ((((((u) = 2 * (sto_bp_affine_unique_second_product) /\ (sto_bn_affine_unique_second_product) = 0) \/ exists ge_signed_half_affine_unique_second_productright. (((u) = 2 * ge_signed_half_affine_unique_second_productright + 1 /\ (sto_bp_affine_unique_second_product) = 0) /\ (sto_bn_affine_unique_second_product) = S ge_signed_half_affine_unique_second_productright))) /\ ((((((d) = 2 * (sto_cp_affine_unique_second_product) /\ (sto_cn_affine_unique_second_product) = 0) \/ exists ge_signed_half_affine_unique_second_productoutput. (((d) = 2 * ge_signed_half_affine_unique_second_productoutput + 1 /\ (sto_cp_affine_unique_second_product) = 0) /\ (sto_cn_affine_unique_second_product) = S ge_signed_half_affine_unique_second_productoutput))) /\ ((sto_ap_affine_unique_second_product * sto_bp_affine_unique_second_product + sto_an_affine_unique_second_product * sto_bn_affine_unique_second_product) + sto_cn_affine_unique_second_product = (sto_ap_affine_unique_second_product * sto_bn_affine_unique_second_product + sto_an_affine_unique_second_product * sto_bp_affine_unique_second_product) + sto_cp_affine_unique_second_product))))))) -> (exists dsa_ap_affine_unique_second_sum dsa_an_affine_unique_second_sum dsa_bp_affine_unique_second_sum dsa_bn_affine_unique_second_sum dsa_cp_affine_unique_second_sum dsa_cn_affine_unique_second_sum. (((((r) = 2 * (dsa_ap_affine_unique_second_sum) /\ (dsa_an_affine_unique_second_sum) = 0) \/ exists ge_signed_half_affine_unique_second_sumleft. (((r) = 2 * ge_signed_half_affine_unique_second_sumleft + 1 /\ (dsa_ap_affine_unique_second_sum) = 0) /\ (dsa_an_affine_unique_second_sum) = S ge_signed_half_affine_unique_second_sumleft))) /\ ((((((d) = 2 * (dsa_bp_affine_unique_second_sum) /\ (dsa_bn_affine_unique_second_sum) = 0) \/ exists ge_signed_half_affine_unique_second_sumright. (((d) = 2 * ge_signed_half_affine_unique_second_sumright + 1 /\ (dsa_bp_affine_unique_second_sum) = 0) /\ (dsa_bn_affine_unique_second_sum) = S ge_signed_half_affine_unique_second_sumright))) /\ ((((((e) = 2 * (dsa_cp_affine_unique_second_sum) /\ (dsa_cn_affine_unique_second_sum) = 0) \/ exists ge_signed_half_affine_unique_second_sumoutput. (((e) = 2 * ge_signed_half_affine_unique_second_sumoutput + 1 /\ (dsa_cp_affine_unique_second_sum) = 0) /\ (dsa_cn_affine_unique_second_sum) = S ge_signed_half_affine_unique_second_sumoutput))) /\ ((dsa_ap_affine_unique_second_sum + dsa_bp_affine_unique_second_sum) + dsa_cn_affine_unique_second_sum = (dsa_an_affine_unique_second_sum + dsa_bn_affine_unique_second_sum) + dsa_cp_affine_unique_second_sum))))))) -> a=c /\ b=d

Complete tactic proof in conservative notation

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

32 script commands · 7 reading checkpoints · 1 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 (2)
dirichlet signed add cancel leftdirichlet signed unit multiply cancel right
01Fix variables and assumptionsL1–10

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

  1. L1
    intro r
  2. L2
    intro u
  3. L3
    intro e
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro hu
  9. L9
    intro hab
  10. L10
    intro hbe
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hcd
  2. L12
    intro hde
03Establish heqL13–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet signed add cancel left.

  1. L13
    have heq : b=d
  2. L14
    specialize dirichlet_signed_add_cancel_left (r)
  3. L15
    specialize dirichlet_signed_add_cancel_left (b)
  4. L16
    specialize dirichlet_signed_add_cancel_left (d)
  5. L17
    specialize dirichlet_signed_add_cancel_left (e)
  6. L18
    apply dirichlet_signed_add_cancel_left
  7. L19
    exact hbe
  8. L20
    exact hde
04Separate the logical casesL21–21

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

  1. L21
    split
05Use earlier factsL22–27

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

  1. L22
    specialize dirichlet_signed_unit_multiply_cancel_right (u)
  2. L23
    specialize dirichlet_signed_unit_multiply_cancel_right (a)
  3. L24
    specialize dirichlet_signed_unit_multiply_cancel_right (c)
  4. L25
    specialize dirichlet_signed_unit_multiply_cancel_right (d)
  5. L26
    apply dirichlet_signed_unit_multiply_cancel_right
  6. L27
    exact hu
06Calculate and transport equalitiesL28–29

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

  1. L28
    rewrite heq at hab
  2. L29
    rewrite heq at hab
07Use earlier factsL30–32

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

  1. L30
    exact hab
  2. L31
    exact hcd
  3. L32
    exact heq

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro r
  2. 0002intro u
  3. 0003intro e
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro hu
  9. 0009intro hab
  10. 0010intro hbe
  11. 0011intro hcd
  12. 0012intro hde
  13. 0013have heq : b=d
  14. 0014specialize dirichlet_signed_add_cancel_left (r)
  15. 0015specialize dirichlet_signed_add_cancel_left (b)
  16. 0016specialize dirichlet_signed_add_cancel_left (d)
  17. 0017specialize dirichlet_signed_add_cancel_left (e)
  18. 0018apply dirichlet_signed_add_cancel_left
  19. 0019exact hbe
  20. 0020exact hde
  21. 0021split
  22. 0022specialize dirichlet_signed_unit_multiply_cancel_right (u)
  23. 0023specialize dirichlet_signed_unit_multiply_cancel_right (a)
  24. 0024specialize dirichlet_signed_unit_multiply_cancel_right (c)
  25. 0025specialize dirichlet_signed_unit_multiply_cancel_right (d)
  26. 0026apply dirichlet_signed_unit_multiply_cancel_right
  27. 0027exact hu
  28. 0028rewrite heq at hab
  29. 0029rewrite heq at hab
  30. 0030exact hab
  31. 0031exact hcd
  32. 0032exact heq