GF0037

gaussian_multiply_add_compose

The sum of two actual Gaussian products is the product with their actual summed second factors.

Alpha v34 checked-use · first admitted v30 · 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.

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(a,b,p) → GMul(a,c,q) → ZPairAdd(p,q,t) → GMul(a,s,t)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 7ZPairAdd(a,b,c) · 2GMul(a,b,c) · 3

Actual proof prerequisites

gaussian_valid_has_representationgaussian_multiply_input_left_validgaussian_multiply_input_right_validgaussian_multiply_for_representations · checked external prerequisitegaussian_add_for_representations · checked external prerequisitegaussian_multiply_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_equal_symmetric · checked external prerequisitegaussian_ring_raw_multiply_add_distributive
Original expanded first-order statement 
forall a b c s p q t. (exists ge_first_rp_distribute_sum ge_first_rn_distribute_sum ge_first_ip_distribute_sum ge_first_in_distribute_sum ge_second_rp_distribute_sum ge_second_rn_distribute_sum ge_second_ip_distribute_sum ge_second_in_distribute_sum. ((exists ge_representation_real_code_distribute_sumfirst ge_representation_imaginary_code_distribute_sumfirst. (((b) = ((ge_representation_real_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst)) * S ((ge_representation_real_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst)) + ((ge_representation_imaginary_code_distribute_sumfirst) + (ge_representation_imaginary_code_distribute_sumfirst))) /\ ((exists ge_balance_positive_distribute_sumfirstreal ge_balance_negative_distribute_sumfirstreal. (((((ge_representation_real_code_distribute_sumfirst) = 2 * (ge_balance_positive_distribute_sumfirstreal) /\ (ge_balance_negative_distribute_sumfirstreal) = 0) \/ exists ge_signed_half_distribute_sumfirstrealdecode. (((ge_representation_real_code_distribute_sumfirst) = 2 * ge_signed_half_distribute_sumfirstrealdecode + 1 /\ (ge_balance_positive_distribute_sumfirstreal) = 0) /\ (ge_balance_negative_distribute_sumfirstreal) = S ge_signed_half_distribute_sumfirstrealdecode))) /\ ((ge_first_rp_distribute_sum) + ge_balance_negative_distribute_sumfirstreal = (ge_first_rn_distribute_sum) + ge_balance_positive_distribute_sumfirstreal))) /\ (exists ge_balance_positive_distribute_sumfirstimaginary ge_balance_negative_distribute_sumfirstimaginary. (((((ge_representation_imaginary_code_distribute_sumfirst) = 2 * (ge_balance_positive_distribute_sumfirstimaginary) /\ (ge_balance_negative_distribute_sumfirstimaginary) = 0) \/ exists ge_signed_half_distribute_sumfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_sumfirst) = 2 * ge_signed_half_distribute_sumfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumfirstimaginary) = 0) /\ (ge_balance_negative_distribute_sumfirstimaginary) = S ge_signed_half_distribute_sumfirstimaginarydecode))) /\ ((ge_first_ip_distribute_sum) + ge_balance_negative_distribute_sumfirstimaginary = (ge_first_in_distribute_sum) + ge_balance_positive_distribute_sumfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_sumsecond ge_representation_imaginary_code_distribute_sumsecond. (((c) = ((ge_representation_real_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond)) * S ((ge_representation_real_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond)) + ((ge_representation_imaginary_code_distribute_sumsecond) + (ge_representation_imaginary_code_distribute_sumsecond))) /\ ((exists ge_balance_positive_distribute_sumsecondreal ge_balance_negative_distribute_sumsecondreal. (((((ge_representation_real_code_distribute_sumsecond) = 2 * (ge_balance_positive_distribute_sumsecondreal) /\ (ge_balance_negative_distribute_sumsecondreal) = 0) \/ exists ge_signed_half_distribute_sumsecondrealdecode. (((ge_representation_real_code_distribute_sumsecond) = 2 * ge_signed_half_distribute_sumsecondrealdecode + 1 /\ (ge_balance_positive_distribute_sumsecondreal) = 0) /\ (ge_balance_negative_distribute_sumsecondreal) = S ge_signed_half_distribute_sumsecondrealdecode))) /\ ((ge_second_rp_distribute_sum) + ge_balance_negative_distribute_sumsecondreal = (ge_second_rn_distribute_sum) + ge_balance_positive_distribute_sumsecondreal))) /\ (exists ge_balance_positive_distribute_sumsecondimaginary ge_balance_negative_distribute_sumsecondimaginary. (((((ge_representation_imaginary_code_distribute_sumsecond) = 2 * (ge_balance_positive_distribute_sumsecondimaginary) /\ (ge_balance_negative_distribute_sumsecondimaginary) = 0) \/ exists ge_signed_half_distribute_sumsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_sumsecond) = 2 * ge_signed_half_distribute_sumsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumsecondimaginary) = 0) /\ (ge_balance_negative_distribute_sumsecondimaginary) = S ge_signed_half_distribute_sumsecondimaginarydecode))) /\ ((ge_second_ip_distribute_sum) + ge_balance_negative_distribute_sumsecondimaginary = (ge_second_in_distribute_sum) + ge_balance_positive_distribute_sumsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_sumoutput ge_representation_imaginary_code_distribute_sumoutput. (((s) = ((ge_representation_real_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput)) * S ((ge_representation_real_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput)) + ((ge_representation_imaginary_code_distribute_sumoutput) + (ge_representation_imaginary_code_distribute_sumoutput))) /\ ((exists ge_balance_positive_distribute_sumoutputreal ge_balance_negative_distribute_sumoutputreal. (((((ge_representation_real_code_distribute_sumoutput) = 2 * (ge_balance_positive_distribute_sumoutputreal) /\ (ge_balance_negative_distribute_sumoutputreal) = 0) \/ exists ge_signed_half_distribute_sumoutputrealdecode. (((ge_representation_real_code_distribute_sumoutput) = 2 * ge_signed_half_distribute_sumoutputrealdecode + 1 /\ (ge_balance_positive_distribute_sumoutputreal) = 0) /\ (ge_balance_negative_distribute_sumoutputreal) = S ge_signed_half_distribute_sumoutputrealdecode))) /\ ((((ge_first_rp_distribute_sum) + (ge_second_rp_distribute_sum))) + ge_balance_negative_distribute_sumoutputreal = (((ge_first_rn_distribute_sum) + (ge_second_rn_distribute_sum))) + ge_balance_positive_distribute_sumoutputreal))) /\ (exists ge_balance_positive_distribute_sumoutputimaginary ge_balance_negative_distribute_sumoutputimaginary. (((((ge_representation_imaginary_code_distribute_sumoutput) = 2 * (ge_balance_positive_distribute_sumoutputimaginary) /\ (ge_balance_negative_distribute_sumoutputimaginary) = 0) \/ exists ge_signed_half_distribute_sumoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_sumoutput) = 2 * ge_signed_half_distribute_sumoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_sumoutputimaginary) = 0) /\ (ge_balance_negative_distribute_sumoutputimaginary) = S ge_signed_half_distribute_sumoutputimaginarydecode))) /\ ((((ge_first_ip_distribute_sum) + (ge_second_ip_distribute_sum))) + ge_balance_negative_distribute_sumoutputimaginary = (((ge_first_in_distribute_sum) + (ge_second_in_distribute_sum))) + ge_balance_positive_distribute_sumoutputimaginary))))))))) -> (exists ge_first_rp_distribute_first ge_first_rn_distribute_first ge_first_ip_distribute_first ge_first_in_distribute_first ge_second_rp_distribute_first ge_second_rn_distribute_first ge_second_ip_distribute_first ge_second_in_distribute_first. ((exists ge_representation_real_code_distribute_firstfirst ge_representation_imaginary_code_distribute_firstfirst. (((a) = ((ge_representation_real_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst)) * S ((ge_representation_real_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst)) + ((ge_representation_imaginary_code_distribute_firstfirst) + (ge_representation_imaginary_code_distribute_firstfirst))) /\ ((exists ge_balance_positive_distribute_firstfirstreal ge_balance_negative_distribute_firstfirstreal. (((((ge_representation_real_code_distribute_firstfirst) = 2 * (ge_balance_positive_distribute_firstfirstreal) /\ (ge_balance_negative_distribute_firstfirstreal) = 0) \/ exists ge_signed_half_distribute_firstfirstrealdecode. (((ge_representation_real_code_distribute_firstfirst) = 2 * ge_signed_half_distribute_firstfirstrealdecode + 1 /\ (ge_balance_positive_distribute_firstfirstreal) = 0) /\ (ge_balance_negative_distribute_firstfirstreal) = S ge_signed_half_distribute_firstfirstrealdecode))) /\ ((ge_first_rp_distribute_first) + ge_balance_negative_distribute_firstfirstreal = (ge_first_rn_distribute_first) + ge_balance_positive_distribute_firstfirstreal))) /\ (exists ge_balance_positive_distribute_firstfirstimaginary ge_balance_negative_distribute_firstfirstimaginary. (((((ge_representation_imaginary_code_distribute_firstfirst) = 2 * (ge_balance_positive_distribute_firstfirstimaginary) /\ (ge_balance_negative_distribute_firstfirstimaginary) = 0) \/ exists ge_signed_half_distribute_firstfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_firstfirst) = 2 * ge_signed_half_distribute_firstfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstfirstimaginary) = 0) /\ (ge_balance_negative_distribute_firstfirstimaginary) = S ge_signed_half_distribute_firstfirstimaginarydecode))) /\ ((ge_first_ip_distribute_first) + ge_balance_negative_distribute_firstfirstimaginary = (ge_first_in_distribute_first) + ge_balance_positive_distribute_firstfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_firstsecond ge_representation_imaginary_code_distribute_firstsecond. (((b) = ((ge_representation_real_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond)) * S ((ge_representation_real_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond)) + ((ge_representation_imaginary_code_distribute_firstsecond) + (ge_representation_imaginary_code_distribute_firstsecond))) /\ ((exists ge_balance_positive_distribute_firstsecondreal ge_balance_negative_distribute_firstsecondreal. (((((ge_representation_real_code_distribute_firstsecond) = 2 * (ge_balance_positive_distribute_firstsecondreal) /\ (ge_balance_negative_distribute_firstsecondreal) = 0) \/ exists ge_signed_half_distribute_firstsecondrealdecode. (((ge_representation_real_code_distribute_firstsecond) = 2 * ge_signed_half_distribute_firstsecondrealdecode + 1 /\ (ge_balance_positive_distribute_firstsecondreal) = 0) /\ (ge_balance_negative_distribute_firstsecondreal) = S ge_signed_half_distribute_firstsecondrealdecode))) /\ ((ge_second_rp_distribute_first) + ge_balance_negative_distribute_firstsecondreal = (ge_second_rn_distribute_first) + ge_balance_positive_distribute_firstsecondreal))) /\ (exists ge_balance_positive_distribute_firstsecondimaginary ge_balance_negative_distribute_firstsecondimaginary. (((((ge_representation_imaginary_code_distribute_firstsecond) = 2 * (ge_balance_positive_distribute_firstsecondimaginary) /\ (ge_balance_negative_distribute_firstsecondimaginary) = 0) \/ exists ge_signed_half_distribute_firstsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_firstsecond) = 2 * ge_signed_half_distribute_firstsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstsecondimaginary) = 0) /\ (ge_balance_negative_distribute_firstsecondimaginary) = S ge_signed_half_distribute_firstsecondimaginarydecode))) /\ ((ge_second_ip_distribute_first) + ge_balance_negative_distribute_firstsecondimaginary = (ge_second_in_distribute_first) + ge_balance_positive_distribute_firstsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_firstoutput ge_representation_imaginary_code_distribute_firstoutput. (((p) = ((ge_representation_real_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput)) * S ((ge_representation_real_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput)) + ((ge_representation_imaginary_code_distribute_firstoutput) + (ge_representation_imaginary_code_distribute_firstoutput))) /\ ((exists ge_balance_positive_distribute_firstoutputreal ge_balance_negative_distribute_firstoutputreal. (((((ge_representation_real_code_distribute_firstoutput) = 2 * (ge_balance_positive_distribute_firstoutputreal) /\ (ge_balance_negative_distribute_firstoutputreal) = 0) \/ exists ge_signed_half_distribute_firstoutputrealdecode. (((ge_representation_real_code_distribute_firstoutput) = 2 * ge_signed_half_distribute_firstoutputrealdecode + 1 /\ (ge_balance_positive_distribute_firstoutputreal) = 0) /\ (ge_balance_negative_distribute_firstoutputreal) = S ge_signed_half_distribute_firstoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_first) * (ge_second_rp_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_rn_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_in_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_ip_distribute_first))))))) + ge_balance_negative_distribute_firstoutputreal = (((((((ge_first_rp_distribute_first) * (ge_second_rn_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_rp_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_ip_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_in_distribute_first))))))) + ge_balance_positive_distribute_firstoutputreal))) /\ (exists ge_balance_positive_distribute_firstoutputimaginary ge_balance_negative_distribute_firstoutputimaginary. (((((ge_representation_imaginary_code_distribute_firstoutput) = 2 * (ge_balance_positive_distribute_firstoutputimaginary) /\ (ge_balance_negative_distribute_firstoutputimaginary) = 0) \/ exists ge_signed_half_distribute_firstoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_firstoutput) = 2 * ge_signed_half_distribute_firstoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_firstoutputimaginary) = 0) /\ (ge_balance_negative_distribute_firstoutputimaginary) = S ge_signed_half_distribute_firstoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_first) * (ge_second_ip_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_in_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_rp_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_rn_distribute_first))))))) + ge_balance_negative_distribute_firstoutputimaginary = (((((((ge_first_rp_distribute_first) * (ge_second_in_distribute_first))) + (((ge_first_rn_distribute_first) * (ge_second_ip_distribute_first))))) + (((((ge_first_ip_distribute_first) * (ge_second_rn_distribute_first))) + (((ge_first_in_distribute_first) * (ge_second_rp_distribute_first))))))) + ge_balance_positive_distribute_firstoutputimaginary))))))))) -> (exists ge_first_rp_distribute_second ge_first_rn_distribute_second ge_first_ip_distribute_second ge_first_in_distribute_second ge_second_rp_distribute_second ge_second_rn_distribute_second ge_second_ip_distribute_second ge_second_in_distribute_second. ((exists ge_representation_real_code_distribute_secondfirst ge_representation_imaginary_code_distribute_secondfirst. (((a) = ((ge_representation_real_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst)) * S ((ge_representation_real_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst)) + ((ge_representation_imaginary_code_distribute_secondfirst) + (ge_representation_imaginary_code_distribute_secondfirst))) /\ ((exists ge_balance_positive_distribute_secondfirstreal ge_balance_negative_distribute_secondfirstreal. (((((ge_representation_real_code_distribute_secondfirst) = 2 * (ge_balance_positive_distribute_secondfirstreal) /\ (ge_balance_negative_distribute_secondfirstreal) = 0) \/ exists ge_signed_half_distribute_secondfirstrealdecode. (((ge_representation_real_code_distribute_secondfirst) = 2 * ge_signed_half_distribute_secondfirstrealdecode + 1 /\ (ge_balance_positive_distribute_secondfirstreal) = 0) /\ (ge_balance_negative_distribute_secondfirstreal) = S ge_signed_half_distribute_secondfirstrealdecode))) /\ ((ge_first_rp_distribute_second) + ge_balance_negative_distribute_secondfirstreal = (ge_first_rn_distribute_second) + ge_balance_positive_distribute_secondfirstreal))) /\ (exists ge_balance_positive_distribute_secondfirstimaginary ge_balance_negative_distribute_secondfirstimaginary. (((((ge_representation_imaginary_code_distribute_secondfirst) = 2 * (ge_balance_positive_distribute_secondfirstimaginary) /\ (ge_balance_negative_distribute_secondfirstimaginary) = 0) \/ exists ge_signed_half_distribute_secondfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_secondfirst) = 2 * ge_signed_half_distribute_secondfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondfirstimaginary) = 0) /\ (ge_balance_negative_distribute_secondfirstimaginary) = S ge_signed_half_distribute_secondfirstimaginarydecode))) /\ ((ge_first_ip_distribute_second) + ge_balance_negative_distribute_secondfirstimaginary = (ge_first_in_distribute_second) + ge_balance_positive_distribute_secondfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_secondsecond ge_representation_imaginary_code_distribute_secondsecond. (((c) = ((ge_representation_real_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond)) * S ((ge_representation_real_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond)) + ((ge_representation_imaginary_code_distribute_secondsecond) + (ge_representation_imaginary_code_distribute_secondsecond))) /\ ((exists ge_balance_positive_distribute_secondsecondreal ge_balance_negative_distribute_secondsecondreal. (((((ge_representation_real_code_distribute_secondsecond) = 2 * (ge_balance_positive_distribute_secondsecondreal) /\ (ge_balance_negative_distribute_secondsecondreal) = 0) \/ exists ge_signed_half_distribute_secondsecondrealdecode. (((ge_representation_real_code_distribute_secondsecond) = 2 * ge_signed_half_distribute_secondsecondrealdecode + 1 /\ (ge_balance_positive_distribute_secondsecondreal) = 0) /\ (ge_balance_negative_distribute_secondsecondreal) = S ge_signed_half_distribute_secondsecondrealdecode))) /\ ((ge_second_rp_distribute_second) + ge_balance_negative_distribute_secondsecondreal = (ge_second_rn_distribute_second) + ge_balance_positive_distribute_secondsecondreal))) /\ (exists ge_balance_positive_distribute_secondsecondimaginary ge_balance_negative_distribute_secondsecondimaginary. (((((ge_representation_imaginary_code_distribute_secondsecond) = 2 * (ge_balance_positive_distribute_secondsecondimaginary) /\ (ge_balance_negative_distribute_secondsecondimaginary) = 0) \/ exists ge_signed_half_distribute_secondsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_secondsecond) = 2 * ge_signed_half_distribute_secondsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondsecondimaginary) = 0) /\ (ge_balance_negative_distribute_secondsecondimaginary) = S ge_signed_half_distribute_secondsecondimaginarydecode))) /\ ((ge_second_ip_distribute_second) + ge_balance_negative_distribute_secondsecondimaginary = (ge_second_in_distribute_second) + ge_balance_positive_distribute_secondsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_secondoutput ge_representation_imaginary_code_distribute_secondoutput. (((q) = ((ge_representation_real_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput)) * S ((ge_representation_real_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput)) + ((ge_representation_imaginary_code_distribute_secondoutput) + (ge_representation_imaginary_code_distribute_secondoutput))) /\ ((exists ge_balance_positive_distribute_secondoutputreal ge_balance_negative_distribute_secondoutputreal. (((((ge_representation_real_code_distribute_secondoutput) = 2 * (ge_balance_positive_distribute_secondoutputreal) /\ (ge_balance_negative_distribute_secondoutputreal) = 0) \/ exists ge_signed_half_distribute_secondoutputrealdecode. (((ge_representation_real_code_distribute_secondoutput) = 2 * ge_signed_half_distribute_secondoutputrealdecode + 1 /\ (ge_balance_positive_distribute_secondoutputreal) = 0) /\ (ge_balance_negative_distribute_secondoutputreal) = S ge_signed_half_distribute_secondoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_second) * (ge_second_rp_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_rn_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_in_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_ip_distribute_second))))))) + ge_balance_negative_distribute_secondoutputreal = (((((((ge_first_rp_distribute_second) * (ge_second_rn_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_rp_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_ip_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_in_distribute_second))))))) + ge_balance_positive_distribute_secondoutputreal))) /\ (exists ge_balance_positive_distribute_secondoutputimaginary ge_balance_negative_distribute_secondoutputimaginary. (((((ge_representation_imaginary_code_distribute_secondoutput) = 2 * (ge_balance_positive_distribute_secondoutputimaginary) /\ (ge_balance_negative_distribute_secondoutputimaginary) = 0) \/ exists ge_signed_half_distribute_secondoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_secondoutput) = 2 * ge_signed_half_distribute_secondoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_secondoutputimaginary) = 0) /\ (ge_balance_negative_distribute_secondoutputimaginary) = S ge_signed_half_distribute_secondoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_second) * (ge_second_ip_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_in_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_rp_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_rn_distribute_second))))))) + ge_balance_negative_distribute_secondoutputimaginary = (((((((ge_first_rp_distribute_second) * (ge_second_in_distribute_second))) + (((ge_first_rn_distribute_second) * (ge_second_ip_distribute_second))))) + (((((ge_first_ip_distribute_second) * (ge_second_rn_distribute_second))) + (((ge_first_in_distribute_second) * (ge_second_rp_distribute_second))))))) + ge_balance_positive_distribute_secondoutputimaginary))))))))) -> (exists ge_first_rp_distribute_total ge_first_rn_distribute_total ge_first_ip_distribute_total ge_first_in_distribute_total ge_second_rp_distribute_total ge_second_rn_distribute_total ge_second_ip_distribute_total ge_second_in_distribute_total. ((exists ge_representation_real_code_distribute_totalfirst ge_representation_imaginary_code_distribute_totalfirst. (((p) = ((ge_representation_real_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst)) * S ((ge_representation_real_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst)) + ((ge_representation_imaginary_code_distribute_totalfirst) + (ge_representation_imaginary_code_distribute_totalfirst))) /\ ((exists ge_balance_positive_distribute_totalfirstreal ge_balance_negative_distribute_totalfirstreal. (((((ge_representation_real_code_distribute_totalfirst) = 2 * (ge_balance_positive_distribute_totalfirstreal) /\ (ge_balance_negative_distribute_totalfirstreal) = 0) \/ exists ge_signed_half_distribute_totalfirstrealdecode. (((ge_representation_real_code_distribute_totalfirst) = 2 * ge_signed_half_distribute_totalfirstrealdecode + 1 /\ (ge_balance_positive_distribute_totalfirstreal) = 0) /\ (ge_balance_negative_distribute_totalfirstreal) = S ge_signed_half_distribute_totalfirstrealdecode))) /\ ((ge_first_rp_distribute_total) + ge_balance_negative_distribute_totalfirstreal = (ge_first_rn_distribute_total) + ge_balance_positive_distribute_totalfirstreal))) /\ (exists ge_balance_positive_distribute_totalfirstimaginary ge_balance_negative_distribute_totalfirstimaginary. (((((ge_representation_imaginary_code_distribute_totalfirst) = 2 * (ge_balance_positive_distribute_totalfirstimaginary) /\ (ge_balance_negative_distribute_totalfirstimaginary) = 0) \/ exists ge_signed_half_distribute_totalfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_totalfirst) = 2 * ge_signed_half_distribute_totalfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_totalfirstimaginary) = 0) /\ (ge_balance_negative_distribute_totalfirstimaginary) = S ge_signed_half_distribute_totalfirstimaginarydecode))) /\ ((ge_first_ip_distribute_total) + ge_balance_negative_distribute_totalfirstimaginary = (ge_first_in_distribute_total) + ge_balance_positive_distribute_totalfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_totalsecond ge_representation_imaginary_code_distribute_totalsecond. (((q) = ((ge_representation_real_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond)) * S ((ge_representation_real_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond)) + ((ge_representation_imaginary_code_distribute_totalsecond) + (ge_representation_imaginary_code_distribute_totalsecond))) /\ ((exists ge_balance_positive_distribute_totalsecondreal ge_balance_negative_distribute_totalsecondreal. (((((ge_representation_real_code_distribute_totalsecond) = 2 * (ge_balance_positive_distribute_totalsecondreal) /\ (ge_balance_negative_distribute_totalsecondreal) = 0) \/ exists ge_signed_half_distribute_totalsecondrealdecode. (((ge_representation_real_code_distribute_totalsecond) = 2 * ge_signed_half_distribute_totalsecondrealdecode + 1 /\ (ge_balance_positive_distribute_totalsecondreal) = 0) /\ (ge_balance_negative_distribute_totalsecondreal) = S ge_signed_half_distribute_totalsecondrealdecode))) /\ ((ge_second_rp_distribute_total) + ge_balance_negative_distribute_totalsecondreal = (ge_second_rn_distribute_total) + ge_balance_positive_distribute_totalsecondreal))) /\ (exists ge_balance_positive_distribute_totalsecondimaginary ge_balance_negative_distribute_totalsecondimaginary. (((((ge_representation_imaginary_code_distribute_totalsecond) = 2 * (ge_balance_positive_distribute_totalsecondimaginary) /\ (ge_balance_negative_distribute_totalsecondimaginary) = 0) \/ exists ge_signed_half_distribute_totalsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_totalsecond) = 2 * ge_signed_half_distribute_totalsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_totalsecondimaginary) = 0) /\ (ge_balance_negative_distribute_totalsecondimaginary) = S ge_signed_half_distribute_totalsecondimaginarydecode))) /\ ((ge_second_ip_distribute_total) + ge_balance_negative_distribute_totalsecondimaginary = (ge_second_in_distribute_total) + ge_balance_positive_distribute_totalsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_totaloutput ge_representation_imaginary_code_distribute_totaloutput. (((t) = ((ge_representation_real_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput)) * S ((ge_representation_real_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput)) + ((ge_representation_imaginary_code_distribute_totaloutput) + (ge_representation_imaginary_code_distribute_totaloutput))) /\ ((exists ge_balance_positive_distribute_totaloutputreal ge_balance_negative_distribute_totaloutputreal. (((((ge_representation_real_code_distribute_totaloutput) = 2 * (ge_balance_positive_distribute_totaloutputreal) /\ (ge_balance_negative_distribute_totaloutputreal) = 0) \/ exists ge_signed_half_distribute_totaloutputrealdecode. (((ge_representation_real_code_distribute_totaloutput) = 2 * ge_signed_half_distribute_totaloutputrealdecode + 1 /\ (ge_balance_positive_distribute_totaloutputreal) = 0) /\ (ge_balance_negative_distribute_totaloutputreal) = S ge_signed_half_distribute_totaloutputrealdecode))) /\ ((((ge_first_rp_distribute_total) + (ge_second_rp_distribute_total))) + ge_balance_negative_distribute_totaloutputreal = (((ge_first_rn_distribute_total) + (ge_second_rn_distribute_total))) + ge_balance_positive_distribute_totaloutputreal))) /\ (exists ge_balance_positive_distribute_totaloutputimaginary ge_balance_negative_distribute_totaloutputimaginary. (((((ge_representation_imaginary_code_distribute_totaloutput) = 2 * (ge_balance_positive_distribute_totaloutputimaginary) /\ (ge_balance_negative_distribute_totaloutputimaginary) = 0) \/ exists ge_signed_half_distribute_totaloutputimaginarydecode. (((ge_representation_imaginary_code_distribute_totaloutput) = 2 * ge_signed_half_distribute_totaloutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_totaloutputimaginary) = 0) /\ (ge_balance_negative_distribute_totaloutputimaginary) = S ge_signed_half_distribute_totaloutputimaginarydecode))) /\ ((((ge_first_ip_distribute_total) + (ge_second_ip_distribute_total))) + ge_balance_negative_distribute_totaloutputimaginary = (((ge_first_in_distribute_total) + (ge_second_in_distribute_total))) + ge_balance_positive_distribute_totaloutputimaginary))))))))) -> (exists ge_first_rp_distribute_product ge_first_rn_distribute_product ge_first_ip_distribute_product ge_first_in_distribute_product ge_second_rp_distribute_product ge_second_rn_distribute_product ge_second_ip_distribute_product ge_second_in_distribute_product. ((exists ge_representation_real_code_distribute_productfirst ge_representation_imaginary_code_distribute_productfirst. (((a) = ((ge_representation_real_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst)) * S ((ge_representation_real_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst)) + ((ge_representation_imaginary_code_distribute_productfirst) + (ge_representation_imaginary_code_distribute_productfirst))) /\ ((exists ge_balance_positive_distribute_productfirstreal ge_balance_negative_distribute_productfirstreal. (((((ge_representation_real_code_distribute_productfirst) = 2 * (ge_balance_positive_distribute_productfirstreal) /\ (ge_balance_negative_distribute_productfirstreal) = 0) \/ exists ge_signed_half_distribute_productfirstrealdecode. (((ge_representation_real_code_distribute_productfirst) = 2 * ge_signed_half_distribute_productfirstrealdecode + 1 /\ (ge_balance_positive_distribute_productfirstreal) = 0) /\ (ge_balance_negative_distribute_productfirstreal) = S ge_signed_half_distribute_productfirstrealdecode))) /\ ((ge_first_rp_distribute_product) + ge_balance_negative_distribute_productfirstreal = (ge_first_rn_distribute_product) + ge_balance_positive_distribute_productfirstreal))) /\ (exists ge_balance_positive_distribute_productfirstimaginary ge_balance_negative_distribute_productfirstimaginary. (((((ge_representation_imaginary_code_distribute_productfirst) = 2 * (ge_balance_positive_distribute_productfirstimaginary) /\ (ge_balance_negative_distribute_productfirstimaginary) = 0) \/ exists ge_signed_half_distribute_productfirstimaginarydecode. (((ge_representation_imaginary_code_distribute_productfirst) = 2 * ge_signed_half_distribute_productfirstimaginarydecode + 1 /\ (ge_balance_positive_distribute_productfirstimaginary) = 0) /\ (ge_balance_negative_distribute_productfirstimaginary) = S ge_signed_half_distribute_productfirstimaginarydecode))) /\ ((ge_first_ip_distribute_product) + ge_balance_negative_distribute_productfirstimaginary = (ge_first_in_distribute_product) + ge_balance_positive_distribute_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_distribute_productsecond ge_representation_imaginary_code_distribute_productsecond. (((s) = ((ge_representation_real_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond)) * S ((ge_representation_real_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond)) + ((ge_representation_imaginary_code_distribute_productsecond) + (ge_representation_imaginary_code_distribute_productsecond))) /\ ((exists ge_balance_positive_distribute_productsecondreal ge_balance_negative_distribute_productsecondreal. (((((ge_representation_real_code_distribute_productsecond) = 2 * (ge_balance_positive_distribute_productsecondreal) /\ (ge_balance_negative_distribute_productsecondreal) = 0) \/ exists ge_signed_half_distribute_productsecondrealdecode. (((ge_representation_real_code_distribute_productsecond) = 2 * ge_signed_half_distribute_productsecondrealdecode + 1 /\ (ge_balance_positive_distribute_productsecondreal) = 0) /\ (ge_balance_negative_distribute_productsecondreal) = S ge_signed_half_distribute_productsecondrealdecode))) /\ ((ge_second_rp_distribute_product) + ge_balance_negative_distribute_productsecondreal = (ge_second_rn_distribute_product) + ge_balance_positive_distribute_productsecondreal))) /\ (exists ge_balance_positive_distribute_productsecondimaginary ge_balance_negative_distribute_productsecondimaginary. (((((ge_representation_imaginary_code_distribute_productsecond) = 2 * (ge_balance_positive_distribute_productsecondimaginary) /\ (ge_balance_negative_distribute_productsecondimaginary) = 0) \/ exists ge_signed_half_distribute_productsecondimaginarydecode. (((ge_representation_imaginary_code_distribute_productsecond) = 2 * ge_signed_half_distribute_productsecondimaginarydecode + 1 /\ (ge_balance_positive_distribute_productsecondimaginary) = 0) /\ (ge_balance_negative_distribute_productsecondimaginary) = S ge_signed_half_distribute_productsecondimaginarydecode))) /\ ((ge_second_ip_distribute_product) + ge_balance_negative_distribute_productsecondimaginary = (ge_second_in_distribute_product) + ge_balance_positive_distribute_productsecondimaginary)))))) /\ (exists ge_representation_real_code_distribute_productoutput ge_representation_imaginary_code_distribute_productoutput. (((t) = ((ge_representation_real_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput)) * S ((ge_representation_real_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput)) + ((ge_representation_imaginary_code_distribute_productoutput) + (ge_representation_imaginary_code_distribute_productoutput))) /\ ((exists ge_balance_positive_distribute_productoutputreal ge_balance_negative_distribute_productoutputreal. (((((ge_representation_real_code_distribute_productoutput) = 2 * (ge_balance_positive_distribute_productoutputreal) /\ (ge_balance_negative_distribute_productoutputreal) = 0) \/ exists ge_signed_half_distribute_productoutputrealdecode. (((ge_representation_real_code_distribute_productoutput) = 2 * ge_signed_half_distribute_productoutputrealdecode + 1 /\ (ge_balance_positive_distribute_productoutputreal) = 0) /\ (ge_balance_negative_distribute_productoutputreal) = S ge_signed_half_distribute_productoutputrealdecode))) /\ ((((((((ge_first_rp_distribute_product) * (ge_second_rp_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_rn_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_in_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_ip_distribute_product))))))) + ge_balance_negative_distribute_productoutputreal = (((((((ge_first_rp_distribute_product) * (ge_second_rn_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_rp_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_ip_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_in_distribute_product))))))) + ge_balance_positive_distribute_productoutputreal))) /\ (exists ge_balance_positive_distribute_productoutputimaginary ge_balance_negative_distribute_productoutputimaginary. (((((ge_representation_imaginary_code_distribute_productoutput) = 2 * (ge_balance_positive_distribute_productoutputimaginary) /\ (ge_balance_negative_distribute_productoutputimaginary) = 0) \/ exists ge_signed_half_distribute_productoutputimaginarydecode. (((ge_representation_imaginary_code_distribute_productoutput) = 2 * ge_signed_half_distribute_productoutputimaginarydecode + 1 /\ (ge_balance_positive_distribute_productoutputimaginary) = 0) /\ (ge_balance_negative_distribute_productoutputimaginary) = S ge_signed_half_distribute_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_distribute_product) * (ge_second_ip_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_in_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_rp_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_rn_distribute_product))))))) + ge_balance_negative_distribute_productoutputimaginary = (((((((ge_first_rp_distribute_product) * (ge_second_in_distribute_product))) + (((ge_first_rn_distribute_product) * (ge_second_ip_distribute_product))))) + (((((ge_first_ip_distribute_product) * (ge_second_rn_distribute_product))) + (((ge_first_in_distribute_product) * (ge_second_rp_distribute_product))))))) + ge_balance_positive_distribute_productoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

158 script commands · 21 reading checkpoints · 7 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 (4)
gaussian valid has representationgaussian multiply input left validgaussian multiply input right validgaussian ring raw multiply add distributive
01Fix variables and assumptionsL1–10

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro s
  5. L5
    intro p
  6. L6
    intro q
  7. L7
    intro t
  8. L8
    intro hBC
  9. L9
    intro hAB
  10. L10
    intro hAC
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hPQ
03Establish hAL12–19

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

  1. L12
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep(a,rp,rn,ip,inn)Original native command in the exact edition
  2. L13
    specialize gaussian_valid_has_representation (a)
  3. L14
    apply gaussian_valid_has_representation
  4. L15
    specialize gaussian_multiply_input_left_valid (a)
  5. L16
    specialize gaussian_multiply_input_left_valid (b)
  6. L17
    specialize gaussian_multiply_input_left_valid (p)
  7. L18
    apply gaussian_multiply_input_left_valid
  8. L19
    exact hAB
04Separate the logical casesL20–23

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

  1. L20
    cases hA
  2. L21
    cases hA_witness
  3. L22
    cases hA_witness_witness
  4. L23
    cases hA_witness_witness_witness
05Establish hBL24–31

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

  1. L24
    have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)Definitions: ZPairRep(b,rp,rn,ip,inn)Original native command in the exact edition
  2. L25
    specialize gaussian_valid_has_representation (b)
  3. L26
    apply gaussian_valid_has_representation
  4. L27
    specialize gaussian_multiply_input_right_valid (a)
  5. L28
    specialize gaussian_multiply_input_right_valid (b)
  6. L29
    specialize gaussian_multiply_input_right_valid (p)
  7. L30
    apply gaussian_multiply_input_right_valid
  8. L31
    exact hAB
06Separate the logical casesL32–35

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

  1. L32
    cases hB
  2. L33
    cases hB_witness
  3. L34
    cases hB_witness_witness
  4. L35
    cases hB_witness_witness_witness
07Establish hCL36–43

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

  1. L36
    have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)Definitions: ZPairRep(c,rp,rn,ip,inn)Original native command in the exact edition
  2. L37
    specialize gaussian_valid_has_representation (c)
  3. L38
    apply gaussian_valid_has_representation
  4. L39
    specialize gaussian_multiply_input_right_valid (a)
  5. L40
    specialize gaussian_multiply_input_right_valid (c)
  6. L41
    specialize gaussian_multiply_input_right_valid (q)
  7. L42
    apply gaussian_multiply_input_right_valid
  8. L43
    exact hAC
08Separate the logical casesL44–47

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

  1. L44
    cases hC
  2. L45
    cases hC_witness
  3. L46
    cases hC_witness_witness
  4. L47
    cases hC_witness_witness_witness
09Establish hpL48–57

Establish this local claim before using it. It is not an additional assumption.

  1. L48
    have hp : ZPairRep(p,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))Definitions: ZPairRep(p,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))Original native command in the exact edition
  2. L49
    specialize gaussian_multiply_for_representations (a)
  3. L50
    specialize gaussian_multiply_for_representations (b)
  4. L51
    specialize gaussian_multiply_for_representations (p)
  5. L52
    specialize gaussian_multiply_for_representations (x)
  6. L53
    specialize gaussian_multiply_for_representations (x1)
  7. L54
    specialize gaussian_multiply_for_representations (x2)
  8. L55
    specialize gaussian_multiply_for_representations (x3)
  9. L56
    specialize gaussian_multiply_for_representations (x4)
  10. L57
    specialize gaussian_multiply_for_representations (x5)
10Use earlier factsL58–63

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

  1. L58
    specialize gaussian_multiply_for_representations (x6)
  2. L59
    specialize gaussian_multiply_for_representations (x7)
  3. L60
    apply gaussian_multiply_for_representations
  4. L61
    exact hA_witness_witness_witness_witness
  5. L62
    exact hB_witness_witness_witness_witness
  6. L63
    exact hAB
11Establish hqL64–73

Establish this local claim before using it. It is not an additional assumption.

  1. L64
    have hq : ZPairRep(q,x · x8 + x1 · x9 + (x2 · x11 + x3 · x10),x · x9 + x1 · x8 + (x2 · x10 + x3 · x11),x · x10 + x1 · x11 + (x2 · x8 + x3 · x9),x · x11 + x1 · x10 + (x2 · x9 + x3 · x8))Definitions: ZPairRep(q,x · x8 + x1 · x9 + (x2 · x11 + x3 · x10),x · x9 + x1 · x8 + (x2 · x10 + x3 · x11),x · x10 + x1 · x11 + (x2 · x8 + x3 · x9),x · x11 + x1 · x10 + (x2 · x9 + x3 · x8))Original native command in the exact edition
  2. L65
    specialize gaussian_multiply_for_representations (a)
  3. L66
    specialize gaussian_multiply_for_representations (c)
  4. L67
    specialize gaussian_multiply_for_representations (q)
  5. L68
    specialize gaussian_multiply_for_representations (x)
  6. L69
    specialize gaussian_multiply_for_representations (x1)
  7. L70
    specialize gaussian_multiply_for_representations (x2)
  8. L71
    specialize gaussian_multiply_for_representations (x3)
  9. L72
    specialize gaussian_multiply_for_representations (x8)
  10. L73
    specialize gaussian_multiply_for_representations (x9)
12Use earlier factsL74–79

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

  1. L74
    specialize gaussian_multiply_for_representations (x10)
  2. L75
    specialize gaussian_multiply_for_representations (x11)
  3. L76
    apply gaussian_multiply_for_representations
  4. L77
    exact hA_witness_witness_witness_witness
  5. L78
    exact hC_witness_witness_witness_witness
  6. L79
    exact hAC
13Establish hsL80–89

Establish this local claim before using it. It is not an additional assumption.

  1. L80
    have hs : ZPairRep(s,x4 + x8,x5 + x9,x6 + x10,x7 + x11)Definitions: ZPairRep(s,x4 + x8,x5 + x9,x6 + x10,x7 + x11)Original native command in the exact edition
  2. L81
    specialize gaussian_add_for_representations (b)
  3. L82
    specialize gaussian_add_for_representations (c)
  4. L83
    specialize gaussian_add_for_representations (s)
  5. L84
    specialize gaussian_add_for_representations (x4)
  6. L85
    specialize gaussian_add_for_representations (x5)
  7. L86
    specialize gaussian_add_for_representations (x6)
  8. L87
    specialize gaussian_add_for_representations (x7)
  9. L88
    specialize gaussian_add_for_representations (x8)
  10. L89
    specialize gaussian_add_for_representations (x9)
14Use earlier factsL90–95

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

  1. L90
    specialize gaussian_add_for_representations (x10)
  2. L91
    specialize gaussian_add_for_representations (x11)
  3. L92
    apply gaussian_add_for_representations
  4. L93
    exact hB_witness_witness_witness_witness
  5. L94
    exact hC_witness_witness_witness_witness
  6. L95
    exact hBC
15Establish htL96–105

Establish this local claim before using it. It is not an additional assumption.

  1. L96
    have ht : ZPairRep(t,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6) + (x · x8 + x1 · x9 + (x2 · x11 + x3 · x10)),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7) + (x · x9 + x1 · x8 + (x2 · x10 + x3 · x11)),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x · x10 + x1 · x11 + (x2 · x8 + x3 · x9)),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x · x11 + x1 · x10 + (x2 · x9 + x3 · x8)))Definitions: ZPairRep(t,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6) + (x · x8 + x1 · x9 + (x2 · x11 + x3 · x10)),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7) + (x · x9 + x1 · x8 + (x2 · x10 + x3 · x11)),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x · x10 + x1 · x11 + (x2 · x8 + x3 · x9)),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x · x11 + x1 · x10 + (x2 · x9 + x3 · x8)))Original native command in the exact edition
  2. L97
    specialize gaussian_add_for_representations (p)
  3. L98
    specialize gaussian_add_for_representations (q)
  4. L99
    specialize gaussian_add_for_representations (t)
  5. L100
    specialize gaussian_add_for_representations (((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6)))))))
  6. L101
    specialize gaussian_add_for_representations (((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7)))))))
  7. L102
    specialize gaussian_add_for_representations (((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5)))))))
  8. L103
    specialize gaussian_add_for_representations (((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4)))))))
  9. L104
    specialize gaussian_add_for_representations (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))
  10. L105
    specialize gaussian_add_for_representations (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))
16Use earlier factsL106–115

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

  1. L106
    specialize gaussian_add_for_representations (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))
  2. L107
    specialize gaussian_add_for_representations (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))
  3. L108
    apply gaussian_add_for_representations
  4. L109
    exact hp
  5. L110
    exact hq
  6. L111
    exact hPQ
  7. L112
    specialize gaussian_multiply_of_representations (a)
  8. L113
    specialize gaussian_multiply_of_representations (s)
  9. L114
    specialize gaussian_multiply_of_representations (t)
  10. L115
    specialize gaussian_multiply_of_representations (x)
17Use earlier factsL116–125

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

  1. L116
    specialize gaussian_multiply_of_representations (x1)
  2. L117
    specialize gaussian_multiply_of_representations (x2)
  3. L118
    specialize gaussian_multiply_of_representations (x3)
  4. L119
    specialize gaussian_multiply_of_representations (((x4) + (x8)))
  5. L120
    specialize gaussian_multiply_of_representations (((x5) + (x9)))
  6. L121
    specialize gaussian_multiply_of_representations (((x6) + (x10)))
  7. L122
    specialize gaussian_multiply_of_representations (((x7) + (x11)))
  8. L123
    apply gaussian_multiply_of_representations
  9. L124
    exact hA_witness_witness_witness_witness
  10. L125
    exact hs
18Use earlier factsL126–135

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

  1. L126
    specialize gaussian_representation_integer_transport (t)
  2. L127
    specialize gaussian_representation_integer_transport (((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) + (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))))
  3. L128
    specialize gaussian_representation_integer_transport (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) + (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))))
  4. L129
    specialize gaussian_representation_integer_transport (((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))))
  5. L130
    specialize gaussian_representation_integer_transport (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))))
  6. L131
    specialize gaussian_representation_integer_transport (((((((x) * (((x4) + (x8))))) + (((x1) * (((x5) + (x9))))))) + (((((x2) * (((x7) + (x11))))) + (((x3) * (((x6) + (x10)))))))))
  7. L132
    specialize gaussian_representation_integer_transport (((((((x) * (((x5) + (x9))))) + (((x1) * (((x4) + (x8))))))) + (((((x2) * (((x6) + (x10))))) + (((x3) * (((x7) + (x11)))))))))
  8. L133
    specialize gaussian_representation_integer_transport (((((((x) * (((x6) + (x10))))) + (((x1) * (((x7) + (x11))))))) + (((((x2) * (((x4) + (x8))))) + (((x3) * (((x5) + (x9)))))))))
  9. L134
    specialize gaussian_representation_integer_transport (((((((x) * (((x7) + (x11))))) + (((x1) * (((x6) + (x10))))))) + (((((x2) * (((x5) + (x9))))) + (((x3) * (((x4) + (x8)))))))))
  10. L135
    apply gaussian_representation_integer_transport
19Use earlier factsL136–145

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

  1. L136
    specialize gaussian_equal_symmetric (((((((x) * (((x4) + (x8))))) + (((x1) * (((x5) + (x9))))))) + (((((x2) * (((x7) + (x11))))) + (((x3) * (((x6) + (x10)))))))))
  2. L137
    specialize gaussian_equal_symmetric (((((((x) * (((x5) + (x9))))) + (((x1) * (((x4) + (x8))))))) + (((((x2) * (((x6) + (x10))))) + (((x3) * (((x7) + (x11)))))))))
  3. L138
    specialize gaussian_equal_symmetric (((((((x) * (((x6) + (x10))))) + (((x1) * (((x7) + (x11))))))) + (((((x2) * (((x4) + (x8))))) + (((x3) * (((x5) + (x9)))))))))
  4. L139
    specialize gaussian_equal_symmetric (((((((x) * (((x7) + (x11))))) + (((x1) * (((x6) + (x10))))))) + (((((x2) * (((x5) + (x9))))) + (((x3) * (((x4) + (x8)))))))))
  5. L140
    specialize gaussian_equal_symmetric (((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) + (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))))
  6. L141
    specialize gaussian_equal_symmetric (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) + (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))))
  7. L142
    specialize gaussian_equal_symmetric (((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))))
  8. L143
    specialize gaussian_equal_symmetric (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))))
  9. L144
    apply gaussian_equal_symmetric
  10. L145
    specialize gaussian_ring_raw_multiply_add_distributive (x)
20Use earlier factsL146–155

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

  1. L146
    specialize gaussian_ring_raw_multiply_add_distributive (x1)
  2. L147
    specialize gaussian_ring_raw_multiply_add_distributive (x2)
  3. L148
    specialize gaussian_ring_raw_multiply_add_distributive (x3)
  4. L149
    specialize gaussian_ring_raw_multiply_add_distributive (x4)
  5. L150
    specialize gaussian_ring_raw_multiply_add_distributive (x5)
  6. L151
    specialize gaussian_ring_raw_multiply_add_distributive (x6)
  7. L152
    specialize gaussian_ring_raw_multiply_add_distributive (x7)
  8. L153
    specialize gaussian_ring_raw_multiply_add_distributive (x8)
  9. L154
    specialize gaussian_ring_raw_multiply_add_distributive (x9)
  10. L155
    specialize gaussian_ring_raw_multiply_add_distributive (x10)
21Use earlier factsL156–158

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

  1. L156
    specialize gaussian_ring_raw_multiply_add_distributive (x11)
  2. L157
    apply gaussian_ring_raw_multiply_add_distributive
  3. L158
    exact ht

Library-wide reading audit

Original defined command ledger · 158 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro s
  5. 0005intro p
  6. 0006intro q
  7. 0007intro t
  8. 0008intro hBC
  9. 0009intro hAB
  10. 0010intro hAC
  11. 0011intro hPQ
  12. 0012have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  13. 0013specialize gaussian_valid_has_representation (a)
  14. 0014apply gaussian_valid_has_representation
  15. 0015specialize gaussian_multiply_input_left_valid (a)
  16. 0016specialize gaussian_multiply_input_left_valid (b)
  17. 0017specialize gaussian_multiply_input_left_valid (p)
  18. 0018apply gaussian_multiply_input_left_valid
  19. 0019exact hAB
  20. 0020cases hA
  21. 0021cases hA_witness
  22. 0022cases hA_witness_witness
  23. 0023cases hA_witness_witness_witness
  24. 0024have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)
  25. 0025specialize gaussian_valid_has_representation (b)
  26. 0026apply gaussian_valid_has_representation
  27. 0027specialize gaussian_multiply_input_right_valid (a)
  28. 0028specialize gaussian_multiply_input_right_valid (b)
  29. 0029specialize gaussian_multiply_input_right_valid (p)
  30. 0030apply gaussian_multiply_input_right_valid
  31. 0031exact hAB
  32. 0032cases hB
  33. 0033cases hB_witness
  34. 0034cases hB_witness_witness
  35. 0035cases hB_witness_witness_witness
  36. 0036have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)
  37. 0037specialize gaussian_valid_has_representation (c)
  38. 0038apply gaussian_valid_has_representation
  39. 0039specialize gaussian_multiply_input_right_valid (a)
  40. 0040specialize gaussian_multiply_input_right_valid (c)
  41. 0041specialize gaussian_multiply_input_right_valid (q)
  42. 0042apply gaussian_multiply_input_right_valid
  43. 0043exact hAC
  44. 0044cases hC
  45. 0045cases hC_witness
  46. 0046cases hC_witness_witness
  47. 0047cases hC_witness_witness_witness
  48. 0048have hp : ZPairRep(p,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4))
  49. 0049specialize gaussian_multiply_for_representations (a)
  50. 0050specialize gaussian_multiply_for_representations (b)
  51. 0051specialize gaussian_multiply_for_representations (p)
  52. 0052specialize gaussian_multiply_for_representations (x)
  53. 0053specialize gaussian_multiply_for_representations (x1)
  54. 0054specialize gaussian_multiply_for_representations (x2)
  55. 0055specialize gaussian_multiply_for_representations (x3)
  56. 0056specialize gaussian_multiply_for_representations (x4)
  57. 0057specialize gaussian_multiply_for_representations (x5)
  58. 0058specialize gaussian_multiply_for_representations (x6)
  59. 0059specialize gaussian_multiply_for_representations (x7)
  60. 0060apply gaussian_multiply_for_representations
  61. 0061exact hA_witness_witness_witness_witness
  62. 0062exact hB_witness_witness_witness_witness
  63. 0063exact hAB
  64. 0064have hq : ZPairRep(q,x · x8 + x1 · x9 + (x2 · x11 + x3 · x10),x · x9 + x1 · x8 + (x2 · x10 + x3 · x11),x · x10 + x1 · x11 + (x2 · x8 + x3 · x9),x · x11 + x1 · x10 + (x2 · x9 + x3 · x8))
  65. 0065specialize gaussian_multiply_for_representations (a)
  66. 0066specialize gaussian_multiply_for_representations (c)
  67. 0067specialize gaussian_multiply_for_representations (q)
  68. 0068specialize gaussian_multiply_for_representations (x)
  69. 0069specialize gaussian_multiply_for_representations (x1)
  70. 0070specialize gaussian_multiply_for_representations (x2)
  71. 0071specialize gaussian_multiply_for_representations (x3)
  72. 0072specialize gaussian_multiply_for_representations (x8)
  73. 0073specialize gaussian_multiply_for_representations (x9)
  74. 0074specialize gaussian_multiply_for_representations (x10)
  75. 0075specialize gaussian_multiply_for_representations (x11)
  76. 0076apply gaussian_multiply_for_representations
  77. 0077exact hA_witness_witness_witness_witness
  78. 0078exact hC_witness_witness_witness_witness
  79. 0079exact hAC
  80. 0080have hs : ZPairRep(s,x4 + x8,x5 + x9,x6 + x10,x7 + x11)
  81. 0081specialize gaussian_add_for_representations (b)
  82. 0082specialize gaussian_add_for_representations (c)
  83. 0083specialize gaussian_add_for_representations (s)
  84. 0084specialize gaussian_add_for_representations (x4)
  85. 0085specialize gaussian_add_for_representations (x5)
  86. 0086specialize gaussian_add_for_representations (x6)
  87. 0087specialize gaussian_add_for_representations (x7)
  88. 0088specialize gaussian_add_for_representations (x8)
  89. 0089specialize gaussian_add_for_representations (x9)
  90. 0090specialize gaussian_add_for_representations (x10)
  91. 0091specialize gaussian_add_for_representations (x11)
  92. 0092apply gaussian_add_for_representations
  93. 0093exact hB_witness_witness_witness_witness
  94. 0094exact hC_witness_witness_witness_witness
  95. 0095exact hBC
  96. 0096have ht : ZPairRep(t,x · x4 + x1 · x5 + (x2 · x7 + x3 · x6) + (x · x8 + x1 · x9 + (x2 · x11 + x3 · x10)),x · x5 + x1 · x4 + (x2 · x6 + x3 · x7) + (x · x9 + x1 · x8 + (x2 · x10 + x3 · x11)),x · x6 + x1 · x7 + (x2 · x4 + x3 · x5) + (x · x10 + x1 · x11 + (x2 · x8 + x3 · x9)),x · x7 + x1 · x6 + (x2 · x5 + x3 · x4) + (x · x11 + x1 · x10 + (x2 · x9 + x3 · x8)))
  97. 0097specialize gaussian_add_for_representations (p)
  98. 0098specialize gaussian_add_for_representations (q)
  99. 0099specialize gaussian_add_for_representations (t)
  100. 0100specialize gaussian_add_for_representations (((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6)))))))
  101. 0101specialize gaussian_add_for_representations (((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7)))))))
  102. 0102specialize gaussian_add_for_representations (((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5)))))))
  103. 0103specialize gaussian_add_for_representations (((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4)))))))
  104. 0104specialize gaussian_add_for_representations (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))
  105. 0105specialize gaussian_add_for_representations (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))
  106. 0106specialize gaussian_add_for_representations (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))
  107. 0107specialize gaussian_add_for_representations (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))
  108. 0108apply gaussian_add_for_representations
  109. 0109exact hp
  110. 0110exact hq
  111. 0111exact hPQ
  112. 0112specialize gaussian_multiply_of_representations (a)
  113. 0113specialize gaussian_multiply_of_representations (s)
  114. 0114specialize gaussian_multiply_of_representations (t)
  115. 0115specialize gaussian_multiply_of_representations (x)
  116. 0116specialize gaussian_multiply_of_representations (x1)
  117. 0117specialize gaussian_multiply_of_representations (x2)
  118. 0118specialize gaussian_multiply_of_representations (x3)
  119. 0119specialize gaussian_multiply_of_representations (((x4) + (x8)))
  120. 0120specialize gaussian_multiply_of_representations (((x5) + (x9)))
  121. 0121specialize gaussian_multiply_of_representations (((x6) + (x10)))
  122. 0122specialize gaussian_multiply_of_representations (((x7) + (x11)))
  123. 0123apply gaussian_multiply_of_representations
  124. 0124exact hA_witness_witness_witness_witness
  125. 0125exact hs
  126. 0126specialize gaussian_representation_integer_transport (t)
  127. 0127specialize gaussian_representation_integer_transport (((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) + (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))))
  128. 0128specialize gaussian_representation_integer_transport (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) + (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))))
  129. 0129specialize gaussian_representation_integer_transport (((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))))
  130. 0130specialize gaussian_representation_integer_transport (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))))
  131. 0131specialize gaussian_representation_integer_transport (((((((x) * (((x4) + (x8))))) + (((x1) * (((x5) + (x9))))))) + (((((x2) * (((x7) + (x11))))) + (((x3) * (((x6) + (x10)))))))))
  132. 0132specialize gaussian_representation_integer_transport (((((((x) * (((x5) + (x9))))) + (((x1) * (((x4) + (x8))))))) + (((((x2) * (((x6) + (x10))))) + (((x3) * (((x7) + (x11)))))))))
  133. 0133specialize gaussian_representation_integer_transport (((((((x) * (((x6) + (x10))))) + (((x1) * (((x7) + (x11))))))) + (((((x2) * (((x4) + (x8))))) + (((x3) * (((x5) + (x9)))))))))
  134. 0134specialize gaussian_representation_integer_transport (((((((x) * (((x7) + (x11))))) + (((x1) * (((x6) + (x10))))))) + (((((x2) * (((x5) + (x9))))) + (((x3) * (((x4) + (x8)))))))))
  135. 0135apply gaussian_representation_integer_transport
  136. 0136specialize gaussian_equal_symmetric (((((((x) * (((x4) + (x8))))) + (((x1) * (((x5) + (x9))))))) + (((((x2) * (((x7) + (x11))))) + (((x3) * (((x6) + (x10)))))))))
  137. 0137specialize gaussian_equal_symmetric (((((((x) * (((x5) + (x9))))) + (((x1) * (((x4) + (x8))))))) + (((((x2) * (((x6) + (x10))))) + (((x3) * (((x7) + (x11)))))))))
  138. 0138specialize gaussian_equal_symmetric (((((((x) * (((x6) + (x10))))) + (((x1) * (((x7) + (x11))))))) + (((((x2) * (((x4) + (x8))))) + (((x3) * (((x5) + (x9)))))))))
  139. 0139specialize gaussian_equal_symmetric (((((((x) * (((x7) + (x11))))) + (((x1) * (((x6) + (x10))))))) + (((((x2) * (((x5) + (x9))))) + (((x3) * (((x4) + (x8)))))))))
  140. 0140specialize gaussian_equal_symmetric (((((((((x) * (x4))) + (((x1) * (x5))))) + (((((x2) * (x7))) + (((x3) * (x6))))))) + (((((((x) * (x8))) + (((x1) * (x9))))) + (((((x2) * (x11))) + (((x3) * (x10)))))))))
  141. 0141specialize gaussian_equal_symmetric (((((((((x) * (x5))) + (((x1) * (x4))))) + (((((x2) * (x6))) + (((x3) * (x7))))))) + (((((((x) * (x9))) + (((x1) * (x8))))) + (((((x2) * (x10))) + (((x3) * (x11)))))))))
  142. 0142specialize gaussian_equal_symmetric (((((((((x) * (x6))) + (((x1) * (x7))))) + (((((x2) * (x4))) + (((x3) * (x5))))))) + (((((((x) * (x10))) + (((x1) * (x11))))) + (((((x2) * (x8))) + (((x3) * (x9)))))))))
  143. 0143specialize gaussian_equal_symmetric (((((((((x) * (x7))) + (((x1) * (x6))))) + (((((x2) * (x5))) + (((x3) * (x4))))))) + (((((((x) * (x11))) + (((x1) * (x10))))) + (((((x2) * (x9))) + (((x3) * (x8)))))))))
  144. 0144apply gaussian_equal_symmetric
  145. 0145specialize gaussian_ring_raw_multiply_add_distributive (x)
  146. 0146specialize gaussian_ring_raw_multiply_add_distributive (x1)
  147. 0147specialize gaussian_ring_raw_multiply_add_distributive (x2)
  148. 0148specialize gaussian_ring_raw_multiply_add_distributive (x3)
  149. 0149specialize gaussian_ring_raw_multiply_add_distributive (x4)
  150. 0150specialize gaussian_ring_raw_multiply_add_distributive (x5)
  151. 0151specialize gaussian_ring_raw_multiply_add_distributive (x6)
  152. 0152specialize gaussian_ring_raw_multiply_add_distributive (x7)
  153. 0153specialize gaussian_ring_raw_multiply_add_distributive (x8)
  154. 0154specialize gaussian_ring_raw_multiply_add_distributive (x9)
  155. 0155specialize gaussian_ring_raw_multiply_add_distributive (x10)
  156. 0156specialize gaussian_ring_raw_multiply_add_distributive (x11)
  157. 0157apply gaussian_ring_raw_multiply_add_distributive
  158. 0158exact ht