GProperNormDivisor(d,z,N)

((~(exists gr_inverse_gaussianfactorizationnonunit. (exists ge_first_rp_gaussianfactorizationnonunitidentity ge_first_rn_gaussianfactorizationnonunitidentity ge_first_ip_gaussianfactorizationnonunitidentity ge_first_in_gaussianfactorizationnonunitidentity ge_second_rp_gaussianfactorizationnonunitidentity ge_second_rn_gaussianfactorizationnonunitidentity ge_second_ip_gaussianfactorizationnonunitidentity ge_second_in_gaussianfactorizationnonunitidentity. ((exists ge_representation_real_code_gaussianfactorizationnonunitidentityfirst ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst. ((((d)) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstreal = (ge_first_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityfirst) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentityfirstimaginary = (ge_first_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationnonunitidentitysecond ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond. (((gr_inverse_gaussianfactorizationnonunit) = ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondreal = (ge_second_rn_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentitysecond) = 2 * ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationnonunitidentity) + ge_balance_negative_gaussianfactorizationnonunitidentitysecondimaginary = (ge_second_in_gaussianfactorizationnonunitidentity) + ge_balance_positive_gaussianfactorizationnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationnonunitidentityoutput ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput. (((6) = ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) * S ((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) + (ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal. (((((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputreal = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnonunitidentityoutput) = 2 * ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary) = S ge_signed_half_gaussianfactorizationnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))))))) + ge_balance_negative_gaussianfactorizationnonunitidentityoutputimaginary = (((((((ge_first_rp_gaussianfactorizationnonunitidentity) * (ge_second_in_gaussianfactorizationnonunitidentity))) + (((ge_first_rn_gaussianfactorizationnonunitidentity) * (ge_second_ip_gaussianfactorizationnonunitidentity))))) + (((((ge_first_ip_gaussianfactorizationnonunitidentity) * (ge_second_rn_gaussianfactorizationnonunitidentity))) + (((ge_first_in_gaussianfactorizationnonunitidentity) * (ge_second_rp_gaussianfactorizationnonunitidentity))))))) + ge_balance_positive_gaussianfactorizationnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_gaussianfactorizationquotient. (exists ge_first_rp_gaussianfactorizationquotientproduct ge_first_rn_gaussianfactorizationquotientproduct ge_first_ip_gaussianfactorizationquotientproduct ge_first_in_gaussianfactorizationquotientproduct ge_second_rp_gaussianfactorizationquotientproduct ge_second_rn_gaussianfactorizationquotientproduct ge_second_ip_gaussianfactorizationquotientproduct ge_second_in_gaussianfactorizationquotientproduct. ((exists ge_representation_real_code_gaussianfactorizationquotientproductfirst ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst. ((((d)) = ((ge_representation_real_code_gaussianfactorizationquotientproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst)) * S ((ge_representation_real_code_gaussianfactorizationquotientproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst)) + ((ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst))) /\ ((exists ge_balance_positive_gaussianfactorizationquotientproductfirstreal ge_balance_negative_gaussianfactorizationquotientproductfirstreal. (((((ge_representation_real_code_gaussianfactorizationquotientproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductfirstreal) /\ (ge_balance_negative_gaussianfactorizationquotientproductfirstreal) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductfirstrealdecode. (((ge_representation_real_code_gaussianfactorizationquotientproductfirst) = 2 * ge_signed_half_gaussianfactorizationquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductfirstreal) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductfirstreal) = S ge_signed_half_gaussianfactorizationquotientproductfirstrealdecode))) /\ ((ge_first_rp_gaussianfactorizationquotientproduct) + ge_balance_negative_gaussianfactorizationquotientproductfirstreal = (ge_first_rn_gaussianfactorizationquotientproduct) + ge_balance_positive_gaussianfactorizationquotientproductfirstreal))) /\ (exists ge_balance_positive_gaussianfactorizationquotientproductfirstimaginary ge_balance_negative_gaussianfactorizationquotientproductfirstimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductfirstimaginary) /\ (ge_balance_negative_gaussianfactorizationquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationquotientproductfirst) = 2 * ge_signed_half_gaussianfactorizationquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductfirstimaginary) = S ge_signed_half_gaussianfactorizationquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_gaussianfactorizationquotientproduct) + ge_balance_negative_gaussianfactorizationquotientproductfirstimaginary = (ge_first_in_gaussianfactorizationquotientproduct) + ge_balance_positive_gaussianfactorizationquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_gaussianfactorizationquotientproductsecond ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond. (((gr_quotient_gaussianfactorizationquotient) = ((ge_representation_real_code_gaussianfactorizationquotientproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond)) * S ((ge_representation_real_code_gaussianfactorizationquotientproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond)) + ((ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond))) /\ ((exists ge_balance_positive_gaussianfactorizationquotientproductsecondreal ge_balance_negative_gaussianfactorizationquotientproductsecondreal. (((((ge_representation_real_code_gaussianfactorizationquotientproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductsecondreal) /\ (ge_balance_negative_gaussianfactorizationquotientproductsecondreal) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductsecondrealdecode. (((ge_representation_real_code_gaussianfactorizationquotientproductsecond) = 2 * ge_signed_half_gaussianfactorizationquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductsecondreal) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductsecondreal) = S ge_signed_half_gaussianfactorizationquotientproductsecondrealdecode))) /\ ((ge_second_rp_gaussianfactorizationquotientproduct) + ge_balance_negative_gaussianfactorizationquotientproductsecondreal = (ge_second_rn_gaussianfactorizationquotientproduct) + ge_balance_positive_gaussianfactorizationquotientproductsecondreal))) /\ (exists ge_balance_positive_gaussianfactorizationquotientproductsecondimaginary ge_balance_negative_gaussianfactorizationquotientproductsecondimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductsecondimaginary) /\ (ge_balance_negative_gaussianfactorizationquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationquotientproductsecond) = 2 * ge_signed_half_gaussianfactorizationquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductsecondimaginary) = S ge_signed_half_gaussianfactorizationquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_gaussianfactorizationquotientproduct) + ge_balance_negative_gaussianfactorizationquotientproductsecondimaginary = (ge_second_in_gaussianfactorizationquotientproduct) + ge_balance_positive_gaussianfactorizationquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_gaussianfactorizationquotientproductoutput ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput. ((((z)) = ((ge_representation_real_code_gaussianfactorizationquotientproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput)) * S ((ge_representation_real_code_gaussianfactorizationquotientproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput)) + ((ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput) + (ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput))) /\ ((exists ge_balance_positive_gaussianfactorizationquotientproductoutputreal ge_balance_negative_gaussianfactorizationquotientproductoutputreal. (((((ge_representation_real_code_gaussianfactorizationquotientproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductoutputreal) /\ (ge_balance_negative_gaussianfactorizationquotientproductoutputreal) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductoutputrealdecode. (((ge_representation_real_code_gaussianfactorizationquotientproductoutput) = 2 * ge_signed_half_gaussianfactorizationquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductoutputreal) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductoutputreal) = S ge_signed_half_gaussianfactorizationquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_gaussianfactorizationquotientproduct) * (ge_second_rp_gaussianfactorizationquotientproduct))) + (((ge_first_rn_gaussianfactorizationquotientproduct) * (ge_second_rn_gaussianfactorizationquotientproduct))))) + (((((ge_first_ip_gaussianfactorizationquotientproduct) * (ge_second_in_gaussianfactorizationquotientproduct))) + (((ge_first_in_gaussianfactorizationquotientproduct) * (ge_second_ip_gaussianfactorizationquotientproduct))))))) + ge_balance_negative_gaussianfactorizationquotientproductoutputreal = (((((((ge_first_rp_gaussianfactorizationquotientproduct) * (ge_second_rn_gaussianfactorizationquotientproduct))) + (((ge_first_rn_gaussianfactorizationquotientproduct) * (ge_second_rp_gaussianfactorizationquotientproduct))))) + (((((ge_first_ip_gaussianfactorizationquotientproduct) * (ge_second_ip_gaussianfactorizationquotientproduct))) + (((ge_first_in_gaussianfactorizationquotientproduct) * (ge_second_in_gaussianfactorizationquotientproduct))))))) + ge_balance_positive_gaussianfactorizationquotientproductoutputreal))) /\ (exists ge_balance_positive_gaussianfactorizationquotientproductoutputimaginary ge_balance_negative_gaussianfactorizationquotientproductoutputimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput) = 2 * (ge_balance_positive_gaussianfactorizationquotientproductoutputimaginary) /\ (ge_balance_negative_gaussianfactorizationquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationquotientproductoutput) = 2 * ge_signed_half_gaussianfactorizationquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationquotientproductoutputimaginary) = S ge_signed_half_gaussianfactorizationquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_gaussianfactorizationquotientproduct) * (ge_second_ip_gaussianfactorizationquotientproduct))) + (((ge_first_rn_gaussianfactorizationquotientproduct) * (ge_second_in_gaussianfactorizationquotientproduct))))) + (((((ge_first_ip_gaussianfactorizationquotientproduct) * (ge_second_rp_gaussianfactorizationquotientproduct))) + (((ge_first_in_gaussianfactorizationquotientproduct) * (ge_second_rn_gaussianfactorizationquotientproduct))))))) + ge_balance_negative_gaussianfactorizationquotientproductoutputimaginary = (((((((ge_first_rp_gaussianfactorizationquotientproduct) * (ge_second_in_gaussianfactorizationquotientproduct))) + (((ge_first_rn_gaussianfactorizationquotientproduct) * (ge_second_ip_gaussianfactorizationquotientproduct))))) + (((((ge_first_ip_gaussianfactorizationquotientproduct) * (ge_second_rn_gaussianfactorizationquotientproduct))) + (((ge_first_in_gaussianfactorizationquotientproduct) * (ge_second_rp_gaussianfactorizationquotientproduct))))))) + ge_balance_positive_gaussianfactorizationquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_gaussianfactorization. ((exists ge_norm_rp_gaussianfactorizationnorm ge_norm_rn_gaussianfactorizationnorm ge_norm_ip_gaussianfactorizationnorm ge_norm_in_gaussianfactorizationnorm. ((exists ge_representation_real_code_gaussianfactorizationnormrepresentation ge_representation_imaginary_code_gaussianfactorizationnormrepresentation. ((((d)) = ((ge_representation_real_code_gaussianfactorizationnormrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationnormrepresentation)) * S ((ge_representation_real_code_gaussianfactorizationnormrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationnormrepresentation)) + ((ge_representation_imaginary_code_gaussianfactorizationnormrepresentation) + (ge_representation_imaginary_code_gaussianfactorizationnormrepresentation))) /\ ((exists ge_balance_positive_gaussianfactorizationnormrepresentationreal ge_balance_negative_gaussianfactorizationnormrepresentationreal. (((((ge_representation_real_code_gaussianfactorizationnormrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationnormrepresentationreal) /\ (ge_balance_negative_gaussianfactorizationnormrepresentationreal) = 0) \/ exists ge_signed_half_gaussianfactorizationnormrepresentationrealdecode. (((ge_representation_real_code_gaussianfactorizationnormrepresentation) = 2 * ge_signed_half_gaussianfactorizationnormrepresentationrealdecode + 1 /\ (ge_balance_positive_gaussianfactorizationnormrepresentationreal) = 0) /\ (ge_balance_negative_gaussianfactorizationnormrepresentationreal) = S ge_signed_half_gaussianfactorizationnormrepresentationrealdecode))) /\ ((ge_norm_rp_gaussianfactorizationnorm) + ge_balance_negative_gaussianfactorizationnormrepresentationreal = (ge_norm_rn_gaussianfactorizationnorm) + ge_balance_positive_gaussianfactorizationnormrepresentationreal))) /\ (exists ge_balance_positive_gaussianfactorizationnormrepresentationimaginary ge_balance_negative_gaussianfactorizationnormrepresentationimaginary. (((((ge_representation_imaginary_code_gaussianfactorizationnormrepresentation) = 2 * (ge_balance_positive_gaussianfactorizationnormrepresentationimaginary) /\ (ge_balance_negative_gaussianfactorizationnormrepresentationimaginary) = 0) \/ exists ge_signed_half_gaussianfactorizationnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_gaussianfactorizationnormrepresentation) = 2 * ge_signed_half_gaussianfactorizationnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_gaussianfactorizationnormrepresentationimaginary) = 0) /\ (ge_balance_negative_gaussianfactorizationnormrepresentationimaginary) = S ge_signed_half_gaussianfactorizationnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_gaussianfactorizationnorm) + ge_balance_negative_gaussianfactorizationnormrepresentationimaginary = (ge_norm_in_gaussianfactorizationnorm) + ge_balance_positive_gaussianfactorizationnormrepresentationimaginary)))))) /\ (exists ge_real_square_gaussianfactorizationnormsquare ge_imaginary_square_gaussianfactorizationnormsquare. ((((((ge_norm_rp_gaussianfactorizationnorm) * (ge_norm_rp_gaussianfactorizationnorm))) + (((ge_norm_rn_gaussianfactorizationnorm) * (ge_norm_rn_gaussianfactorizationnorm)))) = ((ge_real_square_gaussianfactorizationnormsquare) + (((((ge_norm_rp_gaussianfactorizationnorm) * (ge_norm_rn_gaussianfactorizationnorm))) + (((ge_norm_rn_gaussianfactorizationnorm) * (ge_norm_rp_gaussianfactorizationnorm))))))) /\ ((((((ge_norm_ip_gaussianfactorizationnorm) * (ge_norm_ip_gaussianfactorizationnorm))) + (((ge_norm_in_gaussianfactorizationnorm) * (ge_norm_in_gaussianfactorizationnorm)))) = ((ge_imaginary_square_gaussianfactorizationnormsquare) + (((((ge_norm_ip_gaussianfactorizationnorm) * (ge_norm_in_gaussianfactorizationnorm))) + (((ge_norm_in_gaussianfactorizationnorm) * (ge_norm_ip_gaussianfactorizationnorm))))))) /\ ((gr_proper_divisor_norm_gaussianfactorization) = ge_real_square_gaussianfactorizationnormsquare + ge_imaginary_square_gaussianfactorizationnormsquare)))))) /\ (exists ge_gap_gaussianfactorizationstrict. ge_gap_gaussianfactorizationstrict + S (gr_proper_divisor_norm_gaussianfactorization) = ((N)))))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.