ZU0008

dirichlet_signed_unit_affine_solve

Given either actual signed unit, construct both x and its actual product y with r+y=e; no difference, product or solution witness is supplied.

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. SignedUnit(u) → ∃ x. ∃ y. SignedMul(x,u,y) ∧ SignedAdd(r,y,e)

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_solvesigned_mul_total · checked external prerequisitedirichlet_signed_unit_multiply_involution
Original expanded first-order statement 
forall r u e. (((u) = 2 \/ (u) = 1)) -> exists x y. ((exists sto_ap_affine_product sto_an_affine_product sto_bp_affine_product sto_bn_affine_product sto_cp_affine_product sto_cn_affine_product. (((((x) = 2 * (sto_ap_affine_product) /\ (sto_an_affine_product) = 0) \/ exists ge_signed_half_affine_productleft. (((x) = 2 * ge_signed_half_affine_productleft + 1 /\ (sto_ap_affine_product) = 0) /\ (sto_an_affine_product) = S ge_signed_half_affine_productleft))) /\ ((((((u) = 2 * (sto_bp_affine_product) /\ (sto_bn_affine_product) = 0) \/ exists ge_signed_half_affine_productright. (((u) = 2 * ge_signed_half_affine_productright + 1 /\ (sto_bp_affine_product) = 0) /\ (sto_bn_affine_product) = S ge_signed_half_affine_productright))) /\ ((((((y) = 2 * (sto_cp_affine_product) /\ (sto_cn_affine_product) = 0) \/ exists ge_signed_half_affine_productoutput. (((y) = 2 * ge_signed_half_affine_productoutput + 1 /\ (sto_cp_affine_product) = 0) /\ (sto_cn_affine_product) = S ge_signed_half_affine_productoutput))) /\ ((sto_ap_affine_product * sto_bp_affine_product + sto_an_affine_product * sto_bn_affine_product) + sto_cn_affine_product = (sto_ap_affine_product * sto_bn_affine_product + sto_an_affine_product * sto_bp_affine_product) + sto_cp_affine_product))))))) /\ (exists dsa_ap_affine_result dsa_an_affine_result dsa_bp_affine_result dsa_bn_affine_result dsa_cp_affine_result dsa_cn_affine_result. (((((r) = 2 * (dsa_ap_affine_result) /\ (dsa_an_affine_result) = 0) \/ exists ge_signed_half_affine_resultleft. (((r) = 2 * ge_signed_half_affine_resultleft + 1 /\ (dsa_ap_affine_result) = 0) /\ (dsa_an_affine_result) = S ge_signed_half_affine_resultleft))) /\ ((((((y) = 2 * (dsa_bp_affine_result) /\ (dsa_bn_affine_result) = 0) \/ exists ge_signed_half_affine_resultright. (((y) = 2 * ge_signed_half_affine_resultright + 1 /\ (dsa_bp_affine_result) = 0) /\ (dsa_bn_affine_result) = S ge_signed_half_affine_resultright))) /\ ((((((e) = 2 * (dsa_cp_affine_result) /\ (dsa_cn_affine_result) = 0) \/ exists ge_signed_half_affine_resultoutput. (((e) = 2 * ge_signed_half_affine_resultoutput + 1 /\ (dsa_cp_affine_result) = 0) /\ (dsa_cn_affine_result) = S ge_signed_half_affine_resultoutput))) /\ ((dsa_ap_affine_result + dsa_bp_affine_result) + dsa_cn_affine_result = (dsa_an_affine_result + dsa_bn_affine_result) + dsa_cp_affine_result))))))))

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 · 8 reading checkpoints · 2 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 solvedirichlet signed unit multiply involution
01Fix variables and assumptionsL1–4

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 hu
02Establish hyL5–8

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

  1. L5
    have hy : ∃ y. SignedAdd(r,y,e)Definitions: SignedAdd(r,y,e)Original native command in the exact edition
  2. L6
    specialize dirichlet_signed_add_solve (r)
  3. L7
    specialize dirichlet_signed_add_solve (e)
  4. L8
    apply dirichlet_signed_add_solve
03Separate the logical casesL9–9

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

  1. L9
    cases hy
04Establish hxL10–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed mul total.

  1. L10
    have hx : ∃ a. SignedMul(x,u,a)Definitions: SignedMul(x,u,a)Original native command in the exact edition
  2. L11
    specialize signed_mul_total (x)
  3. L12
    specialize signed_mul_total (u)
  4. L13
    apply signed_mul_total
05Separate the logical casesL14–14

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

  1. L14
    cases hx
06Construct an explicit witnessL15–16

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists x1
  2. L16
    exists x
07Separate the logical casesL17–17

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

  1. L17
    split
08Use earlier factsL18–24

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

  1. L18
    specialize dirichlet_signed_unit_multiply_involution (u)
  2. L19
    specialize dirichlet_signed_unit_multiply_involution (x)
  3. L20
    specialize dirichlet_signed_unit_multiply_involution (x1)
  4. L21
    apply dirichlet_signed_unit_multiply_involution
  5. L22
    exact hu
  6. L23
    exact hx_witness
  7. L24
    exact hy_witness

Library-wide reading audit

Original defined command ledger · 24 lines
  1. 0001intro r
  2. 0002intro u
  3. 0003intro e
  4. 0004intro hu
  5. 0005have hy : ∃ y. SignedAdd(r,y,e)
  6. 0006specialize dirichlet_signed_add_solve (r)
  7. 0007specialize dirichlet_signed_add_solve (e)
  8. 0008apply dirichlet_signed_add_solve
  9. 0009cases hy
  10. 0010have hx : ∃ a. SignedMul(x,u,a)
  11. 0011specialize signed_mul_total (x)
  12. 0012specialize signed_mul_total (u)
  13. 0013apply signed_mul_total
  14. 0014cases hx
  15. 0015exists x1
  16. 0016exists x
  17. 0017split
  18. 0018specialize dirichlet_signed_unit_multiply_involution (u)
  19. 0019specialize dirichlet_signed_unit_multiply_involution (x)
  20. 0020specialize dirichlet_signed_unit_multiply_involution (x1)
  21. 0021apply dirichlet_signed_unit_multiply_involution
  22. 0022exact hu
  23. 0023exact hx_witness
  24. 0024exact hy_witness