GF005B — gaussian_divisor_norm_factor

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

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

Exact theorem in conservative defined notation

∀ d. ∀ z. ∀ D. ∀ N. GDvd(d,z) → GNorm(d,D) → GNorm(z,N) → ∃ x. ∃ y. GMul(d,x,z) ∧ (GNorm(x,y) ∧ N = D · y)

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

Definition DAG

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

Actual proof prerequisites

gaussian_norm_exists · checked external prerequisite gaussian_multiply_input_right_valid gaussian_norm_functional · checked external prerequisite gaussian_norm_multiply · checked external prerequisite

Original expanded first-order statement

forall d z D N. (exists gr_quotient_norm_factor_divisor. (exists ge_first_rp_norm_factor_divisorproduct ge_first_rn_norm_factor_divisorproduct ge_first_ip_norm_factor_divisorproduct ge_first_in_norm_factor_divisorproduct ge_second_rp_norm_factor_divisorproduct ge_second_rn_norm_factor_divisorproduct ge_second_ip_norm_factor_divisorproduct ge_second_in_norm_factor_divisorproduct. ((exists ge_representation_real_code_norm_factor_divisorproductfirst ge_representation_imaginary_code_norm_factor_divisorproductfirst. (((d) = ((ge_representation_real_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst)) * S ((ge_representation_real_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst)) + ((ge_representation_imaginary_code_norm_factor_divisorproductfirst) + (ge_representation_imaginary_code_norm_factor_divisorproductfirst))) /\ ((exists ge_balance_positive_norm_factor_divisorproductfirstreal ge_balance_negative_norm_factor_divisorproductfirstreal. (((((ge_representation_real_code_norm_factor_divisorproductfirst) = 2 * (ge_balance_positive_norm_factor_divisorproductfirstreal) /\ (ge_balance_negative_norm_factor_divisorproductfirstreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductfirstrealdecode. (((ge_representation_real_code_norm_factor_divisorproductfirst) = 2 * ge_signed_half_norm_factor_divisorproductfirstrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductfirstreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductfirstreal) = S ge_signed_half_norm_factor_divisorproductfirstrealdecode))) /\ ((ge_first_rp_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductfirstreal = (ge_first_rn_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductfirstreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductfirstimaginary ge_balance_negative_norm_factor_divisorproductfirstimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductfirst) = 2 * (ge_balance_positive_norm_factor_divisorproductfirstimaginary) /\ (ge_balance_negative_norm_factor_divisorproductfirstimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductfirstimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductfirst) = 2 * ge_signed_half_norm_factor_divisorproductfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductfirstimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductfirstimaginary) = S ge_signed_half_norm_factor_divisorproductfirstimaginarydecode))) /\ ((ge_first_ip_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductfirstimaginary = (ge_first_in_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_factor_divisorproductsecond ge_representation_imaginary_code_norm_factor_divisorproductsecond. (((gr_quotient_norm_factor_divisor) = ((ge_representation_real_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond)) * S ((ge_representation_real_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond)) + ((ge_representation_imaginary_code_norm_factor_divisorproductsecond) + (ge_representation_imaginary_code_norm_factor_divisorproductsecond))) /\ ((exists ge_balance_positive_norm_factor_divisorproductsecondreal ge_balance_negative_norm_factor_divisorproductsecondreal. (((((ge_representation_real_code_norm_factor_divisorproductsecond) = 2 * (ge_balance_positive_norm_factor_divisorproductsecondreal) /\ (ge_balance_negative_norm_factor_divisorproductsecondreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductsecondrealdecode. (((ge_representation_real_code_norm_factor_divisorproductsecond) = 2 * ge_signed_half_norm_factor_divisorproductsecondrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductsecondreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductsecondreal) = S ge_signed_half_norm_factor_divisorproductsecondrealdecode))) /\ ((ge_second_rp_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductsecondreal = (ge_second_rn_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductsecondreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductsecondimaginary ge_balance_negative_norm_factor_divisorproductsecondimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductsecond) = 2 * (ge_balance_positive_norm_factor_divisorproductsecondimaginary) /\ (ge_balance_negative_norm_factor_divisorproductsecondimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductsecondimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductsecond) = 2 * ge_signed_half_norm_factor_divisorproductsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductsecondimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductsecondimaginary) = S ge_signed_half_norm_factor_divisorproductsecondimaginarydecode))) /\ ((ge_second_ip_norm_factor_divisorproduct) + ge_balance_negative_norm_factor_divisorproductsecondimaginary = (ge_second_in_norm_factor_divisorproduct) + ge_balance_positive_norm_factor_divisorproductsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_factor_divisorproductoutput ge_representation_imaginary_code_norm_factor_divisorproductoutput. (((z) = ((ge_representation_real_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput)) * S ((ge_representation_real_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput)) + ((ge_representation_imaginary_code_norm_factor_divisorproductoutput) + (ge_representation_imaginary_code_norm_factor_divisorproductoutput))) /\ ((exists ge_balance_positive_norm_factor_divisorproductoutputreal ge_balance_negative_norm_factor_divisorproductoutputreal. (((((ge_representation_real_code_norm_factor_divisorproductoutput) = 2 * (ge_balance_positive_norm_factor_divisorproductoutputreal) /\ (ge_balance_negative_norm_factor_divisorproductoutputreal) = 0) \/ exists ge_signed_half_norm_factor_divisorproductoutputrealdecode. (((ge_representation_real_code_norm_factor_divisorproductoutput) = 2 * ge_signed_half_norm_factor_divisorproductoutputrealdecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductoutputreal) = 0) /\ (ge_balance_negative_norm_factor_divisorproductoutputreal) = S ge_signed_half_norm_factor_divisorproductoutputrealdecode))) /\ ((((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))))))) + ge_balance_negative_norm_factor_divisorproductoutputreal = (((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))))))) + ge_balance_positive_norm_factor_divisorproductoutputreal))) /\ (exists ge_balance_positive_norm_factor_divisorproductoutputimaginary ge_balance_negative_norm_factor_divisorproductoutputimaginary. (((((ge_representation_imaginary_code_norm_factor_divisorproductoutput) = 2 * (ge_balance_positive_norm_factor_divisorproductoutputimaginary) /\ (ge_balance_negative_norm_factor_divisorproductoutputimaginary) = 0) \/ exists ge_signed_half_norm_factor_divisorproductoutputimaginarydecode. (((ge_representation_imaginary_code_norm_factor_divisorproductoutput) = 2 * ge_signed_half_norm_factor_divisorproductoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_divisorproductoutputimaginary) = 0) /\ (ge_balance_negative_norm_factor_divisorproductoutputimaginary) = S ge_signed_half_norm_factor_divisorproductoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))))))) + ge_balance_negative_norm_factor_divisorproductoutputimaginary = (((((((ge_first_rp_norm_factor_divisorproduct) * (ge_second_in_norm_factor_divisorproduct))) + (((ge_first_rn_norm_factor_divisorproduct) * (ge_second_ip_norm_factor_divisorproduct))))) + (((((ge_first_ip_norm_factor_divisorproduct) * (ge_second_rn_norm_factor_divisorproduct))) + (((ge_first_in_norm_factor_divisorproduct) * (ge_second_rp_norm_factor_divisorproduct))))))) + ge_balance_positive_norm_factor_divisorproductoutputimaginary)))))))))) -> (exists ge_norm_rp_norm_factor_first ge_norm_rn_norm_factor_first ge_norm_ip_norm_factor_first ge_norm_in_norm_factor_first. ((exists ge_representation_real_code_norm_factor_firstrepresentation ge_representation_imaginary_code_norm_factor_firstrepresentation. (((d) = ((ge_representation_real_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation)) * S ((ge_representation_real_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation)) + ((ge_representation_imaginary_code_norm_factor_firstrepresentation) + (ge_representation_imaginary_code_norm_factor_firstrepresentation))) /\ ((exists ge_balance_positive_norm_factor_firstrepresentationreal ge_balance_negative_norm_factor_firstrepresentationreal. (((((ge_representation_real_code_norm_factor_firstrepresentation) = 2 * (ge_balance_positive_norm_factor_firstrepresentationreal) /\ (ge_balance_negative_norm_factor_firstrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_firstrepresentationrealdecode. (((ge_representation_real_code_norm_factor_firstrepresentation) = 2 * ge_signed_half_norm_factor_firstrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_firstrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_firstrepresentationreal) = S ge_signed_half_norm_factor_firstrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_first) + ge_balance_negative_norm_factor_firstrepresentationreal = (ge_norm_rn_norm_factor_first) + ge_balance_positive_norm_factor_firstrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_firstrepresentationimaginary ge_balance_negative_norm_factor_firstrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_firstrepresentation) = 2 * (ge_balance_positive_norm_factor_firstrepresentationimaginary) /\ (ge_balance_negative_norm_factor_firstrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_firstrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_firstrepresentation) = 2 * ge_signed_half_norm_factor_firstrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_firstrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_firstrepresentationimaginary) = S ge_signed_half_norm_factor_firstrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_first) + ge_balance_negative_norm_factor_firstrepresentationimaginary = (ge_norm_in_norm_factor_first) + ge_balance_positive_norm_factor_firstrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_firstsquare ge_imaginary_square_norm_factor_firstsquare. ((((((ge_norm_rp_norm_factor_first) * (ge_norm_rp_norm_factor_first))) + (((ge_norm_rn_norm_factor_first) * (ge_norm_rn_norm_factor_first)))) = ((ge_real_square_norm_factor_firstsquare) + (((((ge_norm_rp_norm_factor_first) * (ge_norm_rn_norm_factor_first))) + (((ge_norm_rn_norm_factor_first) * (ge_norm_rp_norm_factor_first))))))) /\ ((((((ge_norm_ip_norm_factor_first) * (ge_norm_ip_norm_factor_first))) + (((ge_norm_in_norm_factor_first) * (ge_norm_in_norm_factor_first)))) = ((ge_imaginary_square_norm_factor_firstsquare) + (((((ge_norm_ip_norm_factor_first) * (ge_norm_in_norm_factor_first))) + (((ge_norm_in_norm_factor_first) * (ge_norm_ip_norm_factor_first))))))) /\ ((D) = ge_real_square_norm_factor_firstsquare + ge_imaginary_square_norm_factor_firstsquare)))))) -> (exists ge_norm_rp_norm_factor_total ge_norm_rn_norm_factor_total ge_norm_ip_norm_factor_total ge_norm_in_norm_factor_total. ((exists ge_representation_real_code_norm_factor_totalrepresentation ge_representation_imaginary_code_norm_factor_totalrepresentation. (((z) = ((ge_representation_real_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation)) * S ((ge_representation_real_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation)) + ((ge_representation_imaginary_code_norm_factor_totalrepresentation) + (ge_representation_imaginary_code_norm_factor_totalrepresentation))) /\ ((exists ge_balance_positive_norm_factor_totalrepresentationreal ge_balance_negative_norm_factor_totalrepresentationreal. (((((ge_representation_real_code_norm_factor_totalrepresentation) = 2 * (ge_balance_positive_norm_factor_totalrepresentationreal) /\ (ge_balance_negative_norm_factor_totalrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_totalrepresentationrealdecode. (((ge_representation_real_code_norm_factor_totalrepresentation) = 2 * ge_signed_half_norm_factor_totalrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_totalrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_totalrepresentationreal) = S ge_signed_half_norm_factor_totalrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_total) + ge_balance_negative_norm_factor_totalrepresentationreal = (ge_norm_rn_norm_factor_total) + ge_balance_positive_norm_factor_totalrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_totalrepresentationimaginary ge_balance_negative_norm_factor_totalrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_totalrepresentation) = 2 * (ge_balance_positive_norm_factor_totalrepresentationimaginary) /\ (ge_balance_negative_norm_factor_totalrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_totalrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_totalrepresentation) = 2 * ge_signed_half_norm_factor_totalrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_totalrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_totalrepresentationimaginary) = S ge_signed_half_norm_factor_totalrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_total) + ge_balance_negative_norm_factor_totalrepresentationimaginary = (ge_norm_in_norm_factor_total) + ge_balance_positive_norm_factor_totalrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_totalsquare ge_imaginary_square_norm_factor_totalsquare. ((((((ge_norm_rp_norm_factor_total) * (ge_norm_rp_norm_factor_total))) + (((ge_norm_rn_norm_factor_total) * (ge_norm_rn_norm_factor_total)))) = ((ge_real_square_norm_factor_totalsquare) + (((((ge_norm_rp_norm_factor_total) * (ge_norm_rn_norm_factor_total))) + (((ge_norm_rn_norm_factor_total) * (ge_norm_rp_norm_factor_total))))))) /\ ((((((ge_norm_ip_norm_factor_total) * (ge_norm_ip_norm_factor_total))) + (((ge_norm_in_norm_factor_total) * (ge_norm_in_norm_factor_total)))) = ((ge_imaginary_square_norm_factor_totalsquare) + (((((ge_norm_ip_norm_factor_total) * (ge_norm_in_norm_factor_total))) + (((ge_norm_in_norm_factor_total) * (ge_norm_ip_norm_factor_total))))))) /\ ((N) = ge_real_square_norm_factor_totalsquare + ge_imaginary_square_norm_factor_totalsquare)))))) -> exists q Q. ((exists ge_first_rp_norm_factor_product ge_first_rn_norm_factor_product ge_first_ip_norm_factor_product ge_first_in_norm_factor_product ge_second_rp_norm_factor_product ge_second_rn_norm_factor_product ge_second_ip_norm_factor_product ge_second_in_norm_factor_product. ((exists ge_representation_real_code_norm_factor_productfirst ge_representation_imaginary_code_norm_factor_productfirst. (((d) = ((ge_representation_real_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst)) * S ((ge_representation_real_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst)) + ((ge_representation_imaginary_code_norm_factor_productfirst) + (ge_representation_imaginary_code_norm_factor_productfirst))) /\ ((exists ge_balance_positive_norm_factor_productfirstreal ge_balance_negative_norm_factor_productfirstreal. (((((ge_representation_real_code_norm_factor_productfirst) = 2 * (ge_balance_positive_norm_factor_productfirstreal) /\ (ge_balance_negative_norm_factor_productfirstreal) = 0) \/ exists ge_signed_half_norm_factor_productfirstrealdecode. (((ge_representation_real_code_norm_factor_productfirst) = 2 * ge_signed_half_norm_factor_productfirstrealdecode + 1 /\ (ge_balance_positive_norm_factor_productfirstreal) = 0) /\ (ge_balance_negative_norm_factor_productfirstreal) = S ge_signed_half_norm_factor_productfirstrealdecode))) /\ ((ge_first_rp_norm_factor_product) + ge_balance_negative_norm_factor_productfirstreal = (ge_first_rn_norm_factor_product) + ge_balance_positive_norm_factor_productfirstreal))) /\ (exists ge_balance_positive_norm_factor_productfirstimaginary ge_balance_negative_norm_factor_productfirstimaginary. (((((ge_representation_imaginary_code_norm_factor_productfirst) = 2 * (ge_balance_positive_norm_factor_productfirstimaginary) /\ (ge_balance_negative_norm_factor_productfirstimaginary) = 0) \/ exists ge_signed_half_norm_factor_productfirstimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productfirst) = 2 * ge_signed_half_norm_factor_productfirstimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productfirstimaginary) = 0) /\ (ge_balance_negative_norm_factor_productfirstimaginary) = S ge_signed_half_norm_factor_productfirstimaginarydecode))) /\ ((ge_first_ip_norm_factor_product) + ge_balance_negative_norm_factor_productfirstimaginary = (ge_first_in_norm_factor_product) + ge_balance_positive_norm_factor_productfirstimaginary)))))) /\ ((exists ge_representation_real_code_norm_factor_productsecond ge_representation_imaginary_code_norm_factor_productsecond. (((q) = ((ge_representation_real_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond)) * S ((ge_representation_real_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond)) + ((ge_representation_imaginary_code_norm_factor_productsecond) + (ge_representation_imaginary_code_norm_factor_productsecond))) /\ ((exists ge_balance_positive_norm_factor_productsecondreal ge_balance_negative_norm_factor_productsecondreal. (((((ge_representation_real_code_norm_factor_productsecond) = 2 * (ge_balance_positive_norm_factor_productsecondreal) /\ (ge_balance_negative_norm_factor_productsecondreal) = 0) \/ exists ge_signed_half_norm_factor_productsecondrealdecode. (((ge_representation_real_code_norm_factor_productsecond) = 2 * ge_signed_half_norm_factor_productsecondrealdecode + 1 /\ (ge_balance_positive_norm_factor_productsecondreal) = 0) /\ (ge_balance_negative_norm_factor_productsecondreal) = S ge_signed_half_norm_factor_productsecondrealdecode))) /\ ((ge_second_rp_norm_factor_product) + ge_balance_negative_norm_factor_productsecondreal = (ge_second_rn_norm_factor_product) + ge_balance_positive_norm_factor_productsecondreal))) /\ (exists ge_balance_positive_norm_factor_productsecondimaginary ge_balance_negative_norm_factor_productsecondimaginary. (((((ge_representation_imaginary_code_norm_factor_productsecond) = 2 * (ge_balance_positive_norm_factor_productsecondimaginary) /\ (ge_balance_negative_norm_factor_productsecondimaginary) = 0) \/ exists ge_signed_half_norm_factor_productsecondimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productsecond) = 2 * ge_signed_half_norm_factor_productsecondimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productsecondimaginary) = 0) /\ (ge_balance_negative_norm_factor_productsecondimaginary) = S ge_signed_half_norm_factor_productsecondimaginarydecode))) /\ ((ge_second_ip_norm_factor_product) + ge_balance_negative_norm_factor_productsecondimaginary = (ge_second_in_norm_factor_product) + ge_balance_positive_norm_factor_productsecondimaginary)))))) /\ (exists ge_representation_real_code_norm_factor_productoutput ge_representation_imaginary_code_norm_factor_productoutput. (((z) = ((ge_representation_real_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput)) * S ((ge_representation_real_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput)) + ((ge_representation_imaginary_code_norm_factor_productoutput) + (ge_representation_imaginary_code_norm_factor_productoutput))) /\ ((exists ge_balance_positive_norm_factor_productoutputreal ge_balance_negative_norm_factor_productoutputreal. (((((ge_representation_real_code_norm_factor_productoutput) = 2 * (ge_balance_positive_norm_factor_productoutputreal) /\ (ge_balance_negative_norm_factor_productoutputreal) = 0) \/ exists ge_signed_half_norm_factor_productoutputrealdecode. (((ge_representation_real_code_norm_factor_productoutput) = 2 * ge_signed_half_norm_factor_productoutputrealdecode + 1 /\ (ge_balance_positive_norm_factor_productoutputreal) = 0) /\ (ge_balance_negative_norm_factor_productoutputreal) = S ge_signed_half_norm_factor_productoutputrealdecode))) /\ ((((((((ge_first_rp_norm_factor_product) * (ge_second_rp_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_rn_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_in_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_ip_norm_factor_product))))))) + ge_balance_negative_norm_factor_productoutputreal = (((((((ge_first_rp_norm_factor_product) * (ge_second_rn_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_rp_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_ip_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_in_norm_factor_product))))))) + ge_balance_positive_norm_factor_productoutputreal))) /\ (exists ge_balance_positive_norm_factor_productoutputimaginary ge_balance_negative_norm_factor_productoutputimaginary. (((((ge_representation_imaginary_code_norm_factor_productoutput) = 2 * (ge_balance_positive_norm_factor_productoutputimaginary) /\ (ge_balance_negative_norm_factor_productoutputimaginary) = 0) \/ exists ge_signed_half_norm_factor_productoutputimaginarydecode. (((ge_representation_imaginary_code_norm_factor_productoutput) = 2 * ge_signed_half_norm_factor_productoutputimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_productoutputimaginary) = 0) /\ (ge_balance_negative_norm_factor_productoutputimaginary) = S ge_signed_half_norm_factor_productoutputimaginarydecode))) /\ ((((((((ge_first_rp_norm_factor_product) * (ge_second_ip_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_in_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_rp_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_rn_norm_factor_product))))))) + ge_balance_negative_norm_factor_productoutputimaginary = (((((((ge_first_rp_norm_factor_product) * (ge_second_in_norm_factor_product))) + (((ge_first_rn_norm_factor_product) * (ge_second_ip_norm_factor_product))))) + (((((ge_first_ip_norm_factor_product) * (ge_second_rn_norm_factor_product))) + (((ge_first_in_norm_factor_product) * (ge_second_rp_norm_factor_product))))))) + ge_balance_positive_norm_factor_productoutputimaginary))))))))) /\ ((exists ge_norm_rp_norm_factor_quotient ge_norm_rn_norm_factor_quotient ge_norm_ip_norm_factor_quotient ge_norm_in_norm_factor_quotient. ((exists ge_representation_real_code_norm_factor_quotientrepresentation ge_representation_imaginary_code_norm_factor_quotientrepresentation. (((q) = ((ge_representation_real_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation)) * S ((ge_representation_real_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation)) + ((ge_representation_imaginary_code_norm_factor_quotientrepresentation) + (ge_representation_imaginary_code_norm_factor_quotientrepresentation))) /\ ((exists ge_balance_positive_norm_factor_quotientrepresentationreal ge_balance_negative_norm_factor_quotientrepresentationreal. (((((ge_representation_real_code_norm_factor_quotientrepresentation) = 2 * (ge_balance_positive_norm_factor_quotientrepresentationreal) /\ (ge_balance_negative_norm_factor_quotientrepresentationreal) = 0) \/ exists ge_signed_half_norm_factor_quotientrepresentationrealdecode. (((ge_representation_real_code_norm_factor_quotientrepresentation) = 2 * ge_signed_half_norm_factor_quotientrepresentationrealdecode + 1 /\ (ge_balance_positive_norm_factor_quotientrepresentationreal) = 0) /\ (ge_balance_negative_norm_factor_quotientrepresentationreal) = S ge_signed_half_norm_factor_quotientrepresentationrealdecode))) /\ ((ge_norm_rp_norm_factor_quotient) + ge_balance_negative_norm_factor_quotientrepresentationreal = (ge_norm_rn_norm_factor_quotient) + ge_balance_positive_norm_factor_quotientrepresentationreal))) /\ (exists ge_balance_positive_norm_factor_quotientrepresentationimaginary ge_balance_negative_norm_factor_quotientrepresentationimaginary. (((((ge_representation_imaginary_code_norm_factor_quotientrepresentation) = 2 * (ge_balance_positive_norm_factor_quotientrepresentationimaginary) /\ (ge_balance_negative_norm_factor_quotientrepresentationimaginary) = 0) \/ exists ge_signed_half_norm_factor_quotientrepresentationimaginarydecode. (((ge_representation_imaginary_code_norm_factor_quotientrepresentation) = 2 * ge_signed_half_norm_factor_quotientrepresentationimaginarydecode + 1 /\ (ge_balance_positive_norm_factor_quotientrepresentationimaginary) = 0) /\ (ge_balance_negative_norm_factor_quotientrepresentationimaginary) = S ge_signed_half_norm_factor_quotientrepresentationimaginarydecode))) /\ ((ge_norm_ip_norm_factor_quotient) + ge_balance_negative_norm_factor_quotientrepresentationimaginary = (ge_norm_in_norm_factor_quotient) + ge_balance_positive_norm_factor_quotientrepresentationimaginary)))))) /\ (exists ge_real_square_norm_factor_quotientsquare ge_imaginary_square_norm_factor_quotientsquare. ((((((ge_norm_rp_norm_factor_quotient) * (ge_norm_rp_norm_factor_quotient))) + (((ge_norm_rn_norm_factor_quotient) * (ge_norm_rn_norm_factor_quotient)))) = ((ge_real_square_norm_factor_quotientsquare) + (((((ge_norm_rp_norm_factor_quotient) * (ge_norm_rn_norm_factor_quotient))) + (((ge_norm_rn_norm_factor_quotient) * (ge_norm_rp_norm_factor_quotient))))))) /\ ((((((ge_norm_ip_norm_factor_quotient) * (ge_norm_ip_norm_factor_quotient))) + (((ge_norm_in_norm_factor_quotient) * (ge_norm_in_norm_factor_quotient)))) = ((ge_imaginary_square_norm_factor_quotientsquare) + (((((ge_norm_ip_norm_factor_quotient) * (ge_norm_in_norm_factor_quotient))) + (((ge_norm_in_norm_factor_quotient) * (ge_norm_ip_norm_factor_quotient))))))) /\ ((Q) = ge_real_square_norm_factor_quotientsquare + ge_imaginary_square_norm_factor_quotientsquare)))))) /\ (N=D*Q)))

Complete tactic proof in conservative notation

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

37 script commands · 10 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)

gaussian multiply input right valid

01Fix variables and assumptionsL1–7

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

L1
intro d
L2
intro z
L3
intro D
L4
intro N
L5
intro hdiv
L6
intro hd
L7
intro hz

02Separate the logical casesL8–8

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

L8
cases hdiv

03Establish hnL9–16

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

L9
have hn : ∃ Q. GNorm(x,Q)Definitions: GNorm(x,Q)Original native command in the exact edition
L10
specialize gaussian_norm_exists (x)
L11
apply gaussian_norm_exists
L12
specialize gaussian_multiply_input_right_valid (d)
L13
specialize gaussian_multiply_input_right_valid (x)
L14
specialize gaussian_multiply_input_right_valid (z)
L15
apply gaussian_multiply_input_right_valid
L16
exact hdiv_witness

04Separate the logical casesL17–17

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

L17
cases hn

05Construct an explicit witnessL18–19

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

L18
exists (x)
L19
exists (x1)

06Separate the logical casesL20–20

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

L20
split

07Use earlier factsL21–21

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

L21
exact hdiv_witness

08Separate the logical casesL22–22

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

L22
split

09Use earlier factsL23–32

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

L23
exact hn_witness
L24
specialize gaussian_norm_functional (z)
L25
specialize gaussian_norm_functional (N)
L26
specialize gaussian_norm_functional (D*x1)
L27
apply gaussian_norm_functional
L28
exact hz
L29
specialize gaussian_norm_multiply (d)
L30
specialize gaussian_norm_multiply (x)
L31
specialize gaussian_norm_multiply (z)
L32
specialize gaussian_norm_multiply (D)

10Use earlier factsL33–37

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

L33
specialize gaussian_norm_multiply (x1)
L34
apply gaussian_norm_multiply
L35
exact hd
L36
exact hn_witness
L37
exact hdiv_witness

Library-wide reading audit

Original defined command ledger · 37 lines

0001intro d
0002intro z
0003intro D
0004intro N
0005intro hdiv
0006intro hd
0007intro hz
0008cases hdiv
0009have hn : ∃ Q. GNorm(x,Q)
0010specialize gaussian_norm_exists (x)
0011apply gaussian_norm_exists
0012specialize gaussian_multiply_input_right_valid (d)
0013specialize gaussian_multiply_input_right_valid (x)
0014specialize gaussian_multiply_input_right_valid (z)
0015apply gaussian_multiply_input_right_valid
0016exact hdiv_witness
0017cases hn
0018exists (x)
0019exists (x1)
0020split
0021exact hdiv_witness
0022split
0023exact hn_witness
0024specialize gaussian_norm_functional (z)
0025specialize gaussian_norm_functional (N)
0026specialize gaussian_norm_functional (D*x1)
0027apply gaussian_norm_functional
0028exact hz
0029specialize gaussian_norm_multiply (d)
0030specialize gaussian_norm_multiply (x)
0031specialize gaussian_norm_multiply (z)
0032specialize gaussian_norm_multiply (D)
0033specialize gaussian_norm_multiply (x1)
0034apply gaussian_norm_multiply
0035exact hd
0036exact hn_witness
0037exact hdiv_witness