GI004A

gaussian_signed_add_to_balance

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

The unchanged historic signed-add 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_add ge_balance_negative_bridge_elim_first_add. (((((ac) = 2 * (ge_balance_positive_bridge_elim_first_add) /\ (ge_balance_negative_bridge_elim_first_add) = 0) \/ exists ge_signed_half_bridge_elim_first_adddecode. (((ac) = 2 * ge_signed_half_bridge_elim_first_adddecode + 1 /\ (ge_balance_positive_bridge_elim_first_add) = 0) /\ (ge_balance_negative_bridge_elim_first_add) = S ge_signed_half_bridge_elim_first_adddecode))) /\ ((p) + ge_balance_negative_bridge_elim_first_add = (n) + ge_balance_positive_bridge_elim_first_add))) -> (exists ge_balance_positive_bridge_elim_second_add ge_balance_negative_bridge_elim_second_add. (((((bc) = 2 * (ge_balance_positive_bridge_elim_second_add) /\ (ge_balance_negative_bridge_elim_second_add) = 0) \/ exists ge_signed_half_bridge_elim_second_adddecode. (((bc) = 2 * ge_signed_half_bridge_elim_second_adddecode + 1 /\ (ge_balance_positive_bridge_elim_second_add) = 0) /\ (ge_balance_negative_bridge_elim_second_add) = S ge_signed_half_bridge_elim_second_adddecode))) /\ ((q) + ge_balance_negative_bridge_elim_second_add = (m) + ge_balance_positive_bridge_elim_second_add))) -> (exists sa_lp_gaussian_bridge_elim_add sa_ln_gaussian_bridge_elim_add sa_rp_gaussian_bridge_elim_add sa_rn_gaussian_bridge_elim_add sa_op_gaussian_bridge_elim_add sa_on_gaussian_bridge_elim_add. (((ac = 2 * sa_lp_gaussian_bridge_elim_add /\ sa_ln_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_left. ((ac = 2 * sd_half_gaussian_bridge_elim_add_left + 1 /\ sa_lp_gaussian_bridge_elim_add = 0) /\ sa_ln_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_left)) /\ (((bc = 2 * sa_rp_gaussian_bridge_elim_add /\ sa_rn_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_right. ((bc = 2 * sd_half_gaussian_bridge_elim_add_right + 1 /\ sa_rp_gaussian_bridge_elim_add = 0) /\ sa_rn_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_right)) /\ (((cc = 2 * sa_op_gaussian_bridge_elim_add /\ sa_on_gaussian_bridge_elim_add = 0) \/ exists sd_half_gaussian_bridge_elim_add_output. ((cc = 2 * sd_half_gaussian_bridge_elim_add_output + 1 /\ sa_op_gaussian_bridge_elim_add = 0) /\ sa_on_gaussian_bridge_elim_add = S sd_half_gaussian_bridge_elim_add_output)) /\ (sa_lp_gaussian_bridge_elim_add + sa_rp_gaussian_bridge_elim_add) + sa_on_gaussian_bridge_elim_add = (sa_ln_gaussian_bridge_elim_add + sa_rn_gaussian_bridge_elim_add) + sa_op_gaussian_bridge_elim_add)))) -> (exists ge_balance_positive_signed_bridge_elimination_add ge_balance_negative_signed_bridge_elimination_add. (((((cc) = 2 * (ge_balance_positive_signed_bridge_elimination_add) /\ (ge_balance_negative_signed_bridge_elimination_add) = 0) \/ exists ge_signed_half_signed_bridge_elimination_adddecode. (((cc) = 2 * ge_signed_half_signed_bridge_elimination_adddecode + 1 /\ (ge_balance_positive_signed_bridge_elimination_add) = 0) /\ (ge_balance_negative_signed_bridge_elimination_add) = S ge_signed_half_signed_bridge_elimination_adddecode))) /\ ((((p) + (q))) + ge_balance_negative_signed_bridge_elimination_add = (((n) + (m))) + ge_balance_positive_signed_bridge_elimination_add)))

Constructive proof overview

Generated structural guide

The unchanged historic signed-add 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_add_functional Alpha theorem; checked-use authorized GI0049 gaussian_signed_add_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 add 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)Definitions: SignedBalance
  2. L12
    specialize signed_balance_total ((p) + (q))
  3. L13
    specialize signed_balance_total ((n) + (m))
  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 add functional.

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

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

  1. L26
    specialize gaussian_signed_add_of_balances p
  2. L27
    specialize gaussian_signed_add_of_balances n
  3. L28
    specialize gaussian_signed_add_of_balances q
  4. L29
    specialize gaussian_signed_add_of_balances m
  5. L30
    apply gaussian_signed_add_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_add ge_balance_negative_signed_bridge_construct_add. (((((output) = 2 * (ge_balance_positive_signed_bridge_construct_add) /\ (ge_balance_negative_signed_bridge_construct_add) = 0) \/ exists ge_signed_half_signed_bridge_construct_adddecode. (((output) = 2 * ge_signed_half_signed_bridge_construct_adddecode + 1 /\ (ge_balance_positive_signed_bridge_construct_add) = 0) /\ (ge_balance_negative_signed_bridge_construct_add) = S ge_signed_half_signed_bridge_construct_adddecode))) /\ ((((p) + (q))) + ge_balance_negative_signed_bridge_construct_add = (((n) + (m))) + ge_balance_positive_signed_bridge_construct_add)))
  12. 0012specialize signed_balance_total ((p) + (q))
  13. 0013specialize signed_balance_total ((n) + (m))
  14. 0014apply signed_balance_total
  15. 0015cases houtput
  16. 0016have hequal : cc = x
  17. 0017specialize signed_add_functional ac
  18. 0018specialize signed_add_functional bc
  19. 0019specialize signed_add_functional cc
  20. 0020specialize signed_add_functional x
  21. 0021apply signed_add_functional
  22. 0022exact hoperation
  23. 0023specialize gaussian_signed_add_of_balances ac
  24. 0024specialize gaussian_signed_add_of_balances bc
  25. 0025specialize gaussian_signed_add_of_balances x
  26. 0026specialize gaussian_signed_add_of_balances p
  27. 0027specialize gaussian_signed_add_of_balances n
  28. 0028specialize gaussian_signed_add_of_balances q
  29. 0029specialize gaussian_signed_add_of_balances m
  30. 0030apply gaussian_signed_add_of_balances
  31. 0031exact hfirst
  32. 0032exact hsecond
  33. 0033exact houtput_witness
  34. 0034rewrite hequal
  35. 0035rewrite hequal
  36. 0036exact houtput_witness