EI003B

eisenstein_multiply_of_representations

The genuine signed-coordinate Eisenstein product constructs the exact canonical multiplication graph.

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

∀ ac. ∀ bc. ∀ cc. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ZPairRep(ac,a,b,c,d) → ZPairRep(bc,e,f,g,h) → ZPairRep(cc,a · e + b · f + (c · h + d · g),a · f + b · e + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · h + b · g + (c · f + d · e) + (c · g + d · h)) → EMul(ac,bc,cc)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 3EMul(a,b,c) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall ac bc cc a b c d e f g h. (exists ge_representation_real_code_multiply_intro_first ge_representation_imaginary_code_multiply_intro_first. (((ac) = ((ge_representation_real_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first)) * S ((ge_representation_real_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first)) + ((ge_representation_imaginary_code_multiply_intro_first) + (ge_representation_imaginary_code_multiply_intro_first))) /\ ((exists ge_balance_positive_multiply_intro_firstreal ge_balance_negative_multiply_intro_firstreal. (((((ge_representation_real_code_multiply_intro_first) = 2 * (ge_balance_positive_multiply_intro_firstreal) /\ (ge_balance_negative_multiply_intro_firstreal) = 0) \/ exists ge_signed_half_multiply_intro_firstrealdecode. (((ge_representation_real_code_multiply_intro_first) = 2 * ge_signed_half_multiply_intro_firstrealdecode + 1 /\ (ge_balance_positive_multiply_intro_firstreal) = 0) /\ (ge_balance_negative_multiply_intro_firstreal) = S ge_signed_half_multiply_intro_firstrealdecode))) /\ ((a) + ge_balance_negative_multiply_intro_firstreal = (b) + ge_balance_positive_multiply_intro_firstreal))) /\ (exists ge_balance_positive_multiply_intro_firstimaginary ge_balance_negative_multiply_intro_firstimaginary. (((((ge_representation_imaginary_code_multiply_intro_first) = 2 * (ge_balance_positive_multiply_intro_firstimaginary) /\ (ge_balance_negative_multiply_intro_firstimaginary) = 0) \/ exists ge_signed_half_multiply_intro_firstimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_first) = 2 * ge_signed_half_multiply_intro_firstimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_firstimaginary) = 0) /\ (ge_balance_negative_multiply_intro_firstimaginary) = S ge_signed_half_multiply_intro_firstimaginarydecode))) /\ ((c) + ge_balance_negative_multiply_intro_firstimaginary = (d) + ge_balance_positive_multiply_intro_firstimaginary)))))) -> (exists ge_representation_real_code_multiply_intro_second ge_representation_imaginary_code_multiply_intro_second. (((bc) = ((ge_representation_real_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second)) * S ((ge_representation_real_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second)) + ((ge_representation_imaginary_code_multiply_intro_second) + (ge_representation_imaginary_code_multiply_intro_second))) /\ ((exists ge_balance_positive_multiply_intro_secondreal ge_balance_negative_multiply_intro_secondreal. (((((ge_representation_real_code_multiply_intro_second) = 2 * (ge_balance_positive_multiply_intro_secondreal) /\ (ge_balance_negative_multiply_intro_secondreal) = 0) \/ exists ge_signed_half_multiply_intro_secondrealdecode. (((ge_representation_real_code_multiply_intro_second) = 2 * ge_signed_half_multiply_intro_secondrealdecode + 1 /\ (ge_balance_positive_multiply_intro_secondreal) = 0) /\ (ge_balance_negative_multiply_intro_secondreal) = S ge_signed_half_multiply_intro_secondrealdecode))) /\ ((e) + ge_balance_negative_multiply_intro_secondreal = (f) + ge_balance_positive_multiply_intro_secondreal))) /\ (exists ge_balance_positive_multiply_intro_secondimaginary ge_balance_negative_multiply_intro_secondimaginary. (((((ge_representation_imaginary_code_multiply_intro_second) = 2 * (ge_balance_positive_multiply_intro_secondimaginary) /\ (ge_balance_negative_multiply_intro_secondimaginary) = 0) \/ exists ge_signed_half_multiply_intro_secondimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_second) = 2 * ge_signed_half_multiply_intro_secondimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_secondimaginary) = 0) /\ (ge_balance_negative_multiply_intro_secondimaginary) = S ge_signed_half_multiply_intro_secondimaginarydecode))) /\ ((g) + ge_balance_negative_multiply_intro_secondimaginary = (h) + ge_balance_positive_multiply_intro_secondimaginary)))))) -> (exists ge_representation_real_code_multiply_intro_output ge_representation_imaginary_code_multiply_intro_output. (((cc) = ((ge_representation_real_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output)) * S ((ge_representation_real_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output)) + ((ge_representation_imaginary_code_multiply_intro_output) + (ge_representation_imaginary_code_multiply_intro_output))) /\ ((exists ge_balance_positive_multiply_intro_outputreal ge_balance_negative_multiply_intro_outputreal. (((((ge_representation_real_code_multiply_intro_output) = 2 * (ge_balance_positive_multiply_intro_outputreal) /\ (ge_balance_negative_multiply_intro_outputreal) = 0) \/ exists ge_signed_half_multiply_intro_outputrealdecode. (((ge_representation_real_code_multiply_intro_output) = 2 * ge_signed_half_multiply_intro_outputrealdecode + 1 /\ (ge_balance_positive_multiply_intro_outputreal) = 0) /\ (ge_balance_negative_multiply_intro_outputreal) = S ge_signed_half_multiply_intro_outputrealdecode))) /\ ((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_intro_outputreal = (((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_intro_outputreal))) /\ (exists ge_balance_positive_multiply_intro_outputimaginary ge_balance_negative_multiply_intro_outputimaginary. (((((ge_representation_imaginary_code_multiply_intro_output) = 2 * (ge_balance_positive_multiply_intro_outputimaginary) /\ (ge_balance_negative_multiply_intro_outputimaginary) = 0) \/ exists ge_signed_half_multiply_intro_outputimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_output) = 2 * ge_signed_half_multiply_intro_outputimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_outputimaginary) = 0) /\ (ge_balance_negative_multiply_intro_outputimaginary) = S ge_signed_half_multiply_intro_outputimaginarydecode))) /\ ((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) + (((((c) * (h))) + (((d) * (g))))))) + ge_balance_negative_multiply_intro_outputimaginary = (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) + (((((c) * (g))) + (((d) * (h))))))) + ge_balance_positive_multiply_intro_outputimaginary)))))) -> (exists ee_first_rp_multiply_intro_graph ee_first_rn_multiply_intro_graph ee_first_ip_multiply_intro_graph ee_first_in_multiply_intro_graph ee_second_rp_multiply_intro_graph ee_second_rn_multiply_intro_graph ee_second_ip_multiply_intro_graph ee_second_in_multiply_intro_graph. ((exists ge_representation_real_code_multiply_intro_graphfirst ge_representation_imaginary_code_multiply_intro_graphfirst. (((ac) = ((ge_representation_real_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst)) * S ((ge_representation_real_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst)) + ((ge_representation_imaginary_code_multiply_intro_graphfirst) + (ge_representation_imaginary_code_multiply_intro_graphfirst))) /\ ((exists ge_balance_positive_multiply_intro_graphfirstreal ge_balance_negative_multiply_intro_graphfirstreal. (((((ge_representation_real_code_multiply_intro_graphfirst) = 2 * (ge_balance_positive_multiply_intro_graphfirstreal) /\ (ge_balance_negative_multiply_intro_graphfirstreal) = 0) \/ exists ge_signed_half_multiply_intro_graphfirstrealdecode. (((ge_representation_real_code_multiply_intro_graphfirst) = 2 * ge_signed_half_multiply_intro_graphfirstrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphfirstreal) = 0) /\ (ge_balance_negative_multiply_intro_graphfirstreal) = S ge_signed_half_multiply_intro_graphfirstrealdecode))) /\ ((ee_first_rp_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphfirstreal = (ee_first_rn_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphfirstreal))) /\ (exists ge_balance_positive_multiply_intro_graphfirstimaginary ge_balance_negative_multiply_intro_graphfirstimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphfirst) = 2 * (ge_balance_positive_multiply_intro_graphfirstimaginary) /\ (ge_balance_negative_multiply_intro_graphfirstimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphfirst) = 2 * ge_signed_half_multiply_intro_graphfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphfirstimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphfirstimaginary) = S ge_signed_half_multiply_intro_graphfirstimaginarydecode))) /\ ((ee_first_ip_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphfirstimaginary = (ee_first_in_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_intro_graphsecond ge_representation_imaginary_code_multiply_intro_graphsecond. (((bc) = ((ge_representation_real_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond)) * S ((ge_representation_real_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond)) + ((ge_representation_imaginary_code_multiply_intro_graphsecond) + (ge_representation_imaginary_code_multiply_intro_graphsecond))) /\ ((exists ge_balance_positive_multiply_intro_graphsecondreal ge_balance_negative_multiply_intro_graphsecondreal. (((((ge_representation_real_code_multiply_intro_graphsecond) = 2 * (ge_balance_positive_multiply_intro_graphsecondreal) /\ (ge_balance_negative_multiply_intro_graphsecondreal) = 0) \/ exists ge_signed_half_multiply_intro_graphsecondrealdecode. (((ge_representation_real_code_multiply_intro_graphsecond) = 2 * ge_signed_half_multiply_intro_graphsecondrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphsecondreal) = 0) /\ (ge_balance_negative_multiply_intro_graphsecondreal) = S ge_signed_half_multiply_intro_graphsecondrealdecode))) /\ ((ee_second_rp_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphsecondreal = (ee_second_rn_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphsecondreal))) /\ (exists ge_balance_positive_multiply_intro_graphsecondimaginary ge_balance_negative_multiply_intro_graphsecondimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphsecond) = 2 * (ge_balance_positive_multiply_intro_graphsecondimaginary) /\ (ge_balance_negative_multiply_intro_graphsecondimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphsecond) = 2 * ge_signed_half_multiply_intro_graphsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphsecondimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphsecondimaginary) = S ge_signed_half_multiply_intro_graphsecondimaginarydecode))) /\ ((ee_second_ip_multiply_intro_graph) + ge_balance_negative_multiply_intro_graphsecondimaginary = (ee_second_in_multiply_intro_graph) + ge_balance_positive_multiply_intro_graphsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_intro_graphoutput ge_representation_imaginary_code_multiply_intro_graphoutput. (((cc) = ((ge_representation_real_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput)) * S ((ge_representation_real_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput)) + ((ge_representation_imaginary_code_multiply_intro_graphoutput) + (ge_representation_imaginary_code_multiply_intro_graphoutput))) /\ ((exists ge_balance_positive_multiply_intro_graphoutputreal ge_balance_negative_multiply_intro_graphoutputreal. (((((ge_representation_real_code_multiply_intro_graphoutput) = 2 * (ge_balance_positive_multiply_intro_graphoutputreal) /\ (ge_balance_negative_multiply_intro_graphoutputreal) = 0) \/ exists ge_signed_half_multiply_intro_graphoutputrealdecode. (((ge_representation_real_code_multiply_intro_graphoutput) = 2 * ge_signed_half_multiply_intro_graphoutputrealdecode + 1 /\ (ge_balance_positive_multiply_intro_graphoutputreal) = 0) /\ (ge_balance_negative_multiply_intro_graphoutputreal) = S ge_signed_half_multiply_intro_graphoutputrealdecode))) /\ ((((((((ee_first_rp_multiply_intro_graph) * (ee_second_rp_multiply_intro_graph))) + (((ee_first_rn_multiply_intro_graph) * (ee_second_rn_multiply_intro_graph))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))))))) + ge_balance_negative_multiply_intro_graphoutputreal = (((((((ee_first_rp_multiply_intro_graph) * (ee_second_rn_multiply_intro_graph))) + (((ee_first_rn_multiply_intro_graph) * (ee_second_rp_multiply_intro_graph))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))))))) + ge_balance_positive_multiply_intro_graphoutputreal))) /\ (exists ge_balance_positive_multiply_intro_graphoutputimaginary ge_balance_negative_multiply_intro_graphoutputimaginary. (((((ge_representation_imaginary_code_multiply_intro_graphoutput) = 2 * (ge_balance_positive_multiply_intro_graphoutputimaginary) /\ (ge_balance_negative_multiply_intro_graphoutputimaginary) = 0) \/ exists ge_signed_half_multiply_intro_graphoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_intro_graphoutput) = 2 * ge_signed_half_multiply_intro_graphoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_intro_graphoutputimaginary) = 0) /\ (ge_balance_negative_multiply_intro_graphoutputimaginary) = S ge_signed_half_multiply_intro_graphoutputimaginarydecode))) /\ ((((((((((ee_first_rp_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))) + (((ee_first_rn_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_rp_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_rn_multiply_intro_graph))))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))))))) + ge_balance_negative_multiply_intro_graphoutputimaginary = (((((((((ee_first_rp_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))) + (((ee_first_rn_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_rn_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_rp_multiply_intro_graph))))))) + (((((ee_first_ip_multiply_intro_graph) * (ee_second_ip_multiply_intro_graph))) + (((ee_first_in_multiply_intro_graph) * (ee_second_in_multiply_intro_graph))))))) + ge_balance_positive_multiply_intro_graphoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

27 script commands · 7 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 ac
  2. L2
    intro bc
  3. L3
    intro cc
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro d
  8. L8
    intro e
  9. L9
    intro f
  10. L10
    intro g
02Fix variables and assumptionsL11–14

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

  1. L11
    intro h
  2. L12
    intro hfirst
  3. L13
    intro hsecond
  4. L14
    intro houtput
03Construct an explicit witnessL15–22

Supply the displayed value, then prove that it has the required property.

  1. L15
    exists a
  2. L16
    exists b
  3. L17
    exists c
  4. L18
    exists d
  5. L19
    exists e
  6. L20
    exists f
  7. L21
    exists g
  8. L22
    exists h
04Separate the logical casesL23–23

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

  1. L23
    split
05Use earlier factsL24–24

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

  1. L24
    exact hfirst
06Separate the logical casesL25–25

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

  1. L25
    split
07Use earlier factsL26–27

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

  1. L26
    exact hsecond
  2. L27
    exact houtput

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro cc
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro d
  8. 0008intro e
  9. 0009intro f
  10. 0010intro g
  11. 0011intro h
  12. 0012intro hfirst
  13. 0013intro hsecond
  14. 0014intro houtput
  15. 0015exists a
  16. 0016exists b
  17. 0017exists c
  18. 0018exists d
  19. 0019exists e
  20. 0020exists f
  21. 0021exists g
  22. 0022exists h
  23. 0023split
  24. 0024exact hfirst
  25. 0025split
  26. 0026exact hsecond
  27. 0027exact houtput