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.
Definition in prerequisite notation
∃ ge_norm_rp_lowerlayer. ∃ ge_norm_rn_lowerlayer. ∃ ge_norm_ip_lowerlayer. ∃ ge_norm_in_lowerlayer. ZPairRep(z,ge_norm_rp_lowerlayer,ge_norm_rn_lowerlayer,ge_norm_ip_lowerlayer,ge_norm_in_lowerlayer) ∧ GaussianSignedNorm(ge_norm_rp_lowerlayer,ge_norm_rn_lowerlayer,ge_norm_ip_lowerlayer,ge_norm_in_lowerlayer,n)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ge_norm_rp_lowerlayer ge_norm_rn_lowerlayer ge_norm_ip_lowerlayer ge_norm_in_lowerlayer. ((exists ge_representation_real_code_lowerlayerrepresentation ge_representation_imaginary_code_lowerlayerrepresentation. (((z) = ((ge_representation_real_code_lowerlayerrepresentation) + (ge_representation_imaginary_code_lowerlayerrepresentation)) * S ((ge_representation_real_code_lowerlayerrepresentation) + (ge_representation_imaginary_code_lowerlayerrepresentation)) + ((ge_representation_imaginary_code_lowerlayerrepresentation) + (ge_representation_imaginary_code_lowerlayerrepresentation))) /\ ((exists ge_balance_positive_lowerlayerrepresentationreal ge_balance_negative_lowerlayerrepresentationreal. (((((ge_representation_real_code_lowerlayerrepresentation) = 2 * (ge_balance_positive_lowerlayerrepresentationreal) /\ (ge_balance_negative_lowerlayerrepresentationreal) = 0) \/ exists ge_signed_half_lowerlayerrepresentationrealdecode. (((ge_representation_real_code_lowerlayerrepresentation) = 2 * ge_signed_half_lowerlayerrepresentationrealdecode + 1 /\ (ge_balance_positive_lowerlayerrepresentationreal) = 0) /\ (ge_balance_negative_lowerlayerrepresentationreal) = S ge_signed_half_lowerlayerrepresentationrealdecode))) /\ ((ge_norm_rp_lowerlayer) + ge_balance_negative_lowerlayerrepresentationreal = (ge_norm_rn_lowerlayer) + ge_balance_positive_lowerlayerrepresentationreal))) /\ (exists ge_balance_positive_lowerlayerrepresentationimaginary ge_balance_negative_lowerlayerrepresentationimaginary. (((((ge_representation_imaginary_code_lowerlayerrepresentation) = 2 * (ge_balance_positive_lowerlayerrepresentationimaginary) /\ (ge_balance_negative_lowerlayerrepresentationimaginary) = 0) \/ exists ge_signed_half_lowerlayerrepresentationimaginarydecode. (((ge_representation_imaginary_code_lowerlayerrepresentation) = 2 * ge_signed_half_lowerlayerrepresentationimaginarydecode + 1 /\ (ge_balance_positive_lowerlayerrepresentationimaginary) = 0) /\ (ge_balance_negative_lowerlayerrepresentationimaginary) = S ge_signed_half_lowerlayerrepresentationimaginarydecode))) /\ ((ge_norm_ip_lowerlayer) + ge_balance_negative_lowerlayerrepresentationimaginary = (ge_norm_in_lowerlayer) + ge_balance_positive_lowerlayerrepresentationimaginary)))))) /\ (exists ge_real_square_lowerlayersquare ge_imaginary_square_lowerlayersquare. ((((((ge_norm_rp_lowerlayer) * (ge_norm_rp_lowerlayer))) + (((ge_norm_rn_lowerlayer) * (ge_norm_rn_lowerlayer)))) = ((ge_real_square_lowerlayersquare) + (((((ge_norm_rp_lowerlayer) * (ge_norm_rn_lowerlayer))) + (((ge_norm_rn_lowerlayer) * (ge_norm_rp_lowerlayer))))))) /\ ((((((ge_norm_ip_lowerlayer) * (ge_norm_ip_lowerlayer))) + (((ge_norm_in_lowerlayer) * (ge_norm_in_lowerlayer)))) = ((ge_imaginary_square_lowerlayersquare) + (((((ge_norm_ip_lowerlayer) * (ge_norm_in_lowerlayer))) + (((ge_norm_in_lowerlayer) * (ge_norm_ip_lowerlayer))))))) /\ ((n) = ge_real_square_lowerlayersquare + ge_imaginary_square_lowerlayersquare)))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.
Direct definition dependencies
Definitions depending on this notation
Checked theorems using this definition
GF0003 · gaussian_norm_input_validGF000D · gaussian_zero_normGF0010 · gaussian_one_normGF0015 · gaussian_norm_value_transportGF0016 · gaussian_norm_nonzeroGF0017 · gaussian_norm_zero_implies_code_zeroGF0018 · gaussian_code_zero_implies_norm_zeroGF0019 · gaussian_unit_has_norm_oneGF001A · gaussian_norm_one_is_unitGF001B · gaussian_unit_iff_norm_oneGF001C · gaussian_unit_decidableGF001F · gaussian_multiply_zero_implies_zero_factorGF0052 · gaussian_division_divisible_remainder_zeroGF0053 · gaussian_divides_decidableGF0059 · gaussian_associate_normGF005B · gaussian_divisor_norm_factorGF005C · gaussian_divisor_norm_boundGF0064 · gaussian_gcd_bezout_bounded_existsGF0065 · gaussian_gcd_bezout_existsGF0070 · gaussian_norm_bounded_coordinatesGF0074 · gaussian_proper_norm_divisor_decidableGF0078 · gaussian_factor_search_completeGF0079 · gaussian_search_nonunit_norm_twoGF007A · gaussian_search_norm_factors_strictGF007B · gaussian_nonunit_factor_is_proper_norm_divisorGF007D · gaussian_proper_norm_divisor_splitGF007E · gaussian_irreducible_or_strict_nonunit_factorizationGF007F · gaussian_irreducible_decidableGF0080 · gaussian_irreducible_divisor_bounded_normGF0081 · gaussian_irreducible_divisor_existsGF0082 · gaussian_nonunit_divisor_strict_quotientGF0083 · gaussian_irreducible_factor_reductionGF0094 · gaussian_irreducible_factorization_bounded_normGF0095 · gaussian_irreducible_factorization_exists