GF0051

gaussian_division_zero_remainder_divides

An actual Gaussian zero remainder gives an actual quotient witnessing divisibility.

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. ∀ q. ∀ r. (∃ x. GMul(b,q,x) ∧ ZPairAdd(x,r,a)) → r = 0 → GDvd(b,a)

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

Definition DAG

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

Actual proof prerequisites

gaussian_add_functional · checked external prerequisitegaussian_add_zero_rightgaussian_multiply_output_validgaussian_multiply_output_transport
Original expanded first-order statement 
forall a b q r. (exists ge_division_product_zero_remainder_equation. ((exists ge_first_rp_zero_remainder_equationproduct ge_first_rn_zero_remainder_equationproduct ge_first_ip_zero_remainder_equationproduct ge_first_in_zero_remainder_equationproduct ge_second_rp_zero_remainder_equationproduct ge_second_rn_zero_remainder_equationproduct ge_second_ip_zero_remainder_equationproduct ge_second_in_zero_remainder_equationproduct. ((exists ge_representation_real_code_zero_remainder_equationproductfirst ge_representation_imaginary_code_zero_remainder_equationproductfirst. (((b) = ((ge_representation_real_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst)) * S ((ge_representation_real_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst)) + ((ge_representation_imaginary_code_zero_remainder_equationproductfirst) + (ge_representation_imaginary_code_zero_remainder_equationproductfirst))) /\ ((exists ge_balance_positive_zero_remainder_equationproductfirstreal ge_balance_negative_zero_remainder_equationproductfirstreal. (((((ge_representation_real_code_zero_remainder_equationproductfirst) = 2 * (ge_balance_positive_zero_remainder_equationproductfirstreal) /\ (ge_balance_negative_zero_remainder_equationproductfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductfirstrealdecode. (((ge_representation_real_code_zero_remainder_equationproductfirst) = 2 * ge_signed_half_zero_remainder_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductfirstreal) = S ge_signed_half_zero_remainder_equationproductfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductfirstreal = (ge_first_rn_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductfirstreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductfirstimaginary ge_balance_negative_zero_remainder_equationproductfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductfirst) = 2 * (ge_balance_positive_zero_remainder_equationproductfirstimaginary) /\ (ge_balance_negative_zero_remainder_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductfirst) = 2 * ge_signed_half_zero_remainder_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductfirstimaginary) = S ge_signed_half_zero_remainder_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductfirstimaginary = (ge_first_in_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_equationproductsecond ge_representation_imaginary_code_zero_remainder_equationproductsecond. (((q) = ((ge_representation_real_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond)) * S ((ge_representation_real_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond)) + ((ge_representation_imaginary_code_zero_remainder_equationproductsecond) + (ge_representation_imaginary_code_zero_remainder_equationproductsecond))) /\ ((exists ge_balance_positive_zero_remainder_equationproductsecondreal ge_balance_negative_zero_remainder_equationproductsecondreal. (((((ge_representation_real_code_zero_remainder_equationproductsecond) = 2 * (ge_balance_positive_zero_remainder_equationproductsecondreal) /\ (ge_balance_negative_zero_remainder_equationproductsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductsecondrealdecode. (((ge_representation_real_code_zero_remainder_equationproductsecond) = 2 * ge_signed_half_zero_remainder_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductsecondreal) = S ge_signed_half_zero_remainder_equationproductsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductsecondreal = (ge_second_rn_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductsecondreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductsecondimaginary ge_balance_negative_zero_remainder_equationproductsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductsecond) = 2 * (ge_balance_positive_zero_remainder_equationproductsecondimaginary) /\ (ge_balance_negative_zero_remainder_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductsecond) = 2 * ge_signed_half_zero_remainder_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductsecondimaginary) = S ge_signed_half_zero_remainder_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_equationproduct) + ge_balance_negative_zero_remainder_equationproductsecondimaginary = (ge_second_in_zero_remainder_equationproduct) + ge_balance_positive_zero_remainder_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_equationproductoutput ge_representation_imaginary_code_zero_remainder_equationproductoutput. (((ge_division_product_zero_remainder_equation) = ((ge_representation_real_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput)) * S ((ge_representation_real_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput)) + ((ge_representation_imaginary_code_zero_remainder_equationproductoutput) + (ge_representation_imaginary_code_zero_remainder_equationproductoutput))) /\ ((exists ge_balance_positive_zero_remainder_equationproductoutputreal ge_balance_negative_zero_remainder_equationproductoutputreal. (((((ge_representation_real_code_zero_remainder_equationproductoutput) = 2 * (ge_balance_positive_zero_remainder_equationproductoutputreal) /\ (ge_balance_negative_zero_remainder_equationproductoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_equationproductoutputrealdecode. (((ge_representation_real_code_zero_remainder_equationproductoutput) = 2 * ge_signed_half_zero_remainder_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_equationproductoutputreal) = S ge_signed_half_zero_remainder_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))))))) + ge_balance_negative_zero_remainder_equationproductoutputreal = (((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))))))) + ge_balance_positive_zero_remainder_equationproductoutputreal))) /\ (exists ge_balance_positive_zero_remainder_equationproductoutputimaginary ge_balance_negative_zero_remainder_equationproductoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationproductoutput) = 2 * (ge_balance_positive_zero_remainder_equationproductoutputimaginary) /\ (ge_balance_negative_zero_remainder_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationproductoutput) = 2 * ge_signed_half_zero_remainder_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationproductoutputimaginary) = S ge_signed_half_zero_remainder_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))))))) + ge_balance_negative_zero_remainder_equationproductoutputimaginary = (((((((ge_first_rp_zero_remainder_equationproduct) * (ge_second_in_zero_remainder_equationproduct))) + (((ge_first_rn_zero_remainder_equationproduct) * (ge_second_ip_zero_remainder_equationproduct))))) + (((((ge_first_ip_zero_remainder_equationproduct) * (ge_second_rn_zero_remainder_equationproduct))) + (((ge_first_in_zero_remainder_equationproduct) * (ge_second_rp_zero_remainder_equationproduct))))))) + ge_balance_positive_zero_remainder_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_zero_remainder_equationsum ge_first_rn_zero_remainder_equationsum ge_first_ip_zero_remainder_equationsum ge_first_in_zero_remainder_equationsum ge_second_rp_zero_remainder_equationsum ge_second_rn_zero_remainder_equationsum ge_second_ip_zero_remainder_equationsum ge_second_in_zero_remainder_equationsum. ((exists ge_representation_real_code_zero_remainder_equationsumfirst ge_representation_imaginary_code_zero_remainder_equationsumfirst. (((ge_division_product_zero_remainder_equation) = ((ge_representation_real_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst)) * S ((ge_representation_real_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst)) + ((ge_representation_imaginary_code_zero_remainder_equationsumfirst) + (ge_representation_imaginary_code_zero_remainder_equationsumfirst))) /\ ((exists ge_balance_positive_zero_remainder_equationsumfirstreal ge_balance_negative_zero_remainder_equationsumfirstreal. (((((ge_representation_real_code_zero_remainder_equationsumfirst) = 2 * (ge_balance_positive_zero_remainder_equationsumfirstreal) /\ (ge_balance_negative_zero_remainder_equationsumfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumfirstrealdecode. (((ge_representation_real_code_zero_remainder_equationsumfirst) = 2 * ge_signed_half_zero_remainder_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumfirstreal) = S ge_signed_half_zero_remainder_equationsumfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumfirstreal = (ge_first_rn_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumfirstreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumfirstimaginary ge_balance_negative_zero_remainder_equationsumfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumfirst) = 2 * (ge_balance_positive_zero_remainder_equationsumfirstimaginary) /\ (ge_balance_negative_zero_remainder_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumfirst) = 2 * ge_signed_half_zero_remainder_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumfirstimaginary) = S ge_signed_half_zero_remainder_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumfirstimaginary = (ge_first_in_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_equationsumsecond ge_representation_imaginary_code_zero_remainder_equationsumsecond. (((r) = ((ge_representation_real_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond)) * S ((ge_representation_real_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond)) + ((ge_representation_imaginary_code_zero_remainder_equationsumsecond) + (ge_representation_imaginary_code_zero_remainder_equationsumsecond))) /\ ((exists ge_balance_positive_zero_remainder_equationsumsecondreal ge_balance_negative_zero_remainder_equationsumsecondreal. (((((ge_representation_real_code_zero_remainder_equationsumsecond) = 2 * (ge_balance_positive_zero_remainder_equationsumsecondreal) /\ (ge_balance_negative_zero_remainder_equationsumsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumsecondrealdecode. (((ge_representation_real_code_zero_remainder_equationsumsecond) = 2 * ge_signed_half_zero_remainder_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumsecondreal) = S ge_signed_half_zero_remainder_equationsumsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumsecondreal = (ge_second_rn_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumsecondreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumsecondimaginary ge_balance_negative_zero_remainder_equationsumsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumsecond) = 2 * (ge_balance_positive_zero_remainder_equationsumsecondimaginary) /\ (ge_balance_negative_zero_remainder_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumsecond) = 2 * ge_signed_half_zero_remainder_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumsecondimaginary) = S ge_signed_half_zero_remainder_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_equationsum) + ge_balance_negative_zero_remainder_equationsumsecondimaginary = (ge_second_in_zero_remainder_equationsum) + ge_balance_positive_zero_remainder_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_equationsumoutput ge_representation_imaginary_code_zero_remainder_equationsumoutput. (((a) = ((ge_representation_real_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput)) * S ((ge_representation_real_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput)) + ((ge_representation_imaginary_code_zero_remainder_equationsumoutput) + (ge_representation_imaginary_code_zero_remainder_equationsumoutput))) /\ ((exists ge_balance_positive_zero_remainder_equationsumoutputreal ge_balance_negative_zero_remainder_equationsumoutputreal. (((((ge_representation_real_code_zero_remainder_equationsumoutput) = 2 * (ge_balance_positive_zero_remainder_equationsumoutputreal) /\ (ge_balance_negative_zero_remainder_equationsumoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_equationsumoutputrealdecode. (((ge_representation_real_code_zero_remainder_equationsumoutput) = 2 * ge_signed_half_zero_remainder_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_equationsumoutputreal) = S ge_signed_half_zero_remainder_equationsumoutputrealdecode))) /\ ((((ge_first_rp_zero_remainder_equationsum) + (ge_second_rp_zero_remainder_equationsum))) + ge_balance_negative_zero_remainder_equationsumoutputreal = (((ge_first_rn_zero_remainder_equationsum) + (ge_second_rn_zero_remainder_equationsum))) + ge_balance_positive_zero_remainder_equationsumoutputreal))) /\ (exists ge_balance_positive_zero_remainder_equationsumoutputimaginary ge_balance_negative_zero_remainder_equationsumoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_equationsumoutput) = 2 * (ge_balance_positive_zero_remainder_equationsumoutputimaginary) /\ (ge_balance_negative_zero_remainder_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_equationsumoutput) = 2 * ge_signed_half_zero_remainder_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_equationsumoutputimaginary) = S ge_signed_half_zero_remainder_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_zero_remainder_equationsum) + (ge_second_ip_zero_remainder_equationsum))) + ge_balance_negative_zero_remainder_equationsumoutputimaginary = (((ge_first_in_zero_remainder_equationsum) + (ge_second_in_zero_remainder_equationsum))) + ge_balance_positive_zero_remainder_equationsumoutputimaginary))))))))))) -> r=0 -> (exists gr_quotient_zero_remainder_divides. (exists ge_first_rp_zero_remainder_dividesproduct ge_first_rn_zero_remainder_dividesproduct ge_first_ip_zero_remainder_dividesproduct ge_first_in_zero_remainder_dividesproduct ge_second_rp_zero_remainder_dividesproduct ge_second_rn_zero_remainder_dividesproduct ge_second_ip_zero_remainder_dividesproduct ge_second_in_zero_remainder_dividesproduct. ((exists ge_representation_real_code_zero_remainder_dividesproductfirst ge_representation_imaginary_code_zero_remainder_dividesproductfirst. (((b) = ((ge_representation_real_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst)) * S ((ge_representation_real_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) + (ge_representation_imaginary_code_zero_remainder_dividesproductfirst))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductfirstreal ge_balance_negative_zero_remainder_dividesproductfirstreal. (((((ge_representation_real_code_zero_remainder_dividesproductfirst) = 2 * (ge_balance_positive_zero_remainder_dividesproductfirstreal) /\ (ge_balance_negative_zero_remainder_dividesproductfirstreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductfirstrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductfirst) = 2 * ge_signed_half_zero_remainder_dividesproductfirstrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductfirstreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductfirstreal) = S ge_signed_half_zero_remainder_dividesproductfirstrealdecode))) /\ ((ge_first_rp_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductfirstreal = (ge_first_rn_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductfirstreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductfirstimaginary ge_balance_negative_zero_remainder_dividesproductfirstimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) = 2 * (ge_balance_positive_zero_remainder_dividesproductfirstimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductfirstimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductfirst) = 2 * ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductfirstimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductfirstimaginary) = S ge_signed_half_zero_remainder_dividesproductfirstimaginarydecode))) /\ ((ge_first_ip_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductfirstimaginary = (ge_first_in_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_zero_remainder_dividesproductsecond ge_representation_imaginary_code_zero_remainder_dividesproductsecond. (((gr_quotient_zero_remainder_divides) = ((ge_representation_real_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond)) * S ((ge_representation_real_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) + (ge_representation_imaginary_code_zero_remainder_dividesproductsecond))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductsecondreal ge_balance_negative_zero_remainder_dividesproductsecondreal. (((((ge_representation_real_code_zero_remainder_dividesproductsecond) = 2 * (ge_balance_positive_zero_remainder_dividesproductsecondreal) /\ (ge_balance_negative_zero_remainder_dividesproductsecondreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductsecondrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductsecond) = 2 * ge_signed_half_zero_remainder_dividesproductsecondrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductsecondreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductsecondreal) = S ge_signed_half_zero_remainder_dividesproductsecondrealdecode))) /\ ((ge_second_rp_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductsecondreal = (ge_second_rn_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductsecondreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductsecondimaginary ge_balance_negative_zero_remainder_dividesproductsecondimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) = 2 * (ge_balance_positive_zero_remainder_dividesproductsecondimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductsecondimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductsecond) = 2 * ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductsecondimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductsecondimaginary) = S ge_signed_half_zero_remainder_dividesproductsecondimaginarydecode))) /\ ((ge_second_ip_zero_remainder_dividesproduct) + ge_balance_negative_zero_remainder_dividesproductsecondimaginary = (ge_second_in_zero_remainder_dividesproduct) + ge_balance_positive_zero_remainder_dividesproductsecondimaginary)))))) /\ (exists ge_representation_real_code_zero_remainder_dividesproductoutput ge_representation_imaginary_code_zero_remainder_dividesproductoutput. (((a) = ((ge_representation_real_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput)) * S ((ge_representation_real_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput)) + ((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) + (ge_representation_imaginary_code_zero_remainder_dividesproductoutput))) /\ ((exists ge_balance_positive_zero_remainder_dividesproductoutputreal ge_balance_negative_zero_remainder_dividesproductoutputreal. (((((ge_representation_real_code_zero_remainder_dividesproductoutput) = 2 * (ge_balance_positive_zero_remainder_dividesproductoutputreal) /\ (ge_balance_negative_zero_remainder_dividesproductoutputreal) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductoutputrealdecode. (((ge_representation_real_code_zero_remainder_dividesproductoutput) = 2 * ge_signed_half_zero_remainder_dividesproductoutputrealdecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductoutputreal) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductoutputreal) = S ge_signed_half_zero_remainder_dividesproductoutputrealdecode))) /\ ((((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))))))) + ge_balance_negative_zero_remainder_dividesproductoutputreal = (((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))))))) + ge_balance_positive_zero_remainder_dividesproductoutputreal))) /\ (exists ge_balance_positive_zero_remainder_dividesproductoutputimaginary ge_balance_negative_zero_remainder_dividesproductoutputimaginary. (((((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) = 2 * (ge_balance_positive_zero_remainder_dividesproductoutputimaginary) /\ (ge_balance_negative_zero_remainder_dividesproductoutputimaginary) = 0) \/ exists ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode. (((ge_representation_imaginary_code_zero_remainder_dividesproductoutput) = 2 * ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode + 1 /\ (ge_balance_positive_zero_remainder_dividesproductoutputimaginary) = 0) /\ (ge_balance_negative_zero_remainder_dividesproductoutputimaginary) = S ge_signed_half_zero_remainder_dividesproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))))))) + ge_balance_negative_zero_remainder_dividesproductoutputimaginary = (((((((ge_first_rp_zero_remainder_dividesproduct) * (ge_second_in_zero_remainder_dividesproduct))) + (((ge_first_rn_zero_remainder_dividesproduct) * (ge_second_ip_zero_remainder_dividesproduct))))) + (((((ge_first_ip_zero_remainder_dividesproduct) * (ge_second_rn_zero_remainder_dividesproduct))) + (((ge_first_in_zero_remainder_dividesproduct) * (ge_second_rp_zero_remainder_dividesproduct))))))) + ge_balance_positive_zero_remainder_dividesproductoutputimaginary))))))))))

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 · 9 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 (3)
gaussian add zero rightgaussian multiply output validgaussian multiply output transport
01Fix variables and assumptionsL1–6

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro heq
  6. L6
    intro hr
02Separate the logical casesL7–8

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

  1. L7
    cases heq
  2. L8
    cases heq_witness
03Calculate and transport equalitiesL9–9

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L9
    rewrite hr at heq_witness_right
04Establish houtputL10–19

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

  1. L10
    have houtput : a=x
  2. L11
    specialize gaussian_add_functional (x)
  3. L12
    specialize gaussian_add_functional (0)
  4. L13
    specialize gaussian_add_functional (a)
  5. L14
    specialize gaussian_add_functional (x)
  6. L15
    apply gaussian_add_functional
  7. L16
    exact heq_witness_right
  8. L17
    specialize gaussian_add_zero_right (x)
  9. L18
    apply gaussian_add_zero_right
  10. L19
    specialize gaussian_multiply_output_valid (b)
05Use earlier factsL20–23

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

  1. L20
    specialize gaussian_multiply_output_valid (q)
  2. L21
    specialize gaussian_multiply_output_valid (x)
  3. L22
    apply gaussian_multiply_output_valid
  4. L23
    exact heq_witness_left
06Construct an explicit witnessL24–24

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

  1. L24
    exists (q)
07Use earlier factsL25–29

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

  1. L25
    specialize gaussian_multiply_output_transport (b)
  2. L26
    specialize gaussian_multiply_output_transport (q)
  3. L27
    specialize gaussian_multiply_output_transport (x)
  4. L28
    specialize gaussian_multiply_output_transport (a)
  5. L29
    apply gaussian_multiply_output_transport
08Calculate and transport equalitiesL30–30

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L30
    symm
09Use earlier factsL31–32

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

  1. L31
    exact houtput
  2. L32
    exact heq_witness_left

Library-wide reading audit

Original defined command ledger · 32 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro heq
  6. 0006intro hr
  7. 0007cases heq
  8. 0008cases heq_witness
  9. 0009rewrite hr at heq_witness_right
  10. 0010have houtput : a=x
  11. 0011specialize gaussian_add_functional (x)
  12. 0012specialize gaussian_add_functional (0)
  13. 0013specialize gaussian_add_functional (a)
  14. 0014specialize gaussian_add_functional (x)
  15. 0015apply gaussian_add_functional
  16. 0016exact heq_witness_right
  17. 0017specialize gaussian_add_zero_right (x)
  18. 0018apply gaussian_add_zero_right
  19. 0019specialize gaussian_multiply_output_valid (b)
  20. 0020specialize gaussian_multiply_output_valid (q)
  21. 0021specialize gaussian_multiply_output_valid (x)
  22. 0022apply gaussian_multiply_output_valid
  23. 0023exact heq_witness_left
  24. 0024exists (q)
  25. 0025specialize gaussian_multiply_output_transport (b)
  26. 0026specialize gaussian_multiply_output_transport (q)
  27. 0027specialize gaussian_multiply_output_transport (x)
  28. 0028specialize gaussian_multiply_output_transport (a)
  29. 0029apply gaussian_multiply_output_transport
  30. 0030symm
  31. 0031exact houtput
  32. 0032exact heq_witness_left