EI0040

eisenstein_division_remainder_of_representations

An actual signed-coordinate a=bq+r equation constructs the genuine canonical Eisenstein product-and-sum graph.

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. ∀ qc. ∀ rc. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ∀ i. ∀ j. ∀ k. ∀ l. ∀ o. ∀ p. ∀ s. ∀ t. ZPairRep(ac,a,b,c,d) → ZPairRep(bc,e,f,g,h) → ZPairRep(qc,i,j,k,l) → ZPairRep(rc,o,p,s,t) → e · i + f · j + (g · l + h · k) + o + b = a + (e · j + f · i + (g · k + h · l) + p) ∧ e · k + f · l + (g · i + h · j) + (g · l + h · k) + s + d = c + (e · l + f · k + (g · j + h · i) + (g · k + h · l) + t) → EDivRem(ac,bc,qc,rc)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 5EDivRem(a,b,q,r) · 1

Actual proof prerequisites

gaussian_representation_exists · checked external prerequisiteeisenstein_multiply_of_representationsgaussian_add_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_equal_symmetric · checked external prerequisite
Original expanded first-order statement 
forall ac bc qc rc a b c d e f g h i j k l o p s t. (exists ge_representation_real_code_equation_first_rep ge_representation_imaginary_code_equation_first_rep. (((ac) = ((ge_representation_real_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep)) * S ((ge_representation_real_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep)) + ((ge_representation_imaginary_code_equation_first_rep) + (ge_representation_imaginary_code_equation_first_rep))) /\ ((exists ge_balance_positive_equation_first_repreal ge_balance_negative_equation_first_repreal. (((((ge_representation_real_code_equation_first_rep) = 2 * (ge_balance_positive_equation_first_repreal) /\ (ge_balance_negative_equation_first_repreal) = 0) \/ exists ge_signed_half_equation_first_reprealdecode. (((ge_representation_real_code_equation_first_rep) = 2 * ge_signed_half_equation_first_reprealdecode + 1 /\ (ge_balance_positive_equation_first_repreal) = 0) /\ (ge_balance_negative_equation_first_repreal) = S ge_signed_half_equation_first_reprealdecode))) /\ ((a) + ge_balance_negative_equation_first_repreal = (b) + ge_balance_positive_equation_first_repreal))) /\ (exists ge_balance_positive_equation_first_repimaginary ge_balance_negative_equation_first_repimaginary. (((((ge_representation_imaginary_code_equation_first_rep) = 2 * (ge_balance_positive_equation_first_repimaginary) /\ (ge_balance_negative_equation_first_repimaginary) = 0) \/ exists ge_signed_half_equation_first_repimaginarydecode. (((ge_representation_imaginary_code_equation_first_rep) = 2 * ge_signed_half_equation_first_repimaginarydecode + 1 /\ (ge_balance_positive_equation_first_repimaginary) = 0) /\ (ge_balance_negative_equation_first_repimaginary) = S ge_signed_half_equation_first_repimaginarydecode))) /\ ((c) + ge_balance_negative_equation_first_repimaginary = (d) + ge_balance_positive_equation_first_repimaginary)))))) -> (exists ge_representation_real_code_equation_second_rep ge_representation_imaginary_code_equation_second_rep. (((bc) = ((ge_representation_real_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep)) * S ((ge_representation_real_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep)) + ((ge_representation_imaginary_code_equation_second_rep) + (ge_representation_imaginary_code_equation_second_rep))) /\ ((exists ge_balance_positive_equation_second_repreal ge_balance_negative_equation_second_repreal. (((((ge_representation_real_code_equation_second_rep) = 2 * (ge_balance_positive_equation_second_repreal) /\ (ge_balance_negative_equation_second_repreal) = 0) \/ exists ge_signed_half_equation_second_reprealdecode. (((ge_representation_real_code_equation_second_rep) = 2 * ge_signed_half_equation_second_reprealdecode + 1 /\ (ge_balance_positive_equation_second_repreal) = 0) /\ (ge_balance_negative_equation_second_repreal) = S ge_signed_half_equation_second_reprealdecode))) /\ ((e) + ge_balance_negative_equation_second_repreal = (f) + ge_balance_positive_equation_second_repreal))) /\ (exists ge_balance_positive_equation_second_repimaginary ge_balance_negative_equation_second_repimaginary. (((((ge_representation_imaginary_code_equation_second_rep) = 2 * (ge_balance_positive_equation_second_repimaginary) /\ (ge_balance_negative_equation_second_repimaginary) = 0) \/ exists ge_signed_half_equation_second_repimaginarydecode. (((ge_representation_imaginary_code_equation_second_rep) = 2 * ge_signed_half_equation_second_repimaginarydecode + 1 /\ (ge_balance_positive_equation_second_repimaginary) = 0) /\ (ge_balance_negative_equation_second_repimaginary) = S ge_signed_half_equation_second_repimaginarydecode))) /\ ((g) + ge_balance_negative_equation_second_repimaginary = (h) + ge_balance_positive_equation_second_repimaginary)))))) -> (exists ge_representation_real_code_equation_quotient_rep ge_representation_imaginary_code_equation_quotient_rep. (((qc) = ((ge_representation_real_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep)) * S ((ge_representation_real_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep)) + ((ge_representation_imaginary_code_equation_quotient_rep) + (ge_representation_imaginary_code_equation_quotient_rep))) /\ ((exists ge_balance_positive_equation_quotient_repreal ge_balance_negative_equation_quotient_repreal. (((((ge_representation_real_code_equation_quotient_rep) = 2 * (ge_balance_positive_equation_quotient_repreal) /\ (ge_balance_negative_equation_quotient_repreal) = 0) \/ exists ge_signed_half_equation_quotient_reprealdecode. (((ge_representation_real_code_equation_quotient_rep) = 2 * ge_signed_half_equation_quotient_reprealdecode + 1 /\ (ge_balance_positive_equation_quotient_repreal) = 0) /\ (ge_balance_negative_equation_quotient_repreal) = S ge_signed_half_equation_quotient_reprealdecode))) /\ ((i) + ge_balance_negative_equation_quotient_repreal = (j) + ge_balance_positive_equation_quotient_repreal))) /\ (exists ge_balance_positive_equation_quotient_repimaginary ge_balance_negative_equation_quotient_repimaginary. (((((ge_representation_imaginary_code_equation_quotient_rep) = 2 * (ge_balance_positive_equation_quotient_repimaginary) /\ (ge_balance_negative_equation_quotient_repimaginary) = 0) \/ exists ge_signed_half_equation_quotient_repimaginarydecode. (((ge_representation_imaginary_code_equation_quotient_rep) = 2 * ge_signed_half_equation_quotient_repimaginarydecode + 1 /\ (ge_balance_positive_equation_quotient_repimaginary) = 0) /\ (ge_balance_negative_equation_quotient_repimaginary) = S ge_signed_half_equation_quotient_repimaginarydecode))) /\ ((k) + ge_balance_negative_equation_quotient_repimaginary = (l) + ge_balance_positive_equation_quotient_repimaginary)))))) -> (exists ge_representation_real_code_equation_remainder_rep ge_representation_imaginary_code_equation_remainder_rep. (((rc) = ((ge_representation_real_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep)) * S ((ge_representation_real_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep)) + ((ge_representation_imaginary_code_equation_remainder_rep) + (ge_representation_imaginary_code_equation_remainder_rep))) /\ ((exists ge_balance_positive_equation_remainder_repreal ge_balance_negative_equation_remainder_repreal. (((((ge_representation_real_code_equation_remainder_rep) = 2 * (ge_balance_positive_equation_remainder_repreal) /\ (ge_balance_negative_equation_remainder_repreal) = 0) \/ exists ge_signed_half_equation_remainder_reprealdecode. (((ge_representation_real_code_equation_remainder_rep) = 2 * ge_signed_half_equation_remainder_reprealdecode + 1 /\ (ge_balance_positive_equation_remainder_repreal) = 0) /\ (ge_balance_negative_equation_remainder_repreal) = S ge_signed_half_equation_remainder_reprealdecode))) /\ ((o) + ge_balance_negative_equation_remainder_repreal = (p) + ge_balance_positive_equation_remainder_repreal))) /\ (exists ge_balance_positive_equation_remainder_repimaginary ge_balance_negative_equation_remainder_repimaginary. (((((ge_representation_imaginary_code_equation_remainder_rep) = 2 * (ge_balance_positive_equation_remainder_repimaginary) /\ (ge_balance_negative_equation_remainder_repimaginary) = 0) \/ exists ge_signed_half_equation_remainder_repimaginarydecode. (((ge_representation_imaginary_code_equation_remainder_rep) = 2 * ge_signed_half_equation_remainder_repimaginarydecode + 1 /\ (ge_balance_positive_equation_remainder_repimaginary) = 0) /\ (ge_balance_negative_equation_remainder_repimaginary) = S ge_signed_half_equation_remainder_repimaginarydecode))) /\ ((s) + ge_balance_negative_equation_remainder_repimaginary = (t) + ge_balance_positive_equation_remainder_repimaginary)))))) -> (((((((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))) + (b)) = ((a) + (((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))))) /\ (((((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))) + (s))) + (d)) = ((c) + (((((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))) + (t))))))) -> (exists ee_division_product_equation_code_graph. ((exists ee_first_rp_equation_code_graphproduct ee_first_rn_equation_code_graphproduct ee_first_ip_equation_code_graphproduct ee_first_in_equation_code_graphproduct ee_second_rp_equation_code_graphproduct ee_second_rn_equation_code_graphproduct ee_second_ip_equation_code_graphproduct ee_second_in_equation_code_graphproduct. ((exists ge_representation_real_code_equation_code_graphproductfirst ge_representation_imaginary_code_equation_code_graphproductfirst. (((bc) = ((ge_representation_real_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst)) * S ((ge_representation_real_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst)) + ((ge_representation_imaginary_code_equation_code_graphproductfirst) + (ge_representation_imaginary_code_equation_code_graphproductfirst))) /\ ((exists ge_balance_positive_equation_code_graphproductfirstreal ge_balance_negative_equation_code_graphproductfirstreal. (((((ge_representation_real_code_equation_code_graphproductfirst) = 2 * (ge_balance_positive_equation_code_graphproductfirstreal) /\ (ge_balance_negative_equation_code_graphproductfirstreal) = 0) \/ exists ge_signed_half_equation_code_graphproductfirstrealdecode. (((ge_representation_real_code_equation_code_graphproductfirst) = 2 * ge_signed_half_equation_code_graphproductfirstrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductfirstreal) = 0) /\ (ge_balance_negative_equation_code_graphproductfirstreal) = S ge_signed_half_equation_code_graphproductfirstrealdecode))) /\ ((ee_first_rp_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductfirstreal = (ee_first_rn_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductfirstreal))) /\ (exists ge_balance_positive_equation_code_graphproductfirstimaginary ge_balance_negative_equation_code_graphproductfirstimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductfirst) = 2 * (ge_balance_positive_equation_code_graphproductfirstimaginary) /\ (ge_balance_negative_equation_code_graphproductfirstimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductfirstimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductfirst) = 2 * ge_signed_half_equation_code_graphproductfirstimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductfirstimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductfirstimaginary) = S ge_signed_half_equation_code_graphproductfirstimaginarydecode))) /\ ((ee_first_ip_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductfirstimaginary = (ee_first_in_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_equation_code_graphproductsecond ge_representation_imaginary_code_equation_code_graphproductsecond. (((qc) = ((ge_representation_real_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond)) * S ((ge_representation_real_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond)) + ((ge_representation_imaginary_code_equation_code_graphproductsecond) + (ge_representation_imaginary_code_equation_code_graphproductsecond))) /\ ((exists ge_balance_positive_equation_code_graphproductsecondreal ge_balance_negative_equation_code_graphproductsecondreal. (((((ge_representation_real_code_equation_code_graphproductsecond) = 2 * (ge_balance_positive_equation_code_graphproductsecondreal) /\ (ge_balance_negative_equation_code_graphproductsecondreal) = 0) \/ exists ge_signed_half_equation_code_graphproductsecondrealdecode. (((ge_representation_real_code_equation_code_graphproductsecond) = 2 * ge_signed_half_equation_code_graphproductsecondrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductsecondreal) = 0) /\ (ge_balance_negative_equation_code_graphproductsecondreal) = S ge_signed_half_equation_code_graphproductsecondrealdecode))) /\ ((ee_second_rp_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductsecondreal = (ee_second_rn_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductsecondreal))) /\ (exists ge_balance_positive_equation_code_graphproductsecondimaginary ge_balance_negative_equation_code_graphproductsecondimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductsecond) = 2 * (ge_balance_positive_equation_code_graphproductsecondimaginary) /\ (ge_balance_negative_equation_code_graphproductsecondimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductsecondimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductsecond) = 2 * ge_signed_half_equation_code_graphproductsecondimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductsecondimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductsecondimaginary) = S ge_signed_half_equation_code_graphproductsecondimaginarydecode))) /\ ((ee_second_ip_equation_code_graphproduct) + ge_balance_negative_equation_code_graphproductsecondimaginary = (ee_second_in_equation_code_graphproduct) + ge_balance_positive_equation_code_graphproductsecondimaginary)))))) /\ (exists ge_representation_real_code_equation_code_graphproductoutput ge_representation_imaginary_code_equation_code_graphproductoutput. (((ee_division_product_equation_code_graph) = ((ge_representation_real_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput)) * S ((ge_representation_real_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput)) + ((ge_representation_imaginary_code_equation_code_graphproductoutput) + (ge_representation_imaginary_code_equation_code_graphproductoutput))) /\ ((exists ge_balance_positive_equation_code_graphproductoutputreal ge_balance_negative_equation_code_graphproductoutputreal. (((((ge_representation_real_code_equation_code_graphproductoutput) = 2 * (ge_balance_positive_equation_code_graphproductoutputreal) /\ (ge_balance_negative_equation_code_graphproductoutputreal) = 0) \/ exists ge_signed_half_equation_code_graphproductoutputrealdecode. (((ge_representation_real_code_equation_code_graphproductoutput) = 2 * ge_signed_half_equation_code_graphproductoutputrealdecode + 1 /\ (ge_balance_positive_equation_code_graphproductoutputreal) = 0) /\ (ge_balance_negative_equation_code_graphproductoutputreal) = S ge_signed_half_equation_code_graphproductoutputrealdecode))) /\ ((((((((ee_first_rp_equation_code_graphproduct) * (ee_second_rp_equation_code_graphproduct))) + (((ee_first_rn_equation_code_graphproduct) * (ee_second_rn_equation_code_graphproduct))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))))))) + ge_balance_negative_equation_code_graphproductoutputreal = (((((((ee_first_rp_equation_code_graphproduct) * (ee_second_rn_equation_code_graphproduct))) + (((ee_first_rn_equation_code_graphproduct) * (ee_second_rp_equation_code_graphproduct))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))))))) + ge_balance_positive_equation_code_graphproductoutputreal))) /\ (exists ge_balance_positive_equation_code_graphproductoutputimaginary ge_balance_negative_equation_code_graphproductoutputimaginary. (((((ge_representation_imaginary_code_equation_code_graphproductoutput) = 2 * (ge_balance_positive_equation_code_graphproductoutputimaginary) /\ (ge_balance_negative_equation_code_graphproductoutputimaginary) = 0) \/ exists ge_signed_half_equation_code_graphproductoutputimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphproductoutput) = 2 * ge_signed_half_equation_code_graphproductoutputimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphproductoutputimaginary) = 0) /\ (ge_balance_negative_equation_code_graphproductoutputimaginary) = S ge_signed_half_equation_code_graphproductoutputimaginarydecode))) /\ ((((((((((ee_first_rp_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))) + (((ee_first_rn_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_rp_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_rn_equation_code_graphproduct))))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))))))) + ge_balance_negative_equation_code_graphproductoutputimaginary = (((((((((ee_first_rp_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))) + (((ee_first_rn_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_rn_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_rp_equation_code_graphproduct))))))) + (((((ee_first_ip_equation_code_graphproduct) * (ee_second_ip_equation_code_graphproduct))) + (((ee_first_in_equation_code_graphproduct) * (ee_second_in_equation_code_graphproduct))))))) + ge_balance_positive_equation_code_graphproductoutputimaginary))))))))) /\ (exists ge_first_rp_equation_code_graphsum ge_first_rn_equation_code_graphsum ge_first_ip_equation_code_graphsum ge_first_in_equation_code_graphsum ge_second_rp_equation_code_graphsum ge_second_rn_equation_code_graphsum ge_second_ip_equation_code_graphsum ge_second_in_equation_code_graphsum. ((exists ge_representation_real_code_equation_code_graphsumfirst ge_representation_imaginary_code_equation_code_graphsumfirst. (((ee_division_product_equation_code_graph) = ((ge_representation_real_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst)) * S ((ge_representation_real_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst)) + ((ge_representation_imaginary_code_equation_code_graphsumfirst) + (ge_representation_imaginary_code_equation_code_graphsumfirst))) /\ ((exists ge_balance_positive_equation_code_graphsumfirstreal ge_balance_negative_equation_code_graphsumfirstreal. (((((ge_representation_real_code_equation_code_graphsumfirst) = 2 * (ge_balance_positive_equation_code_graphsumfirstreal) /\ (ge_balance_negative_equation_code_graphsumfirstreal) = 0) \/ exists ge_signed_half_equation_code_graphsumfirstrealdecode. (((ge_representation_real_code_equation_code_graphsumfirst) = 2 * ge_signed_half_equation_code_graphsumfirstrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumfirstreal) = 0) /\ (ge_balance_negative_equation_code_graphsumfirstreal) = S ge_signed_half_equation_code_graphsumfirstrealdecode))) /\ ((ge_first_rp_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumfirstreal = (ge_first_rn_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumfirstreal))) /\ (exists ge_balance_positive_equation_code_graphsumfirstimaginary ge_balance_negative_equation_code_graphsumfirstimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumfirst) = 2 * (ge_balance_positive_equation_code_graphsumfirstimaginary) /\ (ge_balance_negative_equation_code_graphsumfirstimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumfirstimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumfirst) = 2 * ge_signed_half_equation_code_graphsumfirstimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumfirstimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumfirstimaginary) = S ge_signed_half_equation_code_graphsumfirstimaginarydecode))) /\ ((ge_first_ip_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumfirstimaginary = (ge_first_in_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumfirstimaginary)))))) /\ ((exists ge_representation_real_code_equation_code_graphsumsecond ge_representation_imaginary_code_equation_code_graphsumsecond. (((rc) = ((ge_representation_real_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond)) * S ((ge_representation_real_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond)) + ((ge_representation_imaginary_code_equation_code_graphsumsecond) + (ge_representation_imaginary_code_equation_code_graphsumsecond))) /\ ((exists ge_balance_positive_equation_code_graphsumsecondreal ge_balance_negative_equation_code_graphsumsecondreal. (((((ge_representation_real_code_equation_code_graphsumsecond) = 2 * (ge_balance_positive_equation_code_graphsumsecondreal) /\ (ge_balance_negative_equation_code_graphsumsecondreal) = 0) \/ exists ge_signed_half_equation_code_graphsumsecondrealdecode. (((ge_representation_real_code_equation_code_graphsumsecond) = 2 * ge_signed_half_equation_code_graphsumsecondrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumsecondreal) = 0) /\ (ge_balance_negative_equation_code_graphsumsecondreal) = S ge_signed_half_equation_code_graphsumsecondrealdecode))) /\ ((ge_second_rp_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumsecondreal = (ge_second_rn_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumsecondreal))) /\ (exists ge_balance_positive_equation_code_graphsumsecondimaginary ge_balance_negative_equation_code_graphsumsecondimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumsecond) = 2 * (ge_balance_positive_equation_code_graphsumsecondimaginary) /\ (ge_balance_negative_equation_code_graphsumsecondimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumsecondimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumsecond) = 2 * ge_signed_half_equation_code_graphsumsecondimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumsecondimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumsecondimaginary) = S ge_signed_half_equation_code_graphsumsecondimaginarydecode))) /\ ((ge_second_ip_equation_code_graphsum) + ge_balance_negative_equation_code_graphsumsecondimaginary = (ge_second_in_equation_code_graphsum) + ge_balance_positive_equation_code_graphsumsecondimaginary)))))) /\ (exists ge_representation_real_code_equation_code_graphsumoutput ge_representation_imaginary_code_equation_code_graphsumoutput. (((ac) = ((ge_representation_real_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput)) * S ((ge_representation_real_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput)) + ((ge_representation_imaginary_code_equation_code_graphsumoutput) + (ge_representation_imaginary_code_equation_code_graphsumoutput))) /\ ((exists ge_balance_positive_equation_code_graphsumoutputreal ge_balance_negative_equation_code_graphsumoutputreal. (((((ge_representation_real_code_equation_code_graphsumoutput) = 2 * (ge_balance_positive_equation_code_graphsumoutputreal) /\ (ge_balance_negative_equation_code_graphsumoutputreal) = 0) \/ exists ge_signed_half_equation_code_graphsumoutputrealdecode. (((ge_representation_real_code_equation_code_graphsumoutput) = 2 * ge_signed_half_equation_code_graphsumoutputrealdecode + 1 /\ (ge_balance_positive_equation_code_graphsumoutputreal) = 0) /\ (ge_balance_negative_equation_code_graphsumoutputreal) = S ge_signed_half_equation_code_graphsumoutputrealdecode))) /\ ((((ge_first_rp_equation_code_graphsum) + (ge_second_rp_equation_code_graphsum))) + ge_balance_negative_equation_code_graphsumoutputreal = (((ge_first_rn_equation_code_graphsum) + (ge_second_rn_equation_code_graphsum))) + ge_balance_positive_equation_code_graphsumoutputreal))) /\ (exists ge_balance_positive_equation_code_graphsumoutputimaginary ge_balance_negative_equation_code_graphsumoutputimaginary. (((((ge_representation_imaginary_code_equation_code_graphsumoutput) = 2 * (ge_balance_positive_equation_code_graphsumoutputimaginary) /\ (ge_balance_negative_equation_code_graphsumoutputimaginary) = 0) \/ exists ge_signed_half_equation_code_graphsumoutputimaginarydecode. (((ge_representation_imaginary_code_equation_code_graphsumoutput) = 2 * ge_signed_half_equation_code_graphsumoutputimaginarydecode + 1 /\ (ge_balance_positive_equation_code_graphsumoutputimaginary) = 0) /\ (ge_balance_negative_equation_code_graphsumoutputimaginary) = S ge_signed_half_equation_code_graphsumoutputimaginarydecode))) /\ ((((ge_first_ip_equation_code_graphsum) + (ge_second_ip_equation_code_graphsum))) + ge_balance_negative_equation_code_graphsumoutputimaginary = (((ge_first_in_equation_code_graphsum) + (ge_second_in_equation_code_graphsum))) + ge_balance_positive_equation_code_graphsumoutputimaginary)))))))))))

Complete tactic proof in conservative notation

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

84 script commands · 12 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (1)
eisenstein multiply of representations
01Fix variables and assumptionsL1–10

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

  1. L1
    intro ac
  2. L2
    intro bc
  3. L3
    intro qc
  4. L4
    intro rc
  5. L5
    intro a
  6. L6
    intro b
  7. L7
    intro c
  8. L8
    intro d
  9. L9
    intro e
  10. L10
    intro f
02Fix variables and assumptionsL11–20

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

  1. L11
    intro g
  2. L12
    intro h
  3. L13
    intro i
  4. L14
    intro j
  5. L15
    intro k
  6. L16
    intro l
  7. L17
    intro o
  8. L18
    intro p
  9. L19
    intro s
  10. L20
    intro t
03Fix variables and assumptionsL21–25

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

  1. L21
    intro hfirst
  2. L22
    intro hsecond
  3. L23
    intro hquotient
  4. L24
    intro hremainder
  5. L25
    intro hequation
04Establish hproductL26–31

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

  1. L26
    have hproduct : ∃ pc. ZPairRep(pc,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l))Definitions: ZPairRep(pc,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l))Original native command in the exact edition
  2. L27
    specialize gaussian_representation_exists ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  3. L28
    specialize gaussian_representation_exists ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  4. L29
    specialize gaussian_representation_exists ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  5. L30
    specialize gaussian_representation_exists ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  6. L31
    apply gaussian_representation_exists
05Separate the logical casesL32–32

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

  1. L32
    cases hproduct
06Construct an explicit witnessL33–33

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

  1. L33
    exists x
07Separate the logical casesL34–34

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

  1. L34
    split
08Use earlier factsL35–44

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

  1. L35
    specialize eisenstein_multiply_of_representations bc
  2. L36
    specialize eisenstein_multiply_of_representations qc
  3. L37
    specialize eisenstein_multiply_of_representations x
  4. L38
    specialize eisenstein_multiply_of_representations e
  5. L39
    specialize eisenstein_multiply_of_representations f
  6. L40
    specialize eisenstein_multiply_of_representations g
  7. L41
    specialize eisenstein_multiply_of_representations h
  8. L42
    specialize eisenstein_multiply_of_representations i
  9. L43
    specialize eisenstein_multiply_of_representations j
  10. L44
    specialize eisenstein_multiply_of_representations k
09Use earlier factsL45–54

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

  1. L45
    specialize eisenstein_multiply_of_representations l
  2. L46
    apply eisenstein_multiply_of_representations
  3. L47
    exact hsecond
  4. L48
    exact hquotient
  5. L49
    exact hproduct_witness
  6. L50
    specialize gaussian_add_of_representations x
  7. L51
    specialize gaussian_add_of_representations rc
  8. L52
    specialize gaussian_add_of_representations ac
  9. L53
    specialize gaussian_add_of_representations ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  10. L54
    specialize gaussian_add_of_representations ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
10Use earlier factsL55–64

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

  1. L55
    specialize gaussian_add_of_representations ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  2. L56
    specialize gaussian_add_of_representations ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  3. L57
    specialize gaussian_add_of_representations o
  4. L58
    specialize gaussian_add_of_representations p
  5. L59
    specialize gaussian_add_of_representations s
  6. L60
    specialize gaussian_add_of_representations t
  7. L61
    apply gaussian_add_of_representations
  8. L62
    exact hproduct_witness
  9. L63
    exact hremainder
  10. L64
    specialize gaussian_representation_integer_transport ac
11Use earlier factsL65–74

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

  1. L65
    specialize gaussian_representation_integer_transport a
  2. L66
    specialize gaussian_representation_integer_transport b
  3. L67
    specialize gaussian_representation_integer_transport c
  4. L68
    specialize gaussian_representation_integer_transport d
  5. L69
    specialize gaussian_representation_integer_transport ((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))
  6. L70
    specialize gaussian_representation_integer_transport ((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))
  7. L71
    specialize gaussian_representation_integer_transport ((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))) + (s))
  8. L72
    specialize gaussian_representation_integer_transport ((((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))) + (t))
  9. L73
    apply gaussian_representation_integer_transport
  10. L74
    specialize gaussian_equal_symmetric ((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))
12Use earlier factsL75–84

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

  1. L75
    specialize gaussian_equal_symmetric ((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))
  2. L76
    specialize gaussian_equal_symmetric ((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))) + (s))
  3. L77
    specialize gaussian_equal_symmetric ((((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))) + (t))
  4. L78
    specialize gaussian_equal_symmetric a
  5. L79
    specialize gaussian_equal_symmetric b
  6. L80
    specialize gaussian_equal_symmetric c
  7. L81
    specialize gaussian_equal_symmetric d
  8. L82
    apply gaussian_equal_symmetric
  9. L83
    exact hequation
  10. L84
    exact hfirst

Library-wide reading audit

Original defined command ledger · 84 lines
  1. 0001intro ac
  2. 0002intro bc
  3. 0003intro qc
  4. 0004intro rc
  5. 0005intro a
  6. 0006intro b
  7. 0007intro c
  8. 0008intro d
  9. 0009intro e
  10. 0010intro f
  11. 0011intro g
  12. 0012intro h
  13. 0013intro i
  14. 0014intro j
  15. 0015intro k
  16. 0016intro l
  17. 0017intro o
  18. 0018intro p
  19. 0019intro s
  20. 0020intro t
  21. 0021intro hfirst
  22. 0022intro hsecond
  23. 0023intro hquotient
  24. 0024intro hremainder
  25. 0025intro hequation
  26. 0026have hproduct : ∃ pc. ZPairRep(pc,e · i + f · j + (g · l + h · k),e · j + f · i + (g · k + h · l),e · k + f · l + (g · i + h · j) + (g · l + h · k),e · l + f · k + (g · j + h · i) + (g · k + h · l))
  27. 0027specialize gaussian_representation_exists ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  28. 0028specialize gaussian_representation_exists ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  29. 0029specialize gaussian_representation_exists ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  30. 0030specialize gaussian_representation_exists ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  31. 0031apply gaussian_representation_exists
  32. 0032cases hproduct
  33. 0033exists x
  34. 0034split
  35. 0035specialize eisenstein_multiply_of_representations bc
  36. 0036specialize eisenstein_multiply_of_representations qc
  37. 0037specialize eisenstein_multiply_of_representations x
  38. 0038specialize eisenstein_multiply_of_representations e
  39. 0039specialize eisenstein_multiply_of_representations f
  40. 0040specialize eisenstein_multiply_of_representations g
  41. 0041specialize eisenstein_multiply_of_representations h
  42. 0042specialize eisenstein_multiply_of_representations i
  43. 0043specialize eisenstein_multiply_of_representations j
  44. 0044specialize eisenstein_multiply_of_representations k
  45. 0045specialize eisenstein_multiply_of_representations l
  46. 0046apply eisenstein_multiply_of_representations
  47. 0047exact hsecond
  48. 0048exact hquotient
  49. 0049exact hproduct_witness
  50. 0050specialize gaussian_add_of_representations x
  51. 0051specialize gaussian_add_of_representations rc
  52. 0052specialize gaussian_add_of_representations ac
  53. 0053specialize gaussian_add_of_representations ((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))
  54. 0054specialize gaussian_add_of_representations ((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))
  55. 0055specialize gaussian_add_of_representations ((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))
  56. 0056specialize gaussian_add_of_representations ((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))
  57. 0057specialize gaussian_add_of_representations o
  58. 0058specialize gaussian_add_of_representations p
  59. 0059specialize gaussian_add_of_representations s
  60. 0060specialize gaussian_add_of_representations t
  61. 0061apply gaussian_add_of_representations
  62. 0062exact hproduct_witness
  63. 0063exact hremainder
  64. 0064specialize gaussian_representation_integer_transport ac
  65. 0065specialize gaussian_representation_integer_transport a
  66. 0066specialize gaussian_representation_integer_transport b
  67. 0067specialize gaussian_representation_integer_transport c
  68. 0068specialize gaussian_representation_integer_transport d
  69. 0069specialize gaussian_representation_integer_transport ((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))
  70. 0070specialize gaussian_representation_integer_transport ((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))
  71. 0071specialize gaussian_representation_integer_transport ((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))) + (s))
  72. 0072specialize gaussian_representation_integer_transport ((((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))) + (t))
  73. 0073apply gaussian_representation_integer_transport
  74. 0074specialize gaussian_equal_symmetric ((((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))) + (o))
  75. 0075specialize gaussian_equal_symmetric ((((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))) + (p))
  76. 0076specialize gaussian_equal_symmetric ((((((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))) + (((((g) * (l))) + (((h) * (k))))))) + (s))
  77. 0077specialize gaussian_equal_symmetric ((((((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))) + (((((g) * (k))) + (((h) * (l))))))) + (t))
  78. 0078specialize gaussian_equal_symmetric a
  79. 0079specialize gaussian_equal_symmetric b
  80. 0080specialize gaussian_equal_symmetric c
  81. 0081specialize gaussian_equal_symmetric d
  82. 0082apply gaussian_equal_symmetric
  83. 0083exact hequation
  84. 0084exact hfirst