GI0049

gaussian_signed_add_of_balances

Actual arbitrary signed-pair add contribution balances construct the unchanged historic canonical signed-add graph.

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) → SignedBalance(cc,p + q,n + m) → SignedAdd(ac,bc,cc)

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

integer_span_pair_add_congruence · checked external prerequisitegaussian_signed_balance_integer_transportsigned_add_of_decoded_equation · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall ac bc cc p n q m. (exists ge_balance_positive_bridge_first_add ge_balance_negative_bridge_first_add. (((((ac) = 2 * (ge_balance_positive_bridge_first_add) /\ (ge_balance_negative_bridge_first_add) = 0) \/ exists ge_signed_half_bridge_first_adddecode. (((ac) = 2 * ge_signed_half_bridge_first_adddecode + 1 /\ (ge_balance_positive_bridge_first_add) = 0) /\ (ge_balance_negative_bridge_first_add) = S ge_signed_half_bridge_first_adddecode))) /\ ((p) + ge_balance_negative_bridge_first_add = (n) + ge_balance_positive_bridge_first_add))) -> (exists ge_balance_positive_bridge_second_add ge_balance_negative_bridge_second_add. (((((bc) = 2 * (ge_balance_positive_bridge_second_add) /\ (ge_balance_negative_bridge_second_add) = 0) \/ exists ge_signed_half_bridge_second_adddecode. (((bc) = 2 * ge_signed_half_bridge_second_adddecode + 1 /\ (ge_balance_positive_bridge_second_add) = 0) /\ (ge_balance_negative_bridge_second_add) = S ge_signed_half_bridge_second_adddecode))) /\ ((q) + ge_balance_negative_bridge_second_add = (m) + ge_balance_positive_bridge_second_add))) -> (exists ge_balance_positive_bridge_output_add ge_balance_negative_bridge_output_add. (((((cc) = 2 * (ge_balance_positive_bridge_output_add) /\ (ge_balance_negative_bridge_output_add) = 0) \/ exists ge_signed_half_bridge_output_adddecode. (((cc) = 2 * ge_signed_half_bridge_output_adddecode + 1 /\ (ge_balance_positive_bridge_output_add) = 0) /\ (ge_balance_negative_bridge_output_add) = S ge_signed_half_bridge_output_adddecode))) /\ ((((p) + (q))) + ge_balance_negative_bridge_output_add = (((n) + (m))) + ge_balance_positive_bridge_output_add))) -> (exists sa_lp_gaussian_bridge_add sa_ln_gaussian_bridge_add sa_rp_gaussian_bridge_add sa_rn_gaussian_bridge_add sa_op_gaussian_bridge_add sa_on_gaussian_bridge_add. (((ac = 2 * sa_lp_gaussian_bridge_add /\ sa_ln_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_left. ((ac = 2 * sd_half_gaussian_bridge_add_left + 1 /\ sa_lp_gaussian_bridge_add = 0) /\ sa_ln_gaussian_bridge_add = S sd_half_gaussian_bridge_add_left)) /\ (((bc = 2 * sa_rp_gaussian_bridge_add /\ sa_rn_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_right. ((bc = 2 * sd_half_gaussian_bridge_add_right + 1 /\ sa_rp_gaussian_bridge_add = 0) /\ sa_rn_gaussian_bridge_add = S sd_half_gaussian_bridge_add_right)) /\ (((cc = 2 * sa_op_gaussian_bridge_add /\ sa_on_gaussian_bridge_add = 0) \/ exists sd_half_gaussian_bridge_add_output. ((cc = 2 * sd_half_gaussian_bridge_add_output + 1 /\ sa_op_gaussian_bridge_add = 0) /\ sa_on_gaussian_bridge_add = S sd_half_gaussian_bridge_add_output)) /\ (sa_lp_gaussian_bridge_add + sa_rp_gaussian_bridge_add) + sa_on_gaussian_bridge_add = (sa_ln_gaussian_bridge_add + sa_rn_gaussian_bridge_add) + sa_op_gaussian_bridge_add))))

Complete tactic proof in conservative notation

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

58 script commands · 11 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 balance integer transport
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 houtput
02Separate the logical casesL11–16

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

  1. L11
    cases hfirst
  2. L12
    cases hfirst_witness
  3. L13
    cases hfirst_witness_witness
  4. L14
    cases hsecond
  5. L15
    cases hsecond_witness
  6. L16
    cases hsecond_witness_witness
03Establish hequalL17–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply integer span pair add congruence.

  1. L17
    have hequal : ((((p) + (q))) + (((x1) + (x3)))) = ((((x) + (x2))) + (((n) + (m))))
  2. L18
    specialize integer_span_pair_add_congruence p
  3. L19
    specialize integer_span_pair_add_congruence n
  4. L20
    specialize integer_span_pair_add_congruence q
  5. L21
    specialize integer_span_pair_add_congruence m
  6. L22
    specialize integer_span_pair_add_congruence x
  7. L23
    specialize integer_span_pair_add_congruence x1
  8. L24
    specialize integer_span_pair_add_congruence x2
  9. L25
    specialize integer_span_pair_add_congruence x3
  10. L26
    apply integer_span_pair_add_congruence
04Calculate and transport equalitiesL27–27

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

  1. L27
    trans n + x
05Use earlier factsL28–29

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

  1. L28
    exact hfirst_witness_witness_right
  2. L29
    apply add_comm
06Calculate and transport equalitiesL30–30

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

  1. L30
    trans m + x2
07Use earlier factsL31–32

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

  1. L31
    exact hsecond_witness_witness_right
  2. L32
    apply add_comm
08Establish hnormalizedL33–41

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

  1. L33
    have hnormalized : SignedBalance(cc,x + x2,x1 + x3)Definitions: SignedBalance(cc,x + x2,x1 + x3)Original native command in the exact edition
  2. L34
    specialize gaussian_signed_balance_integer_transport cc
  3. L35
    specialize gaussian_signed_balance_integer_transport ((p) + (q))
  4. L36
    specialize gaussian_signed_balance_integer_transport ((n) + (m))
  5. L37
    specialize gaussian_signed_balance_integer_transport ((x) + (x2))
  6. L38
    specialize gaussian_signed_balance_integer_transport ((x1) + (x3))
  7. L39
    apply gaussian_signed_balance_integer_transport
  8. L40
    exact hequal
  9. L41
    exact houtput
09Separate the logical casesL42–44

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

  1. L42
    cases hnormalized
  2. L43
    cases hnormalized_witness
  3. L44
    cases hnormalized_witness_witness
10Use earlier factsL45–54

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

  1. L45
    specialize signed_add_of_decoded_equation ac
  2. L46
    specialize signed_add_of_decoded_equation bc
  3. L47
    specialize signed_add_of_decoded_equation cc
  4. L48
    specialize signed_add_of_decoded_equation x
  5. L49
    specialize signed_add_of_decoded_equation x1
  6. L50
    specialize signed_add_of_decoded_equation x2
  7. L51
    specialize signed_add_of_decoded_equation x3
  8. L52
    specialize signed_add_of_decoded_equation x4
  9. L53
    specialize signed_add_of_decoded_equation x5
  10. L54
    apply signed_add_of_decoded_equation
11Use earlier factsL55–58

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

  1. L55
    exact hfirst_witness_witness_left
  2. L56
    exact hsecond_witness_witness_left
  3. L57
    exact hnormalized_witness_witness_left
  4. L58
    exact hnormalized_witness_witness_right

Library-wide reading audit

Original defined command ledger · 58 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 houtput
  11. 0011cases hfirst
  12. 0012cases hfirst_witness
  13. 0013cases hfirst_witness_witness
  14. 0014cases hsecond
  15. 0015cases hsecond_witness
  16. 0016cases hsecond_witness_witness
  17. 0017have hequal : ((((p) + (q))) + (((x1) + (x3)))) = ((((x) + (x2))) + (((n) + (m))))
  18. 0018specialize integer_span_pair_add_congruence p
  19. 0019specialize integer_span_pair_add_congruence n
  20. 0020specialize integer_span_pair_add_congruence q
  21. 0021specialize integer_span_pair_add_congruence m
  22. 0022specialize integer_span_pair_add_congruence x
  23. 0023specialize integer_span_pair_add_congruence x1
  24. 0024specialize integer_span_pair_add_congruence x2
  25. 0025specialize integer_span_pair_add_congruence x3
  26. 0026apply integer_span_pair_add_congruence
  27. 0027trans n + x
  28. 0028exact hfirst_witness_witness_right
  29. 0029apply add_comm
  30. 0030trans m + x2
  31. 0031exact hsecond_witness_witness_right
  32. 0032apply add_comm
  33. 0033have hnormalized : SignedBalance(cc,x + x2,x1 + x3)
  34. 0034specialize gaussian_signed_balance_integer_transport cc
  35. 0035specialize gaussian_signed_balance_integer_transport ((p) + (q))
  36. 0036specialize gaussian_signed_balance_integer_transport ((n) + (m))
  37. 0037specialize gaussian_signed_balance_integer_transport ((x) + (x2))
  38. 0038specialize gaussian_signed_balance_integer_transport ((x1) + (x3))
  39. 0039apply gaussian_signed_balance_integer_transport
  40. 0040exact hequal
  41. 0041exact houtput
  42. 0042cases hnormalized
  43. 0043cases hnormalized_witness
  44. 0044cases hnormalized_witness_witness
  45. 0045specialize signed_add_of_decoded_equation ac
  46. 0046specialize signed_add_of_decoded_equation bc
  47. 0047specialize signed_add_of_decoded_equation cc
  48. 0048specialize signed_add_of_decoded_equation x
  49. 0049specialize signed_add_of_decoded_equation x1
  50. 0050specialize signed_add_of_decoded_equation x2
  51. 0051specialize signed_add_of_decoded_equation x3
  52. 0052specialize signed_add_of_decoded_equation x4
  53. 0053specialize signed_add_of_decoded_equation x5
  54. 0054apply signed_add_of_decoded_equation
  55. 0055exact hfirst_witness_witness_left
  56. 0056exact hsecond_witness_witness_left
  57. 0057exact hnormalized_witness_witness_left
  58. 0058exact hnormalized_witness_witness_right