ZU0009

dirichlet_signed_unit_affine_unique

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

ZU0004 dirichlet_signed_add_cancel_left ZU0007 dirichlet_signed_unit_multiply_cancel_right

Direct dependents

none

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

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.

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