GF0048

gaussian_divides_transitive

Compose actual Gaussian quotient witnesses using the proved canonical multiplication law.

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

∀ d. ∀ a. ∀ z. GDvd(d,a) → GDvd(a,z) → GDvd(d,z)

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

Definition DAG

GMul(a,b,c) · 1GDvd(d,z) · 3

Actual proof prerequisites

gaussian_multiply_exists · checked external prerequisitegaussian_multiply_input_right_validgaussian_multiply_associative
Original expanded first-order statement 
forall d a z. (exists gr_quotient_transitive_first. (exists ge_first_rp_transitive_firstproduct ge_first_rn_transitive_firstproduct ge_first_ip_transitive_firstproduct ge_first_in_transitive_firstproduct ge_second_rp_transitive_firstproduct ge_second_rn_transitive_firstproduct ge_second_ip_transitive_firstproduct ge_second_in_transitive_firstproduct. ((exists ge_representation_real_code_transitive_firstproductfirst ge_representation_imaginary_code_transitive_firstproductfirst. (((d) = ((ge_representation_real_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst)) * S ((ge_representation_real_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst)) + ((ge_representation_imaginary_code_transitive_firstproductfirst) + (ge_representation_imaginary_code_transitive_firstproductfirst))) /\ ((exists ge_balance_positive_transitive_firstproductfirstreal ge_balance_negative_transitive_firstproductfirstreal. (((((ge_representation_real_code_transitive_firstproductfirst) = 2 * (ge_balance_positive_transitive_firstproductfirstreal) /\ (ge_balance_negative_transitive_firstproductfirstreal) = 0) \/ exists ge_signed_half_transitive_firstproductfirstrealdecode. (((ge_representation_real_code_transitive_firstproductfirst) = 2 * ge_signed_half_transitive_firstproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductfirstreal) = 0) /\ (ge_balance_negative_transitive_firstproductfirstreal) = S ge_signed_half_transitive_firstproductfirstrealdecode))) /\ ((ge_first_rp_transitive_firstproduct) + ge_balance_negative_transitive_firstproductfirstreal = (ge_first_rn_transitive_firstproduct) + ge_balance_positive_transitive_firstproductfirstreal))) /\ (exists ge_balance_positive_transitive_firstproductfirstimaginary ge_balance_negative_transitive_firstproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_firstproductfirst) = 2 * (ge_balance_positive_transitive_firstproductfirstimaginary) /\ (ge_balance_negative_transitive_firstproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductfirst) = 2 * ge_signed_half_transitive_firstproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductfirstimaginary) = S ge_signed_half_transitive_firstproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_firstproduct) + ge_balance_negative_transitive_firstproductfirstimaginary = (ge_first_in_transitive_firstproduct) + ge_balance_positive_transitive_firstproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_firstproductsecond ge_representation_imaginary_code_transitive_firstproductsecond. (((gr_quotient_transitive_first) = ((ge_representation_real_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond)) * S ((ge_representation_real_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond)) + ((ge_representation_imaginary_code_transitive_firstproductsecond) + (ge_representation_imaginary_code_transitive_firstproductsecond))) /\ ((exists ge_balance_positive_transitive_firstproductsecondreal ge_balance_negative_transitive_firstproductsecondreal. (((((ge_representation_real_code_transitive_firstproductsecond) = 2 * (ge_balance_positive_transitive_firstproductsecondreal) /\ (ge_balance_negative_transitive_firstproductsecondreal) = 0) \/ exists ge_signed_half_transitive_firstproductsecondrealdecode. (((ge_representation_real_code_transitive_firstproductsecond) = 2 * ge_signed_half_transitive_firstproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductsecondreal) = 0) /\ (ge_balance_negative_transitive_firstproductsecondreal) = S ge_signed_half_transitive_firstproductsecondrealdecode))) /\ ((ge_second_rp_transitive_firstproduct) + ge_balance_negative_transitive_firstproductsecondreal = (ge_second_rn_transitive_firstproduct) + ge_balance_positive_transitive_firstproductsecondreal))) /\ (exists ge_balance_positive_transitive_firstproductsecondimaginary ge_balance_negative_transitive_firstproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_firstproductsecond) = 2 * (ge_balance_positive_transitive_firstproductsecondimaginary) /\ (ge_balance_negative_transitive_firstproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductsecond) = 2 * ge_signed_half_transitive_firstproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductsecondimaginary) = S ge_signed_half_transitive_firstproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_firstproduct) + ge_balance_negative_transitive_firstproductsecondimaginary = (ge_second_in_transitive_firstproduct) + ge_balance_positive_transitive_firstproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_firstproductoutput ge_representation_imaginary_code_transitive_firstproductoutput. (((a) = ((ge_representation_real_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput)) * S ((ge_representation_real_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput)) + ((ge_representation_imaginary_code_transitive_firstproductoutput) + (ge_representation_imaginary_code_transitive_firstproductoutput))) /\ ((exists ge_balance_positive_transitive_firstproductoutputreal ge_balance_negative_transitive_firstproductoutputreal. (((((ge_representation_real_code_transitive_firstproductoutput) = 2 * (ge_balance_positive_transitive_firstproductoutputreal) /\ (ge_balance_negative_transitive_firstproductoutputreal) = 0) \/ exists ge_signed_half_transitive_firstproductoutputrealdecode. (((ge_representation_real_code_transitive_firstproductoutput) = 2 * ge_signed_half_transitive_firstproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_firstproductoutputreal) = 0) /\ (ge_balance_negative_transitive_firstproductoutputreal) = S ge_signed_half_transitive_firstproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))))))) + ge_balance_negative_transitive_firstproductoutputreal = (((((((ge_first_rp_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))))))) + ge_balance_positive_transitive_firstproductoutputreal))) /\ (exists ge_balance_positive_transitive_firstproductoutputimaginary ge_balance_negative_transitive_firstproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_firstproductoutput) = 2 * (ge_balance_positive_transitive_firstproductoutputimaginary) /\ (ge_balance_negative_transitive_firstproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_firstproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_firstproductoutput) = 2 * ge_signed_half_transitive_firstproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_firstproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_firstproductoutputimaginary) = S ge_signed_half_transitive_firstproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))))))) + ge_balance_negative_transitive_firstproductoutputimaginary = (((((((ge_first_rp_transitive_firstproduct) * (ge_second_in_transitive_firstproduct))) + (((ge_first_rn_transitive_firstproduct) * (ge_second_ip_transitive_firstproduct))))) + (((((ge_first_ip_transitive_firstproduct) * (ge_second_rn_transitive_firstproduct))) + (((ge_first_in_transitive_firstproduct) * (ge_second_rp_transitive_firstproduct))))))) + ge_balance_positive_transitive_firstproductoutputimaginary)))))))))) -> (exists gr_quotient_transitive_second. (exists ge_first_rp_transitive_secondproduct ge_first_rn_transitive_secondproduct ge_first_ip_transitive_secondproduct ge_first_in_transitive_secondproduct ge_second_rp_transitive_secondproduct ge_second_rn_transitive_secondproduct ge_second_ip_transitive_secondproduct ge_second_in_transitive_secondproduct. ((exists ge_representation_real_code_transitive_secondproductfirst ge_representation_imaginary_code_transitive_secondproductfirst. (((a) = ((ge_representation_real_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst)) * S ((ge_representation_real_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst)) + ((ge_representation_imaginary_code_transitive_secondproductfirst) + (ge_representation_imaginary_code_transitive_secondproductfirst))) /\ ((exists ge_balance_positive_transitive_secondproductfirstreal ge_balance_negative_transitive_secondproductfirstreal. (((((ge_representation_real_code_transitive_secondproductfirst) = 2 * (ge_balance_positive_transitive_secondproductfirstreal) /\ (ge_balance_negative_transitive_secondproductfirstreal) = 0) \/ exists ge_signed_half_transitive_secondproductfirstrealdecode. (((ge_representation_real_code_transitive_secondproductfirst) = 2 * ge_signed_half_transitive_secondproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductfirstreal) = 0) /\ (ge_balance_negative_transitive_secondproductfirstreal) = S ge_signed_half_transitive_secondproductfirstrealdecode))) /\ ((ge_first_rp_transitive_secondproduct) + ge_balance_negative_transitive_secondproductfirstreal = (ge_first_rn_transitive_secondproduct) + ge_balance_positive_transitive_secondproductfirstreal))) /\ (exists ge_balance_positive_transitive_secondproductfirstimaginary ge_balance_negative_transitive_secondproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_secondproductfirst) = 2 * (ge_balance_positive_transitive_secondproductfirstimaginary) /\ (ge_balance_negative_transitive_secondproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductfirst) = 2 * ge_signed_half_transitive_secondproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductfirstimaginary) = S ge_signed_half_transitive_secondproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_secondproduct) + ge_balance_negative_transitive_secondproductfirstimaginary = (ge_first_in_transitive_secondproduct) + ge_balance_positive_transitive_secondproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_secondproductsecond ge_representation_imaginary_code_transitive_secondproductsecond. (((gr_quotient_transitive_second) = ((ge_representation_real_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond)) * S ((ge_representation_real_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond)) + ((ge_representation_imaginary_code_transitive_secondproductsecond) + (ge_representation_imaginary_code_transitive_secondproductsecond))) /\ ((exists ge_balance_positive_transitive_secondproductsecondreal ge_balance_negative_transitive_secondproductsecondreal. (((((ge_representation_real_code_transitive_secondproductsecond) = 2 * (ge_balance_positive_transitive_secondproductsecondreal) /\ (ge_balance_negative_transitive_secondproductsecondreal) = 0) \/ exists ge_signed_half_transitive_secondproductsecondrealdecode. (((ge_representation_real_code_transitive_secondproductsecond) = 2 * ge_signed_half_transitive_secondproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductsecondreal) = 0) /\ (ge_balance_negative_transitive_secondproductsecondreal) = S ge_signed_half_transitive_secondproductsecondrealdecode))) /\ ((ge_second_rp_transitive_secondproduct) + ge_balance_negative_transitive_secondproductsecondreal = (ge_second_rn_transitive_secondproduct) + ge_balance_positive_transitive_secondproductsecondreal))) /\ (exists ge_balance_positive_transitive_secondproductsecondimaginary ge_balance_negative_transitive_secondproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_secondproductsecond) = 2 * (ge_balance_positive_transitive_secondproductsecondimaginary) /\ (ge_balance_negative_transitive_secondproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductsecond) = 2 * ge_signed_half_transitive_secondproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductsecondimaginary) = S ge_signed_half_transitive_secondproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_secondproduct) + ge_balance_negative_transitive_secondproductsecondimaginary = (ge_second_in_transitive_secondproduct) + ge_balance_positive_transitive_secondproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_secondproductoutput ge_representation_imaginary_code_transitive_secondproductoutput. (((z) = ((ge_representation_real_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput)) * S ((ge_representation_real_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput)) + ((ge_representation_imaginary_code_transitive_secondproductoutput) + (ge_representation_imaginary_code_transitive_secondproductoutput))) /\ ((exists ge_balance_positive_transitive_secondproductoutputreal ge_balance_negative_transitive_secondproductoutputreal. (((((ge_representation_real_code_transitive_secondproductoutput) = 2 * (ge_balance_positive_transitive_secondproductoutputreal) /\ (ge_balance_negative_transitive_secondproductoutputreal) = 0) \/ exists ge_signed_half_transitive_secondproductoutputrealdecode. (((ge_representation_real_code_transitive_secondproductoutput) = 2 * ge_signed_half_transitive_secondproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_secondproductoutputreal) = 0) /\ (ge_balance_negative_transitive_secondproductoutputreal) = S ge_signed_half_transitive_secondproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))))))) + ge_balance_negative_transitive_secondproductoutputreal = (((((((ge_first_rp_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))))))) + ge_balance_positive_transitive_secondproductoutputreal))) /\ (exists ge_balance_positive_transitive_secondproductoutputimaginary ge_balance_negative_transitive_secondproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_secondproductoutput) = 2 * (ge_balance_positive_transitive_secondproductoutputimaginary) /\ (ge_balance_negative_transitive_secondproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_secondproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_secondproductoutput) = 2 * ge_signed_half_transitive_secondproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_secondproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_secondproductoutputimaginary) = S ge_signed_half_transitive_secondproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))))))) + ge_balance_negative_transitive_secondproductoutputimaginary = (((((((ge_first_rp_transitive_secondproduct) * (ge_second_in_transitive_secondproduct))) + (((ge_first_rn_transitive_secondproduct) * (ge_second_ip_transitive_secondproduct))))) + (((((ge_first_ip_transitive_secondproduct) * (ge_second_rn_transitive_secondproduct))) + (((ge_first_in_transitive_secondproduct) * (ge_second_rp_transitive_secondproduct))))))) + ge_balance_positive_transitive_secondproductoutputimaginary)))))))))) -> (exists gr_quotient_transitive_result. (exists ge_first_rp_transitive_resultproduct ge_first_rn_transitive_resultproduct ge_first_ip_transitive_resultproduct ge_first_in_transitive_resultproduct ge_second_rp_transitive_resultproduct ge_second_rn_transitive_resultproduct ge_second_ip_transitive_resultproduct ge_second_in_transitive_resultproduct. ((exists ge_representation_real_code_transitive_resultproductfirst ge_representation_imaginary_code_transitive_resultproductfirst. (((d) = ((ge_representation_real_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst)) * S ((ge_representation_real_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst)) + ((ge_representation_imaginary_code_transitive_resultproductfirst) + (ge_representation_imaginary_code_transitive_resultproductfirst))) /\ ((exists ge_balance_positive_transitive_resultproductfirstreal ge_balance_negative_transitive_resultproductfirstreal. (((((ge_representation_real_code_transitive_resultproductfirst) = 2 * (ge_balance_positive_transitive_resultproductfirstreal) /\ (ge_balance_negative_transitive_resultproductfirstreal) = 0) \/ exists ge_signed_half_transitive_resultproductfirstrealdecode. (((ge_representation_real_code_transitive_resultproductfirst) = 2 * ge_signed_half_transitive_resultproductfirstrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductfirstreal) = 0) /\ (ge_balance_negative_transitive_resultproductfirstreal) = S ge_signed_half_transitive_resultproductfirstrealdecode))) /\ ((ge_first_rp_transitive_resultproduct) + ge_balance_negative_transitive_resultproductfirstreal = (ge_first_rn_transitive_resultproduct) + ge_balance_positive_transitive_resultproductfirstreal))) /\ (exists ge_balance_positive_transitive_resultproductfirstimaginary ge_balance_negative_transitive_resultproductfirstimaginary. (((((ge_representation_imaginary_code_transitive_resultproductfirst) = 2 * (ge_balance_positive_transitive_resultproductfirstimaginary) /\ (ge_balance_negative_transitive_resultproductfirstimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductfirstimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductfirst) = 2 * ge_signed_half_transitive_resultproductfirstimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductfirstimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductfirstimaginary) = S ge_signed_half_transitive_resultproductfirstimaginarydecode))) /\ ((ge_first_ip_transitive_resultproduct) + ge_balance_negative_transitive_resultproductfirstimaginary = (ge_first_in_transitive_resultproduct) + ge_balance_positive_transitive_resultproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_transitive_resultproductsecond ge_representation_imaginary_code_transitive_resultproductsecond. (((gr_quotient_transitive_result) = ((ge_representation_real_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond)) * S ((ge_representation_real_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond)) + ((ge_representation_imaginary_code_transitive_resultproductsecond) + (ge_representation_imaginary_code_transitive_resultproductsecond))) /\ ((exists ge_balance_positive_transitive_resultproductsecondreal ge_balance_negative_transitive_resultproductsecondreal. (((((ge_representation_real_code_transitive_resultproductsecond) = 2 * (ge_balance_positive_transitive_resultproductsecondreal) /\ (ge_balance_negative_transitive_resultproductsecondreal) = 0) \/ exists ge_signed_half_transitive_resultproductsecondrealdecode. (((ge_representation_real_code_transitive_resultproductsecond) = 2 * ge_signed_half_transitive_resultproductsecondrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductsecondreal) = 0) /\ (ge_balance_negative_transitive_resultproductsecondreal) = S ge_signed_half_transitive_resultproductsecondrealdecode))) /\ ((ge_second_rp_transitive_resultproduct) + ge_balance_negative_transitive_resultproductsecondreal = (ge_second_rn_transitive_resultproduct) + ge_balance_positive_transitive_resultproductsecondreal))) /\ (exists ge_balance_positive_transitive_resultproductsecondimaginary ge_balance_negative_transitive_resultproductsecondimaginary. (((((ge_representation_imaginary_code_transitive_resultproductsecond) = 2 * (ge_balance_positive_transitive_resultproductsecondimaginary) /\ (ge_balance_negative_transitive_resultproductsecondimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductsecondimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductsecond) = 2 * ge_signed_half_transitive_resultproductsecondimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductsecondimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductsecondimaginary) = S ge_signed_half_transitive_resultproductsecondimaginarydecode))) /\ ((ge_second_ip_transitive_resultproduct) + ge_balance_negative_transitive_resultproductsecondimaginary = (ge_second_in_transitive_resultproduct) + ge_balance_positive_transitive_resultproductsecondimaginary)))))) /\ (exists ge_representation_real_code_transitive_resultproductoutput ge_representation_imaginary_code_transitive_resultproductoutput. (((z) = ((ge_representation_real_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput)) * S ((ge_representation_real_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput)) + ((ge_representation_imaginary_code_transitive_resultproductoutput) + (ge_representation_imaginary_code_transitive_resultproductoutput))) /\ ((exists ge_balance_positive_transitive_resultproductoutputreal ge_balance_negative_transitive_resultproductoutputreal. (((((ge_representation_real_code_transitive_resultproductoutput) = 2 * (ge_balance_positive_transitive_resultproductoutputreal) /\ (ge_balance_negative_transitive_resultproductoutputreal) = 0) \/ exists ge_signed_half_transitive_resultproductoutputrealdecode. (((ge_representation_real_code_transitive_resultproductoutput) = 2 * ge_signed_half_transitive_resultproductoutputrealdecode + 1 /\ (ge_balance_positive_transitive_resultproductoutputreal) = 0) /\ (ge_balance_negative_transitive_resultproductoutputreal) = S ge_signed_half_transitive_resultproductoutputrealdecode))) /\ ((((((((ge_first_rp_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))))))) + ge_balance_negative_transitive_resultproductoutputreal = (((((((ge_first_rp_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))))))) + ge_balance_positive_transitive_resultproductoutputreal))) /\ (exists ge_balance_positive_transitive_resultproductoutputimaginary ge_balance_negative_transitive_resultproductoutputimaginary. (((((ge_representation_imaginary_code_transitive_resultproductoutput) = 2 * (ge_balance_positive_transitive_resultproductoutputimaginary) /\ (ge_balance_negative_transitive_resultproductoutputimaginary) = 0) \/ exists ge_signed_half_transitive_resultproductoutputimaginarydecode. (((ge_representation_imaginary_code_transitive_resultproductoutput) = 2 * ge_signed_half_transitive_resultproductoutputimaginarydecode + 1 /\ (ge_balance_positive_transitive_resultproductoutputimaginary) = 0) /\ (ge_balance_negative_transitive_resultproductoutputimaginary) = S ge_signed_half_transitive_resultproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))))))) + ge_balance_negative_transitive_resultproductoutputimaginary = (((((((ge_first_rp_transitive_resultproduct) * (ge_second_in_transitive_resultproduct))) + (((ge_first_rn_transitive_resultproduct) * (ge_second_ip_transitive_resultproduct))))) + (((((ge_first_ip_transitive_resultproduct) * (ge_second_rn_transitive_resultproduct))) + (((ge_first_in_transitive_resultproduct) * (ge_second_rp_transitive_resultproduct))))))) + ge_balance_positive_transitive_resultproductoutputimaginary))))))))))

Complete tactic proof in conservative notation

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

33 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 d
  2. L2
    intro a
  3. L3
    intro z
  4. L4
    intro hA
  5. L5
    intro hZ
02Separate the logical casesL6–7

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

  1. L6
    cases hA
  2. L7
    cases hZ
03Establish hqL8–17

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

  1. L8
    have hq : ∃ q. GMul(x,x1,q)Definitions: GMul(x,x1,q)Original native command in the exact edition
  2. L9
    specialize gaussian_multiply_exists (x)
  3. L10
    specialize gaussian_multiply_exists (x1)
  4. L11
    apply gaussian_multiply_exists
  5. L12
    specialize gaussian_multiply_input_right_valid (d)
  6. L13
    specialize gaussian_multiply_input_right_valid (x)
  7. L14
    specialize gaussian_multiply_input_right_valid (a)
  8. L15
    apply gaussian_multiply_input_right_valid
  9. L16
    exact hA_witness
  10. L17
    specialize gaussian_multiply_input_right_valid (a)
04Use earlier factsL18–21

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

  1. L18
    specialize gaussian_multiply_input_right_valid (x1)
  2. L19
    specialize gaussian_multiply_input_right_valid (z)
  3. L20
    apply gaussian_multiply_input_right_valid
  4. L21
    exact hZ_witness
05Separate the logical casesL22–22

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

  1. L22
    cases hq
06Construct an explicit witnessL23–23

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

  1. L23
    exists (x2)
07Use earlier factsL24–33

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

  1. L24
    specialize gaussian_multiply_associative (d)
  2. L25
    specialize gaussian_multiply_associative (x)
  3. L26
    specialize gaussian_multiply_associative (x1)
  4. L27
    specialize gaussian_multiply_associative (a)
  5. L28
    specialize gaussian_multiply_associative (x2)
  6. L29
    specialize gaussian_multiply_associative (z)
  7. L30
    apply gaussian_multiply_associative
  8. L31
    exact hA_witness
  9. L32
    exact hZ_witness
  10. L33
    exact hq_witness

Library-wide reading audit

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