EI003A

eisenstein_add_functional

The same canonical ZPair addition has one literal output code in the Eisenstein presentation; no duplicate additive definition is introduced.

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. ∀ dd. ZPairAdd(ac,bc,cc) → ZPairAdd(ac,bc,dd) → cc = dd

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

Definition DAG

ZPairAdd(a,b,c) · 2

Actual proof prerequisites

gaussian_add_functional · checked external prerequisite
Original expanded first-order statement 
forall ac bc cc dd. (exists ge_first_rp_add_unique_first ge_first_rn_add_unique_first ge_first_ip_add_unique_first ge_first_in_add_unique_first ge_second_rp_add_unique_first ge_second_rn_add_unique_first ge_second_ip_add_unique_first ge_second_in_add_unique_first. ((exists ge_representation_real_code_add_unique_firstfirst ge_representation_imaginary_code_add_unique_firstfirst. (((ac) = ((ge_representation_real_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst)) * S ((ge_representation_real_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst)) + ((ge_representation_imaginary_code_add_unique_firstfirst) + (ge_representation_imaginary_code_add_unique_firstfirst))) /\ ((exists ge_balance_positive_add_unique_firstfirstreal ge_balance_negative_add_unique_firstfirstreal. (((((ge_representation_real_code_add_unique_firstfirst) = 2 * (ge_balance_positive_add_unique_firstfirstreal) /\ (ge_balance_negative_add_unique_firstfirstreal) = 0) \/ exists ge_signed_half_add_unique_firstfirstrealdecode. (((ge_representation_real_code_add_unique_firstfirst) = 2 * ge_signed_half_add_unique_firstfirstrealdecode + 1 /\ (ge_balance_positive_add_unique_firstfirstreal) = 0) /\ (ge_balance_negative_add_unique_firstfirstreal) = S ge_signed_half_add_unique_firstfirstrealdecode))) /\ ((ge_first_rp_add_unique_first) + ge_balance_negative_add_unique_firstfirstreal = (ge_first_rn_add_unique_first) + ge_balance_positive_add_unique_firstfirstreal))) /\ (exists ge_balance_positive_add_unique_firstfirstimaginary ge_balance_negative_add_unique_firstfirstimaginary. (((((ge_representation_imaginary_code_add_unique_firstfirst) = 2 * (ge_balance_positive_add_unique_firstfirstimaginary) /\ (ge_balance_negative_add_unique_firstfirstimaginary) = 0) \/ exists ge_signed_half_add_unique_firstfirstimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstfirst) = 2 * ge_signed_half_add_unique_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstfirstimaginary) = 0) /\ (ge_balance_negative_add_unique_firstfirstimaginary) = S ge_signed_half_add_unique_firstfirstimaginarydecode))) /\ ((ge_first_ip_add_unique_first) + ge_balance_negative_add_unique_firstfirstimaginary = (ge_first_in_add_unique_first) + ge_balance_positive_add_unique_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_unique_firstsecond ge_representation_imaginary_code_add_unique_firstsecond. (((bc) = ((ge_representation_real_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond)) * S ((ge_representation_real_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond)) + ((ge_representation_imaginary_code_add_unique_firstsecond) + (ge_representation_imaginary_code_add_unique_firstsecond))) /\ ((exists ge_balance_positive_add_unique_firstsecondreal ge_balance_negative_add_unique_firstsecondreal. (((((ge_representation_real_code_add_unique_firstsecond) = 2 * (ge_balance_positive_add_unique_firstsecondreal) /\ (ge_balance_negative_add_unique_firstsecondreal) = 0) \/ exists ge_signed_half_add_unique_firstsecondrealdecode. (((ge_representation_real_code_add_unique_firstsecond) = 2 * ge_signed_half_add_unique_firstsecondrealdecode + 1 /\ (ge_balance_positive_add_unique_firstsecondreal) = 0) /\ (ge_balance_negative_add_unique_firstsecondreal) = S ge_signed_half_add_unique_firstsecondrealdecode))) /\ ((ge_second_rp_add_unique_first) + ge_balance_negative_add_unique_firstsecondreal = (ge_second_rn_add_unique_first) + ge_balance_positive_add_unique_firstsecondreal))) /\ (exists ge_balance_positive_add_unique_firstsecondimaginary ge_balance_negative_add_unique_firstsecondimaginary. (((((ge_representation_imaginary_code_add_unique_firstsecond) = 2 * (ge_balance_positive_add_unique_firstsecondimaginary) /\ (ge_balance_negative_add_unique_firstsecondimaginary) = 0) \/ exists ge_signed_half_add_unique_firstsecondimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstsecond) = 2 * ge_signed_half_add_unique_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstsecondimaginary) = 0) /\ (ge_balance_negative_add_unique_firstsecondimaginary) = S ge_signed_half_add_unique_firstsecondimaginarydecode))) /\ ((ge_second_ip_add_unique_first) + ge_balance_negative_add_unique_firstsecondimaginary = (ge_second_in_add_unique_first) + ge_balance_positive_add_unique_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_add_unique_firstoutput ge_representation_imaginary_code_add_unique_firstoutput. (((cc) = ((ge_representation_real_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput)) * S ((ge_representation_real_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput)) + ((ge_representation_imaginary_code_add_unique_firstoutput) + (ge_representation_imaginary_code_add_unique_firstoutput))) /\ ((exists ge_balance_positive_add_unique_firstoutputreal ge_balance_negative_add_unique_firstoutputreal. (((((ge_representation_real_code_add_unique_firstoutput) = 2 * (ge_balance_positive_add_unique_firstoutputreal) /\ (ge_balance_negative_add_unique_firstoutputreal) = 0) \/ exists ge_signed_half_add_unique_firstoutputrealdecode. (((ge_representation_real_code_add_unique_firstoutput) = 2 * ge_signed_half_add_unique_firstoutputrealdecode + 1 /\ (ge_balance_positive_add_unique_firstoutputreal) = 0) /\ (ge_balance_negative_add_unique_firstoutputreal) = S ge_signed_half_add_unique_firstoutputrealdecode))) /\ ((((ge_first_rp_add_unique_first) + (ge_second_rp_add_unique_first))) + ge_balance_negative_add_unique_firstoutputreal = (((ge_first_rn_add_unique_first) + (ge_second_rn_add_unique_first))) + ge_balance_positive_add_unique_firstoutputreal))) /\ (exists ge_balance_positive_add_unique_firstoutputimaginary ge_balance_negative_add_unique_firstoutputimaginary. (((((ge_representation_imaginary_code_add_unique_firstoutput) = 2 * (ge_balance_positive_add_unique_firstoutputimaginary) /\ (ge_balance_negative_add_unique_firstoutputimaginary) = 0) \/ exists ge_signed_half_add_unique_firstoutputimaginarydecode. (((ge_representation_imaginary_code_add_unique_firstoutput) = 2 * ge_signed_half_add_unique_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_add_unique_firstoutputimaginary) = 0) /\ (ge_balance_negative_add_unique_firstoutputimaginary) = S ge_signed_half_add_unique_firstoutputimaginarydecode))) /\ ((((ge_first_ip_add_unique_first) + (ge_second_ip_add_unique_first))) + ge_balance_negative_add_unique_firstoutputimaginary = (((ge_first_in_add_unique_first) + (ge_second_in_add_unique_first))) + ge_balance_positive_add_unique_firstoutputimaginary))))))))) -> (exists ge_first_rp_add_unique_second ge_first_rn_add_unique_second ge_first_ip_add_unique_second ge_first_in_add_unique_second ge_second_rp_add_unique_second ge_second_rn_add_unique_second ge_second_ip_add_unique_second ge_second_in_add_unique_second. ((exists ge_representation_real_code_add_unique_secondfirst ge_representation_imaginary_code_add_unique_secondfirst. (((ac) = ((ge_representation_real_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst)) * S ((ge_representation_real_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst)) + ((ge_representation_imaginary_code_add_unique_secondfirst) + (ge_representation_imaginary_code_add_unique_secondfirst))) /\ ((exists ge_balance_positive_add_unique_secondfirstreal ge_balance_negative_add_unique_secondfirstreal. (((((ge_representation_real_code_add_unique_secondfirst) = 2 * (ge_balance_positive_add_unique_secondfirstreal) /\ (ge_balance_negative_add_unique_secondfirstreal) = 0) \/ exists ge_signed_half_add_unique_secondfirstrealdecode. (((ge_representation_real_code_add_unique_secondfirst) = 2 * ge_signed_half_add_unique_secondfirstrealdecode + 1 /\ (ge_balance_positive_add_unique_secondfirstreal) = 0) /\ (ge_balance_negative_add_unique_secondfirstreal) = S ge_signed_half_add_unique_secondfirstrealdecode))) /\ ((ge_first_rp_add_unique_second) + ge_balance_negative_add_unique_secondfirstreal = (ge_first_rn_add_unique_second) + ge_balance_positive_add_unique_secondfirstreal))) /\ (exists ge_balance_positive_add_unique_secondfirstimaginary ge_balance_negative_add_unique_secondfirstimaginary. (((((ge_representation_imaginary_code_add_unique_secondfirst) = 2 * (ge_balance_positive_add_unique_secondfirstimaginary) /\ (ge_balance_negative_add_unique_secondfirstimaginary) = 0) \/ exists ge_signed_half_add_unique_secondfirstimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondfirst) = 2 * ge_signed_half_add_unique_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondfirstimaginary) = 0) /\ (ge_balance_negative_add_unique_secondfirstimaginary) = S ge_signed_half_add_unique_secondfirstimaginarydecode))) /\ ((ge_first_ip_add_unique_second) + ge_balance_negative_add_unique_secondfirstimaginary = (ge_first_in_add_unique_second) + ge_balance_positive_add_unique_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_unique_secondsecond ge_representation_imaginary_code_add_unique_secondsecond. (((bc) = ((ge_representation_real_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond)) * S ((ge_representation_real_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond)) + ((ge_representation_imaginary_code_add_unique_secondsecond) + (ge_representation_imaginary_code_add_unique_secondsecond))) /\ ((exists ge_balance_positive_add_unique_secondsecondreal ge_balance_negative_add_unique_secondsecondreal. (((((ge_representation_real_code_add_unique_secondsecond) = 2 * (ge_balance_positive_add_unique_secondsecondreal) /\ (ge_balance_negative_add_unique_secondsecondreal) = 0) \/ exists ge_signed_half_add_unique_secondsecondrealdecode. (((ge_representation_real_code_add_unique_secondsecond) = 2 * ge_signed_half_add_unique_secondsecondrealdecode + 1 /\ (ge_balance_positive_add_unique_secondsecondreal) = 0) /\ (ge_balance_negative_add_unique_secondsecondreal) = S ge_signed_half_add_unique_secondsecondrealdecode))) /\ ((ge_second_rp_add_unique_second) + ge_balance_negative_add_unique_secondsecondreal = (ge_second_rn_add_unique_second) + ge_balance_positive_add_unique_secondsecondreal))) /\ (exists ge_balance_positive_add_unique_secondsecondimaginary ge_balance_negative_add_unique_secondsecondimaginary. (((((ge_representation_imaginary_code_add_unique_secondsecond) = 2 * (ge_balance_positive_add_unique_secondsecondimaginary) /\ (ge_balance_negative_add_unique_secondsecondimaginary) = 0) \/ exists ge_signed_half_add_unique_secondsecondimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondsecond) = 2 * ge_signed_half_add_unique_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondsecondimaginary) = 0) /\ (ge_balance_negative_add_unique_secondsecondimaginary) = S ge_signed_half_add_unique_secondsecondimaginarydecode))) /\ ((ge_second_ip_add_unique_second) + ge_balance_negative_add_unique_secondsecondimaginary = (ge_second_in_add_unique_second) + ge_balance_positive_add_unique_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_add_unique_secondoutput ge_representation_imaginary_code_add_unique_secondoutput. (((dd) = ((ge_representation_real_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput)) * S ((ge_representation_real_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput)) + ((ge_representation_imaginary_code_add_unique_secondoutput) + (ge_representation_imaginary_code_add_unique_secondoutput))) /\ ((exists ge_balance_positive_add_unique_secondoutputreal ge_balance_negative_add_unique_secondoutputreal. (((((ge_representation_real_code_add_unique_secondoutput) = 2 * (ge_balance_positive_add_unique_secondoutputreal) /\ (ge_balance_negative_add_unique_secondoutputreal) = 0) \/ exists ge_signed_half_add_unique_secondoutputrealdecode. (((ge_representation_real_code_add_unique_secondoutput) = 2 * ge_signed_half_add_unique_secondoutputrealdecode + 1 /\ (ge_balance_positive_add_unique_secondoutputreal) = 0) /\ (ge_balance_negative_add_unique_secondoutputreal) = S ge_signed_half_add_unique_secondoutputrealdecode))) /\ ((((ge_first_rp_add_unique_second) + (ge_second_rp_add_unique_second))) + ge_balance_negative_add_unique_secondoutputreal = (((ge_first_rn_add_unique_second) + (ge_second_rn_add_unique_second))) + ge_balance_positive_add_unique_secondoutputreal))) /\ (exists ge_balance_positive_add_unique_secondoutputimaginary ge_balance_negative_add_unique_secondoutputimaginary. (((((ge_representation_imaginary_code_add_unique_secondoutput) = 2 * (ge_balance_positive_add_unique_secondoutputimaginary) /\ (ge_balance_negative_add_unique_secondoutputimaginary) = 0) \/ exists ge_signed_half_add_unique_secondoutputimaginarydecode. (((ge_representation_imaginary_code_add_unique_secondoutput) = 2 * ge_signed_half_add_unique_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_add_unique_secondoutputimaginary) = 0) /\ (ge_balance_negative_add_unique_secondoutputimaginary) = S ge_signed_half_add_unique_secondoutputimaginarydecode))) /\ ((((ge_first_ip_add_unique_second) + (ge_second_ip_add_unique_second))) + ge_balance_negative_add_unique_secondoutputimaginary = (((ge_first_in_add_unique_second) + (ge_second_in_add_unique_second))) + ge_balance_positive_add_unique_secondoutputimaginary))))))))) -> cc = dd

Complete tactic proof in conservative notation

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

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

01Use earlier factsL1–1

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

  1. L1
    exact gaussian_add_functional

Library-wide reading audit

Original defined command ledger · 1 lines
  1. 0001exact gaussian_add_functional