EI001D

eisenstein_product_associate_real

Real Eisenstein associativity follows from checked Gaussian real associativity and associative scalar triple products, with all natural contribution equations explicit.

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

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

Definition DAG

none

Actual proof prerequisites

eisenstein_real_associate_left_positiveeisenstein_real_associate_left_negativeeisenstein_real_associate_right_positiveeisenstein_real_associate_right_negativesigned_pair_mul_components_associate · checked external prerequisitegaussian_product_associate_real_positive · checked external prerequisitegaussian_product_associate_real_negative · 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) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((d) * (((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (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))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))) + (((((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) * (k))) + (((((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) * (l))))))))

Complete tactic proof in conservative notation

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

39 script commands · 16 reading checkpoints · 1 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 (4)
eisenstein real associate left positiveeisenstein real associate right positiveeisenstein real associate left negativeeisenstein real associate right negative
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
03Establish htailL13–20

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply signed pair mul components associate.

  1. L13
    have htail : (((((((((c) * (g))) + (((d) * (h))))) * (k))) + (((((((c) * (h))) + (((d) * (g))))) * (l)))) = ((((c) * (((((g) * (k))) + (((h) * (l))))))) + (((d) * (((((g) * (l))) + (((h) * (k))))))))) /\ (((((((((c) * (g))) + (((d) * (h))))) * (l))) + (((((((c) * (h))) + (((d) * (g))))) * (k)))) = ((((c) * (((((g) * (l))) + (((h) * (k))))))) + (((d) * (((((g) * (k))) + (((h) * (l)))))))))
  2. L14
    specialize signed_pair_mul_components_associate c
  3. L15
    specialize signed_pair_mul_components_associate d
  4. L16
    specialize signed_pair_mul_components_associate g
  5. L17
    specialize signed_pair_mul_components_associate h
  6. L18
    specialize signed_pair_mul_components_associate k
  7. L19
    specialize signed_pair_mul_components_associate l
  8. L20
    apply signed_pair_mul_components_associate
04Separate the logical casesL21–21

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

  1. L21
    cases htail
05Calculate and transport equalitiesL22–23

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

  1. L22
    congr
  2. L23
    trans ((((((((((((((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))))))
06Use earlier factsL24–24

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

  1. L24
    apply eisenstein_real_associate_left_positive
07Calculate and transport equalitiesL25–26

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

  1. L25
    trans ((((((((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))))))))))
  2. L26
    congr
08Use earlier factsL27–28

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

  1. L27
    apply gaussian_product_associate_real_positive
  2. L28
    exact htail_left
09Calculate and transport equalitiesL29–29

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

  1. L29
    symm
10Use earlier factsL30–30

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

  1. L30
    apply eisenstein_real_associate_right_positive
11Calculate and transport equalitiesL31–32

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

  1. L31
    symm
  2. L32
    trans ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (k))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (l))))))) + (((((((((c) * (g))) + (((d) * (h))))) * (l))) + (((((((c) * (h))) + (((d) * (g))))) * (k))))))
12Use earlier factsL33–33

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

  1. L33
    apply eisenstein_real_associate_left_negative
13Calculate and transport equalitiesL34–35

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

  1. L34
    trans ((((((((a) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((d) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))) + (((((c) * (((((g) * (l))) + (((h) * (k))))))) + (((d) * (((((g) * (k))) + (((h) * (l))))))))))
  2. L35
    congr
14Use earlier factsL36–37

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

  1. L36
    apply gaussian_product_associate_real_negative
  2. L37
    exact htail_right
15Calculate and transport equalitiesL38–38

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

  1. L38
    symm
16Use earlier factsL39–39

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

  1. L39
    apply eisenstein_real_associate_right_negative

Library-wide reading audit

Original defined command ledger · 39 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. 0013have htail : (((((((((c) * (g))) + (((d) * (h))))) * (k))) + (((((((c) * (h))) + (((d) * (g))))) * (l)))) = ((((c) * (((((g) * (k))) + (((h) * (l))))))) + (((d) * (((((g) * (l))) + (((h) * (k))))))))) /\ (((((((((c) * (g))) + (((d) * (h))))) * (l))) + (((((((c) * (h))) + (((d) * (g))))) * (k)))) = ((((c) * (((((g) * (l))) + (((h) * (k))))))) + (((d) * (((((g) * (k))) + (((h) * (l)))))))))
  14. 0014specialize signed_pair_mul_components_associate c
  15. 0015specialize signed_pair_mul_components_associate d
  16. 0016specialize signed_pair_mul_components_associate g
  17. 0017specialize signed_pair_mul_components_associate h
  18. 0018specialize signed_pair_mul_components_associate k
  19. 0019specialize signed_pair_mul_components_associate l
  20. 0020apply signed_pair_mul_components_associate
  21. 0021cases htail
  22. 0022congr
  23. 0023trans ((((((((((((((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))))))
  24. 0024apply eisenstein_real_associate_left_positive
  25. 0025trans ((((((((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))))))))))
  26. 0026congr
  27. 0027apply gaussian_product_associate_real_positive
  28. 0028exact htail_left
  29. 0029symm
  30. 0030apply eisenstein_real_associate_right_positive
  31. 0031symm
  32. 0032trans ((((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (j))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (i))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (k))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (l))))))) + (((((((((c) * (g))) + (((d) * (h))))) * (l))) + (((((((c) * (h))) + (((d) * (g))))) * (k))))))
  33. 0033apply eisenstein_real_associate_left_negative
  34. 0034trans ((((((((a) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))) + (((b) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))))) + (((((c) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))) + (((d) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))))))) + (((((c) * (((((g) * (l))) + (((h) * (k))))))) + (((d) * (((((g) * (k))) + (((h) * (l))))))))))
  35. 0035congr
  36. 0036apply gaussian_product_associate_real_negative
  37. 0037exact htail_right
  38. 0038symm
  39. 0039apply eisenstein_real_associate_right_negative