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
∀ u. ∀ v. ∀ w. GMul(u,v,w) → GUnit(u) → GUnit(v) → GUnit(w)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall u v w. (exists ge_first_rp_unit_product ge_first_rn_unit_product ge_first_ip_unit_product ge_first_in_unit_product ge_second_rp_unit_product ge_second_rn_unit_product ge_second_ip_unit_product ge_second_in_unit_product. ((exists ge_representation_real_code_unit_productfirst ge_representation_imaginary_code_unit_productfirst. (((u) = ((ge_representation_real_code_unit_productfirst) + (ge_representation_imaginary_code_unit_productfirst)) * S ((ge_representation_real_code_unit_productfirst) + (ge_representation_imaginary_code_unit_productfirst)) + ((ge_representation_imaginary_code_unit_productfirst) + (ge_representation_imaginary_code_unit_productfirst))) /\ ((exists ge_balance_positive_unit_productfirstreal ge_balance_negative_unit_productfirstreal. (((((ge_representation_real_code_unit_productfirst) = 2 * (ge_balance_positive_unit_productfirstreal) /\ (ge_balance_negative_unit_productfirstreal) = 0) \/ exists ge_signed_half_unit_productfirstrealdecode. (((ge_representation_real_code_unit_productfirst) = 2 * ge_signed_half_unit_productfirstrealdecode + 1 /\ (ge_balance_positive_unit_productfirstreal) = 0) /\ (ge_balance_negative_unit_productfirstreal) = S ge_signed_half_unit_productfirstrealdecode))) /\ ((ge_first_rp_unit_product) + ge_balance_negative_unit_productfirstreal = (ge_first_rn_unit_product) + ge_balance_positive_unit_productfirstreal))) /\ (exists ge_balance_positive_unit_productfirstimaginary ge_balance_negative_unit_productfirstimaginary. (((((ge_representation_imaginary_code_unit_productfirst) = 2 * (ge_balance_positive_unit_productfirstimaginary) /\ (ge_balance_negative_unit_productfirstimaginary) = 0) \/ exists ge_signed_half_unit_productfirstimaginarydecode. (((ge_representation_imaginary_code_unit_productfirst) = 2 * ge_signed_half_unit_productfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_productfirstimaginary) = 0) /\ (ge_balance_negative_unit_productfirstimaginary) = S ge_signed_half_unit_productfirstimaginarydecode))) /\ ((ge_first_ip_unit_product) + ge_balance_negative_unit_productfirstimaginary = (ge_first_in_unit_product) + ge_balance_positive_unit_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_productsecond ge_representation_imaginary_code_unit_productsecond. (((v) = ((ge_representation_real_code_unit_productsecond) + (ge_representation_imaginary_code_unit_productsecond)) * S ((ge_representation_real_code_unit_productsecond) + (ge_representation_imaginary_code_unit_productsecond)) + ((ge_representation_imaginary_code_unit_productsecond) + (ge_representation_imaginary_code_unit_productsecond))) /\ ((exists ge_balance_positive_unit_productsecondreal ge_balance_negative_unit_productsecondreal. (((((ge_representation_real_code_unit_productsecond) = 2 * (ge_balance_positive_unit_productsecondreal) /\ (ge_balance_negative_unit_productsecondreal) = 0) \/ exists ge_signed_half_unit_productsecondrealdecode. (((ge_representation_real_code_unit_productsecond) = 2 * ge_signed_half_unit_productsecondrealdecode + 1 /\ (ge_balance_positive_unit_productsecondreal) = 0) /\ (ge_balance_negative_unit_productsecondreal) = S ge_signed_half_unit_productsecondrealdecode))) /\ ((ge_second_rp_unit_product) + ge_balance_negative_unit_productsecondreal = (ge_second_rn_unit_product) + ge_balance_positive_unit_productsecondreal))) /\ (exists ge_balance_positive_unit_productsecondimaginary ge_balance_negative_unit_productsecondimaginary. (((((ge_representation_imaginary_code_unit_productsecond) = 2 * (ge_balance_positive_unit_productsecondimaginary) /\ (ge_balance_negative_unit_productsecondimaginary) = 0) \/ exists ge_signed_half_unit_productsecondimaginarydecode. (((ge_representation_imaginary_code_unit_productsecond) = 2 * ge_signed_half_unit_productsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_productsecondimaginary) = 0) /\ (ge_balance_negative_unit_productsecondimaginary) = S ge_signed_half_unit_productsecondimaginarydecode))) /\ ((ge_second_ip_unit_product) + ge_balance_negative_unit_productsecondimaginary = (ge_second_in_unit_product) + ge_balance_positive_unit_productsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_productoutput ge_representation_imaginary_code_unit_productoutput. (((w) = ((ge_representation_real_code_unit_productoutput) + (ge_representation_imaginary_code_unit_productoutput)) * S ((ge_representation_real_code_unit_productoutput) + (ge_representation_imaginary_code_unit_productoutput)) + ((ge_representation_imaginary_code_unit_productoutput) + (ge_representation_imaginary_code_unit_productoutput))) /\ ((exists ge_balance_positive_unit_productoutputreal ge_balance_negative_unit_productoutputreal. (((((ge_representation_real_code_unit_productoutput) = 2 * (ge_balance_positive_unit_productoutputreal) /\ (ge_balance_negative_unit_productoutputreal) = 0) \/ exists ge_signed_half_unit_productoutputrealdecode. (((ge_representation_real_code_unit_productoutput) = 2 * ge_signed_half_unit_productoutputrealdecode + 1 /\ (ge_balance_positive_unit_productoutputreal) = 0) /\ (ge_balance_negative_unit_productoutputreal) = S ge_signed_half_unit_productoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product) * (ge_second_rp_unit_product))) + (((ge_first_rn_unit_product) * (ge_second_rn_unit_product))))) + (((((ge_first_ip_unit_product) * (ge_second_in_unit_product))) + (((ge_first_in_unit_product) * (ge_second_ip_unit_product))))))) + ge_balance_negative_unit_productoutputreal = (((((((ge_first_rp_unit_product) * (ge_second_rn_unit_product))) + (((ge_first_rn_unit_product) * (ge_second_rp_unit_product))))) + (((((ge_first_ip_unit_product) * (ge_second_ip_unit_product))) + (((ge_first_in_unit_product) * (ge_second_in_unit_product))))))) + ge_balance_positive_unit_productoutputreal))) /\ (exists ge_balance_positive_unit_productoutputimaginary ge_balance_negative_unit_productoutputimaginary. (((((ge_representation_imaginary_code_unit_productoutput) = 2 * (ge_balance_positive_unit_productoutputimaginary) /\ (ge_balance_negative_unit_productoutputimaginary) = 0) \/ exists ge_signed_half_unit_productoutputimaginarydecode. (((ge_representation_imaginary_code_unit_productoutput) = 2 * ge_signed_half_unit_productoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_productoutputimaginary) = 0) /\ (ge_balance_negative_unit_productoutputimaginary) = S ge_signed_half_unit_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product) * (ge_second_ip_unit_product))) + (((ge_first_rn_unit_product) * (ge_second_in_unit_product))))) + (((((ge_first_ip_unit_product) * (ge_second_rp_unit_product))) + (((ge_first_in_unit_product) * (ge_second_rn_unit_product))))))) + ge_balance_negative_unit_productoutputimaginary = (((((((ge_first_rp_unit_product) * (ge_second_in_unit_product))) + (((ge_first_rn_unit_product) * (ge_second_ip_unit_product))))) + (((((ge_first_ip_unit_product) * (ge_second_rn_unit_product))) + (((ge_first_in_unit_product) * (ge_second_rp_unit_product))))))) + ge_balance_positive_unit_productoutputimaginary))))))))) -> (exists gr_inverse_unit_product_first. (exists ge_first_rp_unit_product_firstidentity ge_first_rn_unit_product_firstidentity ge_first_ip_unit_product_firstidentity ge_first_in_unit_product_firstidentity ge_second_rp_unit_product_firstidentity ge_second_rn_unit_product_firstidentity ge_second_ip_unit_product_firstidentity ge_second_in_unit_product_firstidentity. ((exists ge_representation_real_code_unit_product_firstidentityfirst ge_representation_imaginary_code_unit_product_firstidentityfirst. (((u) = ((ge_representation_real_code_unit_product_firstidentityfirst) + (ge_representation_imaginary_code_unit_product_firstidentityfirst)) * S ((ge_representation_real_code_unit_product_firstidentityfirst) + (ge_representation_imaginary_code_unit_product_firstidentityfirst)) + ((ge_representation_imaginary_code_unit_product_firstidentityfirst) + (ge_representation_imaginary_code_unit_product_firstidentityfirst))) /\ ((exists ge_balance_positive_unit_product_firstidentityfirstreal ge_balance_negative_unit_product_firstidentityfirstreal. (((((ge_representation_real_code_unit_product_firstidentityfirst) = 2 * (ge_balance_positive_unit_product_firstidentityfirstreal) /\ (ge_balance_negative_unit_product_firstidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_firstidentityfirstrealdecode. (((ge_representation_real_code_unit_product_firstidentityfirst) = 2 * ge_signed_half_unit_product_firstidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_firstidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_firstidentityfirstreal) = S ge_signed_half_unit_product_firstidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_firstidentity) + ge_balance_negative_unit_product_firstidentityfirstreal = (ge_first_rn_unit_product_firstidentity) + ge_balance_positive_unit_product_firstidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_firstidentityfirstimaginary ge_balance_negative_unit_product_firstidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_firstidentityfirst) = 2 * (ge_balance_positive_unit_product_firstidentityfirstimaginary) /\ (ge_balance_negative_unit_product_firstidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_firstidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_firstidentityfirst) = 2 * ge_signed_half_unit_product_firstidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_firstidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_firstidentityfirstimaginary) = S ge_signed_half_unit_product_firstidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_firstidentity) + ge_balance_negative_unit_product_firstidentityfirstimaginary = (ge_first_in_unit_product_firstidentity) + ge_balance_positive_unit_product_firstidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_firstidentitysecond ge_representation_imaginary_code_unit_product_firstidentitysecond. (((gr_inverse_unit_product_first) = ((ge_representation_real_code_unit_product_firstidentitysecond) + (ge_representation_imaginary_code_unit_product_firstidentitysecond)) * S ((ge_representation_real_code_unit_product_firstidentitysecond) + (ge_representation_imaginary_code_unit_product_firstidentitysecond)) + ((ge_representation_imaginary_code_unit_product_firstidentitysecond) + (ge_representation_imaginary_code_unit_product_firstidentitysecond))) /\ ((exists ge_balance_positive_unit_product_firstidentitysecondreal ge_balance_negative_unit_product_firstidentitysecondreal. (((((ge_representation_real_code_unit_product_firstidentitysecond) = 2 * (ge_balance_positive_unit_product_firstidentitysecondreal) /\ (ge_balance_negative_unit_product_firstidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_firstidentitysecondrealdecode. (((ge_representation_real_code_unit_product_firstidentitysecond) = 2 * ge_signed_half_unit_product_firstidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_firstidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_firstidentitysecondreal) = S ge_signed_half_unit_product_firstidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_firstidentity) + ge_balance_negative_unit_product_firstidentitysecondreal = (ge_second_rn_unit_product_firstidentity) + ge_balance_positive_unit_product_firstidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_firstidentitysecondimaginary ge_balance_negative_unit_product_firstidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_firstidentitysecond) = 2 * (ge_balance_positive_unit_product_firstidentitysecondimaginary) /\ (ge_balance_negative_unit_product_firstidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_firstidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_firstidentitysecond) = 2 * ge_signed_half_unit_product_firstidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_firstidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_firstidentitysecondimaginary) = S ge_signed_half_unit_product_firstidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_firstidentity) + ge_balance_negative_unit_product_firstidentitysecondimaginary = (ge_second_in_unit_product_firstidentity) + ge_balance_positive_unit_product_firstidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_firstidentityoutput ge_representation_imaginary_code_unit_product_firstidentityoutput. (((6) = ((ge_representation_real_code_unit_product_firstidentityoutput) + (ge_representation_imaginary_code_unit_product_firstidentityoutput)) * S ((ge_representation_real_code_unit_product_firstidentityoutput) + (ge_representation_imaginary_code_unit_product_firstidentityoutput)) + ((ge_representation_imaginary_code_unit_product_firstidentityoutput) + (ge_representation_imaginary_code_unit_product_firstidentityoutput))) /\ ((exists ge_balance_positive_unit_product_firstidentityoutputreal ge_balance_negative_unit_product_firstidentityoutputreal. (((((ge_representation_real_code_unit_product_firstidentityoutput) = 2 * (ge_balance_positive_unit_product_firstidentityoutputreal) /\ (ge_balance_negative_unit_product_firstidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_firstidentityoutputrealdecode. (((ge_representation_real_code_unit_product_firstidentityoutput) = 2 * ge_signed_half_unit_product_firstidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_firstidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_firstidentityoutputreal) = S ge_signed_half_unit_product_firstidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_firstidentity) * (ge_second_rp_unit_product_firstidentity))) + (((ge_first_rn_unit_product_firstidentity) * (ge_second_rn_unit_product_firstidentity))))) + (((((ge_first_ip_unit_product_firstidentity) * (ge_second_in_unit_product_firstidentity))) + (((ge_first_in_unit_product_firstidentity) * (ge_second_ip_unit_product_firstidentity))))))) + ge_balance_negative_unit_product_firstidentityoutputreal = (((((((ge_first_rp_unit_product_firstidentity) * (ge_second_rn_unit_product_firstidentity))) + (((ge_first_rn_unit_product_firstidentity) * (ge_second_rp_unit_product_firstidentity))))) + (((((ge_first_ip_unit_product_firstidentity) * (ge_second_ip_unit_product_firstidentity))) + (((ge_first_in_unit_product_firstidentity) * (ge_second_in_unit_product_firstidentity))))))) + ge_balance_positive_unit_product_firstidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_firstidentityoutputimaginary ge_balance_negative_unit_product_firstidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_firstidentityoutput) = 2 * (ge_balance_positive_unit_product_firstidentityoutputimaginary) /\ (ge_balance_negative_unit_product_firstidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_firstidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_firstidentityoutput) = 2 * ge_signed_half_unit_product_firstidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_firstidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_firstidentityoutputimaginary) = S ge_signed_half_unit_product_firstidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_firstidentity) * (ge_second_ip_unit_product_firstidentity))) + (((ge_first_rn_unit_product_firstidentity) * (ge_second_in_unit_product_firstidentity))))) + (((((ge_first_ip_unit_product_firstidentity) * (ge_second_rp_unit_product_firstidentity))) + (((ge_first_in_unit_product_firstidentity) * (ge_second_rn_unit_product_firstidentity))))))) + ge_balance_negative_unit_product_firstidentityoutputimaginary = (((((((ge_first_rp_unit_product_firstidentity) * (ge_second_in_unit_product_firstidentity))) + (((ge_first_rn_unit_product_firstidentity) * (ge_second_ip_unit_product_firstidentity))))) + (((((ge_first_ip_unit_product_firstidentity) * (ge_second_rn_unit_product_firstidentity))) + (((ge_first_in_unit_product_firstidentity) * (ge_second_rp_unit_product_firstidentity))))))) + ge_balance_positive_unit_product_firstidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_product_second. (exists ge_first_rp_unit_product_secondidentity ge_first_rn_unit_product_secondidentity ge_first_ip_unit_product_secondidentity ge_first_in_unit_product_secondidentity ge_second_rp_unit_product_secondidentity ge_second_rn_unit_product_secondidentity ge_second_ip_unit_product_secondidentity ge_second_in_unit_product_secondidentity. ((exists ge_representation_real_code_unit_product_secondidentityfirst ge_representation_imaginary_code_unit_product_secondidentityfirst. (((v) = ((ge_representation_real_code_unit_product_secondidentityfirst) + (ge_representation_imaginary_code_unit_product_secondidentityfirst)) * S ((ge_representation_real_code_unit_product_secondidentityfirst) + (ge_representation_imaginary_code_unit_product_secondidentityfirst)) + ((ge_representation_imaginary_code_unit_product_secondidentityfirst) + (ge_representation_imaginary_code_unit_product_secondidentityfirst))) /\ ((exists ge_balance_positive_unit_product_secondidentityfirstreal ge_balance_negative_unit_product_secondidentityfirstreal. (((((ge_representation_real_code_unit_product_secondidentityfirst) = 2 * (ge_balance_positive_unit_product_secondidentityfirstreal) /\ (ge_balance_negative_unit_product_secondidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_secondidentityfirstrealdecode. (((ge_representation_real_code_unit_product_secondidentityfirst) = 2 * ge_signed_half_unit_product_secondidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_secondidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_secondidentityfirstreal) = S ge_signed_half_unit_product_secondidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_secondidentity) + ge_balance_negative_unit_product_secondidentityfirstreal = (ge_first_rn_unit_product_secondidentity) + ge_balance_positive_unit_product_secondidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_secondidentityfirstimaginary ge_balance_negative_unit_product_secondidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_secondidentityfirst) = 2 * (ge_balance_positive_unit_product_secondidentityfirstimaginary) /\ (ge_balance_negative_unit_product_secondidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_secondidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_secondidentityfirst) = 2 * ge_signed_half_unit_product_secondidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_secondidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_secondidentityfirstimaginary) = S ge_signed_half_unit_product_secondidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_secondidentity) + ge_balance_negative_unit_product_secondidentityfirstimaginary = (ge_first_in_unit_product_secondidentity) + ge_balance_positive_unit_product_secondidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_secondidentitysecond ge_representation_imaginary_code_unit_product_secondidentitysecond. (((gr_inverse_unit_product_second) = ((ge_representation_real_code_unit_product_secondidentitysecond) + (ge_representation_imaginary_code_unit_product_secondidentitysecond)) * S ((ge_representation_real_code_unit_product_secondidentitysecond) + (ge_representation_imaginary_code_unit_product_secondidentitysecond)) + ((ge_representation_imaginary_code_unit_product_secondidentitysecond) + (ge_representation_imaginary_code_unit_product_secondidentitysecond))) /\ ((exists ge_balance_positive_unit_product_secondidentitysecondreal ge_balance_negative_unit_product_secondidentitysecondreal. (((((ge_representation_real_code_unit_product_secondidentitysecond) = 2 * (ge_balance_positive_unit_product_secondidentitysecondreal) /\ (ge_balance_negative_unit_product_secondidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_secondidentitysecondrealdecode. (((ge_representation_real_code_unit_product_secondidentitysecond) = 2 * ge_signed_half_unit_product_secondidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_secondidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_secondidentitysecondreal) = S ge_signed_half_unit_product_secondidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_secondidentity) + ge_balance_negative_unit_product_secondidentitysecondreal = (ge_second_rn_unit_product_secondidentity) + ge_balance_positive_unit_product_secondidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_secondidentitysecondimaginary ge_balance_negative_unit_product_secondidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_secondidentitysecond) = 2 * (ge_balance_positive_unit_product_secondidentitysecondimaginary) /\ (ge_balance_negative_unit_product_secondidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_secondidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_secondidentitysecond) = 2 * ge_signed_half_unit_product_secondidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_secondidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_secondidentitysecondimaginary) = S ge_signed_half_unit_product_secondidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_secondidentity) + ge_balance_negative_unit_product_secondidentitysecondimaginary = (ge_second_in_unit_product_secondidentity) + ge_balance_positive_unit_product_secondidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_secondidentityoutput ge_representation_imaginary_code_unit_product_secondidentityoutput. (((6) = ((ge_representation_real_code_unit_product_secondidentityoutput) + (ge_representation_imaginary_code_unit_product_secondidentityoutput)) * S ((ge_representation_real_code_unit_product_secondidentityoutput) + (ge_representation_imaginary_code_unit_product_secondidentityoutput)) + ((ge_representation_imaginary_code_unit_product_secondidentityoutput) + (ge_representation_imaginary_code_unit_product_secondidentityoutput))) /\ ((exists ge_balance_positive_unit_product_secondidentityoutputreal ge_balance_negative_unit_product_secondidentityoutputreal. (((((ge_representation_real_code_unit_product_secondidentityoutput) = 2 * (ge_balance_positive_unit_product_secondidentityoutputreal) /\ (ge_balance_negative_unit_product_secondidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_secondidentityoutputrealdecode. (((ge_representation_real_code_unit_product_secondidentityoutput) = 2 * ge_signed_half_unit_product_secondidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_secondidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_secondidentityoutputreal) = S ge_signed_half_unit_product_secondidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_secondidentity) * (ge_second_rp_unit_product_secondidentity))) + (((ge_first_rn_unit_product_secondidentity) * (ge_second_rn_unit_product_secondidentity))))) + (((((ge_first_ip_unit_product_secondidentity) * (ge_second_in_unit_product_secondidentity))) + (((ge_first_in_unit_product_secondidentity) * (ge_second_ip_unit_product_secondidentity))))))) + ge_balance_negative_unit_product_secondidentityoutputreal = (((((((ge_first_rp_unit_product_secondidentity) * (ge_second_rn_unit_product_secondidentity))) + (((ge_first_rn_unit_product_secondidentity) * (ge_second_rp_unit_product_secondidentity))))) + (((((ge_first_ip_unit_product_secondidentity) * (ge_second_ip_unit_product_secondidentity))) + (((ge_first_in_unit_product_secondidentity) * (ge_second_in_unit_product_secondidentity))))))) + ge_balance_positive_unit_product_secondidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_secondidentityoutputimaginary ge_balance_negative_unit_product_secondidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_secondidentityoutput) = 2 * (ge_balance_positive_unit_product_secondidentityoutputimaginary) /\ (ge_balance_negative_unit_product_secondidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_secondidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_secondidentityoutput) = 2 * ge_signed_half_unit_product_secondidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_secondidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_secondidentityoutputimaginary) = S ge_signed_half_unit_product_secondidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_secondidentity) * (ge_second_ip_unit_product_secondidentity))) + (((ge_first_rn_unit_product_secondidentity) * (ge_second_in_unit_product_secondidentity))))) + (((((ge_first_ip_unit_product_secondidentity) * (ge_second_rp_unit_product_secondidentity))) + (((ge_first_in_unit_product_secondidentity) * (ge_second_rn_unit_product_secondidentity))))))) + ge_balance_negative_unit_product_secondidentityoutputimaginary = (((((((ge_first_rp_unit_product_secondidentity) * (ge_second_in_unit_product_secondidentity))) + (((ge_first_rn_unit_product_secondidentity) * (ge_second_ip_unit_product_secondidentity))))) + (((((ge_first_ip_unit_product_secondidentity) * (ge_second_rn_unit_product_secondidentity))) + (((ge_first_in_unit_product_secondidentity) * (ge_second_rp_unit_product_secondidentity))))))) + ge_balance_positive_unit_product_secondidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_product_result. (exists ge_first_rp_unit_product_resultidentity ge_first_rn_unit_product_resultidentity ge_first_ip_unit_product_resultidentity ge_first_in_unit_product_resultidentity ge_second_rp_unit_product_resultidentity ge_second_rn_unit_product_resultidentity ge_second_ip_unit_product_resultidentity ge_second_in_unit_product_resultidentity. ((exists ge_representation_real_code_unit_product_resultidentityfirst ge_representation_imaginary_code_unit_product_resultidentityfirst. (((w) = ((ge_representation_real_code_unit_product_resultidentityfirst) + (ge_representation_imaginary_code_unit_product_resultidentityfirst)) * S ((ge_representation_real_code_unit_product_resultidentityfirst) + (ge_representation_imaginary_code_unit_product_resultidentityfirst)) + ((ge_representation_imaginary_code_unit_product_resultidentityfirst) + (ge_representation_imaginary_code_unit_product_resultidentityfirst))) /\ ((exists ge_balance_positive_unit_product_resultidentityfirstreal ge_balance_negative_unit_product_resultidentityfirstreal. (((((ge_representation_real_code_unit_product_resultidentityfirst) = 2 * (ge_balance_positive_unit_product_resultidentityfirstreal) /\ (ge_balance_negative_unit_product_resultidentityfirstreal) = 0) \/ exists ge_signed_half_unit_product_resultidentityfirstrealdecode. (((ge_representation_real_code_unit_product_resultidentityfirst) = 2 * ge_signed_half_unit_product_resultidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_product_resultidentityfirstreal) = 0) /\ (ge_balance_negative_unit_product_resultidentityfirstreal) = S ge_signed_half_unit_product_resultidentityfirstrealdecode))) /\ ((ge_first_rp_unit_product_resultidentity) + ge_balance_negative_unit_product_resultidentityfirstreal = (ge_first_rn_unit_product_resultidentity) + ge_balance_positive_unit_product_resultidentityfirstreal))) /\ (exists ge_balance_positive_unit_product_resultidentityfirstimaginary ge_balance_negative_unit_product_resultidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_product_resultidentityfirst) = 2 * (ge_balance_positive_unit_product_resultidentityfirstimaginary) /\ (ge_balance_negative_unit_product_resultidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_product_resultidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_product_resultidentityfirst) = 2 * ge_signed_half_unit_product_resultidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_product_resultidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_product_resultidentityfirstimaginary) = S ge_signed_half_unit_product_resultidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_product_resultidentity) + ge_balance_negative_unit_product_resultidentityfirstimaginary = (ge_first_in_unit_product_resultidentity) + ge_balance_positive_unit_product_resultidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_product_resultidentitysecond ge_representation_imaginary_code_unit_product_resultidentitysecond. (((gr_inverse_unit_product_result) = ((ge_representation_real_code_unit_product_resultidentitysecond) + (ge_representation_imaginary_code_unit_product_resultidentitysecond)) * S ((ge_representation_real_code_unit_product_resultidentitysecond) + (ge_representation_imaginary_code_unit_product_resultidentitysecond)) + ((ge_representation_imaginary_code_unit_product_resultidentitysecond) + (ge_representation_imaginary_code_unit_product_resultidentitysecond))) /\ ((exists ge_balance_positive_unit_product_resultidentitysecondreal ge_balance_negative_unit_product_resultidentitysecondreal. (((((ge_representation_real_code_unit_product_resultidentitysecond) = 2 * (ge_balance_positive_unit_product_resultidentitysecondreal) /\ (ge_balance_negative_unit_product_resultidentitysecondreal) = 0) \/ exists ge_signed_half_unit_product_resultidentitysecondrealdecode. (((ge_representation_real_code_unit_product_resultidentitysecond) = 2 * ge_signed_half_unit_product_resultidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_product_resultidentitysecondreal) = 0) /\ (ge_balance_negative_unit_product_resultidentitysecondreal) = S ge_signed_half_unit_product_resultidentitysecondrealdecode))) /\ ((ge_second_rp_unit_product_resultidentity) + ge_balance_negative_unit_product_resultidentitysecondreal = (ge_second_rn_unit_product_resultidentity) + ge_balance_positive_unit_product_resultidentitysecondreal))) /\ (exists ge_balance_positive_unit_product_resultidentitysecondimaginary ge_balance_negative_unit_product_resultidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_product_resultidentitysecond) = 2 * (ge_balance_positive_unit_product_resultidentitysecondimaginary) /\ (ge_balance_negative_unit_product_resultidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_product_resultidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_product_resultidentitysecond) = 2 * ge_signed_half_unit_product_resultidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_product_resultidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_product_resultidentitysecondimaginary) = S ge_signed_half_unit_product_resultidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_product_resultidentity) + ge_balance_negative_unit_product_resultidentitysecondimaginary = (ge_second_in_unit_product_resultidentity) + ge_balance_positive_unit_product_resultidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_product_resultidentityoutput ge_representation_imaginary_code_unit_product_resultidentityoutput. (((6) = ((ge_representation_real_code_unit_product_resultidentityoutput) + (ge_representation_imaginary_code_unit_product_resultidentityoutput)) * S ((ge_representation_real_code_unit_product_resultidentityoutput) + (ge_representation_imaginary_code_unit_product_resultidentityoutput)) + ((ge_representation_imaginary_code_unit_product_resultidentityoutput) + (ge_representation_imaginary_code_unit_product_resultidentityoutput))) /\ ((exists ge_balance_positive_unit_product_resultidentityoutputreal ge_balance_negative_unit_product_resultidentityoutputreal. (((((ge_representation_real_code_unit_product_resultidentityoutput) = 2 * (ge_balance_positive_unit_product_resultidentityoutputreal) /\ (ge_balance_negative_unit_product_resultidentityoutputreal) = 0) \/ exists ge_signed_half_unit_product_resultidentityoutputrealdecode. (((ge_representation_real_code_unit_product_resultidentityoutput) = 2 * ge_signed_half_unit_product_resultidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_product_resultidentityoutputreal) = 0) /\ (ge_balance_negative_unit_product_resultidentityoutputreal) = S ge_signed_half_unit_product_resultidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_product_resultidentity) * (ge_second_rp_unit_product_resultidentity))) + (((ge_first_rn_unit_product_resultidentity) * (ge_second_rn_unit_product_resultidentity))))) + (((((ge_first_ip_unit_product_resultidentity) * (ge_second_in_unit_product_resultidentity))) + (((ge_first_in_unit_product_resultidentity) * (ge_second_ip_unit_product_resultidentity))))))) + ge_balance_negative_unit_product_resultidentityoutputreal = (((((((ge_first_rp_unit_product_resultidentity) * (ge_second_rn_unit_product_resultidentity))) + (((ge_first_rn_unit_product_resultidentity) * (ge_second_rp_unit_product_resultidentity))))) + (((((ge_first_ip_unit_product_resultidentity) * (ge_second_ip_unit_product_resultidentity))) + (((ge_first_in_unit_product_resultidentity) * (ge_second_in_unit_product_resultidentity))))))) + ge_balance_positive_unit_product_resultidentityoutputreal))) /\ (exists ge_balance_positive_unit_product_resultidentityoutputimaginary ge_balance_negative_unit_product_resultidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_product_resultidentityoutput) = 2 * (ge_balance_positive_unit_product_resultidentityoutputimaginary) /\ (ge_balance_negative_unit_product_resultidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_product_resultidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_product_resultidentityoutput) = 2 * ge_signed_half_unit_product_resultidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_product_resultidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_product_resultidentityoutputimaginary) = S ge_signed_half_unit_product_resultidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_product_resultidentity) * (ge_second_ip_unit_product_resultidentity))) + (((ge_first_rn_unit_product_resultidentity) * (ge_second_in_unit_product_resultidentity))))) + (((((ge_first_ip_unit_product_resultidentity) * (ge_second_rp_unit_product_resultidentity))) + (((ge_first_in_unit_product_resultidentity) * (ge_second_rn_unit_product_resultidentity))))))) + ge_balance_negative_unit_product_resultidentityoutputimaginary = (((((((ge_first_rp_unit_product_resultidentity) * (ge_second_in_unit_product_resultidentity))) + (((ge_first_rn_unit_product_resultidentity) * (ge_second_ip_unit_product_resultidentity))))) + (((((ge_first_ip_unit_product_resultidentity) * (ge_second_rn_unit_product_resultidentity))) + (((ge_first_in_unit_product_resultidentity) * (ge_second_rp_unit_product_resultidentity))))))) + ge_balance_positive_unit_product_resultidentityoutputimaginary))))))))))Complete tactic proof in conservative notation
All 26 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
26 script commands · 5 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 (3)
01Fix variables and assumptionsL1–6
02Use earlier factsL7–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
03Calculate and transport equalitiesL13–13
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L13
norm_num
04Use earlier factsL14–23
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
specialize gaussian_norm_multiply (u) - L15
specialize gaussian_norm_multiply (v) - L16
specialize gaussian_norm_multiply (w) - L17
specialize gaussian_norm_multiply (1) - L18
specialize gaussian_norm_multiply (1) - L19
apply gaussian_norm_multiply - L20
specialize gaussian_unit_has_norm_one (u) - L21
apply gaussian_unit_has_norm_one - L22
exact hu - L23
specialize gaussian_unit_has_norm_one (v)
Original defined command ledger · 26 lines
- 0001
intro u - 0002
intro v - 0003
intro w - 0004
intro hprod - 0005
intro hu - 0006
intro hv - 0007
specialize gaussian_norm_one_is_unit (w) - 0008
apply gaussian_norm_one_is_unit - 0009
specialize gaussian_norm_value_transport (w) - 0010
specialize gaussian_norm_value_transport (1*1) - 0011
specialize gaussian_norm_value_transport (1) - 0012
apply gaussian_norm_value_transport - 0013
norm_num - 0014
specialize gaussian_norm_multiply (u) - 0015
specialize gaussian_norm_multiply (v) - 0016
specialize gaussian_norm_multiply (w) - 0017
specialize gaussian_norm_multiply (1) - 0018
specialize gaussian_norm_multiply (1) - 0019
apply gaussian_norm_multiply - 0020
specialize gaussian_unit_has_norm_one (u) - 0021
apply gaussian_unit_has_norm_one - 0022
exact hu - 0023
specialize gaussian_unit_has_norm_one (v) - 0024
apply gaussian_unit_has_norm_one - 0025
exact hv - 0026
exact hprod