EI0004

eisenstein_natural_norm_zero

A zero Eisenstein norm forces both natural coordinates to vanish, including the diagonal boundary.

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.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. a · a + b · b = a · b + 0 → a = 0 ∧ b = 0

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

Definition DAG

none

Actual proof prerequisites

le_total · checked external prerequisiteeisenstein_natural_norm_gap_valueeisenstein_natural_norm_symmetricadd_comm · checked external prerequisitezero_add · checked external prerequisiteadd_eq_zero_left · checked external prerequisiteadd_eq_zero_right · checked external prerequisitesquare_zero_root · checked external prerequisite
Original expanded first-order statement 
forall a b. ((((a) * (a)) + ((b) * (b))) = (((a) * (b)) + (0))) -> a = 0 /\ b = 0

Complete tactic proof in conservative notation

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

98 script commands · 21 reading checkpoints · 13 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 (2)
eisenstein natural norm gap valueeisenstein natural norm symmetric
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hnorm
02Use earlier factsL4–5

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

  1. L4
    specialize le_total a
  2. L5
    specialize le_total b
03Separate the logical casesL6–7

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

  1. L6
    cases le_total
  2. L7
    cases le_total_left
04Establish hlargeL8–12

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

  1. L8
    have hlarge : b = a + x
  2. L9
    trans x + a
  3. L10
    symm
  4. L11
    exact le_total_left_witness
  5. L12
    apply add_comm
05Establish hvalueL13–21

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

  1. L13
    have hvalue : 0 = a * a + a * x + x * x
  2. L14
    specialize eisenstein_natural_norm_gap_value a
  3. L15
    specialize eisenstein_natural_norm_gap_value x
  4. L16
    specialize eisenstein_natural_norm_gap_value 0
  5. L17
    apply eisenstein_natural_norm_gap_value
  6. L18
    rewrite <- hlarge
  7. L19
    rewrite <- hlarge
  8. L20
    rewrite <- hlarge
  9. L21
    exact hnorm
06Establish hfirstL22–27

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

  1. L22
    have hfirst : a * a + a * x = 0
  2. L23
    specialize add_eq_zero_left (a * a + a * x)
  3. L24
    specialize add_eq_zero_left (x * x)
  4. L25
    apply add_eq_zero_left
  5. L26
    symm
  6. L27
    exact hvalue
07Establish hsmallzeroL28–34

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

  1. L28
    have hsmallzero : a = 0
  2. L29
    specialize square_zero_root a
  3. L30
    apply square_zero_root
  4. L31
    specialize add_eq_zero_left (a * a)
  5. L32
    specialize add_eq_zero_left (a * x)
  6. L33
    apply add_eq_zero_left
  7. L34
    exact hfirst
08Establish hgapzeroL35–42

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

  1. L35
    have hgapzero : x = 0
  2. L36
    specialize square_zero_root x
  3. L37
    apply square_zero_root
  4. L38
    specialize add_eq_zero_right (a * a + a * x)
  5. L39
    specialize add_eq_zero_right (x * x)
  6. L40
    apply add_eq_zero_right
  7. L41
    symm
  8. L42
    exact hvalue
09Establish hlargezeroL43–46

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

  1. L43
    have hlargezero : b = 0
  2. L44
    trans a + x
  3. L45
    exact hlarge
  4. L46
    simp [hsmallzero, hgapzero, zero_add]
10Separate the logical casesL47–47

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

  1. L47
    split
11Use earlier factsL48–49

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

  1. L48
    exact hsmallzero
  2. L49
    exact hlargezero
12Establish hreverseL50–55

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

  1. L50
    have hreverse : (((b) * (b)) + ((a) * (a))) = (((b) * (a)) + (0))
  2. L51
    specialize eisenstein_natural_norm_symmetric a
  3. L52
    specialize eisenstein_natural_norm_symmetric b
  4. L53
    specialize eisenstein_natural_norm_symmetric 0
  5. L54
    apply eisenstein_natural_norm_symmetric
  6. L55
    exact hnorm
13Separate the logical casesL56–56

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

  1. L56
    cases le_total_right
14Establish hlargeL57–61

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

  1. L57
    have hlarge : a = b + x
  2. L58
    trans x + b
  3. L59
    symm
  4. L60
    exact le_total_right_witness
  5. L61
    apply add_comm
15Establish hvalueL62–70

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

  1. L62
    have hvalue : 0 = b * b + b * x + x * x
  2. L63
    specialize eisenstein_natural_norm_gap_value b
  3. L64
    specialize eisenstein_natural_norm_gap_value x
  4. L65
    specialize eisenstein_natural_norm_gap_value 0
  5. L66
    apply eisenstein_natural_norm_gap_value
  6. L67
    rewrite <- hlarge
  7. L68
    rewrite <- hlarge
  8. L69
    rewrite <- hlarge
  9. L70
    exact hreverse
16Establish hfirstL71–76

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

  1. L71
    have hfirst : b * b + b * x = 0
  2. L72
    specialize add_eq_zero_left (b * b + b * x)
  3. L73
    specialize add_eq_zero_left (x * x)
  4. L74
    apply add_eq_zero_left
  5. L75
    symm
  6. L76
    exact hvalue
17Establish hsmallzeroL77–83

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

  1. L77
    have hsmallzero : b = 0
  2. L78
    specialize square_zero_root b
  3. L79
    apply square_zero_root
  4. L80
    specialize add_eq_zero_left (b * b)
  5. L81
    specialize add_eq_zero_left (b * x)
  6. L82
    apply add_eq_zero_left
  7. L83
    exact hfirst
18Establish hgapzeroL84–91

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

  1. L84
    have hgapzero : x = 0
  2. L85
    specialize square_zero_root x
  3. L86
    apply square_zero_root
  4. L87
    specialize add_eq_zero_right (b * b + b * x)
  5. L88
    specialize add_eq_zero_right (x * x)
  6. L89
    apply add_eq_zero_right
  7. L90
    symm
  8. L91
    exact hvalue
19Establish hlargezeroL92–95

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

  1. L92
    have hlargezero : a = 0
  2. L93
    trans b + x
  3. L94
    exact hlarge
  4. L95
    simp [hsmallzero, hgapzero, zero_add]
20Separate the logical casesL96–96

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

  1. L96
    split
21Use earlier factsL97–98

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

  1. L97
    exact hlargezero
  2. L98
    exact hsmallzero

Library-wide reading audit

Original defined command ledger · 98 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hnorm
  4. 0004specialize le_total a
  5. 0005specialize le_total b
  6. 0006cases le_total
  7. 0007cases le_total_left
  8. 0008have hlarge : b = a + x
  9. 0009trans x + a
  10. 0010symm
  11. 0011exact le_total_left_witness
  12. 0012apply add_comm
  13. 0013have hvalue : 0 = a * a + a * x + x * x
  14. 0014specialize eisenstein_natural_norm_gap_value a
  15. 0015specialize eisenstein_natural_norm_gap_value x
  16. 0016specialize eisenstein_natural_norm_gap_value 0
  17. 0017apply eisenstein_natural_norm_gap_value
  18. 0018rewrite <- hlarge
  19. 0019rewrite <- hlarge
  20. 0020rewrite <- hlarge
  21. 0021exact hnorm
  22. 0022have hfirst : a * a + a * x = 0
  23. 0023specialize add_eq_zero_left (a * a + a * x)
  24. 0024specialize add_eq_zero_left (x * x)
  25. 0025apply add_eq_zero_left
  26. 0026symm
  27. 0027exact hvalue
  28. 0028have hsmallzero : a = 0
  29. 0029specialize square_zero_root a
  30. 0030apply square_zero_root
  31. 0031specialize add_eq_zero_left (a * a)
  32. 0032specialize add_eq_zero_left (a * x)
  33. 0033apply add_eq_zero_left
  34. 0034exact hfirst
  35. 0035have hgapzero : x = 0
  36. 0036specialize square_zero_root x
  37. 0037apply square_zero_root
  38. 0038specialize add_eq_zero_right (a * a + a * x)
  39. 0039specialize add_eq_zero_right (x * x)
  40. 0040apply add_eq_zero_right
  41. 0041symm
  42. 0042exact hvalue
  43. 0043have hlargezero : b = 0
  44. 0044trans a + x
  45. 0045exact hlarge
  46. 0046simp [hsmallzero, hgapzero, zero_add]
  47. 0047split
  48. 0048exact hsmallzero
  49. 0049exact hlargezero
  50. 0050have hreverse : (((b) * (b)) + ((a) * (a))) = (((b) * (a)) + (0))
  51. 0051specialize eisenstein_natural_norm_symmetric a
  52. 0052specialize eisenstein_natural_norm_symmetric b
  53. 0053specialize eisenstein_natural_norm_symmetric 0
  54. 0054apply eisenstein_natural_norm_symmetric
  55. 0055exact hnorm
  56. 0056cases le_total_right
  57. 0057have hlarge : a = b + x
  58. 0058trans x + b
  59. 0059symm
  60. 0060exact le_total_right_witness
  61. 0061apply add_comm
  62. 0062have hvalue : 0 = b * b + b * x + x * x
  63. 0063specialize eisenstein_natural_norm_gap_value b
  64. 0064specialize eisenstein_natural_norm_gap_value x
  65. 0065specialize eisenstein_natural_norm_gap_value 0
  66. 0066apply eisenstein_natural_norm_gap_value
  67. 0067rewrite <- hlarge
  68. 0068rewrite <- hlarge
  69. 0069rewrite <- hlarge
  70. 0070exact hreverse
  71. 0071have hfirst : b * b + b * x = 0
  72. 0072specialize add_eq_zero_left (b * b + b * x)
  73. 0073specialize add_eq_zero_left (x * x)
  74. 0074apply add_eq_zero_left
  75. 0075symm
  76. 0076exact hvalue
  77. 0077have hsmallzero : b = 0
  78. 0078specialize square_zero_root b
  79. 0079apply square_zero_root
  80. 0080specialize add_eq_zero_left (b * b)
  81. 0081specialize add_eq_zero_left (b * x)
  82. 0082apply add_eq_zero_left
  83. 0083exact hfirst
  84. 0084have hgapzero : x = 0
  85. 0085specialize square_zero_root x
  86. 0086apply square_zero_root
  87. 0087specialize add_eq_zero_right (b * b + b * x)
  88. 0088specialize add_eq_zero_right (x * x)
  89. 0089apply add_eq_zero_right
  90. 0090symm
  91. 0091exact hvalue
  92. 0092have hlargezero : a = 0
  93. 0093trans b + x
  94. 0094exact hlarge
  95. 0095simp [hsmallzero, hgapzero, zero_add]
  96. 0096split
  97. 0097exact hlargezero
  98. 0098exact hsmallzero