WS0018

signed_table_add_reassociate

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Constructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.

Exact expanded first-order arithmetic statement

forall a b c ab bc out. (exists dsa_ap_reverse_ab dsa_an_reverse_ab dsa_bp_reverse_ab dsa_bn_reverse_ab dsa_cp_reverse_ab dsa_cn_reverse_ab. (((((a) = 2 * (dsa_ap_reverse_ab) /\ (dsa_an_reverse_ab) = 0) \/ exists ge_signed_half_reverse_ableft. (((a) = 2 * ge_signed_half_reverse_ableft + 1 /\ (dsa_ap_reverse_ab) = 0) /\ (dsa_an_reverse_ab) = S ge_signed_half_reverse_ableft))) /\ ((((((b) = 2 * (dsa_bp_reverse_ab) /\ (dsa_bn_reverse_ab) = 0) \/ exists ge_signed_half_reverse_abright. (((b) = 2 * ge_signed_half_reverse_abright + 1 /\ (dsa_bp_reverse_ab) = 0) /\ (dsa_bn_reverse_ab) = S ge_signed_half_reverse_abright))) /\ ((((((ab) = 2 * (dsa_cp_reverse_ab) /\ (dsa_cn_reverse_ab) = 0) \/ exists ge_signed_half_reverse_aboutput. (((ab) = 2 * ge_signed_half_reverse_aboutput + 1 /\ (dsa_cp_reverse_ab) = 0) /\ (dsa_cn_reverse_ab) = S ge_signed_half_reverse_aboutput))) /\ ((dsa_ap_reverse_ab + dsa_bp_reverse_ab) + dsa_cn_reverse_ab = (dsa_an_reverse_ab + dsa_bn_reverse_ab) + dsa_cp_reverse_ab))))))) -> (exists dsa_ap_reverse_bc dsa_an_reverse_bc dsa_bp_reverse_bc dsa_bn_reverse_bc dsa_cp_reverse_bc dsa_cn_reverse_bc. (((((b) = 2 * (dsa_ap_reverse_bc) /\ (dsa_an_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcleft. (((b) = 2 * ge_signed_half_reverse_bcleft + 1 /\ (dsa_ap_reverse_bc) = 0) /\ (dsa_an_reverse_bc) = S ge_signed_half_reverse_bcleft))) /\ ((((((c) = 2 * (dsa_bp_reverse_bc) /\ (dsa_bn_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcright. (((c) = 2 * ge_signed_half_reverse_bcright + 1 /\ (dsa_bp_reverse_bc) = 0) /\ (dsa_bn_reverse_bc) = S ge_signed_half_reverse_bcright))) /\ ((((((bc) = 2 * (dsa_cp_reverse_bc) /\ (dsa_cn_reverse_bc) = 0) \/ exists ge_signed_half_reverse_bcoutput. (((bc) = 2 * ge_signed_half_reverse_bcoutput + 1 /\ (dsa_cp_reverse_bc) = 0) /\ (dsa_cn_reverse_bc) = S ge_signed_half_reverse_bcoutput))) /\ ((dsa_ap_reverse_bc + dsa_bp_reverse_bc) + dsa_cn_reverse_bc = (dsa_an_reverse_bc + dsa_bn_reverse_bc) + dsa_cp_reverse_bc))))))) -> (exists dsa_ap_reverse_out dsa_an_reverse_out dsa_bp_reverse_out dsa_bn_reverse_out dsa_cp_reverse_out dsa_cn_reverse_out. (((((a) = 2 * (dsa_ap_reverse_out) /\ (dsa_an_reverse_out) = 0) \/ exists ge_signed_half_reverse_outleft. (((a) = 2 * ge_signed_half_reverse_outleft + 1 /\ (dsa_ap_reverse_out) = 0) /\ (dsa_an_reverse_out) = S ge_signed_half_reverse_outleft))) /\ ((((((bc) = 2 * (dsa_bp_reverse_out) /\ (dsa_bn_reverse_out) = 0) \/ exists ge_signed_half_reverse_outright. (((bc) = 2 * ge_signed_half_reverse_outright + 1 /\ (dsa_bp_reverse_out) = 0) /\ (dsa_bn_reverse_out) = S ge_signed_half_reverse_outright))) /\ ((((((out) = 2 * (dsa_cp_reverse_out) /\ (dsa_cn_reverse_out) = 0) \/ exists ge_signed_half_reverse_outoutput. (((out) = 2 * ge_signed_half_reverse_outoutput + 1 /\ (dsa_cp_reverse_out) = 0) /\ (dsa_cn_reverse_out) = S ge_signed_half_reverse_outoutput))) /\ ((dsa_ap_reverse_out + dsa_bp_reverse_out) + dsa_cn_reverse_out = (dsa_an_reverse_out + dsa_bn_reverse_out) + dsa_cp_reverse_out))))))) -> (exists dsa_ap_reverse_target dsa_an_reverse_target dsa_bp_reverse_target dsa_bn_reverse_target dsa_cp_reverse_target dsa_cn_reverse_target. (((((ab) = 2 * (dsa_ap_reverse_target) /\ (dsa_an_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetleft. (((ab) = 2 * ge_signed_half_reverse_targetleft + 1 /\ (dsa_ap_reverse_target) = 0) /\ (dsa_an_reverse_target) = S ge_signed_half_reverse_targetleft))) /\ ((((((c) = 2 * (dsa_bp_reverse_target) /\ (dsa_bn_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetright. (((c) = 2 * ge_signed_half_reverse_targetright + 1 /\ (dsa_bp_reverse_target) = 0) /\ (dsa_bn_reverse_target) = S ge_signed_half_reverse_targetright))) /\ ((((((out) = 2 * (dsa_cp_reverse_target) /\ (dsa_cn_reverse_target) = 0) \/ exists ge_signed_half_reverse_targetoutput. (((out) = 2 * ge_signed_half_reverse_targetoutput + 1 /\ (dsa_cp_reverse_target) = 0) /\ (dsa_cn_reverse_target) = S ge_signed_half_reverse_targetoutput))) /\ ((dsa_ap_reverse_target + dsa_bp_reverse_target) + dsa_cn_reverse_target = (dsa_an_reverse_target + dsa_bn_reverse_target) + dsa_cp_reverse_target)))))))

Constructive proof overview

Generated structural guide

Constructing the other parenthesization and applying literal signed-add functionality proves reverse associativity.

The unchanged tactic script uses 3 declared prerequisites and contains 34 exact native proof lines.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

Proof neighborhood

Direct dependencies

signed_add_total Alpha theorem; checked-use authorized signed_add_functional Alpha theorem; checked-use authorized signed_add_associative Alpha theorem; checked-use authorized

Direct dependents

WS0019 signed_table_add_medial

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

34 script commands · 7 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–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro ab
  5. L5
    intro bc
  6. L6
    intro out
  7. L7
    intro hab
  8. L8
    intro hbc
  9. L9
    intro hout
02Establish hwL10–13

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

  1. L10
    have hw : ∃ w. SignedAdd(ab,c,w)Definitions: SignedAdd
  2. L11
    specialize signed_add_total (ab)
  3. L12
    specialize signed_add_total (c)
  4. L13
    apply signed_add_total
03Separate the logical casesL14–14

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

  1. L14
    cases hw
04Establish heqL15–24

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

  1. L15
    have heq : x = out
  2. L16
    specialize signed_add_functional (a)
  3. L17
    specialize signed_add_functional (bc)
  4. L18
    specialize signed_add_functional (x)
  5. L19
    specialize signed_add_functional (out)
  6. L20
    apply signed_add_functional
  7. L21
    specialize signed_add_associative (a)
  8. L22
    specialize signed_add_associative (b)
  9. L23
    specialize signed_add_associative (c)
  10. L24
    specialize signed_add_associative (ab)
05Use earlier factsL25–31

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

  1. L25
    specialize signed_add_associative (bc)
  2. L26
    specialize signed_add_associative (x)
  3. L27
    apply signed_add_associative
  4. L28
    exact hab
  5. L29
    exact hw_witness
  6. L30
    exact hbc
  7. L31
    exact hout
06Calculate and transport equalitiesL32–33

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

  1. L32
    rewrite heq at hw_witness
  2. L33
    rewrite heq at hw_witness
07Use earlier factsL34–34

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

  1. L34
    exact hw_witness

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro ab
  5. 0005intro bc
  6. 0006intro out
  7. 0007intro hab
  8. 0008intro hbc
  9. 0009intro hout
  10. 0010have hw : exists w. (exists dsa_ap_reassociate_construct dsa_an_reassociate_construct dsa_bp_reassociate_construct dsa_bn_reassociate_construct dsa_cp_reassociate_construct dsa_cn_reassociate_construct. (((((ab) = 2 * (dsa_ap_reassociate_construct) /\ (dsa_an_reassociate_construct) = 0) \/ exists ge_signed_half_reassociate_constructleft. (((ab) = 2 * ge_signed_half_reassociate_constructleft + 1 /\ (dsa_ap_reassociate_construct) = 0) /\ (dsa_an_reassociate_construct) = S ge_signed_half_reassociate_constructleft))) /\ ((((((c) = 2 * (dsa_bp_reassociate_construct) /\ (dsa_bn_reassociate_construct) = 0) \/ exists ge_signed_half_reassociate_constructright. (((c) = 2 * ge_signed_half_reassociate_constructright + 1 /\ (dsa_bp_reassociate_construct) = 0) /\ (dsa_bn_reassociate_construct) = S ge_signed_half_reassociate_constructright))) /\ ((((((w) = 2 * (dsa_cp_reassociate_construct) /\ (dsa_cn_reassociate_construct) = 0) \/ exists ge_signed_half_reassociate_constructoutput. (((w) = 2 * ge_signed_half_reassociate_constructoutput + 1 /\ (dsa_cp_reassociate_construct) = 0) /\ (dsa_cn_reassociate_construct) = S ge_signed_half_reassociate_constructoutput))) /\ ((dsa_ap_reassociate_construct + dsa_bp_reassociate_construct) + dsa_cn_reassociate_construct = (dsa_an_reassociate_construct + dsa_bn_reassociate_construct) + dsa_cp_reassociate_construct)))))))
  11. 0011specialize signed_add_total (ab)
  12. 0012specialize signed_add_total (c)
  13. 0013apply signed_add_total
  14. 0014cases hw
  15. 0015have heq : x = out
  16. 0016specialize signed_add_functional (a)
  17. 0017specialize signed_add_functional (bc)
  18. 0018specialize signed_add_functional (x)
  19. 0019specialize signed_add_functional (out)
  20. 0020apply signed_add_functional
  21. 0021specialize signed_add_associative (a)
  22. 0022specialize signed_add_associative (b)
  23. 0023specialize signed_add_associative (c)
  24. 0024specialize signed_add_associative (ab)
  25. 0025specialize signed_add_associative (bc)
  26. 0026specialize signed_add_associative (x)
  27. 0027apply signed_add_associative
  28. 0028exact hab
  29. 0029exact hw_witness
  30. 0030exact hbc
  31. 0031exact hout
  32. 0032rewrite heq at hw_witness
  33. 0033rewrite heq at hw_witness
  34. 0034exact hw_witness