GF004C

gaussian_common_divisor_subtract

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A common Gaussian divisor divides an actual difference; quotient subtraction is constructed and verified in the real ring graph.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall d a b c. (exists gr_quotient_difference_first_divisor. (exists ge_first_rp_difference_first_divisorproduct ge_first_rn_difference_first_divisorproduct ge_first_ip_difference_first_divisorproduct ge_first_in_difference_first_divisorproduct ge_second_rp_difference_first_divisorproduct ge_second_rn_difference_first_divisorproduct ge_second_ip_difference_first_divisorproduct ge_second_in_difference_first_divisorproduct. ((exists ge_representation_real_code_difference_first_divisorproductfirst ge_representation_imaginary_code_difference_first_divisorproductfirst. (((d) = ((ge_representation_real_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst)) * S ((ge_representation_real_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst)) + ((ge_representation_imaginary_code_difference_first_divisorproductfirst) + (ge_representation_imaginary_code_difference_first_divisorproductfirst))) /\ ((exists ge_balance_positive_difference_first_divisorproductfirstreal ge_balance_negative_difference_first_divisorproductfirstreal. (((((ge_representation_real_code_difference_first_divisorproductfirst) = 2 * (ge_balance_positive_difference_first_divisorproductfirstreal) /\ (ge_balance_negative_difference_first_divisorproductfirstreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductfirstrealdecode. (((ge_representation_real_code_difference_first_divisorproductfirst) = 2 * ge_signed_half_difference_first_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductfirstreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductfirstreal) = S ge_signed_half_difference_first_divisorproductfirstrealdecode))) /\ ((ge_first_rp_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductfirstreal = (ge_first_rn_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductfirstreal))) /\ (exists ge_balance_positive_difference_first_divisorproductfirstimaginary ge_balance_negative_difference_first_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductfirst) = 2 * (ge_balance_positive_difference_first_divisorproductfirstimaginary) /\ (ge_balance_negative_difference_first_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductfirst) = 2 * ge_signed_half_difference_first_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductfirstimaginary) = S ge_signed_half_difference_first_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductfirstimaginary = (ge_first_in_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_first_divisorproductsecond ge_representation_imaginary_code_difference_first_divisorproductsecond. (((gr_quotient_difference_first_divisor) = ((ge_representation_real_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond)) * S ((ge_representation_real_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond)) + ((ge_representation_imaginary_code_difference_first_divisorproductsecond) + (ge_representation_imaginary_code_difference_first_divisorproductsecond))) /\ ((exists ge_balance_positive_difference_first_divisorproductsecondreal ge_balance_negative_difference_first_divisorproductsecondreal. (((((ge_representation_real_code_difference_first_divisorproductsecond) = 2 * (ge_balance_positive_difference_first_divisorproductsecondreal) /\ (ge_balance_negative_difference_first_divisorproductsecondreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductsecondrealdecode. (((ge_representation_real_code_difference_first_divisorproductsecond) = 2 * ge_signed_half_difference_first_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductsecondreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductsecondreal) = S ge_signed_half_difference_first_divisorproductsecondrealdecode))) /\ ((ge_second_rp_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductsecondreal = (ge_second_rn_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductsecondreal))) /\ (exists ge_balance_positive_difference_first_divisorproductsecondimaginary ge_balance_negative_difference_first_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductsecond) = 2 * (ge_balance_positive_difference_first_divisorproductsecondimaginary) /\ (ge_balance_negative_difference_first_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductsecond) = 2 * ge_signed_half_difference_first_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductsecondimaginary) = S ge_signed_half_difference_first_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_first_divisorproduct) + ge_balance_negative_difference_first_divisorproductsecondimaginary = (ge_second_in_difference_first_divisorproduct) + ge_balance_positive_difference_first_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_first_divisorproductoutput ge_representation_imaginary_code_difference_first_divisorproductoutput. (((a) = ((ge_representation_real_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput)) * S ((ge_representation_real_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput)) + ((ge_representation_imaginary_code_difference_first_divisorproductoutput) + (ge_representation_imaginary_code_difference_first_divisorproductoutput))) /\ ((exists ge_balance_positive_difference_first_divisorproductoutputreal ge_balance_negative_difference_first_divisorproductoutputreal. (((((ge_representation_real_code_difference_first_divisorproductoutput) = 2 * (ge_balance_positive_difference_first_divisorproductoutputreal) /\ (ge_balance_negative_difference_first_divisorproductoutputreal) = 0) \/ exists ge_signed_half_difference_first_divisorproductoutputrealdecode. (((ge_representation_real_code_difference_first_divisorproductoutput) = 2 * ge_signed_half_difference_first_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_first_divisorproductoutputreal) = 0) /\ (ge_balance_negative_difference_first_divisorproductoutputreal) = S ge_signed_half_difference_first_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))))))) + ge_balance_negative_difference_first_divisorproductoutputreal = (((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))))))) + ge_balance_positive_difference_first_divisorproductoutputreal))) /\ (exists ge_balance_positive_difference_first_divisorproductoutputimaginary ge_balance_negative_difference_first_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_difference_first_divisorproductoutput) = 2 * (ge_balance_positive_difference_first_divisorproductoutputimaginary) /\ (ge_balance_negative_difference_first_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_first_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_first_divisorproductoutput) = 2 * ge_signed_half_difference_first_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_first_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_first_divisorproductoutputimaginary) = S ge_signed_half_difference_first_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))))))) + ge_balance_negative_difference_first_divisorproductoutputimaginary = (((((((ge_first_rp_difference_first_divisorproduct) * (ge_second_in_difference_first_divisorproduct))) + (((ge_first_rn_difference_first_divisorproduct) * (ge_second_ip_difference_first_divisorproduct))))) + (((((ge_first_ip_difference_first_divisorproduct) * (ge_second_rn_difference_first_divisorproduct))) + (((ge_first_in_difference_first_divisorproduct) * (ge_second_rp_difference_first_divisorproduct))))))) + ge_balance_positive_difference_first_divisorproductoutputimaginary)))))))))) -> (exists gr_quotient_difference_second_divisor. (exists ge_first_rp_difference_second_divisorproduct ge_first_rn_difference_second_divisorproduct ge_first_ip_difference_second_divisorproduct ge_first_in_difference_second_divisorproduct ge_second_rp_difference_second_divisorproduct ge_second_rn_difference_second_divisorproduct ge_second_ip_difference_second_divisorproduct ge_second_in_difference_second_divisorproduct. ((exists ge_representation_real_code_difference_second_divisorproductfirst ge_representation_imaginary_code_difference_second_divisorproductfirst. (((d) = ((ge_representation_real_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst)) * S ((ge_representation_real_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst)) + ((ge_representation_imaginary_code_difference_second_divisorproductfirst) + (ge_representation_imaginary_code_difference_second_divisorproductfirst))) /\ ((exists ge_balance_positive_difference_second_divisorproductfirstreal ge_balance_negative_difference_second_divisorproductfirstreal. (((((ge_representation_real_code_difference_second_divisorproductfirst) = 2 * (ge_balance_positive_difference_second_divisorproductfirstreal) /\ (ge_balance_negative_difference_second_divisorproductfirstreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductfirstrealdecode. (((ge_representation_real_code_difference_second_divisorproductfirst) = 2 * ge_signed_half_difference_second_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductfirstreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductfirstreal) = S ge_signed_half_difference_second_divisorproductfirstrealdecode))) /\ ((ge_first_rp_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductfirstreal = (ge_first_rn_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductfirstreal))) /\ (exists ge_balance_positive_difference_second_divisorproductfirstimaginary ge_balance_negative_difference_second_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductfirst) = 2 * (ge_balance_positive_difference_second_divisorproductfirstimaginary) /\ (ge_balance_negative_difference_second_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductfirst) = 2 * ge_signed_half_difference_second_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductfirstimaginary) = S ge_signed_half_difference_second_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductfirstimaginary = (ge_first_in_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_second_divisorproductsecond ge_representation_imaginary_code_difference_second_divisorproductsecond. (((gr_quotient_difference_second_divisor) = ((ge_representation_real_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond)) * S ((ge_representation_real_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond)) + ((ge_representation_imaginary_code_difference_second_divisorproductsecond) + (ge_representation_imaginary_code_difference_second_divisorproductsecond))) /\ ((exists ge_balance_positive_difference_second_divisorproductsecondreal ge_balance_negative_difference_second_divisorproductsecondreal. (((((ge_representation_real_code_difference_second_divisorproductsecond) = 2 * (ge_balance_positive_difference_second_divisorproductsecondreal) /\ (ge_balance_negative_difference_second_divisorproductsecondreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductsecondrealdecode. (((ge_representation_real_code_difference_second_divisorproductsecond) = 2 * ge_signed_half_difference_second_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductsecondreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductsecondreal) = S ge_signed_half_difference_second_divisorproductsecondrealdecode))) /\ ((ge_second_rp_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductsecondreal = (ge_second_rn_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductsecondreal))) /\ (exists ge_balance_positive_difference_second_divisorproductsecondimaginary ge_balance_negative_difference_second_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductsecond) = 2 * (ge_balance_positive_difference_second_divisorproductsecondimaginary) /\ (ge_balance_negative_difference_second_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductsecond) = 2 * ge_signed_half_difference_second_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductsecondimaginary) = S ge_signed_half_difference_second_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_second_divisorproduct) + ge_balance_negative_difference_second_divisorproductsecondimaginary = (ge_second_in_difference_second_divisorproduct) + ge_balance_positive_difference_second_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_second_divisorproductoutput ge_representation_imaginary_code_difference_second_divisorproductoutput. (((b) = ((ge_representation_real_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput)) * S ((ge_representation_real_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput)) + ((ge_representation_imaginary_code_difference_second_divisorproductoutput) + (ge_representation_imaginary_code_difference_second_divisorproductoutput))) /\ ((exists ge_balance_positive_difference_second_divisorproductoutputreal ge_balance_negative_difference_second_divisorproductoutputreal. (((((ge_representation_real_code_difference_second_divisorproductoutput) = 2 * (ge_balance_positive_difference_second_divisorproductoutputreal) /\ (ge_balance_negative_difference_second_divisorproductoutputreal) = 0) \/ exists ge_signed_half_difference_second_divisorproductoutputrealdecode. (((ge_representation_real_code_difference_second_divisorproductoutput) = 2 * ge_signed_half_difference_second_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_second_divisorproductoutputreal) = 0) /\ (ge_balance_negative_difference_second_divisorproductoutputreal) = S ge_signed_half_difference_second_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))))))) + ge_balance_negative_difference_second_divisorproductoutputreal = (((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))))))) + ge_balance_positive_difference_second_divisorproductoutputreal))) /\ (exists ge_balance_positive_difference_second_divisorproductoutputimaginary ge_balance_negative_difference_second_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_difference_second_divisorproductoutput) = 2 * (ge_balance_positive_difference_second_divisorproductoutputimaginary) /\ (ge_balance_negative_difference_second_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_second_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_second_divisorproductoutput) = 2 * ge_signed_half_difference_second_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_second_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_second_divisorproductoutputimaginary) = S ge_signed_half_difference_second_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))))))) + ge_balance_negative_difference_second_divisorproductoutputimaginary = (((((((ge_first_rp_difference_second_divisorproduct) * (ge_second_in_difference_second_divisorproduct))) + (((ge_first_rn_difference_second_divisorproduct) * (ge_second_ip_difference_second_divisorproduct))))) + (((((ge_first_ip_difference_second_divisorproduct) * (ge_second_rn_difference_second_divisorproduct))) + (((ge_first_in_difference_second_divisorproduct) * (ge_second_rp_difference_second_divisorproduct))))))) + ge_balance_positive_difference_second_divisorproductoutputimaginary)))))))))) -> (exists ge_first_rp_difference_equation ge_first_rn_difference_equation ge_first_ip_difference_equation ge_first_in_difference_equation ge_second_rp_difference_equation ge_second_rn_difference_equation ge_second_ip_difference_equation ge_second_in_difference_equation. ((exists ge_representation_real_code_difference_equationfirst ge_representation_imaginary_code_difference_equationfirst. (((c) = ((ge_representation_real_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst)) * S ((ge_representation_real_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst)) + ((ge_representation_imaginary_code_difference_equationfirst) + (ge_representation_imaginary_code_difference_equationfirst))) /\ ((exists ge_balance_positive_difference_equationfirstreal ge_balance_negative_difference_equationfirstreal. (((((ge_representation_real_code_difference_equationfirst) = 2 * (ge_balance_positive_difference_equationfirstreal) /\ (ge_balance_negative_difference_equationfirstreal) = 0) \/ exists ge_signed_half_difference_equationfirstrealdecode. (((ge_representation_real_code_difference_equationfirst) = 2 * ge_signed_half_difference_equationfirstrealdecode + 1 /\ (ge_balance_positive_difference_equationfirstreal) = 0) /\ (ge_balance_negative_difference_equationfirstreal) = S ge_signed_half_difference_equationfirstrealdecode))) /\ ((ge_first_rp_difference_equation) + ge_balance_negative_difference_equationfirstreal = (ge_first_rn_difference_equation) + ge_balance_positive_difference_equationfirstreal))) /\ (exists ge_balance_positive_difference_equationfirstimaginary ge_balance_negative_difference_equationfirstimaginary. (((((ge_representation_imaginary_code_difference_equationfirst) = 2 * (ge_balance_positive_difference_equationfirstimaginary) /\ (ge_balance_negative_difference_equationfirstimaginary) = 0) \/ exists ge_signed_half_difference_equationfirstimaginarydecode. (((ge_representation_imaginary_code_difference_equationfirst) = 2 * ge_signed_half_difference_equationfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_equationfirstimaginary) = 0) /\ (ge_balance_negative_difference_equationfirstimaginary) = S ge_signed_half_difference_equationfirstimaginarydecode))) /\ ((ge_first_ip_difference_equation) + ge_balance_negative_difference_equationfirstimaginary = (ge_first_in_difference_equation) + ge_balance_positive_difference_equationfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_equationsecond ge_representation_imaginary_code_difference_equationsecond. (((b) = ((ge_representation_real_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond)) * S ((ge_representation_real_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond)) + ((ge_representation_imaginary_code_difference_equationsecond) + (ge_representation_imaginary_code_difference_equationsecond))) /\ ((exists ge_balance_positive_difference_equationsecondreal ge_balance_negative_difference_equationsecondreal. (((((ge_representation_real_code_difference_equationsecond) = 2 * (ge_balance_positive_difference_equationsecondreal) /\ (ge_balance_negative_difference_equationsecondreal) = 0) \/ exists ge_signed_half_difference_equationsecondrealdecode. (((ge_representation_real_code_difference_equationsecond) = 2 * ge_signed_half_difference_equationsecondrealdecode + 1 /\ (ge_balance_positive_difference_equationsecondreal) = 0) /\ (ge_balance_negative_difference_equationsecondreal) = S ge_signed_half_difference_equationsecondrealdecode))) /\ ((ge_second_rp_difference_equation) + ge_balance_negative_difference_equationsecondreal = (ge_second_rn_difference_equation) + ge_balance_positive_difference_equationsecondreal))) /\ (exists ge_balance_positive_difference_equationsecondimaginary ge_balance_negative_difference_equationsecondimaginary. (((((ge_representation_imaginary_code_difference_equationsecond) = 2 * (ge_balance_positive_difference_equationsecondimaginary) /\ (ge_balance_negative_difference_equationsecondimaginary) = 0) \/ exists ge_signed_half_difference_equationsecondimaginarydecode. (((ge_representation_imaginary_code_difference_equationsecond) = 2 * ge_signed_half_difference_equationsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_equationsecondimaginary) = 0) /\ (ge_balance_negative_difference_equationsecondimaginary) = S ge_signed_half_difference_equationsecondimaginarydecode))) /\ ((ge_second_ip_difference_equation) + ge_balance_negative_difference_equationsecondimaginary = (ge_second_in_difference_equation) + ge_balance_positive_difference_equationsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_equationoutput ge_representation_imaginary_code_difference_equationoutput. (((a) = ((ge_representation_real_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput)) * S ((ge_representation_real_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput)) + ((ge_representation_imaginary_code_difference_equationoutput) + (ge_representation_imaginary_code_difference_equationoutput))) /\ ((exists ge_balance_positive_difference_equationoutputreal ge_balance_negative_difference_equationoutputreal. (((((ge_representation_real_code_difference_equationoutput) = 2 * (ge_balance_positive_difference_equationoutputreal) /\ (ge_balance_negative_difference_equationoutputreal) = 0) \/ exists ge_signed_half_difference_equationoutputrealdecode. (((ge_representation_real_code_difference_equationoutput) = 2 * ge_signed_half_difference_equationoutputrealdecode + 1 /\ (ge_balance_positive_difference_equationoutputreal) = 0) /\ (ge_balance_negative_difference_equationoutputreal) = S ge_signed_half_difference_equationoutputrealdecode))) /\ ((((ge_first_rp_difference_equation) + (ge_second_rp_difference_equation))) + ge_balance_negative_difference_equationoutputreal = (((ge_first_rn_difference_equation) + (ge_second_rn_difference_equation))) + ge_balance_positive_difference_equationoutputreal))) /\ (exists ge_balance_positive_difference_equationoutputimaginary ge_balance_negative_difference_equationoutputimaginary. (((((ge_representation_imaginary_code_difference_equationoutput) = 2 * (ge_balance_positive_difference_equationoutputimaginary) /\ (ge_balance_negative_difference_equationoutputimaginary) = 0) \/ exists ge_signed_half_difference_equationoutputimaginarydecode. (((ge_representation_imaginary_code_difference_equationoutput) = 2 * ge_signed_half_difference_equationoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_equationoutputimaginary) = 0) /\ (ge_balance_negative_difference_equationoutputimaginary) = S ge_signed_half_difference_equationoutputimaginarydecode))) /\ ((((ge_first_ip_difference_equation) + (ge_second_ip_difference_equation))) + ge_balance_negative_difference_equationoutputimaginary = (((ge_first_in_difference_equation) + (ge_second_in_difference_equation))) + ge_balance_positive_difference_equationoutputimaginary))))))))) -> (exists gr_quotient_difference_result. (exists ge_first_rp_difference_resultproduct ge_first_rn_difference_resultproduct ge_first_ip_difference_resultproduct ge_first_in_difference_resultproduct ge_second_rp_difference_resultproduct ge_second_rn_difference_resultproduct ge_second_ip_difference_resultproduct ge_second_in_difference_resultproduct. ((exists ge_representation_real_code_difference_resultproductfirst ge_representation_imaginary_code_difference_resultproductfirst. (((d) = ((ge_representation_real_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst)) * S ((ge_representation_real_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst)) + ((ge_representation_imaginary_code_difference_resultproductfirst) + (ge_representation_imaginary_code_difference_resultproductfirst))) /\ ((exists ge_balance_positive_difference_resultproductfirstreal ge_balance_negative_difference_resultproductfirstreal. (((((ge_representation_real_code_difference_resultproductfirst) = 2 * (ge_balance_positive_difference_resultproductfirstreal) /\ (ge_balance_negative_difference_resultproductfirstreal) = 0) \/ exists ge_signed_half_difference_resultproductfirstrealdecode. (((ge_representation_real_code_difference_resultproductfirst) = 2 * ge_signed_half_difference_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_difference_resultproductfirstreal) = 0) /\ (ge_balance_negative_difference_resultproductfirstreal) = S ge_signed_half_difference_resultproductfirstrealdecode))) /\ ((ge_first_rp_difference_resultproduct) + ge_balance_negative_difference_resultproductfirstreal = (ge_first_rn_difference_resultproduct) + ge_balance_positive_difference_resultproductfirstreal))) /\ (exists ge_balance_positive_difference_resultproductfirstimaginary ge_balance_negative_difference_resultproductfirstimaginary. (((((ge_representation_imaginary_code_difference_resultproductfirst) = 2 * (ge_balance_positive_difference_resultproductfirstimaginary) /\ (ge_balance_negative_difference_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_difference_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductfirst) = 2 * ge_signed_half_difference_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_difference_resultproductfirstimaginary) = S ge_signed_half_difference_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_difference_resultproduct) + ge_balance_negative_difference_resultproductfirstimaginary = (ge_first_in_difference_resultproduct) + ge_balance_positive_difference_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_resultproductsecond ge_representation_imaginary_code_difference_resultproductsecond. (((gr_quotient_difference_result) = ((ge_representation_real_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond)) * S ((ge_representation_real_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond)) + ((ge_representation_imaginary_code_difference_resultproductsecond) + (ge_representation_imaginary_code_difference_resultproductsecond))) /\ ((exists ge_balance_positive_difference_resultproductsecondreal ge_balance_negative_difference_resultproductsecondreal. (((((ge_representation_real_code_difference_resultproductsecond) = 2 * (ge_balance_positive_difference_resultproductsecondreal) /\ (ge_balance_negative_difference_resultproductsecondreal) = 0) \/ exists ge_signed_half_difference_resultproductsecondrealdecode. (((ge_representation_real_code_difference_resultproductsecond) = 2 * ge_signed_half_difference_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_difference_resultproductsecondreal) = 0) /\ (ge_balance_negative_difference_resultproductsecondreal) = S ge_signed_half_difference_resultproductsecondrealdecode))) /\ ((ge_second_rp_difference_resultproduct) + ge_balance_negative_difference_resultproductsecondreal = (ge_second_rn_difference_resultproduct) + ge_balance_positive_difference_resultproductsecondreal))) /\ (exists ge_balance_positive_difference_resultproductsecondimaginary ge_balance_negative_difference_resultproductsecondimaginary. (((((ge_representation_imaginary_code_difference_resultproductsecond) = 2 * (ge_balance_positive_difference_resultproductsecondimaginary) /\ (ge_balance_negative_difference_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_difference_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductsecond) = 2 * ge_signed_half_difference_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_difference_resultproductsecondimaginary) = S ge_signed_half_difference_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_difference_resultproduct) + ge_balance_negative_difference_resultproductsecondimaginary = (ge_second_in_difference_resultproduct) + ge_balance_positive_difference_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_resultproductoutput ge_representation_imaginary_code_difference_resultproductoutput. (((c) = ((ge_representation_real_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput)) * S ((ge_representation_real_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput)) + ((ge_representation_imaginary_code_difference_resultproductoutput) + (ge_representation_imaginary_code_difference_resultproductoutput))) /\ ((exists ge_balance_positive_difference_resultproductoutputreal ge_balance_negative_difference_resultproductoutputreal. (((((ge_representation_real_code_difference_resultproductoutput) = 2 * (ge_balance_positive_difference_resultproductoutputreal) /\ (ge_balance_negative_difference_resultproductoutputreal) = 0) \/ exists ge_signed_half_difference_resultproductoutputrealdecode. (((ge_representation_real_code_difference_resultproductoutput) = 2 * ge_signed_half_difference_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_difference_resultproductoutputreal) = 0) /\ (ge_balance_negative_difference_resultproductoutputreal) = S ge_signed_half_difference_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_difference_resultproduct) * (ge_second_rp_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_rn_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_in_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_ip_difference_resultproduct))))))) + ge_balance_negative_difference_resultproductoutputreal = (((((((ge_first_rp_difference_resultproduct) * (ge_second_rn_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_rp_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_ip_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_in_difference_resultproduct))))))) + ge_balance_positive_difference_resultproductoutputreal))) /\ (exists ge_balance_positive_difference_resultproductoutputimaginary ge_balance_negative_difference_resultproductoutputimaginary. (((((ge_representation_imaginary_code_difference_resultproductoutput) = 2 * (ge_balance_positive_difference_resultproductoutputimaginary) /\ (ge_balance_negative_difference_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_difference_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_difference_resultproductoutput) = 2 * ge_signed_half_difference_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_difference_resultproductoutputimaginary) = S ge_signed_half_difference_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_resultproduct) * (ge_second_ip_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_in_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_rp_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_rn_difference_resultproduct))))))) + ge_balance_negative_difference_resultproductoutputimaginary = (((((((ge_first_rp_difference_resultproduct) * (ge_second_in_difference_resultproduct))) + (((ge_first_rn_difference_resultproduct) * (ge_second_ip_difference_resultproduct))))) + (((((ge_first_ip_difference_resultproduct) * (ge_second_rn_difference_resultproduct))) + (((ge_first_in_difference_resultproduct) * (ge_second_rp_difference_resultproduct))))))) + ge_balance_positive_difference_resultproductoutputimaginary))))))))))

Constructive proof overview

Generated structural guide

A common Gaussian divisor divides an actual difference; quotient subtraction is constructed and verified in the real ring graph.

The unchanged tactic script uses 8 declared prerequisites and contains 68 exact native proof lines.

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

Proof neighborhood

Direct dependencies

GF002C gaussian_subtract_exists GF0008 gaussian_multiply_input_right_valid GF0007 gaussian_multiply_input_left_valid GF0004 gaussian_add_input_left_valid gaussian_multiply_exists Alpha theorem; checked-use authorized GF0038 gaussian_multiply_add_distribute GF003A gaussian_add_cancel_right GF002F gaussian_multiply_output_transport

Direct dependents

GF0050 gaussian_common_divisor_euclidean_backward

Formal native tactic body

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

Read the argument

Proof checkpoints

68 script commands · 13 reading checkpoints · 4 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.

Named ingredients (7)
gaussian subtract existsgaussian multiply input right validgaussian multiply input left validgaussian add input left validgaussian multiply add distributegaussian add cancel rightgaussian multiply output transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–7

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

  1. L1
    intro d
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hA
  6. L6
    intro hB
  7. L7
    intro hdifference
02Separate the logical casesL8–9

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

  1. L8
    cases hA
  2. L9
    cases hB
03Establish hqL10–19

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

  1. L10
    have hq : ∃ q. ZPairAdd(q,x1,x)Definitions: ZPairAdd
  2. L11
    specialize gaussian_subtract_exists (x)
  3. L12
    specialize gaussian_subtract_exists (x1)
  4. L13
    apply gaussian_subtract_exists
  5. L14
    specialize gaussian_multiply_input_right_valid (d)
  6. L15
    specialize gaussian_multiply_input_right_valid (x)
  7. L16
    specialize gaussian_multiply_input_right_valid (a)
  8. L17
    apply gaussian_multiply_input_right_valid
  9. L18
    exact hA_witness
  10. L19
    specialize gaussian_multiply_input_right_valid (d)
04Use earlier factsL20–23

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

  1. L20
    specialize gaussian_multiply_input_right_valid (x1)
  2. L21
    specialize gaussian_multiply_input_right_valid (b)
  3. L22
    apply gaussian_multiply_input_right_valid
  4. L23
    exact hB_witness
05Separate the logical casesL24–24

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

  1. L24
    cases hq
06Establish hprodL25–34

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

  1. L25
    have hprod : ∃ p. GMul(d,x2,p)Definitions: GMul
  2. L26
    specialize gaussian_multiply_exists (d)
  3. L27
    specialize gaussian_multiply_exists (x2)
  4. L28
    apply gaussian_multiply_exists
  5. L29
    specialize gaussian_multiply_input_left_valid (d)
  6. L30
    specialize gaussian_multiply_input_left_valid (x)
  7. L31
    specialize gaussian_multiply_input_left_valid (a)
  8. L32
    apply gaussian_multiply_input_left_valid
  9. L33
    exact hA_witness
  10. L34
    specialize gaussian_add_input_left_valid (x2)
07Use earlier factsL35–38

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

  1. L35
    specialize gaussian_add_input_left_valid (x1)
  2. L36
    specialize gaussian_add_input_left_valid (x)
  3. L37
    apply gaussian_add_input_left_valid
  4. L38
    exact hq_witness
08Separate the logical casesL39–39

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

  1. L39
    cases hprod
09Establish hsumL40–49

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply add distribute.

  1. L40
    have hsum : ZPairAdd(x3,b,a)Definitions: ZPairAdd
  2. L41
    specialize gaussian_multiply_add_distribute (d)
  3. L42
    specialize gaussian_multiply_add_distribute (x2)
  4. L43
    specialize gaussian_multiply_add_distribute (x1)
  5. L44
    specialize gaussian_multiply_add_distribute (x)
  6. L45
    specialize gaussian_multiply_add_distribute (x3)
  7. L46
    specialize gaussian_multiply_add_distribute (b)
  8. L47
    specialize gaussian_multiply_add_distribute (a)
  9. L48
    apply gaussian_multiply_add_distribute
  10. L49
    exact hq_witness
10Use earlier factsL50–52

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

  1. L50
    exact hprod_witness
  2. L51
    exact hB_witness
  3. L52
    exact hA_witness
11Establish heqL53–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian add cancel right.

  1. L53
    have heq : x3=c
  2. L54
    specialize gaussian_add_cancel_right (x3)
  3. L55
    specialize gaussian_add_cancel_right (c)
  4. L56
    specialize gaussian_add_cancel_right (b)
  5. L57
    specialize gaussian_add_cancel_right (a)
  6. L58
    apply gaussian_add_cancel_right
  7. L59
    exact hsum
  8. L60
    exact hdifference
12Construct an explicit witnessL61–61

Supply the displayed value, then prove that it has the required property.

  1. L61
    exists (x2)
13Use earlier factsL62–68

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

  1. L62
    specialize gaussian_multiply_output_transport (d)
  2. L63
    specialize gaussian_multiply_output_transport (x2)
  3. L64
    specialize gaussian_multiply_output_transport (x3)
  4. L65
    specialize gaussian_multiply_output_transport (c)
  5. L66
    apply gaussian_multiply_output_transport
  6. L67
    exact heq
  7. L68
    exact hprod_witness

Library-wide reading audit

Original exact command ledger · 68 lines
  1. 0001intro d
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hA
  6. 0006intro hB
  7. 0007intro hdifference
  8. 0008cases hA
  9. 0009cases hB
  10. 0010have hq : exists q. (exists ge_first_rp_difference_quotient ge_first_rn_difference_quotient ge_first_ip_difference_quotient ge_first_in_difference_quotient ge_second_rp_difference_quotient ge_second_rn_difference_quotient ge_second_ip_difference_quotient ge_second_in_difference_quotient. ((exists ge_representation_real_code_difference_quotientfirst ge_representation_imaginary_code_difference_quotientfirst. (((q) = ((ge_representation_real_code_difference_quotientfirst) + (ge_representation_imaginary_code_difference_quotientfirst)) * S ((ge_representation_real_code_difference_quotientfirst) + (ge_representation_imaginary_code_difference_quotientfirst)) + ((ge_representation_imaginary_code_difference_quotientfirst) + (ge_representation_imaginary_code_difference_quotientfirst))) /\ ((exists ge_balance_positive_difference_quotientfirstreal ge_balance_negative_difference_quotientfirstreal. (((((ge_representation_real_code_difference_quotientfirst) = 2 * (ge_balance_positive_difference_quotientfirstreal) /\ (ge_balance_negative_difference_quotientfirstreal) = 0) \/ exists ge_signed_half_difference_quotientfirstrealdecode. (((ge_representation_real_code_difference_quotientfirst) = 2 * ge_signed_half_difference_quotientfirstrealdecode + 1 /\ (ge_balance_positive_difference_quotientfirstreal) = 0) /\ (ge_balance_negative_difference_quotientfirstreal) = S ge_signed_half_difference_quotientfirstrealdecode))) /\ ((ge_first_rp_difference_quotient) + ge_balance_negative_difference_quotientfirstreal = (ge_first_rn_difference_quotient) + ge_balance_positive_difference_quotientfirstreal))) /\ (exists ge_balance_positive_difference_quotientfirstimaginary ge_balance_negative_difference_quotientfirstimaginary. (((((ge_representation_imaginary_code_difference_quotientfirst) = 2 * (ge_balance_positive_difference_quotientfirstimaginary) /\ (ge_balance_negative_difference_quotientfirstimaginary) = 0) \/ exists ge_signed_half_difference_quotientfirstimaginarydecode. (((ge_representation_imaginary_code_difference_quotientfirst) = 2 * ge_signed_half_difference_quotientfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_quotientfirstimaginary) = 0) /\ (ge_balance_negative_difference_quotientfirstimaginary) = S ge_signed_half_difference_quotientfirstimaginarydecode))) /\ ((ge_first_ip_difference_quotient) + ge_balance_negative_difference_quotientfirstimaginary = (ge_first_in_difference_quotient) + ge_balance_positive_difference_quotientfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_quotientsecond ge_representation_imaginary_code_difference_quotientsecond. (((x1) = ((ge_representation_real_code_difference_quotientsecond) + (ge_representation_imaginary_code_difference_quotientsecond)) * S ((ge_representation_real_code_difference_quotientsecond) + (ge_representation_imaginary_code_difference_quotientsecond)) + ((ge_representation_imaginary_code_difference_quotientsecond) + (ge_representation_imaginary_code_difference_quotientsecond))) /\ ((exists ge_balance_positive_difference_quotientsecondreal ge_balance_negative_difference_quotientsecondreal. (((((ge_representation_real_code_difference_quotientsecond) = 2 * (ge_balance_positive_difference_quotientsecondreal) /\ (ge_balance_negative_difference_quotientsecondreal) = 0) \/ exists ge_signed_half_difference_quotientsecondrealdecode. (((ge_representation_real_code_difference_quotientsecond) = 2 * ge_signed_half_difference_quotientsecondrealdecode + 1 /\ (ge_balance_positive_difference_quotientsecondreal) = 0) /\ (ge_balance_negative_difference_quotientsecondreal) = S ge_signed_half_difference_quotientsecondrealdecode))) /\ ((ge_second_rp_difference_quotient) + ge_balance_negative_difference_quotientsecondreal = (ge_second_rn_difference_quotient) + ge_balance_positive_difference_quotientsecondreal))) /\ (exists ge_balance_positive_difference_quotientsecondimaginary ge_balance_negative_difference_quotientsecondimaginary. (((((ge_representation_imaginary_code_difference_quotientsecond) = 2 * (ge_balance_positive_difference_quotientsecondimaginary) /\ (ge_balance_negative_difference_quotientsecondimaginary) = 0) \/ exists ge_signed_half_difference_quotientsecondimaginarydecode. (((ge_representation_imaginary_code_difference_quotientsecond) = 2 * ge_signed_half_difference_quotientsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_quotientsecondimaginary) = 0) /\ (ge_balance_negative_difference_quotientsecondimaginary) = S ge_signed_half_difference_quotientsecondimaginarydecode))) /\ ((ge_second_ip_difference_quotient) + ge_balance_negative_difference_quotientsecondimaginary = (ge_second_in_difference_quotient) + ge_balance_positive_difference_quotientsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_quotientoutput ge_representation_imaginary_code_difference_quotientoutput. (((x) = ((ge_representation_real_code_difference_quotientoutput) + (ge_representation_imaginary_code_difference_quotientoutput)) * S ((ge_representation_real_code_difference_quotientoutput) + (ge_representation_imaginary_code_difference_quotientoutput)) + ((ge_representation_imaginary_code_difference_quotientoutput) + (ge_representation_imaginary_code_difference_quotientoutput))) /\ ((exists ge_balance_positive_difference_quotientoutputreal ge_balance_negative_difference_quotientoutputreal. (((((ge_representation_real_code_difference_quotientoutput) = 2 * (ge_balance_positive_difference_quotientoutputreal) /\ (ge_balance_negative_difference_quotientoutputreal) = 0) \/ exists ge_signed_half_difference_quotientoutputrealdecode. (((ge_representation_real_code_difference_quotientoutput) = 2 * ge_signed_half_difference_quotientoutputrealdecode + 1 /\ (ge_balance_positive_difference_quotientoutputreal) = 0) /\ (ge_balance_negative_difference_quotientoutputreal) = S ge_signed_half_difference_quotientoutputrealdecode))) /\ ((((ge_first_rp_difference_quotient) + (ge_second_rp_difference_quotient))) + ge_balance_negative_difference_quotientoutputreal = (((ge_first_rn_difference_quotient) + (ge_second_rn_difference_quotient))) + ge_balance_positive_difference_quotientoutputreal))) /\ (exists ge_balance_positive_difference_quotientoutputimaginary ge_balance_negative_difference_quotientoutputimaginary. (((((ge_representation_imaginary_code_difference_quotientoutput) = 2 * (ge_balance_positive_difference_quotientoutputimaginary) /\ (ge_balance_negative_difference_quotientoutputimaginary) = 0) \/ exists ge_signed_half_difference_quotientoutputimaginarydecode. (((ge_representation_imaginary_code_difference_quotientoutput) = 2 * ge_signed_half_difference_quotientoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_quotientoutputimaginary) = 0) /\ (ge_balance_negative_difference_quotientoutputimaginary) = S ge_signed_half_difference_quotientoutputimaginarydecode))) /\ ((((ge_first_ip_difference_quotient) + (ge_second_ip_difference_quotient))) + ge_balance_negative_difference_quotientoutputimaginary = (((ge_first_in_difference_quotient) + (ge_second_in_difference_quotient))) + ge_balance_positive_difference_quotientoutputimaginary)))))))))
  11. 0011specialize gaussian_subtract_exists (x)
  12. 0012specialize gaussian_subtract_exists (x1)
  13. 0013apply gaussian_subtract_exists
  14. 0014specialize gaussian_multiply_input_right_valid (d)
  15. 0015specialize gaussian_multiply_input_right_valid (x)
  16. 0016specialize gaussian_multiply_input_right_valid (a)
  17. 0017apply gaussian_multiply_input_right_valid
  18. 0018exact hA_witness
  19. 0019specialize gaussian_multiply_input_right_valid (d)
  20. 0020specialize gaussian_multiply_input_right_valid (x1)
  21. 0021specialize gaussian_multiply_input_right_valid (b)
  22. 0022apply gaussian_multiply_input_right_valid
  23. 0023exact hB_witness
  24. 0024cases hq
  25. 0025have hprod : exists p. (exists ge_first_rp_difference_constructed ge_first_rn_difference_constructed ge_first_ip_difference_constructed ge_first_in_difference_constructed ge_second_rp_difference_constructed ge_second_rn_difference_constructed ge_second_ip_difference_constructed ge_second_in_difference_constructed. ((exists ge_representation_real_code_difference_constructedfirst ge_representation_imaginary_code_difference_constructedfirst. (((d) = ((ge_representation_real_code_difference_constructedfirst) + (ge_representation_imaginary_code_difference_constructedfirst)) * S ((ge_representation_real_code_difference_constructedfirst) + (ge_representation_imaginary_code_difference_constructedfirst)) + ((ge_representation_imaginary_code_difference_constructedfirst) + (ge_representation_imaginary_code_difference_constructedfirst))) /\ ((exists ge_balance_positive_difference_constructedfirstreal ge_balance_negative_difference_constructedfirstreal. (((((ge_representation_real_code_difference_constructedfirst) = 2 * (ge_balance_positive_difference_constructedfirstreal) /\ (ge_balance_negative_difference_constructedfirstreal) = 0) \/ exists ge_signed_half_difference_constructedfirstrealdecode. (((ge_representation_real_code_difference_constructedfirst) = 2 * ge_signed_half_difference_constructedfirstrealdecode + 1 /\ (ge_balance_positive_difference_constructedfirstreal) = 0) /\ (ge_balance_negative_difference_constructedfirstreal) = S ge_signed_half_difference_constructedfirstrealdecode))) /\ ((ge_first_rp_difference_constructed) + ge_balance_negative_difference_constructedfirstreal = (ge_first_rn_difference_constructed) + ge_balance_positive_difference_constructedfirstreal))) /\ (exists ge_balance_positive_difference_constructedfirstimaginary ge_balance_negative_difference_constructedfirstimaginary. (((((ge_representation_imaginary_code_difference_constructedfirst) = 2 * (ge_balance_positive_difference_constructedfirstimaginary) /\ (ge_balance_negative_difference_constructedfirstimaginary) = 0) \/ exists ge_signed_half_difference_constructedfirstimaginarydecode. (((ge_representation_imaginary_code_difference_constructedfirst) = 2 * ge_signed_half_difference_constructedfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_constructedfirstimaginary) = 0) /\ (ge_balance_negative_difference_constructedfirstimaginary) = S ge_signed_half_difference_constructedfirstimaginarydecode))) /\ ((ge_first_ip_difference_constructed) + ge_balance_negative_difference_constructedfirstimaginary = (ge_first_in_difference_constructed) + ge_balance_positive_difference_constructedfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_constructedsecond ge_representation_imaginary_code_difference_constructedsecond. (((x2) = ((ge_representation_real_code_difference_constructedsecond) + (ge_representation_imaginary_code_difference_constructedsecond)) * S ((ge_representation_real_code_difference_constructedsecond) + (ge_representation_imaginary_code_difference_constructedsecond)) + ((ge_representation_imaginary_code_difference_constructedsecond) + (ge_representation_imaginary_code_difference_constructedsecond))) /\ ((exists ge_balance_positive_difference_constructedsecondreal ge_balance_negative_difference_constructedsecondreal. (((((ge_representation_real_code_difference_constructedsecond) = 2 * (ge_balance_positive_difference_constructedsecondreal) /\ (ge_balance_negative_difference_constructedsecondreal) = 0) \/ exists ge_signed_half_difference_constructedsecondrealdecode. (((ge_representation_real_code_difference_constructedsecond) = 2 * ge_signed_half_difference_constructedsecondrealdecode + 1 /\ (ge_balance_positive_difference_constructedsecondreal) = 0) /\ (ge_balance_negative_difference_constructedsecondreal) = S ge_signed_half_difference_constructedsecondrealdecode))) /\ ((ge_second_rp_difference_constructed) + ge_balance_negative_difference_constructedsecondreal = (ge_second_rn_difference_constructed) + ge_balance_positive_difference_constructedsecondreal))) /\ (exists ge_balance_positive_difference_constructedsecondimaginary ge_balance_negative_difference_constructedsecondimaginary. (((((ge_representation_imaginary_code_difference_constructedsecond) = 2 * (ge_balance_positive_difference_constructedsecondimaginary) /\ (ge_balance_negative_difference_constructedsecondimaginary) = 0) \/ exists ge_signed_half_difference_constructedsecondimaginarydecode. (((ge_representation_imaginary_code_difference_constructedsecond) = 2 * ge_signed_half_difference_constructedsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_constructedsecondimaginary) = 0) /\ (ge_balance_negative_difference_constructedsecondimaginary) = S ge_signed_half_difference_constructedsecondimaginarydecode))) /\ ((ge_second_ip_difference_constructed) + ge_balance_negative_difference_constructedsecondimaginary = (ge_second_in_difference_constructed) + ge_balance_positive_difference_constructedsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_constructedoutput ge_representation_imaginary_code_difference_constructedoutput. (((p) = ((ge_representation_real_code_difference_constructedoutput) + (ge_representation_imaginary_code_difference_constructedoutput)) * S ((ge_representation_real_code_difference_constructedoutput) + (ge_representation_imaginary_code_difference_constructedoutput)) + ((ge_representation_imaginary_code_difference_constructedoutput) + (ge_representation_imaginary_code_difference_constructedoutput))) /\ ((exists ge_balance_positive_difference_constructedoutputreal ge_balance_negative_difference_constructedoutputreal. (((((ge_representation_real_code_difference_constructedoutput) = 2 * (ge_balance_positive_difference_constructedoutputreal) /\ (ge_balance_negative_difference_constructedoutputreal) = 0) \/ exists ge_signed_half_difference_constructedoutputrealdecode. (((ge_representation_real_code_difference_constructedoutput) = 2 * ge_signed_half_difference_constructedoutputrealdecode + 1 /\ (ge_balance_positive_difference_constructedoutputreal) = 0) /\ (ge_balance_negative_difference_constructedoutputreal) = S ge_signed_half_difference_constructedoutputrealdecode))) /\ ((((((((ge_first_rp_difference_constructed) * (ge_second_rp_difference_constructed))) + (((ge_first_rn_difference_constructed) * (ge_second_rn_difference_constructed))))) + (((((ge_first_ip_difference_constructed) * (ge_second_in_difference_constructed))) + (((ge_first_in_difference_constructed) * (ge_second_ip_difference_constructed))))))) + ge_balance_negative_difference_constructedoutputreal = (((((((ge_first_rp_difference_constructed) * (ge_second_rn_difference_constructed))) + (((ge_first_rn_difference_constructed) * (ge_second_rp_difference_constructed))))) + (((((ge_first_ip_difference_constructed) * (ge_second_ip_difference_constructed))) + (((ge_first_in_difference_constructed) * (ge_second_in_difference_constructed))))))) + ge_balance_positive_difference_constructedoutputreal))) /\ (exists ge_balance_positive_difference_constructedoutputimaginary ge_balance_negative_difference_constructedoutputimaginary. (((((ge_representation_imaginary_code_difference_constructedoutput) = 2 * (ge_balance_positive_difference_constructedoutputimaginary) /\ (ge_balance_negative_difference_constructedoutputimaginary) = 0) \/ exists ge_signed_half_difference_constructedoutputimaginarydecode. (((ge_representation_imaginary_code_difference_constructedoutput) = 2 * ge_signed_half_difference_constructedoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_constructedoutputimaginary) = 0) /\ (ge_balance_negative_difference_constructedoutputimaginary) = S ge_signed_half_difference_constructedoutputimaginarydecode))) /\ ((((((((ge_first_rp_difference_constructed) * (ge_second_ip_difference_constructed))) + (((ge_first_rn_difference_constructed) * (ge_second_in_difference_constructed))))) + (((((ge_first_ip_difference_constructed) * (ge_second_rp_difference_constructed))) + (((ge_first_in_difference_constructed) * (ge_second_rn_difference_constructed))))))) + ge_balance_negative_difference_constructedoutputimaginary = (((((((ge_first_rp_difference_constructed) * (ge_second_in_difference_constructed))) + (((ge_first_rn_difference_constructed) * (ge_second_ip_difference_constructed))))) + (((((ge_first_ip_difference_constructed) * (ge_second_rn_difference_constructed))) + (((ge_first_in_difference_constructed) * (ge_second_rp_difference_constructed))))))) + ge_balance_positive_difference_constructedoutputimaginary)))))))))
  26. 0026specialize gaussian_multiply_exists (d)
  27. 0027specialize gaussian_multiply_exists (x2)
  28. 0028apply gaussian_multiply_exists
  29. 0029specialize gaussian_multiply_input_left_valid (d)
  30. 0030specialize gaussian_multiply_input_left_valid (x)
  31. 0031specialize gaussian_multiply_input_left_valid (a)
  32. 0032apply gaussian_multiply_input_left_valid
  33. 0033exact hA_witness
  34. 0034specialize gaussian_add_input_left_valid (x2)
  35. 0035specialize gaussian_add_input_left_valid (x1)
  36. 0036specialize gaussian_add_input_left_valid (x)
  37. 0037apply gaussian_add_input_left_valid
  38. 0038exact hq_witness
  39. 0039cases hprod
  40. 0040have hsum : exists ge_first_rp_difference_reconstructed ge_first_rn_difference_reconstructed ge_first_ip_difference_reconstructed ge_first_in_difference_reconstructed ge_second_rp_difference_reconstructed ge_second_rn_difference_reconstructed ge_second_ip_difference_reconstructed ge_second_in_difference_reconstructed. ((exists ge_representation_real_code_difference_reconstructedfirst ge_representation_imaginary_code_difference_reconstructedfirst. (((x3) = ((ge_representation_real_code_difference_reconstructedfirst) + (ge_representation_imaginary_code_difference_reconstructedfirst)) * S ((ge_representation_real_code_difference_reconstructedfirst) + (ge_representation_imaginary_code_difference_reconstructedfirst)) + ((ge_representation_imaginary_code_difference_reconstructedfirst) + (ge_representation_imaginary_code_difference_reconstructedfirst))) /\ ((exists ge_balance_positive_difference_reconstructedfirstreal ge_balance_negative_difference_reconstructedfirstreal. (((((ge_representation_real_code_difference_reconstructedfirst) = 2 * (ge_balance_positive_difference_reconstructedfirstreal) /\ (ge_balance_negative_difference_reconstructedfirstreal) = 0) \/ exists ge_signed_half_difference_reconstructedfirstrealdecode. (((ge_representation_real_code_difference_reconstructedfirst) = 2 * ge_signed_half_difference_reconstructedfirstrealdecode + 1 /\ (ge_balance_positive_difference_reconstructedfirstreal) = 0) /\ (ge_balance_negative_difference_reconstructedfirstreal) = S ge_signed_half_difference_reconstructedfirstrealdecode))) /\ ((ge_first_rp_difference_reconstructed) + ge_balance_negative_difference_reconstructedfirstreal = (ge_first_rn_difference_reconstructed) + ge_balance_positive_difference_reconstructedfirstreal))) /\ (exists ge_balance_positive_difference_reconstructedfirstimaginary ge_balance_negative_difference_reconstructedfirstimaginary. (((((ge_representation_imaginary_code_difference_reconstructedfirst) = 2 * (ge_balance_positive_difference_reconstructedfirstimaginary) /\ (ge_balance_negative_difference_reconstructedfirstimaginary) = 0) \/ exists ge_signed_half_difference_reconstructedfirstimaginarydecode. (((ge_representation_imaginary_code_difference_reconstructedfirst) = 2 * ge_signed_half_difference_reconstructedfirstimaginarydecode + 1 /\ (ge_balance_positive_difference_reconstructedfirstimaginary) = 0) /\ (ge_balance_negative_difference_reconstructedfirstimaginary) = S ge_signed_half_difference_reconstructedfirstimaginarydecode))) /\ ((ge_first_ip_difference_reconstructed) + ge_balance_negative_difference_reconstructedfirstimaginary = (ge_first_in_difference_reconstructed) + ge_balance_positive_difference_reconstructedfirstimaginary)))))) /\ ((exists ge_representation_real_code_difference_reconstructedsecond ge_representation_imaginary_code_difference_reconstructedsecond. (((b) = ((ge_representation_real_code_difference_reconstructedsecond) + (ge_representation_imaginary_code_difference_reconstructedsecond)) * S ((ge_representation_real_code_difference_reconstructedsecond) + (ge_representation_imaginary_code_difference_reconstructedsecond)) + ((ge_representation_imaginary_code_difference_reconstructedsecond) + (ge_representation_imaginary_code_difference_reconstructedsecond))) /\ ((exists ge_balance_positive_difference_reconstructedsecondreal ge_balance_negative_difference_reconstructedsecondreal. (((((ge_representation_real_code_difference_reconstructedsecond) = 2 * (ge_balance_positive_difference_reconstructedsecondreal) /\ (ge_balance_negative_difference_reconstructedsecondreal) = 0) \/ exists ge_signed_half_difference_reconstructedsecondrealdecode. (((ge_representation_real_code_difference_reconstructedsecond) = 2 * ge_signed_half_difference_reconstructedsecondrealdecode + 1 /\ (ge_balance_positive_difference_reconstructedsecondreal) = 0) /\ (ge_balance_negative_difference_reconstructedsecondreal) = S ge_signed_half_difference_reconstructedsecondrealdecode))) /\ ((ge_second_rp_difference_reconstructed) + ge_balance_negative_difference_reconstructedsecondreal = (ge_second_rn_difference_reconstructed) + ge_balance_positive_difference_reconstructedsecondreal))) /\ (exists ge_balance_positive_difference_reconstructedsecondimaginary ge_balance_negative_difference_reconstructedsecondimaginary. (((((ge_representation_imaginary_code_difference_reconstructedsecond) = 2 * (ge_balance_positive_difference_reconstructedsecondimaginary) /\ (ge_balance_negative_difference_reconstructedsecondimaginary) = 0) \/ exists ge_signed_half_difference_reconstructedsecondimaginarydecode. (((ge_representation_imaginary_code_difference_reconstructedsecond) = 2 * ge_signed_half_difference_reconstructedsecondimaginarydecode + 1 /\ (ge_balance_positive_difference_reconstructedsecondimaginary) = 0) /\ (ge_balance_negative_difference_reconstructedsecondimaginary) = S ge_signed_half_difference_reconstructedsecondimaginarydecode))) /\ ((ge_second_ip_difference_reconstructed) + ge_balance_negative_difference_reconstructedsecondimaginary = (ge_second_in_difference_reconstructed) + ge_balance_positive_difference_reconstructedsecondimaginary)))))) /\ (exists ge_representation_real_code_difference_reconstructedoutput ge_representation_imaginary_code_difference_reconstructedoutput. (((a) = ((ge_representation_real_code_difference_reconstructedoutput) + (ge_representation_imaginary_code_difference_reconstructedoutput)) * S ((ge_representation_real_code_difference_reconstructedoutput) + (ge_representation_imaginary_code_difference_reconstructedoutput)) + ((ge_representation_imaginary_code_difference_reconstructedoutput) + (ge_representation_imaginary_code_difference_reconstructedoutput))) /\ ((exists ge_balance_positive_difference_reconstructedoutputreal ge_balance_negative_difference_reconstructedoutputreal. (((((ge_representation_real_code_difference_reconstructedoutput) = 2 * (ge_balance_positive_difference_reconstructedoutputreal) /\ (ge_balance_negative_difference_reconstructedoutputreal) = 0) \/ exists ge_signed_half_difference_reconstructedoutputrealdecode. (((ge_representation_real_code_difference_reconstructedoutput) = 2 * ge_signed_half_difference_reconstructedoutputrealdecode + 1 /\ (ge_balance_positive_difference_reconstructedoutputreal) = 0) /\ (ge_balance_negative_difference_reconstructedoutputreal) = S ge_signed_half_difference_reconstructedoutputrealdecode))) /\ ((((ge_first_rp_difference_reconstructed) + (ge_second_rp_difference_reconstructed))) + ge_balance_negative_difference_reconstructedoutputreal = (((ge_first_rn_difference_reconstructed) + (ge_second_rn_difference_reconstructed))) + ge_balance_positive_difference_reconstructedoutputreal))) /\ (exists ge_balance_positive_difference_reconstructedoutputimaginary ge_balance_negative_difference_reconstructedoutputimaginary. (((((ge_representation_imaginary_code_difference_reconstructedoutput) = 2 * (ge_balance_positive_difference_reconstructedoutputimaginary) /\ (ge_balance_negative_difference_reconstructedoutputimaginary) = 0) \/ exists ge_signed_half_difference_reconstructedoutputimaginarydecode. (((ge_representation_imaginary_code_difference_reconstructedoutput) = 2 * ge_signed_half_difference_reconstructedoutputimaginarydecode + 1 /\ (ge_balance_positive_difference_reconstructedoutputimaginary) = 0) /\ (ge_balance_negative_difference_reconstructedoutputimaginary) = S ge_signed_half_difference_reconstructedoutputimaginarydecode))) /\ ((((ge_first_ip_difference_reconstructed) + (ge_second_ip_difference_reconstructed))) + ge_balance_negative_difference_reconstructedoutputimaginary = (((ge_first_in_difference_reconstructed) + (ge_second_in_difference_reconstructed))) + ge_balance_positive_difference_reconstructedoutputimaginary))))))))
  41. 0041specialize gaussian_multiply_add_distribute (d)
  42. 0042specialize gaussian_multiply_add_distribute (x2)
  43. 0043specialize gaussian_multiply_add_distribute (x1)
  44. 0044specialize gaussian_multiply_add_distribute (x)
  45. 0045specialize gaussian_multiply_add_distribute (x3)
  46. 0046specialize gaussian_multiply_add_distribute (b)
  47. 0047specialize gaussian_multiply_add_distribute (a)
  48. 0048apply gaussian_multiply_add_distribute
  49. 0049exact hq_witness
  50. 0050exact hprod_witness
  51. 0051exact hB_witness
  52. 0052exact hA_witness
  53. 0053have heq : x3=c
  54. 0054specialize gaussian_add_cancel_right (x3)
  55. 0055specialize gaussian_add_cancel_right (c)
  56. 0056specialize gaussian_add_cancel_right (b)
  57. 0057specialize gaussian_add_cancel_right (a)
  58. 0058apply gaussian_add_cancel_right
  59. 0059exact hsum
  60. 0060exact hdifference
  61. 0061exists (x2)
  62. 0062specialize gaussian_multiply_output_transport (d)
  63. 0063specialize gaussian_multiply_output_transport (x2)
  64. 0064specialize gaussian_multiply_output_transport (x3)
  65. 0065specialize gaussian_multiply_output_transport (c)
  66. 0066apply gaussian_multiply_output_transport
  67. 0067exact heq
  68. 0068exact hprod_witness