GI0049

gaussian_signed_add_of_balances

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

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

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

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

integer_span_pair_add_congruence Alpha theorem; checked-use authorized GI003B gaussian_signed_balance_integer_transport signed_add_of_decoded_equation Alpha theorem; checked-use authorized add_comm Stable theorem; checked-use authorized

Direct dependents

GI004A gaussian_signed_add_to_balance

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

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.

Named ingredients (1)
gaussian signed balance integer transport

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 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
  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 exact 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 : exists ge_balance_positive_signed_bridge_normalized_add ge_balance_negative_signed_bridge_normalized_add. (((((cc) = 2 * (ge_balance_positive_signed_bridge_normalized_add) /\ (ge_balance_negative_signed_bridge_normalized_add) = 0) \/ exists ge_signed_half_signed_bridge_normalized_adddecode. (((cc) = 2 * ge_signed_half_signed_bridge_normalized_adddecode + 1 /\ (ge_balance_positive_signed_bridge_normalized_add) = 0) /\ (ge_balance_negative_signed_bridge_normalized_add) = S ge_signed_half_signed_bridge_normalized_adddecode))) /\ ((((x) + (x2))) + ge_balance_negative_signed_bridge_normalized_add = (((x1) + (x3))) + ge_balance_positive_signed_bridge_normalized_add))
  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