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.