SL0000 · bounded_euler_criterion_completeComplete bounded Euler criterion, including both residue and nonresidue equivalences.
layer 0 · 36 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableCurrent 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.
SL0001 · prime_predecessor_nonzeroThe predecessor of a prime cannot be zero.
layer 0 · 10 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0002 · odd_predecessor_double_halfAn odd successor has predecessor equal to twice its odd half.
layer 0 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0003 · quadratic_supplement_minus_one_half_parityFor an odd prime, its predecessor is a quadratic residue exactly when the prime's half is even, and a nonresidue exactly when that half is odd.
layer 1 · 91 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0004 · quadratic_supplement_minus_one_residue_iff_mod_four_oneThe first supplementary law: minus one is a quadratic residue modulo an odd prime exactly when that prime is one modulo four.
layer 2 · 38 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0005 · quadratic_supplement_minus_one_nonresidue_iff_mod_four_threeThe first supplementary law's complementary branch: minus one is a nonresidue exactly for odd primes that are three modulo four.
layer 2 · 40 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0006 · quadratic_supplement_minus_one_completeComplete constructive first supplementary law, including both the one-modulo-four residue and three-modulo-four nonresidue cases.
layer 3 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0007 · bounded_gauss_lemma_completeA canonical Gauss reflection count is even exactly for residues and odd exactly for nonresidues.
layer 1 · 204 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0008 · eight_mul_eq_double_fourMultiplication by eight is twice multiplication by four.
layer 0 · 6 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL0009 · odd_mod_eight_casesEvery odd natural constructively belongs to one of the four residue classes one, three, five or seven modulo eight.
layer 1 · 47 lines · Dependency-curried candidate body; not Alpha-enrolled; no checked-use authoritySL000A · doubling_gauss_count_shape_existsThe explicit reflection-count shape for doubling exists constructively for every odd-prime half.
layer 0 · 13 lines · Dependency-curried candidate body; not Alpha-enrolled; no checked-use authoritySL000B · mod_eight_remainder_uniqueTwo bounded decompositions modulo eight have the same remainder.
layer 0 · 23 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000C · mod_eight_good_bad_exclusiveThe favorable modulo-eight classes one and seven cannot equal the unfavorable classes three and five.
layer 1 · 104 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000D · doubling_gauss_even_count_implies_good_mod_eightAn even doubling reflection count forces the prime to be one or seven modulo eight.
layer 1 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000E · doubling_gauss_odd_count_implies_bad_mod_eightAn odd doubling reflection count forces the prime to be three or five modulo eight.
layer 1 · 32 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000F · doubling_gauss_count_parity_mod_eight_completeFor the exact doubling reflection-count shape, evenness is equivalent to classes one/seven and oddness to three/five.
layer 2 · 60 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000G · doubling_floor_below_implies_double_at_most_halfA source at most the odd-half floor has doubled value at most the half.
layer 0 · 21 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000H · doubling_floor_above_implies_double_above_halfA source strictly above the odd-half floor doubles beyond the half.
layer 0 · 17 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000I · doubling_half_range_below_odd_modulusDoubling a value in the canonical half range never wraps modulo the odd modulus.
layer 0 · 18 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000J · reflected_double_above_odd_halfAn exact reflected doubled value necessarily lies above the odd half.
layer 0 · 46 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000K · doubling_gauss_initial_segment_complementFor multiplication by two, every actual Gauss sign bit is exactly complementary to the floor-half initial-segment bit.
layer 1 · 167 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000L · doubling_half_decomposition_lower_boundA natural half in either doubled decomposition is at most the full length.
layer 0 · 25 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000M · doubling_gauss_count_shape_from_initial_segment_complementThe existing initial-segment count and complementary BitCount theorems prove the exact doubling reflection-count shape once pointwise complementarity of the actual signs is supplied.
layer 1 · 80 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000N · doubling_gauss_reflection_count_shapeThe beta-coded Gauss reflection count for multiplication by two has exactly the explicit ceiling-half shape.
layer 2 · 57 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000O · quadratic_supplement_two_conditional_on_gauss_count_shapeThe exact second supplementary law follows constructively once the existing Gauss reflection count is identified with the explicit doubling-count shape.
layer 3 · 41 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000P · odd_prime_strictly_exceeds_twoEvery prime admitting an odd decomposition is strictly greater than two.
layer 0 · 20 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000Q · quadratic_supplement_two_half_completeComplete constructive second supplementary law for an explicitly decomposed odd prime, with no unproved count-shape hypothesis.
layer 4 · 71 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000R · quadratic_supplement_two_residue_iff_mod_eight_one_or_sevenThe second supplementary law: two is a quadratic residue modulo an odd prime exactly in classes one and seven modulo eight.
layer 5 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000S · quadratic_supplement_two_nonresidue_iff_mod_eight_three_or_fiveThe complementary second supplementary law: two is a nonresidue exactly in classes three and five modulo eight.
layer 5 · 14 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableSL000T · quadratic_supplement_two_completeComplete constructive second supplementary law: the quadratic residue status of two is classified exactly by the four odd classes modulo eight.
layer 6 · 12 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 28 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.