EI0039 — eisenstein_add_exists

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. ZPairAdd(ac,bc,x)

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

Definition DAG

ZPairValid(z) · 2 ZPairAdd(a,b,c) · 1

Actual proof prerequisites

gaussian_add_exists · checked external prerequisite

Original expanded first-order statement

forall ac bc. (exists ge_real_positive_add_first ge_real_negative_add_first ge_imaginary_positive_add_first ge_imaginary_negative_add_first. (exists ge_real_code_add_firstdecode ge_imaginary_code_add_firstdecode. (((ac) = ((ge_real_code_add_firstdecode) + (ge_imaginary_code_add_firstdecode)) * S ((ge_real_code_add_firstdecode) + (ge_imaginary_code_add_firstdecode)) + ((ge_imaginary_code_add_firstdecode) + (ge_imaginary_code_add_firstdecode))) /\ (((((ge_real_code_add_firstdecode) = 2 * (ge_real_positive_add_first) /\ (ge_real_negative_add_first) = 0) \/ exists ge_signed_half_ge_add_firstdecode_real. (((ge_real_code_add_firstdecode) = 2 * ge_signed_half_ge_add_firstdecode_real + 1 /\ (ge_real_positive_add_first) = 0) /\ (ge_real_negative_add_first) = S ge_signed_half_ge_add_firstdecode_real))) /\ ((((ge_imaginary_code_add_firstdecode) = 2 * (ge_imaginary_positive_add_first) /\ (ge_imaginary_negative_add_first) = 0) \/ exists ge_signed_half_ge_add_firstdecode_imaginary. (((ge_imaginary_code_add_firstdecode) = 2 * ge_signed_half_ge_add_firstdecode_imaginary + 1 /\ (ge_imaginary_positive_add_first) = 0) /\ (ge_imaginary_negative_add_first) = S ge_signed_half_ge_add_firstdecode_imaginary))))))) -> (exists ge_real_positive_add_second ge_real_negative_add_second ge_imaginary_positive_add_second ge_imaginary_negative_add_second. (exists ge_real_code_add_seconddecode ge_imaginary_code_add_seconddecode. (((bc) = ((ge_real_code_add_seconddecode) + (ge_imaginary_code_add_seconddecode)) * S ((ge_real_code_add_seconddecode) + (ge_imaginary_code_add_seconddecode)) + ((ge_imaginary_code_add_seconddecode) + (ge_imaginary_code_add_seconddecode))) /\ (((((ge_real_code_add_seconddecode) = 2 * (ge_real_positive_add_second) /\ (ge_real_negative_add_second) = 0) \/ exists ge_signed_half_ge_add_seconddecode_real. (((ge_real_code_add_seconddecode) = 2 * ge_signed_half_ge_add_seconddecode_real + 1 /\ (ge_real_positive_add_second) = 0) /\ (ge_real_negative_add_second) = S ge_signed_half_ge_add_seconddecode_real))) /\ ((((ge_imaginary_code_add_seconddecode) = 2 * (ge_imaginary_positive_add_second) /\ (ge_imaginary_negative_add_second) = 0) \/ exists ge_signed_half_ge_add_seconddecode_imaginary. (((ge_imaginary_code_add_seconddecode) = 2 * ge_signed_half_ge_add_seconddecode_imaginary + 1 /\ (ge_imaginary_positive_add_second) = 0) /\ (ge_imaginary_negative_add_second) = S ge_signed_half_ge_add_seconddecode_imaginary))))))) -> exists cc. (exists ge_first_rp_add_output ge_first_rn_add_output ge_first_ip_add_output ge_first_in_add_output ge_second_rp_add_output ge_second_rn_add_output ge_second_ip_add_output ge_second_in_add_output. ((exists ge_representation_real_code_add_outputfirst ge_representation_imaginary_code_add_outputfirst. (((ac) = ((ge_representation_real_code_add_outputfirst) + (ge_representation_imaginary_code_add_outputfirst)) * S ((ge_representation_real_code_add_outputfirst) + (ge_representation_imaginary_code_add_outputfirst)) + ((ge_representation_imaginary_code_add_outputfirst) + (ge_representation_imaginary_code_add_outputfirst))) /\ ((exists ge_balance_positive_add_outputfirstreal ge_balance_negative_add_outputfirstreal. (((((ge_representation_real_code_add_outputfirst) = 2 * (ge_balance_positive_add_outputfirstreal) /\ (ge_balance_negative_add_outputfirstreal) = 0) \/ exists ge_signed_half_add_outputfirstrealdecode. (((ge_representation_real_code_add_outputfirst) = 2 * ge_signed_half_add_outputfirstrealdecode + 1 /\ (ge_balance_positive_add_outputfirstreal) = 0) /\ (ge_balance_negative_add_outputfirstreal) = S ge_signed_half_add_outputfirstrealdecode))) /\ ((ge_first_rp_add_output) + ge_balance_negative_add_outputfirstreal = (ge_first_rn_add_output) + ge_balance_positive_add_outputfirstreal))) /\ (exists ge_balance_positive_add_outputfirstimaginary ge_balance_negative_add_outputfirstimaginary. (((((ge_representation_imaginary_code_add_outputfirst) = 2 * (ge_balance_positive_add_outputfirstimaginary) /\ (ge_balance_negative_add_outputfirstimaginary) = 0) \/ exists ge_signed_half_add_outputfirstimaginarydecode. (((ge_representation_imaginary_code_add_outputfirst) = 2 * ge_signed_half_add_outputfirstimaginarydecode + 1 /\ (ge_balance_positive_add_outputfirstimaginary) = 0) /\ (ge_balance_negative_add_outputfirstimaginary) = S ge_signed_half_add_outputfirstimaginarydecode))) /\ ((ge_first_ip_add_output) + ge_balance_negative_add_outputfirstimaginary = (ge_first_in_add_output) + ge_balance_positive_add_outputfirstimaginary)))))) /\ ((exists ge_representation_real_code_add_outputsecond ge_representation_imaginary_code_add_outputsecond. (((bc) = ((ge_representation_real_code_add_outputsecond) + (ge_representation_imaginary_code_add_outputsecond)) * S ((ge_representation_real_code_add_outputsecond) + (ge_representation_imaginary_code_add_outputsecond)) + ((ge_representation_imaginary_code_add_outputsecond) + (ge_representation_imaginary_code_add_outputsecond))) /\ ((exists ge_balance_positive_add_outputsecondreal ge_balance_negative_add_outputsecondreal. (((((ge_representation_real_code_add_outputsecond) = 2 * (ge_balance_positive_add_outputsecondreal) /\ (ge_balance_negative_add_outputsecondreal) = 0) \/ exists ge_signed_half_add_outputsecondrealdecode. (((ge_representation_real_code_add_outputsecond) = 2 * ge_signed_half_add_outputsecondrealdecode + 1 /\ (ge_balance_positive_add_outputsecondreal) = 0) /\ (ge_balance_negative_add_outputsecondreal) = S ge_signed_half_add_outputsecondrealdecode))) /\ ((ge_second_rp_add_output) + ge_balance_negative_add_outputsecondreal = (ge_second_rn_add_output) + ge_balance_positive_add_outputsecondreal))) /\ (exists ge_balance_positive_add_outputsecondimaginary ge_balance_negative_add_outputsecondimaginary. (((((ge_representation_imaginary_code_add_outputsecond) = 2 * (ge_balance_positive_add_outputsecondimaginary) /\ (ge_balance_negative_add_outputsecondimaginary) = 0) \/ exists ge_signed_half_add_outputsecondimaginarydecode. (((ge_representation_imaginary_code_add_outputsecond) = 2 * ge_signed_half_add_outputsecondimaginarydecode + 1 /\ (ge_balance_positive_add_outputsecondimaginary) = 0) /\ (ge_balance_negative_add_outputsecondimaginary) = S ge_signed_half_add_outputsecondimaginarydecode))) /\ ((ge_second_ip_add_output) + ge_balance_negative_add_outputsecondimaginary = (ge_second_in_add_output) + ge_balance_positive_add_outputsecondimaginary)))))) /\ (exists ge_representation_real_code_add_outputoutput ge_representation_imaginary_code_add_outputoutput. (((cc) = ((ge_representation_real_code_add_outputoutput) + (ge_representation_imaginary_code_add_outputoutput)) * S ((ge_representation_real_code_add_outputoutput) + (ge_representation_imaginary_code_add_outputoutput)) + ((ge_representation_imaginary_code_add_outputoutput) + (ge_representation_imaginary_code_add_outputoutput))) /\ ((exists ge_balance_positive_add_outputoutputreal ge_balance_negative_add_outputoutputreal. (((((ge_representation_real_code_add_outputoutput) = 2 * (ge_balance_positive_add_outputoutputreal) /\ (ge_balance_negative_add_outputoutputreal) = 0) \/ exists ge_signed_half_add_outputoutputrealdecode. (((ge_representation_real_code_add_outputoutput) = 2 * ge_signed_half_add_outputoutputrealdecode + 1 /\ (ge_balance_positive_add_outputoutputreal) = 0) /\ (ge_balance_negative_add_outputoutputreal) = S ge_signed_half_add_outputoutputrealdecode))) /\ ((((ge_first_rp_add_output) + (ge_second_rp_add_output))) + ge_balance_negative_add_outputoutputreal = (((ge_first_rn_add_output) + (ge_second_rn_add_output))) + ge_balance_positive_add_outputoutputreal))) /\ (exists ge_balance_positive_add_outputoutputimaginary ge_balance_negative_add_outputoutputimaginary. (((((ge_representation_imaginary_code_add_outputoutput) = 2 * (ge_balance_positive_add_outputoutputimaginary) /\ (ge_balance_negative_add_outputoutputimaginary) = 0) \/ exists ge_signed_half_add_outputoutputimaginarydecode. (((ge_representation_imaginary_code_add_outputoutput) = 2 * ge_signed_half_add_outputoutputimaginarydecode + 1 /\ (ge_balance_positive_add_outputoutputimaginary) = 0) /\ (ge_balance_negative_add_outputoutputimaginary) = S ge_signed_half_add_outputoutputimaginarydecode))) /\ ((((ge_first_ip_add_output) + (ge_second_ip_add_output))) + ge_balance_negative_add_outputoutputimaginary = (((ge_first_in_add_output) + (ge_second_in_add_output))) + ge_balance_positive_add_outputoutputimaginary)))))))))

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.

L1
exact gaussian_add_exists

Library-wide reading audit

Original defined command ledger · 1 lines

0001exact gaussian_add_exists