ZU0005

dirichlet_signed_add_solve

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

Construct the signed addend taking any canonical signed r to any canonical signed e, including zero and negative values.

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 e. exists y. (exists dsa_ap_add_solve dsa_an_add_solve dsa_bp_add_solve dsa_bn_add_solve dsa_cp_add_solve dsa_cn_add_solve. (((((r) = 2 * (dsa_ap_add_solve) /\ (dsa_an_add_solve) = 0) \/ exists ge_signed_half_add_solveleft. (((r) = 2 * ge_signed_half_add_solveleft + 1 /\ (dsa_ap_add_solve) = 0) /\ (dsa_an_add_solve) = S ge_signed_half_add_solveleft))) /\ ((((((y) = 2 * (dsa_bp_add_solve) /\ (dsa_bn_add_solve) = 0) \/ exists ge_signed_half_add_solveright. (((y) = 2 * ge_signed_half_add_solveright + 1 /\ (dsa_bp_add_solve) = 0) /\ (dsa_bn_add_solve) = S ge_signed_half_add_solveright))) /\ ((((((e) = 2 * (dsa_cp_add_solve) /\ (dsa_cn_add_solve) = 0) \/ exists ge_signed_half_add_solveoutput. (((e) = 2 * ge_signed_half_add_solveoutput + 1 /\ (dsa_cp_add_solve) = 0) /\ (dsa_cn_add_solve) = S ge_signed_half_add_solveoutput))) /\ ((dsa_ap_add_solve + dsa_bp_add_solve) + dsa_cn_add_solve = (dsa_an_add_solve + dsa_bn_add_solve) + dsa_cp_add_solve)))))))

Constructive proof overview

Generated structural guide

Construct the signed addend taking any canonical signed r to any canonical signed e, including zero and negative values.

The unchanged tactic script uses 5 declared prerequisites and contains 26 exact native proof lines.

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

Proof neighborhood

Direct dependencies

signed_negate_total Alpha theorem; checked-use authorized signed_add_total Alpha theorem; checked-use authorized signed_add_associative Alpha theorem; checked-use authorized signed_add_negate_right_zero Alpha theorem; checked-use authorized signed_add_zero_left Alpha theorem; checked-use authorized

Direct dependents

ZU0008 dirichlet_signed_unit_affine_solve

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

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

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro r
  2. L2
    intro e
02Establish hnL3–5

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

  1. L3
    have hn : ∃ n. ∃ x. ∃ y. SignedDecode(r,x,y) ∧ SignedDecode(n,y,x)Definitions: SignedDecode
  2. L4
    specialize signed_negate_total (r)
  3. L5
    apply signed_negate_total
03Separate the logical casesL6–6

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

  1. L6
    cases hn
04Establish hyL7–10

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

  1. L7
    have hy : ∃ y. SignedAdd(x,e,y)Definitions: SignedAdd
  2. L8
    specialize signed_add_total (x)
  3. L9
    specialize signed_add_total (e)
  4. L10
    apply signed_add_total
05Separate the logical casesL11–11

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

  1. L11
    cases hy
06Construct an explicit witnessL12–12

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

  1. L12
    exists x1
07Use earlier factsL13–22

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

  1. L13
    specialize signed_add_associative (r)
  2. L14
    specialize signed_add_associative (x)
  3. L15
    specialize signed_add_associative (e)
  4. L16
    specialize signed_add_associative (0)
  5. L17
    specialize signed_add_associative (x1)
  6. L18
    specialize signed_add_associative (e)
  7. L19
    apply signed_add_associative
  8. L20
    specialize signed_add_negate_right_zero (r)
  9. L21
    specialize signed_add_negate_right_zero (x)
  10. L22
    apply signed_add_negate_right_zero
08Use earlier factsL23–26

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

  1. L23
    exact hn_witness
  2. L24
    specialize signed_add_zero_left (e)
  3. L25
    apply signed_add_zero_left
  4. L26
    exact hy_witness

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro r
  2. 0002intro e
  3. 0003have hn : exists n. (exists mps_positive_solve_negate mps_negative_solve_negate. (((((r) = 2 * (mps_positive_solve_negate) /\ (mps_negative_solve_negate) = 0) \/ exists ge_signed_half_solve_negatesource. (((r) = 2 * ge_signed_half_solve_negatesource + 1 /\ (mps_positive_solve_negate) = 0) /\ (mps_negative_solve_negate) = S ge_signed_half_solve_negatesource))) /\ ((((n) = 2 * (mps_negative_solve_negate) /\ (mps_positive_solve_negate) = 0) \/ exists ge_signed_half_solve_negatetarget. (((n) = 2 * ge_signed_half_solve_negatetarget + 1 /\ (mps_negative_solve_negate) = 0) /\ (mps_positive_solve_negate) = S ge_signed_half_solve_negatetarget)))))
  4. 0004specialize signed_negate_total (r)
  5. 0005apply signed_negate_total
  6. 0006cases hn
  7. 0007have hy : exists y. (exists dsa_ap_solve_addend dsa_an_solve_addend dsa_bp_solve_addend dsa_bn_solve_addend dsa_cp_solve_addend dsa_cn_solve_addend. (((((x) = 2 * (dsa_ap_solve_addend) /\ (dsa_an_solve_addend) = 0) \/ exists ge_signed_half_solve_addendleft. (((x) = 2 * ge_signed_half_solve_addendleft + 1 /\ (dsa_ap_solve_addend) = 0) /\ (dsa_an_solve_addend) = S ge_signed_half_solve_addendleft))) /\ ((((((e) = 2 * (dsa_bp_solve_addend) /\ (dsa_bn_solve_addend) = 0) \/ exists ge_signed_half_solve_addendright. (((e) = 2 * ge_signed_half_solve_addendright + 1 /\ (dsa_bp_solve_addend) = 0) /\ (dsa_bn_solve_addend) = S ge_signed_half_solve_addendright))) /\ ((((((y) = 2 * (dsa_cp_solve_addend) /\ (dsa_cn_solve_addend) = 0) \/ exists ge_signed_half_solve_addendoutput. (((y) = 2 * ge_signed_half_solve_addendoutput + 1 /\ (dsa_cp_solve_addend) = 0) /\ (dsa_cn_solve_addend) = S ge_signed_half_solve_addendoutput))) /\ ((dsa_ap_solve_addend + dsa_bp_solve_addend) + dsa_cn_solve_addend = (dsa_an_solve_addend + dsa_bn_solve_addend) + dsa_cp_solve_addend)))))))
  8. 0008specialize signed_add_total (x)
  9. 0009specialize signed_add_total (e)
  10. 0010apply signed_add_total
  11. 0011cases hy
  12. 0012exists x1
  13. 0013specialize signed_add_associative (r)
  14. 0014specialize signed_add_associative (x)
  15. 0015specialize signed_add_associative (e)
  16. 0016specialize signed_add_associative (0)
  17. 0017specialize signed_add_associative (x1)
  18. 0018specialize signed_add_associative (e)
  19. 0019apply signed_add_associative
  20. 0020specialize signed_add_negate_right_zero (r)
  21. 0021specialize signed_add_negate_right_zero (x)
  22. 0022apply signed_add_negate_right_zero
  23. 0023exact hn_witness
  24. 0024specialize signed_add_zero_left (e)
  25. 0025apply signed_add_zero_left
  26. 0026exact hy_witness