Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.
Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.
Exact theorem in conservative defined notation
∀ a. ∀ b. GAssociate(a,b) → GDvd(a,b)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall a b. (exists gr_unit_associate_division. ((exists gr_inverse_associate_divisionunit. (exists ge_first_rp_associate_divisionunitidentity ge_first_rn_associate_divisionunitidentity ge_first_ip_associate_divisionunitidentity ge_first_in_associate_divisionunitidentity ge_second_rp_associate_divisionunitidentity ge_second_rn_associate_divisionunitidentity ge_second_ip_associate_divisionunitidentity ge_second_in_associate_divisionunitidentity. ((exists ge_representation_real_code_associate_divisionunitidentityfirst ge_representation_imaginary_code_associate_divisionunitidentityfirst. (((gr_unit_associate_division) = ((ge_representation_real_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst)) * S ((ge_representation_real_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst)) + ((ge_representation_imaginary_code_associate_divisionunitidentityfirst) + (ge_representation_imaginary_code_associate_divisionunitidentityfirst))) /\ ((exists ge_balance_positive_associate_divisionunitidentityfirstreal ge_balance_negative_associate_divisionunitidentityfirstreal. (((((ge_representation_real_code_associate_divisionunitidentityfirst) = 2 * (ge_balance_positive_associate_divisionunitidentityfirstreal) /\ (ge_balance_negative_associate_divisionunitidentityfirstreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentityfirstrealdecode. (((ge_representation_real_code_associate_divisionunitidentityfirst) = 2 * ge_signed_half_associate_divisionunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityfirstreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentityfirstreal) = S ge_signed_half_associate_divisionunitidentityfirstrealdecode))) /\ ((ge_first_rp_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentityfirstreal = (ge_first_rn_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentityfirstreal))) /\ (exists ge_balance_positive_associate_divisionunitidentityfirstimaginary ge_balance_negative_associate_divisionunitidentityfirstimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentityfirst) = 2 * (ge_balance_positive_associate_divisionunitidentityfirstimaginary) /\ (ge_balance_negative_associate_divisionunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentityfirst) = 2 * ge_signed_half_associate_divisionunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentityfirstimaginary) = S ge_signed_half_associate_divisionunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentityfirstimaginary = (ge_first_in_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_divisionunitidentitysecond ge_representation_imaginary_code_associate_divisionunitidentitysecond. (((gr_inverse_associate_divisionunit) = ((ge_representation_real_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond)) * S ((ge_representation_real_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond)) + ((ge_representation_imaginary_code_associate_divisionunitidentitysecond) + (ge_representation_imaginary_code_associate_divisionunitidentitysecond))) /\ ((exists ge_balance_positive_associate_divisionunitidentitysecondreal ge_balance_negative_associate_divisionunitidentitysecondreal. (((((ge_representation_real_code_associate_divisionunitidentitysecond) = 2 * (ge_balance_positive_associate_divisionunitidentitysecondreal) /\ (ge_balance_negative_associate_divisionunitidentitysecondreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentitysecondrealdecode. (((ge_representation_real_code_associate_divisionunitidentitysecond) = 2 * ge_signed_half_associate_divisionunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentitysecondreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentitysecondreal) = S ge_signed_half_associate_divisionunitidentitysecondrealdecode))) /\ ((ge_second_rp_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentitysecondreal = (ge_second_rn_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentitysecondreal))) /\ (exists ge_balance_positive_associate_divisionunitidentitysecondimaginary ge_balance_negative_associate_divisionunitidentitysecondimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentitysecond) = 2 * (ge_balance_positive_associate_divisionunitidentitysecondimaginary) /\ (ge_balance_negative_associate_divisionunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentitysecond) = 2 * ge_signed_half_associate_divisionunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentitysecondimaginary) = S ge_signed_half_associate_divisionunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_associate_divisionunitidentity) + ge_balance_negative_associate_divisionunitidentitysecondimaginary = (ge_second_in_associate_divisionunitidentity) + ge_balance_positive_associate_divisionunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_associate_divisionunitidentityoutput ge_representation_imaginary_code_associate_divisionunitidentityoutput. (((6) = ((ge_representation_real_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput)) * S ((ge_representation_real_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput)) + ((ge_representation_imaginary_code_associate_divisionunitidentityoutput) + (ge_representation_imaginary_code_associate_divisionunitidentityoutput))) /\ ((exists ge_balance_positive_associate_divisionunitidentityoutputreal ge_balance_negative_associate_divisionunitidentityoutputreal. (((((ge_representation_real_code_associate_divisionunitidentityoutput) = 2 * (ge_balance_positive_associate_divisionunitidentityoutputreal) /\ (ge_balance_negative_associate_divisionunitidentityoutputreal) = 0) \/ exists ge_signed_half_associate_divisionunitidentityoutputrealdecode. (((ge_representation_real_code_associate_divisionunitidentityoutput) = 2 * ge_signed_half_associate_divisionunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityoutputreal) = 0) /\ (ge_balance_negative_associate_divisionunitidentityoutputreal) = S ge_signed_half_associate_divisionunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))))))) + ge_balance_negative_associate_divisionunitidentityoutputreal = (((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))))))) + ge_balance_positive_associate_divisionunitidentityoutputreal))) /\ (exists ge_balance_positive_associate_divisionunitidentityoutputimaginary ge_balance_negative_associate_divisionunitidentityoutputimaginary. (((((ge_representation_imaginary_code_associate_divisionunitidentityoutput) = 2 * (ge_balance_positive_associate_divisionunitidentityoutputimaginary) /\ (ge_balance_negative_associate_divisionunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_associate_divisionunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_associate_divisionunitidentityoutput) = 2 * ge_signed_half_associate_divisionunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_divisionunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_associate_divisionunitidentityoutputimaginary) = S ge_signed_half_associate_divisionunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))))))) + ge_balance_negative_associate_divisionunitidentityoutputimaginary = (((((((ge_first_rp_associate_divisionunitidentity) * (ge_second_in_associate_divisionunitidentity))) + (((ge_first_rn_associate_divisionunitidentity) * (ge_second_ip_associate_divisionunitidentity))))) + (((((ge_first_ip_associate_divisionunitidentity) * (ge_second_rn_associate_divisionunitidentity))) + (((ge_first_in_associate_divisionunitidentity) * (ge_second_rp_associate_divisionunitidentity))))))) + ge_balance_positive_associate_divisionunitidentityoutputimaginary)))))))))) /\ (exists ge_first_rp_associate_divisiontransport ge_first_rn_associate_divisiontransport ge_first_ip_associate_divisiontransport ge_first_in_associate_divisiontransport ge_second_rp_associate_divisiontransport ge_second_rn_associate_divisiontransport ge_second_ip_associate_divisiontransport ge_second_in_associate_divisiontransport. ((exists ge_representation_real_code_associate_divisiontransportfirst ge_representation_imaginary_code_associate_divisiontransportfirst. (((gr_unit_associate_division) = ((ge_representation_real_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst)) * S ((ge_representation_real_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst)) + ((ge_representation_imaginary_code_associate_divisiontransportfirst) + (ge_representation_imaginary_code_associate_divisiontransportfirst))) /\ ((exists ge_balance_positive_associate_divisiontransportfirstreal ge_balance_negative_associate_divisiontransportfirstreal. (((((ge_representation_real_code_associate_divisiontransportfirst) = 2 * (ge_balance_positive_associate_divisiontransportfirstreal) /\ (ge_balance_negative_associate_divisiontransportfirstreal) = 0) \/ exists ge_signed_half_associate_divisiontransportfirstrealdecode. (((ge_representation_real_code_associate_divisiontransportfirst) = 2 * ge_signed_half_associate_divisiontransportfirstrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportfirstreal) = 0) /\ (ge_balance_negative_associate_divisiontransportfirstreal) = S ge_signed_half_associate_divisiontransportfirstrealdecode))) /\ ((ge_first_rp_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportfirstreal = (ge_first_rn_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportfirstreal))) /\ (exists ge_balance_positive_associate_divisiontransportfirstimaginary ge_balance_negative_associate_divisiontransportfirstimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportfirst) = 2 * (ge_balance_positive_associate_divisiontransportfirstimaginary) /\ (ge_balance_negative_associate_divisiontransportfirstimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportfirstimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportfirst) = 2 * ge_signed_half_associate_divisiontransportfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportfirstimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportfirstimaginary) = S ge_signed_half_associate_divisiontransportfirstimaginarydecode))) /\ ((ge_first_ip_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportfirstimaginary = (ge_first_in_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_divisiontransportsecond ge_representation_imaginary_code_associate_divisiontransportsecond. (((a) = ((ge_representation_real_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond)) * S ((ge_representation_real_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond)) + ((ge_representation_imaginary_code_associate_divisiontransportsecond) + (ge_representation_imaginary_code_associate_divisiontransportsecond))) /\ ((exists ge_balance_positive_associate_divisiontransportsecondreal ge_balance_negative_associate_divisiontransportsecondreal. (((((ge_representation_real_code_associate_divisiontransportsecond) = 2 * (ge_balance_positive_associate_divisiontransportsecondreal) /\ (ge_balance_negative_associate_divisiontransportsecondreal) = 0) \/ exists ge_signed_half_associate_divisiontransportsecondrealdecode. (((ge_representation_real_code_associate_divisiontransportsecond) = 2 * ge_signed_half_associate_divisiontransportsecondrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportsecondreal) = 0) /\ (ge_balance_negative_associate_divisiontransportsecondreal) = S ge_signed_half_associate_divisiontransportsecondrealdecode))) /\ ((ge_second_rp_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportsecondreal = (ge_second_rn_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportsecondreal))) /\ (exists ge_balance_positive_associate_divisiontransportsecondimaginary ge_balance_negative_associate_divisiontransportsecondimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportsecond) = 2 * (ge_balance_positive_associate_divisiontransportsecondimaginary) /\ (ge_balance_negative_associate_divisiontransportsecondimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportsecondimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportsecond) = 2 * ge_signed_half_associate_divisiontransportsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportsecondimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportsecondimaginary) = S ge_signed_half_associate_divisiontransportsecondimaginarydecode))) /\ ((ge_second_ip_associate_divisiontransport) + ge_balance_negative_associate_divisiontransportsecondimaginary = (ge_second_in_associate_divisiontransport) + ge_balance_positive_associate_divisiontransportsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_divisiontransportoutput ge_representation_imaginary_code_associate_divisiontransportoutput. (((b) = ((ge_representation_real_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput)) * S ((ge_representation_real_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput)) + ((ge_representation_imaginary_code_associate_divisiontransportoutput) + (ge_representation_imaginary_code_associate_divisiontransportoutput))) /\ ((exists ge_balance_positive_associate_divisiontransportoutputreal ge_balance_negative_associate_divisiontransportoutputreal. (((((ge_representation_real_code_associate_divisiontransportoutput) = 2 * (ge_balance_positive_associate_divisiontransportoutputreal) /\ (ge_balance_negative_associate_divisiontransportoutputreal) = 0) \/ exists ge_signed_half_associate_divisiontransportoutputrealdecode. (((ge_representation_real_code_associate_divisiontransportoutput) = 2 * ge_signed_half_associate_divisiontransportoutputrealdecode + 1 /\ (ge_balance_positive_associate_divisiontransportoutputreal) = 0) /\ (ge_balance_negative_associate_divisiontransportoutputreal) = S ge_signed_half_associate_divisiontransportoutputrealdecode))) /\ ((((((((ge_first_rp_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))))))) + ge_balance_negative_associate_divisiontransportoutputreal = (((((((ge_first_rp_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))))))) + ge_balance_positive_associate_divisiontransportoutputreal))) /\ (exists ge_balance_positive_associate_divisiontransportoutputimaginary ge_balance_negative_associate_divisiontransportoutputimaginary. (((((ge_representation_imaginary_code_associate_divisiontransportoutput) = 2 * (ge_balance_positive_associate_divisiontransportoutputimaginary) /\ (ge_balance_negative_associate_divisiontransportoutputimaginary) = 0) \/ exists ge_signed_half_associate_divisiontransportoutputimaginarydecode. (((ge_representation_imaginary_code_associate_divisiontransportoutput) = 2 * ge_signed_half_associate_divisiontransportoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_divisiontransportoutputimaginary) = 0) /\ (ge_balance_negative_associate_divisiontransportoutputimaginary) = S ge_signed_half_associate_divisiontransportoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))))))) + ge_balance_negative_associate_divisiontransportoutputimaginary = (((((((ge_first_rp_associate_divisiontransport) * (ge_second_in_associate_divisiontransport))) + (((ge_first_rn_associate_divisiontransport) * (ge_second_ip_associate_divisiontransport))))) + (((((ge_first_ip_associate_divisiontransport) * (ge_second_rn_associate_divisiontransport))) + (((ge_first_in_associate_divisiontransport) * (ge_second_rp_associate_divisiontransport))))))) + ge_balance_positive_associate_divisiontransportoutputimaginary))))))))))) -> (exists gr_quotient_associate_divides. (exists ge_first_rp_associate_dividesproduct ge_first_rn_associate_dividesproduct ge_first_ip_associate_dividesproduct ge_first_in_associate_dividesproduct ge_second_rp_associate_dividesproduct ge_second_rn_associate_dividesproduct ge_second_ip_associate_dividesproduct ge_second_in_associate_dividesproduct. ((exists ge_representation_real_code_associate_dividesproductfirst ge_representation_imaginary_code_associate_dividesproductfirst. (((a) = ((ge_representation_real_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst)) * S ((ge_representation_real_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst)) + ((ge_representation_imaginary_code_associate_dividesproductfirst) + (ge_representation_imaginary_code_associate_dividesproductfirst))) /\ ((exists ge_balance_positive_associate_dividesproductfirstreal ge_balance_negative_associate_dividesproductfirstreal. (((((ge_representation_real_code_associate_dividesproductfirst) = 2 * (ge_balance_positive_associate_dividesproductfirstreal) /\ (ge_balance_negative_associate_dividesproductfirstreal) = 0) \/ exists ge_signed_half_associate_dividesproductfirstrealdecode. (((ge_representation_real_code_associate_dividesproductfirst) = 2 * ge_signed_half_associate_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductfirstreal) = 0) /\ (ge_balance_negative_associate_dividesproductfirstreal) = S ge_signed_half_associate_dividesproductfirstrealdecode))) /\ ((ge_first_rp_associate_dividesproduct) + ge_balance_negative_associate_dividesproductfirstreal = (ge_first_rn_associate_dividesproduct) + ge_balance_positive_associate_dividesproductfirstreal))) /\ (exists ge_balance_positive_associate_dividesproductfirstimaginary ge_balance_negative_associate_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_associate_dividesproductfirst) = 2 * (ge_balance_positive_associate_dividesproductfirstimaginary) /\ (ge_balance_negative_associate_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductfirst) = 2 * ge_signed_half_associate_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductfirstimaginary) = S ge_signed_half_associate_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_associate_dividesproduct) + ge_balance_negative_associate_dividesproductfirstimaginary = (ge_first_in_associate_dividesproduct) + ge_balance_positive_associate_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_dividesproductsecond ge_representation_imaginary_code_associate_dividesproductsecond. (((gr_quotient_associate_divides) = ((ge_representation_real_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond)) * S ((ge_representation_real_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond)) + ((ge_representation_imaginary_code_associate_dividesproductsecond) + (ge_representation_imaginary_code_associate_dividesproductsecond))) /\ ((exists ge_balance_positive_associate_dividesproductsecondreal ge_balance_negative_associate_dividesproductsecondreal. (((((ge_representation_real_code_associate_dividesproductsecond) = 2 * (ge_balance_positive_associate_dividesproductsecondreal) /\ (ge_balance_negative_associate_dividesproductsecondreal) = 0) \/ exists ge_signed_half_associate_dividesproductsecondrealdecode. (((ge_representation_real_code_associate_dividesproductsecond) = 2 * ge_signed_half_associate_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductsecondreal) = 0) /\ (ge_balance_negative_associate_dividesproductsecondreal) = S ge_signed_half_associate_dividesproductsecondrealdecode))) /\ ((ge_second_rp_associate_dividesproduct) + ge_balance_negative_associate_dividesproductsecondreal = (ge_second_rn_associate_dividesproduct) + ge_balance_positive_associate_dividesproductsecondreal))) /\ (exists ge_balance_positive_associate_dividesproductsecondimaginary ge_balance_negative_associate_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_associate_dividesproductsecond) = 2 * (ge_balance_positive_associate_dividesproductsecondimaginary) /\ (ge_balance_negative_associate_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductsecond) = 2 * ge_signed_half_associate_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductsecondimaginary) = S ge_signed_half_associate_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_associate_dividesproduct) + ge_balance_negative_associate_dividesproductsecondimaginary = (ge_second_in_associate_dividesproduct) + ge_balance_positive_associate_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_dividesproductoutput ge_representation_imaginary_code_associate_dividesproductoutput. (((b) = ((ge_representation_real_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput)) * S ((ge_representation_real_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput)) + ((ge_representation_imaginary_code_associate_dividesproductoutput) + (ge_representation_imaginary_code_associate_dividesproductoutput))) /\ ((exists ge_balance_positive_associate_dividesproductoutputreal ge_balance_negative_associate_dividesproductoutputreal. (((((ge_representation_real_code_associate_dividesproductoutput) = 2 * (ge_balance_positive_associate_dividesproductoutputreal) /\ (ge_balance_negative_associate_dividesproductoutputreal) = 0) \/ exists ge_signed_half_associate_dividesproductoutputrealdecode. (((ge_representation_real_code_associate_dividesproductoutput) = 2 * ge_signed_half_associate_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_associate_dividesproductoutputreal) = 0) /\ (ge_balance_negative_associate_dividesproductoutputreal) = S ge_signed_half_associate_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))))))) + ge_balance_negative_associate_dividesproductoutputreal = (((((((ge_first_rp_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))))))) + ge_balance_positive_associate_dividesproductoutputreal))) /\ (exists ge_balance_positive_associate_dividesproductoutputimaginary ge_balance_negative_associate_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_associate_dividesproductoutput) = 2 * (ge_balance_positive_associate_dividesproductoutputimaginary) /\ (ge_balance_negative_associate_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_associate_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_associate_dividesproductoutput) = 2 * ge_signed_half_associate_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_associate_dividesproductoutputimaginary) = S ge_signed_half_associate_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))))))) + ge_balance_negative_associate_dividesproductoutputimaginary = (((((((ge_first_rp_associate_dividesproduct) * (ge_second_in_associate_dividesproduct))) + (((ge_first_rn_associate_dividesproduct) * (ge_second_ip_associate_dividesproduct))))) + (((((ge_first_ip_associate_dividesproduct) * (ge_second_rn_associate_dividesproduct))) + (((ge_first_in_associate_dividesproduct) * (ge_second_rp_associate_dividesproduct))))))) + ge_balance_positive_associate_dividesproductoutputimaginary))))))))))Complete tactic proof in conservative notation
All 11 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
11 script commands · 4 reading checkpoints · 0 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 (1)
01Fix variables and assumptionsL1–3
02Separate the logical casesL4–5
03Construct an explicit witnessL6–6
Supply the displayed value, then prove that it has the required property.
- L6
exists (x)
04Use earlier factsL7–11
Original defined command ledger · 11 lines
- 0001
intro a - 0002
intro b - 0003
intro h - 0004
cases h - 0005
cases h_witness - 0006
exists (x) - 0007
specialize gaussian_multiply_commutative (x) - 0008
specialize gaussian_multiply_commutative (a) - 0009
specialize gaussian_multiply_commutative (b) - 0010
apply gaussian_multiply_commutative - 0011
exact h_witness_right