GI004C

gaussian_signed_mul_to_balance

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

The unchanged historic signed-mul graph has the exact arbitrary-representative contribution balance; this proves the converse rather than an unproved notation alias.

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 original first-admission records.

Exact expanded first-order arithmetic statement

forall ac bc cc p n q m. (exists ge_balance_positive_bridge_elim_first_mul ge_balance_negative_bridge_elim_first_mul. (((((ac) = 2 * (ge_balance_positive_bridge_elim_first_mul) /\ (ge_balance_negative_bridge_elim_first_mul) = 0) \/ exists ge_signed_half_bridge_elim_first_muldecode. (((ac) = 2 * ge_signed_half_bridge_elim_first_muldecode + 1 /\ (ge_balance_positive_bridge_elim_first_mul) = 0) /\ (ge_balance_negative_bridge_elim_first_mul) = S ge_signed_half_bridge_elim_first_muldecode))) /\ ((p) + ge_balance_negative_bridge_elim_first_mul = (n) + ge_balance_positive_bridge_elim_first_mul))) -> (exists ge_balance_positive_bridge_elim_second_mul ge_balance_negative_bridge_elim_second_mul. (((((bc) = 2 * (ge_balance_positive_bridge_elim_second_mul) /\ (ge_balance_negative_bridge_elim_second_mul) = 0) \/ exists ge_signed_half_bridge_elim_second_muldecode. (((bc) = 2 * ge_signed_half_bridge_elim_second_muldecode + 1 /\ (ge_balance_positive_bridge_elim_second_mul) = 0) /\ (ge_balance_negative_bridge_elim_second_mul) = S ge_signed_half_bridge_elim_second_muldecode))) /\ ((q) + ge_balance_negative_bridge_elim_second_mul = (m) + ge_balance_positive_bridge_elim_second_mul))) -> (exists sm_lp_gaussian_bridge_elim_mul sm_ln_gaussian_bridge_elim_mul sm_rp_gaussian_bridge_elim_mul sm_rn_gaussian_bridge_elim_mul sm_op_gaussian_bridge_elim_mul sm_on_gaussian_bridge_elim_mul. (((ac = 2 * sm_lp_gaussian_bridge_elim_mul /\ sm_ln_gaussian_bridge_elim_mul = 0) \/ exists sd_half_gaussian_bridge_elim_mul_left. ((ac = 2 * sd_half_gaussian_bridge_elim_mul_left + 1 /\ sm_lp_gaussian_bridge_elim_mul = 0) /\ sm_ln_gaussian_bridge_elim_mul = S sd_half_gaussian_bridge_elim_mul_left)) /\ (((bc = 2 * sm_rp_gaussian_bridge_elim_mul /\ sm_rn_gaussian_bridge_elim_mul = 0) \/ exists sd_half_gaussian_bridge_elim_mul_right. ((bc = 2 * sd_half_gaussian_bridge_elim_mul_right + 1 /\ sm_rp_gaussian_bridge_elim_mul = 0) /\ sm_rn_gaussian_bridge_elim_mul = S sd_half_gaussian_bridge_elim_mul_right)) /\ (((cc = 2 * sm_op_gaussian_bridge_elim_mul /\ sm_on_gaussian_bridge_elim_mul = 0) \/ exists sd_half_gaussian_bridge_elim_mul_output. ((cc = 2 * sd_half_gaussian_bridge_elim_mul_output + 1 /\ sm_op_gaussian_bridge_elim_mul = 0) /\ sm_on_gaussian_bridge_elim_mul = S sd_half_gaussian_bridge_elim_mul_output)) /\ (sm_lp_gaussian_bridge_elim_mul * sm_rp_gaussian_bridge_elim_mul + sm_ln_gaussian_bridge_elim_mul * sm_rn_gaussian_bridge_elim_mul) + sm_on_gaussian_bridge_elim_mul = (sm_lp_gaussian_bridge_elim_mul * sm_rn_gaussian_bridge_elim_mul + sm_ln_gaussian_bridge_elim_mul * sm_rp_gaussian_bridge_elim_mul) + sm_op_gaussian_bridge_elim_mul)))) -> (exists ge_balance_positive_signed_bridge_elimination_mul ge_balance_negative_signed_bridge_elimination_mul. (((((cc) = 2 * (ge_balance_positive_signed_bridge_elimination_mul) /\ (ge_balance_negative_signed_bridge_elimination_mul) = 0) \/ exists ge_signed_half_signed_bridge_elimination_muldecode. (((cc) = 2 * ge_signed_half_signed_bridge_elimination_muldecode + 1 /\ (ge_balance_positive_signed_bridge_elimination_mul) = 0) /\ (ge_balance_negative_signed_bridge_elimination_mul) = S ge_signed_half_signed_bridge_elimination_muldecode))) /\ ((((((p) * (q))) + (((n) * (m))))) + ge_balance_negative_signed_bridge_elimination_mul = (((((p) * (m))) + (((n) * (q))))) + ge_balance_positive_signed_bridge_elimination_mul)))

Constructive proof overview

Generated structural guide

The unchanged historic signed-mul graph has the exact arbitrary-representative contribution balance; this proves the converse rather than an unproved notation alias.

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

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

Proof neighborhood

Direct dependencies

signed_balance_total Alpha theorem; checked-use authorized signed_mul_functional Alpha theorem; checked-use authorized GI004B gaussian_signed_mul_of_balances

Direct dependents

none

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

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

Named ingredients (1)
gaussian signed mul of balances

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–10

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro cc
  4. L4
    intro p
  5. L5
    intro n
  6. L6
    intro q
  7. L7
    intro m
  8. L8
    intro hfirst
  9. L9
    intro hsecond
  10. L10
    intro hoperation
02Establish houtputL11–14

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

  1. L11
    have houtput : ∃ output. SignedBalance(output,p · q + n · m,p · m + n · q)Definitions: SignedBalance
  2. L12
    specialize signed_balance_total ((((p) * (q))) + (((n) * (m))))
  3. L13
    specialize signed_balance_total ((((p) * (m))) + (((n) * (q))))
  4. L14
    apply signed_balance_total
03Separate the logical casesL15–15

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

  1. L15
    cases houtput
04Establish hequalL16–25

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

  1. L16
    have hequal : cc = x
  2. L17
    specialize signed_mul_functional ac
  3. L18
    specialize signed_mul_functional bc
  4. L19
    specialize signed_mul_functional cc
  5. L20
    specialize signed_mul_functional x
  6. L21
    apply signed_mul_functional
  7. L22
    exact hoperation
  8. L23
    specialize gaussian_signed_mul_of_balances ac
  9. L24
    specialize gaussian_signed_mul_of_balances bc
  10. L25
    specialize gaussian_signed_mul_of_balances x
05Use earlier factsL26–33

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

  1. L26
    specialize gaussian_signed_mul_of_balances p
  2. L27
    specialize gaussian_signed_mul_of_balances n
  3. L28
    specialize gaussian_signed_mul_of_balances q
  4. L29
    specialize gaussian_signed_mul_of_balances m
  5. L30
    apply gaussian_signed_mul_of_balances
  6. L31
    exact hfirst
  7. L32
    exact hsecond
  8. L33
    exact houtput_witness
06Calculate and transport equalitiesL34–35

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

  1. L34
    rewrite hequal
  2. L35
    rewrite hequal
07Use earlier factsL36–36

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

  1. L36
    exact houtput_witness

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro p
  5. 0005intro n
  6. 0006intro q
  7. 0007intro m
  8. 0008intro hfirst
  9. 0009intro hsecond
  10. 0010intro hoperation
  11. 0011have houtput : exists output. (exists ge_balance_positive_signed_bridge_construct_mul ge_balance_negative_signed_bridge_construct_mul. (((((output) = 2 * (ge_balance_positive_signed_bridge_construct_mul) /\ (ge_balance_negative_signed_bridge_construct_mul) = 0) \/ exists ge_signed_half_signed_bridge_construct_muldecode. (((output) = 2 * ge_signed_half_signed_bridge_construct_muldecode + 1 /\ (ge_balance_positive_signed_bridge_construct_mul) = 0) /\ (ge_balance_negative_signed_bridge_construct_mul) = S ge_signed_half_signed_bridge_construct_muldecode))) /\ ((((((p) * (q))) + (((n) * (m))))) + ge_balance_negative_signed_bridge_construct_mul = (((((p) * (m))) + (((n) * (q))))) + ge_balance_positive_signed_bridge_construct_mul)))
  12. 0012specialize signed_balance_total ((((p) * (q))) + (((n) * (m))))
  13. 0013specialize signed_balance_total ((((p) * (m))) + (((n) * (q))))
  14. 0014apply signed_balance_total
  15. 0015cases houtput
  16. 0016have hequal : cc = x
  17. 0017specialize signed_mul_functional ac
  18. 0018specialize signed_mul_functional bc
  19. 0019specialize signed_mul_functional cc
  20. 0020specialize signed_mul_functional x
  21. 0021apply signed_mul_functional
  22. 0022exact hoperation
  23. 0023specialize gaussian_signed_mul_of_balances ac
  24. 0024specialize gaussian_signed_mul_of_balances bc
  25. 0025specialize gaussian_signed_mul_of_balances x
  26. 0026specialize gaussian_signed_mul_of_balances p
  27. 0027specialize gaussian_signed_mul_of_balances n
  28. 0028specialize gaussian_signed_mul_of_balances q
  29. 0029specialize gaussian_signed_mul_of_balances m
  30. 0030apply gaussian_signed_mul_of_balances
  31. 0031exact hfirst
  32. 0032exact hsecond
  33. 0033exact houtput_witness
  34. 0034rewrite hequal
  35. 0035rewrite hequal
  36. 0036exact houtput_witness