EI003D

eisenstein_multiply_exists

Construct the actual canonical Eisenstein product of every two valid signed-coordinate codes.

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. ZPairValid(ac) → ZPairValid(bc) → ∃ x. EMul(ac,bc,x)

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

Definition DAG

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

Actual proof prerequisites

gaussian_representation_exists · checked external prerequisiteeisenstein_multiply_of_representationsgaussian_decode_representation · checked external prerequisite
Original expanded first-order statement 
forall ac bc. (exists ge_real_positive_multiply_total_first ge_real_negative_multiply_total_first ge_imaginary_positive_multiply_total_first ge_imaginary_negative_multiply_total_first. (exists ge_real_code_multiply_total_firstdecode ge_imaginary_code_multiply_total_firstdecode. (((ac) = ((ge_real_code_multiply_total_firstdecode) + (ge_imaginary_code_multiply_total_firstdecode)) * S ((ge_real_code_multiply_total_firstdecode) + (ge_imaginary_code_multiply_total_firstdecode)) + ((ge_imaginary_code_multiply_total_firstdecode) + (ge_imaginary_code_multiply_total_firstdecode))) /\ (((((ge_real_code_multiply_total_firstdecode) = 2 * (ge_real_positive_multiply_total_first) /\ (ge_real_negative_multiply_total_first) = 0) \/ exists ge_signed_half_ge_multiply_total_firstdecode_real. (((ge_real_code_multiply_total_firstdecode) = 2 * ge_signed_half_ge_multiply_total_firstdecode_real + 1 /\ (ge_real_positive_multiply_total_first) = 0) /\ (ge_real_negative_multiply_total_first) = S ge_signed_half_ge_multiply_total_firstdecode_real))) /\ ((((ge_imaginary_code_multiply_total_firstdecode) = 2 * (ge_imaginary_positive_multiply_total_first) /\ (ge_imaginary_negative_multiply_total_first) = 0) \/ exists ge_signed_half_ge_multiply_total_firstdecode_imaginary. (((ge_imaginary_code_multiply_total_firstdecode) = 2 * ge_signed_half_ge_multiply_total_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_multiply_total_first) = 0) /\ (ge_imaginary_negative_multiply_total_first) = S ge_signed_half_ge_multiply_total_firstdecode_imaginary))))))) -> (exists ge_real_positive_multiply_total_second ge_real_negative_multiply_total_second ge_imaginary_positive_multiply_total_second ge_imaginary_negative_multiply_total_second. (exists ge_real_code_multiply_total_seconddecode ge_imaginary_code_multiply_total_seconddecode. (((bc) = ((ge_real_code_multiply_total_seconddecode) + (ge_imaginary_code_multiply_total_seconddecode)) * S ((ge_real_code_multiply_total_seconddecode) + (ge_imaginary_code_multiply_total_seconddecode)) + ((ge_imaginary_code_multiply_total_seconddecode) + (ge_imaginary_code_multiply_total_seconddecode))) /\ (((((ge_real_code_multiply_total_seconddecode) = 2 * (ge_real_positive_multiply_total_second) /\ (ge_real_negative_multiply_total_second) = 0) \/ exists ge_signed_half_ge_multiply_total_seconddecode_real. (((ge_real_code_multiply_total_seconddecode) = 2 * ge_signed_half_ge_multiply_total_seconddecode_real + 1 /\ (ge_real_positive_multiply_total_second) = 0) /\ (ge_real_negative_multiply_total_second) = S ge_signed_half_ge_multiply_total_seconddecode_real))) /\ ((((ge_imaginary_code_multiply_total_seconddecode) = 2 * (ge_imaginary_positive_multiply_total_second) /\ (ge_imaginary_negative_multiply_total_second) = 0) \/ exists ge_signed_half_ge_multiply_total_seconddecode_imaginary. (((ge_imaginary_code_multiply_total_seconddecode) = 2 * ge_signed_half_ge_multiply_total_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_multiply_total_second) = 0) /\ (ge_imaginary_negative_multiply_total_second) = S ge_signed_half_ge_multiply_total_seconddecode_imaginary))))))) -> exists cc. (exists ee_first_rp_multiply_total_output ee_first_rn_multiply_total_output ee_first_ip_multiply_total_output ee_first_in_multiply_total_output ee_second_rp_multiply_total_output ee_second_rn_multiply_total_output ee_second_ip_multiply_total_output ee_second_in_multiply_total_output. ((exists ge_representation_real_code_multiply_total_outputfirst ge_representation_imaginary_code_multiply_total_outputfirst. (((ac) = ((ge_representation_real_code_multiply_total_outputfirst) + (ge_representation_imaginary_code_multiply_total_outputfirst)) * S ((ge_representation_real_code_multiply_total_outputfirst) + (ge_representation_imaginary_code_multiply_total_outputfirst)) + ((ge_representation_imaginary_code_multiply_total_outputfirst) + (ge_representation_imaginary_code_multiply_total_outputfirst))) /\ ((exists ge_balance_positive_multiply_total_outputfirstreal ge_balance_negative_multiply_total_outputfirstreal. (((((ge_representation_real_code_multiply_total_outputfirst) = 2 * (ge_balance_positive_multiply_total_outputfirstreal) /\ (ge_balance_negative_multiply_total_outputfirstreal) = 0) \/ exists ge_signed_half_multiply_total_outputfirstrealdecode. (((ge_representation_real_code_multiply_total_outputfirst) = 2 * ge_signed_half_multiply_total_outputfirstrealdecode + 1 /\ (ge_balance_positive_multiply_total_outputfirstreal) = 0) /\ (ge_balance_negative_multiply_total_outputfirstreal) = S ge_signed_half_multiply_total_outputfirstrealdecode))) /\ ((ee_first_rp_multiply_total_output) + ge_balance_negative_multiply_total_outputfirstreal = (ee_first_rn_multiply_total_output) + ge_balance_positive_multiply_total_outputfirstreal))) /\ (exists ge_balance_positive_multiply_total_outputfirstimaginary ge_balance_negative_multiply_total_outputfirstimaginary. (((((ge_representation_imaginary_code_multiply_total_outputfirst) = 2 * (ge_balance_positive_multiply_total_outputfirstimaginary) /\ (ge_balance_negative_multiply_total_outputfirstimaginary) = 0) \/ exists ge_signed_half_multiply_total_outputfirstimaginarydecode. (((ge_representation_imaginary_code_multiply_total_outputfirst) = 2 * ge_signed_half_multiply_total_outputfirstimaginarydecode + 1 /\ (ge_balance_positive_multiply_total_outputfirstimaginary) = 0) /\ (ge_balance_negative_multiply_total_outputfirstimaginary) = S ge_signed_half_multiply_total_outputfirstimaginarydecode))) /\ ((ee_first_ip_multiply_total_output) + ge_balance_negative_multiply_total_outputfirstimaginary = (ee_first_in_multiply_total_output) + ge_balance_positive_multiply_total_outputfirstimaginary)))))) /\ ((exists ge_representation_real_code_multiply_total_outputsecond ge_representation_imaginary_code_multiply_total_outputsecond. (((bc) = ((ge_representation_real_code_multiply_total_outputsecond) + (ge_representation_imaginary_code_multiply_total_outputsecond)) * S ((ge_representation_real_code_multiply_total_outputsecond) + (ge_representation_imaginary_code_multiply_total_outputsecond)) + ((ge_representation_imaginary_code_multiply_total_outputsecond) + (ge_representation_imaginary_code_multiply_total_outputsecond))) /\ ((exists ge_balance_positive_multiply_total_outputsecondreal ge_balance_negative_multiply_total_outputsecondreal. (((((ge_representation_real_code_multiply_total_outputsecond) = 2 * (ge_balance_positive_multiply_total_outputsecondreal) /\ (ge_balance_negative_multiply_total_outputsecondreal) = 0) \/ exists ge_signed_half_multiply_total_outputsecondrealdecode. (((ge_representation_real_code_multiply_total_outputsecond) = 2 * ge_signed_half_multiply_total_outputsecondrealdecode + 1 /\ (ge_balance_positive_multiply_total_outputsecondreal) = 0) /\ (ge_balance_negative_multiply_total_outputsecondreal) = S ge_signed_half_multiply_total_outputsecondrealdecode))) /\ ((ee_second_rp_multiply_total_output) + ge_balance_negative_multiply_total_outputsecondreal = (ee_second_rn_multiply_total_output) + ge_balance_positive_multiply_total_outputsecondreal))) /\ (exists ge_balance_positive_multiply_total_outputsecondimaginary ge_balance_negative_multiply_total_outputsecondimaginary. (((((ge_representation_imaginary_code_multiply_total_outputsecond) = 2 * (ge_balance_positive_multiply_total_outputsecondimaginary) /\ (ge_balance_negative_multiply_total_outputsecondimaginary) = 0) \/ exists ge_signed_half_multiply_total_outputsecondimaginarydecode. (((ge_representation_imaginary_code_multiply_total_outputsecond) = 2 * ge_signed_half_multiply_total_outputsecondimaginarydecode + 1 /\ (ge_balance_positive_multiply_total_outputsecondimaginary) = 0) /\ (ge_balance_negative_multiply_total_outputsecondimaginary) = S ge_signed_half_multiply_total_outputsecondimaginarydecode))) /\ ((ee_second_ip_multiply_total_output) + ge_balance_negative_multiply_total_outputsecondimaginary = (ee_second_in_multiply_total_output) + ge_balance_positive_multiply_total_outputsecondimaginary)))))) /\ (exists ge_representation_real_code_multiply_total_outputoutput ge_representation_imaginary_code_multiply_total_outputoutput. (((cc) = ((ge_representation_real_code_multiply_total_outputoutput) + (ge_representation_imaginary_code_multiply_total_outputoutput)) * S ((ge_representation_real_code_multiply_total_outputoutput) + (ge_representation_imaginary_code_multiply_total_outputoutput)) + ((ge_representation_imaginary_code_multiply_total_outputoutput) + (ge_representation_imaginary_code_multiply_total_outputoutput))) /\ ((exists ge_balance_positive_multiply_total_outputoutputreal ge_balance_negative_multiply_total_outputoutputreal. (((((ge_representation_real_code_multiply_total_outputoutput) = 2 * (ge_balance_positive_multiply_total_outputoutputreal) /\ (ge_balance_negative_multiply_total_outputoutputreal) = 0) \/ exists ge_signed_half_multiply_total_outputoutputrealdecode. (((ge_representation_real_code_multiply_total_outputoutput) = 2 * ge_signed_half_multiply_total_outputoutputrealdecode + 1 /\ (ge_balance_positive_multiply_total_outputoutputreal) = 0) /\ (ge_balance_negative_multiply_total_outputoutputreal) = S ge_signed_half_multiply_total_outputoutputrealdecode))) /\ ((((((((ee_first_rp_multiply_total_output) * (ee_second_rp_multiply_total_output))) + (((ee_first_rn_multiply_total_output) * (ee_second_rn_multiply_total_output))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_in_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_ip_multiply_total_output))))))) + ge_balance_negative_multiply_total_outputoutputreal = (((((((ee_first_rp_multiply_total_output) * (ee_second_rn_multiply_total_output))) + (((ee_first_rn_multiply_total_output) * (ee_second_rp_multiply_total_output))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_ip_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_in_multiply_total_output))))))) + ge_balance_positive_multiply_total_outputoutputreal))) /\ (exists ge_balance_positive_multiply_total_outputoutputimaginary ge_balance_negative_multiply_total_outputoutputimaginary. (((((ge_representation_imaginary_code_multiply_total_outputoutput) = 2 * (ge_balance_positive_multiply_total_outputoutputimaginary) /\ (ge_balance_negative_multiply_total_outputoutputimaginary) = 0) \/ exists ge_signed_half_multiply_total_outputoutputimaginarydecode. (((ge_representation_imaginary_code_multiply_total_outputoutput) = 2 * ge_signed_half_multiply_total_outputoutputimaginarydecode + 1 /\ (ge_balance_positive_multiply_total_outputoutputimaginary) = 0) /\ (ge_balance_negative_multiply_total_outputoutputimaginary) = S ge_signed_half_multiply_total_outputoutputimaginarydecode))) /\ ((((((((((ee_first_rp_multiply_total_output) * (ee_second_ip_multiply_total_output))) + (((ee_first_rn_multiply_total_output) * (ee_second_in_multiply_total_output))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_rp_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_rn_multiply_total_output))))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_in_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_ip_multiply_total_output))))))) + ge_balance_negative_multiply_total_outputoutputimaginary = (((((((((ee_first_rp_multiply_total_output) * (ee_second_in_multiply_total_output))) + (((ee_first_rn_multiply_total_output) * (ee_second_ip_multiply_total_output))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_rn_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_rp_multiply_total_output))))))) + (((((ee_first_ip_multiply_total_output) * (ee_second_ip_multiply_total_output))) + (((ee_first_in_multiply_total_output) * (ee_second_in_multiply_total_output))))))) + ge_balance_positive_multiply_total_outputoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

47 script commands · 8 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 (1)
eisenstein multiply of representations
01Fix variables and assumptionsL1–4

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro hfirst
  4. L4
    intro hsecond
02Separate the logical casesL5–12

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

  1. L5
    cases hfirst
  2. L6
    cases hfirst_witness
  3. L7
    cases hfirst_witness_witness
  4. L8
    cases hfirst_witness_witness_witness
  5. L9
    cases hsecond
  6. L10
    cases hsecond_witness
  7. L11
    cases hsecond_witness_witness
  8. L12
    cases hsecond_witness_witness_witness
03Establish houtputL13–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian representation exists.

  1. L13
    have houtput : ∃ cc. ZPairRep(cc,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x2 · x7 + x3 · x6),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x2 · x6 + x3 · x7))Definitions: ZPairRep(cc,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x2 · x7 + x3 · x6),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x2 · x6 + x3 · x7))Original native command in the exact edition
  2. L14
    specialize gaussian_representation_exists ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  3. L15
    specialize gaussian_representation_exists ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  4. L16
    specialize gaussian_representation_exists ((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  5. L17
    specialize gaussian_representation_exists ((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  6. L18
    apply gaussian_representation_exists
04Separate the logical casesL19–19

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

  1. L19
    cases houtput
05Construct an explicit witnessL20–20

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

  1. L20
    exists x8
06Use earlier factsL21–30

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

  1. L21
    specialize eisenstein_multiply_of_representations ac
  2. L22
    specialize eisenstein_multiply_of_representations bc
  3. L23
    specialize eisenstein_multiply_of_representations x8
  4. L24
    specialize eisenstein_multiply_of_representations x
  5. L25
    specialize eisenstein_multiply_of_representations x1
  6. L26
    specialize eisenstein_multiply_of_representations x2
  7. L27
    specialize eisenstein_multiply_of_representations x3
  8. L28
    specialize eisenstein_multiply_of_representations x4
  9. L29
    specialize eisenstein_multiply_of_representations x5
  10. L30
    specialize eisenstein_multiply_of_representations x6
07Use earlier factsL31–40

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

  1. L31
    specialize eisenstein_multiply_of_representations x7
  2. L32
    apply eisenstein_multiply_of_representations
  3. L33
    specialize gaussian_decode_representation ac
  4. L34
    specialize gaussian_decode_representation x
  5. L35
    specialize gaussian_decode_representation x1
  6. L36
    specialize gaussian_decode_representation x2
  7. L37
    specialize gaussian_decode_representation x3
  8. L38
    apply gaussian_decode_representation
  9. L39
    exact hfirst_witness_witness_witness_witness
  10. L40
    specialize gaussian_decode_representation bc
08Use earlier factsL41–47

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

  1. L41
    specialize gaussian_decode_representation x4
  2. L42
    specialize gaussian_decode_representation x5
  3. L43
    specialize gaussian_decode_representation x6
  4. L44
    specialize gaussian_decode_representation x7
  5. L45
    apply gaussian_decode_representation
  6. L46
    exact hsecond_witness_witness_witness_witness
  7. L47
    exact houtput_witness

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro hfirst
  4. 0004intro hsecond
  5. 0005cases hfirst
  6. 0006cases hfirst_witness
  7. 0007cases hfirst_witness_witness
  8. 0008cases hfirst_witness_witness_witness
  9. 0009cases hsecond
  10. 0010cases hsecond_witness
  11. 0011cases hsecond_witness_witness
  12. 0012cases hsecond_witness_witness_witness
  13. 0013have houtput : ∃ cc. ZPairRep(cc,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x2 · x7 + x3 · x6),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x2 · x6 + x3 · x7))
  14. 0014specialize gaussian_representation_exists ((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  15. 0015specialize gaussian_representation_exists ((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  16. 0016specialize gaussian_representation_exists ((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((x2) * (x7))) + (((x3) * (x6))))))
  17. 0017specialize gaussian_representation_exists ((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((x2) * (x6))) + (((x3) * (x7))))))
  18. 0018apply gaussian_representation_exists
  19. 0019cases houtput
  20. 0020exists x8
  21. 0021specialize eisenstein_multiply_of_representations ac
  22. 0022specialize eisenstein_multiply_of_representations bc
  23. 0023specialize eisenstein_multiply_of_representations x8
  24. 0024specialize eisenstein_multiply_of_representations x
  25. 0025specialize eisenstein_multiply_of_representations x1
  26. 0026specialize eisenstein_multiply_of_representations x2
  27. 0027specialize eisenstein_multiply_of_representations x3
  28. 0028specialize eisenstein_multiply_of_representations x4
  29. 0029specialize eisenstein_multiply_of_representations x5
  30. 0030specialize eisenstein_multiply_of_representations x6
  31. 0031specialize eisenstein_multiply_of_representations x7
  32. 0032apply eisenstein_multiply_of_representations
  33. 0033specialize gaussian_decode_representation ac
  34. 0034specialize gaussian_decode_representation x
  35. 0035specialize gaussian_decode_representation x1
  36. 0036specialize gaussian_decode_representation x2
  37. 0037specialize gaussian_decode_representation x3
  38. 0038apply gaussian_decode_representation
  39. 0039exact hfirst_witness_witness_witness_witness
  40. 0040specialize gaussian_decode_representation bc
  41. 0041specialize gaussian_decode_representation x4
  42. 0042specialize gaussian_decode_representation x5
  43. 0043specialize gaussian_decode_representation x6
  44. 0044specialize gaussian_decode_representation x7
  45. 0045apply gaussian_decode_representation
  46. 0046exact hsecond_witness_witness_witness_witness
  47. 0047exact houtput_witness