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
∃ gr_search_real_gaussianfactorization. ∃ gr_search_imaginary_gaussianfactorization. NaturalPair(z,gr_search_real_gaussianfactorization,gr_search_imaginary_gaussianfactorization) ∧ (Le(gr_search_real_gaussianfactorization,2 · N) ∧ Le(gr_search_imaginary_gaussianfactorization,2 · N))Only definitions earlier in this acyclic notation graph are used here.
Hygienic expanded first-order definition
exists gr_search_real_gaussianfactorization gr_search_imaginary_gaussianfactorization. ((((z))=((gr_search_real_gaussianfactorization) + (gr_search_imaginary_gaussianfactorization)) * S ((gr_search_real_gaussianfactorization) + (gr_search_imaginary_gaussianfactorization)) + ((gr_search_imaginary_gaussianfactorization) + (gr_search_imaginary_gaussianfactorization))) /\ ((exists ge_gap_gaussianfactorizationreal_bound. ge_gap_gaussianfactorizationreal_bound + (gr_search_real_gaussianfactorization) = (2*((N)))) /\ (exists ge_gap_gaussianfactorizationimaginary_bound. ge_gap_gaussianfactorizationimaginary_bound + (gr_search_imaginary_gaussianfactorization) = (2*((N))))))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
none