EI0019

eisenstein_real_associate_left_positive

The left associated Eisenstein real positive contribution is the checked Gaussian contribution plus the actual triple-imaginary contribution.

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. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ∀ i. ∀ j. ∀ k. ∀ l. (a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f) + (c · h + d · g)) · l + (a · h + b · g + (c · f + d · e) + (c · g + d · h)) · k) = (a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f)) · l + (a · h + b · g + (c · f + d · e)) · k) + ((c · g + d · h) · k + (c · h + d · g) · l)

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

Definition DAG

none

Actual proof prerequisites

add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisite
Original expanded first-order statement 
forall a b c d e f g h i j k l. ((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (l))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (k)))))) = ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (l))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (k))))))) + (((((((((c) * (g))) + (((d) * (h))))) * (k))) + (((((((c) * (h))) + (((d) * (g))))) * (l))))))

Complete tactic proof in conservative notation

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

90 script commands · 18 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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–12

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

  1. L11
    intro k
  2. L12
    intro l
03Calculate and transport equalitiesL13–22

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

  1. L13
    trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  2. L14
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L15
    trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + ((((d) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + (((d) * (((g) * (l))))))))))))))))))))))))
  4. L16
    congr
  5. L17
    refl
  6. L18
    congr
  7. L19
    refl
  8. L20
    congr
  9. L21
    refl
  10. L22
    congr
04Calculate and transport equalitiesL23–32

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

  1. L23
    refl
  2. L24
    congr
  3. L25
    refl
  4. L26
    congr
  5. L27
    refl
  6. L28
    congr
  7. L29
    refl
  8. L30
    congr
  9. L31
    refl
  10. L32
    congr
05Calculate and transport equalitiesL33–42

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

  1. L33
    refl
  2. L34
    congr
  3. L35
    refl
  4. L36
    congr
  5. L37
    refl
  6. L38
    congr
  7. L39
    refl
  8. L40
    trans ((((a) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))
  9. L41
    trans ((((c) * (((h) * (l))))) + ((((a) * (((h) * (k))))) + ((((d) * (((g) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))
  10. L42
    congr
06Calculate and transport equalitiesL43–43

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

  1. L43
    refl
07Use earlier factsL44–45

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

  1. L44
    apply four_square_add_swap_right_tail
  2. L45
    apply four_square_add_swap_right_tail
08Calculate and transport equalitiesL46–51

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

  1. L46
    congr
  2. L47
    refl
  3. L48
    trans ((((b) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))))
  4. L49
    trans ((((c) * (((h) * (l))))) + ((((b) * (((g) * (k))))) + ((((d) * (((g) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))))
  5. L50
    congr
  6. L51
    refl
09Use earlier factsL52–53

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

  1. L52
    apply four_square_add_swap_right_tail
  2. L53
    apply four_square_add_swap_right_tail
10Calculate and transport equalitiesL54–59

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

  1. L54
    congr
  2. L55
    refl
  3. L56
    trans ((((c) * (((f) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))
  4. L57
    trans ((((c) * (((h) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((g) * (l))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))
  5. L58
    congr
  6. L59
    refl
11Use earlier factsL60–61

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

  1. L60
    apply four_square_add_swap_right_tail
  2. L61
    apply four_square_add_swap_right_tail
12Calculate and transport equalitiesL62–67

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

  1. L62
    congr
  2. L63
    refl
  3. L64
    trans ((((d) * (((e) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))
  4. L65
    trans ((((c) * (((h) * (l))))) + ((((d) * (((e) * (k))))) + ((((d) * (((g) * (l))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))
  5. L66
    congr
  6. L67
    refl
13Use earlier factsL68–69

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

  1. L68
    apply four_square_add_swap_right_tail
  2. L69
    apply four_square_add_swap_right_tail
14Calculate and transport equalitiesL70–75

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

  1. L70
    congr
  2. L71
    refl
  3. L72
    trans ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))
  4. L73
    trans ((((c) * (((h) * (l))))) + ((((c) * (((g) * (k))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))
  5. L74
    congr
  6. L75
    refl
15Use earlier factsL76–77

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

  1. L76
    apply four_square_add_swap_right_tail
  2. L77
    apply four_square_add_swap_right_tail
16Calculate and transport equalitiesL78–83

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

  1. L78
    congr
  2. L79
    refl
  3. L80
    trans ((((d) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + (((d) * (((g) * (l)))))))
  4. L81
    trans ((((c) * (((h) * (l))))) + ((((d) * (((h) * (k))))) + (((d) * (((g) * (l)))))))
  5. L82
    congr
  6. L83
    refl
17Use earlier factsL84–85

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

  1. L84
    apply add_comm
  2. L85
    apply four_square_add_swap_right_tail
18Calculate and transport equalitiesL86–90

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

  1. L86
    congr
  2. L87
    refl
  3. L88
    refl
  4. L89
    symm
  5. L90
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original defined command ledger · 90 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. 0013trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  14. 0014simp [add_mul, mul_add, mul_assoc, add_assoc]
  15. 0015trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + ((((d) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + (((d) * (((g) * (l))))))))))))))))))))))))
  16. 0016congr
  17. 0017refl
  18. 0018congr
  19. 0019refl
  20. 0020congr
  21. 0021refl
  22. 0022congr
  23. 0023refl
  24. 0024congr
  25. 0025refl
  26. 0026congr
  27. 0027refl
  28. 0028congr
  29. 0029refl
  30. 0030congr
  31. 0031refl
  32. 0032congr
  33. 0033refl
  34. 0034congr
  35. 0035refl
  36. 0036congr
  37. 0037refl
  38. 0038congr
  39. 0039refl
  40. 0040trans ((((a) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))
  41. 0041trans ((((c) * (((h) * (l))))) + ((((a) * (((h) * (k))))) + ((((d) * (((g) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))))
  42. 0042congr
  43. 0043refl
  44. 0044apply four_square_add_swap_right_tail
  45. 0045apply four_square_add_swap_right_tail
  46. 0046congr
  47. 0047refl
  48. 0048trans ((((b) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))))
  49. 0049trans ((((c) * (((h) * (l))))) + ((((b) * (((g) * (k))))) + ((((d) * (((g) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))))
  50. 0050congr
  51. 0051refl
  52. 0052apply four_square_add_swap_right_tail
  53. 0053apply four_square_add_swap_right_tail
  54. 0054congr
  55. 0055refl
  56. 0056trans ((((c) * (((f) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))
  57. 0057trans ((((c) * (((h) * (l))))) + ((((c) * (((f) * (k))))) + ((((d) * (((g) * (l))))) + ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k))))))))))
  58. 0058congr
  59. 0059refl
  60. 0060apply four_square_add_swap_right_tail
  61. 0061apply four_square_add_swap_right_tail
  62. 0062congr
  63. 0063refl
  64. 0064trans ((((d) * (((e) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))
  65. 0065trans ((((c) * (((h) * (l))))) + ((((d) * (((e) * (k))))) + ((((d) * (((g) * (l))))) + ((((c) * (((g) * (k))))) + (((d) * (((h) * (k)))))))))
  66. 0066congr
  67. 0067refl
  68. 0068apply four_square_add_swap_right_tail
  69. 0069apply four_square_add_swap_right_tail
  70. 0070congr
  71. 0071refl
  72. 0072trans ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))
  73. 0073trans ((((c) * (((h) * (l))))) + ((((c) * (((g) * (k))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))
  74. 0074congr
  75. 0075refl
  76. 0076apply four_square_add_swap_right_tail
  77. 0077apply four_square_add_swap_right_tail
  78. 0078congr
  79. 0079refl
  80. 0080trans ((((d) * (((h) * (k))))) + ((((c) * (((h) * (l))))) + (((d) * (((g) * (l)))))))
  81. 0081trans ((((c) * (((h) * (l))))) + ((((d) * (((h) * (k))))) + (((d) * (((g) * (l)))))))
  82. 0082congr
  83. 0083refl
  84. 0084apply add_comm
  85. 0085apply four_square_add_swap_right_tail
  86. 0086congr
  87. 0087refl
  88. 0088refl
  89. 0089symm
  90. 0090simp [add_mul, mul_add, mul_assoc, add_assoc]