GF0052

gaussian_division_divisible_remainder_zero

A strictly norm-bounded Gaussian remainder must vanish when the original divisor actually divides the dividend.

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

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

Definition DAG

GNorm(z,n) · 3ZPairAdd(a,b,c) · 1GMul(a,b,c) · 1GDvd(d,z) · 2Lt(a,b) · 1

Actual proof prerequisites

gaussian_common_divisor_euclidean_backwardgaussian_divides_reflexivegaussian_norm_input_validgaussian_norm_exists · checked external prerequisitegaussian_multiply_input_right_validgaussian_norm_functional · checked external prerequisitegaussian_norm_multiply · checked external prerequisitefour_square_bounded_multiple_is_zero · checked external prerequisitegaussian_norm_zero_implies_code_zerogaussian_norm_value_transport
Original expanded first-order statement 
forall a b q r U V. (exists ge_division_product_divisible_equation. ((exists ge_first_rp_divisible_equationproduct ge_first_rn_divisible_equationproduct ge_first_ip_divisible_equationproduct ge_first_in_divisible_equationproduct ge_second_rp_divisible_equationproduct ge_second_rn_divisible_equationproduct ge_second_ip_divisible_equationproduct ge_second_in_divisible_equationproduct. ((exists ge_representation_real_code_divisible_equationproductfirst ge_representation_imaginary_code_divisible_equationproductfirst. (((b) = ((ge_representation_real_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst)) * S ((ge_representation_real_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst)) + ((ge_representation_imaginary_code_divisible_equationproductfirst) + (ge_representation_imaginary_code_divisible_equationproductfirst))) /\ ((exists ge_balance_positive_divisible_equationproductfirstreal ge_balance_negative_divisible_equationproductfirstreal. (((((ge_representation_real_code_divisible_equationproductfirst) = 2 * (ge_balance_positive_divisible_equationproductfirstreal) /\ (ge_balance_negative_divisible_equationproductfirstreal) = 0) \/ exists ge_signed_half_divisible_equationproductfirstrealdecode. (((ge_representation_real_code_divisible_equationproductfirst) = 2 * ge_signed_half_divisible_equationproductfirstrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductfirstreal) = 0) /\ (ge_balance_negative_divisible_equationproductfirstreal) = S ge_signed_half_divisible_equationproductfirstrealdecode))) /\ ((ge_first_rp_divisible_equationproduct) + ge_balance_negative_divisible_equationproductfirstreal = (ge_first_rn_divisible_equationproduct) + ge_balance_positive_divisible_equationproductfirstreal))) /\ (exists ge_balance_positive_divisible_equationproductfirstimaginary ge_balance_negative_divisible_equationproductfirstimaginary. (((((ge_representation_imaginary_code_divisible_equationproductfirst) = 2 * (ge_balance_positive_divisible_equationproductfirstimaginary) /\ (ge_balance_negative_divisible_equationproductfirstimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductfirst) = 2 * ge_signed_half_divisible_equationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductfirstimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductfirstimaginary) = S ge_signed_half_divisible_equationproductfirstimaginarydecode))) /\ ((ge_first_ip_divisible_equationproduct) + ge_balance_negative_divisible_equationproductfirstimaginary = (ge_first_in_divisible_equationproduct) + ge_balance_positive_divisible_equationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_equationproductsecond ge_representation_imaginary_code_divisible_equationproductsecond. (((q) = ((ge_representation_real_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond)) * S ((ge_representation_real_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond)) + ((ge_representation_imaginary_code_divisible_equationproductsecond) + (ge_representation_imaginary_code_divisible_equationproductsecond))) /\ ((exists ge_balance_positive_divisible_equationproductsecondreal ge_balance_negative_divisible_equationproductsecondreal. (((((ge_representation_real_code_divisible_equationproductsecond) = 2 * (ge_balance_positive_divisible_equationproductsecondreal) /\ (ge_balance_negative_divisible_equationproductsecondreal) = 0) \/ exists ge_signed_half_divisible_equationproductsecondrealdecode. (((ge_representation_real_code_divisible_equationproductsecond) = 2 * ge_signed_half_divisible_equationproductsecondrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductsecondreal) = 0) /\ (ge_balance_negative_divisible_equationproductsecondreal) = S ge_signed_half_divisible_equationproductsecondrealdecode))) /\ ((ge_second_rp_divisible_equationproduct) + ge_balance_negative_divisible_equationproductsecondreal = (ge_second_rn_divisible_equationproduct) + ge_balance_positive_divisible_equationproductsecondreal))) /\ (exists ge_balance_positive_divisible_equationproductsecondimaginary ge_balance_negative_divisible_equationproductsecondimaginary. (((((ge_representation_imaginary_code_divisible_equationproductsecond) = 2 * (ge_balance_positive_divisible_equationproductsecondimaginary) /\ (ge_balance_negative_divisible_equationproductsecondimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductsecond) = 2 * ge_signed_half_divisible_equationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductsecondimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductsecondimaginary) = S ge_signed_half_divisible_equationproductsecondimaginarydecode))) /\ ((ge_second_ip_divisible_equationproduct) + ge_balance_negative_divisible_equationproductsecondimaginary = (ge_second_in_divisible_equationproduct) + ge_balance_positive_divisible_equationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_equationproductoutput ge_representation_imaginary_code_divisible_equationproductoutput. (((ge_division_product_divisible_equation) = ((ge_representation_real_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput)) * S ((ge_representation_real_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput)) + ((ge_representation_imaginary_code_divisible_equationproductoutput) + (ge_representation_imaginary_code_divisible_equationproductoutput))) /\ ((exists ge_balance_positive_divisible_equationproductoutputreal ge_balance_negative_divisible_equationproductoutputreal. (((((ge_representation_real_code_divisible_equationproductoutput) = 2 * (ge_balance_positive_divisible_equationproductoutputreal) /\ (ge_balance_negative_divisible_equationproductoutputreal) = 0) \/ exists ge_signed_half_divisible_equationproductoutputrealdecode. (((ge_representation_real_code_divisible_equationproductoutput) = 2 * ge_signed_half_divisible_equationproductoutputrealdecode + 1 /\ (ge_balance_positive_divisible_equationproductoutputreal) = 0) /\ (ge_balance_negative_divisible_equationproductoutputreal) = S ge_signed_half_divisible_equationproductoutputrealdecode))) /\ ((((((((ge_first_rp_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))))))) + ge_balance_negative_divisible_equationproductoutputreal = (((((((ge_first_rp_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))))))) + ge_balance_positive_divisible_equationproductoutputreal))) /\ (exists ge_balance_positive_divisible_equationproductoutputimaginary ge_balance_negative_divisible_equationproductoutputimaginary. (((((ge_representation_imaginary_code_divisible_equationproductoutput) = 2 * (ge_balance_positive_divisible_equationproductoutputimaginary) /\ (ge_balance_negative_divisible_equationproductoutputimaginary) = 0) \/ exists ge_signed_half_divisible_equationproductoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_equationproductoutput) = 2 * ge_signed_half_divisible_equationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationproductoutputimaginary) = 0) /\ (ge_balance_negative_divisible_equationproductoutputimaginary) = S ge_signed_half_divisible_equationproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))))))) + ge_balance_negative_divisible_equationproductoutputimaginary = (((((((ge_first_rp_divisible_equationproduct) * (ge_second_in_divisible_equationproduct))) + (((ge_first_rn_divisible_equationproduct) * (ge_second_ip_divisible_equationproduct))))) + (((((ge_first_ip_divisible_equationproduct) * (ge_second_rn_divisible_equationproduct))) + (((ge_first_in_divisible_equationproduct) * (ge_second_rp_divisible_equationproduct))))))) + ge_balance_positive_divisible_equationproductoutputimaginary))))))))) /\ (exists ge_first_rp_divisible_equationsum ge_first_rn_divisible_equationsum ge_first_ip_divisible_equationsum ge_first_in_divisible_equationsum ge_second_rp_divisible_equationsum ge_second_rn_divisible_equationsum ge_second_ip_divisible_equationsum ge_second_in_divisible_equationsum. ((exists ge_representation_real_code_divisible_equationsumfirst ge_representation_imaginary_code_divisible_equationsumfirst. (((ge_division_product_divisible_equation) = ((ge_representation_real_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst)) * S ((ge_representation_real_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst)) + ((ge_representation_imaginary_code_divisible_equationsumfirst) + (ge_representation_imaginary_code_divisible_equationsumfirst))) /\ ((exists ge_balance_positive_divisible_equationsumfirstreal ge_balance_negative_divisible_equationsumfirstreal. (((((ge_representation_real_code_divisible_equationsumfirst) = 2 * (ge_balance_positive_divisible_equationsumfirstreal) /\ (ge_balance_negative_divisible_equationsumfirstreal) = 0) \/ exists ge_signed_half_divisible_equationsumfirstrealdecode. (((ge_representation_real_code_divisible_equationsumfirst) = 2 * ge_signed_half_divisible_equationsumfirstrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumfirstreal) = 0) /\ (ge_balance_negative_divisible_equationsumfirstreal) = S ge_signed_half_divisible_equationsumfirstrealdecode))) /\ ((ge_first_rp_divisible_equationsum) + ge_balance_negative_divisible_equationsumfirstreal = (ge_first_rn_divisible_equationsum) + ge_balance_positive_divisible_equationsumfirstreal))) /\ (exists ge_balance_positive_divisible_equationsumfirstimaginary ge_balance_negative_divisible_equationsumfirstimaginary. (((((ge_representation_imaginary_code_divisible_equationsumfirst) = 2 * (ge_balance_positive_divisible_equationsumfirstimaginary) /\ (ge_balance_negative_divisible_equationsumfirstimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumfirst) = 2 * ge_signed_half_divisible_equationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumfirstimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumfirstimaginary) = S ge_signed_half_divisible_equationsumfirstimaginarydecode))) /\ ((ge_first_ip_divisible_equationsum) + ge_balance_negative_divisible_equationsumfirstimaginary = (ge_first_in_divisible_equationsum) + ge_balance_positive_divisible_equationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_equationsumsecond ge_representation_imaginary_code_divisible_equationsumsecond. (((r) = ((ge_representation_real_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond)) * S ((ge_representation_real_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond)) + ((ge_representation_imaginary_code_divisible_equationsumsecond) + (ge_representation_imaginary_code_divisible_equationsumsecond))) /\ ((exists ge_balance_positive_divisible_equationsumsecondreal ge_balance_negative_divisible_equationsumsecondreal. (((((ge_representation_real_code_divisible_equationsumsecond) = 2 * (ge_balance_positive_divisible_equationsumsecondreal) /\ (ge_balance_negative_divisible_equationsumsecondreal) = 0) \/ exists ge_signed_half_divisible_equationsumsecondrealdecode. (((ge_representation_real_code_divisible_equationsumsecond) = 2 * ge_signed_half_divisible_equationsumsecondrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumsecondreal) = 0) /\ (ge_balance_negative_divisible_equationsumsecondreal) = S ge_signed_half_divisible_equationsumsecondrealdecode))) /\ ((ge_second_rp_divisible_equationsum) + ge_balance_negative_divisible_equationsumsecondreal = (ge_second_rn_divisible_equationsum) + ge_balance_positive_divisible_equationsumsecondreal))) /\ (exists ge_balance_positive_divisible_equationsumsecondimaginary ge_balance_negative_divisible_equationsumsecondimaginary. (((((ge_representation_imaginary_code_divisible_equationsumsecond) = 2 * (ge_balance_positive_divisible_equationsumsecondimaginary) /\ (ge_balance_negative_divisible_equationsumsecondimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumsecond) = 2 * ge_signed_half_divisible_equationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumsecondimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumsecondimaginary) = S ge_signed_half_divisible_equationsumsecondimaginarydecode))) /\ ((ge_second_ip_divisible_equationsum) + ge_balance_negative_divisible_equationsumsecondimaginary = (ge_second_in_divisible_equationsum) + ge_balance_positive_divisible_equationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_equationsumoutput ge_representation_imaginary_code_divisible_equationsumoutput. (((a) = ((ge_representation_real_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput)) * S ((ge_representation_real_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput)) + ((ge_representation_imaginary_code_divisible_equationsumoutput) + (ge_representation_imaginary_code_divisible_equationsumoutput))) /\ ((exists ge_balance_positive_divisible_equationsumoutputreal ge_balance_negative_divisible_equationsumoutputreal. (((((ge_representation_real_code_divisible_equationsumoutput) = 2 * (ge_balance_positive_divisible_equationsumoutputreal) /\ (ge_balance_negative_divisible_equationsumoutputreal) = 0) \/ exists ge_signed_half_divisible_equationsumoutputrealdecode. (((ge_representation_real_code_divisible_equationsumoutput) = 2 * ge_signed_half_divisible_equationsumoutputrealdecode + 1 /\ (ge_balance_positive_divisible_equationsumoutputreal) = 0) /\ (ge_balance_negative_divisible_equationsumoutputreal) = S ge_signed_half_divisible_equationsumoutputrealdecode))) /\ ((((ge_first_rp_divisible_equationsum) + (ge_second_rp_divisible_equationsum))) + ge_balance_negative_divisible_equationsumoutputreal = (((ge_first_rn_divisible_equationsum) + (ge_second_rn_divisible_equationsum))) + ge_balance_positive_divisible_equationsumoutputreal))) /\ (exists ge_balance_positive_divisible_equationsumoutputimaginary ge_balance_negative_divisible_equationsumoutputimaginary. (((((ge_representation_imaginary_code_divisible_equationsumoutput) = 2 * (ge_balance_positive_divisible_equationsumoutputimaginary) /\ (ge_balance_negative_divisible_equationsumoutputimaginary) = 0) \/ exists ge_signed_half_divisible_equationsumoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_equationsumoutput) = 2 * ge_signed_half_divisible_equationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_equationsumoutputimaginary) = 0) /\ (ge_balance_negative_divisible_equationsumoutputimaginary) = S ge_signed_half_divisible_equationsumoutputimaginarydecode))) /\ ((((ge_first_ip_divisible_equationsum) + (ge_second_ip_divisible_equationsum))) + ge_balance_negative_divisible_equationsumoutputimaginary = (((ge_first_in_divisible_equationsum) + (ge_second_in_divisible_equationsum))) + ge_balance_positive_divisible_equationsumoutputimaginary))))))))))) -> (exists ge_norm_rp_divisible_remainder_norm ge_norm_rn_divisible_remainder_norm ge_norm_ip_divisible_remainder_norm ge_norm_in_divisible_remainder_norm. ((exists ge_representation_real_code_divisible_remainder_normrepresentation ge_representation_imaginary_code_divisible_remainder_normrepresentation. (((r) = ((ge_representation_real_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation)) * S ((ge_representation_real_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation)) + ((ge_representation_imaginary_code_divisible_remainder_normrepresentation) + (ge_representation_imaginary_code_divisible_remainder_normrepresentation))) /\ ((exists ge_balance_positive_divisible_remainder_normrepresentationreal ge_balance_negative_divisible_remainder_normrepresentationreal. (((((ge_representation_real_code_divisible_remainder_normrepresentation) = 2 * (ge_balance_positive_divisible_remainder_normrepresentationreal) /\ (ge_balance_negative_divisible_remainder_normrepresentationreal) = 0) \/ exists ge_signed_half_divisible_remainder_normrepresentationrealdecode. (((ge_representation_real_code_divisible_remainder_normrepresentation) = 2 * ge_signed_half_divisible_remainder_normrepresentationrealdecode + 1 /\ (ge_balance_positive_divisible_remainder_normrepresentationreal) = 0) /\ (ge_balance_negative_divisible_remainder_normrepresentationreal) = S ge_signed_half_divisible_remainder_normrepresentationrealdecode))) /\ ((ge_norm_rp_divisible_remainder_norm) + ge_balance_negative_divisible_remainder_normrepresentationreal = (ge_norm_rn_divisible_remainder_norm) + ge_balance_positive_divisible_remainder_normrepresentationreal))) /\ (exists ge_balance_positive_divisible_remainder_normrepresentationimaginary ge_balance_negative_divisible_remainder_normrepresentationimaginary. (((((ge_representation_imaginary_code_divisible_remainder_normrepresentation) = 2 * (ge_balance_positive_divisible_remainder_normrepresentationimaginary) /\ (ge_balance_negative_divisible_remainder_normrepresentationimaginary) = 0) \/ exists ge_signed_half_divisible_remainder_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_divisible_remainder_normrepresentation) = 2 * ge_signed_half_divisible_remainder_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_divisible_remainder_normrepresentationimaginary) = 0) /\ (ge_balance_negative_divisible_remainder_normrepresentationimaginary) = S ge_signed_half_divisible_remainder_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_divisible_remainder_norm) + ge_balance_negative_divisible_remainder_normrepresentationimaginary = (ge_norm_in_divisible_remainder_norm) + ge_balance_positive_divisible_remainder_normrepresentationimaginary)))))) /\ (exists ge_real_square_divisible_remainder_normsquare ge_imaginary_square_divisible_remainder_normsquare. ((((((ge_norm_rp_divisible_remainder_norm) * (ge_norm_rp_divisible_remainder_norm))) + (((ge_norm_rn_divisible_remainder_norm) * (ge_norm_rn_divisible_remainder_norm)))) = ((ge_real_square_divisible_remainder_normsquare) + (((((ge_norm_rp_divisible_remainder_norm) * (ge_norm_rn_divisible_remainder_norm))) + (((ge_norm_rn_divisible_remainder_norm) * (ge_norm_rp_divisible_remainder_norm))))))) /\ ((((((ge_norm_ip_divisible_remainder_norm) * (ge_norm_ip_divisible_remainder_norm))) + (((ge_norm_in_divisible_remainder_norm) * (ge_norm_in_divisible_remainder_norm)))) = ((ge_imaginary_square_divisible_remainder_normsquare) + (((((ge_norm_ip_divisible_remainder_norm) * (ge_norm_in_divisible_remainder_norm))) + (((ge_norm_in_divisible_remainder_norm) * (ge_norm_ip_divisible_remainder_norm))))))) /\ ((U) = ge_real_square_divisible_remainder_normsquare + ge_imaginary_square_divisible_remainder_normsquare)))))) -> (exists ge_norm_rp_divisible_divisor_norm ge_norm_rn_divisible_divisor_norm ge_norm_ip_divisible_divisor_norm ge_norm_in_divisible_divisor_norm. ((exists ge_representation_real_code_divisible_divisor_normrepresentation ge_representation_imaginary_code_divisible_divisor_normrepresentation. (((b) = ((ge_representation_real_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation)) * S ((ge_representation_real_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation)) + ((ge_representation_imaginary_code_divisible_divisor_normrepresentation) + (ge_representation_imaginary_code_divisible_divisor_normrepresentation))) /\ ((exists ge_balance_positive_divisible_divisor_normrepresentationreal ge_balance_negative_divisible_divisor_normrepresentationreal. (((((ge_representation_real_code_divisible_divisor_normrepresentation) = 2 * (ge_balance_positive_divisible_divisor_normrepresentationreal) /\ (ge_balance_negative_divisible_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_divisible_divisor_normrepresentationrealdecode. (((ge_representation_real_code_divisible_divisor_normrepresentation) = 2 * ge_signed_half_divisible_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_divisible_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_divisible_divisor_normrepresentationreal) = S ge_signed_half_divisible_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_divisible_divisor_norm) + ge_balance_negative_divisible_divisor_normrepresentationreal = (ge_norm_rn_divisible_divisor_norm) + ge_balance_positive_divisible_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_divisible_divisor_normrepresentationimaginary ge_balance_negative_divisible_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_divisible_divisor_normrepresentation) = 2 * (ge_balance_positive_divisible_divisor_normrepresentationimaginary) /\ (ge_balance_negative_divisible_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_divisible_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_divisible_divisor_normrepresentation) = 2 * ge_signed_half_divisible_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_divisible_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_divisible_divisor_normrepresentationimaginary) = S ge_signed_half_divisible_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_divisible_divisor_norm) + ge_balance_negative_divisible_divisor_normrepresentationimaginary = (ge_norm_in_divisible_divisor_norm) + ge_balance_positive_divisible_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_divisible_divisor_normsquare ge_imaginary_square_divisible_divisor_normsquare. ((((((ge_norm_rp_divisible_divisor_norm) * (ge_norm_rp_divisible_divisor_norm))) + (((ge_norm_rn_divisible_divisor_norm) * (ge_norm_rn_divisible_divisor_norm)))) = ((ge_real_square_divisible_divisor_normsquare) + (((((ge_norm_rp_divisible_divisor_norm) * (ge_norm_rn_divisible_divisor_norm))) + (((ge_norm_rn_divisible_divisor_norm) * (ge_norm_rp_divisible_divisor_norm))))))) /\ ((((((ge_norm_ip_divisible_divisor_norm) * (ge_norm_ip_divisible_divisor_norm))) + (((ge_norm_in_divisible_divisor_norm) * (ge_norm_in_divisible_divisor_norm)))) = ((ge_imaginary_square_divisible_divisor_normsquare) + (((((ge_norm_ip_divisible_divisor_norm) * (ge_norm_in_divisible_divisor_norm))) + (((ge_norm_in_divisible_divisor_norm) * (ge_norm_ip_divisible_divisor_norm))))))) /\ ((V) = ge_real_square_divisible_divisor_normsquare + ge_imaginary_square_divisible_divisor_normsquare)))))) -> (exists ge_gap_divisible_strict. ge_gap_divisible_strict + S (U) = (V)) -> (exists gr_quotient_divisible_given. (exists ge_first_rp_divisible_givenproduct ge_first_rn_divisible_givenproduct ge_first_ip_divisible_givenproduct ge_first_in_divisible_givenproduct ge_second_rp_divisible_givenproduct ge_second_rn_divisible_givenproduct ge_second_ip_divisible_givenproduct ge_second_in_divisible_givenproduct. ((exists ge_representation_real_code_divisible_givenproductfirst ge_representation_imaginary_code_divisible_givenproductfirst. (((b) = ((ge_representation_real_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst)) * S ((ge_representation_real_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst)) + ((ge_representation_imaginary_code_divisible_givenproductfirst) + (ge_representation_imaginary_code_divisible_givenproductfirst))) /\ ((exists ge_balance_positive_divisible_givenproductfirstreal ge_balance_negative_divisible_givenproductfirstreal. (((((ge_representation_real_code_divisible_givenproductfirst) = 2 * (ge_balance_positive_divisible_givenproductfirstreal) /\ (ge_balance_negative_divisible_givenproductfirstreal) = 0) \/ exists ge_signed_half_divisible_givenproductfirstrealdecode. (((ge_representation_real_code_divisible_givenproductfirst) = 2 * ge_signed_half_divisible_givenproductfirstrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductfirstreal) = 0) /\ (ge_balance_negative_divisible_givenproductfirstreal) = S ge_signed_half_divisible_givenproductfirstrealdecode))) /\ ((ge_first_rp_divisible_givenproduct) + ge_balance_negative_divisible_givenproductfirstreal = (ge_first_rn_divisible_givenproduct) + ge_balance_positive_divisible_givenproductfirstreal))) /\ (exists ge_balance_positive_divisible_givenproductfirstimaginary ge_balance_negative_divisible_givenproductfirstimaginary. (((((ge_representation_imaginary_code_divisible_givenproductfirst) = 2 * (ge_balance_positive_divisible_givenproductfirstimaginary) /\ (ge_balance_negative_divisible_givenproductfirstimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductfirstimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductfirst) = 2 * ge_signed_half_divisible_givenproductfirstimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductfirstimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductfirstimaginary) = S ge_signed_half_divisible_givenproductfirstimaginarydecode))) /\ ((ge_first_ip_divisible_givenproduct) + ge_balance_negative_divisible_givenproductfirstimaginary = (ge_first_in_divisible_givenproduct) + ge_balance_positive_divisible_givenproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_divisible_givenproductsecond ge_representation_imaginary_code_divisible_givenproductsecond. (((gr_quotient_divisible_given) = ((ge_representation_real_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond)) * S ((ge_representation_real_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond)) + ((ge_representation_imaginary_code_divisible_givenproductsecond) + (ge_representation_imaginary_code_divisible_givenproductsecond))) /\ ((exists ge_balance_positive_divisible_givenproductsecondreal ge_balance_negative_divisible_givenproductsecondreal. (((((ge_representation_real_code_divisible_givenproductsecond) = 2 * (ge_balance_positive_divisible_givenproductsecondreal) /\ (ge_balance_negative_divisible_givenproductsecondreal) = 0) \/ exists ge_signed_half_divisible_givenproductsecondrealdecode. (((ge_representation_real_code_divisible_givenproductsecond) = 2 * ge_signed_half_divisible_givenproductsecondrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductsecondreal) = 0) /\ (ge_balance_negative_divisible_givenproductsecondreal) = S ge_signed_half_divisible_givenproductsecondrealdecode))) /\ ((ge_second_rp_divisible_givenproduct) + ge_balance_negative_divisible_givenproductsecondreal = (ge_second_rn_divisible_givenproduct) + ge_balance_positive_divisible_givenproductsecondreal))) /\ (exists ge_balance_positive_divisible_givenproductsecondimaginary ge_balance_negative_divisible_givenproductsecondimaginary. (((((ge_representation_imaginary_code_divisible_givenproductsecond) = 2 * (ge_balance_positive_divisible_givenproductsecondimaginary) /\ (ge_balance_negative_divisible_givenproductsecondimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductsecondimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductsecond) = 2 * ge_signed_half_divisible_givenproductsecondimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductsecondimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductsecondimaginary) = S ge_signed_half_divisible_givenproductsecondimaginarydecode))) /\ ((ge_second_ip_divisible_givenproduct) + ge_balance_negative_divisible_givenproductsecondimaginary = (ge_second_in_divisible_givenproduct) + ge_balance_positive_divisible_givenproductsecondimaginary)))))) /\ (exists ge_representation_real_code_divisible_givenproductoutput ge_representation_imaginary_code_divisible_givenproductoutput. (((a) = ((ge_representation_real_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput)) * S ((ge_representation_real_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput)) + ((ge_representation_imaginary_code_divisible_givenproductoutput) + (ge_representation_imaginary_code_divisible_givenproductoutput))) /\ ((exists ge_balance_positive_divisible_givenproductoutputreal ge_balance_negative_divisible_givenproductoutputreal. (((((ge_representation_real_code_divisible_givenproductoutput) = 2 * (ge_balance_positive_divisible_givenproductoutputreal) /\ (ge_balance_negative_divisible_givenproductoutputreal) = 0) \/ exists ge_signed_half_divisible_givenproductoutputrealdecode. (((ge_representation_real_code_divisible_givenproductoutput) = 2 * ge_signed_half_divisible_givenproductoutputrealdecode + 1 /\ (ge_balance_positive_divisible_givenproductoutputreal) = 0) /\ (ge_balance_negative_divisible_givenproductoutputreal) = S ge_signed_half_divisible_givenproductoutputrealdecode))) /\ ((((((((ge_first_rp_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))))))) + ge_balance_negative_divisible_givenproductoutputreal = (((((((ge_first_rp_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))))))) + ge_balance_positive_divisible_givenproductoutputreal))) /\ (exists ge_balance_positive_divisible_givenproductoutputimaginary ge_balance_negative_divisible_givenproductoutputimaginary. (((((ge_representation_imaginary_code_divisible_givenproductoutput) = 2 * (ge_balance_positive_divisible_givenproductoutputimaginary) /\ (ge_balance_negative_divisible_givenproductoutputimaginary) = 0) \/ exists ge_signed_half_divisible_givenproductoutputimaginarydecode. (((ge_representation_imaginary_code_divisible_givenproductoutput) = 2 * ge_signed_half_divisible_givenproductoutputimaginarydecode + 1 /\ (ge_balance_positive_divisible_givenproductoutputimaginary) = 0) /\ (ge_balance_negative_divisible_givenproductoutputimaginary) = S ge_signed_half_divisible_givenproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))))))) + ge_balance_negative_divisible_givenproductoutputimaginary = (((((((ge_first_rp_divisible_givenproduct) * (ge_second_in_divisible_givenproduct))) + (((ge_first_rn_divisible_givenproduct) * (ge_second_ip_divisible_givenproduct))))) + (((((ge_first_ip_divisible_givenproduct) * (ge_second_rn_divisible_givenproduct))) + (((ge_first_in_divisible_givenproduct) * (ge_second_rp_divisible_givenproduct))))))) + ge_balance_positive_divisible_givenproductoutputimaginary)))))))))) -> r=0

Complete tactic proof in conservative notation

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

66 script commands · 12 reading checkpoints · 4 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 (6)
gaussian common divisor euclidean backwardgaussian divides reflexivegaussian norm input validgaussian multiply input right validgaussian norm zero implies code zerogaussian norm value transport
01Fix variables and assumptionsL1–10

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 U
  6. L6
    intro V
  7. L7
    intro heq
  8. L8
    intro hr
  9. L9
    intro hb
  10. L10
    intro hlt
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hdiv
03Establish hremL12–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply gaussian common divisor euclidean backward.

  1. L12
  2. L13
    specialize gaussian_common_divisor_euclidean_backward (b)
  3. L14
    specialize gaussian_common_divisor_euclidean_backward (a)
  4. L15
    specialize gaussian_common_divisor_euclidean_backward (b)
  5. L16
    specialize gaussian_common_divisor_euclidean_backward (q)
  6. L17
    specialize gaussian_common_divisor_euclidean_backward (r)
  7. L18
    apply gaussian_common_divisor_euclidean_backward
  8. L19
    exact heq
  9. L20
    exact hdiv
  10. L21
    specialize gaussian_divides_reflexive (b)
04Use earlier factsL22–26

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

  1. L22
    apply gaussian_divides_reflexive
  2. L23
    specialize gaussian_norm_input_valid (b)
  3. L24
    specialize gaussian_norm_input_valid (V)
  4. L25
    apply gaussian_norm_input_valid
  5. L26
    exact hb
05Separate the logical casesL27–27

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

  1. L27
    cases hrem
06Establish hML28–35

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

  1. L28
    have hM : ∃ M. GNorm(x,M)Definitions: GNorm(x,M)Original native command in the exact edition
  2. L29
    specialize gaussian_norm_exists (x)
  3. L30
    apply gaussian_norm_exists
  4. L31
    specialize gaussian_multiply_input_right_valid (b)
  5. L32
    specialize gaussian_multiply_input_right_valid (x)
  6. L33
    specialize gaussian_multiply_input_right_valid (r)
  7. L34
    apply gaussian_multiply_input_right_valid
  8. L35
    exact hrem_witness
07Separate the logical casesL36–36

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

  1. L36
    cases hM
08Establish hvalueL37–46

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

  1. L37
    have hvalue : U=V*x1
  2. L38
    specialize gaussian_norm_functional (r)
  3. L39
    specialize gaussian_norm_functional (U)
  4. L40
    specialize gaussian_norm_functional (V*x1)
  5. L41
    apply gaussian_norm_functional
  6. L42
    exact hr
  7. L43
    specialize gaussian_norm_multiply (b)
  8. L44
    specialize gaussian_norm_multiply (x)
  9. L45
    specialize gaussian_norm_multiply (r)
  10. L46
    specialize gaussian_norm_multiply (V)
09Use earlier factsL47–51

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

  1. L47
    specialize gaussian_norm_multiply (x1)
  2. L48
    apply gaussian_norm_multiply
  3. L49
    exact hb
  4. L50
    exact hM_witness
  5. L51
    exact hrem_witness
10Establish hzeroL52–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square bounded multiple is zero.

  1. L52
    have hzero : U=0
  2. L53
    specialize four_square_bounded_multiple_is_zero (V)
  3. L54
    specialize four_square_bounded_multiple_is_zero (U)
  4. L55
    apply four_square_bounded_multiple_is_zero
  5. L56
    exact hlt
11Construct an explicit witnessL57–57

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

  1. L57
    exists (x1)
12Use earlier factsL58–66

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

  1. L58
    exact hvalue
  2. L59
    specialize gaussian_norm_zero_implies_code_zero (r)
  3. L60
    apply gaussian_norm_zero_implies_code_zero
  4. L61
    specialize gaussian_norm_value_transport (r)
  5. L62
    specialize gaussian_norm_value_transport (U)
  6. L63
    specialize gaussian_norm_value_transport (0)
  7. L64
    apply gaussian_norm_value_transport
  8. L65
    exact hzero
  9. L66
    exact hr

Library-wide reading audit

Original defined command ledger · 66 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro U
  6. 0006intro V
  7. 0007intro heq
  8. 0008intro hr
  9. 0009intro hb
  10. 0010intro hlt
  11. 0011intro hdiv
  12. 0012have hrem : GDvd(b,r)
  13. 0013specialize gaussian_common_divisor_euclidean_backward (b)
  14. 0014specialize gaussian_common_divisor_euclidean_backward (a)
  15. 0015specialize gaussian_common_divisor_euclidean_backward (b)
  16. 0016specialize gaussian_common_divisor_euclidean_backward (q)
  17. 0017specialize gaussian_common_divisor_euclidean_backward (r)
  18. 0018apply gaussian_common_divisor_euclidean_backward
  19. 0019exact heq
  20. 0020exact hdiv
  21. 0021specialize gaussian_divides_reflexive (b)
  22. 0022apply gaussian_divides_reflexive
  23. 0023specialize gaussian_norm_input_valid (b)
  24. 0024specialize gaussian_norm_input_valid (V)
  25. 0025apply gaussian_norm_input_valid
  26. 0026exact hb
  27. 0027cases hrem
  28. 0028have hM : ∃ M. GNorm(x,M)
  29. 0029specialize gaussian_norm_exists (x)
  30. 0030apply gaussian_norm_exists
  31. 0031specialize gaussian_multiply_input_right_valid (b)
  32. 0032specialize gaussian_multiply_input_right_valid (x)
  33. 0033specialize gaussian_multiply_input_right_valid (r)
  34. 0034apply gaussian_multiply_input_right_valid
  35. 0035exact hrem_witness
  36. 0036cases hM
  37. 0037have hvalue : U=V*x1
  38. 0038specialize gaussian_norm_functional (r)
  39. 0039specialize gaussian_norm_functional (U)
  40. 0040specialize gaussian_norm_functional (V*x1)
  41. 0041apply gaussian_norm_functional
  42. 0042exact hr
  43. 0043specialize gaussian_norm_multiply (b)
  44. 0044specialize gaussian_norm_multiply (x)
  45. 0045specialize gaussian_norm_multiply (r)
  46. 0046specialize gaussian_norm_multiply (V)
  47. 0047specialize gaussian_norm_multiply (x1)
  48. 0048apply gaussian_norm_multiply
  49. 0049exact hb
  50. 0050exact hM_witness
  51. 0051exact hrem_witness
  52. 0052have hzero : U=0
  53. 0053specialize four_square_bounded_multiple_is_zero (V)
  54. 0054specialize four_square_bounded_multiple_is_zero (U)
  55. 0055apply four_square_bounded_multiple_is_zero
  56. 0056exact hlt
  57. 0057exists (x1)
  58. 0058exact hvalue
  59. 0059specialize gaussian_norm_zero_implies_code_zero (r)
  60. 0060apply gaussian_norm_zero_implies_code_zero
  61. 0061specialize gaussian_norm_value_transport (r)
  62. 0062specialize gaussian_norm_value_transport (U)
  63. 0063specialize gaussian_norm_value_transport (0)
  64. 0064apply gaussian_norm_value_transport
  65. 0065exact hzero
  66. 0066exact hr