GF0039 — gaussian_multiply_add_distribute_right

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.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ s. ∀ p. ∀ q. ∀ t. ZPairAdd(b,c,s) → GMul(b,a,p) → GMul(c,a,q) → GMul(s,a,t) → ZPairAdd(p,q,t)

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

Definition DAG

ZPairAdd(a,b,c) · 2 GMul(a,b,c) · 3

Actual proof prerequisites

gaussian_multiply_add_distribute gaussian_multiply_commutative

Original expanded first-order statement

forall a b c s p q t. (exists ge_first_rp_expand_right_sum ge_first_rn_expand_right_sum ge_first_ip_expand_right_sum ge_first_in_expand_right_sum ge_second_rp_expand_right_sum ge_second_rn_expand_right_sum ge_second_ip_expand_right_sum ge_second_in_expand_right_sum. ((exists ge_representation_real_code_expand_right_sumfirst ge_representation_imaginary_code_expand_right_sumfirst. (((b) = ((ge_representation_real_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst)) * S ((ge_representation_real_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst)) + ((ge_representation_imaginary_code_expand_right_sumfirst) + (ge_representation_imaginary_code_expand_right_sumfirst))) /\ ((exists ge_balance_positive_expand_right_sumfirstreal ge_balance_negative_expand_right_sumfirstreal. (((((ge_representation_real_code_expand_right_sumfirst) = 2 * (ge_balance_positive_expand_right_sumfirstreal) /\ (ge_balance_negative_expand_right_sumfirstreal) = 0) \/ exists ge_signed_half_expand_right_sumfirstrealdecode. (((ge_representation_real_code_expand_right_sumfirst) = 2 * ge_signed_half_expand_right_sumfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_sumfirstreal) = 0) /\ (ge_balance_negative_expand_right_sumfirstreal) = S ge_signed_half_expand_right_sumfirstrealdecode))) /\ ((ge_first_rp_expand_right_sum) + ge_balance_negative_expand_right_sumfirstreal = (ge_first_rn_expand_right_sum) + ge_balance_positive_expand_right_sumfirstreal))) /\ (exists ge_balance_positive_expand_right_sumfirstimaginary ge_balance_negative_expand_right_sumfirstimaginary. (((((ge_representation_imaginary_code_expand_right_sumfirst) = 2 * (ge_balance_positive_expand_right_sumfirstimaginary) /\ (ge_balance_negative_expand_right_sumfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_sumfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumfirst) = 2 * ge_signed_half_expand_right_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_sumfirstimaginary) = S ge_signed_half_expand_right_sumfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_sum) + ge_balance_negative_expand_right_sumfirstimaginary = (ge_first_in_expand_right_sum) + ge_balance_positive_expand_right_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_sumsecond ge_representation_imaginary_code_expand_right_sumsecond. (((c) = ((ge_representation_real_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond)) * S ((ge_representation_real_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond)) + ((ge_representation_imaginary_code_expand_right_sumsecond) + (ge_representation_imaginary_code_expand_right_sumsecond))) /\ ((exists ge_balance_positive_expand_right_sumsecondreal ge_balance_negative_expand_right_sumsecondreal. (((((ge_representation_real_code_expand_right_sumsecond) = 2 * (ge_balance_positive_expand_right_sumsecondreal) /\ (ge_balance_negative_expand_right_sumsecondreal) = 0) \/ exists ge_signed_half_expand_right_sumsecondrealdecode. (((ge_representation_real_code_expand_right_sumsecond) = 2 * ge_signed_half_expand_right_sumsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_sumsecondreal) = 0) /\ (ge_balance_negative_expand_right_sumsecondreal) = S ge_signed_half_expand_right_sumsecondrealdecode))) /\ ((ge_second_rp_expand_right_sum) + ge_balance_negative_expand_right_sumsecondreal = (ge_second_rn_expand_right_sum) + ge_balance_positive_expand_right_sumsecondreal))) /\ (exists ge_balance_positive_expand_right_sumsecondimaginary ge_balance_negative_expand_right_sumsecondimaginary. (((((ge_representation_imaginary_code_expand_right_sumsecond) = 2 * (ge_balance_positive_expand_right_sumsecondimaginary) /\ (ge_balance_negative_expand_right_sumsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_sumsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumsecond) = 2 * ge_signed_half_expand_right_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_sumsecondimaginary) = S ge_signed_half_expand_right_sumsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_sum) + ge_balance_negative_expand_right_sumsecondimaginary = (ge_second_in_expand_right_sum) + ge_balance_positive_expand_right_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_sumoutput ge_representation_imaginary_code_expand_right_sumoutput. (((s) = ((ge_representation_real_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput)) * S ((ge_representation_real_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput)) + ((ge_representation_imaginary_code_expand_right_sumoutput) + (ge_representation_imaginary_code_expand_right_sumoutput))) /\ ((exists ge_balance_positive_expand_right_sumoutputreal ge_balance_negative_expand_right_sumoutputreal. (((((ge_representation_real_code_expand_right_sumoutput) = 2 * (ge_balance_positive_expand_right_sumoutputreal) /\ (ge_balance_negative_expand_right_sumoutputreal) = 0) \/ exists ge_signed_half_expand_right_sumoutputrealdecode. (((ge_representation_real_code_expand_right_sumoutput) = 2 * ge_signed_half_expand_right_sumoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_sumoutputreal) = 0) /\ (ge_balance_negative_expand_right_sumoutputreal) = S ge_signed_half_expand_right_sumoutputrealdecode))) /\ ((((ge_first_rp_expand_right_sum) + (ge_second_rp_expand_right_sum))) + ge_balance_negative_expand_right_sumoutputreal = (((ge_first_rn_expand_right_sum) + (ge_second_rn_expand_right_sum))) + ge_balance_positive_expand_right_sumoutputreal))) /\ (exists ge_balance_positive_expand_right_sumoutputimaginary ge_balance_negative_expand_right_sumoutputimaginary. (((((ge_representation_imaginary_code_expand_right_sumoutput) = 2 * (ge_balance_positive_expand_right_sumoutputimaginary) /\ (ge_balance_negative_expand_right_sumoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_sumoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_sumoutput) = 2 * ge_signed_half_expand_right_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_sumoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_sumoutputimaginary) = S ge_signed_half_expand_right_sumoutputimaginarydecode))) /\ ((((ge_first_ip_expand_right_sum) + (ge_second_ip_expand_right_sum))) + ge_balance_negative_expand_right_sumoutputimaginary = (((ge_first_in_expand_right_sum) + (ge_second_in_expand_right_sum))) + ge_balance_positive_expand_right_sumoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_first ge_first_rn_expand_right_first ge_first_ip_expand_right_first ge_first_in_expand_right_first ge_second_rp_expand_right_first ge_second_rn_expand_right_first ge_second_ip_expand_right_first ge_second_in_expand_right_first. ((exists ge_representation_real_code_expand_right_firstfirst ge_representation_imaginary_code_expand_right_firstfirst. (((b) = ((ge_representation_real_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst)) * S ((ge_representation_real_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst)) + ((ge_representation_imaginary_code_expand_right_firstfirst) + (ge_representation_imaginary_code_expand_right_firstfirst))) /\ ((exists ge_balance_positive_expand_right_firstfirstreal ge_balance_negative_expand_right_firstfirstreal. (((((ge_representation_real_code_expand_right_firstfirst) = 2 * (ge_balance_positive_expand_right_firstfirstreal) /\ (ge_balance_negative_expand_right_firstfirstreal) = 0) \/ exists ge_signed_half_expand_right_firstfirstrealdecode. (((ge_representation_real_code_expand_right_firstfirst) = 2 * ge_signed_half_expand_right_firstfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_firstfirstreal) = 0) /\ (ge_balance_negative_expand_right_firstfirstreal) = S ge_signed_half_expand_right_firstfirstrealdecode))) /\ ((ge_first_rp_expand_right_first) + ge_balance_negative_expand_right_firstfirstreal = (ge_first_rn_expand_right_first) + ge_balance_positive_expand_right_firstfirstreal))) /\ (exists ge_balance_positive_expand_right_firstfirstimaginary ge_balance_negative_expand_right_firstfirstimaginary. (((((ge_representation_imaginary_code_expand_right_firstfirst) = 2 * (ge_balance_positive_expand_right_firstfirstimaginary) /\ (ge_balance_negative_expand_right_firstfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_firstfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstfirst) = 2 * ge_signed_half_expand_right_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_firstfirstimaginary) = S ge_signed_half_expand_right_firstfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_first) + ge_balance_negative_expand_right_firstfirstimaginary = (ge_first_in_expand_right_first) + ge_balance_positive_expand_right_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_firstsecond ge_representation_imaginary_code_expand_right_firstsecond. (((a) = ((ge_representation_real_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond)) * S ((ge_representation_real_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond)) + ((ge_representation_imaginary_code_expand_right_firstsecond) + (ge_representation_imaginary_code_expand_right_firstsecond))) /\ ((exists ge_balance_positive_expand_right_firstsecondreal ge_balance_negative_expand_right_firstsecondreal. (((((ge_representation_real_code_expand_right_firstsecond) = 2 * (ge_balance_positive_expand_right_firstsecondreal) /\ (ge_balance_negative_expand_right_firstsecondreal) = 0) \/ exists ge_signed_half_expand_right_firstsecondrealdecode. (((ge_representation_real_code_expand_right_firstsecond) = 2 * ge_signed_half_expand_right_firstsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_firstsecondreal) = 0) /\ (ge_balance_negative_expand_right_firstsecondreal) = S ge_signed_half_expand_right_firstsecondrealdecode))) /\ ((ge_second_rp_expand_right_first) + ge_balance_negative_expand_right_firstsecondreal = (ge_second_rn_expand_right_first) + ge_balance_positive_expand_right_firstsecondreal))) /\ (exists ge_balance_positive_expand_right_firstsecondimaginary ge_balance_negative_expand_right_firstsecondimaginary. (((((ge_representation_imaginary_code_expand_right_firstsecond) = 2 * (ge_balance_positive_expand_right_firstsecondimaginary) /\ (ge_balance_negative_expand_right_firstsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_firstsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstsecond) = 2 * ge_signed_half_expand_right_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_firstsecondimaginary) = S ge_signed_half_expand_right_firstsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_first) + ge_balance_negative_expand_right_firstsecondimaginary = (ge_second_in_expand_right_first) + ge_balance_positive_expand_right_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_firstoutput ge_representation_imaginary_code_expand_right_firstoutput. (((p) = ((ge_representation_real_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput)) * S ((ge_representation_real_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput)) + ((ge_representation_imaginary_code_expand_right_firstoutput) + (ge_representation_imaginary_code_expand_right_firstoutput))) /\ ((exists ge_balance_positive_expand_right_firstoutputreal ge_balance_negative_expand_right_firstoutputreal. (((((ge_representation_real_code_expand_right_firstoutput) = 2 * (ge_balance_positive_expand_right_firstoutputreal) /\ (ge_balance_negative_expand_right_firstoutputreal) = 0) \/ exists ge_signed_half_expand_right_firstoutputrealdecode. (((ge_representation_real_code_expand_right_firstoutput) = 2 * ge_signed_half_expand_right_firstoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_firstoutputreal) = 0) /\ (ge_balance_negative_expand_right_firstoutputreal) = S ge_signed_half_expand_right_firstoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_first) * (ge_second_rp_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_rn_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_in_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_ip_expand_right_first))))))) + ge_balance_negative_expand_right_firstoutputreal = (((((((ge_first_rp_expand_right_first) * (ge_second_rn_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_rp_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_ip_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_in_expand_right_first))))))) + ge_balance_positive_expand_right_firstoutputreal))) /\ (exists ge_balance_positive_expand_right_firstoutputimaginary ge_balance_negative_expand_right_firstoutputimaginary. (((((ge_representation_imaginary_code_expand_right_firstoutput) = 2 * (ge_balance_positive_expand_right_firstoutputimaginary) /\ (ge_balance_negative_expand_right_firstoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_firstoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_firstoutput) = 2 * ge_signed_half_expand_right_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_firstoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_firstoutputimaginary) = S ge_signed_half_expand_right_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_first) * (ge_second_ip_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_in_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_rp_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_rn_expand_right_first))))))) + ge_balance_negative_expand_right_firstoutputimaginary = (((((((ge_first_rp_expand_right_first) * (ge_second_in_expand_right_first))) + (((ge_first_rn_expand_right_first) * (ge_second_ip_expand_right_first))))) + (((((ge_first_ip_expand_right_first) * (ge_second_rn_expand_right_first))) + (((ge_first_in_expand_right_first) * (ge_second_rp_expand_right_first))))))) + ge_balance_positive_expand_right_firstoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_second ge_first_rn_expand_right_second ge_first_ip_expand_right_second ge_first_in_expand_right_second ge_second_rp_expand_right_second ge_second_rn_expand_right_second ge_second_ip_expand_right_second ge_second_in_expand_right_second. ((exists ge_representation_real_code_expand_right_secondfirst ge_representation_imaginary_code_expand_right_secondfirst. (((c) = ((ge_representation_real_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst)) * S ((ge_representation_real_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst)) + ((ge_representation_imaginary_code_expand_right_secondfirst) + (ge_representation_imaginary_code_expand_right_secondfirst))) /\ ((exists ge_balance_positive_expand_right_secondfirstreal ge_balance_negative_expand_right_secondfirstreal. (((((ge_representation_real_code_expand_right_secondfirst) = 2 * (ge_balance_positive_expand_right_secondfirstreal) /\ (ge_balance_negative_expand_right_secondfirstreal) = 0) \/ exists ge_signed_half_expand_right_secondfirstrealdecode. (((ge_representation_real_code_expand_right_secondfirst) = 2 * ge_signed_half_expand_right_secondfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_secondfirstreal) = 0) /\ (ge_balance_negative_expand_right_secondfirstreal) = S ge_signed_half_expand_right_secondfirstrealdecode))) /\ ((ge_first_rp_expand_right_second) + ge_balance_negative_expand_right_secondfirstreal = (ge_first_rn_expand_right_second) + ge_balance_positive_expand_right_secondfirstreal))) /\ (exists ge_balance_positive_expand_right_secondfirstimaginary ge_balance_negative_expand_right_secondfirstimaginary. (((((ge_representation_imaginary_code_expand_right_secondfirst) = 2 * (ge_balance_positive_expand_right_secondfirstimaginary) /\ (ge_balance_negative_expand_right_secondfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_secondfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondfirst) = 2 * ge_signed_half_expand_right_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_secondfirstimaginary) = S ge_signed_half_expand_right_secondfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_second) + ge_balance_negative_expand_right_secondfirstimaginary = (ge_first_in_expand_right_second) + ge_balance_positive_expand_right_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_secondsecond ge_representation_imaginary_code_expand_right_secondsecond. (((a) = ((ge_representation_real_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond)) * S ((ge_representation_real_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond)) + ((ge_representation_imaginary_code_expand_right_secondsecond) + (ge_representation_imaginary_code_expand_right_secondsecond))) /\ ((exists ge_balance_positive_expand_right_secondsecondreal ge_balance_negative_expand_right_secondsecondreal. (((((ge_representation_real_code_expand_right_secondsecond) = 2 * (ge_balance_positive_expand_right_secondsecondreal) /\ (ge_balance_negative_expand_right_secondsecondreal) = 0) \/ exists ge_signed_half_expand_right_secondsecondrealdecode. (((ge_representation_real_code_expand_right_secondsecond) = 2 * ge_signed_half_expand_right_secondsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_secondsecondreal) = 0) /\ (ge_balance_negative_expand_right_secondsecondreal) = S ge_signed_half_expand_right_secondsecondrealdecode))) /\ ((ge_second_rp_expand_right_second) + ge_balance_negative_expand_right_secondsecondreal = (ge_second_rn_expand_right_second) + ge_balance_positive_expand_right_secondsecondreal))) /\ (exists ge_balance_positive_expand_right_secondsecondimaginary ge_balance_negative_expand_right_secondsecondimaginary. (((((ge_representation_imaginary_code_expand_right_secondsecond) = 2 * (ge_balance_positive_expand_right_secondsecondimaginary) /\ (ge_balance_negative_expand_right_secondsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_secondsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondsecond) = 2 * ge_signed_half_expand_right_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_secondsecondimaginary) = S ge_signed_half_expand_right_secondsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_second) + ge_balance_negative_expand_right_secondsecondimaginary = (ge_second_in_expand_right_second) + ge_balance_positive_expand_right_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_secondoutput ge_representation_imaginary_code_expand_right_secondoutput. (((q) = ((ge_representation_real_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput)) * S ((ge_representation_real_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput)) + ((ge_representation_imaginary_code_expand_right_secondoutput) + (ge_representation_imaginary_code_expand_right_secondoutput))) /\ ((exists ge_balance_positive_expand_right_secondoutputreal ge_balance_negative_expand_right_secondoutputreal. (((((ge_representation_real_code_expand_right_secondoutput) = 2 * (ge_balance_positive_expand_right_secondoutputreal) /\ (ge_balance_negative_expand_right_secondoutputreal) = 0) \/ exists ge_signed_half_expand_right_secondoutputrealdecode. (((ge_representation_real_code_expand_right_secondoutput) = 2 * ge_signed_half_expand_right_secondoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_secondoutputreal) = 0) /\ (ge_balance_negative_expand_right_secondoutputreal) = S ge_signed_half_expand_right_secondoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_second) * (ge_second_rp_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_rn_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_in_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_ip_expand_right_second))))))) + ge_balance_negative_expand_right_secondoutputreal = (((((((ge_first_rp_expand_right_second) * (ge_second_rn_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_rp_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_ip_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_in_expand_right_second))))))) + ge_balance_positive_expand_right_secondoutputreal))) /\ (exists ge_balance_positive_expand_right_secondoutputimaginary ge_balance_negative_expand_right_secondoutputimaginary. (((((ge_representation_imaginary_code_expand_right_secondoutput) = 2 * (ge_balance_positive_expand_right_secondoutputimaginary) /\ (ge_balance_negative_expand_right_secondoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_secondoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_secondoutput) = 2 * ge_signed_half_expand_right_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_secondoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_secondoutputimaginary) = S ge_signed_half_expand_right_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_second) * (ge_second_ip_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_in_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_rp_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_rn_expand_right_second))))))) + ge_balance_negative_expand_right_secondoutputimaginary = (((((((ge_first_rp_expand_right_second) * (ge_second_in_expand_right_second))) + (((ge_first_rn_expand_right_second) * (ge_second_ip_expand_right_second))))) + (((((ge_first_ip_expand_right_second) * (ge_second_rn_expand_right_second))) + (((ge_first_in_expand_right_second) * (ge_second_rp_expand_right_second))))))) + ge_balance_positive_expand_right_secondoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_product ge_first_rn_expand_right_product ge_first_ip_expand_right_product ge_first_in_expand_right_product ge_second_rp_expand_right_product ge_second_rn_expand_right_product ge_second_ip_expand_right_product ge_second_in_expand_right_product. ((exists ge_representation_real_code_expand_right_productfirst ge_representation_imaginary_code_expand_right_productfirst. (((s) = ((ge_representation_real_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst)) * S ((ge_representation_real_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst)) + ((ge_representation_imaginary_code_expand_right_productfirst) + (ge_representation_imaginary_code_expand_right_productfirst))) /\ ((exists ge_balance_positive_expand_right_productfirstreal ge_balance_negative_expand_right_productfirstreal. (((((ge_representation_real_code_expand_right_productfirst) = 2 * (ge_balance_positive_expand_right_productfirstreal) /\ (ge_balance_negative_expand_right_productfirstreal) = 0) \/ exists ge_signed_half_expand_right_productfirstrealdecode. (((ge_representation_real_code_expand_right_productfirst) = 2 * ge_signed_half_expand_right_productfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_productfirstreal) = 0) /\ (ge_balance_negative_expand_right_productfirstreal) = S ge_signed_half_expand_right_productfirstrealdecode))) /\ ((ge_first_rp_expand_right_product) + ge_balance_negative_expand_right_productfirstreal = (ge_first_rn_expand_right_product) + ge_balance_positive_expand_right_productfirstreal))) /\ (exists ge_balance_positive_expand_right_productfirstimaginary ge_balance_negative_expand_right_productfirstimaginary. (((((ge_representation_imaginary_code_expand_right_productfirst) = 2 * (ge_balance_positive_expand_right_productfirstimaginary) /\ (ge_balance_negative_expand_right_productfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_productfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_productfirst) = 2 * ge_signed_half_expand_right_productfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_productfirstimaginary) = S ge_signed_half_expand_right_productfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_product) + ge_balance_negative_expand_right_productfirstimaginary = (ge_first_in_expand_right_product) + ge_balance_positive_expand_right_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_productsecond ge_representation_imaginary_code_expand_right_productsecond. (((a) = ((ge_representation_real_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond)) * S ((ge_representation_real_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond)) + ((ge_representation_imaginary_code_expand_right_productsecond) + (ge_representation_imaginary_code_expand_right_productsecond))) /\ ((exists ge_balance_positive_expand_right_productsecondreal ge_balance_negative_expand_right_productsecondreal. (((((ge_representation_real_code_expand_right_productsecond) = 2 * (ge_balance_positive_expand_right_productsecondreal) /\ (ge_balance_negative_expand_right_productsecondreal) = 0) \/ exists ge_signed_half_expand_right_productsecondrealdecode. (((ge_representation_real_code_expand_right_productsecond) = 2 * ge_signed_half_expand_right_productsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_productsecondreal) = 0) /\ (ge_balance_negative_expand_right_productsecondreal) = S ge_signed_half_expand_right_productsecondrealdecode))) /\ ((ge_second_rp_expand_right_product) + ge_balance_negative_expand_right_productsecondreal = (ge_second_rn_expand_right_product) + ge_balance_positive_expand_right_productsecondreal))) /\ (exists ge_balance_positive_expand_right_productsecondimaginary ge_balance_negative_expand_right_productsecondimaginary. (((((ge_representation_imaginary_code_expand_right_productsecond) = 2 * (ge_balance_positive_expand_right_productsecondimaginary) /\ (ge_balance_negative_expand_right_productsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_productsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_productsecond) = 2 * ge_signed_half_expand_right_productsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_productsecondimaginary) = S ge_signed_half_expand_right_productsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_product) + ge_balance_negative_expand_right_productsecondimaginary = (ge_second_in_expand_right_product) + ge_balance_positive_expand_right_productsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_productoutput ge_representation_imaginary_code_expand_right_productoutput. (((t) = ((ge_representation_real_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput)) * S ((ge_representation_real_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput)) + ((ge_representation_imaginary_code_expand_right_productoutput) + (ge_representation_imaginary_code_expand_right_productoutput))) /\ ((exists ge_balance_positive_expand_right_productoutputreal ge_balance_negative_expand_right_productoutputreal. (((((ge_representation_real_code_expand_right_productoutput) = 2 * (ge_balance_positive_expand_right_productoutputreal) /\ (ge_balance_negative_expand_right_productoutputreal) = 0) \/ exists ge_signed_half_expand_right_productoutputrealdecode. (((ge_representation_real_code_expand_right_productoutput) = 2 * ge_signed_half_expand_right_productoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_productoutputreal) = 0) /\ (ge_balance_negative_expand_right_productoutputreal) = S ge_signed_half_expand_right_productoutputrealdecode))) /\ ((((((((ge_first_rp_expand_right_product) * (ge_second_rp_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_rn_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_in_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_ip_expand_right_product))))))) + ge_balance_negative_expand_right_productoutputreal = (((((((ge_first_rp_expand_right_product) * (ge_second_rn_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_rp_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_ip_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_in_expand_right_product))))))) + ge_balance_positive_expand_right_productoutputreal))) /\ (exists ge_balance_positive_expand_right_productoutputimaginary ge_balance_negative_expand_right_productoutputimaginary. (((((ge_representation_imaginary_code_expand_right_productoutput) = 2 * (ge_balance_positive_expand_right_productoutputimaginary) /\ (ge_balance_negative_expand_right_productoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_productoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_productoutput) = 2 * ge_signed_half_expand_right_productoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_productoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_productoutputimaginary) = S ge_signed_half_expand_right_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_expand_right_product) * (ge_second_ip_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_in_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_rp_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_rn_expand_right_product))))))) + ge_balance_negative_expand_right_productoutputimaginary = (((((((ge_first_rp_expand_right_product) * (ge_second_in_expand_right_product))) + (((ge_first_rn_expand_right_product) * (ge_second_ip_expand_right_product))))) + (((((ge_first_ip_expand_right_product) * (ge_second_rn_expand_right_product))) + (((ge_first_in_expand_right_product) * (ge_second_rp_expand_right_product))))))) + ge_balance_positive_expand_right_productoutputimaginary))))))))) -> (exists ge_first_rp_expand_right_result ge_first_rn_expand_right_result ge_first_ip_expand_right_result ge_first_in_expand_right_result ge_second_rp_expand_right_result ge_second_rn_expand_right_result ge_second_ip_expand_right_result ge_second_in_expand_right_result. ((exists ge_representation_real_code_expand_right_resultfirst ge_representation_imaginary_code_expand_right_resultfirst. (((p) = ((ge_representation_real_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst)) * S ((ge_representation_real_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst)) + ((ge_representation_imaginary_code_expand_right_resultfirst) + (ge_representation_imaginary_code_expand_right_resultfirst))) /\ ((exists ge_balance_positive_expand_right_resultfirstreal ge_balance_negative_expand_right_resultfirstreal. (((((ge_representation_real_code_expand_right_resultfirst) = 2 * (ge_balance_positive_expand_right_resultfirstreal) /\ (ge_balance_negative_expand_right_resultfirstreal) = 0) \/ exists ge_signed_half_expand_right_resultfirstrealdecode. (((ge_representation_real_code_expand_right_resultfirst) = 2 * ge_signed_half_expand_right_resultfirstrealdecode + 1 /\ (ge_balance_positive_expand_right_resultfirstreal) = 0) /\ (ge_balance_negative_expand_right_resultfirstreal) = S ge_signed_half_expand_right_resultfirstrealdecode))) /\ ((ge_first_rp_expand_right_result) + ge_balance_negative_expand_right_resultfirstreal = (ge_first_rn_expand_right_result) + ge_balance_positive_expand_right_resultfirstreal))) /\ (exists ge_balance_positive_expand_right_resultfirstimaginary ge_balance_negative_expand_right_resultfirstimaginary. (((((ge_representation_imaginary_code_expand_right_resultfirst) = 2 * (ge_balance_positive_expand_right_resultfirstimaginary) /\ (ge_balance_negative_expand_right_resultfirstimaginary) = 0) \/ exists ge_signed_half_expand_right_resultfirstimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultfirst) = 2 * ge_signed_half_expand_right_resultfirstimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultfirstimaginary) = 0) /\ (ge_balance_negative_expand_right_resultfirstimaginary) = S ge_signed_half_expand_right_resultfirstimaginarydecode))) /\ ((ge_first_ip_expand_right_result) + ge_balance_negative_expand_right_resultfirstimaginary = (ge_first_in_expand_right_result) + ge_balance_positive_expand_right_resultfirstimaginary)))))) /\ ((exists ge_representation_real_code_expand_right_resultsecond ge_representation_imaginary_code_expand_right_resultsecond. (((q) = ((ge_representation_real_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond)) * S ((ge_representation_real_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond)) + ((ge_representation_imaginary_code_expand_right_resultsecond) + (ge_representation_imaginary_code_expand_right_resultsecond))) /\ ((exists ge_balance_positive_expand_right_resultsecondreal ge_balance_negative_expand_right_resultsecondreal. (((((ge_representation_real_code_expand_right_resultsecond) = 2 * (ge_balance_positive_expand_right_resultsecondreal) /\ (ge_balance_negative_expand_right_resultsecondreal) = 0) \/ exists ge_signed_half_expand_right_resultsecondrealdecode. (((ge_representation_real_code_expand_right_resultsecond) = 2 * ge_signed_half_expand_right_resultsecondrealdecode + 1 /\ (ge_balance_positive_expand_right_resultsecondreal) = 0) /\ (ge_balance_negative_expand_right_resultsecondreal) = S ge_signed_half_expand_right_resultsecondrealdecode))) /\ ((ge_second_rp_expand_right_result) + ge_balance_negative_expand_right_resultsecondreal = (ge_second_rn_expand_right_result) + ge_balance_positive_expand_right_resultsecondreal))) /\ (exists ge_balance_positive_expand_right_resultsecondimaginary ge_balance_negative_expand_right_resultsecondimaginary. (((((ge_representation_imaginary_code_expand_right_resultsecond) = 2 * (ge_balance_positive_expand_right_resultsecondimaginary) /\ (ge_balance_negative_expand_right_resultsecondimaginary) = 0) \/ exists ge_signed_half_expand_right_resultsecondimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultsecond) = 2 * ge_signed_half_expand_right_resultsecondimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultsecondimaginary) = 0) /\ (ge_balance_negative_expand_right_resultsecondimaginary) = S ge_signed_half_expand_right_resultsecondimaginarydecode))) /\ ((ge_second_ip_expand_right_result) + ge_balance_negative_expand_right_resultsecondimaginary = (ge_second_in_expand_right_result) + ge_balance_positive_expand_right_resultsecondimaginary)))))) /\ (exists ge_representation_real_code_expand_right_resultoutput ge_representation_imaginary_code_expand_right_resultoutput. (((t) = ((ge_representation_real_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput)) * S ((ge_representation_real_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput)) + ((ge_representation_imaginary_code_expand_right_resultoutput) + (ge_representation_imaginary_code_expand_right_resultoutput))) /\ ((exists ge_balance_positive_expand_right_resultoutputreal ge_balance_negative_expand_right_resultoutputreal. (((((ge_representation_real_code_expand_right_resultoutput) = 2 * (ge_balance_positive_expand_right_resultoutputreal) /\ (ge_balance_negative_expand_right_resultoutputreal) = 0) \/ exists ge_signed_half_expand_right_resultoutputrealdecode. (((ge_representation_real_code_expand_right_resultoutput) = 2 * ge_signed_half_expand_right_resultoutputrealdecode + 1 /\ (ge_balance_positive_expand_right_resultoutputreal) = 0) /\ (ge_balance_negative_expand_right_resultoutputreal) = S ge_signed_half_expand_right_resultoutputrealdecode))) /\ ((((ge_first_rp_expand_right_result) + (ge_second_rp_expand_right_result))) + ge_balance_negative_expand_right_resultoutputreal = (((ge_first_rn_expand_right_result) + (ge_second_rn_expand_right_result))) + ge_balance_positive_expand_right_resultoutputreal))) /\ (exists ge_balance_positive_expand_right_resultoutputimaginary ge_balance_negative_expand_right_resultoutputimaginary. (((((ge_representation_imaginary_code_expand_right_resultoutput) = 2 * (ge_balance_positive_expand_right_resultoutputimaginary) /\ (ge_balance_negative_expand_right_resultoutputimaginary) = 0) \/ exists ge_signed_half_expand_right_resultoutputimaginarydecode. (((ge_representation_imaginary_code_expand_right_resultoutput) = 2 * ge_signed_half_expand_right_resultoutputimaginarydecode + 1 /\ (ge_balance_positive_expand_right_resultoutputimaginary) = 0) /\ (ge_balance_negative_expand_right_resultoutputimaginary) = S ge_signed_half_expand_right_resultoutputimaginarydecode))) /\ ((((ge_first_ip_expand_right_result) + (ge_second_ip_expand_right_result))) + ge_balance_negative_expand_right_resultoutputimaginary = (((ge_first_in_expand_right_result) + (ge_second_in_expand_right_result))) + ge_balance_positive_expand_right_resultoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

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

Named ingredients (2)

gaussian multiply add distribute gaussian multiply commutative

01Fix variables and assumptionsL1–10

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