EI001B

eisenstein_real_associate_right_positive

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

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

Complete tactic proof in conservative notation

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

74 script commands · 14 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))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  2. L14
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L15
    trans ((((a) * (((e) * (i))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  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 ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))
  9. L41
    trans ((((c) * (((g) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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 ((((d) * (((f) * (l))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k)))))))))))
  4. L49
    trans ((((c) * (((g) * (k))))) + ((((d) * (((f) * (l))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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 ((((d) * (((g) * (i))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))
  4. L57
    trans ((((c) * (((g) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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) * (((h) * (j))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k)))))))))
  4. L65
    trans ((((c) * (((g) * (k))))) + ((((d) * (((h) * (j))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((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–74

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
    refl
  4. L73
    symm
  5. L74
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original defined command ledger · 74 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))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  14. 0014simp [add_mul, mul_add, mul_assoc, add_assoc]
  15. 0015trans ((((a) * (((e) * (i))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))))))))))))))
  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 ((((d) * (((e) * (k))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))))
  41. 0041trans ((((c) * (((g) * (k))))) + ((((d) * (((e) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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 ((((d) * (((f) * (l))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k)))))))))))
  49. 0049trans ((((c) * (((g) * (k))))) + ((((d) * (((f) * (l))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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 ((((d) * (((g) * (i))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k))))))))))
  57. 0057trans ((((c) * (((g) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((g) * (l))))) + (((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) * (((h) * (j))))) + ((((c) * (((g) * (k))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((d) * (((h) * (k)))))))))
  65. 0065trans ((((c) * (((g) * (k))))) + ((((d) * (((h) * (j))))) + ((((c) * (((h) * (l))))) + ((((d) * (((g) * (l))))) + (((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. 0072refl
  73. 0073symm
  74. 0074simp [add_mul, mul_add, mul_assoc, add_assoc]