GI0053

gaussian_add_of_representations

Actual signed-coordinate add representatives construct the canonical Gaussian operation 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. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ZPairRep(ac,a,b,c,d) → ZPairRep(bc,e,f,g,h) → ZPairRep(cc,a + e,b + f,c + g,d + h) → ZPairAdd(ac,bc,cc)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 3ZPairAdd(a,b,c) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall ac bc cc a b c d e f g h. (exists ge_representation_real_code_add_intro_first ge_representation_imaginary_code_add_intro_first. (((ac) = ((ge_representation_real_code_add_intro_first) + (ge_representation_imaginary_code_add_intro_first)) * S ((ge_representation_real_code_add_intro_first) + (ge_representation_imaginary_code_add_intro_first)) + ((ge_representation_imaginary_code_add_intro_first) + (ge_representation_imaginary_code_add_intro_first))) /\ ((exists ge_balance_positive_add_intro_firstreal ge_balance_negative_add_intro_firstreal. (((((ge_representation_real_code_add_intro_first) = 2 * (ge_balance_positive_add_intro_firstreal) /\ (ge_balance_negative_add_intro_firstreal) = 0) \/ exists ge_signed_half_add_intro_firstrealdecode. (((ge_representation_real_code_add_intro_first) = 2 * ge_signed_half_add_intro_firstrealdecode + 1 /\ (ge_balance_positive_add_intro_firstreal) = 0) /\ (ge_balance_negative_add_intro_firstreal) = S ge_signed_half_add_intro_firstrealdecode))) /\ ((a) + ge_balance_negative_add_intro_firstreal = (b) + ge_balance_positive_add_intro_firstreal))) /\ (exists ge_balance_positive_add_intro_firstimaginary ge_balance_negative_add_intro_firstimaginary. (((((ge_representation_imaginary_code_add_intro_first) = 2 * (ge_balance_positive_add_intro_firstimaginary) /\ (ge_balance_negative_add_intro_firstimaginary) = 0) \/ exists ge_signed_half_add_intro_firstimaginarydecode. (((ge_representation_imaginary_code_add_intro_first) = 2 * ge_signed_half_add_intro_firstimaginarydecode + 1 /\ (ge_balance_positive_add_intro_firstimaginary) = 0) /\ (ge_balance_negative_add_intro_firstimaginary) = S ge_signed_half_add_intro_firstimaginarydecode))) /\ ((c) + ge_balance_negative_add_intro_firstimaginary = (d) + ge_balance_positive_add_intro_firstimaginary)))))) -> (exists ge_representation_real_code_add_intro_second ge_representation_imaginary_code_add_intro_second. (((bc) = ((ge_representation_real_code_add_intro_second) + (ge_representation_imaginary_code_add_intro_second)) * S ((ge_representation_real_code_add_intro_second) + (ge_representation_imaginary_code_add_intro_second)) + ((ge_representation_imaginary_code_add_intro_second) + (ge_representation_imaginary_code_add_intro_second))) /\ ((exists ge_balance_positive_add_intro_secondreal ge_balance_negative_add_intro_secondreal. (((((ge_representation_real_code_add_intro_second) = 2 * (ge_balance_positive_add_intro_secondreal) /\ (ge_balance_negative_add_intro_secondreal) = 0) \/ exists ge_signed_half_add_intro_secondrealdecode. (((ge_representation_real_code_add_intro_second) = 2 * ge_signed_half_add_intro_secondrealdecode + 1 /\ (ge_balance_positive_add_intro_secondreal) = 0) /\ (ge_balance_negative_add_intro_secondreal) = S ge_signed_half_add_intro_secondrealdecode))) /\ ((e) + ge_balance_negative_add_intro_secondreal = (f) + ge_balance_positive_add_intro_secondreal))) /\ (exists ge_balance_positive_add_intro_secondimaginary ge_balance_negative_add_intro_secondimaginary. (((((ge_representation_imaginary_code_add_intro_second) = 2 * (ge_balance_positive_add_intro_secondimaginary) /\ (ge_balance_negative_add_intro_secondimaginary) = 0) \/ exists ge_signed_half_add_intro_secondimaginarydecode. (((ge_representation_imaginary_code_add_intro_second) = 2 * ge_signed_half_add_intro_secondimaginarydecode + 1 /\ (ge_balance_positive_add_intro_secondimaginary) = 0) /\ (ge_balance_negative_add_intro_secondimaginary) = S ge_signed_half_add_intro_secondimaginarydecode))) /\ ((g) + ge_balance_negative_add_intro_secondimaginary = (h) + ge_balance_positive_add_intro_secondimaginary)))))) -> (exists ge_representation_real_code_add_intro_output ge_representation_imaginary_code_add_intro_output. (((cc) = ((ge_representation_real_code_add_intro_output) + (ge_representation_imaginary_code_add_intro_output)) * S ((ge_representation_real_code_add_intro_output) + (ge_representation_imaginary_code_add_intro_output)) + ((ge_representation_imaginary_code_add_intro_output) + (ge_representation_imaginary_code_add_intro_output))) /\ ((exists ge_balance_positive_add_intro_outputreal ge_balance_negative_add_intro_outputreal. (((((ge_representation_real_code_add_intro_output) = 2 * (ge_balance_positive_add_intro_outputreal) /\ (ge_balance_negative_add_intro_outputreal) = 0) \/ exists ge_signed_half_add_intro_outputrealdecode. (((ge_representation_real_code_add_intro_output) = 2 * ge_signed_half_add_intro_outputrealdecode + 1 /\ (ge_balance_positive_add_intro_outputreal) = 0) /\ (ge_balance_negative_add_intro_outputreal) = S ge_signed_half_add_intro_outputrealdecode))) /\ ((((a) + (e))) + ge_balance_negative_add_intro_outputreal = (((b) + (f))) + ge_balance_positive_add_intro_outputreal))) /\ (exists ge_balance_positive_add_intro_outputimaginary ge_balance_negative_add_intro_outputimaginary. (((((ge_representation_imaginary_code_add_intro_output) = 2 * (ge_balance_positive_add_intro_outputimaginary) /\ (ge_balance_negative_add_intro_outputimaginary) = 0) \/ exists ge_signed_half_add_intro_outputimaginarydecode. (((ge_representation_imaginary_code_add_intro_output) = 2 * ge_signed_half_add_intro_outputimaginarydecode + 1 /\ (ge_balance_positive_add_intro_outputimaginary) = 0) /\ (ge_balance_negative_add_intro_outputimaginary) = S ge_signed_half_add_intro_outputimaginarydecode))) /\ ((((c) + (g))) + ge_balance_negative_add_intro_outputimaginary = (((d) + (h))) + ge_balance_positive_add_intro_outputimaginary)))))) -> (exists ge_first_rp_add_intro_graph ge_first_rn_add_intro_graph ge_first_ip_add_intro_graph ge_first_in_add_intro_graph ge_second_rp_add_intro_graph ge_second_rn_add_intro_graph ge_second_ip_add_intro_graph ge_second_in_add_intro_graph. ((exists ge_representation_real_code_add_intro_graphfirst ge_representation_imaginary_code_add_intro_graphfirst. (((ac) = ((ge_representation_real_code_add_intro_graphfirst) + (ge_representation_imaginary_code_add_intro_graphfirst)) * S ((ge_representation_real_code_add_intro_graphfirst) + (ge_representation_imaginary_code_add_intro_graphfirst)) + ((ge_representation_imaginary_code_add_intro_graphfirst) + (ge_representation_imaginary_code_add_intro_graphfirst))) /\ ((exists ge_balance_positive_add_intro_graphfirstreal ge_balance_negative_add_intro_graphfirstreal. (((((ge_representation_real_code_add_intro_graphfirst) = 2 * (ge_balance_positive_add_intro_graphfirstreal) /\ (ge_balance_negative_add_intro_graphfirstreal) = 0) \/ exists ge_signed_half_add_intro_graphfirstrealdecode. (((ge_representation_real_code_add_intro_graphfirst) = 2 * ge_signed_half_add_intro_graphfirstrealdecode + 1 /\ (ge_balance_positive_add_intro_graphfirstreal) = 0) /\ (ge_balance_negative_add_intro_graphfirstreal) = S ge_signed_half_add_intro_graphfirstrealdecode))) /\ ((ge_first_rp_add_intro_graph) + ge_balance_negative_add_intro_graphfirstreal = (ge_first_rn_add_intro_graph) + ge_balance_positive_add_intro_graphfirstreal))) /\ (exists ge_balance_positive_add_intro_graphfirstimaginary ge_balance_negative_add_intro_graphfirstimaginary. (((((ge_representation_imaginary_code_add_intro_graphfirst) = 2 * (ge_balance_positive_add_intro_graphfirstimaginary) /\ (ge_balance_negative_add_intro_graphfirstimaginary) = 0) \/ exists ge_signed_half_add_intro_graphfirstimaginarydecode. (((ge_representation_imaginary_code_add_intro_graphfirst) = 2 * ge_signed_half_add_intro_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_add_intro_graphfirstimaginary) = 0) /\ (ge_balance_negative_add_intro_graphfirstimaginary) = S ge_signed_half_add_intro_graphfirstimaginarydecode))) /\ ((ge_first_ip_add_intro_graph) + ge_balance_negative_add_intro_graphfirstimaginary = (ge_first_in_add_intro_graph) + ge_balance_positive_add_intro_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_intro_graphsecond ge_representation_imaginary_code_add_intro_graphsecond. (((bc) = ((ge_representation_real_code_add_intro_graphsecond) + (ge_representation_imaginary_code_add_intro_graphsecond)) * S ((ge_representation_real_code_add_intro_graphsecond) + (ge_representation_imaginary_code_add_intro_graphsecond)) + ((ge_representation_imaginary_code_add_intro_graphsecond) + (ge_representation_imaginary_code_add_intro_graphsecond))) /\ ((exists ge_balance_positive_add_intro_graphsecondreal ge_balance_negative_add_intro_graphsecondreal. (((((ge_representation_real_code_add_intro_graphsecond) = 2 * (ge_balance_positive_add_intro_graphsecondreal) /\ (ge_balance_negative_add_intro_graphsecondreal) = 0) \/ exists ge_signed_half_add_intro_graphsecondrealdecode. (((ge_representation_real_code_add_intro_graphsecond) = 2 * ge_signed_half_add_intro_graphsecondrealdecode + 1 /\ (ge_balance_positive_add_intro_graphsecondreal) = 0) /\ (ge_balance_negative_add_intro_graphsecondreal) = S ge_signed_half_add_intro_graphsecondrealdecode))) /\ ((ge_second_rp_add_intro_graph) + ge_balance_negative_add_intro_graphsecondreal = (ge_second_rn_add_intro_graph) + ge_balance_positive_add_intro_graphsecondreal))) /\ (exists ge_balance_positive_add_intro_graphsecondimaginary ge_balance_negative_add_intro_graphsecondimaginary. (((((ge_representation_imaginary_code_add_intro_graphsecond) = 2 * (ge_balance_positive_add_intro_graphsecondimaginary) /\ (ge_balance_negative_add_intro_graphsecondimaginary) = 0) \/ exists ge_signed_half_add_intro_graphsecondimaginarydecode. (((ge_representation_imaginary_code_add_intro_graphsecond) = 2 * ge_signed_half_add_intro_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_add_intro_graphsecondimaginary) = 0) /\ (ge_balance_negative_add_intro_graphsecondimaginary) = S ge_signed_half_add_intro_graphsecondimaginarydecode))) /\ ((ge_second_ip_add_intro_graph) + ge_balance_negative_add_intro_graphsecondimaginary = (ge_second_in_add_intro_graph) + ge_balance_positive_add_intro_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_add_intro_graphoutput ge_representation_imaginary_code_add_intro_graphoutput. (((cc) = ((ge_representation_real_code_add_intro_graphoutput) + (ge_representation_imaginary_code_add_intro_graphoutput)) * S ((ge_representation_real_code_add_intro_graphoutput) + (ge_representation_imaginary_code_add_intro_graphoutput)) + ((ge_representation_imaginary_code_add_intro_graphoutput) + (ge_representation_imaginary_code_add_intro_graphoutput))) /\ ((exists ge_balance_positive_add_intro_graphoutputreal ge_balance_negative_add_intro_graphoutputreal. (((((ge_representation_real_code_add_intro_graphoutput) = 2 * (ge_balance_positive_add_intro_graphoutputreal) /\ (ge_balance_negative_add_intro_graphoutputreal) = 0) \/ exists ge_signed_half_add_intro_graphoutputrealdecode. (((ge_representation_real_code_add_intro_graphoutput) = 2 * ge_signed_half_add_intro_graphoutputrealdecode + 1 /\ (ge_balance_positive_add_intro_graphoutputreal) = 0) /\ (ge_balance_negative_add_intro_graphoutputreal) = S ge_signed_half_add_intro_graphoutputrealdecode))) /\ ((((ge_first_rp_add_intro_graph) + (ge_second_rp_add_intro_graph))) + ge_balance_negative_add_intro_graphoutputreal = (((ge_first_rn_add_intro_graph) + (ge_second_rn_add_intro_graph))) + ge_balance_positive_add_intro_graphoutputreal))) /\ (exists ge_balance_positive_add_intro_graphoutputimaginary ge_balance_negative_add_intro_graphoutputimaginary. (((((ge_representation_imaginary_code_add_intro_graphoutput) = 2 * (ge_balance_positive_add_intro_graphoutputimaginary) /\ (ge_balance_negative_add_intro_graphoutputimaginary) = 0) \/ exists ge_signed_half_add_intro_graphoutputimaginarydecode. (((ge_representation_imaginary_code_add_intro_graphoutput) = 2 * ge_signed_half_add_intro_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_add_intro_graphoutputimaginary) = 0) /\ (ge_balance_negative_add_intro_graphoutputimaginary) = S ge_signed_half_add_intro_graphoutputimaginarydecode))) /\ ((((ge_first_ip_add_intro_graph) + (ge_second_ip_add_intro_graph))) + ge_balance_negative_add_intro_graphoutputimaginary = (((ge_first_in_add_intro_graph) + (ge_second_in_add_intro_graph))) + ge_balance_positive_add_intro_graphoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

27 script commands · 7 reading checkpoints · 0 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.

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 a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro f
  10. L10
    intro g
02Fix variables and assumptionsL11–14

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

  1. L11
    intro h
  2. L12
    intro hfirst
  3. L13
    intro hsecond
  4. L14
    intro houtput
03Construct an explicit witnessL15–22

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists a
  2. L16
    exists b
  3. L17
    exists c
  4. L18
    exists d
  5. L19
    exists e
  6. L20
    exists f
  7. L21
    exists g
  8. L22
    exists h
04Separate the logical casesL23–23

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

  1. L23
    split
05Use earlier factsL24–24

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

  1. L24
    exact hfirst
06Separate the logical casesL25–25

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

  1. L25
    split
07Use earlier factsL26–27

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

  1. L26
    exact hsecond
  2. L27
    exact houtput

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro h
  12. 0012intro hfirst
  13. 0013intro hsecond
  14. 0014intro houtput
  15. 0015exists a
  16. 0016exists b
  17. 0017exists c
  18. 0018exists d
  19. 0019exists e
  20. 0020exists f
  21. 0021exists g
  22. 0022exists h
  23. 0023split
  24. 0024exact hfirst
  25. 0025split
  26. 0026exact hsecond
  27. 0027exact houtput