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.

Exact expanded first-order arithmetic 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)))))))))

Constructive proof overview

Generated structural guide

Eisenstein addition is exactly the shared neutral ZPair addition, with its already-checked constructive existence theorem.

The unchanged tactic script uses 1 declared prerequisite and contains 1 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

gaussian_add_exists Alpha theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact command ledger · 1 lines

0001exact gaussian_add_exists