GI002C

gaussian_equal_transitive

Represented Gaussian integer equality is transitive by actual signed cross-sum cancellation.

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

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ∀ i. ∀ j. ∀ k. ∀ l. a + f = e + b ∧ c + h = g + d → e + j = i + f ∧ g + l = k + h → a + j = i + b ∧ c + l = k + d

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

Definition DAG

none

Actual proof prerequisites

integer_span_pair_equal_transitive · checked external prerequisite
Original expanded first-order statement 
forall a b c d e f g h i j k l. (((((a) + (f)) = ((e) + (b))) /\ (((c) + (h)) = ((g) + (d))))) -> (((((e) + (j)) = ((i) + (f))) /\ (((g) + (l)) = ((k) + (h))))) -> (((((a) + (j)) = ((i) + (b))) /\ (((c) + (l)) = ((k) + (d)))))

Complete tactic proof in conservative notation

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

35 script commands · 5 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 a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro f
  7. L7
    intro g
  8. L8
    intro h
  9. L9
    intro i
  10. L10
    intro j
02Fix variables and assumptionsL11–14

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

  1. L11
    intro k
  2. L12
    intro l
  3. L13
    intro hfirst
  4. L14
    intro hsecond
03Separate the logical casesL15–17

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

  1. L15
    cases hfirst
  2. L16
    cases hsecond
  3. L17
    split
04Use earlier factsL18–27

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

  1. L18
    specialize integer_span_pair_equal_transitive a
  2. L19
    specialize integer_span_pair_equal_transitive b
  3. L20
    specialize integer_span_pair_equal_transitive e
  4. L21
    specialize integer_span_pair_equal_transitive f
  5. L22
    specialize integer_span_pair_equal_transitive i
  6. L23
    specialize integer_span_pair_equal_transitive j
  7. L24
    apply integer_span_pair_equal_transitive
  8. L25
    exact hfirst_left
  9. L26
    exact hsecond_left
  10. L27
    specialize integer_span_pair_equal_transitive c
05Use earlier factsL28–35

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

  1. L28
    specialize integer_span_pair_equal_transitive d
  2. L29
    specialize integer_span_pair_equal_transitive g
  3. L30
    specialize integer_span_pair_equal_transitive h
  4. L31
    specialize integer_span_pair_equal_transitive k
  5. L32
    specialize integer_span_pair_equal_transitive l
  6. L33
    apply integer_span_pair_equal_transitive
  7. L34
    exact hfirst_right
  8. L35
    exact hsecond_right

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro i
  10. 0010intro j
  11. 0011intro k
  12. 0012intro l
  13. 0013intro hfirst
  14. 0014intro hsecond
  15. 0015cases hfirst
  16. 0016cases hsecond
  17. 0017split
  18. 0018specialize integer_span_pair_equal_transitive a
  19. 0019specialize integer_span_pair_equal_transitive b
  20. 0020specialize integer_span_pair_equal_transitive e
  21. 0021specialize integer_span_pair_equal_transitive f
  22. 0022specialize integer_span_pair_equal_transitive i
  23. 0023specialize integer_span_pair_equal_transitive j
  24. 0024apply integer_span_pair_equal_transitive
  25. 0025exact hfirst_left
  26. 0026exact hsecond_left
  27. 0027specialize integer_span_pair_equal_transitive c
  28. 0028specialize integer_span_pair_equal_transitive d
  29. 0029specialize integer_span_pair_equal_transitive g
  30. 0030specialize integer_span_pair_equal_transitive h
  31. 0031specialize integer_span_pair_equal_transitive k
  32. 0032specialize integer_span_pair_equal_transitive l
  33. 0033apply integer_span_pair_equal_transitive
  34. 0034exact hfirst_right
  35. 0035exact hsecond_right