GF0082

gaussian_nonunit_divisor_strict_quotient

Dividing a nonzero Gaussian value by an actual nonunit strictly decreases the quotient norm, even when the quotient itself is a unit.

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. ∀ z. ∀ D. ∀ N. GDvd(d,z) → GNorm(d,D) → GNorm(z,N) → ¬z = 0 → ¬GUnit(d) → ∃ x. ∃ y. GMul(d,x,z) ∧ (GNorm(x,y) ∧ (Lt(y,N) ∧ ¬x = 0))

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

Definition DAG

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

Actual proof prerequisites

gaussian_divisor_norm_factorgaussian_norm_nonzerofactor_nonzero_left · checked external prerequisitefactor_nonzero_right · checked external prerequisitegaussian_search_nonunit_norm_twosucc_le_mul_of_two_le_right · checked external prerequisitemul_comm · checked external prerequisitegaussian_code_zero_implies_norm_zero
Original expanded first-order statement 
forall d z D N. (exists gr_quotient_quotient_divisor. (exists ge_first_rp_quotient_divisorproduct ge_first_rn_quotient_divisorproduct ge_first_ip_quotient_divisorproduct ge_first_in_quotient_divisorproduct ge_second_rp_quotient_divisorproduct ge_second_rn_quotient_divisorproduct ge_second_ip_quotient_divisorproduct ge_second_in_quotient_divisorproduct. ((exists ge_representation_real_code_quotient_divisorproductfirst ge_representation_imaginary_code_quotient_divisorproductfirst. (((d) = ((ge_representation_real_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst)) * S ((ge_representation_real_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst)) + ((ge_representation_imaginary_code_quotient_divisorproductfirst) + (ge_representation_imaginary_code_quotient_divisorproductfirst))) /\ ((exists ge_balance_positive_quotient_divisorproductfirstreal ge_balance_negative_quotient_divisorproductfirstreal. (((((ge_representation_real_code_quotient_divisorproductfirst) = 2 * (ge_balance_positive_quotient_divisorproductfirstreal) /\ (ge_balance_negative_quotient_divisorproductfirstreal) = 0) \/ exists ge_signed_half_quotient_divisorproductfirstrealdecode. (((ge_representation_real_code_quotient_divisorproductfirst) = 2 * ge_signed_half_quotient_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductfirstreal) = 0) /\ (ge_balance_negative_quotient_divisorproductfirstreal) = S ge_signed_half_quotient_divisorproductfirstrealdecode))) /\ ((ge_first_rp_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductfirstreal = (ge_first_rn_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductfirstreal))) /\ (exists ge_balance_positive_quotient_divisorproductfirstimaginary ge_balance_negative_quotient_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductfirst) = 2 * (ge_balance_positive_quotient_divisorproductfirstimaginary) /\ (ge_balance_negative_quotient_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductfirst) = 2 * ge_signed_half_quotient_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductfirstimaginary) = S ge_signed_half_quotient_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductfirstimaginary = (ge_first_in_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_divisorproductsecond ge_representation_imaginary_code_quotient_divisorproductsecond. (((gr_quotient_quotient_divisor) = ((ge_representation_real_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond)) * S ((ge_representation_real_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond)) + ((ge_representation_imaginary_code_quotient_divisorproductsecond) + (ge_representation_imaginary_code_quotient_divisorproductsecond))) /\ ((exists ge_balance_positive_quotient_divisorproductsecondreal ge_balance_negative_quotient_divisorproductsecondreal. (((((ge_representation_real_code_quotient_divisorproductsecond) = 2 * (ge_balance_positive_quotient_divisorproductsecondreal) /\ (ge_balance_negative_quotient_divisorproductsecondreal) = 0) \/ exists ge_signed_half_quotient_divisorproductsecondrealdecode. (((ge_representation_real_code_quotient_divisorproductsecond) = 2 * ge_signed_half_quotient_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductsecondreal) = 0) /\ (ge_balance_negative_quotient_divisorproductsecondreal) = S ge_signed_half_quotient_divisorproductsecondrealdecode))) /\ ((ge_second_rp_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductsecondreal = (ge_second_rn_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductsecondreal))) /\ (exists ge_balance_positive_quotient_divisorproductsecondimaginary ge_balance_negative_quotient_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductsecond) = 2 * (ge_balance_positive_quotient_divisorproductsecondimaginary) /\ (ge_balance_negative_quotient_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductsecond) = 2 * ge_signed_half_quotient_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductsecondimaginary) = S ge_signed_half_quotient_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_quotient_divisorproduct) + ge_balance_negative_quotient_divisorproductsecondimaginary = (ge_second_in_quotient_divisorproduct) + ge_balance_positive_quotient_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_divisorproductoutput ge_representation_imaginary_code_quotient_divisorproductoutput. (((z) = ((ge_representation_real_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput)) * S ((ge_representation_real_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput)) + ((ge_representation_imaginary_code_quotient_divisorproductoutput) + (ge_representation_imaginary_code_quotient_divisorproductoutput))) /\ ((exists ge_balance_positive_quotient_divisorproductoutputreal ge_balance_negative_quotient_divisorproductoutputreal. (((((ge_representation_real_code_quotient_divisorproductoutput) = 2 * (ge_balance_positive_quotient_divisorproductoutputreal) /\ (ge_balance_negative_quotient_divisorproductoutputreal) = 0) \/ exists ge_signed_half_quotient_divisorproductoutputrealdecode. (((ge_representation_real_code_quotient_divisorproductoutput) = 2 * ge_signed_half_quotient_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_quotient_divisorproductoutputreal) = 0) /\ (ge_balance_negative_quotient_divisorproductoutputreal) = S ge_signed_half_quotient_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))))))) + ge_balance_negative_quotient_divisorproductoutputreal = (((((((ge_first_rp_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))))))) + ge_balance_positive_quotient_divisorproductoutputreal))) /\ (exists ge_balance_positive_quotient_divisorproductoutputimaginary ge_balance_negative_quotient_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_quotient_divisorproductoutput) = 2 * (ge_balance_positive_quotient_divisorproductoutputimaginary) /\ (ge_balance_negative_quotient_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_quotient_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_divisorproductoutput) = 2 * ge_signed_half_quotient_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_quotient_divisorproductoutputimaginary) = S ge_signed_half_quotient_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))))))) + ge_balance_negative_quotient_divisorproductoutputimaginary = (((((((ge_first_rp_quotient_divisorproduct) * (ge_second_in_quotient_divisorproduct))) + (((ge_first_rn_quotient_divisorproduct) * (ge_second_ip_quotient_divisorproduct))))) + (((((ge_first_ip_quotient_divisorproduct) * (ge_second_rn_quotient_divisorproduct))) + (((ge_first_in_quotient_divisorproduct) * (ge_second_rp_quotient_divisorproduct))))))) + ge_balance_positive_quotient_divisorproductoutputimaginary)))))))))) -> (exists ge_norm_rp_quotient_divisor_norm ge_norm_rn_quotient_divisor_norm ge_norm_ip_quotient_divisor_norm ge_norm_in_quotient_divisor_norm. ((exists ge_representation_real_code_quotient_divisor_normrepresentation ge_representation_imaginary_code_quotient_divisor_normrepresentation. (((d) = ((ge_representation_real_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation)) * S ((ge_representation_real_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation)) + ((ge_representation_imaginary_code_quotient_divisor_normrepresentation) + (ge_representation_imaginary_code_quotient_divisor_normrepresentation))) /\ ((exists ge_balance_positive_quotient_divisor_normrepresentationreal ge_balance_negative_quotient_divisor_normrepresentationreal. (((((ge_representation_real_code_quotient_divisor_normrepresentation) = 2 * (ge_balance_positive_quotient_divisor_normrepresentationreal) /\ (ge_balance_negative_quotient_divisor_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_divisor_normrepresentationrealdecode. (((ge_representation_real_code_quotient_divisor_normrepresentation) = 2 * ge_signed_half_quotient_divisor_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_divisor_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_divisor_normrepresentationreal) = S ge_signed_half_quotient_divisor_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_divisor_norm) + ge_balance_negative_quotient_divisor_normrepresentationreal = (ge_norm_rn_quotient_divisor_norm) + ge_balance_positive_quotient_divisor_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_divisor_normrepresentationimaginary ge_balance_negative_quotient_divisor_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_divisor_normrepresentation) = 2 * (ge_balance_positive_quotient_divisor_normrepresentationimaginary) /\ (ge_balance_negative_quotient_divisor_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_divisor_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_divisor_normrepresentation) = 2 * ge_signed_half_quotient_divisor_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_divisor_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_divisor_normrepresentationimaginary) = S ge_signed_half_quotient_divisor_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_divisor_norm) + ge_balance_negative_quotient_divisor_normrepresentationimaginary = (ge_norm_in_quotient_divisor_norm) + ge_balance_positive_quotient_divisor_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_divisor_normsquare ge_imaginary_square_quotient_divisor_normsquare. ((((((ge_norm_rp_quotient_divisor_norm) * (ge_norm_rp_quotient_divisor_norm))) + (((ge_norm_rn_quotient_divisor_norm) * (ge_norm_rn_quotient_divisor_norm)))) = ((ge_real_square_quotient_divisor_normsquare) + (((((ge_norm_rp_quotient_divisor_norm) * (ge_norm_rn_quotient_divisor_norm))) + (((ge_norm_rn_quotient_divisor_norm) * (ge_norm_rp_quotient_divisor_norm))))))) /\ ((((((ge_norm_ip_quotient_divisor_norm) * (ge_norm_ip_quotient_divisor_norm))) + (((ge_norm_in_quotient_divisor_norm) * (ge_norm_in_quotient_divisor_norm)))) = ((ge_imaginary_square_quotient_divisor_normsquare) + (((((ge_norm_ip_quotient_divisor_norm) * (ge_norm_in_quotient_divisor_norm))) + (((ge_norm_in_quotient_divisor_norm) * (ge_norm_ip_quotient_divisor_norm))))))) /\ ((D) = ge_real_square_quotient_divisor_normsquare + ge_imaginary_square_quotient_divisor_normsquare)))))) -> (exists ge_norm_rp_quotient_total_norm ge_norm_rn_quotient_total_norm ge_norm_ip_quotient_total_norm ge_norm_in_quotient_total_norm. ((exists ge_representation_real_code_quotient_total_normrepresentation ge_representation_imaginary_code_quotient_total_normrepresentation. (((z) = ((ge_representation_real_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation)) * S ((ge_representation_real_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation)) + ((ge_representation_imaginary_code_quotient_total_normrepresentation) + (ge_representation_imaginary_code_quotient_total_normrepresentation))) /\ ((exists ge_balance_positive_quotient_total_normrepresentationreal ge_balance_negative_quotient_total_normrepresentationreal. (((((ge_representation_real_code_quotient_total_normrepresentation) = 2 * (ge_balance_positive_quotient_total_normrepresentationreal) /\ (ge_balance_negative_quotient_total_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_total_normrepresentationrealdecode. (((ge_representation_real_code_quotient_total_normrepresentation) = 2 * ge_signed_half_quotient_total_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_total_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_total_normrepresentationreal) = S ge_signed_half_quotient_total_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_total_norm) + ge_balance_negative_quotient_total_normrepresentationreal = (ge_norm_rn_quotient_total_norm) + ge_balance_positive_quotient_total_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_total_normrepresentationimaginary ge_balance_negative_quotient_total_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_total_normrepresentation) = 2 * (ge_balance_positive_quotient_total_normrepresentationimaginary) /\ (ge_balance_negative_quotient_total_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_total_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_total_normrepresentation) = 2 * ge_signed_half_quotient_total_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_total_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_total_normrepresentationimaginary) = S ge_signed_half_quotient_total_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_total_norm) + ge_balance_negative_quotient_total_normrepresentationimaginary = (ge_norm_in_quotient_total_norm) + ge_balance_positive_quotient_total_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_total_normsquare ge_imaginary_square_quotient_total_normsquare. ((((((ge_norm_rp_quotient_total_norm) * (ge_norm_rp_quotient_total_norm))) + (((ge_norm_rn_quotient_total_norm) * (ge_norm_rn_quotient_total_norm)))) = ((ge_real_square_quotient_total_normsquare) + (((((ge_norm_rp_quotient_total_norm) * (ge_norm_rn_quotient_total_norm))) + (((ge_norm_rn_quotient_total_norm) * (ge_norm_rp_quotient_total_norm))))))) /\ ((((((ge_norm_ip_quotient_total_norm) * (ge_norm_ip_quotient_total_norm))) + (((ge_norm_in_quotient_total_norm) * (ge_norm_in_quotient_total_norm)))) = ((ge_imaginary_square_quotient_total_normsquare) + (((((ge_norm_ip_quotient_total_norm) * (ge_norm_in_quotient_total_norm))) + (((ge_norm_in_quotient_total_norm) * (ge_norm_ip_quotient_total_norm))))))) /\ ((N) = ge_real_square_quotient_total_normsquare + ge_imaginary_square_quotient_total_normsquare)))))) -> ~(z=0) -> ~(exists gr_inverse_quotient_nonunit. (exists ge_first_rp_quotient_nonunitidentity ge_first_rn_quotient_nonunitidentity ge_first_ip_quotient_nonunitidentity ge_first_in_quotient_nonunitidentity ge_second_rp_quotient_nonunitidentity ge_second_rn_quotient_nonunitidentity ge_second_ip_quotient_nonunitidentity ge_second_in_quotient_nonunitidentity. ((exists ge_representation_real_code_quotient_nonunitidentityfirst ge_representation_imaginary_code_quotient_nonunitidentityfirst. (((d) = ((ge_representation_real_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst)) * S ((ge_representation_real_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst)) + ((ge_representation_imaginary_code_quotient_nonunitidentityfirst) + (ge_representation_imaginary_code_quotient_nonunitidentityfirst))) /\ ((exists ge_balance_positive_quotient_nonunitidentityfirstreal ge_balance_negative_quotient_nonunitidentityfirstreal. (((((ge_representation_real_code_quotient_nonunitidentityfirst) = 2 * (ge_balance_positive_quotient_nonunitidentityfirstreal) /\ (ge_balance_negative_quotient_nonunitidentityfirstreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentityfirstrealdecode. (((ge_representation_real_code_quotient_nonunitidentityfirst) = 2 * ge_signed_half_quotient_nonunitidentityfirstrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityfirstreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentityfirstreal) = S ge_signed_half_quotient_nonunitidentityfirstrealdecode))) /\ ((ge_first_rp_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentityfirstreal = (ge_first_rn_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentityfirstreal))) /\ (exists ge_balance_positive_quotient_nonunitidentityfirstimaginary ge_balance_negative_quotient_nonunitidentityfirstimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentityfirst) = 2 * (ge_balance_positive_quotient_nonunitidentityfirstimaginary) /\ (ge_balance_negative_quotient_nonunitidentityfirstimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentityfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentityfirst) = 2 * ge_signed_half_quotient_nonunitidentityfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityfirstimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentityfirstimaginary) = S ge_signed_half_quotient_nonunitidentityfirstimaginarydecode))) /\ ((ge_first_ip_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentityfirstimaginary = (ge_first_in_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentityfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_nonunitidentitysecond ge_representation_imaginary_code_quotient_nonunitidentitysecond. (((gr_inverse_quotient_nonunit) = ((ge_representation_real_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond)) * S ((ge_representation_real_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond)) + ((ge_representation_imaginary_code_quotient_nonunitidentitysecond) + (ge_representation_imaginary_code_quotient_nonunitidentitysecond))) /\ ((exists ge_balance_positive_quotient_nonunitidentitysecondreal ge_balance_negative_quotient_nonunitidentitysecondreal. (((((ge_representation_real_code_quotient_nonunitidentitysecond) = 2 * (ge_balance_positive_quotient_nonunitidentitysecondreal) /\ (ge_balance_negative_quotient_nonunitidentitysecondreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentitysecondrealdecode. (((ge_representation_real_code_quotient_nonunitidentitysecond) = 2 * ge_signed_half_quotient_nonunitidentitysecondrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentitysecondreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentitysecondreal) = S ge_signed_half_quotient_nonunitidentitysecondrealdecode))) /\ ((ge_second_rp_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentitysecondreal = (ge_second_rn_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentitysecondreal))) /\ (exists ge_balance_positive_quotient_nonunitidentitysecondimaginary ge_balance_negative_quotient_nonunitidentitysecondimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentitysecond) = 2 * (ge_balance_positive_quotient_nonunitidentitysecondimaginary) /\ (ge_balance_negative_quotient_nonunitidentitysecondimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentitysecondimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentitysecond) = 2 * ge_signed_half_quotient_nonunitidentitysecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentitysecondimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentitysecondimaginary) = S ge_signed_half_quotient_nonunitidentitysecondimaginarydecode))) /\ ((ge_second_ip_quotient_nonunitidentity) + ge_balance_negative_quotient_nonunitidentitysecondimaginary = (ge_second_in_quotient_nonunitidentity) + ge_balance_positive_quotient_nonunitidentitysecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_nonunitidentityoutput ge_representation_imaginary_code_quotient_nonunitidentityoutput. (((6) = ((ge_representation_real_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput)) * S ((ge_representation_real_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput)) + ((ge_representation_imaginary_code_quotient_nonunitidentityoutput) + (ge_representation_imaginary_code_quotient_nonunitidentityoutput))) /\ ((exists ge_balance_positive_quotient_nonunitidentityoutputreal ge_balance_negative_quotient_nonunitidentityoutputreal. (((((ge_representation_real_code_quotient_nonunitidentityoutput) = 2 * (ge_balance_positive_quotient_nonunitidentityoutputreal) /\ (ge_balance_negative_quotient_nonunitidentityoutputreal) = 0) \/ exists ge_signed_half_quotient_nonunitidentityoutputrealdecode. (((ge_representation_real_code_quotient_nonunitidentityoutput) = 2 * ge_signed_half_quotient_nonunitidentityoutputrealdecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityoutputreal) = 0) /\ (ge_balance_negative_quotient_nonunitidentityoutputreal) = S ge_signed_half_quotient_nonunitidentityoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))))))) + ge_balance_negative_quotient_nonunitidentityoutputreal = (((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))))))) + ge_balance_positive_quotient_nonunitidentityoutputreal))) /\ (exists ge_balance_positive_quotient_nonunitidentityoutputimaginary ge_balance_negative_quotient_nonunitidentityoutputimaginary. (((((ge_representation_imaginary_code_quotient_nonunitidentityoutput) = 2 * (ge_balance_positive_quotient_nonunitidentityoutputimaginary) /\ (ge_balance_negative_quotient_nonunitidentityoutputimaginary) = 0) \/ exists ge_signed_half_quotient_nonunitidentityoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_nonunitidentityoutput) = 2 * ge_signed_half_quotient_nonunitidentityoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_nonunitidentityoutputimaginary) = 0) /\ (ge_balance_negative_quotient_nonunitidentityoutputimaginary) = S ge_signed_half_quotient_nonunitidentityoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))))))) + ge_balance_negative_quotient_nonunitidentityoutputimaginary = (((((((ge_first_rp_quotient_nonunitidentity) * (ge_second_in_quotient_nonunitidentity))) + (((ge_first_rn_quotient_nonunitidentity) * (ge_second_ip_quotient_nonunitidentity))))) + (((((ge_first_ip_quotient_nonunitidentity) * (ge_second_rn_quotient_nonunitidentity))) + (((ge_first_in_quotient_nonunitidentity) * (ge_second_rp_quotient_nonunitidentity))))))) + ge_balance_positive_quotient_nonunitidentityoutputimaginary)))))))))) -> exists q Q. ((exists ge_first_rp_quotient_product ge_first_rn_quotient_product ge_first_ip_quotient_product ge_first_in_quotient_product ge_second_rp_quotient_product ge_second_rn_quotient_product ge_second_ip_quotient_product ge_second_in_quotient_product. ((exists ge_representation_real_code_quotient_productfirst ge_representation_imaginary_code_quotient_productfirst. (((d) = ((ge_representation_real_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst)) * S ((ge_representation_real_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst)) + ((ge_representation_imaginary_code_quotient_productfirst) + (ge_representation_imaginary_code_quotient_productfirst))) /\ ((exists ge_balance_positive_quotient_productfirstreal ge_balance_negative_quotient_productfirstreal. (((((ge_representation_real_code_quotient_productfirst) = 2 * (ge_balance_positive_quotient_productfirstreal) /\ (ge_balance_negative_quotient_productfirstreal) = 0) \/ exists ge_signed_half_quotient_productfirstrealdecode. (((ge_representation_real_code_quotient_productfirst) = 2 * ge_signed_half_quotient_productfirstrealdecode + 1 /\ (ge_balance_positive_quotient_productfirstreal) = 0) /\ (ge_balance_negative_quotient_productfirstreal) = S ge_signed_half_quotient_productfirstrealdecode))) /\ ((ge_first_rp_quotient_product) + ge_balance_negative_quotient_productfirstreal = (ge_first_rn_quotient_product) + ge_balance_positive_quotient_productfirstreal))) /\ (exists ge_balance_positive_quotient_productfirstimaginary ge_balance_negative_quotient_productfirstimaginary. (((((ge_representation_imaginary_code_quotient_productfirst) = 2 * (ge_balance_positive_quotient_productfirstimaginary) /\ (ge_balance_negative_quotient_productfirstimaginary) = 0) \/ exists ge_signed_half_quotient_productfirstimaginarydecode. (((ge_representation_imaginary_code_quotient_productfirst) = 2 * ge_signed_half_quotient_productfirstimaginarydecode + 1 /\ (ge_balance_positive_quotient_productfirstimaginary) = 0) /\ (ge_balance_negative_quotient_productfirstimaginary) = S ge_signed_half_quotient_productfirstimaginarydecode))) /\ ((ge_first_ip_quotient_product) + ge_balance_negative_quotient_productfirstimaginary = (ge_first_in_quotient_product) + ge_balance_positive_quotient_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_quotient_productsecond ge_representation_imaginary_code_quotient_productsecond. (((q) = ((ge_representation_real_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond)) * S ((ge_representation_real_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond)) + ((ge_representation_imaginary_code_quotient_productsecond) + (ge_representation_imaginary_code_quotient_productsecond))) /\ ((exists ge_balance_positive_quotient_productsecondreal ge_balance_negative_quotient_productsecondreal. (((((ge_representation_real_code_quotient_productsecond) = 2 * (ge_balance_positive_quotient_productsecondreal) /\ (ge_balance_negative_quotient_productsecondreal) = 0) \/ exists ge_signed_half_quotient_productsecondrealdecode. (((ge_representation_real_code_quotient_productsecond) = 2 * ge_signed_half_quotient_productsecondrealdecode + 1 /\ (ge_balance_positive_quotient_productsecondreal) = 0) /\ (ge_balance_negative_quotient_productsecondreal) = S ge_signed_half_quotient_productsecondrealdecode))) /\ ((ge_second_rp_quotient_product) + ge_balance_negative_quotient_productsecondreal = (ge_second_rn_quotient_product) + ge_balance_positive_quotient_productsecondreal))) /\ (exists ge_balance_positive_quotient_productsecondimaginary ge_balance_negative_quotient_productsecondimaginary. (((((ge_representation_imaginary_code_quotient_productsecond) = 2 * (ge_balance_positive_quotient_productsecondimaginary) /\ (ge_balance_negative_quotient_productsecondimaginary) = 0) \/ exists ge_signed_half_quotient_productsecondimaginarydecode. (((ge_representation_imaginary_code_quotient_productsecond) = 2 * ge_signed_half_quotient_productsecondimaginarydecode + 1 /\ (ge_balance_positive_quotient_productsecondimaginary) = 0) /\ (ge_balance_negative_quotient_productsecondimaginary) = S ge_signed_half_quotient_productsecondimaginarydecode))) /\ ((ge_second_ip_quotient_product) + ge_balance_negative_quotient_productsecondimaginary = (ge_second_in_quotient_product) + ge_balance_positive_quotient_productsecondimaginary)))))) /\ (exists ge_representation_real_code_quotient_productoutput ge_representation_imaginary_code_quotient_productoutput. (((z) = ((ge_representation_real_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput)) * S ((ge_representation_real_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput)) + ((ge_representation_imaginary_code_quotient_productoutput) + (ge_representation_imaginary_code_quotient_productoutput))) /\ ((exists ge_balance_positive_quotient_productoutputreal ge_balance_negative_quotient_productoutputreal. (((((ge_representation_real_code_quotient_productoutput) = 2 * (ge_balance_positive_quotient_productoutputreal) /\ (ge_balance_negative_quotient_productoutputreal) = 0) \/ exists ge_signed_half_quotient_productoutputrealdecode. (((ge_representation_real_code_quotient_productoutput) = 2 * ge_signed_half_quotient_productoutputrealdecode + 1 /\ (ge_balance_positive_quotient_productoutputreal) = 0) /\ (ge_balance_negative_quotient_productoutputreal) = S ge_signed_half_quotient_productoutputrealdecode))) /\ ((((((((ge_first_rp_quotient_product) * (ge_second_rp_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_rn_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_in_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_ip_quotient_product))))))) + ge_balance_negative_quotient_productoutputreal = (((((((ge_first_rp_quotient_product) * (ge_second_rn_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_rp_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_ip_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_in_quotient_product))))))) + ge_balance_positive_quotient_productoutputreal))) /\ (exists ge_balance_positive_quotient_productoutputimaginary ge_balance_negative_quotient_productoutputimaginary. (((((ge_representation_imaginary_code_quotient_productoutput) = 2 * (ge_balance_positive_quotient_productoutputimaginary) /\ (ge_balance_negative_quotient_productoutputimaginary) = 0) \/ exists ge_signed_half_quotient_productoutputimaginarydecode. (((ge_representation_imaginary_code_quotient_productoutput) = 2 * ge_signed_half_quotient_productoutputimaginarydecode + 1 /\ (ge_balance_positive_quotient_productoutputimaginary) = 0) /\ (ge_balance_negative_quotient_productoutputimaginary) = S ge_signed_half_quotient_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_quotient_product) * (ge_second_ip_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_in_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_rp_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_rn_quotient_product))))))) + ge_balance_negative_quotient_productoutputimaginary = (((((((ge_first_rp_quotient_product) * (ge_second_in_quotient_product))) + (((ge_first_rn_quotient_product) * (ge_second_ip_quotient_product))))) + (((((ge_first_ip_quotient_product) * (ge_second_rn_quotient_product))) + (((ge_first_in_quotient_product) * (ge_second_rp_quotient_product))))))) + ge_balance_positive_quotient_productoutputimaginary))))))))) /\ ((exists ge_norm_rp_quotient_norm ge_norm_rn_quotient_norm ge_norm_ip_quotient_norm ge_norm_in_quotient_norm. ((exists ge_representation_real_code_quotient_normrepresentation ge_representation_imaginary_code_quotient_normrepresentation. (((q) = ((ge_representation_real_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation)) * S ((ge_representation_real_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation)) + ((ge_representation_imaginary_code_quotient_normrepresentation) + (ge_representation_imaginary_code_quotient_normrepresentation))) /\ ((exists ge_balance_positive_quotient_normrepresentationreal ge_balance_negative_quotient_normrepresentationreal. (((((ge_representation_real_code_quotient_normrepresentation) = 2 * (ge_balance_positive_quotient_normrepresentationreal) /\ (ge_balance_negative_quotient_normrepresentationreal) = 0) \/ exists ge_signed_half_quotient_normrepresentationrealdecode. (((ge_representation_real_code_quotient_normrepresentation) = 2 * ge_signed_half_quotient_normrepresentationrealdecode + 1 /\ (ge_balance_positive_quotient_normrepresentationreal) = 0) /\ (ge_balance_negative_quotient_normrepresentationreal) = S ge_signed_half_quotient_normrepresentationrealdecode))) /\ ((ge_norm_rp_quotient_norm) + ge_balance_negative_quotient_normrepresentationreal = (ge_norm_rn_quotient_norm) + ge_balance_positive_quotient_normrepresentationreal))) /\ (exists ge_balance_positive_quotient_normrepresentationimaginary ge_balance_negative_quotient_normrepresentationimaginary. (((((ge_representation_imaginary_code_quotient_normrepresentation) = 2 * (ge_balance_positive_quotient_normrepresentationimaginary) /\ (ge_balance_negative_quotient_normrepresentationimaginary) = 0) \/ exists ge_signed_half_quotient_normrepresentationimaginarydecode. (((ge_representation_imaginary_code_quotient_normrepresentation) = 2 * ge_signed_half_quotient_normrepresentationimaginarydecode + 1 /\ (ge_balance_positive_quotient_normrepresentationimaginary) = 0) /\ (ge_balance_negative_quotient_normrepresentationimaginary) = S ge_signed_half_quotient_normrepresentationimaginarydecode))) /\ ((ge_norm_ip_quotient_norm) + ge_balance_negative_quotient_normrepresentationimaginary = (ge_norm_in_quotient_norm) + ge_balance_positive_quotient_normrepresentationimaginary)))))) /\ (exists ge_real_square_quotient_normsquare ge_imaginary_square_quotient_normsquare. ((((((ge_norm_rp_quotient_norm) * (ge_norm_rp_quotient_norm))) + (((ge_norm_rn_quotient_norm) * (ge_norm_rn_quotient_norm)))) = ((ge_real_square_quotient_normsquare) + (((((ge_norm_rp_quotient_norm) * (ge_norm_rn_quotient_norm))) + (((ge_norm_rn_quotient_norm) * (ge_norm_rp_quotient_norm))))))) /\ ((((((ge_norm_ip_quotient_norm) * (ge_norm_ip_quotient_norm))) + (((ge_norm_in_quotient_norm) * (ge_norm_in_quotient_norm)))) = ((ge_imaginary_square_quotient_normsquare) + (((((ge_norm_ip_quotient_norm) * (ge_norm_in_quotient_norm))) + (((ge_norm_in_quotient_norm) * (ge_norm_ip_quotient_norm))))))) /\ ((Q) = ge_real_square_quotient_normsquare + ge_imaginary_square_quotient_normsquare)))))) /\ ((exists ge_gap_quotient_strict. ge_gap_quotient_strict + S (Q) = (N)) /\ (~(q=0)))))

Complete tactic proof in conservative notation

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

77 script commands · 16 reading checkpoints · 5 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 (4)
gaussian divisor norm factorgaussian norm nonzerogaussian search nonunit norm twogaussian code zero implies norm zero
01Fix variables and assumptionsL1–9

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

  1. L1
    intro d
  2. L2
    intro z
  3. L3
    intro D
  4. L4
    intro N
  5. L5
    intro hd
  6. L6
    intro hD
  7. L7
    intro hN
  8. L8
    intro hz
  9. L9
    intro hu
02Establish hfL10–18

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

  1. L10
    have hf : ∃ q. ∃ Q. GMul(d,q,z) ∧ (GNorm(q,Q) ∧ N = D · Q)Definitions: GMul(d,q,z)GNorm(q,Q)Original native command in the exact edition
  2. L11
    specialize gaussian_divisor_norm_factor (d)
  3. L12
    specialize gaussian_divisor_norm_factor (z)
  4. L13
    specialize gaussian_divisor_norm_factor (D)
  5. L14
    specialize gaussian_divisor_norm_factor (N)
  6. L15
    apply gaussian_divisor_norm_factor
  7. L16
    exact hd
  8. L17
    exact hD
  9. L18
    exact hN
03Separate the logical casesL19–22

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

  1. L19
    cases hf
  2. L20
    cases hf_witness
  3. L21
    cases hf_witness_witness
  4. L22
    cases hf_witness_witness_right
04Establish hpositiveL23–30

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

  1. L23
    have hpositive : ~(N=0)
  2. L24
    intro hzero
  3. L25
    specialize gaussian_norm_nonzero (z)
  4. L26
    specialize gaussian_norm_nonzero (N)
  5. L27
    apply gaussian_norm_nonzero
  6. L28
    exact hN
  7. L29
    exact hz
  8. L30
    exact hzero
05Establish hDpositiveL31–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero left.

  1. L31
    have hDpositive : ~(D=0)
  2. L32
    intro hzero
  3. L33
    specialize factor_nonzero_left (N)
  4. L34
    specialize factor_nonzero_left (D)
  5. L35
    specialize factor_nonzero_left (x1)
  6. L36
    apply factor_nonzero_left
  7. L37
    exact hpositive
  8. L38
    exact hf_witness_witness_right_right
  9. L39
    exact hzero
06Establish hQpositiveL40–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor nonzero right.

  1. L40
    have hQpositive : ~(x1=0)
  2. L41
    intro hzero
  3. L42
    specialize factor_nonzero_right (N)
  4. L43
    specialize factor_nonzero_right (D)
  5. L44
    specialize factor_nonzero_right (x1)
  6. L45
    apply factor_nonzero_right
  7. L46
    exact hpositive
  8. L47
    exact hf_witness_witness_right_right
  9. L48
    exact hzero
07Construct an explicit witnessL49–50

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

  1. L49
    exists (x)
  2. L50
    exists (x1)
08Separate the logical casesL51–51

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

  1. L51
    split
09Use earlier factsL52–52

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

  1. L52
    exact hf_witness_witness_left
10Separate the logical casesL53–53

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

  1. L53
    split
11Use earlier factsL54–54

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

  1. L54
    exact hf_witness_witness_right_left
12Separate the logical casesL55–55

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

  1. L55
    split
13Establish heqL56–65

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L56
    have heq : N=x1*D
  2. L57
    trans D*x1
  3. L58
    exact hf_witness_witness_right_right
  4. L59
    apply mul_comm
  5. L60
    rewrite heq
  6. L61
    specialize succ_le_mul_of_two_le_right (x1)
  7. L62
    specialize succ_le_mul_of_two_le_right (D)
  8. L63
    apply succ_le_mul_of_two_le_right
  9. L64
    exact hQpositive
  10. L65
    specialize gaussian_search_nonunit_norm_two (d)
14Use earlier factsL66–70

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

  1. L66
    specialize gaussian_search_nonunit_norm_two (D)
  2. L67
    apply gaussian_search_nonunit_norm_two
  3. L68
    exact hD
  4. L69
    exact hDpositive
  5. L70
    exact hu
15Fix variables and assumptionsL71–71

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

  1. L71
    intro hqzero
16Use earlier factsL72–77

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

  1. L72
    apply hQpositive
  2. L73
    specialize gaussian_code_zero_implies_norm_zero (x)
  3. L74
    specialize gaussian_code_zero_implies_norm_zero (x1)
  4. L75
    apply gaussian_code_zero_implies_norm_zero
  5. L76
    exact hf_witness_witness_right_left
  6. L77
    exact hqzero

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro d
  2. 0002intro z
  3. 0003intro D
  4. 0004intro N
  5. 0005intro hd
  6. 0006intro hD
  7. 0007intro hN
  8. 0008intro hz
  9. 0009intro hu
  10. 0010have hf : ∃ q. ∃ Q. GMul(d,q,z) ∧ (GNorm(q,Q) ∧ N = D · Q)
  11. 0011specialize gaussian_divisor_norm_factor (d)
  12. 0012specialize gaussian_divisor_norm_factor (z)
  13. 0013specialize gaussian_divisor_norm_factor (D)
  14. 0014specialize gaussian_divisor_norm_factor (N)
  15. 0015apply gaussian_divisor_norm_factor
  16. 0016exact hd
  17. 0017exact hD
  18. 0018exact hN
  19. 0019cases hf
  20. 0020cases hf_witness
  21. 0021cases hf_witness_witness
  22. 0022cases hf_witness_witness_right
  23. 0023have hpositive : ~(N=0)
  24. 0024intro hzero
  25. 0025specialize gaussian_norm_nonzero (z)
  26. 0026specialize gaussian_norm_nonzero (N)
  27. 0027apply gaussian_norm_nonzero
  28. 0028exact hN
  29. 0029exact hz
  30. 0030exact hzero
  31. 0031have hDpositive : ~(D=0)
  32. 0032intro hzero
  33. 0033specialize factor_nonzero_left (N)
  34. 0034specialize factor_nonzero_left (D)
  35. 0035specialize factor_nonzero_left (x1)
  36. 0036apply factor_nonzero_left
  37. 0037exact hpositive
  38. 0038exact hf_witness_witness_right_right
  39. 0039exact hzero
  40. 0040have hQpositive : ~(x1=0)
  41. 0041intro hzero
  42. 0042specialize factor_nonzero_right (N)
  43. 0043specialize factor_nonzero_right (D)
  44. 0044specialize factor_nonzero_right (x1)
  45. 0045apply factor_nonzero_right
  46. 0046exact hpositive
  47. 0047exact hf_witness_witness_right_right
  48. 0048exact hzero
  49. 0049exists (x)
  50. 0050exists (x1)
  51. 0051split
  52. 0052exact hf_witness_witness_left
  53. 0053split
  54. 0054exact hf_witness_witness_right_left
  55. 0055split
  56. 0056have heq : N=x1*D
  57. 0057trans D*x1
  58. 0058exact hf_witness_witness_right_right
  59. 0059apply mul_comm
  60. 0060rewrite heq
  61. 0061specialize succ_le_mul_of_two_le_right (x1)
  62. 0062specialize succ_le_mul_of_two_le_right (D)
  63. 0063apply succ_le_mul_of_two_le_right
  64. 0064exact hQpositive
  65. 0065specialize gaussian_search_nonunit_norm_two (d)
  66. 0066specialize gaussian_search_nonunit_norm_two (D)
  67. 0067apply gaussian_search_nonunit_norm_two
  68. 0068exact hD
  69. 0069exact hDpositive
  70. 0070exact hu
  71. 0071intro hqzero
  72. 0072apply hQpositive
  73. 0073specialize gaussian_code_zero_implies_norm_zero (x)
  74. 0074specialize gaussian_code_zero_implies_norm_zero (x1)
  75. 0075apply gaussian_code_zero_implies_norm_zero
  76. 0076exact hf_witness_witness_right_left
  77. 0077exact hqzero