WS0025

signed_weighted_scalar_commute

Construct the reordered product and identify its canonical value by signed multiplication associativity, commutativity and functionality.

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. ∀ ab. ∀ cb. ∀ out. SignedMul(a,b,ab) → SignedMul(c,b,cb) → SignedMul(c,ab,out) → SignedMul(a,cb,out)

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

Definition DAG

SignedMul(a,b,c) · 5

Actual proof prerequisites

signed_mul_total · checked external prerequisitesigned_mul_functional · checked external prerequisitesigned_mul_associative · checked external prerequisitesigned_mul_commutative · checked external prerequisite
Original expanded first-order statement 
forall a b c ab cb out. (exists sto_ap_weighted_commute_first sto_an_weighted_commute_first sto_bp_weighted_commute_first sto_bn_weighted_commute_first sto_cp_weighted_commute_first sto_cn_weighted_commute_first. (((((a) = 2 * (sto_ap_weighted_commute_first) /\ (sto_an_weighted_commute_first) = 0) \/ exists ge_signed_half_weighted_commute_firstleft. (((a) = 2 * ge_signed_half_weighted_commute_firstleft + 1 /\ (sto_ap_weighted_commute_first) = 0) /\ (sto_an_weighted_commute_first) = S ge_signed_half_weighted_commute_firstleft))) /\ ((((((b) = 2 * (sto_bp_weighted_commute_first) /\ (sto_bn_weighted_commute_first) = 0) \/ exists ge_signed_half_weighted_commute_firstright. (((b) = 2 * ge_signed_half_weighted_commute_firstright + 1 /\ (sto_bp_weighted_commute_first) = 0) /\ (sto_bn_weighted_commute_first) = S ge_signed_half_weighted_commute_firstright))) /\ ((((((ab) = 2 * (sto_cp_weighted_commute_first) /\ (sto_cn_weighted_commute_first) = 0) \/ exists ge_signed_half_weighted_commute_firstoutput. (((ab) = 2 * ge_signed_half_weighted_commute_firstoutput + 1 /\ (sto_cp_weighted_commute_first) = 0) /\ (sto_cn_weighted_commute_first) = S ge_signed_half_weighted_commute_firstoutput))) /\ ((sto_ap_weighted_commute_first * sto_bp_weighted_commute_first + sto_an_weighted_commute_first * sto_bn_weighted_commute_first) + sto_cn_weighted_commute_first = (sto_ap_weighted_commute_first * sto_bn_weighted_commute_first + sto_an_weighted_commute_first * sto_bp_weighted_commute_first) + sto_cp_weighted_commute_first))))))) -> (exists sto_ap_weighted_commute_second sto_an_weighted_commute_second sto_bp_weighted_commute_second sto_bn_weighted_commute_second sto_cp_weighted_commute_second sto_cn_weighted_commute_second. (((((c) = 2 * (sto_ap_weighted_commute_second) /\ (sto_an_weighted_commute_second) = 0) \/ exists ge_signed_half_weighted_commute_secondleft. (((c) = 2 * ge_signed_half_weighted_commute_secondleft + 1 /\ (sto_ap_weighted_commute_second) = 0) /\ (sto_an_weighted_commute_second) = S ge_signed_half_weighted_commute_secondleft))) /\ ((((((b) = 2 * (sto_bp_weighted_commute_second) /\ (sto_bn_weighted_commute_second) = 0) \/ exists ge_signed_half_weighted_commute_secondright. (((b) = 2 * ge_signed_half_weighted_commute_secondright + 1 /\ (sto_bp_weighted_commute_second) = 0) /\ (sto_bn_weighted_commute_second) = S ge_signed_half_weighted_commute_secondright))) /\ ((((((cb) = 2 * (sto_cp_weighted_commute_second) /\ (sto_cn_weighted_commute_second) = 0) \/ exists ge_signed_half_weighted_commute_secondoutput. (((cb) = 2 * ge_signed_half_weighted_commute_secondoutput + 1 /\ (sto_cp_weighted_commute_second) = 0) /\ (sto_cn_weighted_commute_second) = S ge_signed_half_weighted_commute_secondoutput))) /\ ((sto_ap_weighted_commute_second * sto_bp_weighted_commute_second + sto_an_weighted_commute_second * sto_bn_weighted_commute_second) + sto_cn_weighted_commute_second = (sto_ap_weighted_commute_second * sto_bn_weighted_commute_second + sto_an_weighted_commute_second * sto_bp_weighted_commute_second) + sto_cp_weighted_commute_second))))))) -> (exists sto_ap_weighted_commute_output sto_an_weighted_commute_output sto_bp_weighted_commute_output sto_bn_weighted_commute_output sto_cp_weighted_commute_output sto_cn_weighted_commute_output. (((((c) = 2 * (sto_ap_weighted_commute_output) /\ (sto_an_weighted_commute_output) = 0) \/ exists ge_signed_half_weighted_commute_outputleft. (((c) = 2 * ge_signed_half_weighted_commute_outputleft + 1 /\ (sto_ap_weighted_commute_output) = 0) /\ (sto_an_weighted_commute_output) = S ge_signed_half_weighted_commute_outputleft))) /\ ((((((ab) = 2 * (sto_bp_weighted_commute_output) /\ (sto_bn_weighted_commute_output) = 0) \/ exists ge_signed_half_weighted_commute_outputright. (((ab) = 2 * ge_signed_half_weighted_commute_outputright + 1 /\ (sto_bp_weighted_commute_output) = 0) /\ (sto_bn_weighted_commute_output) = S ge_signed_half_weighted_commute_outputright))) /\ ((((((out) = 2 * (sto_cp_weighted_commute_output) /\ (sto_cn_weighted_commute_output) = 0) \/ exists ge_signed_half_weighted_commute_outputoutput. (((out) = 2 * ge_signed_half_weighted_commute_outputoutput + 1 /\ (sto_cp_weighted_commute_output) = 0) /\ (sto_cn_weighted_commute_output) = S ge_signed_half_weighted_commute_outputoutput))) /\ ((sto_ap_weighted_commute_output * sto_bp_weighted_commute_output + sto_an_weighted_commute_output * sto_bn_weighted_commute_output) + sto_cn_weighted_commute_output = (sto_ap_weighted_commute_output * sto_bn_weighted_commute_output + sto_an_weighted_commute_output * sto_bp_weighted_commute_output) + sto_cp_weighted_commute_output))))))) -> (exists sto_ap_weighted_commute_target sto_an_weighted_commute_target sto_bp_weighted_commute_target sto_bn_weighted_commute_target sto_cp_weighted_commute_target sto_cn_weighted_commute_target. (((((a) = 2 * (sto_ap_weighted_commute_target) /\ (sto_an_weighted_commute_target) = 0) \/ exists ge_signed_half_weighted_commute_targetleft. (((a) = 2 * ge_signed_half_weighted_commute_targetleft + 1 /\ (sto_ap_weighted_commute_target) = 0) /\ (sto_an_weighted_commute_target) = S ge_signed_half_weighted_commute_targetleft))) /\ ((((((cb) = 2 * (sto_bp_weighted_commute_target) /\ (sto_bn_weighted_commute_target) = 0) \/ exists ge_signed_half_weighted_commute_targetright. (((cb) = 2 * ge_signed_half_weighted_commute_targetright + 1 /\ (sto_bp_weighted_commute_target) = 0) /\ (sto_bn_weighted_commute_target) = S ge_signed_half_weighted_commute_targetright))) /\ ((((((out) = 2 * (sto_cp_weighted_commute_target) /\ (sto_cn_weighted_commute_target) = 0) \/ exists ge_signed_half_weighted_commute_targetoutput. (((out) = 2 * ge_signed_half_weighted_commute_targetoutput + 1 /\ (sto_cp_weighted_commute_target) = 0) /\ (sto_cn_weighted_commute_target) = S ge_signed_half_weighted_commute_targetoutput))) /\ ((sto_ap_weighted_commute_target * sto_bp_weighted_commute_target + sto_an_weighted_commute_target * sto_bn_weighted_commute_target) + sto_cn_weighted_commute_target = (sto_ap_weighted_commute_target * sto_bn_weighted_commute_target + sto_an_weighted_commute_target * sto_bp_weighted_commute_target) + sto_cp_weighted_commute_target)))))))

Complete tactic proof in conservative notation

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

42 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–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 cb
  6. L6
    intro out
  7. L7
    intro hab
  8. L8
    intro hcb
  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 mul total.

  1. L10
    have hw : ∃ w. SignedMul(a,cb,w)Definitions: SignedMul(a,cb,w)Original native command in the exact edition
  2. L11
    specialize signed_mul_total (a)
  3. L12
    specialize signed_mul_total (cb)
  4. L13
    apply signed_mul_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 mul functional.

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

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

  1. L25
    specialize signed_mul_associative (ab)
  2. L26
    specialize signed_mul_associative (x)
  3. L27
    apply signed_mul_associative
  4. L28
    exact hcb
  5. L29
    specialize signed_mul_commutative (a)
  6. L30
    specialize signed_mul_commutative (cb)
  7. L31
    specialize signed_mul_commutative (x)
  8. L32
    apply signed_mul_commutative
  9. L33
    exact hw_witness
  10. L34
    specialize signed_mul_commutative (a)
06Use earlier factsL35–39

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

  1. L35
    specialize signed_mul_commutative (b)
  2. L36
    specialize signed_mul_commutative (ab)
  3. L37
    apply signed_mul_commutative
  4. L38
    exact hab
  5. L39
    exact hout
07Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite heq at hw_witness
  2. L41
    rewrite heq at hw_witness
08Use earlier factsL42–42

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

  1. L42
    exact hw_witness

Library-wide reading audit

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