GF003A

gaussian_add_cancel_right

A common right summand cancels in the actual canonical Gaussian additive graph.

Alpha v34 checked-use · first admitted v30 · 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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ t. ZPairAdd(a,c,t) → ZPairAdd(b,c,t) → a = b

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

Definition DAG

ZPairAdd(a,b,c) · 2

Actual proof prerequisites

gaussian_add_cancel_leftgaussian_add_commutative
Original expanded first-order statement 
forall a b c t. (exists ge_first_rp_cancel_right_first ge_first_rn_cancel_right_first ge_first_ip_cancel_right_first ge_first_in_cancel_right_first ge_second_rp_cancel_right_first ge_second_rn_cancel_right_first ge_second_ip_cancel_right_first ge_second_in_cancel_right_first. ((exists ge_representation_real_code_cancel_right_firstfirst ge_representation_imaginary_code_cancel_right_firstfirst. (((a) = ((ge_representation_real_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst)) * S ((ge_representation_real_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst)) + ((ge_representation_imaginary_code_cancel_right_firstfirst) + (ge_representation_imaginary_code_cancel_right_firstfirst))) /\ ((exists ge_balance_positive_cancel_right_firstfirstreal ge_balance_negative_cancel_right_firstfirstreal. (((((ge_representation_real_code_cancel_right_firstfirst) = 2 * (ge_balance_positive_cancel_right_firstfirstreal) /\ (ge_balance_negative_cancel_right_firstfirstreal) = 0) \/ exists ge_signed_half_cancel_right_firstfirstrealdecode. (((ge_representation_real_code_cancel_right_firstfirst) = 2 * ge_signed_half_cancel_right_firstfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstfirstreal) = 0) /\ (ge_balance_negative_cancel_right_firstfirstreal) = S ge_signed_half_cancel_right_firstfirstrealdecode))) /\ ((ge_first_rp_cancel_right_first) + ge_balance_negative_cancel_right_firstfirstreal = (ge_first_rn_cancel_right_first) + ge_balance_positive_cancel_right_firstfirstreal))) /\ (exists ge_balance_positive_cancel_right_firstfirstimaginary ge_balance_negative_cancel_right_firstfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_firstfirst) = 2 * (ge_balance_positive_cancel_right_firstfirstimaginary) /\ (ge_balance_negative_cancel_right_firstfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstfirst) = 2 * ge_signed_half_cancel_right_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstfirstimaginary) = S ge_signed_half_cancel_right_firstfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_first) + ge_balance_negative_cancel_right_firstfirstimaginary = (ge_first_in_cancel_right_first) + ge_balance_positive_cancel_right_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_firstsecond ge_representation_imaginary_code_cancel_right_firstsecond. (((c) = ((ge_representation_real_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond)) * S ((ge_representation_real_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond)) + ((ge_representation_imaginary_code_cancel_right_firstsecond) + (ge_representation_imaginary_code_cancel_right_firstsecond))) /\ ((exists ge_balance_positive_cancel_right_firstsecondreal ge_balance_negative_cancel_right_firstsecondreal. (((((ge_representation_real_code_cancel_right_firstsecond) = 2 * (ge_balance_positive_cancel_right_firstsecondreal) /\ (ge_balance_negative_cancel_right_firstsecondreal) = 0) \/ exists ge_signed_half_cancel_right_firstsecondrealdecode. (((ge_representation_real_code_cancel_right_firstsecond) = 2 * ge_signed_half_cancel_right_firstsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstsecondreal) = 0) /\ (ge_balance_negative_cancel_right_firstsecondreal) = S ge_signed_half_cancel_right_firstsecondrealdecode))) /\ ((ge_second_rp_cancel_right_first) + ge_balance_negative_cancel_right_firstsecondreal = (ge_second_rn_cancel_right_first) + ge_balance_positive_cancel_right_firstsecondreal))) /\ (exists ge_balance_positive_cancel_right_firstsecondimaginary ge_balance_negative_cancel_right_firstsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_firstsecond) = 2 * (ge_balance_positive_cancel_right_firstsecondimaginary) /\ (ge_balance_negative_cancel_right_firstsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstsecond) = 2 * ge_signed_half_cancel_right_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstsecondimaginary) = S ge_signed_half_cancel_right_firstsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_first) + ge_balance_negative_cancel_right_firstsecondimaginary = (ge_second_in_cancel_right_first) + ge_balance_positive_cancel_right_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_firstoutput ge_representation_imaginary_code_cancel_right_firstoutput. (((t) = ((ge_representation_real_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput)) * S ((ge_representation_real_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput)) + ((ge_representation_imaginary_code_cancel_right_firstoutput) + (ge_representation_imaginary_code_cancel_right_firstoutput))) /\ ((exists ge_balance_positive_cancel_right_firstoutputreal ge_balance_negative_cancel_right_firstoutputreal. (((((ge_representation_real_code_cancel_right_firstoutput) = 2 * (ge_balance_positive_cancel_right_firstoutputreal) /\ (ge_balance_negative_cancel_right_firstoutputreal) = 0) \/ exists ge_signed_half_cancel_right_firstoutputrealdecode. (((ge_representation_real_code_cancel_right_firstoutput) = 2 * ge_signed_half_cancel_right_firstoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_firstoutputreal) = 0) /\ (ge_balance_negative_cancel_right_firstoutputreal) = S ge_signed_half_cancel_right_firstoutputrealdecode))) /\ ((((ge_first_rp_cancel_right_first) + (ge_second_rp_cancel_right_first))) + ge_balance_negative_cancel_right_firstoutputreal = (((ge_first_rn_cancel_right_first) + (ge_second_rn_cancel_right_first))) + ge_balance_positive_cancel_right_firstoutputreal))) /\ (exists ge_balance_positive_cancel_right_firstoutputimaginary ge_balance_negative_cancel_right_firstoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_firstoutput) = 2 * (ge_balance_positive_cancel_right_firstoutputimaginary) /\ (ge_balance_negative_cancel_right_firstoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_firstoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_firstoutput) = 2 * ge_signed_half_cancel_right_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_firstoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_firstoutputimaginary) = S ge_signed_half_cancel_right_firstoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_right_first) + (ge_second_ip_cancel_right_first))) + ge_balance_negative_cancel_right_firstoutputimaginary = (((ge_first_in_cancel_right_first) + (ge_second_in_cancel_right_first))) + ge_balance_positive_cancel_right_firstoutputimaginary))))))))) -> (exists ge_first_rp_cancel_right_second ge_first_rn_cancel_right_second ge_first_ip_cancel_right_second ge_first_in_cancel_right_second ge_second_rp_cancel_right_second ge_second_rn_cancel_right_second ge_second_ip_cancel_right_second ge_second_in_cancel_right_second. ((exists ge_representation_real_code_cancel_right_secondfirst ge_representation_imaginary_code_cancel_right_secondfirst. (((b) = ((ge_representation_real_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst)) * S ((ge_representation_real_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst)) + ((ge_representation_imaginary_code_cancel_right_secondfirst) + (ge_representation_imaginary_code_cancel_right_secondfirst))) /\ ((exists ge_balance_positive_cancel_right_secondfirstreal ge_balance_negative_cancel_right_secondfirstreal. (((((ge_representation_real_code_cancel_right_secondfirst) = 2 * (ge_balance_positive_cancel_right_secondfirstreal) /\ (ge_balance_negative_cancel_right_secondfirstreal) = 0) \/ exists ge_signed_half_cancel_right_secondfirstrealdecode. (((ge_representation_real_code_cancel_right_secondfirst) = 2 * ge_signed_half_cancel_right_secondfirstrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondfirstreal) = 0) /\ (ge_balance_negative_cancel_right_secondfirstreal) = S ge_signed_half_cancel_right_secondfirstrealdecode))) /\ ((ge_first_rp_cancel_right_second) + ge_balance_negative_cancel_right_secondfirstreal = (ge_first_rn_cancel_right_second) + ge_balance_positive_cancel_right_secondfirstreal))) /\ (exists ge_balance_positive_cancel_right_secondfirstimaginary ge_balance_negative_cancel_right_secondfirstimaginary. (((((ge_representation_imaginary_code_cancel_right_secondfirst) = 2 * (ge_balance_positive_cancel_right_secondfirstimaginary) /\ (ge_balance_negative_cancel_right_secondfirstimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondfirstimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondfirst) = 2 * ge_signed_half_cancel_right_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondfirstimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondfirstimaginary) = S ge_signed_half_cancel_right_secondfirstimaginarydecode))) /\ ((ge_first_ip_cancel_right_second) + ge_balance_negative_cancel_right_secondfirstimaginary = (ge_first_in_cancel_right_second) + ge_balance_positive_cancel_right_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_cancel_right_secondsecond ge_representation_imaginary_code_cancel_right_secondsecond. (((c) = ((ge_representation_real_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond)) * S ((ge_representation_real_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond)) + ((ge_representation_imaginary_code_cancel_right_secondsecond) + (ge_representation_imaginary_code_cancel_right_secondsecond))) /\ ((exists ge_balance_positive_cancel_right_secondsecondreal ge_balance_negative_cancel_right_secondsecondreal. (((((ge_representation_real_code_cancel_right_secondsecond) = 2 * (ge_balance_positive_cancel_right_secondsecondreal) /\ (ge_balance_negative_cancel_right_secondsecondreal) = 0) \/ exists ge_signed_half_cancel_right_secondsecondrealdecode. (((ge_representation_real_code_cancel_right_secondsecond) = 2 * ge_signed_half_cancel_right_secondsecondrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondsecondreal) = 0) /\ (ge_balance_negative_cancel_right_secondsecondreal) = S ge_signed_half_cancel_right_secondsecondrealdecode))) /\ ((ge_second_rp_cancel_right_second) + ge_balance_negative_cancel_right_secondsecondreal = (ge_second_rn_cancel_right_second) + ge_balance_positive_cancel_right_secondsecondreal))) /\ (exists ge_balance_positive_cancel_right_secondsecondimaginary ge_balance_negative_cancel_right_secondsecondimaginary. (((((ge_representation_imaginary_code_cancel_right_secondsecond) = 2 * (ge_balance_positive_cancel_right_secondsecondimaginary) /\ (ge_balance_negative_cancel_right_secondsecondimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondsecondimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondsecond) = 2 * ge_signed_half_cancel_right_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondsecondimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondsecondimaginary) = S ge_signed_half_cancel_right_secondsecondimaginarydecode))) /\ ((ge_second_ip_cancel_right_second) + ge_balance_negative_cancel_right_secondsecondimaginary = (ge_second_in_cancel_right_second) + ge_balance_positive_cancel_right_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_cancel_right_secondoutput ge_representation_imaginary_code_cancel_right_secondoutput. (((t) = ((ge_representation_real_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput)) * S ((ge_representation_real_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput)) + ((ge_representation_imaginary_code_cancel_right_secondoutput) + (ge_representation_imaginary_code_cancel_right_secondoutput))) /\ ((exists ge_balance_positive_cancel_right_secondoutputreal ge_balance_negative_cancel_right_secondoutputreal. (((((ge_representation_real_code_cancel_right_secondoutput) = 2 * (ge_balance_positive_cancel_right_secondoutputreal) /\ (ge_balance_negative_cancel_right_secondoutputreal) = 0) \/ exists ge_signed_half_cancel_right_secondoutputrealdecode. (((ge_representation_real_code_cancel_right_secondoutput) = 2 * ge_signed_half_cancel_right_secondoutputrealdecode + 1 /\ (ge_balance_positive_cancel_right_secondoutputreal) = 0) /\ (ge_balance_negative_cancel_right_secondoutputreal) = S ge_signed_half_cancel_right_secondoutputrealdecode))) /\ ((((ge_first_rp_cancel_right_second) + (ge_second_rp_cancel_right_second))) + ge_balance_negative_cancel_right_secondoutputreal = (((ge_first_rn_cancel_right_second) + (ge_second_rn_cancel_right_second))) + ge_balance_positive_cancel_right_secondoutputreal))) /\ (exists ge_balance_positive_cancel_right_secondoutputimaginary ge_balance_negative_cancel_right_secondoutputimaginary. (((((ge_representation_imaginary_code_cancel_right_secondoutput) = 2 * (ge_balance_positive_cancel_right_secondoutputimaginary) /\ (ge_balance_negative_cancel_right_secondoutputimaginary) = 0) \/ exists ge_signed_half_cancel_right_secondoutputimaginarydecode. (((ge_representation_imaginary_code_cancel_right_secondoutput) = 2 * ge_signed_half_cancel_right_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_cancel_right_secondoutputimaginary) = 0) /\ (ge_balance_negative_cancel_right_secondoutputimaginary) = S ge_signed_half_cancel_right_secondoutputimaginarydecode))) /\ ((((ge_first_ip_cancel_right_second) + (ge_second_ip_cancel_right_second))) + ge_balance_negative_cancel_right_secondoutputimaginary = (((ge_first_in_cancel_right_second) + (ge_second_in_cancel_right_second))) + ge_balance_positive_cancel_right_secondoutputimaginary))))))))) -> a=b

Complete tactic proof in conservative notation

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

21 script commands · 3 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.

Named ingredients (2)
gaussian add cancel leftgaussian add commutative
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro t
  5. L5
    intro hA
  6. L6
    intro hB
02Use earlier factsL7–16

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

  1. L7
    specialize gaussian_add_cancel_left (c)
  2. L8
    specialize gaussian_add_cancel_left (a)
  3. L9
    specialize gaussian_add_cancel_left (b)
  4. L10
    specialize gaussian_add_cancel_left (t)
  5. L11
    apply gaussian_add_cancel_left
  6. L12
    specialize gaussian_add_commutative (a)
  7. L13
    specialize gaussian_add_commutative (c)
  8. L14
    specialize gaussian_add_commutative (t)
  9. L15
    apply gaussian_add_commutative
  10. L16
    exact hA
03Use earlier factsL17–21

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

  1. L17
    specialize gaussian_add_commutative (b)
  2. L18
    specialize gaussian_add_commutative (c)
  3. L19
    specialize gaussian_add_commutative (t)
  4. L20
    apply gaussian_add_commutative
  5. L21
    exact hB

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro t
  5. 0005intro hA
  6. 0006intro hB
  7. 0007specialize gaussian_add_cancel_left (c)
  8. 0008specialize gaussian_add_cancel_left (a)
  9. 0009specialize gaussian_add_cancel_left (b)
  10. 0010specialize gaussian_add_cancel_left (t)
  11. 0011apply gaussian_add_cancel_left
  12. 0012specialize gaussian_add_commutative (a)
  13. 0013specialize gaussian_add_commutative (c)
  14. 0014specialize gaussian_add_commutative (t)
  15. 0015apply gaussian_add_commutative
  16. 0016exact hA
  17. 0017specialize gaussian_add_commutative (b)
  18. 0018specialize gaussian_add_commutative (c)
  19. 0019specialize gaussian_add_commutative (t)
  20. 0020apply gaussian_add_commutative
  21. 0021exact hB