GI004A

gaussian_signed_add_to_balance

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

Alpha v34 checked-use · first admitted v28 · 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. Exact original first-admission records.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ∀ cc. ∀ p. ∀ n. ∀ q. ∀ m. SignedBalance(ac,p,n) → SignedBalance(bc,q,m) → SignedAdd(ac,bc,cc) → SignedBalance(cc,p + q,n + m)

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

Definition DAG

SignedBalance(z,p,n) · 4SignedAdd(a,b,c) · 1

Actual proof prerequisites

signed_balance_total · checked external prerequisitesigned_add_functional · checked external prerequisitegaussian_signed_add_of_balances
Original expanded first-order 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)))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
gaussian signed add of balances
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(output,p + q,n + m)Original native command in the exact edition
  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 defined 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 : ∃ output. SignedBalance(output,p + q,n + m)
  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