WS0025

signed_weighted_scalar_commute

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

signed_mul_total Alpha theorem; checked-use authorized signed_mul_functional Alpha theorem; checked-use authorized signed_mul_associative Alpha theorem; checked-use authorized signed_mul_commutative Alpha theorem; checked-use authorized

Direct dependents

WS0026 signed_table_weighted_scalar_commute

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

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.

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 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
  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 exact 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 : exists w. (exists sto_ap_scalar_commute_construct sto_an_scalar_commute_construct sto_bp_scalar_commute_construct sto_bn_scalar_commute_construct sto_cp_scalar_commute_construct sto_cn_scalar_commute_construct. (((((a) = 2 * (sto_ap_scalar_commute_construct) /\ (sto_an_scalar_commute_construct) = 0) \/ exists ge_signed_half_scalar_commute_constructleft. (((a) = 2 * ge_signed_half_scalar_commute_constructleft + 1 /\ (sto_ap_scalar_commute_construct) = 0) /\ (sto_an_scalar_commute_construct) = S ge_signed_half_scalar_commute_constructleft))) /\ ((((((cb) = 2 * (sto_bp_scalar_commute_construct) /\ (sto_bn_scalar_commute_construct) = 0) \/ exists ge_signed_half_scalar_commute_constructright. (((cb) = 2 * ge_signed_half_scalar_commute_constructright + 1 /\ (sto_bp_scalar_commute_construct) = 0) /\ (sto_bn_scalar_commute_construct) = S ge_signed_half_scalar_commute_constructright))) /\ ((((((w) = 2 * (sto_cp_scalar_commute_construct) /\ (sto_cn_scalar_commute_construct) = 0) \/ exists ge_signed_half_scalar_commute_constructoutput. (((w) = 2 * ge_signed_half_scalar_commute_constructoutput + 1 /\ (sto_cp_scalar_commute_construct) = 0) /\ (sto_cn_scalar_commute_construct) = S ge_signed_half_scalar_commute_constructoutput))) /\ ((sto_ap_scalar_commute_construct * sto_bp_scalar_commute_construct + sto_an_scalar_commute_construct * sto_bn_scalar_commute_construct) + sto_cn_scalar_commute_construct = (sto_ap_scalar_commute_construct * sto_bn_scalar_commute_construct + sto_an_scalar_commute_construct * sto_bp_scalar_commute_construct) + sto_cp_scalar_commute_construct)))))))
  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