Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ d. ∀ z. ∀ N. ZPairValid(d) → ZPairValid(z) → GProperNormDivisor(d,z,N) ∨ ¬GProperNormDivisor(d,z,N)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
gaussian_unit_decidablegaussian_divides_decidablegaussian_norm_exists · checked external prerequisitele_or_lt · checked external prerequisitegaussian_norm_functional · checked external prerequisitelt_not_le · checked external prerequisite
Original expanded first-order statement
forall d z N. (exists ge_real_positive_proper_candidate_valid ge_real_negative_proper_candidate_valid ge_imaginary_positive_proper_candidate_valid ge_imaginary_negative_proper_candidate_valid. (exists ge_real_code_proper_candidate_validdecode ge_imaginary_code_proper_candidate_validdecode. (((d) = ((ge_real_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode)) * S ((ge_real_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode)) + ((ge_imaginary_code_proper_candidate_validdecode) + (ge_imaginary_code_proper_candidate_validdecode))) /\ (((((ge_real_code_proper_candidate_validdecode) = 2 * (ge_real_positive_proper_candidate_valid) /\ (ge_real_negative_proper_candidate_valid) = 0) \/ exists ge_signed_half_ge_proper_candidate_validdecode_real. (((ge_real_code_proper_candidate_validdecode) = 2 * ge_signed_half_ge_proper_candidate_validdecode_real + 1 /\ (ge_real_positive_proper_candidate_valid) = 0) /\ (ge_real_negative_proper_candidate_valid) = S ge_signed_half_ge_proper_candidate_validdecode_real))) /\ ((((ge_imaginary_code_proper_candidate_validdecode) = 2 * (ge_imaginary_positive_proper_candidate_valid) /\ (ge_imaginary_negative_proper_candidate_valid) = 0) \/ exists ge_signed_half_ge_proper_candidate_validdecode_imaginary. (((ge_imaginary_code_proper_candidate_validdecode) = 2 * ge_signed_half_ge_proper_candidate_validdecode_imaginary + 1 /\ (ge_imaginary_positive_proper_candidate_valid) = 0) /\ (ge_imaginary_negative_proper_candidate_valid) = S ge_signed_half_ge_proper_candidate_validdecode_imaginary))))))) -> (exists ge_real_positive_proper_target_valid ge_real_negative_proper_target_valid ge_imaginary_positive_proper_target_valid ge_imaginary_negative_proper_target_valid. (exists ge_real_code_proper_target_validdecode ge_imaginary_code_proper_target_validdecode. (((z) = ((ge_real_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode)) * S ((ge_real_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode)) + ((ge_imaginary_code_proper_target_validdecode) + (ge_imaginary_code_proper_target_validdecode))) /\ (((((ge_real_code_proper_target_validdecode) = 2 * (ge_real_positive_proper_target_valid) /\ (ge_real_negative_proper_target_valid) = 0) \/ exists ge_signed_half_ge_proper_target_validdecode_real. (((ge_real_code_proper_target_validdecode) = 2 * ge_signed_half_ge_proper_target_validdecode_real + 1 /\ (ge_real_positive_proper_target_valid) = 0) /\ (ge_real_negative_proper_target_valid) = S ge_signed_half_ge_proper_target_validdecode_real))) /\ ((((ge_imaginary_code_proper_target_validdecode) = 2 * (ge_imaginary_positive_proper_target_valid) /\ (ge_imaginary_negative_proper_target_valid) = 0) \/ exists ge_signed_half_ge_proper_target_validdecode_imaginary. (((ge_imaginary_code_proper_target_validdecode) = 2 * ge_signed_half_ge_proper_target_validdecode_imaginary + 1 /\ (ge_imaginary_positive_proper_target_valid) = 0) /\ (ge_imaginary_negative_proper_target_valid) = S ge_signed_half_ge_proper_target_validdecode_imaginary))))))) -> (((~(exists gr_inverse_proper_decision_yesnonunit. (exists ge_first_rp_proper_decision_yesnonunitidentity ge_first_rn_proper_decision_yesnonunitidentity ge_first_ip_proper_decision_yesnonunitidentity ge_first_in_proper_decision_yesnonunitidentity ge_second_rp_proper_decision_yesnonunitidentity ge_second_rn_proper_decision_yesnonunitidentity ge_second_ip_proper_decision_yesnonunitidentity ge_second_in_proper_decision_yesnonunitidentity. ((exists ge_representation_real_code_proper_decision_yesnonunitidentityfirst ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentityfirstreal ge_balance_negative_proper_decision_yesnonunitidentityfirstreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityfirstreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstreal) = S ge_signed_half_proper_decision_yesnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentityfirstreal = (ge_first_rn_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentityfirst) = 2 * ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary) = S ge_signed_half_proper_decision_yesnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentityfirstimaginary = (ge_first_in_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_yesnonunitidentitysecond ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond. (((gr_inverse_proper_decision_yesnonunit) = ((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentitysecondreal ge_balance_negative_proper_decision_yesnonunitidentitysecondreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentitysecondreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondreal) = S ge_signed_half_proper_decision_yesnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentitysecondreal = (ge_second_rn_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentitysecond) = 2 * ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary) = S ge_signed_half_proper_decision_yesnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_yesnonunitidentity) + ge_balance_negative_proper_decision_yesnonunitidentitysecondimaginary = (ge_second_in_proper_decision_yesnonunitidentity) + ge_balance_positive_proper_decision_yesnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_yesnonunitidentityoutput ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput)) * S ((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_decision_yesnonunitidentityoutputreal ge_balance_negative_proper_decision_yesnonunitidentityoutputreal. (((((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityoutputreal) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputreal) = S ge_signed_half_proper_decision_yesnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))))))) + ge_balance_negative_proper_decision_yesnonunitidentityoutputreal = (((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))))))) + ge_balance_positive_proper_decision_yesnonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnonunitidentityoutput) = 2 * ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary) = S ge_signed_half_proper_decision_yesnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))))))) + ge_balance_negative_proper_decision_yesnonunitidentityoutputimaginary = (((((((ge_first_rp_proper_decision_yesnonunitidentity) * (ge_second_in_proper_decision_yesnonunitidentity))) + (((ge_first_rn_proper_decision_yesnonunitidentity) * (ge_second_ip_proper_decision_yesnonunitidentity))))) + (((((ge_first_ip_proper_decision_yesnonunitidentity) * (ge_second_rn_proper_decision_yesnonunitidentity))) + (((ge_first_in_proper_decision_yesnonunitidentity) * (ge_second_rp_proper_decision_yesnonunitidentity))))))) + ge_balance_positive_proper_decision_yesnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_decision_yesquotient. (exists ge_first_rp_proper_decision_yesquotientproduct ge_first_rn_proper_decision_yesquotientproduct ge_first_ip_proper_decision_yesquotientproduct ge_first_in_proper_decision_yesquotientproduct ge_second_rp_proper_decision_yesquotientproduct ge_second_rn_proper_decision_yesquotientproduct ge_second_ip_proper_decision_yesquotientproduct ge_second_in_proper_decision_yesquotientproduct. ((exists ge_representation_real_code_proper_decision_yesquotientproductfirst ge_representation_imaginary_code_proper_decision_yesquotientproductfirst. (((d) = ((ge_representation_real_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst)) * S ((ge_representation_real_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_yesquotientproductfirst))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductfirstreal ge_balance_negative_proper_decision_yesquotientproductfirstreal. (((((ge_representation_real_code_proper_decision_yesquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_yesquotientproductfirstreal) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductfirstrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductfirst) = 2 * ge_signed_half_proper_decision_yesquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstreal) = S ge_signed_half_proper_decision_yesquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductfirstreal = (ge_first_rn_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductfirstimaginary ge_balance_negative_proper_decision_yesquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_yesquotientproductfirstimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductfirst) = 2 * ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductfirstimaginary) = S ge_signed_half_proper_decision_yesquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductfirstimaginary = (ge_first_in_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_yesquotientproductsecond ge_representation_imaginary_code_proper_decision_yesquotientproductsecond. (((gr_quotient_proper_decision_yesquotient) = ((ge_representation_real_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond)) * S ((ge_representation_real_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_yesquotientproductsecond))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductsecondreal ge_balance_negative_proper_decision_yesquotientproductsecondreal. (((((ge_representation_real_code_proper_decision_yesquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_yesquotientproductsecondreal) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductsecondrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductsecond) = 2 * ge_signed_half_proper_decision_yesquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondreal) = S ge_signed_half_proper_decision_yesquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductsecondreal = (ge_second_rn_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductsecondimaginary ge_balance_negative_proper_decision_yesquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_yesquotientproductsecondimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductsecond) = 2 * ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductsecondimaginary) = S ge_signed_half_proper_decision_yesquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_yesquotientproduct) + ge_balance_negative_proper_decision_yesquotientproductsecondimaginary = (ge_second_in_proper_decision_yesquotientproduct) + ge_balance_positive_proper_decision_yesquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_yesquotientproductoutput ge_representation_imaginary_code_proper_decision_yesquotientproductoutput. (((z) = ((ge_representation_real_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput)) * S ((ge_representation_real_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput)) + ((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_yesquotientproductoutput))) /\ ((exists ge_balance_positive_proper_decision_yesquotientproductoutputreal ge_balance_negative_proper_decision_yesquotientproductoutputreal. (((((ge_representation_real_code_proper_decision_yesquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_yesquotientproductoutputreal) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductoutputrealdecode. (((ge_representation_real_code_proper_decision_yesquotientproductoutput) = 2 * ge_signed_half_proper_decision_yesquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputreal) = S ge_signed_half_proper_decision_yesquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))))))) + ge_balance_negative_proper_decision_yesquotientproductoutputreal = (((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))))))) + ge_balance_positive_proper_decision_yesquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_decision_yesquotientproductoutputimaginary ge_balance_negative_proper_decision_yesquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_yesquotientproductoutputimaginary) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesquotientproductoutput) = 2 * ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesquotientproductoutputimaginary) = S ge_signed_half_proper_decision_yesquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))))))) + ge_balance_negative_proper_decision_yesquotientproductoutputimaginary = (((((((ge_first_rp_proper_decision_yesquotientproduct) * (ge_second_in_proper_decision_yesquotientproduct))) + (((ge_first_rn_proper_decision_yesquotientproduct) * (ge_second_ip_proper_decision_yesquotientproduct))))) + (((((ge_first_ip_proper_decision_yesquotientproduct) * (ge_second_rn_proper_decision_yesquotientproduct))) + (((ge_first_in_proper_decision_yesquotientproduct) * (ge_second_rp_proper_decision_yesquotientproduct))))))) + ge_balance_positive_proper_decision_yesquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_decision_yes. ((exists ge_norm_rp_proper_decision_yesnorm ge_norm_rn_proper_decision_yesnorm ge_norm_ip_proper_decision_yesnorm ge_norm_in_proper_decision_yesnorm. ((exists ge_representation_real_code_proper_decision_yesnormrepresentation ge_representation_imaginary_code_proper_decision_yesnormrepresentation. (((d) = ((ge_representation_real_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation)) * S ((ge_representation_real_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation)) + ((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) + (ge_representation_imaginary_code_proper_decision_yesnormrepresentation))) /\ ((exists ge_balance_positive_proper_decision_yesnormrepresentationreal ge_balance_negative_proper_decision_yesnormrepresentationreal. (((((ge_representation_real_code_proper_decision_yesnormrepresentation) = 2 * (ge_balance_positive_proper_decision_yesnormrepresentationreal) /\ (ge_balance_negative_proper_decision_yesnormrepresentationreal) = 0) \/ exists ge_signed_half_proper_decision_yesnormrepresentationrealdecode. (((ge_representation_real_code_proper_decision_yesnormrepresentation) = 2 * ge_signed_half_proper_decision_yesnormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_decision_yesnormrepresentationreal) = 0) /\ (ge_balance_negative_proper_decision_yesnormrepresentationreal) = S ge_signed_half_proper_decision_yesnormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_decision_yesnorm) + ge_balance_negative_proper_decision_yesnormrepresentationreal = (ge_norm_rn_proper_decision_yesnorm) + ge_balance_positive_proper_decision_yesnormrepresentationreal))) /\ (exists ge_balance_positive_proper_decision_yesnormrepresentationimaginary ge_balance_negative_proper_decision_yesnormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) = 2 * (ge_balance_positive_proper_decision_yesnormrepresentationimaginary) /\ (ge_balance_negative_proper_decision_yesnormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_decision_yesnormrepresentation) = 2 * ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_yesnormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_decision_yesnormrepresentationimaginary) = S ge_signed_half_proper_decision_yesnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_decision_yesnorm) + ge_balance_negative_proper_decision_yesnormrepresentationimaginary = (ge_norm_in_proper_decision_yesnorm) + ge_balance_positive_proper_decision_yesnormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_decision_yesnormsquare ge_imaginary_square_proper_decision_yesnormsquare. ((((((ge_norm_rp_proper_decision_yesnorm) * (ge_norm_rp_proper_decision_yesnorm))) + (((ge_norm_rn_proper_decision_yesnorm) * (ge_norm_rn_proper_decision_yesnorm)))) = ((ge_real_square_proper_decision_yesnormsquare) + (((((ge_norm_rp_proper_decision_yesnorm) * (ge_norm_rn_proper_decision_yesnorm))) + (((ge_norm_rn_proper_decision_yesnorm) * (ge_norm_rp_proper_decision_yesnorm))))))) /\ ((((((ge_norm_ip_proper_decision_yesnorm) * (ge_norm_ip_proper_decision_yesnorm))) + (((ge_norm_in_proper_decision_yesnorm) * (ge_norm_in_proper_decision_yesnorm)))) = ((ge_imaginary_square_proper_decision_yesnormsquare) + (((((ge_norm_ip_proper_decision_yesnorm) * (ge_norm_in_proper_decision_yesnorm))) + (((ge_norm_in_proper_decision_yesnorm) * (ge_norm_ip_proper_decision_yesnorm))))))) /\ ((gr_proper_divisor_norm_proper_decision_yes) = ge_real_square_proper_decision_yesnormsquare + ge_imaginary_square_proper_decision_yesnormsquare)))))) /\ (exists ge_gap_proper_decision_yesstrict. ge_gap_proper_decision_yesstrict + S (gr_proper_divisor_norm_proper_decision_yes) = (N))))))) \/ ~(((~(exists gr_inverse_proper_decision_nononunit. (exists ge_first_rp_proper_decision_nononunitidentity ge_first_rn_proper_decision_nononunitidentity ge_first_ip_proper_decision_nononunitidentity ge_first_in_proper_decision_nononunitidentity ge_second_rp_proper_decision_nononunitidentity ge_second_rn_proper_decision_nononunitidentity ge_second_ip_proper_decision_nononunitidentity ge_second_in_proper_decision_nononunitidentity. ((exists ge_representation_real_code_proper_decision_nononunitidentityfirst ge_representation_imaginary_code_proper_decision_nononunitidentityfirst. (((d) = ((ge_representation_real_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst)) * S ((ge_representation_real_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) + (ge_representation_imaginary_code_proper_decision_nononunitidentityfirst))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentityfirstreal ge_balance_negative_proper_decision_nononunitidentityfirstreal. (((((ge_representation_real_code_proper_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_nononunitidentityfirstreal) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityfirstrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentityfirst) = 2 * ge_signed_half_proper_decision_nononunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstreal) = S ge_signed_half_proper_decision_nononunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentityfirstreal = (ge_first_rn_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentityfirstimaginary ge_balance_negative_proper_decision_nononunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) = 2 * (ge_balance_positive_proper_decision_nononunitidentityfirstimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentityfirst) = 2 * ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityfirstimaginary) = S ge_signed_half_proper_decision_nononunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentityfirstimaginary = (ge_first_in_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_nononunitidentitysecond ge_representation_imaginary_code_proper_decision_nononunitidentitysecond. (((gr_inverse_proper_decision_nononunit) = ((ge_representation_real_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond)) * S ((ge_representation_real_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) + (ge_representation_imaginary_code_proper_decision_nononunitidentitysecond))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentitysecondreal ge_balance_negative_proper_decision_nononunitidentitysecondreal. (((((ge_representation_real_code_proper_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_nononunitidentitysecondreal) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentitysecondrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentitysecond) = 2 * ge_signed_half_proper_decision_nononunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondreal) = S ge_signed_half_proper_decision_nononunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentitysecondreal = (ge_second_rn_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentitysecondimaginary ge_balance_negative_proper_decision_nononunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) = 2 * (ge_balance_positive_proper_decision_nononunitidentitysecondimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentitysecond) = 2 * ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentitysecondimaginary) = S ge_signed_half_proper_decision_nononunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_nononunitidentity) + ge_balance_negative_proper_decision_nononunitidentitysecondimaginary = (ge_second_in_proper_decision_nononunitidentity) + ge_balance_positive_proper_decision_nononunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_nononunitidentityoutput ge_representation_imaginary_code_proper_decision_nononunitidentityoutput. (((6) = ((ge_representation_real_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput)) * S ((ge_representation_real_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput)) + ((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) + (ge_representation_imaginary_code_proper_decision_nononunitidentityoutput))) /\ ((exists ge_balance_positive_proper_decision_nononunitidentityoutputreal ge_balance_negative_proper_decision_nononunitidentityoutputreal. (((((ge_representation_real_code_proper_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_nononunitidentityoutputreal) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityoutputrealdecode. (((ge_representation_real_code_proper_decision_nononunitidentityoutput) = 2 * ge_signed_half_proper_decision_nononunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputreal) = S ge_signed_half_proper_decision_nononunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))))))) + ge_balance_negative_proper_decision_nononunitidentityoutputreal = (((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))))))) + ge_balance_positive_proper_decision_nononunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_decision_nononunitidentityoutputimaginary ge_balance_negative_proper_decision_nononunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) = 2 * (ge_balance_positive_proper_decision_nononunitidentityoutputimaginary) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nononunitidentityoutput) = 2 * ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nononunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_nononunitidentityoutputimaginary) = S ge_signed_half_proper_decision_nononunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))))))) + ge_balance_negative_proper_decision_nononunitidentityoutputimaginary = (((((((ge_first_rp_proper_decision_nononunitidentity) * (ge_second_in_proper_decision_nononunitidentity))) + (((ge_first_rn_proper_decision_nononunitidentity) * (ge_second_ip_proper_decision_nononunitidentity))))) + (((((ge_first_ip_proper_decision_nononunitidentity) * (ge_second_rn_proper_decision_nononunitidentity))) + (((ge_first_in_proper_decision_nononunitidentity) * (ge_second_rp_proper_decision_nononunitidentity))))))) + ge_balance_positive_proper_decision_nononunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_decision_noquotient. (exists ge_first_rp_proper_decision_noquotientproduct ge_first_rn_proper_decision_noquotientproduct ge_first_ip_proper_decision_noquotientproduct ge_first_in_proper_decision_noquotientproduct ge_second_rp_proper_decision_noquotientproduct ge_second_rn_proper_decision_noquotientproduct ge_second_ip_proper_decision_noquotientproduct ge_second_in_proper_decision_noquotientproduct. ((exists ge_representation_real_code_proper_decision_noquotientproductfirst ge_representation_imaginary_code_proper_decision_noquotientproductfirst. (((d) = ((ge_representation_real_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst)) * S ((ge_representation_real_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) + (ge_representation_imaginary_code_proper_decision_noquotientproductfirst))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductfirstreal ge_balance_negative_proper_decision_noquotientproductfirstreal. (((((ge_representation_real_code_proper_decision_noquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_noquotientproductfirstreal) /\ (ge_balance_negative_proper_decision_noquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductfirstrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductfirst) = 2 * ge_signed_half_proper_decision_noquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductfirstreal) = S ge_signed_half_proper_decision_noquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductfirstreal = (ge_first_rn_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductfirstimaginary ge_balance_negative_proper_decision_noquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) = 2 * (ge_balance_positive_proper_decision_noquotientproductfirstimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductfirst) = 2 * ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductfirstimaginary) = S ge_signed_half_proper_decision_noquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductfirstimaginary = (ge_first_in_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_decision_noquotientproductsecond ge_representation_imaginary_code_proper_decision_noquotientproductsecond. (((gr_quotient_proper_decision_noquotient) = ((ge_representation_real_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond)) * S ((ge_representation_real_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) + (ge_representation_imaginary_code_proper_decision_noquotientproductsecond))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductsecondreal ge_balance_negative_proper_decision_noquotientproductsecondreal. (((((ge_representation_real_code_proper_decision_noquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_noquotientproductsecondreal) /\ (ge_balance_negative_proper_decision_noquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductsecondrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductsecond) = 2 * ge_signed_half_proper_decision_noquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductsecondreal) = S ge_signed_half_proper_decision_noquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductsecondreal = (ge_second_rn_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductsecondimaginary ge_balance_negative_proper_decision_noquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) = 2 * (ge_balance_positive_proper_decision_noquotientproductsecondimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductsecond) = 2 * ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductsecondimaginary) = S ge_signed_half_proper_decision_noquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_decision_noquotientproduct) + ge_balance_negative_proper_decision_noquotientproductsecondimaginary = (ge_second_in_proper_decision_noquotientproduct) + ge_balance_positive_proper_decision_noquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_decision_noquotientproductoutput ge_representation_imaginary_code_proper_decision_noquotientproductoutput. (((z) = ((ge_representation_real_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput)) * S ((ge_representation_real_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput)) + ((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) + (ge_representation_imaginary_code_proper_decision_noquotientproductoutput))) /\ ((exists ge_balance_positive_proper_decision_noquotientproductoutputreal ge_balance_negative_proper_decision_noquotientproductoutputreal. (((((ge_representation_real_code_proper_decision_noquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_noquotientproductoutputreal) /\ (ge_balance_negative_proper_decision_noquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductoutputrealdecode. (((ge_representation_real_code_proper_decision_noquotientproductoutput) = 2 * ge_signed_half_proper_decision_noquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductoutputreal) = S ge_signed_half_proper_decision_noquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))))))) + ge_balance_negative_proper_decision_noquotientproductoutputreal = (((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))))))) + ge_balance_positive_proper_decision_noquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_decision_noquotientproductoutputimaginary ge_balance_negative_proper_decision_noquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) = 2 * (ge_balance_positive_proper_decision_noquotientproductoutputimaginary) /\ (ge_balance_negative_proper_decision_noquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_decision_noquotientproductoutput) = 2 * ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_noquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_decision_noquotientproductoutputimaginary) = S ge_signed_half_proper_decision_noquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))))))) + ge_balance_negative_proper_decision_noquotientproductoutputimaginary = (((((((ge_first_rp_proper_decision_noquotientproduct) * (ge_second_in_proper_decision_noquotientproduct))) + (((ge_first_rn_proper_decision_noquotientproduct) * (ge_second_ip_proper_decision_noquotientproduct))))) + (((((ge_first_ip_proper_decision_noquotientproduct) * (ge_second_rn_proper_decision_noquotientproduct))) + (((ge_first_in_proper_decision_noquotientproduct) * (ge_second_rp_proper_decision_noquotientproduct))))))) + ge_balance_positive_proper_decision_noquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_decision_no. ((exists ge_norm_rp_proper_decision_nonorm ge_norm_rn_proper_decision_nonorm ge_norm_ip_proper_decision_nonorm ge_norm_in_proper_decision_nonorm. ((exists ge_representation_real_code_proper_decision_nonormrepresentation ge_representation_imaginary_code_proper_decision_nonormrepresentation. (((d) = ((ge_representation_real_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation)) * S ((ge_representation_real_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation)) + ((ge_representation_imaginary_code_proper_decision_nonormrepresentation) + (ge_representation_imaginary_code_proper_decision_nonormrepresentation))) /\ ((exists ge_balance_positive_proper_decision_nonormrepresentationreal ge_balance_negative_proper_decision_nonormrepresentationreal. (((((ge_representation_real_code_proper_decision_nonormrepresentation) = 2 * (ge_balance_positive_proper_decision_nonormrepresentationreal) /\ (ge_balance_negative_proper_decision_nonormrepresentationreal) = 0) \/ exists ge_signed_half_proper_decision_nonormrepresentationrealdecode. (((ge_representation_real_code_proper_decision_nonormrepresentation) = 2 * ge_signed_half_proper_decision_nonormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_decision_nonormrepresentationreal) = 0) /\ (ge_balance_negative_proper_decision_nonormrepresentationreal) = S ge_signed_half_proper_decision_nonormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_decision_nonorm) + ge_balance_negative_proper_decision_nonormrepresentationreal = (ge_norm_rn_proper_decision_nonorm) + ge_balance_positive_proper_decision_nonormrepresentationreal))) /\ (exists ge_balance_positive_proper_decision_nonormrepresentationimaginary ge_balance_negative_proper_decision_nonormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_decision_nonormrepresentation) = 2 * (ge_balance_positive_proper_decision_nonormrepresentationimaginary) /\ (ge_balance_negative_proper_decision_nonormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_decision_nonormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_decision_nonormrepresentation) = 2 * ge_signed_half_proper_decision_nonormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_decision_nonormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_decision_nonormrepresentationimaginary) = S ge_signed_half_proper_decision_nonormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_decision_nonorm) + ge_balance_negative_proper_decision_nonormrepresentationimaginary = (ge_norm_in_proper_decision_nonorm) + ge_balance_positive_proper_decision_nonormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_decision_nonormsquare ge_imaginary_square_proper_decision_nonormsquare. ((((((ge_norm_rp_proper_decision_nonorm) * (ge_norm_rp_proper_decision_nonorm))) + (((ge_norm_rn_proper_decision_nonorm) * (ge_norm_rn_proper_decision_nonorm)))) = ((ge_real_square_proper_decision_nonormsquare) + (((((ge_norm_rp_proper_decision_nonorm) * (ge_norm_rn_proper_decision_nonorm))) + (((ge_norm_rn_proper_decision_nonorm) * (ge_norm_rp_proper_decision_nonorm))))))) /\ ((((((ge_norm_ip_proper_decision_nonorm) * (ge_norm_ip_proper_decision_nonorm))) + (((ge_norm_in_proper_decision_nonorm) * (ge_norm_in_proper_decision_nonorm)))) = ((ge_imaginary_square_proper_decision_nonormsquare) + (((((ge_norm_ip_proper_decision_nonorm) * (ge_norm_in_proper_decision_nonorm))) + (((ge_norm_in_proper_decision_nonorm) * (ge_norm_ip_proper_decision_nonorm))))))) /\ ((gr_proper_divisor_norm_proper_decision_no) = ge_real_square_proper_decision_nonormsquare + ge_imaginary_square_proper_decision_nonormsquare)))))) /\ (exists ge_gap_proper_decision_nostrict. ge_gap_proper_decision_nostrict + S (gr_proper_divisor_norm_proper_decision_no) = (N)))))))Complete tactic proof in conservative notation
All 66 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
66 script commands · 27 reading checkpoints · 5 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–5
02Establish huL6–9
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian unit decidable.
03Separate the logical casesL10–11
04Fix variables and assumptionsL12–12
Work with arbitrary variables or the premises of the current implication.
- L12
intro hp
05Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
cases hp
06Use earlier factsL14–15
07Establish hvL16–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian divides decidable.
08Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
cases hv
09Establish hnL23–26
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm exists.
10Separate the logical casesL27–27
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L27
cases hn
11Establish hbL28–31
12Separate the logical casesL32–33
13Fix variables and assumptionsL34–34
Work with arbitrary variables or the premises of the current implication.
- L34
intro hp
14Separate the logical casesL35–38
15Establish heqL39–48
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm functional.
- L39
have heq : x1=x - L40
specialize gaussian_norm_functional (d) - L41
specialize gaussian_norm_functional (x1) - L42
specialize gaussian_norm_functional (x) - L43
apply gaussian_norm_functional - L44
exact hp_right_right_witness_left - L45
exact hn_witness - L46
rewrite heq at hp_right_right_witness_right - L47
specialize lt_not_le (x) - L48
specialize lt_not_le (N)
16Use earlier factsL49–51
17Separate the logical casesL52–53
18Use earlier factsL54–54
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L54
exact hu_right
19Separate the logical casesL55–55
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L55
split
20Use earlier factsL56–56
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L56
exact hv_left
21Construct an explicit witnessL57–57
Supply the displayed value, then prove that it has the required property.
- L57
exists (x)
22Separate the logical casesL58–58
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L58
split
23Use earlier factsL59–60
24Separate the logical casesL61–61
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L61
right
25Fix variables and assumptionsL62–62
Work with arbitrary variables or the premises of the current implication.
- L62
intro hp
26Separate the logical casesL63–64
Original defined command ledger · 66 lines
- 0001
intro d - 0002
intro z - 0003
intro N - 0004
intro hd - 0005
intro hz - 0006
have hu : GUnit(d) ∨ ¬GUnit(d) - 0007
specialize gaussian_unit_decidable (d) - 0008
apply gaussian_unit_decidable - 0009
exact hd - 0010
cases hu - 0011
right - 0012
intro hp - 0013
cases hp - 0014
apply hp_left - 0015
exact hu_left - 0016
have hv : GDvd(d,z) ∨ ¬GDvd(d,z) - 0017
specialize gaussian_divides_decidable (d) - 0018
specialize gaussian_divides_decidable (z) - 0019
apply gaussian_divides_decidable - 0020
exact hd - 0021
exact hz - 0022
cases hv - 0023
have hn : ∃ D. GNorm(d,D) - 0024
specialize gaussian_norm_exists (d) - 0025
apply gaussian_norm_exists - 0026
exact hd - 0027
cases hn - 0028
have hb : Le(N,x) ∨ Lt(x,N) - 0029
specialize le_or_lt (N) - 0030
specialize le_or_lt (x) - 0031
apply le_or_lt - 0032
cases hb - 0033
right - 0034
intro hp - 0035
cases hp - 0036
cases hp_right - 0037
cases hp_right_right - 0038
cases hp_right_right_witness - 0039
have heq : x1=x - 0040
specialize gaussian_norm_functional (d) - 0041
specialize gaussian_norm_functional (x1) - 0042
specialize gaussian_norm_functional (x) - 0043
apply gaussian_norm_functional - 0044
exact hp_right_right_witness_left - 0045
exact hn_witness - 0046
rewrite heq at hp_right_right_witness_right - 0047
specialize lt_not_le (x) - 0048
specialize lt_not_le (N) - 0049
apply lt_not_le - 0050
exact hp_right_right_witness_right - 0051
exact hb_left - 0052
left - 0053
split - 0054
exact hu_right - 0055
split - 0056
exact hv_left - 0057
exists (x) - 0058
split - 0059
exact hn_witness - 0060
exact hb_right - 0061
right - 0062
intro hp - 0063
cases hp - 0064
cases hp_right - 0065
apply hv_right - 0066
exact hp_right_left