EI0030

eisenstein_coordinate_norm_zero

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

A genuine Eisenstein norm can be zero only when both represented integer coordinates are zero, with no sign-normality or positivity hypothesis.

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. (((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c)))))) = ((((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))) + (0))) -> a = b /\ c = d

Constructive proof overview

Generated structural guide

A genuine Eisenstein norm can be zero only when both represented integer coordinates are zero, with no sign-normality or positivity hypothesis.

The unchanged tactic script uses 6 declared prerequisites and contains 81 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

EI0012 eisenstein_norm_to_weighted_norm add_eq_zero_left Stable theorem; checked-use authorized add_eq_zero_right Stable theorem; checked-use authorized mul_left_cancel_nonzero Stable theorem; checked-use authorized gaussian_signed_square_zero_iff Alpha theorem; checked-use authorized add_right_cancel Stable theorem; checked-use authorized

Direct dependents

EI0031 eisenstein_coordinate_norm_nonzero

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

81 script commands · 25 reading checkpoints · 9 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.

Named ingredients (1)
eisenstein norm to weighted norm
01Fix variables and assumptionsL1–5

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 hnorm
02Establish hweightedL6–13

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein norm to weighted norm.

  1. L6
    have hweighted : exists ee_real_square_zero ee_imag_square_zero. (((((((((2) * (a))) + (d))) * (((((2) * (a))) + (d))))) + (((((((2) * (b))) + (c))) * (((((2) * (b))) + (c)))))) = ((ee_real_square_zero) + (((((((((2) * (a))) + (d))) * (((((2) * (b))) + (c))))) + (((((((2) * (b))) + (c))) * (((((2) * (a))) + (d))))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ee_imag_square_zero) + (((((c) * (d))) + (((d) * (c))))))) /\ (4 * 0) = ee_real_square_zero + 3 * ee_imag_square_zero)
  2. L7
    specialize eisenstein_norm_to_weighted_norm a
  3. L8
    specialize eisenstein_norm_to_weighted_norm b
  4. L9
    specialize eisenstein_norm_to_weighted_norm c
  5. L10
    specialize eisenstein_norm_to_weighted_norm d
  6. L11
    specialize eisenstein_norm_to_weighted_norm 0
  7. L12
    apply eisenstein_norm_to_weighted_norm
  8. L13
    exact hnorm
03Separate the logical casesL14–17

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

  1. L14
    cases hweighted
  2. L15
    cases hweighted_witness
  3. L16
    cases hweighted_witness_witness
  4. L17
    cases hweighted_witness_witness_right
04Establish hsumzeroL18–22

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hsumzero : x + 3 * x1 = 0
  2. L19
    trans 4 * 0
  3. L20
    symm
  4. L21
    exact hweighted_witness_witness_right_right
  5. L22
    norm_num
05Establish hfirstzeroL23–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero left.

  1. L23
    have hfirstzero : x = 0
  2. L24
    specialize add_eq_zero_left x
  3. L25
    specialize add_eq_zero_left (3 * x1)
  4. L26
    apply add_eq_zero_left
  5. L27
    exact hsumzero
06Establish htriplezeroL28–32

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

  1. L28
    have htriplezero : 3 * x1 = 0
  2. L29
    specialize add_eq_zero_right x
  3. L30
    specialize add_eq_zero_right (3 * x1)
  4. L31
    apply add_eq_zero_right
  5. L32
    exact hsumzero
07Establish hsecondzeroL33–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul left cancel nonzero.

  1. L33
    have hsecondzero : x1 = 0
  2. L34
    specialize mul_left_cancel_nonzero 3
  3. L35
    specialize mul_left_cancel_nonzero x1
  4. L36
    specialize mul_left_cancel_nonzero 0
  5. L37
    apply mul_left_cancel_nonzero
  6. L38
    intro hthreezero
  7. L39
    apply PA1
  8. L40
    exact hthreezero
  9. L41
    trans 0
  10. L42
    exact htriplezero
08Calculate and transport equalitiesL43–43

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

  1. L43
    symm
09Use earlier factsL44–44

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

  1. L44
    apply PA5
10Establish himaginaryL45–45

Establish this local claim before using it. It is not an additional assumption.

  1. L45
    have himaginary : c = d
11Establish hsquareiffL46–51

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

  1. L46
    have hsquareiff : (x1 = 0 -> c = d) /\ (c = d -> x1 = 0)
  2. L47
    specialize gaussian_signed_square_zero_iff c
  3. L48
    specialize gaussian_signed_square_zero_iff d
  4. L49
    specialize gaussian_signed_square_zero_iff x1
  5. L50
    apply gaussian_signed_square_zero_iff
  6. L51
    exact hweighted_witness_witness_right_left
12Separate the logical casesL52–52

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

  1. L52
    cases hsquareiff
13Use earlier factsL53–54

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

  1. L53
    apply hsquareiff_left
  2. L54
    exact hsecondzero
14Establish htransformedL55–55

Establish this local claim before using it. It is not an additional assumption.

  1. L55
    have htransformed : ((((2) * (a))) + (d)) = ((((2) * (b))) + (c))
15Establish hsquareiffL56–61

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

  1. L56
    have hsquareiff : (x = 0 -> ((((2) * (a))) + (d)) = ((((2) * (b))) + (c))) /\ (((((2) * (a))) + (d)) = ((((2) * (b))) + (c)) -> x = 0)
  2. L57
    specialize gaussian_signed_square_zero_iff ((((2) * (a))) + (d))
  3. L58
    specialize gaussian_signed_square_zero_iff ((((2) * (b))) + (c))
  4. L59
    specialize gaussian_signed_square_zero_iff x
  5. L60
    apply gaussian_signed_square_zero_iff
  6. L61
    exact hweighted_witness_witness_left
16Separate the logical casesL62–62

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

  1. L62
    cases hsquareiff
17Use earlier factsL63–64

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

  1. L63
    apply hsquareiff_left
  2. L64
    exact hfirstzero
18Separate the logical casesL65–65

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

  1. L65
    split
19Use earlier factsL66–69

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

  1. L66
    specialize mul_left_cancel_nonzero 2
  2. L67
    specialize mul_left_cancel_nonzero a
  3. L68
    specialize mul_left_cancel_nonzero b
  4. L69
    apply mul_left_cancel_nonzero
20Fix variables and assumptionsL70–70

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

  1. L70
    intro htwozero
21Use earlier factsL71–76

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

  1. L71
    apply PA1
  2. L72
    exact htwozero
  3. L73
    specialize add_right_cancel (2 * a)
  4. L74
    specialize add_right_cancel (2 * b)
  5. L75
    specialize add_right_cancel d
  6. L76
    apply add_right_cancel
22Calculate and transport equalitiesL77–77

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

  1. L77
    trans 2 * b + c
23Use earlier factsL78–78

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

  1. L78
    exact htransformed
24Calculate and transport equalitiesL79–80

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

  1. L79
    rewrite himaginary
  2. L80
    refl
25Use earlier factsL81–81

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

  1. L81
    exact himaginary

Library-wide reading audit

Original exact command ledger · 81 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hnorm
  6. 0006have hweighted : exists ee_real_square_zero ee_imag_square_zero. (((((((((2) * (a))) + (d))) * (((((2) * (a))) + (d))))) + (((((((2) * (b))) + (c))) * (((((2) * (b))) + (c)))))) = ((ee_real_square_zero) + (((((((((2) * (a))) + (d))) * (((((2) * (b))) + (c))))) + (((((((2) * (b))) + (c))) * (((((2) * (a))) + (d))))))))) /\ ((((((c) * (c))) + (((d) * (d)))) = ((ee_imag_square_zero) + (((((c) * (d))) + (((d) * (c))))))) /\ (4 * 0) = ee_real_square_zero + 3 * ee_imag_square_zero)
  7. 0007specialize eisenstein_norm_to_weighted_norm a
  8. 0008specialize eisenstein_norm_to_weighted_norm b
  9. 0009specialize eisenstein_norm_to_weighted_norm c
  10. 0010specialize eisenstein_norm_to_weighted_norm d
  11. 0011specialize eisenstein_norm_to_weighted_norm 0
  12. 0012apply eisenstein_norm_to_weighted_norm
  13. 0013exact hnorm
  14. 0014cases hweighted
  15. 0015cases hweighted_witness
  16. 0016cases hweighted_witness_witness
  17. 0017cases hweighted_witness_witness_right
  18. 0018have hsumzero : x + 3 * x1 = 0
  19. 0019trans 4 * 0
  20. 0020symm
  21. 0021exact hweighted_witness_witness_right_right
  22. 0022norm_num
  23. 0023have hfirstzero : x = 0
  24. 0024specialize add_eq_zero_left x
  25. 0025specialize add_eq_zero_left (3 * x1)
  26. 0026apply add_eq_zero_left
  27. 0027exact hsumzero
  28. 0028have htriplezero : 3 * x1 = 0
  29. 0029specialize add_eq_zero_right x
  30. 0030specialize add_eq_zero_right (3 * x1)
  31. 0031apply add_eq_zero_right
  32. 0032exact hsumzero
  33. 0033have hsecondzero : x1 = 0
  34. 0034specialize mul_left_cancel_nonzero 3
  35. 0035specialize mul_left_cancel_nonzero x1
  36. 0036specialize mul_left_cancel_nonzero 0
  37. 0037apply mul_left_cancel_nonzero
  38. 0038intro hthreezero
  39. 0039apply PA1
  40. 0040exact hthreezero
  41. 0041trans 0
  42. 0042exact htriplezero
  43. 0043symm
  44. 0044apply PA5
  45. 0045have himaginary : c = d
  46. 0046have hsquareiff : (x1 = 0 -> c = d) /\ (c = d -> x1 = 0)
  47. 0047specialize gaussian_signed_square_zero_iff c
  48. 0048specialize gaussian_signed_square_zero_iff d
  49. 0049specialize gaussian_signed_square_zero_iff x1
  50. 0050apply gaussian_signed_square_zero_iff
  51. 0051exact hweighted_witness_witness_right_left
  52. 0052cases hsquareiff
  53. 0053apply hsquareiff_left
  54. 0054exact hsecondzero
  55. 0055have htransformed : ((((2) * (a))) + (d)) = ((((2) * (b))) + (c))
  56. 0056have hsquareiff : (x = 0 -> ((((2) * (a))) + (d)) = ((((2) * (b))) + (c))) /\ (((((2) * (a))) + (d)) = ((((2) * (b))) + (c)) -> x = 0)
  57. 0057specialize gaussian_signed_square_zero_iff ((((2) * (a))) + (d))
  58. 0058specialize gaussian_signed_square_zero_iff ((((2) * (b))) + (c))
  59. 0059specialize gaussian_signed_square_zero_iff x
  60. 0060apply gaussian_signed_square_zero_iff
  61. 0061exact hweighted_witness_witness_left
  62. 0062cases hsquareiff
  63. 0063apply hsquareiff_left
  64. 0064exact hfirstzero
  65. 0065split
  66. 0066specialize mul_left_cancel_nonzero 2
  67. 0067specialize mul_left_cancel_nonzero a
  68. 0068specialize mul_left_cancel_nonzero b
  69. 0069apply mul_left_cancel_nonzero
  70. 0070intro htwozero
  71. 0071apply PA1
  72. 0072exact htwozero
  73. 0073specialize add_right_cancel (2 * a)
  74. 0074specialize add_right_cancel (2 * b)
  75. 0075specialize add_right_cancel d
  76. 0076apply add_right_cancel
  77. 0077trans 2 * b + c
  78. 0078exact htransformed
  79. 0079rewrite himaginary
  80. 0080refl
  81. 0081exact himaginary