GI005D

gaussian_euclidean_division_exists

Full constructive Gaussian Euclidean division: every canonical dividend and nonzero canonical divisor produce actual canonical quotient and remainder codes satisfying a=bq+r and strict decrease of their actual squared norms.

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ ac. ∀ bc. ZPairValid(ac) → ZPairValid(bc) → ¬bc = 0 → ∃ x. ∃ y. ∃ z. ∃ n. GEuclideanDivision(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) · 4GaussianSignedDivisionRemainder(ap,an,bp,bn,cp,cn,dp,dn,qp,qn,up,un,rp,rn,sp,sn,U,V) · 1GEuclideanDivision(a,b,q,r,U,V) · 1

Actual proof prerequisites

gaussian_decode_representationgaussian_representation_zero_iffgaussian_signed_euclidean_division_existsgaussian_representation_existsgaussian_representation_is_gaussiangaussian_division_remainder_of_representationsgaussian_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 ge_real_positive_euclidean_canonical_outputquotient ge_real_negative_euclidean_canonical_outputquotient ge_imaginary_positive_euclidean_canonical_outputquotient ge_imaginary_negative_euclidean_canonical_outputquotient. (exists ge_real_code_euclidean_canonical_outputquotientdecode ge_imaginary_code_euclidean_canonical_outputquotientdecode. (((qc) = ((ge_real_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode)) * S ((ge_real_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode)) + ((ge_imaginary_code_euclidean_canonical_outputquotientdecode) + (ge_imaginary_code_euclidean_canonical_outputquotientdecode))) /\ (((((ge_real_code_euclidean_canonical_outputquotientdecode) = 2 * (ge_real_positive_euclidean_canonical_outputquotient) /\ (ge_real_negative_euclidean_canonical_outputquotient) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real. (((ge_real_code_euclidean_canonical_outputquotientdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real + 1 /\ (ge_real_positive_euclidean_canonical_outputquotient) = 0) /\ (ge_real_negative_euclidean_canonical_outputquotient) = S ge_signed_half_ge_euclidean_canonical_outputquotientdecode_real))) /\ ((((ge_imaginary_code_euclidean_canonical_outputquotientdecode) = 2 * (ge_imaginary_positive_euclidean_canonical_outputquotient) /\ (ge_imaginary_negative_euclidean_canonical_outputquotient) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary. (((ge_imaginary_code_euclidean_canonical_outputquotientdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_canonical_outputquotient) = 0) /\ (ge_imaginary_negative_euclidean_canonical_outputquotient) = S ge_signed_half_ge_euclidean_canonical_outputquotientdecode_imaginary))))))) /\ ((exists ge_real_positive_euclidean_canonical_outputremainder ge_real_negative_euclidean_canonical_outputremainder ge_imaginary_positive_euclidean_canonical_outputremainder ge_imaginary_negative_euclidean_canonical_outputremainder. (exists ge_real_code_euclidean_canonical_outputremainderdecode ge_imaginary_code_euclidean_canonical_outputremainderdecode. (((rc) = ((ge_real_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode)) * S ((ge_real_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode)) + ((ge_imaginary_code_euclidean_canonical_outputremainderdecode) + (ge_imaginary_code_euclidean_canonical_outputremainderdecode))) /\ (((((ge_real_code_euclidean_canonical_outputremainderdecode) = 2 * (ge_real_positive_euclidean_canonical_outputremainder) /\ (ge_real_negative_euclidean_canonical_outputremainder) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real. (((ge_real_code_euclidean_canonical_outputremainderdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real + 1 /\ (ge_real_positive_euclidean_canonical_outputremainder) = 0) /\ (ge_real_negative_euclidean_canonical_outputremainder) = S ge_signed_half_ge_euclidean_canonical_outputremainderdecode_real))) /\ ((((ge_imaginary_code_euclidean_canonical_outputremainderdecode) = 2 * (ge_imaginary_positive_euclidean_canonical_outputremainder) /\ (ge_imaginary_negative_euclidean_canonical_outputremainder) = 0) \/ exists ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary. (((ge_imaginary_code_euclidean_canonical_outputremainderdecode) = 2 * ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary + 1 /\ (ge_imaginary_positive_euclidean_canonical_outputremainder) = 0) /\ (ge_imaginary_negative_euclidean_canonical_outputremainder) = S ge_signed_half_ge_euclidean_canonical_outputremainderdecode_imaginary))))))) /\ ((exists ge_division_product_euclidean_canonical_outputequation. ((exists ge_first_rp_euclidean_canonical_outputequationproduct ge_first_rn_euclidean_canonical_outputequationproduct ge_first_ip_euclidean_canonical_outputequationproduct ge_first_in_euclidean_canonical_outputequationproduct ge_second_rp_euclidean_canonical_outputequationproduct ge_second_rn_euclidean_canonical_outputequationproduct ge_second_ip_euclidean_canonical_outputequationproduct ge_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))) /\ ((ge_first_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstreal = (ge_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))) /\ ((ge_first_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductfirstimaginary = (ge_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))) /\ ((ge_second_rp_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondreal = (ge_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))) /\ ((ge_second_ip_euclidean_canonical_outputequationproduct) + ge_balance_negative_euclidean_canonical_outputequationproductsecondimaginary = (ge_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. (((ge_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))) /\ ((((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputreal = (((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_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))) /\ ((((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_rp_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))))))) + ge_balance_negative_euclidean_canonical_outputequationproductoutputimaginary = (((((((ge_first_rp_euclidean_canonical_outputequationproduct) * (ge_second_in_euclidean_canonical_outputequationproduct))) + (((ge_first_rn_euclidean_canonical_outputequationproduct) * (ge_second_ip_euclidean_canonical_outputequationproduct))))) + (((((ge_first_ip_euclidean_canonical_outputequationproduct) * (ge_second_rn_euclidean_canonical_outputequationproduct))) + (((ge_first_in_euclidean_canonical_outputequationproduct) * (ge_second_rp_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. (((ge_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 ge_norm_rp_euclidean_canonical_outputsmallnorm ge_norm_rn_euclidean_canonical_outputsmallnorm ge_norm_ip_euclidean_canonical_outputsmallnorm ge_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))) /\ ((ge_norm_rp_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationreal = (ge_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))) /\ ((ge_norm_ip_euclidean_canonical_outputsmallnorm) + ge_balance_negative_euclidean_canonical_outputsmallnormrepresentationimaginary = (ge_norm_in_euclidean_canonical_outputsmallnorm) + ge_balance_positive_euclidean_canonical_outputsmallnormrepresentationimaginary)))))) /\ (exists ge_real_square_euclidean_canonical_outputsmallnormsquare ge_imaginary_square_euclidean_canonical_outputsmallnormsquare. ((((((ge_norm_rp_euclidean_canonical_outputsmallnorm) * (ge_norm_rp_euclidean_canonical_outputsmallnorm))) + (((ge_norm_rn_euclidean_canonical_outputsmallnorm) * (ge_norm_rn_euclidean_canonical_outputsmallnorm)))) = ((ge_real_square_euclidean_canonical_outputsmallnormsquare) + (((((ge_norm_rp_euclidean_canonical_outputsmallnorm) * (ge_norm_rn_euclidean_canonical_outputsmallnorm))) + (((ge_norm_rn_euclidean_canonical_outputsmallnorm) * (ge_norm_rp_euclidean_canonical_outputsmallnorm))))))) /\ ((((((ge_norm_ip_euclidean_canonical_outputsmallnorm) * (ge_norm_ip_euclidean_canonical_outputsmallnorm))) + (((ge_norm_in_euclidean_canonical_outputsmallnorm) * (ge_norm_in_euclidean_canonical_outputsmallnorm)))) = ((ge_imaginary_square_euclidean_canonical_outputsmallnormsquare) + (((((ge_norm_ip_euclidean_canonical_outputsmallnorm) * (ge_norm_in_euclidean_canonical_outputsmallnorm))) + (((ge_norm_in_euclidean_canonical_outputsmallnorm) * (ge_norm_ip_euclidean_canonical_outputsmallnorm))))))) /\ ((U) = ge_real_square_euclidean_canonical_outputsmallnormsquare + ge_imaginary_square_euclidean_canonical_outputsmallnormsquare)))))) /\ ((exists ge_norm_rp_euclidean_canonical_outputlargenorm ge_norm_rn_euclidean_canonical_outputlargenorm ge_norm_ip_euclidean_canonical_outputlargenorm ge_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))) /\ ((ge_norm_rp_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationreal = (ge_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))) /\ ((ge_norm_ip_euclidean_canonical_outputlargenorm) + ge_balance_negative_euclidean_canonical_outputlargenormrepresentationimaginary = (ge_norm_in_euclidean_canonical_outputlargenorm) + ge_balance_positive_euclidean_canonical_outputlargenormrepresentationimaginary)))))) /\ (exists ge_real_square_euclidean_canonical_outputlargenormsquare ge_imaginary_square_euclidean_canonical_outputlargenormsquare. ((((((ge_norm_rp_euclidean_canonical_outputlargenorm) * (ge_norm_rp_euclidean_canonical_outputlargenorm))) + (((ge_norm_rn_euclidean_canonical_outputlargenorm) * (ge_norm_rn_euclidean_canonical_outputlargenorm)))) = ((ge_real_square_euclidean_canonical_outputlargenormsquare) + (((((ge_norm_rp_euclidean_canonical_outputlargenorm) * (ge_norm_rn_euclidean_canonical_outputlargenorm))) + (((ge_norm_rn_euclidean_canonical_outputlargenorm) * (ge_norm_rp_euclidean_canonical_outputlargenorm))))))) /\ ((((((ge_norm_ip_euclidean_canonical_outputlargenorm) * (ge_norm_ip_euclidean_canonical_outputlargenorm))) + (((ge_norm_in_euclidean_canonical_outputlargenorm) * (ge_norm_in_euclidean_canonical_outputlargenorm)))) = ((ge_imaginary_square_euclidean_canonical_outputlargenormsquare) + (((((ge_norm_ip_euclidean_canonical_outputlargenorm) * (ge_norm_in_euclidean_canonical_outputlargenorm))) + (((ge_norm_in_euclidean_canonical_outputlargenorm) * (ge_norm_ip_euclidean_canonical_outputlargenorm))))))) /\ ((V) = ge_real_square_euclidean_canonical_outputlargenormsquare + ge_imaginary_square_euclidean_canonical_outputlargenormsquare)))))) /\ (exists ge_gap_euclidean_canonical_outputstrict. ge_gap_euclidean_canonical_outputstrict + S (U) = (V))))))))

Complete tactic proof in conservative notation

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

149 script commands · 28 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 (7)
gaussian decode representationgaussian representation zero iffgaussian signed euclidean division existsgaussian representation existsgaussian representation is gaussiangaussian division remainder of representationsgaussian 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 gaussian signed euclidean division exists.

  1. L44
    have hdivision : ∃ i. ∃ j. ∃ k. ∃ l. ∃ o. ∃ p. ∃ s. ∃ t. ∃ U. ∃ V. GaussianSignedDivisionRemainder(x,x1,x2,x3,x4,x5,x6,x7,i,j,k,l,o,p,s,t,U,V)Definitions: GaussianSignedDivisionRemainder(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 gaussian_signed_euclidean_division_exists x
  3. L46
    specialize gaussian_signed_euclidean_division_exists x1
  4. L47
    specialize gaussian_signed_euclidean_division_exists x2
  5. L48
    specialize gaussian_signed_euclidean_division_exists x3
  6. L49
    specialize gaussian_signed_euclidean_division_exists x4
  7. L50
    specialize gaussian_signed_euclidean_division_exists x5
  8. L51
    specialize gaussian_signed_euclidean_division_exists x6
  9. L52
    specialize gaussian_signed_euclidean_division_exists x7
  10. L53
    apply gaussian_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–93

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

  1. L87
    specialize gaussian_representation_is_gaussian x18
  2. L88
    specialize gaussian_representation_is_gaussian x8
  3. L89
    specialize gaussian_representation_is_gaussian x9
  4. L90
    specialize gaussian_representation_is_gaussian x10
  5. L91
    specialize gaussian_representation_is_gaussian x11
  6. L92
    apply gaussian_representation_is_gaussian
  7. L93
    exact hQ_witness
19Separate the logical casesL94–94

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

  1. L94
    split
20Use earlier factsL95–101

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

  1. L95
    specialize gaussian_representation_is_gaussian x19
  2. L96
    specialize gaussian_representation_is_gaussian x12
  3. L97
    specialize gaussian_representation_is_gaussian x13
  4. L98
    specialize gaussian_representation_is_gaussian x14
  5. L99
    specialize gaussian_representation_is_gaussian x15
  6. L100
    apply gaussian_representation_is_gaussian
  7. L101
    exact hR_witness
21Separate the logical casesL102–102

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

  1. L102
    split
22Use earlier factsL103–112

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

  1. L103
    specialize gaussian_division_remainder_of_representations ac
  2. L104
    specialize gaussian_division_remainder_of_representations bc
  3. L105
    specialize gaussian_division_remainder_of_representations x18
  4. L106
    specialize gaussian_division_remainder_of_representations x19
  5. L107
    specialize gaussian_division_remainder_of_representations x
  6. L108
    specialize gaussian_division_remainder_of_representations x1
  7. L109
    specialize gaussian_division_remainder_of_representations x2
  8. L110
    specialize gaussian_division_remainder_of_representations x3
  9. L111
    specialize gaussian_division_remainder_of_representations x4
  10. L112
    specialize gaussian_division_remainder_of_representations x5
23Use earlier factsL113–122

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

  1. L113
    specialize gaussian_division_remainder_of_representations x6
  2. L114
    specialize gaussian_division_remainder_of_representations x7
  3. L115
    specialize gaussian_division_remainder_of_representations x8
  4. L116
    specialize gaussian_division_remainder_of_representations x9
  5. L117
    specialize gaussian_division_remainder_of_representations x10
  6. L118
    specialize gaussian_division_remainder_of_representations x11
  7. L119
    specialize gaussian_division_remainder_of_representations x12
  8. L120
    specialize gaussian_division_remainder_of_representations x13
  9. L121
    specialize gaussian_division_remainder_of_representations x14
  10. L122
    specialize gaussian_division_remainder_of_representations x15
24Use earlier factsL123–128

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

  1. L123
    apply gaussian_division_remainder_of_representations
  2. L124
    exact hA
  3. L125
    exact hB
  4. L126
    exact hQ_witness
  5. L127
    exact hR_witness
  6. L128
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
25Separate the logical casesL129–129

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

  1. L129
    split
26Use earlier factsL130–138

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

  1. L130
    specialize gaussian_norm_of_representation x19
  2. L131
    specialize gaussian_norm_of_representation x12
  3. L132
    specialize gaussian_norm_of_representation x13
  4. L133
    specialize gaussian_norm_of_representation x14
  5. L134
    specialize gaussian_norm_of_representation x15
  6. L135
    specialize gaussian_norm_of_representation x16
  7. L136
    apply gaussian_norm_of_representation
  8. L137
    exact hR_witness
  9. L138
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left
27Separate the logical casesL139–139

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

  1. L139
    split
28Use earlier factsL140–149

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

  1. L140
    specialize gaussian_norm_of_representation bc
  2. L141
    specialize gaussian_norm_of_representation x4
  3. L142
    specialize gaussian_norm_of_representation x5
  4. L143
    specialize gaussian_norm_of_representation x6
  5. L144
    specialize gaussian_norm_of_representation x7
  6. L145
    specialize gaussian_norm_of_representation x17
  7. L146
    apply gaussian_norm_of_representation
  8. L147
    exact hB
  9. L148
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  10. L149
    exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 149 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. GaussianSignedDivisionRemainder(x,x1,x2,x3,x4,x5,x6,x7,i,j,k,l,o,p,s,t,U,V)
  45. 0045specialize gaussian_signed_euclidean_division_exists x
  46. 0046specialize gaussian_signed_euclidean_division_exists x1
  47. 0047specialize gaussian_signed_euclidean_division_exists x2
  48. 0048specialize gaussian_signed_euclidean_division_exists x3
  49. 0049specialize gaussian_signed_euclidean_division_exists x4
  50. 0050specialize gaussian_signed_euclidean_division_exists x5
  51. 0051specialize gaussian_signed_euclidean_division_exists x6
  52. 0052specialize gaussian_signed_euclidean_division_exists x7
  53. 0053apply gaussian_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 gaussian_representation_is_gaussian x18
  88. 0088specialize gaussian_representation_is_gaussian x8
  89. 0089specialize gaussian_representation_is_gaussian x9
  90. 0090specialize gaussian_representation_is_gaussian x10
  91. 0091specialize gaussian_representation_is_gaussian x11
  92. 0092apply gaussian_representation_is_gaussian
  93. 0093exact hQ_witness
  94. 0094split
  95. 0095specialize gaussian_representation_is_gaussian x19
  96. 0096specialize gaussian_representation_is_gaussian x12
  97. 0097specialize gaussian_representation_is_gaussian x13
  98. 0098specialize gaussian_representation_is_gaussian x14
  99. 0099specialize gaussian_representation_is_gaussian x15
  100. 0100apply gaussian_representation_is_gaussian
  101. 0101exact hR_witness
  102. 0102split
  103. 0103specialize gaussian_division_remainder_of_representations ac
  104. 0104specialize gaussian_division_remainder_of_representations bc
  105. 0105specialize gaussian_division_remainder_of_representations x18
  106. 0106specialize gaussian_division_remainder_of_representations x19
  107. 0107specialize gaussian_division_remainder_of_representations x
  108. 0108specialize gaussian_division_remainder_of_representations x1
  109. 0109specialize gaussian_division_remainder_of_representations x2
  110. 0110specialize gaussian_division_remainder_of_representations x3
  111. 0111specialize gaussian_division_remainder_of_representations x4
  112. 0112specialize gaussian_division_remainder_of_representations x5
  113. 0113specialize gaussian_division_remainder_of_representations x6
  114. 0114specialize gaussian_division_remainder_of_representations x7
  115. 0115specialize gaussian_division_remainder_of_representations x8
  116. 0116specialize gaussian_division_remainder_of_representations x9
  117. 0117specialize gaussian_division_remainder_of_representations x10
  118. 0118specialize gaussian_division_remainder_of_representations x11
  119. 0119specialize gaussian_division_remainder_of_representations x12
  120. 0120specialize gaussian_division_remainder_of_representations x13
  121. 0121specialize gaussian_division_remainder_of_representations x14
  122. 0122specialize gaussian_division_remainder_of_representations x15
  123. 0123apply gaussian_division_remainder_of_representations
  124. 0124exact hA
  125. 0125exact hB
  126. 0126exact hQ_witness
  127. 0127exact hR_witness
  128. 0128exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_left
  129. 0129split
  130. 0130specialize gaussian_norm_of_representation x19
  131. 0131specialize gaussian_norm_of_representation x12
  132. 0132specialize gaussian_norm_of_representation x13
  133. 0133specialize gaussian_norm_of_representation x14
  134. 0134specialize gaussian_norm_of_representation x15
  135. 0135specialize gaussian_norm_of_representation x16
  136. 0136apply gaussian_norm_of_representation
  137. 0137exact hR_witness
  138. 0138exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  139. 0139split
  140. 0140specialize gaussian_norm_of_representation bc
  141. 0141specialize gaussian_norm_of_representation x4
  142. 0142specialize gaussian_norm_of_representation x5
  143. 0143specialize gaussian_norm_of_representation x6
  144. 0144specialize gaussian_norm_of_representation x7
  145. 0145specialize gaussian_norm_of_representation x17
  146. 0146apply gaussian_norm_of_representation
  147. 0147exact hB
  148. 0148exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_left
  149. 0149exact hdivision_witness_witness_witness_witness_witness_witness_witness_witness_witness_witness_right_right_right