GI0047

gaussian_representation_zero_iff

A canonical signed-coordinate pair is zero exactly when both represented integer differences vanish, even for overlapping raw representatives.

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. ZPairRep(z,a,b,c,d) → (z = 0 → a = b ∧ c = d) ∧ (a = b ∧ c = d → z = 0)

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

Definition DAG

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

Actual proof prerequisites

signed_balance_zero_iff · checked external prerequisitegaussian_pair_zero_codesmul_zero_left · checked external prerequisitezero_add · checked external prerequisite
Original expanded first-order statement 
forall z a b c d. (exists ge_representation_real_code_representation_zero ge_representation_imaginary_code_representation_zero. (((z) = ((ge_representation_real_code_representation_zero) + (ge_representation_imaginary_code_representation_zero)) * S ((ge_representation_real_code_representation_zero) + (ge_representation_imaginary_code_representation_zero)) + ((ge_representation_imaginary_code_representation_zero) + (ge_representation_imaginary_code_representation_zero))) /\ ((exists ge_balance_positive_representation_zeroreal ge_balance_negative_representation_zeroreal. (((((ge_representation_real_code_representation_zero) = 2 * (ge_balance_positive_representation_zeroreal) /\ (ge_balance_negative_representation_zeroreal) = 0) \/ exists ge_signed_half_representation_zerorealdecode. (((ge_representation_real_code_representation_zero) = 2 * ge_signed_half_representation_zerorealdecode + 1 /\ (ge_balance_positive_representation_zeroreal) = 0) /\ (ge_balance_negative_representation_zeroreal) = S ge_signed_half_representation_zerorealdecode))) /\ ((a) + ge_balance_negative_representation_zeroreal = (b) + ge_balance_positive_representation_zeroreal))) /\ (exists ge_balance_positive_representation_zeroimaginary ge_balance_negative_representation_zeroimaginary. (((((ge_representation_imaginary_code_representation_zero) = 2 * (ge_balance_positive_representation_zeroimaginary) /\ (ge_balance_negative_representation_zeroimaginary) = 0) \/ exists ge_signed_half_representation_zeroimaginarydecode. (((ge_representation_imaginary_code_representation_zero) = 2 * ge_signed_half_representation_zeroimaginarydecode + 1 /\ (ge_balance_positive_representation_zeroimaginary) = 0) /\ (ge_balance_negative_representation_zeroimaginary) = S ge_signed_half_representation_zeroimaginarydecode))) /\ ((c) + ge_balance_negative_representation_zeroimaginary = (d) + ge_balance_positive_representation_zeroimaginary)))))) -> ((z = 0 -> (a = b /\ c = d)) /\ ((a = b /\ c = d) -> z = 0))

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 · 14 reading checkpoints · 5 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 pair zero codes
01Fix variables and assumptionsL1–6

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 hrep
02Separate the logical casesL7–10

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

  1. L7
    cases hrep
  2. L8
    cases hrep_witness
  3. L9
    cases hrep_witness_witness
  4. L10
    cases hrep_witness_witness_right
03Establish hrealL11–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance zero iff.

  1. L11
    have hreal : (x = 0 -> a = b) /\ (a = b -> x = 0)
  2. L12
    specialize signed_balance_zero_iff x
  3. L13
    specialize signed_balance_zero_iff a
  4. L14
    specialize signed_balance_zero_iff b
  5. L15
    apply signed_balance_zero_iff
  6. L16
    exact hrep_witness_witness_right_left
04Separate the logical casesL17–17

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

  1. L17
    cases hreal
05Establish himaginaryL18–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed balance zero iff.

  1. L18
    have himaginary : (x1 = 0 -> c = d) /\ (c = d -> x1 = 0)
  2. L19
    specialize signed_balance_zero_iff x1
  3. L20
    specialize signed_balance_zero_iff c
  4. L21
    specialize signed_balance_zero_iff d
  5. L22
    apply signed_balance_zero_iff
  6. L23
    exact hrep_witness_witness_right_right
06Separate the logical casesL24–25

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

  1. L24
    cases himaginary
  2. L25
    split
07Fix variables and assumptionsL26–26

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

  1. L26
    intro hzero
08Establish hcodesL27–33

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

  1. L27
    have hcodes : x = 0 /\ x1 = 0
  2. L28
    specialize gaussian_pair_zero_codes z
  3. L29
    specialize gaussian_pair_zero_codes x
  4. L30
    specialize gaussian_pair_zero_codes x1
  5. L31
    apply gaussian_pair_zero_codes
  6. L32
    exact hrep_witness_witness_left
  7. L33
    exact hzero
09Separate the logical casesL34–35

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

  1. L34
    cases hcodes
  2. L35
    split
10Use earlier factsL36–39

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

  1. L36
    apply hreal_left
  2. L37
    exact hcodes_left
  3. L38
    apply himaginary_left
  4. L39
    exact hcodes_right
11Fix variables and assumptionsL40–40

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

  1. L40
    intro hequal
12Separate the logical casesL41–41

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

  1. L41
    cases hequal
13Establish hrealzeroL42–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hreal right.

  1. L42
    have hrealzero : x = 0
  2. L43
    apply hreal_right
  3. L44
    exact hequal_left
14Establish himaginaryzeroL45–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply himaginary right.

  1. L45
    have himaginaryzero : x1 = 0
  2. L46
    apply himaginary_right
  3. L47
    exact hequal_right
  4. L48
    trans ((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))
  5. L49
    exact hrep_witness_witness_left
  6. L50
    simp [hrealzero, himaginaryzero, mul_zero_left, zero_add]

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 hrep
  7. 0007cases hrep
  8. 0008cases hrep_witness
  9. 0009cases hrep_witness_witness
  10. 0010cases hrep_witness_witness_right
  11. 0011have hreal : (x = 0 -> a = b) /\ (a = b -> x = 0)
  12. 0012specialize signed_balance_zero_iff x
  13. 0013specialize signed_balance_zero_iff a
  14. 0014specialize signed_balance_zero_iff b
  15. 0015apply signed_balance_zero_iff
  16. 0016exact hrep_witness_witness_right_left
  17. 0017cases hreal
  18. 0018have himaginary : (x1 = 0 -> c = d) /\ (c = d -> x1 = 0)
  19. 0019specialize signed_balance_zero_iff x1
  20. 0020specialize signed_balance_zero_iff c
  21. 0021specialize signed_balance_zero_iff d
  22. 0022apply signed_balance_zero_iff
  23. 0023exact hrep_witness_witness_right_right
  24. 0024cases himaginary
  25. 0025split
  26. 0026intro hzero
  27. 0027have hcodes : x = 0 /\ x1 = 0
  28. 0028specialize gaussian_pair_zero_codes z
  29. 0029specialize gaussian_pair_zero_codes x
  30. 0030specialize gaussian_pair_zero_codes x1
  31. 0031apply gaussian_pair_zero_codes
  32. 0032exact hrep_witness_witness_left
  33. 0033exact hzero
  34. 0034cases hcodes
  35. 0035split
  36. 0036apply hreal_left
  37. 0037exact hcodes_left
  38. 0038apply himaginary_left
  39. 0039exact hcodes_right
  40. 0040intro hequal
  41. 0041cases hequal
  42. 0042have hrealzero : x = 0
  43. 0043apply hreal_right
  44. 0044exact hequal_left
  45. 0045have himaginaryzero : x1 = 0
  46. 0046apply himaginary_right
  47. 0047exact hequal_right
  48. 0048trans ((x) + (x1)) * S ((x) + (x1)) + ((x1) + (x1))
  49. 0049exact hrep_witness_witness_left
  50. 0050simp [hrealzero, himaginaryzero, mul_zero_left, zero_add]