WS001A

signed_table_scalar_add_intro

An actual sum of the two scalar products is the actual scalar multiple of the sum; no product witness or distributivity oracle is assumed.

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.

Operation tables contain actual beta-coded entries and compare represented signed values, not encodings. The strict sum window is i<l and the separately certified endpoint i=l is unused. Rectangular Fubini and full finite signed Möbius inversion are separate, now-admitted families.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ bc. ∀ ab. ∀ ac. ∀ out. SignedAdd(b,c,bc) → SignedMul(a,b,ab) → SignedMul(a,c,ac) → SignedAdd(ab,ac,out) → SignedMul(a,bc,out)

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

Definition DAG

SignedAdd(a,b,c) · 2SignedMul(a,b,c) · 4

Actual proof prerequisites

signed_mul_total · checked external prerequisitesigned_mul_left_distributive · checked external prerequisitesigned_add_functional · checked external prerequisite
Original expanded first-order statement 
forall a b c bc ab ac out. (exists dsa_ap_scalar_intro_sum dsa_an_scalar_intro_sum dsa_bp_scalar_intro_sum dsa_bn_scalar_intro_sum dsa_cp_scalar_intro_sum dsa_cn_scalar_intro_sum. (((((b) = 2 * (dsa_ap_scalar_intro_sum) /\ (dsa_an_scalar_intro_sum) = 0) \/ exists ge_signed_half_scalar_intro_sumleft. (((b) = 2 * ge_signed_half_scalar_intro_sumleft + 1 /\ (dsa_ap_scalar_intro_sum) = 0) /\ (dsa_an_scalar_intro_sum) = S ge_signed_half_scalar_intro_sumleft))) /\ ((((((c) = 2 * (dsa_bp_scalar_intro_sum) /\ (dsa_bn_scalar_intro_sum) = 0) \/ exists ge_signed_half_scalar_intro_sumright. (((c) = 2 * ge_signed_half_scalar_intro_sumright + 1 /\ (dsa_bp_scalar_intro_sum) = 0) /\ (dsa_bn_scalar_intro_sum) = S ge_signed_half_scalar_intro_sumright))) /\ ((((((bc) = 2 * (dsa_cp_scalar_intro_sum) /\ (dsa_cn_scalar_intro_sum) = 0) \/ exists ge_signed_half_scalar_intro_sumoutput. (((bc) = 2 * ge_signed_half_scalar_intro_sumoutput + 1 /\ (dsa_cp_scalar_intro_sum) = 0) /\ (dsa_cn_scalar_intro_sum) = S ge_signed_half_scalar_intro_sumoutput))) /\ ((dsa_ap_scalar_intro_sum + dsa_bp_scalar_intro_sum) + dsa_cn_scalar_intro_sum = (dsa_an_scalar_intro_sum + dsa_bn_scalar_intro_sum) + dsa_cp_scalar_intro_sum))))))) -> (exists sto_ap_scalar_intro_left sto_an_scalar_intro_left sto_bp_scalar_intro_left sto_bn_scalar_intro_left sto_cp_scalar_intro_left sto_cn_scalar_intro_left. (((((a) = 2 * (sto_ap_scalar_intro_left) /\ (sto_an_scalar_intro_left) = 0) \/ exists ge_signed_half_scalar_intro_leftleft. (((a) = 2 * ge_signed_half_scalar_intro_leftleft + 1 /\ (sto_ap_scalar_intro_left) = 0) /\ (sto_an_scalar_intro_left) = S ge_signed_half_scalar_intro_leftleft))) /\ ((((((b) = 2 * (sto_bp_scalar_intro_left) /\ (sto_bn_scalar_intro_left) = 0) \/ exists ge_signed_half_scalar_intro_leftright. (((b) = 2 * ge_signed_half_scalar_intro_leftright + 1 /\ (sto_bp_scalar_intro_left) = 0) /\ (sto_bn_scalar_intro_left) = S ge_signed_half_scalar_intro_leftright))) /\ ((((((ab) = 2 * (sto_cp_scalar_intro_left) /\ (sto_cn_scalar_intro_left) = 0) \/ exists ge_signed_half_scalar_intro_leftoutput. (((ab) = 2 * ge_signed_half_scalar_intro_leftoutput + 1 /\ (sto_cp_scalar_intro_left) = 0) /\ (sto_cn_scalar_intro_left) = S ge_signed_half_scalar_intro_leftoutput))) /\ ((sto_ap_scalar_intro_left * sto_bp_scalar_intro_left + sto_an_scalar_intro_left * sto_bn_scalar_intro_left) + sto_cn_scalar_intro_left = (sto_ap_scalar_intro_left * sto_bn_scalar_intro_left + sto_an_scalar_intro_left * sto_bp_scalar_intro_left) + sto_cp_scalar_intro_left))))))) -> (exists sto_ap_scalar_intro_right sto_an_scalar_intro_right sto_bp_scalar_intro_right sto_bn_scalar_intro_right sto_cp_scalar_intro_right sto_cn_scalar_intro_right. (((((a) = 2 * (sto_ap_scalar_intro_right) /\ (sto_an_scalar_intro_right) = 0) \/ exists ge_signed_half_scalar_intro_rightleft. (((a) = 2 * ge_signed_half_scalar_intro_rightleft + 1 /\ (sto_ap_scalar_intro_right) = 0) /\ (sto_an_scalar_intro_right) = S ge_signed_half_scalar_intro_rightleft))) /\ ((((((c) = 2 * (sto_bp_scalar_intro_right) /\ (sto_bn_scalar_intro_right) = 0) \/ exists ge_signed_half_scalar_intro_rightright. (((c) = 2 * ge_signed_half_scalar_intro_rightright + 1 /\ (sto_bp_scalar_intro_right) = 0) /\ (sto_bn_scalar_intro_right) = S ge_signed_half_scalar_intro_rightright))) /\ ((((((ac) = 2 * (sto_cp_scalar_intro_right) /\ (sto_cn_scalar_intro_right) = 0) \/ exists ge_signed_half_scalar_intro_rightoutput. (((ac) = 2 * ge_signed_half_scalar_intro_rightoutput + 1 /\ (sto_cp_scalar_intro_right) = 0) /\ (sto_cn_scalar_intro_right) = S ge_signed_half_scalar_intro_rightoutput))) /\ ((sto_ap_scalar_intro_right * sto_bp_scalar_intro_right + sto_an_scalar_intro_right * sto_bn_scalar_intro_right) + sto_cn_scalar_intro_right = (sto_ap_scalar_intro_right * sto_bn_scalar_intro_right + sto_an_scalar_intro_right * sto_bp_scalar_intro_right) + sto_cp_scalar_intro_right))))))) -> (exists dsa_ap_scalar_intro_result dsa_an_scalar_intro_result dsa_bp_scalar_intro_result dsa_bn_scalar_intro_result dsa_cp_scalar_intro_result dsa_cn_scalar_intro_result. (((((ab) = 2 * (dsa_ap_scalar_intro_result) /\ (dsa_an_scalar_intro_result) = 0) \/ exists ge_signed_half_scalar_intro_resultleft. (((ab) = 2 * ge_signed_half_scalar_intro_resultleft + 1 /\ (dsa_ap_scalar_intro_result) = 0) /\ (dsa_an_scalar_intro_result) = S ge_signed_half_scalar_intro_resultleft))) /\ ((((((ac) = 2 * (dsa_bp_scalar_intro_result) /\ (dsa_bn_scalar_intro_result) = 0) \/ exists ge_signed_half_scalar_intro_resultright. (((ac) = 2 * ge_signed_half_scalar_intro_resultright + 1 /\ (dsa_bp_scalar_intro_result) = 0) /\ (dsa_bn_scalar_intro_result) = S ge_signed_half_scalar_intro_resultright))) /\ ((((((out) = 2 * (dsa_cp_scalar_intro_result) /\ (dsa_cn_scalar_intro_result) = 0) \/ exists ge_signed_half_scalar_intro_resultoutput. (((out) = 2 * ge_signed_half_scalar_intro_resultoutput + 1 /\ (dsa_cp_scalar_intro_result) = 0) /\ (dsa_cn_scalar_intro_result) = S ge_signed_half_scalar_intro_resultoutput))) /\ ((dsa_ap_scalar_intro_result + dsa_bp_scalar_intro_result) + dsa_cn_scalar_intro_result = (dsa_an_scalar_intro_result + dsa_bn_scalar_intro_result) + dsa_cp_scalar_intro_result))))))) -> (exists sto_ap_scalar_intro_target sto_an_scalar_intro_target sto_bp_scalar_intro_target sto_bn_scalar_intro_target sto_cp_scalar_intro_target sto_cn_scalar_intro_target. (((((a) = 2 * (sto_ap_scalar_intro_target) /\ (sto_an_scalar_intro_target) = 0) \/ exists ge_signed_half_scalar_intro_targetleft. (((a) = 2 * ge_signed_half_scalar_intro_targetleft + 1 /\ (sto_ap_scalar_intro_target) = 0) /\ (sto_an_scalar_intro_target) = S ge_signed_half_scalar_intro_targetleft))) /\ ((((((bc) = 2 * (sto_bp_scalar_intro_target) /\ (sto_bn_scalar_intro_target) = 0) \/ exists ge_signed_half_scalar_intro_targetright. (((bc) = 2 * ge_signed_half_scalar_intro_targetright + 1 /\ (sto_bp_scalar_intro_target) = 0) /\ (sto_bn_scalar_intro_target) = S ge_signed_half_scalar_intro_targetright))) /\ ((((((out) = 2 * (sto_cp_scalar_intro_target) /\ (sto_cn_scalar_intro_target) = 0) \/ exists ge_signed_half_scalar_intro_targetoutput. (((out) = 2 * ge_signed_half_scalar_intro_targetoutput + 1 /\ (sto_cp_scalar_intro_target) = 0) /\ (sto_cn_scalar_intro_target) = S ge_signed_half_scalar_intro_targetoutput))) /\ ((sto_ap_scalar_intro_target * sto_bp_scalar_intro_target + sto_an_scalar_intro_target * sto_bn_scalar_intro_target) + sto_cn_scalar_intro_target = (sto_ap_scalar_intro_target * sto_bn_scalar_intro_target + sto_an_scalar_intro_target * sto_bp_scalar_intro_target) + sto_cp_scalar_intro_target)))))))

Complete tactic proof in conservative notation

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

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

01Fix variables and assumptionsL1–10

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 bc
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro out
  8. L8
    intro hbc
  9. L9
    intro hab
  10. L10
    intro hac
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hout
03Establish hwL12–15

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

  1. L12
    have hw : ∃ w. SignedMul(a,bc,w)Definitions: SignedMul(a,bc,w)Original native command in the exact edition
  2. L13
    specialize signed_mul_total (a)
  3. L14
    specialize signed_mul_total (bc)
  4. L15
    apply signed_mul_total
04Separate the logical casesL16–16

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

  1. L16
    cases hw
05Establish heqL17–26

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

  1. L17
    have heq : x = out
  2. L18
    specialize signed_add_functional (ab)
  3. L19
    specialize signed_add_functional (ac)
  4. L20
    specialize signed_add_functional (x)
  5. L21
    specialize signed_add_functional (out)
  6. L22
    apply signed_add_functional
  7. L23
    specialize signed_mul_left_distributive (a)
  8. L24
    specialize signed_mul_left_distributive (b)
  9. L25
    specialize signed_mul_left_distributive (c)
  10. L26
    specialize signed_mul_left_distributive (bc)
06Use earlier factsL27–35

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

  1. L27
    specialize signed_mul_left_distributive (ab)
  2. L28
    specialize signed_mul_left_distributive (ac)
  3. L29
    specialize signed_mul_left_distributive (x)
  4. L30
    apply signed_mul_left_distributive
  5. L31
    exact hbc
  6. L32
    exact hab
  7. L33
    exact hac
  8. L34
    exact hw_witness
  9. L35
    exact hout
07Calculate and transport equalitiesL36–37

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

  1. L36
    rewrite heq at hw_witness
  2. L37
    rewrite heq at hw_witness
08Use earlier factsL38–38

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

  1. L38
    exact hw_witness

Library-wide reading audit

Original defined command ledger · 38 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro bc
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro out
  8. 0008intro hbc
  9. 0009intro hab
  10. 0010intro hac
  11. 0011intro hout
  12. 0012have hw : ∃ w. SignedMul(a,bc,w)
  13. 0013specialize signed_mul_total (a)
  14. 0014specialize signed_mul_total (bc)
  15. 0015apply signed_mul_total
  16. 0016cases hw
  17. 0017have heq : x = out
  18. 0018specialize signed_add_functional (ab)
  19. 0019specialize signed_add_functional (ac)
  20. 0020specialize signed_add_functional (x)
  21. 0021specialize signed_add_functional (out)
  22. 0022apply signed_add_functional
  23. 0023specialize signed_mul_left_distributive (a)
  24. 0024specialize signed_mul_left_distributive (b)
  25. 0025specialize signed_mul_left_distributive (c)
  26. 0026specialize signed_mul_left_distributive (bc)
  27. 0027specialize signed_mul_left_distributive (ab)
  28. 0028specialize signed_mul_left_distributive (ac)
  29. 0029specialize signed_mul_left_distributive (x)
  30. 0030apply signed_mul_left_distributive
  31. 0031exact hbc
  32. 0032exact hab
  33. 0033exact hac
  34. 0034exact hw_witness
  35. 0035exact hout
  36. 0036rewrite heq at hw_witness
  37. 0037rewrite heq at hw_witness
  38. 0038exact hw_witness