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
∃ ee_norm_rp_lowerlayer. ∃ ee_norm_rn_lowerlayer. ∃ ee_norm_ip_lowerlayer. ∃ ee_norm_in_lowerlayer. ZPairRep(z,ee_norm_rp_lowerlayer,ee_norm_rn_lowerlayer,ee_norm_ip_lowerlayer,ee_norm_in_lowerlayer) ∧ EisensteinCoordinateNorm(ee_norm_rp_lowerlayer,ee_norm_rn_lowerlayer,ee_norm_ip_lowerlayer,ee_norm_in_lowerlayer,n)Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists ee_norm_rp_lowerlayer ee_norm_rn_lowerlayer ee_norm_ip_lowerlayer ee_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))) /\ ((ee_norm_rp_lowerlayer) + ge_balance_negative_lowerlayerrepresentationreal = (ee_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))) /\ ((ee_norm_ip_lowerlayer) + ge_balance_negative_lowerlayerrepresentationimaginary = (ee_norm_in_lowerlayer) + ge_balance_positive_lowerlayerrepresentationimaginary)))))) /\ (((((((((ee_norm_rp_lowerlayer) * (ee_norm_rp_lowerlayer))) + (((ee_norm_rn_lowerlayer) * (ee_norm_rn_lowerlayer))))) + (((((ee_norm_ip_lowerlayer) * (ee_norm_ip_lowerlayer))) + (((ee_norm_in_lowerlayer) * (ee_norm_in_lowerlayer))))))) + (((((ee_norm_rp_lowerlayer) * (ee_norm_in_lowerlayer))) + (((ee_norm_rn_lowerlayer) * (ee_norm_ip_lowerlayer)))))) = ((((((((((ee_norm_rp_lowerlayer) * (ee_norm_rn_lowerlayer))) + (((ee_norm_rn_lowerlayer) * (ee_norm_rp_lowerlayer))))) + (((((ee_norm_ip_lowerlayer) * (ee_norm_in_lowerlayer))) + (((ee_norm_in_lowerlayer) * (ee_norm_ip_lowerlayer))))))) + (((((ee_norm_rp_lowerlayer) * (ee_norm_ip_lowerlayer))) + (((ee_norm_rn_lowerlayer) * (ee_norm_in_lowerlayer))))))) + (n))))The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.