EI0041

eisenstein_euclidean_division_exists

Full constructive Eisenstein Euclidean division: every canonical dividend and nonzero canonical divisor produce actual canonical quotient and remainder, an exact a=bq+r equation, and strict decrease of their actual norms a²-ab+b².

Alpha v34 checked-use · first admitted v28 · 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.

A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ZPairValid(ac) → ZPairValid(bc) → ¬bc = 0 → ∃ x. ∃ y. ∃ z. ∃ n. EEuclideanDivision(ac,bc,x,y,z,n)

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

Definition DAG

ZPairValid(z) · 2ZPairRep(z,ap,an,bp,bn) · 4EEuclideanDivision(a,b,q,r,U,V) · 1EisensteinSignedDivisionRemainder(ap,an,bp,bn,cp,cn,dp,dn,qp,qn,up,un,rp,rn,sp,sn,U,V) · 1

Actual proof prerequisites

gaussian_decode_representation · checked external prerequisitegaussian_representation_zero_iff · checked external prerequisiteeisenstein_signed_euclidean_division_existsgaussian_representation_exists · checked external prerequisiteeisenstein_division_remainder_of_representationseisenstein_norm_of_representation
Original expanded first-order statement 
forall ac bc. (exists ge_real_positive_euclidean_input_dividend ge_real_negative_euclidean_input_dividend ge_imaginary_positive_euclidean_input_dividend ge_imaginary_negative_euclidean_input_dividend. (exists ge_real_code_euclidean_input_dividenddecode ge_imaginary_code_euclidean_input_dividenddecode. (((ac) = ((ge_real_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode)) * S ((ge_real_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode)) + ((ge_imaginary_code_euclidean_input_dividenddecode) + (ge_imaginary_code_euclidean_input_dividenddecode))) /\ (((((ge_real_code_euclidean_input_dividenddecode) = 2 * (ge_real_positive_euclidean_input_dividend) /\ (ge_real_negative_euclidean_input_dividend) = 0) \/ exists ge_signed_half_ge_euclidean_input_dividenddecode_real. (((ge_real_code_euclidean_input_dividenddecode) = 2 * ge_signed_half_ge_euclidean_input_dividenddecode_real + 1 /\ (ge_real_positive_euclidean_input_dividend) = 0) /\ (ge_real_negative_euclidean_input_dividend) = S ge_signed_half_ge_euclidean_input_dividenddecode_real))) /\ ((((ge_imaginary_code_euclidean_input_dividenddecode) = 2 * (ge_imaginary_positive_euclidean_input_dividend) /\ (ge_imaginary_negative_euclidean_input_dividend) = 0) \/ exists ge_signed_half_ge_euclidean_input_dividenddecode_imaginary. (((ge_imaginary_code_euclidean_input_dividenddecode) = 2 * ge_signed_half_ge_euclidean_input_dividenddecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_input_dividend) = 0) /\ (ge_imaginary_negative_euclidean_input_dividend) = S ge_signed_half_ge_euclidean_input_dividenddecode_imaginary))))))) -> (exists ge_real_positive_euclidean_input_divisor ge_real_negative_euclidean_input_divisor ge_imaginary_positive_euclidean_input_divisor ge_imaginary_negative_euclidean_input_divisor. (exists ge_real_code_euclidean_input_divisordecode ge_imaginary_code_euclidean_input_divisordecode. (((bc) = ((ge_real_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode)) * S ((ge_real_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode)) + ((ge_imaginary_code_euclidean_input_divisordecode) + (ge_imaginary_code_euclidean_input_divisordecode))) /\ (((((ge_real_code_euclidean_input_divisordecode) = 2 * (ge_real_positive_euclidean_input_divisor) /\ (ge_real_negative_euclidean_input_divisor) = 0) \/ exists ge_signed_half_ge_euclidean_input_divisordecode_real. (((ge_real_code_euclidean_input_divisordecode) = 2 * ge_signed_half_ge_euclidean_input_divisordecode_real + 1 /\ (ge_real_positive_euclidean_input_divisor) = 0) /\ (ge_real_negative_euclidean_input_divisor) = S ge_signed_half_ge_euclidean_input_divisordecode_real))) /\ ((((ge_imaginary_code_euclidean_input_divisordecode) = 2 * (ge_imaginary_positive_euclidean_input_divisor) /\ (ge_imaginary_negative_euclidean_input_divisor) = 0) \/ exists ge_signed_half_ge_euclidean_input_divisordecode_imaginary. (((ge_imaginary_code_euclidean_input_divisordecode) = 2 * ge_signed_half_ge_euclidean_input_divisordecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_input_divisor) = 0) /\ (ge_imaginary_negative_euclidean_input_divisor) = S ge_signed_half_ge_euclidean_input_divisordecode_imaginary))))))) -> ~(bc = 0) -> exists qc rc U V. (((exists ee_division_product_euclidean_canonical_outputequation. ((exists ee_first_rp_euclidean_canonical_outputequationproduct ee_first_rn_euclidean_canonical_outputequationproduct ee_first_ip_euclidean_canonical_outputequationproduct ee_first_in_euclidean_canonical_outputequationproduct ee_second_rp_euclidean_canonical_outputequationproduct ee_second_rn_euclidean_canonical_outputequationproduct ee_second_ip_euclidean_canonical_outputequationproduct ee_second_in_euclidean_canonical_outputequationproduct. ((exists ge_representation_real_code_euclidean_canonical_outputequationproductfirst ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst. (((bc) = ((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductfirstreal ge_balance_negative_euclidean_canonical_outputequationproductfirstreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductfirstreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductfirstreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstreal) = S ge_signed_half_euclidean_canonical_outputequationproductfirstrealdecode))) /\ ((ee_first_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstreal = (ee_first_rn_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductfirstreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductfirstimaginarydecode))) /\ ((ee_first_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary = (ee_first_in_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclidean_canonical_outputequationproductsecond ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond. (((qc) = ((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductsecondreal ge_balance_negative_euclidean_canonical_outputequationproductsecondreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductsecondreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductsecondreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondreal) = S ge_signed_half_euclidean_canonical_outputequationproductsecondrealdecode))) /\ ((ee_second_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondreal = (ee_second_rn_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductsecondreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductsecondimaginarydecode))) /\ ((ee_second_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary = (ee_second_in_euclidean_canonical_outputequationproduct) + ge_balance_positive_euclidean_canonical_outputequationproductsecondimaginary)))))) /\ (exists ge_representation_real_code_euclidean_canonical_outputequationproductoutput ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput. (((ee_division_product_euclidean_canonical_outputequation) = ((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput)) * S ((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationproductoutputreal ge_balance_negative_euclidean_canonical_outputequationproductoutputreal. (((((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductoutputreal) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationproductoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductoutputreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputreal) = S ge_signed_half_euclidean_canonical_outputequationproductoutputrealdecode))) /\ ((((((((ee_first_rp_euclidean_canonical_outputequationproduct) * (ee_second_rp_euclidean_canonical_outputequationproduct))) + (((ee_first_rn_euclidean_canonical_outputequationproduct) * (ee_second_rn_euclidean_canonical_outputequationproduct))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputreal = (((((((ee_first_rp_euclidean_canonical_outputequationproduct) * (ee_second_rn_euclidean_canonical_outputequationproduct))) + (((ee_first_rn_euclidean_canonical_outputequationproduct) * (ee_second_rp_euclidean_canonical_outputequationproduct))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))))))) + ge_balance_positive_euclidean_canonical_outputequationproductoutputreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationproductoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary) = S ge_signed_half_euclidean_canonical_outputequationproductoutputimaginarydecode))) /\ ((((((((((ee_first_rp_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))) + (((ee_first_rn_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_rp_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_rn_euclidean_canonical_outputequationproduct))))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary = (((((((((ee_first_rp_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))) + (((ee_first_rn_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_rn_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_rp_euclidean_canonical_outputequationproduct))))))) + (((((ee_first_ip_euclidean_canonical_outputequationproduct) * (ee_second_ip_euclidean_canonical_outputequationproduct))) + (((ee_first_in_euclidean_canonical_outputequationproduct) * (ee_second_in_euclidean_canonical_outputequationproduct))))))) + ge_balance_positive_euclidean_canonical_outputequationproductoutputimaginary))))))))) /\ (exists ge_first_rp_euclidean_canonical_outputequationsum ge_first_rn_euclidean_canonical_outputequationsum ge_first_ip_euclidean_canonical_outputequationsum ge_first_in_euclidean_canonical_outputequationsum ge_second_rp_euclidean_canonical_outputequationsum ge_second_rn_euclidean_canonical_outputequationsum ge_second_ip_euclidean_canonical_outputequationsum ge_second_in_euclidean_canonical_outputequationsum. ((exists ge_representation_real_code_euclidean_canonical_outputequationsumfirst ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst. (((ee_division_product_euclidean_canonical_outputequation) = ((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumfirstreal ge_balance_negative_euclidean_canonical_outputequationsumfirstreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumfirstreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumfirstreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstreal) = S ge_signed_half_euclidean_canonical_outputequationsumfirstrealdecode))) /\ ((ge_first_rp_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumfirstreal = (ge_first_rn_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumfirstreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumfirst) = 2 * ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumfirstimaginarydecode))) /\ ((ge_first_ip_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumfirstimaginary = (ge_first_in_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_euclidean_canonical_outputequationsumsecond ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond. (((rc) = ((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumsecondreal ge_balance_negative_euclidean_canonical_outputequationsumsecondreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumsecondreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumsecondreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondreal) = S ge_signed_half_euclidean_canonical_outputequationsumsecondrealdecode))) /\ ((ge_second_rp_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumsecondreal = (ge_second_rn_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumsecondreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumsecond) = 2 * ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumsecondimaginarydecode))) /\ ((ge_second_ip_euclidean_canonical_outputequationsum) + ge_balance_negative_euclidean_canonical_outputequationsumsecondimaginary = (ge_second_in_euclidean_canonical_outputequationsum) + ge_balance_positive_euclidean_canonical_outputequationsumsecondimaginary)))))) /\ (exists ge_representation_real_code_euclidean_canonical_outputequationsumoutput ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput. (((ac) = ((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput)) * S ((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput)) + ((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) + (ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput))) /\ ((exists ge_balance_positive_euclidean_canonical_outputequationsumoutputreal ge_balance_negative_euclidean_canonical_outputequationsumoutputreal. (((((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumoutputreal) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode. (((ge_representation_real_code_euclidean_canonical_outputequationsumoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumoutputreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputreal) = S ge_signed_half_euclidean_canonical_outputequationsumoutputrealdecode))) /\ ((((ge_first_rp_euclidean_canonical_outputequationsum) + (ge_second_rp_euclidean_canonical_outputequationsum))) + ge_balance_negative_euclidean_canonical_outputequationsumoutputreal = (((ge_first_rn_euclidean_canonical_outputequationsum) + (ge_second_rn_euclidean_canonical_outputequationsum))) + ge_balance_positive_euclidean_canonical_outputequationsumoutputreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) = 2 * (ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputequationsumoutput) = 2 * ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary) = S ge_signed_half_euclidean_canonical_outputequationsumoutputimaginarydecode))) /\ ((((ge_first_ip_euclidean_canonical_outputequationsum) + (ge_second_ip_euclidean_canonical_outputequationsum))) + ge_balance_negative_euclidean_canonical_outputequationsumoutputimaginary = (((ge_first_in_euclidean_canonical_outputequationsum) + (ge_second_in_euclidean_canonical_outputequationsum))) + ge_balance_positive_euclidean_canonical_outputequationsumoutputimaginary))))))))))) /\ ((exists ee_norm_rp_euclidean_canonical_outputsmallnorm ee_norm_rn_euclidean_canonical_outputsmallnorm ee_norm_ip_euclidean_canonical_outputsmallnorm ee_norm_in_euclidean_canonical_outputsmallnorm. ((exists ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation. (((rc) = ((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation)) * S ((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation)) + ((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation))) /\ ((exists ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal. (((((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode. (((ge_representation_real_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal) = S ge_signed_half_euclidean_canonical_outputsmallnormrepresentationrealdecode))) /\ ((ee_norm_rp_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal = (ee_norm_rn_euclidean_canonical_outputsmallnorm) + ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputsmallnormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary) = S ge_signed_half_euclidean_canonical_outputsmallnormrepresentationimaginarydecode))) /\ ((ee_norm_ip_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary = (ee_norm_in_euclidean_canonical_outputsmallnorm) + ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_euclidean_canonical_outputsmallnorm) * (ee_norm_rp_euclidean_canonical_outputsmallnorm))) + (((ee_norm_rn_euclidean_canonical_outputsmallnorm) * (ee_norm_rn_euclidean_canonical_outputsmallnorm))))) + (((((ee_norm_ip_euclidean_canonical_outputsmallnorm) * (ee_norm_ip_euclidean_canonical_outputsmallnorm))) + (((ee_norm_in_euclidean_canonical_outputsmallnorm) * (ee_norm_in_euclidean_canonical_outputsmallnorm))))))) + (((((ee_norm_rp_euclidean_canonical_outputsmallnorm) * (ee_norm_in_euclidean_canonical_outputsmallnorm))) + (((ee_norm_rn_euclidean_canonical_outputsmallnorm) * (ee_norm_ip_euclidean_canonical_outputsmallnorm)))))) = ((((((((((ee_norm_rp_euclidean_canonical_outputsmallnorm) * (ee_norm_rn_euclidean_canonical_outputsmallnorm))) + (((ee_norm_rn_euclidean_canonical_outputsmallnorm) * (ee_norm_rp_euclidean_canonical_outputsmallnorm))))) + (((((ee_norm_ip_euclidean_canonical_outputsmallnorm) * (ee_norm_in_euclidean_canonical_outputsmallnorm))) + (((ee_norm_in_euclidean_canonical_outputsmallnorm) * (ee_norm_ip_euclidean_canonical_outputsmallnorm))))))) + (((((ee_norm_rp_euclidean_canonical_outputsmallnorm) * (ee_norm_ip_euclidean_canonical_outputsmallnorm))) + (((ee_norm_rn_euclidean_canonical_outputsmallnorm) * (ee_norm_in_euclidean_canonical_outputsmallnorm))))))) + (U))))) /\ ((exists ee_norm_rp_euclidean_canonical_outputlargenorm ee_norm_rn_euclidean_canonical_outputlargenorm ee_norm_ip_euclidean_canonical_outputlargenorm ee_norm_in_euclidean_canonical_outputlargenorm. ((exists ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation. (((bc) = ((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation)) * S ((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation)) + ((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) + (ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation))) /\ ((exists ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal. (((((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal) = 0) \/ exists ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode. (((ge_representation_real_code_euclidean_canonical_outputlargenormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal) = 0) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal) = S ge_signed_half_euclidean_canonical_outputlargenormrepresentationrealdecode))) /\ ((ee_norm_rp_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal = (ee_norm_rn_euclidean_canonical_outputlargenorm) + ge_balance_positive_euclidean_canonical_outputlargenormrepresentationreal))) /\ (exists ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary. (((((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) = 2 * (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary) = 0) \/ exists ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode. (((ge_representation_imaginary_code_euclidean_canonical_outputlargenormrepresentation) = 2 * ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode + 1 /\ (ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary) = 0) /\ (ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary) = S ge_signed_half_euclidean_canonical_outputlargenormrepresentationimaginarydecode))) /\ ((ee_norm_ip_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary = (ee_norm_in_euclidean_canonical_outputlargenorm) + ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_euclidean_canonical_outputlargenorm) * (ee_norm_rp_euclidean_canonical_outputlargenorm))) + (((ee_norm_rn_euclidean_canonical_outputlargenorm) * (ee_norm_rn_euclidean_canonical_outputlargenorm))))) + (((((ee_norm_ip_euclidean_canonical_outputlargenorm) * (ee_norm_ip_euclidean_canonical_outputlargenorm))) + (((ee_norm_in_euclidean_canonical_outputlargenorm) * (ee_norm_in_euclidean_canonical_outputlargenorm))))))) + (((((ee_norm_rp_euclidean_canonical_outputlargenorm) * (ee_norm_in_euclidean_canonical_outputlargenorm))) + (((ee_norm_rn_euclidean_canonical_outputlargenorm) * (ee_norm_ip_euclidean_canonical_outputlargenorm)))))) = ((((((((((ee_norm_rp_euclidean_canonical_outputlargenorm) * (ee_norm_rn_euclidean_canonical_outputlargenorm))) + (((ee_norm_rn_euclidean_canonical_outputlargenorm) * (ee_norm_rp_euclidean_canonical_outputlargenorm))))) + (((((ee_norm_ip_euclidean_canonical_outputlargenorm) * (ee_norm_in_euclidean_canonical_outputlargenorm))) + (((ee_norm_in_euclidean_canonical_outputlargenorm) * (ee_norm_ip_euclidean_canonical_outputlargenorm))))))) + (((((ee_norm_rp_euclidean_canonical_outputlargenorm) * (ee_norm_ip_euclidean_canonical_outputlargenorm))) + (((ee_norm_rn_euclidean_canonical_outputlargenorm) * (ee_norm_in_euclidean_canonical_outputlargenorm))))))) + (V))))) /\ (exists ee_gap_euclidean_canonical_outputstrict. ee_gap_euclidean_canonical_outputstrict + S (U) = (V))))))

Complete tactic proof in conservative notation

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

133 script commands · 24 reading checkpoints · 7 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)
eisenstein signed euclidean division existseisenstein division remainder of representationseisenstein norm of representation
01Fix variables and assumptionsL1–5

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro hfirst
  4. L4
    intro hsecond
  5. L5
    intro hnonzero
02Separate the logical casesL6–13

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

  1. L6
    cases hfirst
  2. L7
    cases hfirst_witness
  3. L8
    cases hfirst_witness_witness
  4. L9
    cases hfirst_witness_witness_witness
  5. L10
    cases hsecond
  6. L11
    cases hsecond_witness
  7. L12
    cases hsecond_witness_witness
  8. L13
    cases hsecond_witness_witness_witness
03Establish hAL14–21

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

  1. L14
    have hA : ZPairRep(ac,x,x1,x2,x3)Definitions: ZPairRep(ac,x,x1,x2,x3)Original native command in the exact edition
  2. L15
    specialize gaussian_decode_representation ac
  3. L16
    specialize gaussian_decode_representation x
  4. L17
    specialize gaussian_decode_representation x1
  5. L18
    specialize gaussian_decode_representation x2
  6. L19
    specialize gaussian_decode_representation x3
  7. L20
    apply gaussian_decode_representation
  8. L21
    exact hfirst_witness_witness_witness_witness
04Establish hBL22–29

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

  1. L22
    have hB : ZPairRep(bc,x4,x5,x6,x7)Definitions: ZPairRep(bc,x4,x5,x6,x7)Original native command in the exact edition
  2. L23
    specialize gaussian_decode_representation bc
  3. L24
    specialize gaussian_decode_representation x4
  4. L25
    specialize gaussian_decode_representation x5
  5. L26
    specialize gaussian_decode_representation x6
  6. L27
    specialize gaussian_decode_representation x7
  7. L28
    apply gaussian_decode_representation
  8. L29
    exact hsecond_witness_witness_witness_witness
05Establish hzeroL30–37

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

  1. L30
    have hzero : (bc = 0 -> (x4 = x5 /\ x6 = x7)) /\ ((x4 = x5 /\ x6 = x7) -> bc = 0)
  2. L31
    specialize gaussian_representation_zero_iff bc
  3. L32
    specialize gaussian_representation_zero_iff x4
  4. L33
    specialize gaussian_representation_zero_iff x5
  5. L34
    specialize gaussian_representation_zero_iff x6
  6. L35
    specialize gaussian_representation_zero_iff x7
  7. L36
    apply gaussian_representation_zero_iff
  8. L37
    exact hB
06Separate the logical casesL38–38

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

  1. L38
    cases hzero
07Establish hraw_nonzeroL39–43

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

  1. L39
    have hraw_nonzero : ~(x4 = x5 /\ x6 = x7)
  2. L40
    intro hvanishing
  3. L41
    apply hnonzero
  4. L42
    apply hzero_right
  5. L43
    exact hvanishing
08Establish hdivisionL44–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply eisenstein signed euclidean division exists.

  1. L44
    have hdivision : ∃ i. ∃ j. ∃ k. ∃ l. ∃ o. ∃ p. ∃ s. ∃ t. ∃ U. ∃ V. EisensteinSignedDivisionRemainder(x,x1,x2,x3,x4,x5,x6,x7,i,j,k,l,o,p,s,t,U,V)Definitions: EisensteinSignedDivisionRemainder(x,x1,x2,x3,x4,x5,x6,x7,i,j,k,l,o,p,s,t,U,V)Original native command in the exact edition
  2. L45
    specialize eisenstein_signed_euclidean_division_exists x
  3. L46
    specialize eisenstein_signed_euclidean_division_exists x1
  4. L47
    specialize eisenstein_signed_euclidean_division_exists x2
  5. L48
    specialize eisenstein_signed_euclidean_division_exists x3
  6. L49
    specialize eisenstein_signed_euclidean_division_exists x4
  7. L50
    specialize eisenstein_signed_euclidean_division_exists x5
  8. L51
    specialize eisenstein_signed_euclidean_division_exists x6
  9. L52
    specialize eisenstein_signed_euclidean_division_exists x7
  10. L53
    apply eisenstein_signed_euclidean_division_exists
09Use earlier factsL54–54

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

  1. L54
    exact hraw_nonzero
10Separate the logical casesL55–64

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

  1. L55
    cases hdivision
  2. L56
    cases hdivision_witness
  3. L57
    cases hdivision_witness_witness
  4. L58
    cases hdivision_witness_witness_witness
  5. L59
    cases hdivision_witness_witness_witness_witness
  6. L60
    cases hdivision_witness_witness_witness_witness_witness
  7. L61
    cases hdivision_witness_witness_witness_witness_witness_witness
  8. L62
    cases hdivision_witness_witness_witness_witness_witness_witness_witness
  9. L63
    cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness
  10. L64
    cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness
11Separate the logical casesL65–67

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

  1. L65
    cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness
  2. L66
    cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right
  3. L67
    cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right
12Establish hQL68–73

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

  1. L68
    have hQ : ∃ qc. ZPairRep(qc,x8,x9,x10,x11)Definitions: ZPairRep(qc,x8,x9,x10,x11)Original native command in the exact edition
  2. L69
    specialize gaussian_representation_exists x8
  3. L70
    specialize gaussian_representation_exists x9
  4. L71
    specialize gaussian_representation_exists x10
  5. L72
    specialize gaussian_representation_exists x11
  6. L73
    apply gaussian_representation_exists
13Separate the logical casesL74–74

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

  1. L74
    cases hQ
14Establish hRL75–80

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

  1. L75
    have hR : ∃ rc. ZPairRep(rc,x12,x13,x14,x15)Definitions: ZPairRep(rc,x12,x13,x14,x15)Original native command in the exact edition
  2. L76
    specialize gaussian_representation_exists x12
  3. L77
    specialize gaussian_representation_exists x13
  4. L78
    specialize gaussian_representation_exists x14
  5. L79
    specialize gaussian_representation_exists x15
  6. L80
    apply gaussian_representation_exists
15Separate the logical casesL81–81

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

  1. L81
    cases hR
16Construct an explicit witnessL82–85

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

  1. L82
    exists x18
  2. L83
    exists x19
  3. L84
    exists x16
  4. L85
    exists x17
17Separate the logical casesL86–86

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

  1. L86
    split
18Use earlier factsL87–96

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

  1. L87
    specialize eisenstein_division_remainder_of_representations ac
  2. L88
    specialize eisenstein_division_remainder_of_representations bc
  3. L89
    specialize eisenstein_division_remainder_of_representations x18
  4. L90
    specialize eisenstein_division_remainder_of_representations x19
  5. L91
    specialize eisenstein_division_remainder_of_representations x
  6. L92
    specialize eisenstein_division_remainder_of_representations x1
  7. L93
    specialize eisenstein_division_remainder_of_representations x2
  8. L94
    specialize eisenstein_division_remainder_of_representations x3
  9. L95
    specialize eisenstein_division_remainder_of_representations x4
  10. L96
    specialize eisenstein_division_remainder_of_representations x5
19Use earlier factsL97–106

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

  1. L97
    specialize eisenstein_division_remainder_of_representations x6
  2. L98
    specialize eisenstein_division_remainder_of_representations x7
  3. L99
    specialize eisenstein_division_remainder_of_representations x8
  4. L100
    specialize eisenstein_division_remainder_of_representations x9
  5. L101
    specialize eisenstein_division_remainder_of_representations x10
  6. L102
    specialize eisenstein_division_remainder_of_representations x11
  7. L103
    specialize eisenstein_division_remainder_of_representations x12
  8. L104
    specialize eisenstein_division_remainder_of_representations x13
  9. L105
    specialize eisenstein_division_remainder_of_representations x14
  10. L106
    specialize eisenstein_division_remainder_of_representations x15
20Use earlier factsL107–112

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

  1. L107
    apply eisenstein_division_remainder_of_representations
  2. L108
    exact hA
  3. L109
    exact hB
  4. L110
    exact hQ_witness
  5. L111
    exact hR_witness
  6. L112
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
21Separate the logical casesL113–113

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

  1. L113
    split
22Use earlier factsL114–122

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

  1. L114
    specialize eisenstein_norm_of_representation x19
  2. L115
    specialize eisenstein_norm_of_representation x12
  3. L116
    specialize eisenstein_norm_of_representation x13
  4. L117
    specialize eisenstein_norm_of_representation x14
  5. L118
    specialize eisenstein_norm_of_representation x15
  6. L119
    specialize eisenstein_norm_of_representation x16
  7. L120
    apply eisenstein_norm_of_representation
  8. L121
    exact hR_witness
  9. L122
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left
23Separate the logical casesL123–123

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

  1. L123
    split
24Use earlier factsL124–133

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

  1. L124
    specialize eisenstein_norm_of_representation bc
  2. L125
    specialize eisenstein_norm_of_representation x4
  3. L126
    specialize eisenstein_norm_of_representation x5
  4. L127
    specialize eisenstein_norm_of_representation x6
  5. L128
    specialize eisenstein_norm_of_representation x7
  6. L129
    specialize eisenstein_norm_of_representation x17
  7. L130
    apply eisenstein_norm_of_representation
  8. L131
    exact hB
  9. L132
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  10. L133
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 133 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro hfirst
  4. 0004intro hsecond
  5. 0005intro hnonzero
  6. 0006cases hfirst
  7. 0007cases hfirst_witness
  8. 0008cases hfirst_witness_witness
  9. 0009cases hfirst_witness_witness_witness
  10. 0010cases hsecond
  11. 0011cases hsecond_witness
  12. 0012cases hsecond_witness_witness
  13. 0013cases hsecond_witness_witness_witness
  14. 0014have hA : ZPairRep(ac,x,x1,x2,x3)
  15. 0015specialize gaussian_decode_representation ac
  16. 0016specialize gaussian_decode_representation x
  17. 0017specialize gaussian_decode_representation x1
  18. 0018specialize gaussian_decode_representation x2
  19. 0019specialize gaussian_decode_representation x3
  20. 0020apply gaussian_decode_representation
  21. 0021exact hfirst_witness_witness_witness_witness
  22. 0022have hB : ZPairRep(bc,x4,x5,x6,x7)
  23. 0023specialize gaussian_decode_representation bc
  24. 0024specialize gaussian_decode_representation x4
  25. 0025specialize gaussian_decode_representation x5
  26. 0026specialize gaussian_decode_representation x6
  27. 0027specialize gaussian_decode_representation x7
  28. 0028apply gaussian_decode_representation
  29. 0029exact hsecond_witness_witness_witness_witness
  30. 0030have hzero : (bc = 0 -> (x4 = x5 /\ x6 = x7)) /\ ((x4 = x5 /\ x6 = x7) -> bc = 0)
  31. 0031specialize gaussian_representation_zero_iff bc
  32. 0032specialize gaussian_representation_zero_iff x4
  33. 0033specialize gaussian_representation_zero_iff x5
  34. 0034specialize gaussian_representation_zero_iff x6
  35. 0035specialize gaussian_representation_zero_iff x7
  36. 0036apply gaussian_representation_zero_iff
  37. 0037exact hB
  38. 0038cases hzero
  39. 0039have hraw_nonzero : ~(x4 = x5 /\ x6 = x7)
  40. 0040intro hvanishing
  41. 0041apply hnonzero
  42. 0042apply hzero_right
  43. 0043exact hvanishing
  44. 0044have hdivision : ∃ i. ∃ j. ∃ k. ∃ l. ∃ o. ∃ p. ∃ s. ∃ t. ∃ U. ∃ V. EisensteinSignedDivisionRemainder(x,x1,x2,x3,x4,x5,x6,x7,i,j,k,l,o,p,s,t,U,V)
  45. 0045specialize eisenstein_signed_euclidean_division_exists x
  46. 0046specialize eisenstein_signed_euclidean_division_exists x1
  47. 0047specialize eisenstein_signed_euclidean_division_exists x2
  48. 0048specialize eisenstein_signed_euclidean_division_exists x3
  49. 0049specialize eisenstein_signed_euclidean_division_exists x4
  50. 0050specialize eisenstein_signed_euclidean_division_exists x5
  51. 0051specialize eisenstein_signed_euclidean_division_exists x6
  52. 0052specialize eisenstein_signed_euclidean_division_exists x7
  53. 0053apply eisenstein_signed_euclidean_division_exists
  54. 0054exact hraw_nonzero
  55. 0055cases hdivision
  56. 0056cases hdivision_witness
  57. 0057cases hdivision_witness_witness
  58. 0058cases hdivision_witness_witness_witness
  59. 0059cases hdivision_witness_witness_witness_witness
  60. 0060cases hdivision_witness_witness_witness_witness_witness
  61. 0061cases hdivision_witness_witness_witness_witness_witness_witness
  62. 0062cases hdivision_witness_witness_witness_witness_witness_witness_witness
  63. 0063cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness
  64. 0064cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness
  65. 0065cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness
  66. 0066cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right
  67. 0067cases hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right
  68. 0068have hQ : ∃ qc. ZPairRep(qc,x8,x9,x10,x11)
  69. 0069specialize gaussian_representation_exists x8
  70. 0070specialize gaussian_representation_exists x9
  71. 0071specialize gaussian_representation_exists x10
  72. 0072specialize gaussian_representation_exists x11
  73. 0073apply gaussian_representation_exists
  74. 0074cases hQ
  75. 0075have hR : ∃ rc. ZPairRep(rc,x12,x13,x14,x15)
  76. 0076specialize gaussian_representation_exists x12
  77. 0077specialize gaussian_representation_exists x13
  78. 0078specialize gaussian_representation_exists x14
  79. 0079specialize gaussian_representation_exists x15
  80. 0080apply gaussian_representation_exists
  81. 0081cases hR
  82. 0082exists x18
  83. 0083exists x19
  84. 0084exists x16
  85. 0085exists x17
  86. 0086split
  87. 0087specialize eisenstein_division_remainder_of_representations ac
  88. 0088specialize eisenstein_division_remainder_of_representations bc
  89. 0089specialize eisenstein_division_remainder_of_representations x18
  90. 0090specialize eisenstein_division_remainder_of_representations x19
  91. 0091specialize eisenstein_division_remainder_of_representations x
  92. 0092specialize eisenstein_division_remainder_of_representations x1
  93. 0093specialize eisenstein_division_remainder_of_representations x2
  94. 0094specialize eisenstein_division_remainder_of_representations x3
  95. 0095specialize eisenstein_division_remainder_of_representations x4
  96. 0096specialize eisenstein_division_remainder_of_representations x5
  97. 0097specialize eisenstein_division_remainder_of_representations x6
  98. 0098specialize eisenstein_division_remainder_of_representations x7
  99. 0099specialize eisenstein_division_remainder_of_representations x8
  100. 0100specialize eisenstein_division_remainder_of_representations x9
  101. 0101specialize eisenstein_division_remainder_of_representations x10
  102. 0102specialize eisenstein_division_remainder_of_representations x11
  103. 0103specialize eisenstein_division_remainder_of_representations x12
  104. 0104specialize eisenstein_division_remainder_of_representations x13
  105. 0105specialize eisenstein_division_remainder_of_representations x14
  106. 0106specialize eisenstein_division_remainder_of_representations x15
  107. 0107apply eisenstein_division_remainder_of_representations
  108. 0108exact hA
  109. 0109exact hB
  110. 0110exact hQ_witness
  111. 0111exact hR_witness
  112. 0112exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
  113. 0113split
  114. 0114specialize eisenstein_norm_of_representation x19
  115. 0115specialize eisenstein_norm_of_representation x12
  116. 0116specialize eisenstein_norm_of_representation x13
  117. 0117specialize eisenstein_norm_of_representation x14
  118. 0118specialize eisenstein_norm_of_representation x15
  119. 0119specialize eisenstein_norm_of_representation x16
  120. 0120apply eisenstein_norm_of_representation
  121. 0121exact hR_witness
  122. 0122exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  123. 0123split
  124. 0124specialize eisenstein_norm_of_representation bc
  125. 0125specialize eisenstein_norm_of_representation x4
  126. 0126specialize eisenstein_norm_of_representation x5
  127. 0127specialize eisenstein_norm_of_representation x6
  128. 0128specialize eisenstein_norm_of_representation x7
  129. 0129specialize eisenstein_norm_of_representation x17
  130. 0130apply eisenstein_norm_of_representation
  131. 0131exact hB
  132. 0132exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  133. 0133exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right