GI002C

gaussian_equal_transitive

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 1 declared prerequisite and contains 35 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_equal_transitive Alpha theorem; checked-use authorized

Direct dependents

GI0032 gaussian_adjoint_product_is_norm_scale GI0033 gaussian_residual_conjugate_identity GI003A gaussian_signed_euclidean_division_exists

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

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.

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 exact 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