GF0040

gaussian_unit_factor_left

Every actual left factor of a Gaussian unit has a constructed inverse, without an irreducibility assumption.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

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. ∀ c. GMul(a,b,c) → GUnit(c) → GUnit(a)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

GMul(a,b,c) · 2GUnit(z) · 2

Actual proof prerequisites

gaussian_multiply_exists · checked external prerequisitegaussian_multiply_input_right_validgaussian_multiply_associative
Original expanded first-order statement 
forall a b c. (exists ge_first_rp_unit_factor_product ge_first_rn_unit_factor_product ge_first_ip_unit_factor_product ge_first_in_unit_factor_product ge_second_rp_unit_factor_product ge_second_rn_unit_factor_product ge_second_ip_unit_factor_product ge_second_in_unit_factor_product. ((exists ge_representation_real_code_unit_factor_productfirst ge_representation_imaginary_code_unit_factor_productfirst. (((a) = ((ge_representation_real_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst)) * S ((ge_representation_real_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst)) + ((ge_representation_imaginary_code_unit_factor_productfirst) + (ge_representation_imaginary_code_unit_factor_productfirst))) /\ ((exists ge_balance_positive_unit_factor_productfirstreal ge_balance_negative_unit_factor_productfirstreal. (((((ge_representation_real_code_unit_factor_productfirst) = 2 * (ge_balance_positive_unit_factor_productfirstreal) /\ (ge_balance_negative_unit_factor_productfirstreal) = 0) \/ exists ge_signed_half_unit_factor_productfirstrealdecode. (((ge_representation_real_code_unit_factor_productfirst) = 2 * ge_signed_half_unit_factor_productfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_productfirstreal) = 0) /\ (ge_balance_negative_unit_factor_productfirstreal) = S ge_signed_half_unit_factor_productfirstrealdecode))) /\ ((ge_first_rp_unit_factor_product) + ge_balance_negative_unit_factor_productfirstreal = (ge_first_rn_unit_factor_product) + ge_balance_positive_unit_factor_productfirstreal))) /\ (exists ge_balance_positive_unit_factor_productfirstimaginary ge_balance_negative_unit_factor_productfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_productfirst) = 2 * (ge_balance_positive_unit_factor_productfirstimaginary) /\ (ge_balance_negative_unit_factor_productfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_productfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productfirst) = 2 * ge_signed_half_unit_factor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_productfirstimaginary) = S ge_signed_half_unit_factor_productfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_product) + ge_balance_negative_unit_factor_productfirstimaginary = (ge_first_in_unit_factor_product) + ge_balance_positive_unit_factor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_productsecond ge_representation_imaginary_code_unit_factor_productsecond. (((b) = ((ge_representation_real_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond)) * S ((ge_representation_real_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond)) + ((ge_representation_imaginary_code_unit_factor_productsecond) + (ge_representation_imaginary_code_unit_factor_productsecond))) /\ ((exists ge_balance_positive_unit_factor_productsecondreal ge_balance_negative_unit_factor_productsecondreal. (((((ge_representation_real_code_unit_factor_productsecond) = 2 * (ge_balance_positive_unit_factor_productsecondreal) /\ (ge_balance_negative_unit_factor_productsecondreal) = 0) \/ exists ge_signed_half_unit_factor_productsecondrealdecode. (((ge_representation_real_code_unit_factor_productsecond) = 2 * ge_signed_half_unit_factor_productsecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_productsecondreal) = 0) /\ (ge_balance_negative_unit_factor_productsecondreal) = S ge_signed_half_unit_factor_productsecondrealdecode))) /\ ((ge_second_rp_unit_factor_product) + ge_balance_negative_unit_factor_productsecondreal = (ge_second_rn_unit_factor_product) + ge_balance_positive_unit_factor_productsecondreal))) /\ (exists ge_balance_positive_unit_factor_productsecondimaginary ge_balance_negative_unit_factor_productsecondimaginary. (((((ge_representation_imaginary_code_unit_factor_productsecond) = 2 * (ge_balance_positive_unit_factor_productsecondimaginary) /\ (ge_balance_negative_unit_factor_productsecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_productsecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productsecond) = 2 * ge_signed_half_unit_factor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productsecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_productsecondimaginary) = S ge_signed_half_unit_factor_productsecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_product) + ge_balance_negative_unit_factor_productsecondimaginary = (ge_second_in_unit_factor_product) + ge_balance_positive_unit_factor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_productoutput ge_representation_imaginary_code_unit_factor_productoutput. (((c) = ((ge_representation_real_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput)) * S ((ge_representation_real_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput)) + ((ge_representation_imaginary_code_unit_factor_productoutput) + (ge_representation_imaginary_code_unit_factor_productoutput))) /\ ((exists ge_balance_positive_unit_factor_productoutputreal ge_balance_negative_unit_factor_productoutputreal. (((((ge_representation_real_code_unit_factor_productoutput) = 2 * (ge_balance_positive_unit_factor_productoutputreal) /\ (ge_balance_negative_unit_factor_productoutputreal) = 0) \/ exists ge_signed_half_unit_factor_productoutputrealdecode. (((ge_representation_real_code_unit_factor_productoutput) = 2 * ge_signed_half_unit_factor_productoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_productoutputreal) = 0) /\ (ge_balance_negative_unit_factor_productoutputreal) = S ge_signed_half_unit_factor_productoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_product) * (ge_second_rp_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_rn_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_in_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_ip_unit_factor_product))))))) + ge_balance_negative_unit_factor_productoutputreal = (((((((ge_first_rp_unit_factor_product) * (ge_second_rn_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_rp_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_ip_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_in_unit_factor_product))))))) + ge_balance_positive_unit_factor_productoutputreal))) /\ (exists ge_balance_positive_unit_factor_productoutputimaginary ge_balance_negative_unit_factor_productoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_productoutput) = 2 * (ge_balance_positive_unit_factor_productoutputimaginary) /\ (ge_balance_negative_unit_factor_productoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_productoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_productoutput) = 2 * ge_signed_half_unit_factor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_productoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_productoutputimaginary) = S ge_signed_half_unit_factor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_product) * (ge_second_ip_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_in_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_rp_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_rn_unit_factor_product))))))) + ge_balance_negative_unit_factor_productoutputimaginary = (((((((ge_first_rp_unit_factor_product) * (ge_second_in_unit_factor_product))) + (((ge_first_rn_unit_factor_product) * (ge_second_ip_unit_factor_product))))) + (((((ge_first_ip_unit_factor_product) * (ge_second_rn_unit_factor_product))) + (((ge_first_in_unit_factor_product) * (ge_second_rp_unit_factor_product))))))) + ge_balance_positive_unit_factor_productoutputimaginary))))))))) -> (exists gr_inverse_unit_factor_whole. (exists ge_first_rp_unit_factor_wholeidentity ge_first_rn_unit_factor_wholeidentity ge_first_ip_unit_factor_wholeidentity ge_first_in_unit_factor_wholeidentity ge_second_rp_unit_factor_wholeidentity ge_second_rn_unit_factor_wholeidentity ge_second_ip_unit_factor_wholeidentity ge_second_in_unit_factor_wholeidentity. ((exists ge_representation_real_code_unit_factor_wholeidentityfirst ge_representation_imaginary_code_unit_factor_wholeidentityfirst. (((c) = ((ge_representation_real_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst)) * S ((ge_representation_real_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) + (ge_representation_imaginary_code_unit_factor_wholeidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_wholeidentityfirstreal ge_balance_negative_unit_factor_wholeidentityfirstreal. (((((ge_representation_real_code_unit_factor_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_wholeidentityfirstreal) /\ (ge_balance_negative_unit_factor_wholeidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_wholeidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityfirstreal) = S ge_signed_half_unit_factor_wholeidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentityfirstreal = (ge_first_rn_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentityfirstimaginary ge_balance_negative_unit_factor_wholeidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) = 2 * (ge_balance_positive_unit_factor_wholeidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_wholeidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentityfirst) = 2 * ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityfirstimaginary) = S ge_signed_half_unit_factor_wholeidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentityfirstimaginary = (ge_first_in_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_wholeidentitysecond ge_representation_imaginary_code_unit_factor_wholeidentitysecond. (((gr_inverse_unit_factor_whole) = ((ge_representation_real_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond)) * S ((ge_representation_real_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) + (ge_representation_imaginary_code_unit_factor_wholeidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_wholeidentitysecondreal ge_balance_negative_unit_factor_wholeidentitysecondreal. (((((ge_representation_real_code_unit_factor_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_wholeidentitysecondreal) /\ (ge_balance_negative_unit_factor_wholeidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_wholeidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentitysecondreal) = S ge_signed_half_unit_factor_wholeidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentitysecondreal = (ge_second_rn_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentitysecondimaginary ge_balance_negative_unit_factor_wholeidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) = 2 * (ge_balance_positive_unit_factor_wholeidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_wholeidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentitysecond) = 2 * ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentitysecondimaginary) = S ge_signed_half_unit_factor_wholeidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_wholeidentity) + ge_balance_negative_unit_factor_wholeidentitysecondimaginary = (ge_second_in_unit_factor_wholeidentity) + ge_balance_positive_unit_factor_wholeidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_wholeidentityoutput ge_representation_imaginary_code_unit_factor_wholeidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput)) * S ((ge_representation_real_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) + (ge_representation_imaginary_code_unit_factor_wholeidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_wholeidentityoutputreal ge_balance_negative_unit_factor_wholeidentityoutputreal. (((((ge_representation_real_code_unit_factor_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_wholeidentityoutputreal) /\ (ge_balance_negative_unit_factor_wholeidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_wholeidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityoutputreal) = S ge_signed_half_unit_factor_wholeidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))))))) + ge_balance_negative_unit_factor_wholeidentityoutputreal = (((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))))))) + ge_balance_positive_unit_factor_wholeidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_wholeidentityoutputimaginary ge_balance_negative_unit_factor_wholeidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) = 2 * (ge_balance_positive_unit_factor_wholeidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_wholeidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_wholeidentityoutput) = 2 * ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_wholeidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_wholeidentityoutputimaginary) = S ge_signed_half_unit_factor_wholeidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))))))) + ge_balance_negative_unit_factor_wholeidentityoutputimaginary = (((((((ge_first_rp_unit_factor_wholeidentity) * (ge_second_in_unit_factor_wholeidentity))) + (((ge_first_rn_unit_factor_wholeidentity) * (ge_second_ip_unit_factor_wholeidentity))))) + (((((ge_first_ip_unit_factor_wholeidentity) * (ge_second_rn_unit_factor_wholeidentity))) + (((ge_first_in_unit_factor_wholeidentity) * (ge_second_rp_unit_factor_wholeidentity))))))) + ge_balance_positive_unit_factor_wholeidentityoutputimaginary)))))))))) -> (exists gr_inverse_unit_factor_first. (exists ge_first_rp_unit_factor_firstidentity ge_first_rn_unit_factor_firstidentity ge_first_ip_unit_factor_firstidentity ge_first_in_unit_factor_firstidentity ge_second_rp_unit_factor_firstidentity ge_second_rn_unit_factor_firstidentity ge_second_ip_unit_factor_firstidentity ge_second_in_unit_factor_firstidentity. ((exists ge_representation_real_code_unit_factor_firstidentityfirst ge_representation_imaginary_code_unit_factor_firstidentityfirst. (((a) = ((ge_representation_real_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst)) * S ((ge_representation_real_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst)) + ((ge_representation_imaginary_code_unit_factor_firstidentityfirst) + (ge_representation_imaginary_code_unit_factor_firstidentityfirst))) /\ ((exists ge_balance_positive_unit_factor_firstidentityfirstreal ge_balance_negative_unit_factor_firstidentityfirstreal. (((((ge_representation_real_code_unit_factor_firstidentityfirst) = 2 * (ge_balance_positive_unit_factor_firstidentityfirstreal) /\ (ge_balance_negative_unit_factor_firstidentityfirstreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentityfirstrealdecode. (((ge_representation_real_code_unit_factor_firstidentityfirst) = 2 * ge_signed_half_unit_factor_firstidentityfirstrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityfirstreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentityfirstreal) = S ge_signed_half_unit_factor_firstidentityfirstrealdecode))) /\ ((ge_first_rp_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentityfirstreal = (ge_first_rn_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentityfirstreal))) /\ (exists ge_balance_positive_unit_factor_firstidentityfirstimaginary ge_balance_negative_unit_factor_firstidentityfirstimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentityfirst) = 2 * (ge_balance_positive_unit_factor_firstidentityfirstimaginary) /\ (ge_balance_negative_unit_factor_firstidentityfirstimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentityfirstimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentityfirst) = 2 * ge_signed_half_unit_factor_firstidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityfirstimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentityfirstimaginary) = S ge_signed_half_unit_factor_firstidentityfirstimaginarydecode))) /\ ((ge_first_ip_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentityfirstimaginary = (ge_first_in_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_unit_factor_firstidentitysecond ge_representation_imaginary_code_unit_factor_firstidentitysecond. (((gr_inverse_unit_factor_first) = ((ge_representation_real_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond)) * S ((ge_representation_real_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond)) + ((ge_representation_imaginary_code_unit_factor_firstidentitysecond) + (ge_representation_imaginary_code_unit_factor_firstidentitysecond))) /\ ((exists ge_balance_positive_unit_factor_firstidentitysecondreal ge_balance_negative_unit_factor_firstidentitysecondreal. (((((ge_representation_real_code_unit_factor_firstidentitysecond) = 2 * (ge_balance_positive_unit_factor_firstidentitysecondreal) /\ (ge_balance_negative_unit_factor_firstidentitysecondreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentitysecondrealdecode. (((ge_representation_real_code_unit_factor_firstidentitysecond) = 2 * ge_signed_half_unit_factor_firstidentitysecondrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentitysecondreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentitysecondreal) = S ge_signed_half_unit_factor_firstidentitysecondrealdecode))) /\ ((ge_second_rp_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentitysecondreal = (ge_second_rn_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentitysecondreal))) /\ (exists ge_balance_positive_unit_factor_firstidentitysecondimaginary ge_balance_negative_unit_factor_firstidentitysecondimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentitysecond) = 2 * (ge_balance_positive_unit_factor_firstidentitysecondimaginary) /\ (ge_balance_negative_unit_factor_firstidentitysecondimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentitysecondimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentitysecond) = 2 * ge_signed_half_unit_factor_firstidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentitysecondimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentitysecondimaginary) = S ge_signed_half_unit_factor_firstidentitysecondimaginarydecode))) /\ ((ge_second_ip_unit_factor_firstidentity) + ge_balance_negative_unit_factor_firstidentitysecondimaginary = (ge_second_in_unit_factor_firstidentity) + ge_balance_positive_unit_factor_firstidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_unit_factor_firstidentityoutput ge_representation_imaginary_code_unit_factor_firstidentityoutput. (((6) = ((ge_representation_real_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput)) * S ((ge_representation_real_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput)) + ((ge_representation_imaginary_code_unit_factor_firstidentityoutput) + (ge_representation_imaginary_code_unit_factor_firstidentityoutput))) /\ ((exists ge_balance_positive_unit_factor_firstidentityoutputreal ge_balance_negative_unit_factor_firstidentityoutputreal. (((((ge_representation_real_code_unit_factor_firstidentityoutput) = 2 * (ge_balance_positive_unit_factor_firstidentityoutputreal) /\ (ge_balance_negative_unit_factor_firstidentityoutputreal) = 0) \/ exists ge_signed_half_unit_factor_firstidentityoutputrealdecode. (((ge_representation_real_code_unit_factor_firstidentityoutput) = 2 * ge_signed_half_unit_factor_firstidentityoutputrealdecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityoutputreal) = 0) /\ (ge_balance_negative_unit_factor_firstidentityoutputreal) = S ge_signed_half_unit_factor_firstidentityoutputrealdecode))) /\ ((((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))))))) + ge_balance_negative_unit_factor_firstidentityoutputreal = (((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))))))) + ge_balance_positive_unit_factor_firstidentityoutputreal))) /\ (exists ge_balance_positive_unit_factor_firstidentityoutputimaginary ge_balance_negative_unit_factor_firstidentityoutputimaginary. (((((ge_representation_imaginary_code_unit_factor_firstidentityoutput) = 2 * (ge_balance_positive_unit_factor_firstidentityoutputimaginary) /\ (ge_balance_negative_unit_factor_firstidentityoutputimaginary) = 0) \/ exists ge_signed_half_unit_factor_firstidentityoutputimaginarydecode. (((ge_representation_imaginary_code_unit_factor_firstidentityoutput) = 2 * ge_signed_half_unit_factor_firstidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_unit_factor_firstidentityoutputimaginary) = 0) /\ (ge_balance_negative_unit_factor_firstidentityoutputimaginary) = S ge_signed_half_unit_factor_firstidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))))))) + ge_balance_negative_unit_factor_firstidentityoutputimaginary = (((((((ge_first_rp_unit_factor_firstidentity) * (ge_second_in_unit_factor_firstidentity))) + (((ge_first_rn_unit_factor_firstidentity) * (ge_second_ip_unit_factor_firstidentity))))) + (((((ge_first_ip_unit_factor_firstidentity) * (ge_second_rn_unit_factor_firstidentity))) + (((ge_first_in_unit_factor_firstidentity) * (ge_second_rp_unit_factor_firstidentity))))))) + ge_balance_positive_unit_factor_firstidentityoutputimaginary))))))))))

Complete tactic proof in conservative notation

All 32 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

32 script commands · 7 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
gaussian multiply input right validgaussian multiply associative
01Fix variables and assumptionsL1–5

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro hprod
  5. L5
    intro hu
02Separate the logical casesL6–6

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases hu
03Establish hinverseL7–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian multiply exists.

  1. L7
    have hinverse : ∃ v. GMul(b,x,v)Definitions: GMul(b,x,v)Original native command in the exact edition
  2. L8
    specialize gaussian_multiply_exists (b)
  3. L9
    specialize gaussian_multiply_exists (x)
  4. L10
    apply gaussian_multiply_exists
  5. L11
    specialize gaussian_multiply_input_right_valid (a)
  6. L12
    specialize gaussian_multiply_input_right_valid (b)
  7. L13
    specialize gaussian_multiply_input_right_valid (c)
  8. L14
    apply gaussian_multiply_input_right_valid
  9. L15
    exact hprod
  10. L16
    specialize gaussian_multiply_input_right_valid (c)
04Use earlier factsL17–20

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L17
    specialize gaussian_multiply_input_right_valid (x)
  2. L18
    specialize gaussian_multiply_input_right_valid (6)
  3. L19
    apply gaussian_multiply_input_right_valid
  4. L20
    exact hu_witness
05Separate the logical casesL21–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L21
    cases hinverse
06Construct an explicit witnessL22–22

Supply the displayed value, then prove that it has the required property.

  1. L22
    exists (x1)
07Use earlier factsL23–32

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize gaussian_multiply_associative (a)
  2. L24
    specialize gaussian_multiply_associative (b)
  3. L25
    specialize gaussian_multiply_associative (x)
  4. L26
    specialize gaussian_multiply_associative (c)
  5. L27
    specialize gaussian_multiply_associative (x1)
  6. L28
    specialize gaussian_multiply_associative (6)
  7. L29
    apply gaussian_multiply_associative
  8. L30
    exact hprod
  9. L31
    exact hu_witness
  10. L32
    exact hinverse_witness

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro hprod
  5. 0005intro hu
  6. 0006cases hu
  7. 0007have hinverse : ∃ v. GMul(b,x,v)
  8. 0008specialize gaussian_multiply_exists (b)
  9. 0009specialize gaussian_multiply_exists (x)
  10. 0010apply gaussian_multiply_exists
  11. 0011specialize gaussian_multiply_input_right_valid (a)
  12. 0012specialize gaussian_multiply_input_right_valid (b)
  13. 0013specialize gaussian_multiply_input_right_valid (c)
  14. 0014apply gaussian_multiply_input_right_valid
  15. 0015exact hprod
  16. 0016specialize gaussian_multiply_input_right_valid (c)
  17. 0017specialize gaussian_multiply_input_right_valid (x)
  18. 0018specialize gaussian_multiply_input_right_valid (6)
  19. 0019apply gaussian_multiply_input_right_valid
  20. 0020exact hu_witness
  21. 0021cases hinverse
  22. 0022exists (x1)
  23. 0023specialize gaussian_multiply_associative (a)
  24. 0024specialize gaussian_multiply_associative (b)
  25. 0025specialize gaussian_multiply_associative (x)
  26. 0026specialize gaussian_multiply_associative (c)
  27. 0027specialize gaussian_multiply_associative (x1)
  28. 0028specialize gaussian_multiply_associative (6)
  29. 0029apply gaussian_multiply_associative
  30. 0030exact hprod
  31. 0031exact hu_witness
  32. 0032exact hinverse_witness