GI0042

gaussian_representation_equal

Any two signed representatives of the same canonical Gaussian natural code denote the same Gaussian integer.

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

∀ z. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ZPairRep(z,a,b,c,d) → ZPairRep(z,e,f,g,h) → a + f = e + b ∧ c + h = g + d

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 2

Actual proof prerequisites

pair_code_injective · checked external prerequisitegaussian_signed_balance_same_code
Original expanded first-order statement 
forall z a b c d e f g h. (exists ge_representation_real_code_same_gaussian_code_first ge_representation_imaginary_code_same_gaussian_code_first. (((z) = ((ge_representation_real_code_same_gaussian_code_first) + (ge_representation_imaginary_code_same_gaussian_code_first)) * S ((ge_representation_real_code_same_gaussian_code_first) + (ge_representation_imaginary_code_same_gaussian_code_first)) + ((ge_representation_imaginary_code_same_gaussian_code_first) + (ge_representation_imaginary_code_same_gaussian_code_first))) /\ ((exists ge_balance_positive_same_gaussian_code_firstreal ge_balance_negative_same_gaussian_code_firstreal. (((((ge_representation_real_code_same_gaussian_code_first) = 2 * (ge_balance_positive_same_gaussian_code_firstreal) /\ (ge_balance_negative_same_gaussian_code_firstreal) = 0) \/ exists ge_signed_half_same_gaussian_code_firstrealdecode. (((ge_representation_real_code_same_gaussian_code_first) = 2 * ge_signed_half_same_gaussian_code_firstrealdecode + 1 /\ (ge_balance_positive_same_gaussian_code_firstreal) = 0) /\ (ge_balance_negative_same_gaussian_code_firstreal) = S ge_signed_half_same_gaussian_code_firstrealdecode))) /\ ((a) + ge_balance_negative_same_gaussian_code_firstreal = (b) + ge_balance_positive_same_gaussian_code_firstreal))) /\ (exists ge_balance_positive_same_gaussian_code_firstimaginary ge_balance_negative_same_gaussian_code_firstimaginary. (((((ge_representation_imaginary_code_same_gaussian_code_first) = 2 * (ge_balance_positive_same_gaussian_code_firstimaginary) /\ (ge_balance_negative_same_gaussian_code_firstimaginary) = 0) \/ exists ge_signed_half_same_gaussian_code_firstimaginarydecode. (((ge_representation_imaginary_code_same_gaussian_code_first) = 2 * ge_signed_half_same_gaussian_code_firstimaginarydecode + 1 /\ (ge_balance_positive_same_gaussian_code_firstimaginary) = 0) /\ (ge_balance_negative_same_gaussian_code_firstimaginary) = S ge_signed_half_same_gaussian_code_firstimaginarydecode))) /\ ((c) + ge_balance_negative_same_gaussian_code_firstimaginary = (d) + ge_balance_positive_same_gaussian_code_firstimaginary)))))) -> (exists ge_representation_real_code_same_gaussian_code_second ge_representation_imaginary_code_same_gaussian_code_second. (((z) = ((ge_representation_real_code_same_gaussian_code_second) + (ge_representation_imaginary_code_same_gaussian_code_second)) * S ((ge_representation_real_code_same_gaussian_code_second) + (ge_representation_imaginary_code_same_gaussian_code_second)) + ((ge_representation_imaginary_code_same_gaussian_code_second) + (ge_representation_imaginary_code_same_gaussian_code_second))) /\ ((exists ge_balance_positive_same_gaussian_code_secondreal ge_balance_negative_same_gaussian_code_secondreal. (((((ge_representation_real_code_same_gaussian_code_second) = 2 * (ge_balance_positive_same_gaussian_code_secondreal) /\ (ge_balance_negative_same_gaussian_code_secondreal) = 0) \/ exists ge_signed_half_same_gaussian_code_secondrealdecode. (((ge_representation_real_code_same_gaussian_code_second) = 2 * ge_signed_half_same_gaussian_code_secondrealdecode + 1 /\ (ge_balance_positive_same_gaussian_code_secondreal) = 0) /\ (ge_balance_negative_same_gaussian_code_secondreal) = S ge_signed_half_same_gaussian_code_secondrealdecode))) /\ ((e) + ge_balance_negative_same_gaussian_code_secondreal = (f) + ge_balance_positive_same_gaussian_code_secondreal))) /\ (exists ge_balance_positive_same_gaussian_code_secondimaginary ge_balance_negative_same_gaussian_code_secondimaginary. (((((ge_representation_imaginary_code_same_gaussian_code_second) = 2 * (ge_balance_positive_same_gaussian_code_secondimaginary) /\ (ge_balance_negative_same_gaussian_code_secondimaginary) = 0) \/ exists ge_signed_half_same_gaussian_code_secondimaginarydecode. (((ge_representation_imaginary_code_same_gaussian_code_second) = 2 * ge_signed_half_same_gaussian_code_secondimaginarydecode + 1 /\ (ge_balance_positive_same_gaussian_code_secondimaginary) = 0) /\ (ge_balance_negative_same_gaussian_code_secondimaginary) = S ge_signed_half_same_gaussian_code_secondimaginarydecode))) /\ ((g) + ge_balance_negative_same_gaussian_code_secondimaginary = (h) + ge_balance_positive_same_gaussian_code_secondimaginary)))))) -> (((((a) + (f)) = ((e) + (b))) /\ (((c) + (h)) = ((g) + (d)))))

Complete tactic proof in conservative notation

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

50 script commands · 9 reading checkpoints · 1 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 (1)
gaussian signed balance same code
01Fix variables and assumptionsL1–10

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

  1. L1
    intro z
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro h
  10. L10
    intro hfirst
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsecond
03Separate the logical casesL12–19

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

  1. L12
    cases hfirst
  2. L13
    cases hfirst_witness
  3. L14
    cases hfirst_witness_witness
  4. L15
    cases hfirst_witness_witness_right
  5. L16
    cases hsecond
  6. L17
    cases hsecond_witness
  7. L18
    cases hsecond_witness_witness
  8. L19
    cases hsecond_witness_witness_right
04Establish hcodesL20–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pair code injective.

  1. L20
    have hcodes : x = x2 /\ x1 = x3
  2. L21
    specialize pair_code_injective z
  3. L22
    specialize pair_code_injective x
  4. L23
    specialize pair_code_injective x1
  5. L24
    specialize pair_code_injective x2
  6. L25
    specialize pair_code_injective x3
  7. L26
    apply pair_code_injective
  8. L27
    exact hfirst_witness_witness_left
  9. L28
    exact hsecond_witness_witness_left
05Separate the logical casesL29–29

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

  1. L29
    cases hcodes
06Calculate and transport equalitiesL30–33

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    rewrite hcodes_left at hfirst_witness_witness_right_left
  2. L31
    rewrite hcodes_left at hfirst_witness_witness_right_left
  3. L32
    rewrite hcodes_right at hfirst_witness_witness_right_right
  4. L33
    rewrite hcodes_right at hfirst_witness_witness_right_right
07Separate the logical casesL34–34

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

  1. L34
    split
08Use earlier factsL35–44

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

  1. L35
    specialize gaussian_signed_balance_same_code x2
  2. L36
    specialize gaussian_signed_balance_same_code a
  3. L37
    specialize gaussian_signed_balance_same_code b
  4. L38
    specialize gaussian_signed_balance_same_code e
  5. L39
    specialize gaussian_signed_balance_same_code f
  6. L40
    apply gaussian_signed_balance_same_code
  7. L41
    exact hfirst_witness_witness_right_left
  8. L42
    exact hsecond_witness_witness_right_left
  9. L43
    specialize gaussian_signed_balance_same_code x3
  10. L44
    specialize gaussian_signed_balance_same_code c
09Use earlier factsL45–50

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

  1. L45
    specialize gaussian_signed_balance_same_code d
  2. L46
    specialize gaussian_signed_balance_same_code g
  3. L47
    specialize gaussian_signed_balance_same_code h
  4. L48
    apply gaussian_signed_balance_same_code
  5. L49
    exact hfirst_witness_witness_right_right
  6. L50
    exact hsecond_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 50 lines
  1. 0001intro z
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro h
  10. 0010intro hfirst
  11. 0011intro hsecond
  12. 0012cases hfirst
  13. 0013cases hfirst_witness
  14. 0014cases hfirst_witness_witness
  15. 0015cases hfirst_witness_witness_right
  16. 0016cases hsecond
  17. 0017cases hsecond_witness
  18. 0018cases hsecond_witness_witness
  19. 0019cases hsecond_witness_witness_right
  20. 0020have hcodes : x = x2 /\ x1 = x3
  21. 0021specialize pair_code_injective z
  22. 0022specialize pair_code_injective x
  23. 0023specialize pair_code_injective x1
  24. 0024specialize pair_code_injective x2
  25. 0025specialize pair_code_injective x3
  26. 0026apply pair_code_injective
  27. 0027exact hfirst_witness_witness_left
  28. 0028exact hsecond_witness_witness_left
  29. 0029cases hcodes
  30. 0030rewrite hcodes_left at hfirst_witness_witness_right_left
  31. 0031rewrite hcodes_left at hfirst_witness_witness_right_left
  32. 0032rewrite hcodes_right at hfirst_witness_witness_right_right
  33. 0033rewrite hcodes_right at hfirst_witness_witness_right_right
  34. 0034split
  35. 0035specialize gaussian_signed_balance_same_code x2
  36. 0036specialize gaussian_signed_balance_same_code a
  37. 0037specialize gaussian_signed_balance_same_code b
  38. 0038specialize gaussian_signed_balance_same_code e
  39. 0039specialize gaussian_signed_balance_same_code f
  40. 0040apply gaussian_signed_balance_same_code
  41. 0041exact hfirst_witness_witness_right_left
  42. 0042exact hsecond_witness_witness_right_left
  43. 0043specialize gaussian_signed_balance_same_code x3
  44. 0044specialize gaussian_signed_balance_same_code c
  45. 0045specialize gaussian_signed_balance_same_code d
  46. 0046specialize gaussian_signed_balance_same_code g
  47. 0047specialize gaussian_signed_balance_same_code h
  48. 0048apply gaussian_signed_balance_same_code
  49. 0049exact hfirst_witness_witness_right_right
  50. 0050exact hsecond_witness_witness_right_right