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. GProperNormDivisor(d,z,N) → GNorm(z,N) → ¬z = 0 → ∃ x. ∃ y. ∃ n. GStrictNonunitFactorization(z,N,d,x,y,n)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
gaussian_divisor_norm_factorgaussian_unit_has_norm_onegaussian_norm_functional · checked external prerequisitemul_one · checked external prerequisitelt_irrefl_expanded · checked external prerequisitegaussian_search_norm_factors_strictgaussian_norm_nonzero
Original expanded first-order statement
forall d z N. (((~(exists gr_inverse_proper_split_inputnonunit. (exists ge_first_rp_proper_split_inputnonunitidentity ge_first_rn_proper_split_inputnonunitidentity ge_first_ip_proper_split_inputnonunitidentity ge_first_in_proper_split_inputnonunitidentity ge_second_rp_proper_split_inputnonunitidentity ge_second_rn_proper_split_inputnonunitidentity ge_second_ip_proper_split_inputnonunitidentity ge_second_in_proper_split_inputnonunitidentity. ((exists ge_representation_real_code_proper_split_inputnonunitidentityfirst ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst)) * S ((ge_representation_real_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentityfirstreal ge_balance_negative_proper_split_inputnonunitidentityfirstreal. (((((ge_representation_real_code_proper_split_inputnonunitidentityfirst) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityfirstreal) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentityfirst) = 2 * ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstreal) = S ge_signed_half_proper_split_inputnonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentityfirstreal = (ge_first_rn_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentityfirst) = 2 * ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary) = S ge_signed_half_proper_split_inputnonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentityfirstimaginary = (ge_first_in_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_split_inputnonunitidentitysecond ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond. (((gr_inverse_proper_split_inputnonunit) = ((ge_representation_real_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond)) * S ((ge_representation_real_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) + (ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentitysecondreal ge_balance_negative_proper_split_inputnonunitidentitysecondreal. (((((ge_representation_real_code_proper_split_inputnonunitidentitysecond) = 2 * (ge_balance_positive_proper_split_inputnonunitidentitysecondreal) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentitysecond) = 2 * ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondreal) = S ge_signed_half_proper_split_inputnonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentitysecondreal = (ge_second_rn_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) = 2 * (ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentitysecond) = 2 * ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary) = S ge_signed_half_proper_split_inputnonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_split_inputnonunitidentity) + ge_balance_negative_proper_split_inputnonunitidentitysecondimaginary = (ge_second_in_proper_split_inputnonunitidentity) + ge_balance_positive_proper_split_inputnonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_split_inputnonunitidentityoutput ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput)) * S ((ge_representation_real_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) + (ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_split_inputnonunitidentityoutputreal ge_balance_negative_proper_split_inputnonunitidentityoutputreal. (((((ge_representation_real_code_proper_split_inputnonunitidentityoutput) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityoutputreal) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_split_inputnonunitidentityoutput) = 2 * ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputreal) = S ge_signed_half_proper_split_inputnonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))))))) + ge_balance_negative_proper_split_inputnonunitidentityoutputreal = (((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))))))) + ge_balance_positive_proper_split_inputnonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) = 2 * (ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnonunitidentityoutput) = 2 * ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary) = S ge_signed_half_proper_split_inputnonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))))))) + ge_balance_negative_proper_split_inputnonunitidentityoutputimaginary = (((((((ge_first_rp_proper_split_inputnonunitidentity) * (ge_second_in_proper_split_inputnonunitidentity))) + (((ge_first_rn_proper_split_inputnonunitidentity) * (ge_second_ip_proper_split_inputnonunitidentity))))) + (((((ge_first_ip_proper_split_inputnonunitidentity) * (ge_second_rn_proper_split_inputnonunitidentity))) + (((ge_first_in_proper_split_inputnonunitidentity) * (ge_second_rp_proper_split_inputnonunitidentity))))))) + ge_balance_positive_proper_split_inputnonunitidentityoutputimaginary))))))))))) /\ ((exists gr_quotient_proper_split_inputquotient. (exists ge_first_rp_proper_split_inputquotientproduct ge_first_rn_proper_split_inputquotientproduct ge_first_ip_proper_split_inputquotientproduct ge_first_in_proper_split_inputquotientproduct ge_second_rp_proper_split_inputquotientproduct ge_second_rn_proper_split_inputquotientproduct ge_second_ip_proper_split_inputquotientproduct ge_second_in_proper_split_inputquotientproduct. ((exists ge_representation_real_code_proper_split_inputquotientproductfirst ge_representation_imaginary_code_proper_split_inputquotientproductfirst. (((d) = ((ge_representation_real_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst)) * S ((ge_representation_real_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) + (ge_representation_imaginary_code_proper_split_inputquotientproductfirst))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductfirstreal ge_balance_negative_proper_split_inputquotientproductfirstreal. (((((ge_representation_real_code_proper_split_inputquotientproductfirst) = 2 * (ge_balance_positive_proper_split_inputquotientproductfirstreal) /\ (ge_balance_negative_proper_split_inputquotientproductfirstreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductfirstrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductfirst) = 2 * ge_signed_half_proper_split_inputquotientproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductfirstreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductfirstreal) = S ge_signed_half_proper_split_inputquotientproductfirstrealdecode))) /\ ((ge_first_rp_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductfirstreal = (ge_first_rn_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductfirstreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductfirstimaginary ge_balance_negative_proper_split_inputquotientproductfirstimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) = 2 * (ge_balance_positive_proper_split_inputquotientproductfirstimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductfirst) = 2 * ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductfirstimaginary) = S ge_signed_half_proper_split_inputquotientproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductfirstimaginary = (ge_first_in_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_split_inputquotientproductsecond ge_representation_imaginary_code_proper_split_inputquotientproductsecond. (((gr_quotient_proper_split_inputquotient) = ((ge_representation_real_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond)) * S ((ge_representation_real_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) + (ge_representation_imaginary_code_proper_split_inputquotientproductsecond))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductsecondreal ge_balance_negative_proper_split_inputquotientproductsecondreal. (((((ge_representation_real_code_proper_split_inputquotientproductsecond) = 2 * (ge_balance_positive_proper_split_inputquotientproductsecondreal) /\ (ge_balance_negative_proper_split_inputquotientproductsecondreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductsecondrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductsecond) = 2 * ge_signed_half_proper_split_inputquotientproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductsecondreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductsecondreal) = S ge_signed_half_proper_split_inputquotientproductsecondrealdecode))) /\ ((ge_second_rp_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductsecondreal = (ge_second_rn_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductsecondreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductsecondimaginary ge_balance_negative_proper_split_inputquotientproductsecondimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) = 2 * (ge_balance_positive_proper_split_inputquotientproductsecondimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductsecond) = 2 * ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductsecondimaginary) = S ge_signed_half_proper_split_inputquotientproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_split_inputquotientproduct) + ge_balance_negative_proper_split_inputquotientproductsecondimaginary = (ge_second_in_proper_split_inputquotientproduct) + ge_balance_positive_proper_split_inputquotientproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_split_inputquotientproductoutput ge_representation_imaginary_code_proper_split_inputquotientproductoutput. (((z) = ((ge_representation_real_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput)) * S ((ge_representation_real_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput)) + ((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) + (ge_representation_imaginary_code_proper_split_inputquotientproductoutput))) /\ ((exists ge_balance_positive_proper_split_inputquotientproductoutputreal ge_balance_negative_proper_split_inputquotientproductoutputreal. (((((ge_representation_real_code_proper_split_inputquotientproductoutput) = 2 * (ge_balance_positive_proper_split_inputquotientproductoutputreal) /\ (ge_balance_negative_proper_split_inputquotientproductoutputreal) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductoutputrealdecode. (((ge_representation_real_code_proper_split_inputquotientproductoutput) = 2 * ge_signed_half_proper_split_inputquotientproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductoutputreal) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductoutputreal) = S ge_signed_half_proper_split_inputquotientproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))))))) + ge_balance_negative_proper_split_inputquotientproductoutputreal = (((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))))))) + ge_balance_positive_proper_split_inputquotientproductoutputreal))) /\ (exists ge_balance_positive_proper_split_inputquotientproductoutputimaginary ge_balance_negative_proper_split_inputquotientproductoutputimaginary. (((((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) = 2 * (ge_balance_positive_proper_split_inputquotientproductoutputimaginary) /\ (ge_balance_negative_proper_split_inputquotientproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputquotientproductoutput) = 2 * ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputquotientproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_split_inputquotientproductoutputimaginary) = S ge_signed_half_proper_split_inputquotientproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))))))) + ge_balance_negative_proper_split_inputquotientproductoutputimaginary = (((((((ge_first_rp_proper_split_inputquotientproduct) * (ge_second_in_proper_split_inputquotientproduct))) + (((ge_first_rn_proper_split_inputquotientproduct) * (ge_second_ip_proper_split_inputquotientproduct))))) + (((((ge_first_ip_proper_split_inputquotientproduct) * (ge_second_rn_proper_split_inputquotientproduct))) + (((ge_first_in_proper_split_inputquotientproduct) * (ge_second_rp_proper_split_inputquotientproduct))))))) + ge_balance_positive_proper_split_inputquotientproductoutputimaginary)))))))))) /\ (exists gr_proper_divisor_norm_proper_split_input. ((exists ge_norm_rp_proper_split_inputnorm ge_norm_rn_proper_split_inputnorm ge_norm_ip_proper_split_inputnorm ge_norm_in_proper_split_inputnorm. ((exists ge_representation_real_code_proper_split_inputnormrepresentation ge_representation_imaginary_code_proper_split_inputnormrepresentation. (((d) = ((ge_representation_real_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation)) * S ((ge_representation_real_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation)) + ((ge_representation_imaginary_code_proper_split_inputnormrepresentation) + (ge_representation_imaginary_code_proper_split_inputnormrepresentation))) /\ ((exists ge_balance_positive_proper_split_inputnormrepresentationreal ge_balance_negative_proper_split_inputnormrepresentationreal. (((((ge_representation_real_code_proper_split_inputnormrepresentation) = 2 * (ge_balance_positive_proper_split_inputnormrepresentationreal) /\ (ge_balance_negative_proper_split_inputnormrepresentationreal) = 0) \/ exists ge_signed_half_proper_split_inputnormrepresentationrealdecode. (((ge_representation_real_code_proper_split_inputnormrepresentation) = 2 * ge_signed_half_proper_split_inputnormrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_split_inputnormrepresentationreal) = 0) /\ (ge_balance_negative_proper_split_inputnormrepresentationreal) = S ge_signed_half_proper_split_inputnormrepresentationrealdecode))) /\ ((ge_norm_rp_proper_split_inputnorm) + ge_balance_negative_proper_split_inputnormrepresentationreal = (ge_norm_rn_proper_split_inputnorm) + ge_balance_positive_proper_split_inputnormrepresentationreal))) /\ (exists ge_balance_positive_proper_split_inputnormrepresentationimaginary ge_balance_negative_proper_split_inputnormrepresentationimaginary. (((((ge_representation_imaginary_code_proper_split_inputnormrepresentation) = 2 * (ge_balance_positive_proper_split_inputnormrepresentationimaginary) /\ (ge_balance_negative_proper_split_inputnormrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_split_inputnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_split_inputnormrepresentation) = 2 * ge_signed_half_proper_split_inputnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_split_inputnormrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_split_inputnormrepresentationimaginary) = S ge_signed_half_proper_split_inputnormrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_split_inputnorm) + ge_balance_negative_proper_split_inputnormrepresentationimaginary = (ge_norm_in_proper_split_inputnorm) + ge_balance_positive_proper_split_inputnormrepresentationimaginary)))))) /\ (exists ge_real_square_proper_split_inputnormsquare ge_imaginary_square_proper_split_inputnormsquare. ((((((ge_norm_rp_proper_split_inputnorm) * (ge_norm_rp_proper_split_inputnorm))) + (((ge_norm_rn_proper_split_inputnorm) * (ge_norm_rn_proper_split_inputnorm)))) = ((ge_real_square_proper_split_inputnormsquare) + (((((ge_norm_rp_proper_split_inputnorm) * (ge_norm_rn_proper_split_inputnorm))) + (((ge_norm_rn_proper_split_inputnorm) * (ge_norm_rp_proper_split_inputnorm))))))) /\ ((((((ge_norm_ip_proper_split_inputnorm) * (ge_norm_ip_proper_split_inputnorm))) + (((ge_norm_in_proper_split_inputnorm) * (ge_norm_in_proper_split_inputnorm)))) = ((ge_imaginary_square_proper_split_inputnormsquare) + (((((ge_norm_ip_proper_split_inputnorm) * (ge_norm_in_proper_split_inputnorm))) + (((ge_norm_in_proper_split_inputnorm) * (ge_norm_ip_proper_split_inputnorm))))))) /\ ((gr_proper_divisor_norm_proper_split_input) = ge_real_square_proper_split_inputnormsquare + ge_imaginary_square_proper_split_inputnormsquare)))))) /\ (exists ge_gap_proper_split_inputstrict. ge_gap_proper_split_inputstrict + S (gr_proper_divisor_norm_proper_split_input) = (N))))))) -> (exists ge_norm_rp_proper_split_norm ge_norm_rn_proper_split_norm ge_norm_ip_proper_split_norm ge_norm_in_proper_split_norm. ((exists ge_representation_real_code_proper_split_normrepresentation ge_representation_imaginary_code_proper_split_normrepresentation. (((z) = ((ge_representation_real_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation)) * S ((ge_representation_real_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation)) + ((ge_representation_imaginary_code_proper_split_normrepresentation) + (ge_representation_imaginary_code_proper_split_normrepresentation))) /\ ((exists ge_balance_positive_proper_split_normrepresentationreal ge_balance_negative_proper_split_normrepresentationreal. (((((ge_representation_real_code_proper_split_normrepresentation) = 2 * (ge_balance_positive_proper_split_normrepresentationreal) /\ (ge_balance_negative_proper_split_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_split_normrepresentationrealdecode. (((ge_representation_real_code_proper_split_normrepresentation) = 2 * ge_signed_half_proper_split_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_split_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_split_normrepresentationreal) = S ge_signed_half_proper_split_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_split_norm) + ge_balance_negative_proper_split_normrepresentationreal = (ge_norm_rn_proper_split_norm) + ge_balance_positive_proper_split_normrepresentationreal))) /\ (exists ge_balance_positive_proper_split_normrepresentationimaginary ge_balance_negative_proper_split_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_split_normrepresentation) = 2 * (ge_balance_positive_proper_split_normrepresentationimaginary) /\ (ge_balance_negative_proper_split_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_split_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_split_normrepresentation) = 2 * ge_signed_half_proper_split_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_split_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_split_normrepresentationimaginary) = S ge_signed_half_proper_split_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_split_norm) + ge_balance_negative_proper_split_normrepresentationimaginary = (ge_norm_in_proper_split_norm) + ge_balance_positive_proper_split_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_split_normsquare ge_imaginary_square_proper_split_normsquare. ((((((ge_norm_rp_proper_split_norm) * (ge_norm_rp_proper_split_norm))) + (((ge_norm_rn_proper_split_norm) * (ge_norm_rn_proper_split_norm)))) = ((ge_real_square_proper_split_normsquare) + (((((ge_norm_rp_proper_split_norm) * (ge_norm_rn_proper_split_norm))) + (((ge_norm_rn_proper_split_norm) * (ge_norm_rp_proper_split_norm))))))) /\ ((((((ge_norm_ip_proper_split_norm) * (ge_norm_ip_proper_split_norm))) + (((ge_norm_in_proper_split_norm) * (ge_norm_in_proper_split_norm)))) = ((ge_imaginary_square_proper_split_normsquare) + (((((ge_norm_ip_proper_split_norm) * (ge_norm_in_proper_split_norm))) + (((ge_norm_in_proper_split_norm) * (ge_norm_ip_proper_split_norm))))))) /\ ((N) = ge_real_square_proper_split_normsquare + ge_imaginary_square_proper_split_normsquare)))))) -> ~(z=0) -> (exists q D Q. (((exists ge_first_rp_proper_constructed_splitproduct ge_first_rn_proper_constructed_splitproduct ge_first_ip_proper_constructed_splitproduct ge_first_in_proper_constructed_splitproduct ge_second_rp_proper_constructed_splitproduct ge_second_rn_proper_constructed_splitproduct ge_second_ip_proper_constructed_splitproduct ge_second_in_proper_constructed_splitproduct. ((exists ge_representation_real_code_proper_constructed_splitproductfirst ge_representation_imaginary_code_proper_constructed_splitproductfirst. (((d) = ((ge_representation_real_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst)) * S ((ge_representation_real_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitproductfirst) + (ge_representation_imaginary_code_proper_constructed_splitproductfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitproductfirstreal ge_balance_negative_proper_constructed_splitproductfirstreal. (((((ge_representation_real_code_proper_constructed_splitproductfirst) = 2 * (ge_balance_positive_proper_constructed_splitproductfirstreal) /\ (ge_balance_negative_proper_constructed_splitproductfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitproductfirst) = 2 * ge_signed_half_proper_constructed_splitproductfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductfirstreal) = S ge_signed_half_proper_constructed_splitproductfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductfirstreal = (ge_first_rn_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductfirstimaginary ge_balance_negative_proper_constructed_splitproductfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductfirst) = 2 * (ge_balance_positive_proper_constructed_splitproductfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitproductfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductfirst) = 2 * ge_signed_half_proper_constructed_splitproductfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductfirstimaginary) = S ge_signed_half_proper_constructed_splitproductfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductfirstimaginary = (ge_first_in_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitproductsecond ge_representation_imaginary_code_proper_constructed_splitproductsecond. (((q) = ((ge_representation_real_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond)) * S ((ge_representation_real_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond)) + ((ge_representation_imaginary_code_proper_constructed_splitproductsecond) + (ge_representation_imaginary_code_proper_constructed_splitproductsecond))) /\ ((exists ge_balance_positive_proper_constructed_splitproductsecondreal ge_balance_negative_proper_constructed_splitproductsecondreal. (((((ge_representation_real_code_proper_constructed_splitproductsecond) = 2 * (ge_balance_positive_proper_constructed_splitproductsecondreal) /\ (ge_balance_negative_proper_constructed_splitproductsecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductsecondrealdecode. (((ge_representation_real_code_proper_constructed_splitproductsecond) = 2 * ge_signed_half_proper_constructed_splitproductsecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductsecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductsecondreal) = S ge_signed_half_proper_constructed_splitproductsecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductsecondreal = (ge_second_rn_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductsecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductsecondimaginary ge_balance_negative_proper_constructed_splitproductsecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductsecond) = 2 * (ge_balance_positive_proper_constructed_splitproductsecondimaginary) /\ (ge_balance_negative_proper_constructed_splitproductsecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductsecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductsecond) = 2 * ge_signed_half_proper_constructed_splitproductsecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductsecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductsecondimaginary) = S ge_signed_half_proper_constructed_splitproductsecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitproduct) + ge_balance_negative_proper_constructed_splitproductsecondimaginary = (ge_second_in_proper_constructed_splitproduct) + ge_balance_positive_proper_constructed_splitproductsecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitproductoutput ge_representation_imaginary_code_proper_constructed_splitproductoutput. (((z) = ((ge_representation_real_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput)) * S ((ge_representation_real_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitproductoutput) + (ge_representation_imaginary_code_proper_constructed_splitproductoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitproductoutputreal ge_balance_negative_proper_constructed_splitproductoutputreal. (((((ge_representation_real_code_proper_constructed_splitproductoutput) = 2 * (ge_balance_positive_proper_constructed_splitproductoutputreal) /\ (ge_balance_negative_proper_constructed_splitproductoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitproductoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitproductoutput) = 2 * ge_signed_half_proper_constructed_splitproductoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitproductoutputreal) = S ge_signed_half_proper_constructed_splitproductoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))))))) + ge_balance_negative_proper_constructed_splitproductoutputreal = (((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))))))) + ge_balance_positive_proper_constructed_splitproductoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitproductoutputimaginary ge_balance_negative_proper_constructed_splitproductoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitproductoutput) = 2 * (ge_balance_positive_proper_constructed_splitproductoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitproductoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitproductoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitproductoutput) = 2 * ge_signed_half_proper_constructed_splitproductoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitproductoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitproductoutputimaginary) = S ge_signed_half_proper_constructed_splitproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))))))) + ge_balance_negative_proper_constructed_splitproductoutputimaginary = (((((((ge_first_rp_proper_constructed_splitproduct) * (ge_second_in_proper_constructed_splitproduct))) + (((ge_first_rn_proper_constructed_splitproduct) * (ge_second_ip_proper_constructed_splitproduct))))) + (((((ge_first_ip_proper_constructed_splitproduct) * (ge_second_rn_proper_constructed_splitproduct))) + (((ge_first_in_proper_constructed_splitproduct) * (ge_second_rp_proper_constructed_splitproduct))))))) + ge_balance_positive_proper_constructed_splitproductoutputimaginary))))))))) /\ ((exists ge_norm_rp_proper_constructed_splitfirst_norm ge_norm_rn_proper_constructed_splitfirst_norm ge_norm_ip_proper_constructed_splitfirst_norm ge_norm_in_proper_constructed_splitfirst_norm. ((exists ge_representation_real_code_proper_constructed_splitfirst_normrepresentation ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation. (((d) = ((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation)) * S ((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal. (((((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal) = S ge_signed_half_proper_constructed_splitfirst_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_constructed_splitfirst_norm) + ge_balance_negative_proper_constructed_splitfirst_normrepresentationreal = (ge_norm_rn_proper_constructed_splitfirst_norm) + ge_balance_positive_proper_constructed_splitfirst_normrepresentationreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary) = S ge_signed_half_proper_constructed_splitfirst_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_constructed_splitfirst_norm) + ge_balance_negative_proper_constructed_splitfirst_normrepresentationimaginary = (ge_norm_in_proper_constructed_splitfirst_norm) + ge_balance_positive_proper_constructed_splitfirst_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_constructed_splitfirst_normsquare ge_imaginary_square_proper_constructed_splitfirst_normsquare. ((((((ge_norm_rp_proper_constructed_splitfirst_norm) * (ge_norm_rp_proper_constructed_splitfirst_norm))) + (((ge_norm_rn_proper_constructed_splitfirst_norm) * (ge_norm_rn_proper_constructed_splitfirst_norm)))) = ((ge_real_square_proper_constructed_splitfirst_normsquare) + (((((ge_norm_rp_proper_constructed_splitfirst_norm) * (ge_norm_rn_proper_constructed_splitfirst_norm))) + (((ge_norm_rn_proper_constructed_splitfirst_norm) * (ge_norm_rp_proper_constructed_splitfirst_norm))))))) /\ ((((((ge_norm_ip_proper_constructed_splitfirst_norm) * (ge_norm_ip_proper_constructed_splitfirst_norm))) + (((ge_norm_in_proper_constructed_splitfirst_norm) * (ge_norm_in_proper_constructed_splitfirst_norm)))) = ((ge_imaginary_square_proper_constructed_splitfirst_normsquare) + (((((ge_norm_ip_proper_constructed_splitfirst_norm) * (ge_norm_in_proper_constructed_splitfirst_norm))) + (((ge_norm_in_proper_constructed_splitfirst_norm) * (ge_norm_ip_proper_constructed_splitfirst_norm))))))) /\ ((D) = ge_real_square_proper_constructed_splitfirst_normsquare + ge_imaginary_square_proper_constructed_splitfirst_normsquare)))))) /\ ((exists ge_norm_rp_proper_constructed_splitsecond_norm ge_norm_rn_proper_constructed_splitsecond_norm ge_norm_ip_proper_constructed_splitsecond_norm ge_norm_in_proper_constructed_splitsecond_norm. ((exists ge_representation_real_code_proper_constructed_splitsecond_normrepresentation ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation. (((q) = ((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation)) * S ((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) + (ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal. (((((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal) = S ge_signed_half_proper_constructed_splitsecond_normrepresentationrealdecode))) /\ ((ge_norm_rp_proper_constructed_splitsecond_norm) + ge_balance_negative_proper_constructed_splitsecond_normrepresentationreal = (ge_norm_rn_proper_constructed_splitsecond_norm) + ge_balance_positive_proper_constructed_splitsecond_normrepresentationreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) = 2 * (ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_normrepresentation) = 2 * ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary) = S ge_signed_half_proper_constructed_splitsecond_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_proper_constructed_splitsecond_norm) + ge_balance_negative_proper_constructed_splitsecond_normrepresentationimaginary = (ge_norm_in_proper_constructed_splitsecond_norm) + ge_balance_positive_proper_constructed_splitsecond_normrepresentationimaginary)))))) /\ (exists ge_real_square_proper_constructed_splitsecond_normsquare ge_imaginary_square_proper_constructed_splitsecond_normsquare. ((((((ge_norm_rp_proper_constructed_splitsecond_norm) * (ge_norm_rp_proper_constructed_splitsecond_norm))) + (((ge_norm_rn_proper_constructed_splitsecond_norm) * (ge_norm_rn_proper_constructed_splitsecond_norm)))) = ((ge_real_square_proper_constructed_splitsecond_normsquare) + (((((ge_norm_rp_proper_constructed_splitsecond_norm) * (ge_norm_rn_proper_constructed_splitsecond_norm))) + (((ge_norm_rn_proper_constructed_splitsecond_norm) * (ge_norm_rp_proper_constructed_splitsecond_norm))))))) /\ ((((((ge_norm_ip_proper_constructed_splitsecond_norm) * (ge_norm_ip_proper_constructed_splitsecond_norm))) + (((ge_norm_in_proper_constructed_splitsecond_norm) * (ge_norm_in_proper_constructed_splitsecond_norm)))) = ((ge_imaginary_square_proper_constructed_splitsecond_normsquare) + (((((ge_norm_ip_proper_constructed_splitsecond_norm) * (ge_norm_in_proper_constructed_splitsecond_norm))) + (((ge_norm_in_proper_constructed_splitsecond_norm) * (ge_norm_ip_proper_constructed_splitsecond_norm))))))) /\ ((Q) = ge_real_square_proper_constructed_splitsecond_normsquare + ge_imaginary_square_proper_constructed_splitsecond_normsquare)))))) /\ ((~(exists gr_inverse_proper_constructed_splitfirst_nonunit. (exists ge_first_rp_proper_constructed_splitfirst_nonunitidentity ge_first_rn_proper_constructed_splitfirst_nonunitidentity ge_first_ip_proper_constructed_splitfirst_nonunitidentity ge_first_in_proper_constructed_splitfirst_nonunitidentity ge_second_rp_proper_constructed_splitfirst_nonunitidentity ge_second_rn_proper_constructed_splitfirst_nonunitidentity ge_second_ip_proper_constructed_splitfirst_nonunitidentity ge_second_in_proper_constructed_splitfirst_nonunitidentity. ((exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst. (((d) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstreal = (ge_first_rn_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityfirstimaginary = (ge_first_in_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond. (((gr_inverse_proper_constructed_splitfirst_nonunit) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondreal = (ge_second_rn_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitfirst_nonunitidentity) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentitysecondimaginary = (ge_second_in_proper_constructed_splitfirst_nonunitidentity) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput)) * S ((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal. (((((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputreal = (((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitfirst_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary) = S ge_signed_half_proper_constructed_splitfirst_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitfirst_nonunitidentityoutputimaginary = (((((((ge_first_rp_proper_constructed_splitfirst_nonunitidentity) * (ge_second_in_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitfirst_nonunitidentity) * (ge_second_ip_proper_constructed_splitfirst_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rn_proper_constructed_splitfirst_nonunitidentity))) + (((ge_first_in_proper_constructed_splitfirst_nonunitidentity) * (ge_second_rp_proper_constructed_splitfirst_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitfirst_nonunitidentityoutputimaginary))))))))))) /\ ((~(exists gr_inverse_proper_constructed_splitsecond_nonunit. (exists ge_first_rp_proper_constructed_splitsecond_nonunitidentity ge_first_rn_proper_constructed_splitsecond_nonunitidentity ge_first_ip_proper_constructed_splitsecond_nonunitidentity ge_first_in_proper_constructed_splitsecond_nonunitidentity ge_second_rp_proper_constructed_splitsecond_nonunitidentity ge_second_rn_proper_constructed_splitsecond_nonunitidentity ge_second_ip_proper_constructed_splitsecond_nonunitidentity ge_second_in_proper_constructed_splitsecond_nonunitidentity. ((exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst. (((q) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstreal = (ge_first_rn_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityfirst) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityfirstimaginary = (ge_first_in_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond. (((gr_inverse_proper_constructed_splitsecond_nonunit) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondreal = (ge_second_rn_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentitysecond) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_proper_constructed_splitsecond_nonunitidentity) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentitysecondimaginary = (ge_second_in_proper_constructed_splitsecond_nonunitidentity) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput. (((6) = ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput)) * S ((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput)) + ((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) + (ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput))) /\ ((exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal. (((((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode. (((ge_representation_real_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputreal = (((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_proper_constructed_splitsecond_nonunitidentityoutput) = 2 * ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary) = S ge_signed_half_proper_constructed_splitsecond_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_negative_proper_constructed_splitsecond_nonunitidentityoutputimaginary = (((((((ge_first_rp_proper_constructed_splitsecond_nonunitidentity) * (ge_second_in_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_rn_proper_constructed_splitsecond_nonunitidentity) * (ge_second_ip_proper_constructed_splitsecond_nonunitidentity))))) + (((((ge_first_ip_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rn_proper_constructed_splitsecond_nonunitidentity))) + (((ge_first_in_proper_constructed_splitsecond_nonunitidentity) * (ge_second_rp_proper_constructed_splitsecond_nonunitidentity))))))) + ge_balance_positive_proper_constructed_splitsecond_nonunitidentityoutputimaginary))))))))))) /\ ((exists ge_gap_proper_constructed_splitfirst_strict. ge_gap_proper_constructed_splitfirst_strict + S (D) = (N)) /\ (exists ge_gap_proper_constructed_splitsecond_strict. ge_gap_proper_constructed_splitsecond_strict + S (Q) = (N))))))))))Complete tactic proof in conservative notation
All 79 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
79 script commands · 24 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 (4)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–10
03Establish hfactorL11–19
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian divisor norm factor.
- L11
have hfactor : ∃ q. ∃ Q. GMul(d,q,z) ∧ (GNorm(q,Q) ∧ N = x · Q)Definitions: GMul(d,q,z)GNorm(q,Q)Original native command in the exact edition - L12
specialize gaussian_divisor_norm_factor (d) - L13
specialize gaussian_divisor_norm_factor (z) - L14
specialize gaussian_divisor_norm_factor (x) - L15
specialize gaussian_divisor_norm_factor (N) - L16
apply gaussian_divisor_norm_factor - L17
exact hd_right_left - L18
exact hd_right_right_witness_left - L19
exact hn
04Separate the logical casesL20–23
05Establish hquL24–25
Establish this local claim before using it. It is not an additional assumption.
06Establish heqL26–34
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian norm functional.
- L26
have heq : x2=1 - L27
specialize gaussian_norm_functional (x1) - L28
specialize gaussian_norm_functional (x2) - L29
specialize gaussian_norm_functional (1) - L30
apply gaussian_norm_functional - L31
exact hfactor_witness_witness_right_left - L32
specialize gaussian_unit_has_norm_one (x1) - L33
apply gaussian_unit_has_norm_one - L34
exact hu
07Establish htotalL35–43
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul one.
08Establish hstrictL44–53
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian search norm factors strict.
- L44
have hstrict : Lt(x,N) ∧ Lt(x2,N)Definitions: Lt(x,N)Lt(x2,N)Original native command in the exact edition - L45
specialize gaussian_search_norm_factors_strict (d) - L46
specialize gaussian_search_norm_factors_strict (x1) - L47
specialize gaussian_search_norm_factors_strict (x) - L48
specialize gaussian_search_norm_factors_strict (x2) - L49
specialize gaussian_search_norm_factors_strict (N) - L50
apply gaussian_search_norm_factors_strict - L51
exact hd_right_right_witness_left - L52
exact hfactor_witness_witness_right_left - L53
exact hfactor_witness_witness_right_right
09Fix variables and assumptionsL54–54
Work with arbitrary variables or the premises of the current implication.
- L54
intro hzero
10Use earlier factsL55–62
11Separate the logical casesL63–63
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L63
cases hstrict
12Construct an explicit witnessL64–66
13Separate the logical casesL67–67
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L67
split
14Use earlier factsL68–68
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L68
exact hfactor_witness_witness_left
15Separate the logical casesL69–69
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L69
split
16Use earlier factsL70–70
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L70
exact hd_right_right_witness_left
17Separate the logical casesL71–71
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L71
split
18Use earlier factsL72–72
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L72
exact hfactor_witness_witness_right_left
19Separate the logical casesL73–73
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L73
split
20Use earlier factsL74–74
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L74
exact hd_left
21Separate the logical casesL75–75
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L75
split
22Use earlier factsL76–76
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L76
exact hqu
23Separate the logical casesL77–77
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L77
split
Original defined command ledger · 79 lines
- 0001
intro d - 0002
intro z - 0003
intro N - 0004
intro hd - 0005
intro hn - 0006
intro hz - 0007
cases hd - 0008
cases hd_right - 0009
cases hd_right_right - 0010
cases hd_right_right_witness - 0011
have hfactor : ∃ q. ∃ Q. GMul(d,q,z) ∧ (GNorm(q,Q) ∧ N = x · Q) - 0012
specialize gaussian_divisor_norm_factor (d) - 0013
specialize gaussian_divisor_norm_factor (z) - 0014
specialize gaussian_divisor_norm_factor (x) - 0015
specialize gaussian_divisor_norm_factor (N) - 0016
apply gaussian_divisor_norm_factor - 0017
exact hd_right_left - 0018
exact hd_right_right_witness_left - 0019
exact hn - 0020
cases hfactor - 0021
cases hfactor_witness - 0022
cases hfactor_witness_witness - 0023
cases hfactor_witness_witness_right - 0024
have hqu : ¬GUnit(x1) - 0025
intro hu - 0026
have heq : x2=1 - 0027
specialize gaussian_norm_functional (x1) - 0028
specialize gaussian_norm_functional (x2) - 0029
specialize gaussian_norm_functional (1) - 0030
apply gaussian_norm_functional - 0031
exact hfactor_witness_witness_right_left - 0032
specialize gaussian_unit_has_norm_one (x1) - 0033
apply gaussian_unit_has_norm_one - 0034
exact hu - 0035
have htotal : N=x - 0036
trans x*x2 - 0037
exact hfactor_witness_witness_right_right - 0038
rewrite heq - 0039
apply mul_one - 0040
rewrite htotal at hd_right_right_witness_right - 0041
specialize lt_irrefl_expanded (x) - 0042
apply lt_irrefl_expanded - 0043
exact hd_right_right_witness_right - 0044
have hstrict : Lt(x,N) ∧ Lt(x2,N) - 0045
specialize gaussian_search_norm_factors_strict (d) - 0046
specialize gaussian_search_norm_factors_strict (x1) - 0047
specialize gaussian_search_norm_factors_strict (x) - 0048
specialize gaussian_search_norm_factors_strict (x2) - 0049
specialize gaussian_search_norm_factors_strict (N) - 0050
apply gaussian_search_norm_factors_strict - 0051
exact hd_right_right_witness_left - 0052
exact hfactor_witness_witness_right_left - 0053
exact hfactor_witness_witness_right_right - 0054
intro hzero - 0055
specialize gaussian_norm_nonzero (z) - 0056
specialize gaussian_norm_nonzero (N) - 0057
apply gaussian_norm_nonzero - 0058
exact hn - 0059
exact hz - 0060
exact hzero - 0061
exact hd_left - 0062
exact hqu - 0063
cases hstrict - 0064
exists (x1) - 0065
exists (x) - 0066
exists (x2) - 0067
split - 0068
exact hfactor_witness_witness_left - 0069
split - 0070
exact hd_right_right_witness_left - 0071
split - 0072
exact hfactor_witness_witness_right_left - 0073
split - 0074
exact hd_left - 0075
split - 0076
exact hqu - 0077
split - 0078
exact hstrict_left - 0079
exact hstrict_right