GF0024

gaussian_add_associative

The actual canonical Gaussian add graph associates, with all intermediate product/sum codes witnessed.

Alpha v34 checked-use · first admitted v30 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Inputs are genuine canonical signed-pair codes, not arbitrary naturals. Products start at the actual Gaussian identity, whose code is six. The factor list uses the proved prime-divisor property; irreducibility alone is not silently renamed primality. Uniqueness supplies equal lengths, a bounded bijection, and an actual unit at each match, including repeated factors. Units have empty factorizations and zero is excluded. Sorted primary representatives, Gaussian prime classification, and Eisenstein factorization are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ ab. ∀ bc. ∀ t. ZPairAdd(a,b,ab) → ZPairAdd(ab,c,t) → ZPairAdd(b,c,bc) → ZPairAdd(a,bc,t)

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

Definition DAG

ZPairRep(z,ap,an,bp,bn) · 6ZPairAdd(a,b,c) · 4

Actual proof prerequisites

gaussian_valid_has_representationgaussian_add_input_left_validgaussian_add_input_right_validgaussian_add_for_representations · checked external prerequisitegaussian_add_of_representations · checked external prerequisitegaussian_representation_integer_transport · checked external prerequisitegaussian_ring_raw_add_associative
Original expanded first-order statement 
forall a b c ab bc t. (exists ge_first_rp_associate_first_add ge_first_rn_associate_first_add ge_first_ip_associate_first_add ge_first_in_associate_first_add ge_second_rp_associate_first_add ge_second_rn_associate_first_add ge_second_ip_associate_first_add ge_second_in_associate_first_add. ((exists ge_representation_real_code_associate_first_addfirst ge_representation_imaginary_code_associate_first_addfirst. (((a) = ((ge_representation_real_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst)) * S ((ge_representation_real_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst)) + ((ge_representation_imaginary_code_associate_first_addfirst) + (ge_representation_imaginary_code_associate_first_addfirst))) /\ ((exists ge_balance_positive_associate_first_addfirstreal ge_balance_negative_associate_first_addfirstreal. (((((ge_representation_real_code_associate_first_addfirst) = 2 * (ge_balance_positive_associate_first_addfirstreal) /\ (ge_balance_negative_associate_first_addfirstreal) = 0) \/ exists ge_signed_half_associate_first_addfirstrealdecode. (((ge_representation_real_code_associate_first_addfirst) = 2 * ge_signed_half_associate_first_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_first_addfirstreal) = 0) /\ (ge_balance_negative_associate_first_addfirstreal) = S ge_signed_half_associate_first_addfirstrealdecode))) /\ ((ge_first_rp_associate_first_add) + ge_balance_negative_associate_first_addfirstreal = (ge_first_rn_associate_first_add) + ge_balance_positive_associate_first_addfirstreal))) /\ (exists ge_balance_positive_associate_first_addfirstimaginary ge_balance_negative_associate_first_addfirstimaginary. (((((ge_representation_imaginary_code_associate_first_addfirst) = 2 * (ge_balance_positive_associate_first_addfirstimaginary) /\ (ge_balance_negative_associate_first_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_first_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_first_addfirst) = 2 * ge_signed_half_associate_first_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_first_addfirstimaginary) = S ge_signed_half_associate_first_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_first_add) + ge_balance_negative_associate_first_addfirstimaginary = (ge_first_in_associate_first_add) + ge_balance_positive_associate_first_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_first_addsecond ge_representation_imaginary_code_associate_first_addsecond. (((b) = ((ge_representation_real_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond)) * S ((ge_representation_real_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond)) + ((ge_representation_imaginary_code_associate_first_addsecond) + (ge_representation_imaginary_code_associate_first_addsecond))) /\ ((exists ge_balance_positive_associate_first_addsecondreal ge_balance_negative_associate_first_addsecondreal. (((((ge_representation_real_code_associate_first_addsecond) = 2 * (ge_balance_positive_associate_first_addsecondreal) /\ (ge_balance_negative_associate_first_addsecondreal) = 0) \/ exists ge_signed_half_associate_first_addsecondrealdecode. (((ge_representation_real_code_associate_first_addsecond) = 2 * ge_signed_half_associate_first_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_first_addsecondreal) = 0) /\ (ge_balance_negative_associate_first_addsecondreal) = S ge_signed_half_associate_first_addsecondrealdecode))) /\ ((ge_second_rp_associate_first_add) + ge_balance_negative_associate_first_addsecondreal = (ge_second_rn_associate_first_add) + ge_balance_positive_associate_first_addsecondreal))) /\ (exists ge_balance_positive_associate_first_addsecondimaginary ge_balance_negative_associate_first_addsecondimaginary. (((((ge_representation_imaginary_code_associate_first_addsecond) = 2 * (ge_balance_positive_associate_first_addsecondimaginary) /\ (ge_balance_negative_associate_first_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_first_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_first_addsecond) = 2 * ge_signed_half_associate_first_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_first_addsecondimaginary) = S ge_signed_half_associate_first_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_first_add) + ge_balance_negative_associate_first_addsecondimaginary = (ge_second_in_associate_first_add) + ge_balance_positive_associate_first_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_first_addoutput ge_representation_imaginary_code_associate_first_addoutput. (((ab) = ((ge_representation_real_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput)) * S ((ge_representation_real_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput)) + ((ge_representation_imaginary_code_associate_first_addoutput) + (ge_representation_imaginary_code_associate_first_addoutput))) /\ ((exists ge_balance_positive_associate_first_addoutputreal ge_balance_negative_associate_first_addoutputreal. (((((ge_representation_real_code_associate_first_addoutput) = 2 * (ge_balance_positive_associate_first_addoutputreal) /\ (ge_balance_negative_associate_first_addoutputreal) = 0) \/ exists ge_signed_half_associate_first_addoutputrealdecode. (((ge_representation_real_code_associate_first_addoutput) = 2 * ge_signed_half_associate_first_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_first_addoutputreal) = 0) /\ (ge_balance_negative_associate_first_addoutputreal) = S ge_signed_half_associate_first_addoutputrealdecode))) /\ ((((ge_first_rp_associate_first_add) + (ge_second_rp_associate_first_add))) + ge_balance_negative_associate_first_addoutputreal = (((ge_first_rn_associate_first_add) + (ge_second_rn_associate_first_add))) + ge_balance_positive_associate_first_addoutputreal))) /\ (exists ge_balance_positive_associate_first_addoutputimaginary ge_balance_negative_associate_first_addoutputimaginary. (((((ge_representation_imaginary_code_associate_first_addoutput) = 2 * (ge_balance_positive_associate_first_addoutputimaginary) /\ (ge_balance_negative_associate_first_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_first_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_first_addoutput) = 2 * ge_signed_half_associate_first_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_first_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_first_addoutputimaginary) = S ge_signed_half_associate_first_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_first_add) + (ge_second_ip_associate_first_add))) + ge_balance_negative_associate_first_addoutputimaginary = (((ge_first_in_associate_first_add) + (ge_second_in_associate_first_add))) + ge_balance_positive_associate_first_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_second_add ge_first_rn_associate_second_add ge_first_ip_associate_second_add ge_first_in_associate_second_add ge_second_rp_associate_second_add ge_second_rn_associate_second_add ge_second_ip_associate_second_add ge_second_in_associate_second_add. ((exists ge_representation_real_code_associate_second_addfirst ge_representation_imaginary_code_associate_second_addfirst. (((ab) = ((ge_representation_real_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst)) * S ((ge_representation_real_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst)) + ((ge_representation_imaginary_code_associate_second_addfirst) + (ge_representation_imaginary_code_associate_second_addfirst))) /\ ((exists ge_balance_positive_associate_second_addfirstreal ge_balance_negative_associate_second_addfirstreal. (((((ge_representation_real_code_associate_second_addfirst) = 2 * (ge_balance_positive_associate_second_addfirstreal) /\ (ge_balance_negative_associate_second_addfirstreal) = 0) \/ exists ge_signed_half_associate_second_addfirstrealdecode. (((ge_representation_real_code_associate_second_addfirst) = 2 * ge_signed_half_associate_second_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_second_addfirstreal) = 0) /\ (ge_balance_negative_associate_second_addfirstreal) = S ge_signed_half_associate_second_addfirstrealdecode))) /\ ((ge_first_rp_associate_second_add) + ge_balance_negative_associate_second_addfirstreal = (ge_first_rn_associate_second_add) + ge_balance_positive_associate_second_addfirstreal))) /\ (exists ge_balance_positive_associate_second_addfirstimaginary ge_balance_negative_associate_second_addfirstimaginary. (((((ge_representation_imaginary_code_associate_second_addfirst) = 2 * (ge_balance_positive_associate_second_addfirstimaginary) /\ (ge_balance_negative_associate_second_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_second_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_second_addfirst) = 2 * ge_signed_half_associate_second_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_second_addfirstimaginary) = S ge_signed_half_associate_second_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_second_add) + ge_balance_negative_associate_second_addfirstimaginary = (ge_first_in_associate_second_add) + ge_balance_positive_associate_second_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_second_addsecond ge_representation_imaginary_code_associate_second_addsecond. (((c) = ((ge_representation_real_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond)) * S ((ge_representation_real_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond)) + ((ge_representation_imaginary_code_associate_second_addsecond) + (ge_representation_imaginary_code_associate_second_addsecond))) /\ ((exists ge_balance_positive_associate_second_addsecondreal ge_balance_negative_associate_second_addsecondreal. (((((ge_representation_real_code_associate_second_addsecond) = 2 * (ge_balance_positive_associate_second_addsecondreal) /\ (ge_balance_negative_associate_second_addsecondreal) = 0) \/ exists ge_signed_half_associate_second_addsecondrealdecode. (((ge_representation_real_code_associate_second_addsecond) = 2 * ge_signed_half_associate_second_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_second_addsecondreal) = 0) /\ (ge_balance_negative_associate_second_addsecondreal) = S ge_signed_half_associate_second_addsecondrealdecode))) /\ ((ge_second_rp_associate_second_add) + ge_balance_negative_associate_second_addsecondreal = (ge_second_rn_associate_second_add) + ge_balance_positive_associate_second_addsecondreal))) /\ (exists ge_balance_positive_associate_second_addsecondimaginary ge_balance_negative_associate_second_addsecondimaginary. (((((ge_representation_imaginary_code_associate_second_addsecond) = 2 * (ge_balance_positive_associate_second_addsecondimaginary) /\ (ge_balance_negative_associate_second_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_second_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_second_addsecond) = 2 * ge_signed_half_associate_second_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_second_addsecondimaginary) = S ge_signed_half_associate_second_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_second_add) + ge_balance_negative_associate_second_addsecondimaginary = (ge_second_in_associate_second_add) + ge_balance_positive_associate_second_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_second_addoutput ge_representation_imaginary_code_associate_second_addoutput. (((t) = ((ge_representation_real_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput)) * S ((ge_representation_real_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput)) + ((ge_representation_imaginary_code_associate_second_addoutput) + (ge_representation_imaginary_code_associate_second_addoutput))) /\ ((exists ge_balance_positive_associate_second_addoutputreal ge_balance_negative_associate_second_addoutputreal. (((((ge_representation_real_code_associate_second_addoutput) = 2 * (ge_balance_positive_associate_second_addoutputreal) /\ (ge_balance_negative_associate_second_addoutputreal) = 0) \/ exists ge_signed_half_associate_second_addoutputrealdecode. (((ge_representation_real_code_associate_second_addoutput) = 2 * ge_signed_half_associate_second_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_second_addoutputreal) = 0) /\ (ge_balance_negative_associate_second_addoutputreal) = S ge_signed_half_associate_second_addoutputrealdecode))) /\ ((((ge_first_rp_associate_second_add) + (ge_second_rp_associate_second_add))) + ge_balance_negative_associate_second_addoutputreal = (((ge_first_rn_associate_second_add) + (ge_second_rn_associate_second_add))) + ge_balance_positive_associate_second_addoutputreal))) /\ (exists ge_balance_positive_associate_second_addoutputimaginary ge_balance_negative_associate_second_addoutputimaginary. (((((ge_representation_imaginary_code_associate_second_addoutput) = 2 * (ge_balance_positive_associate_second_addoutputimaginary) /\ (ge_balance_negative_associate_second_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_second_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_second_addoutput) = 2 * ge_signed_half_associate_second_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_second_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_second_addoutputimaginary) = S ge_signed_half_associate_second_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_second_add) + (ge_second_ip_associate_second_add))) + ge_balance_negative_associate_second_addoutputimaginary = (((ge_first_in_associate_second_add) + (ge_second_in_associate_second_add))) + ge_balance_positive_associate_second_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_third_add ge_first_rn_associate_third_add ge_first_ip_associate_third_add ge_first_in_associate_third_add ge_second_rp_associate_third_add ge_second_rn_associate_third_add ge_second_ip_associate_third_add ge_second_in_associate_third_add. ((exists ge_representation_real_code_associate_third_addfirst ge_representation_imaginary_code_associate_third_addfirst. (((b) = ((ge_representation_real_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst)) * S ((ge_representation_real_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst)) + ((ge_representation_imaginary_code_associate_third_addfirst) + (ge_representation_imaginary_code_associate_third_addfirst))) /\ ((exists ge_balance_positive_associate_third_addfirstreal ge_balance_negative_associate_third_addfirstreal. (((((ge_representation_real_code_associate_third_addfirst) = 2 * (ge_balance_positive_associate_third_addfirstreal) /\ (ge_balance_negative_associate_third_addfirstreal) = 0) \/ exists ge_signed_half_associate_third_addfirstrealdecode. (((ge_representation_real_code_associate_third_addfirst) = 2 * ge_signed_half_associate_third_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_third_addfirstreal) = 0) /\ (ge_balance_negative_associate_third_addfirstreal) = S ge_signed_half_associate_third_addfirstrealdecode))) /\ ((ge_first_rp_associate_third_add) + ge_balance_negative_associate_third_addfirstreal = (ge_first_rn_associate_third_add) + ge_balance_positive_associate_third_addfirstreal))) /\ (exists ge_balance_positive_associate_third_addfirstimaginary ge_balance_negative_associate_third_addfirstimaginary. (((((ge_representation_imaginary_code_associate_third_addfirst) = 2 * (ge_balance_positive_associate_third_addfirstimaginary) /\ (ge_balance_negative_associate_third_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_third_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_third_addfirst) = 2 * ge_signed_half_associate_third_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_third_addfirstimaginary) = S ge_signed_half_associate_third_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_third_add) + ge_balance_negative_associate_third_addfirstimaginary = (ge_first_in_associate_third_add) + ge_balance_positive_associate_third_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_third_addsecond ge_representation_imaginary_code_associate_third_addsecond. (((c) = ((ge_representation_real_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond)) * S ((ge_representation_real_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond)) + ((ge_representation_imaginary_code_associate_third_addsecond) + (ge_representation_imaginary_code_associate_third_addsecond))) /\ ((exists ge_balance_positive_associate_third_addsecondreal ge_balance_negative_associate_third_addsecondreal. (((((ge_representation_real_code_associate_third_addsecond) = 2 * (ge_balance_positive_associate_third_addsecondreal) /\ (ge_balance_negative_associate_third_addsecondreal) = 0) \/ exists ge_signed_half_associate_third_addsecondrealdecode. (((ge_representation_real_code_associate_third_addsecond) = 2 * ge_signed_half_associate_third_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_third_addsecondreal) = 0) /\ (ge_balance_negative_associate_third_addsecondreal) = S ge_signed_half_associate_third_addsecondrealdecode))) /\ ((ge_second_rp_associate_third_add) + ge_balance_negative_associate_third_addsecondreal = (ge_second_rn_associate_third_add) + ge_balance_positive_associate_third_addsecondreal))) /\ (exists ge_balance_positive_associate_third_addsecondimaginary ge_balance_negative_associate_third_addsecondimaginary. (((((ge_representation_imaginary_code_associate_third_addsecond) = 2 * (ge_balance_positive_associate_third_addsecondimaginary) /\ (ge_balance_negative_associate_third_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_third_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_third_addsecond) = 2 * ge_signed_half_associate_third_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_third_addsecondimaginary) = S ge_signed_half_associate_third_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_third_add) + ge_balance_negative_associate_third_addsecondimaginary = (ge_second_in_associate_third_add) + ge_balance_positive_associate_third_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_third_addoutput ge_representation_imaginary_code_associate_third_addoutput. (((bc) = ((ge_representation_real_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput)) * S ((ge_representation_real_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput)) + ((ge_representation_imaginary_code_associate_third_addoutput) + (ge_representation_imaginary_code_associate_third_addoutput))) /\ ((exists ge_balance_positive_associate_third_addoutputreal ge_balance_negative_associate_third_addoutputreal. (((((ge_representation_real_code_associate_third_addoutput) = 2 * (ge_balance_positive_associate_third_addoutputreal) /\ (ge_balance_negative_associate_third_addoutputreal) = 0) \/ exists ge_signed_half_associate_third_addoutputrealdecode. (((ge_representation_real_code_associate_third_addoutput) = 2 * ge_signed_half_associate_third_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_third_addoutputreal) = 0) /\ (ge_balance_negative_associate_third_addoutputreal) = S ge_signed_half_associate_third_addoutputrealdecode))) /\ ((((ge_first_rp_associate_third_add) + (ge_second_rp_associate_third_add))) + ge_balance_negative_associate_third_addoutputreal = (((ge_first_rn_associate_third_add) + (ge_second_rn_associate_third_add))) + ge_balance_positive_associate_third_addoutputreal))) /\ (exists ge_balance_positive_associate_third_addoutputimaginary ge_balance_negative_associate_third_addoutputimaginary. (((((ge_representation_imaginary_code_associate_third_addoutput) = 2 * (ge_balance_positive_associate_third_addoutputimaginary) /\ (ge_balance_negative_associate_third_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_third_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_third_addoutput) = 2 * ge_signed_half_associate_third_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_third_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_third_addoutputimaginary) = S ge_signed_half_associate_third_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_third_add) + (ge_second_ip_associate_third_add))) + ge_balance_negative_associate_third_addoutputimaginary = (((ge_first_in_associate_third_add) + (ge_second_in_associate_third_add))) + ge_balance_positive_associate_third_addoutputimaginary))))))))) -> (exists ge_first_rp_associate_output_add ge_first_rn_associate_output_add ge_first_ip_associate_output_add ge_first_in_associate_output_add ge_second_rp_associate_output_add ge_second_rn_associate_output_add ge_second_ip_associate_output_add ge_second_in_associate_output_add. ((exists ge_representation_real_code_associate_output_addfirst ge_representation_imaginary_code_associate_output_addfirst. (((a) = ((ge_representation_real_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst)) * S ((ge_representation_real_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst)) + ((ge_representation_imaginary_code_associate_output_addfirst) + (ge_representation_imaginary_code_associate_output_addfirst))) /\ ((exists ge_balance_positive_associate_output_addfirstreal ge_balance_negative_associate_output_addfirstreal. (((((ge_representation_real_code_associate_output_addfirst) = 2 * (ge_balance_positive_associate_output_addfirstreal) /\ (ge_balance_negative_associate_output_addfirstreal) = 0) \/ exists ge_signed_half_associate_output_addfirstrealdecode. (((ge_representation_real_code_associate_output_addfirst) = 2 * ge_signed_half_associate_output_addfirstrealdecode + 1 /\ (ge_balance_positive_associate_output_addfirstreal) = 0) /\ (ge_balance_negative_associate_output_addfirstreal) = S ge_signed_half_associate_output_addfirstrealdecode))) /\ ((ge_first_rp_associate_output_add) + ge_balance_negative_associate_output_addfirstreal = (ge_first_rn_associate_output_add) + ge_balance_positive_associate_output_addfirstreal))) /\ (exists ge_balance_positive_associate_output_addfirstimaginary ge_balance_negative_associate_output_addfirstimaginary. (((((ge_representation_imaginary_code_associate_output_addfirst) = 2 * (ge_balance_positive_associate_output_addfirstimaginary) /\ (ge_balance_negative_associate_output_addfirstimaginary) = 0) \/ exists ge_signed_half_associate_output_addfirstimaginarydecode. (((ge_representation_imaginary_code_associate_output_addfirst) = 2 * ge_signed_half_associate_output_addfirstimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addfirstimaginary) = 0) /\ (ge_balance_negative_associate_output_addfirstimaginary) = S ge_signed_half_associate_output_addfirstimaginarydecode))) /\ ((ge_first_ip_associate_output_add) + ge_balance_negative_associate_output_addfirstimaginary = (ge_first_in_associate_output_add) + ge_balance_positive_associate_output_addfirstimaginary)))))) /\ ((exists ge_representation_real_code_associate_output_addsecond ge_representation_imaginary_code_associate_output_addsecond. (((bc) = ((ge_representation_real_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond)) * S ((ge_representation_real_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond)) + ((ge_representation_imaginary_code_associate_output_addsecond) + (ge_representation_imaginary_code_associate_output_addsecond))) /\ ((exists ge_balance_positive_associate_output_addsecondreal ge_balance_negative_associate_output_addsecondreal. (((((ge_representation_real_code_associate_output_addsecond) = 2 * (ge_balance_positive_associate_output_addsecondreal) /\ (ge_balance_negative_associate_output_addsecondreal) = 0) \/ exists ge_signed_half_associate_output_addsecondrealdecode. (((ge_representation_real_code_associate_output_addsecond) = 2 * ge_signed_half_associate_output_addsecondrealdecode + 1 /\ (ge_balance_positive_associate_output_addsecondreal) = 0) /\ (ge_balance_negative_associate_output_addsecondreal) = S ge_signed_half_associate_output_addsecondrealdecode))) /\ ((ge_second_rp_associate_output_add) + ge_balance_negative_associate_output_addsecondreal = (ge_second_rn_associate_output_add) + ge_balance_positive_associate_output_addsecondreal))) /\ (exists ge_balance_positive_associate_output_addsecondimaginary ge_balance_negative_associate_output_addsecondimaginary. (((((ge_representation_imaginary_code_associate_output_addsecond) = 2 * (ge_balance_positive_associate_output_addsecondimaginary) /\ (ge_balance_negative_associate_output_addsecondimaginary) = 0) \/ exists ge_signed_half_associate_output_addsecondimaginarydecode. (((ge_representation_imaginary_code_associate_output_addsecond) = 2 * ge_signed_half_associate_output_addsecondimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addsecondimaginary) = 0) /\ (ge_balance_negative_associate_output_addsecondimaginary) = S ge_signed_half_associate_output_addsecondimaginarydecode))) /\ ((ge_second_ip_associate_output_add) + ge_balance_negative_associate_output_addsecondimaginary = (ge_second_in_associate_output_add) + ge_balance_positive_associate_output_addsecondimaginary)))))) /\ (exists ge_representation_real_code_associate_output_addoutput ge_representation_imaginary_code_associate_output_addoutput. (((t) = ((ge_representation_real_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput)) * S ((ge_representation_real_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput)) + ((ge_representation_imaginary_code_associate_output_addoutput) + (ge_representation_imaginary_code_associate_output_addoutput))) /\ ((exists ge_balance_positive_associate_output_addoutputreal ge_balance_negative_associate_output_addoutputreal. (((((ge_representation_real_code_associate_output_addoutput) = 2 * (ge_balance_positive_associate_output_addoutputreal) /\ (ge_balance_negative_associate_output_addoutputreal) = 0) \/ exists ge_signed_half_associate_output_addoutputrealdecode. (((ge_representation_real_code_associate_output_addoutput) = 2 * ge_signed_half_associate_output_addoutputrealdecode + 1 /\ (ge_balance_positive_associate_output_addoutputreal) = 0) /\ (ge_balance_negative_associate_output_addoutputreal) = S ge_signed_half_associate_output_addoutputrealdecode))) /\ ((((ge_first_rp_associate_output_add) + (ge_second_rp_associate_output_add))) + ge_balance_negative_associate_output_addoutputreal = (((ge_first_rn_associate_output_add) + (ge_second_rn_associate_output_add))) + ge_balance_positive_associate_output_addoutputreal))) /\ (exists ge_balance_positive_associate_output_addoutputimaginary ge_balance_negative_associate_output_addoutputimaginary. (((((ge_representation_imaginary_code_associate_output_addoutput) = 2 * (ge_balance_positive_associate_output_addoutputimaginary) /\ (ge_balance_negative_associate_output_addoutputimaginary) = 0) \/ exists ge_signed_half_associate_output_addoutputimaginarydecode. (((ge_representation_imaginary_code_associate_output_addoutput) = 2 * ge_signed_half_associate_output_addoutputimaginarydecode + 1 /\ (ge_balance_positive_associate_output_addoutputimaginary) = 0) /\ (ge_balance_negative_associate_output_addoutputimaginary) = S ge_signed_half_associate_output_addoutputimaginarydecode))) /\ ((((ge_first_ip_associate_output_add) + (ge_second_ip_associate_output_add))) + ge_balance_negative_associate_output_addoutputimaginary = (((ge_first_in_associate_output_add) + (ge_second_in_associate_output_add))) + ge_balance_positive_associate_output_addoutputimaginary)))))))))

Complete tactic proof in conservative notation

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

131 script commands · 17 reading checkpoints · 6 local claims

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

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

Named ingredients (4)
gaussian valid has representationgaussian add input left validgaussian add input right validgaussian ring raw add associative
01Fix variables and assumptionsL1–9

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro ab
  5. L5
    intro bc
  6. L6
    intro t
  7. L7
    intro hAB
  8. L8
    intro hABC
  9. L9
    intro hBC
02Establish hAL10–17

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

  1. L10
    have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)Definitions: ZPairRep(a,rp,rn,ip,inn)Original native command in the exact edition
  2. L11
    specialize gaussian_valid_has_representation (a)
  3. L12
    apply gaussian_valid_has_representation
  4. L13
    specialize gaussian_add_input_left_valid (a)
  5. L14
    specialize gaussian_add_input_left_valid (b)
  6. L15
    specialize gaussian_add_input_left_valid (ab)
  7. L16
    apply gaussian_add_input_left_valid
  8. L17
    exact hAB
03Separate the logical casesL18–21

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

  1. L18
    cases hA
  2. L19
    cases hA_witness
  3. L20
    cases hA_witness_witness
  4. L21
    cases hA_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 valid has representation.

  1. L22
    have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)Definitions: ZPairRep(b,rp,rn,ip,inn)Original native command in the exact edition
  2. L23
    specialize gaussian_valid_has_representation (b)
  3. L24
    apply gaussian_valid_has_representation
  4. L25
    specialize gaussian_add_input_right_valid (a)
  5. L26
    specialize gaussian_add_input_right_valid (b)
  6. L27
    specialize gaussian_add_input_right_valid (ab)
  7. L28
    apply gaussian_add_input_right_valid
  8. L29
    exact hAB
05Separate the logical casesL30–33

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

  1. L30
    cases hB
  2. L31
    cases hB_witness
  3. L32
    cases hB_witness_witness
  4. L33
    cases hB_witness_witness_witness
06Establish hCL34–41

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

  1. L34
    have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)Definitions: ZPairRep(c,rp,rn,ip,inn)Original native command in the exact edition
  2. L35
    specialize gaussian_valid_has_representation (c)
  3. L36
    apply gaussian_valid_has_representation
  4. L37
    specialize gaussian_add_input_right_valid (ab)
  5. L38
    specialize gaussian_add_input_right_valid (c)
  6. L39
    specialize gaussian_add_input_right_valid (t)
  7. L40
    apply gaussian_add_input_right_valid
  8. L41
    exact hABC
07Separate the logical casesL42–45

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

  1. L42
    cases hC
  2. L43
    cases hC_witness
  3. L44
    cases hC_witness_witness
  4. L45
    cases hC_witness_witness_witness
08Establish habL46–55

Establish this local claim before using it. It is not an additional assumption.

  1. L46
    have hab : ZPairRep(ab,x + x4,x1 + x5,x2 + x6,x3 + x7)Definitions: ZPairRep(ab,x + x4,x1 + x5,x2 + x6,x3 + x7)Original native command in the exact edition
  2. L47
    specialize gaussian_add_for_representations (a)
  3. L48
    specialize gaussian_add_for_representations (b)
  4. L49
    specialize gaussian_add_for_representations (ab)
  5. L50
    specialize gaussian_add_for_representations (x)
  6. L51
    specialize gaussian_add_for_representations (x1)
  7. L52
    specialize gaussian_add_for_representations (x2)
  8. L53
    specialize gaussian_add_for_representations (x3)
  9. L54
    specialize gaussian_add_for_representations (x4)
  10. L55
    specialize gaussian_add_for_representations (x5)
09Use earlier factsL56–61

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

  1. L56
    specialize gaussian_add_for_representations (x6)
  2. L57
    specialize gaussian_add_for_representations (x7)
  3. L58
    apply gaussian_add_for_representations
  4. L59
    exact hA_witness_witness_witness_witness
  5. L60
    exact hB_witness_witness_witness_witness
  6. L61
    exact hAB
10Establish hbcL62–71

Establish this local claim before using it. It is not an additional assumption.

  1. L62
    have hbc : ZPairRep(bc,x4 + x8,x5 + x9,x6 + x10,x7 + x11)Definitions: ZPairRep(bc,x4 + x8,x5 + x9,x6 + x10,x7 + x11)Original native command in the exact edition
  2. L63
    specialize gaussian_add_for_representations (b)
  3. L64
    specialize gaussian_add_for_representations (c)
  4. L65
    specialize gaussian_add_for_representations (bc)
  5. L66
    specialize gaussian_add_for_representations (x4)
  6. L67
    specialize gaussian_add_for_representations (x5)
  7. L68
    specialize gaussian_add_for_representations (x6)
  8. L69
    specialize gaussian_add_for_representations (x7)
  9. L70
    specialize gaussian_add_for_representations (x8)
  10. L71
    specialize gaussian_add_for_representations (x9)
11Use earlier factsL72–77

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

  1. L72
    specialize gaussian_add_for_representations (x10)
  2. L73
    specialize gaussian_add_for_representations (x11)
  3. L74
    apply gaussian_add_for_representations
  4. L75
    exact hB_witness_witness_witness_witness
  5. L76
    exact hC_witness_witness_witness_witness
  6. L77
    exact hBC
12Establish htL78–87

Establish this local claim before using it. It is not an additional assumption.

  1. L78
    have ht : ZPairRep(t,x + x4 + x8,x1 + x5 + x9,x2 + x6 + x10,x3 + x7 + x11)Definitions: ZPairRep(t,x + x4 + x8,x1 + x5 + x9,x2 + x6 + x10,x3 + x7 + x11)Original native command in the exact edition
  2. L79
    specialize gaussian_add_for_representations (ab)
  3. L80
    specialize gaussian_add_for_representations (c)
  4. L81
    specialize gaussian_add_for_representations (t)
  5. L82
    specialize gaussian_add_for_representations (((x) + (x4)))
  6. L83
    specialize gaussian_add_for_representations (((x1) + (x5)))
  7. L84
    specialize gaussian_add_for_representations (((x2) + (x6)))
  8. L85
    specialize gaussian_add_for_representations (((x3) + (x7)))
  9. L86
    specialize gaussian_add_for_representations (x8)
  10. L87
    specialize gaussian_add_for_representations (x9)
13Use earlier factsL88–97

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

  1. L88
    specialize gaussian_add_for_representations (x10)
  2. L89
    specialize gaussian_add_for_representations (x11)
  3. L90
    apply gaussian_add_for_representations
  4. L91
    exact hab
  5. L92
    exact hC_witness_witness_witness_witness
  6. L93
    exact hABC
  7. L94
    specialize gaussian_add_of_representations (a)
  8. L95
    specialize gaussian_add_of_representations (bc)
  9. L96
    specialize gaussian_add_of_representations (t)
  10. L97
    specialize gaussian_add_of_representations (x)
14Use earlier factsL98–107

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

  1. L98
    specialize gaussian_add_of_representations (x1)
  2. L99
    specialize gaussian_add_of_representations (x2)
  3. L100
    specialize gaussian_add_of_representations (x3)
  4. L101
    specialize gaussian_add_of_representations (((x4) + (x8)))
  5. L102
    specialize gaussian_add_of_representations (((x5) + (x9)))
  6. L103
    specialize gaussian_add_of_representations (((x6) + (x10)))
  7. L104
    specialize gaussian_add_of_representations (((x7) + (x11)))
  8. L105
    apply gaussian_add_of_representations
  9. L106
    exact hA_witness_witness_witness_witness
  10. L107
    exact hbc
15Use earlier factsL108–117

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

  1. L108
    specialize gaussian_representation_integer_transport (t)
  2. L109
    specialize gaussian_representation_integer_transport (((((x) + (x4))) + (x8)))
  3. L110
    specialize gaussian_representation_integer_transport (((((x1) + (x5))) + (x9)))
  4. L111
    specialize gaussian_representation_integer_transport (((((x2) + (x6))) + (x10)))
  5. L112
    specialize gaussian_representation_integer_transport (((((x3) + (x7))) + (x11)))
  6. L113
    specialize gaussian_representation_integer_transport (((x) + (((x4) + (x8)))))
  7. L114
    specialize gaussian_representation_integer_transport (((x1) + (((x5) + (x9)))))
  8. L115
    specialize gaussian_representation_integer_transport (((x2) + (((x6) + (x10)))))
  9. L116
    specialize gaussian_representation_integer_transport (((x3) + (((x7) + (x11)))))
  10. L117
    apply gaussian_representation_integer_transport
16Use earlier factsL118–127

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

  1. L118
    specialize gaussian_ring_raw_add_associative (x)
  2. L119
    specialize gaussian_ring_raw_add_associative (x1)
  3. L120
    specialize gaussian_ring_raw_add_associative (x2)
  4. L121
    specialize gaussian_ring_raw_add_associative (x3)
  5. L122
    specialize gaussian_ring_raw_add_associative (x4)
  6. L123
    specialize gaussian_ring_raw_add_associative (x5)
  7. L124
    specialize gaussian_ring_raw_add_associative (x6)
  8. L125
    specialize gaussian_ring_raw_add_associative (x7)
  9. L126
    specialize gaussian_ring_raw_add_associative (x8)
  10. L127
    specialize gaussian_ring_raw_add_associative (x9)
17Use earlier factsL128–131

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

  1. L128
    specialize gaussian_ring_raw_add_associative (x10)
  2. L129
    specialize gaussian_ring_raw_add_associative (x11)
  3. L130
    apply gaussian_ring_raw_add_associative
  4. L131
    exact ht

Library-wide reading audit

Original defined command ledger · 131 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro ab
  5. 0005intro bc
  6. 0006intro t
  7. 0007intro hAB
  8. 0008intro hABC
  9. 0009intro hBC
  10. 0010have hA : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(a,rp,rn,ip,inn)
  11. 0011specialize gaussian_valid_has_representation (a)
  12. 0012apply gaussian_valid_has_representation
  13. 0013specialize gaussian_add_input_left_valid (a)
  14. 0014specialize gaussian_add_input_left_valid (b)
  15. 0015specialize gaussian_add_input_left_valid (ab)
  16. 0016apply gaussian_add_input_left_valid
  17. 0017exact hAB
  18. 0018cases hA
  19. 0019cases hA_witness
  20. 0020cases hA_witness_witness
  21. 0021cases hA_witness_witness_witness
  22. 0022have hB : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(b,rp,rn,ip,inn)
  23. 0023specialize gaussian_valid_has_representation (b)
  24. 0024apply gaussian_valid_has_representation
  25. 0025specialize gaussian_add_input_right_valid (a)
  26. 0026specialize gaussian_add_input_right_valid (b)
  27. 0027specialize gaussian_add_input_right_valid (ab)
  28. 0028apply gaussian_add_input_right_valid
  29. 0029exact hAB
  30. 0030cases hB
  31. 0031cases hB_witness
  32. 0032cases hB_witness_witness
  33. 0033cases hB_witness_witness_witness
  34. 0034have hC : ∃ rp. ∃ rn. ∃ ip. ∃ inn. ZPairRep(c,rp,rn,ip,inn)
  35. 0035specialize gaussian_valid_has_representation (c)
  36. 0036apply gaussian_valid_has_representation
  37. 0037specialize gaussian_add_input_right_valid (ab)
  38. 0038specialize gaussian_add_input_right_valid (c)
  39. 0039specialize gaussian_add_input_right_valid (t)
  40. 0040apply gaussian_add_input_right_valid
  41. 0041exact hABC
  42. 0042cases hC
  43. 0043cases hC_witness
  44. 0044cases hC_witness_witness
  45. 0045cases hC_witness_witness_witness
  46. 0046have hab : ZPairRep(ab,x + x4,x1 + x5,x2 + x6,x3 + x7)
  47. 0047specialize gaussian_add_for_representations (a)
  48. 0048specialize gaussian_add_for_representations (b)
  49. 0049specialize gaussian_add_for_representations (ab)
  50. 0050specialize gaussian_add_for_representations (x)
  51. 0051specialize gaussian_add_for_representations (x1)
  52. 0052specialize gaussian_add_for_representations (x2)
  53. 0053specialize gaussian_add_for_representations (x3)
  54. 0054specialize gaussian_add_for_representations (x4)
  55. 0055specialize gaussian_add_for_representations (x5)
  56. 0056specialize gaussian_add_for_representations (x6)
  57. 0057specialize gaussian_add_for_representations (x7)
  58. 0058apply gaussian_add_for_representations
  59. 0059exact hA_witness_witness_witness_witness
  60. 0060exact hB_witness_witness_witness_witness
  61. 0061exact hAB
  62. 0062have hbc : ZPairRep(bc,x4 + x8,x5 + x9,x6 + x10,x7 + x11)
  63. 0063specialize gaussian_add_for_representations (b)
  64. 0064specialize gaussian_add_for_representations (c)
  65. 0065specialize gaussian_add_for_representations (bc)
  66. 0066specialize gaussian_add_for_representations (x4)
  67. 0067specialize gaussian_add_for_representations (x5)
  68. 0068specialize gaussian_add_for_representations (x6)
  69. 0069specialize gaussian_add_for_representations (x7)
  70. 0070specialize gaussian_add_for_representations (x8)
  71. 0071specialize gaussian_add_for_representations (x9)
  72. 0072specialize gaussian_add_for_representations (x10)
  73. 0073specialize gaussian_add_for_representations (x11)
  74. 0074apply gaussian_add_for_representations
  75. 0075exact hB_witness_witness_witness_witness
  76. 0076exact hC_witness_witness_witness_witness
  77. 0077exact hBC
  78. 0078have ht : ZPairRep(t,x + x4 + x8,x1 + x5 + x9,x2 + x6 + x10,x3 + x7 + x11)
  79. 0079specialize gaussian_add_for_representations (ab)
  80. 0080specialize gaussian_add_for_representations (c)
  81. 0081specialize gaussian_add_for_representations (t)
  82. 0082specialize gaussian_add_for_representations (((x) + (x4)))
  83. 0083specialize gaussian_add_for_representations (((x1) + (x5)))
  84. 0084specialize gaussian_add_for_representations (((x2) + (x6)))
  85. 0085specialize gaussian_add_for_representations (((x3) + (x7)))
  86. 0086specialize gaussian_add_for_representations (x8)
  87. 0087specialize gaussian_add_for_representations (x9)
  88. 0088specialize gaussian_add_for_representations (x10)
  89. 0089specialize gaussian_add_for_representations (x11)
  90. 0090apply gaussian_add_for_representations
  91. 0091exact hab
  92. 0092exact hC_witness_witness_witness_witness
  93. 0093exact hABC
  94. 0094specialize gaussian_add_of_representations (a)
  95. 0095specialize gaussian_add_of_representations (bc)
  96. 0096specialize gaussian_add_of_representations (t)
  97. 0097specialize gaussian_add_of_representations (x)
  98. 0098specialize gaussian_add_of_representations (x1)
  99. 0099specialize gaussian_add_of_representations (x2)
  100. 0100specialize gaussian_add_of_representations (x3)
  101. 0101specialize gaussian_add_of_representations (((x4) + (x8)))
  102. 0102specialize gaussian_add_of_representations (((x5) + (x9)))
  103. 0103specialize gaussian_add_of_representations (((x6) + (x10)))
  104. 0104specialize gaussian_add_of_representations (((x7) + (x11)))
  105. 0105apply gaussian_add_of_representations
  106. 0106exact hA_witness_witness_witness_witness
  107. 0107exact hbc
  108. 0108specialize gaussian_representation_integer_transport (t)
  109. 0109specialize gaussian_representation_integer_transport (((((x) + (x4))) + (x8)))
  110. 0110specialize gaussian_representation_integer_transport (((((x1) + (x5))) + (x9)))
  111. 0111specialize gaussian_representation_integer_transport (((((x2) + (x6))) + (x10)))
  112. 0112specialize gaussian_representation_integer_transport (((((x3) + (x7))) + (x11)))
  113. 0113specialize gaussian_representation_integer_transport (((x) + (((x4) + (x8)))))
  114. 0114specialize gaussian_representation_integer_transport (((x1) + (((x5) + (x9)))))
  115. 0115specialize gaussian_representation_integer_transport (((x2) + (((x6) + (x10)))))
  116. 0116specialize gaussian_representation_integer_transport (((x3) + (((x7) + (x11)))))
  117. 0117apply gaussian_representation_integer_transport
  118. 0118specialize gaussian_ring_raw_add_associative (x)
  119. 0119specialize gaussian_ring_raw_add_associative (x1)
  120. 0120specialize gaussian_ring_raw_add_associative (x2)
  121. 0121specialize gaussian_ring_raw_add_associative (x3)
  122. 0122specialize gaussian_ring_raw_add_associative (x4)
  123. 0123specialize gaussian_ring_raw_add_associative (x5)
  124. 0124specialize gaussian_ring_raw_add_associative (x6)
  125. 0125specialize gaussian_ring_raw_add_associative (x7)
  126. 0126specialize gaussian_ring_raw_add_associative (x8)
  127. 0127specialize gaussian_ring_raw_add_associative (x9)
  128. 0128specialize gaussian_ring_raw_add_associative (x10)
  129. 0129specialize gaussian_ring_raw_add_associative (x11)
  130. 0130apply gaussian_ring_raw_add_associative
  131. 0131exact ht