PD0004 · Primep is nonunit and every factorization of p has a unit factor.
conservative definition · not a theoremCurrent 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.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.
PD0010 · Oddn has an odd decomposition.
conservative definition · not a theoremPD0009 · Evenn has an even decomposition.
conservative definition · not a theoremPD0011 · Mod4Onen is one modulo four by an explicit quotient.
conservative definition · not a theoremPD0012 · Mod4Threen is three modulo four by an explicit quotient.
conservative definition · not a theoremPD0008 · ModEqBalanced-natural congruence modulo m.
conservative definition · not a theoremPD0021 · QResa has a square root modulo m.
conservative definition · not a theoremPD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremPD0022 · BoundedQResa has a square root strictly below m modulo m.
conservative definition · not a theoremPD0013 · BetaAtx is the bounded beta-decoded value at index i.
conservative definition · not a theoremPD0015 · Sumz is the sum of a beta-coded prefix of length l.
conservative definition · not a theoremPD0016 · AllBitsEvery decoded entry below l is zero or one.
conservative definition · not a theoremPD0017 · BitCountz is the sum of a beta-coded all-bit prefix.
conservative definition · not a theoremCF0006 · Mod8Onep is one modulo eight with a witnessed quotient.
conservative definition · not a theoremCF0007 · Mod8Threep is three modulo eight with a witnessed quotient.
conservative definition · not a theoremCF0008 · Mod8Fivep is five modulo eight with a witnessed quotient.
conservative definition · not a theoremCF0009 · Mod8Sevenp is seven modulo eight with a witnessed quotient.
conservative definition · not a theoremPD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0003 · DvdThe natural number d divides n.
conservative definition · not a theoremPD0018 · RangeThe decoded prefix is a,a+1,...,a+l-1.
conservative definition · not a theoremPD0014 · Productz is the product of a beta-coded prefix of length l.
conservative definition · not a theoremPD0019 · RepeatThe decoded prefix repeats a for l positions.
conservative definition · not a theoremPD0020 · Powz is the relational e-th power of a.
conservative definition · not a theoremSL0000 · bounded_euler_criterion_completeComplete bounded Euler criterion, including both residue and nonresidue equivalences.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL0001 · prime_predecessor_nonzeroThe predecessor of a prime cannot be zero.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL0002 · odd_predecessor_double_halfAn odd successor has predecessor equal to twice its odd half.
theorem body · 0 linked definitions · Alpha v30 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.
theorem body · 7 linked definitions · Alpha v30 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.
theorem body · 5 linked definitions · Alpha v30 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.
theorem body · 5 linked definitions · Alpha v30 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.
theorem body · 5 linked definitions · Alpha v30 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.
theorem body · 12 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL0008 · eight_mul_eq_double_fourMultiplication by eight is twice multiplication by four.
theorem body · 0 linked definitions · Alpha v30 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.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authoritySL000A · doubling_gauss_count_shape_existsThe explicit reflection-count shape for doubling exists constructively for every odd-prime half.
theorem body · 0 linked definitions · unenrolled candidate · no checked-use authoritySL000B · mod_eight_remainder_uniqueTwo bounded decompositions modulo eight have the same remainder.
theorem body · 1 linked definitions · Alpha v30 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.
theorem body · 0 linked definitions · Alpha v30 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.
theorem body · 2 linked definitions · Alpha v30 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.
theorem body · 2 linked definitions · Alpha v30 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.
theorem body · 2 linked definitions · Alpha v30 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.
theorem body · 1 linked definitions · Alpha v30 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.
theorem body · 1 linked definitions · Alpha v30 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.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL000J · reflected_double_above_odd_halfAn exact reflected doubled value necessarily lies above the odd half.
theorem body · 2 linked definitions · Alpha v30 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.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL000L · doubling_half_decomposition_lower_boundA natural half in either doubled decomposition is at most the full length.
theorem body · 1 linked definitions · Alpha v30 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.
theorem body · 4 linked definitions · Alpha v30 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.
theorem body · 6 linked definitions · Alpha v30 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.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableSL000P · odd_prime_strictly_exceeds_twoEvery prime admitting an odd decomposition is strictly greater than two.
theorem body · 2 linked definitions · Alpha v30 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.
theorem body · 10 linked definitions · Alpha v30 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.
theorem body · 3 linked definitions · Alpha v30 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.
theorem body · 3 linked definitions · Alpha v30 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.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not Stable