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.
PD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremPD0013 · BetaAtx is the bounded beta-decoded value at index i.
conservative definition · not a theoremPD0041 · Choosez is the recurrence-defined binomial coefficient of row n and column k.
conservative definition · not a theoremPD0014 · Productz is the product of a beta-coded prefix of length l.
conservative definition · not a theoremPD0018 · RangeThe decoded prefix is a,a+1,...,a+l-1.
conservative definition · not a theoremPD0023 · Factorialz is the relational factorial of n.
conservative definition · not a theoremPD0003 · DvdThe natural number d divides n.
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 theoremPD0044 · PowerDividesThe relational power p to exponent e divides n.
conservative definition · not a theoremPD0045 · BoundedPowerValuatione is the greatest exponent at most b for which p to that exponent divides n.
conservative definition · not a theoremPD0046 · PowerValuatione is the canonical bounded p-adic power valuation of n.
conservative definition · not a theoremPD0015 · Sumz is the sum of a beta-coded prefix of length l.
conservative definition · not a theoremPD0007 · DivRemq and r are a quotient and a strict remainder for n by d.
conservative definition · not a theoremPD0049 · PowerQuotPrefixThe beta-coded prefix stores the quotients of n by the first l positive powers of p.
conservative definition · not a theoremPD0050 · LegendreSume is the finite Legendre sum of the quotients of n by positive powers of p.
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 theoremCF0005 · CarryThe sum of two natural digits is at least the base p.
conservative definition · not a theoremPD0048 · FactorialValuatione is the bounded p-adic valuation of the factorial n!.
conservative definition · not a theoremKU0000 · division_add_quotient_bitAdding arbitrary dividends changes the sum of their quotients by at most one carry.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0001 · division_add_quotient_lowerThe quotient of a sum is at least the sum of its two quotients.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityKU0002 · division_add_quotient_upperThe quotient of a sum is at most one above the sum of its quotients.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityKU0003 · choose_factorial_valuation_balanceAn arbitrary binomial valuation is the deficit between three factorial valuations.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0004 · choose_legendre_valuation_balanceThe valuation of any in-range binomial coefficient is its exact Legendre-sum deficit.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0005 · binomial_legendre_valuation_balanceFor C(a+b,a), the prime valuation equals the three-summand Legendre deficit.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0006 · add_quotient_carry_choiceThree arbitrary power-quotient prefixes admit a constructive pointwise carry bit.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0007 · add_quotient_carry_prefix_extendA three-prefix additive carry code extends by one selected terminal bit.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0008 · add_quotient_carry_prefix_existsThree arbitrary power-quotient prefixes admit a beta-coded additive carry prefix.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU0009 · add_quotient_carry_prefix_all_bitsEvery value decoded from a general additive carry prefix is zero or one.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU000A · add_quotient_carry_prefix_restrictDropping the terminal position preserves a three-prefix additive carry code.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU000B · beta_sum_add_carry_exactThe sum-prefix quotient total equals both addend totals plus the exact carry count.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU000C · kummer_binomial_carry_bit_countKummer's theorem: the valuation of C(a+b,a) is the number of base-p addition carries.
theorem body · 10 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU000D · prime_power_valuation_zero_iff_not_dividesAt a prime base and nonzero value, valuation zero is equivalent to nondivisibility.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableKU000E · kummer_carry_free_iff_not_dividesA constructed general-Kummer carry prefix has count zero exactly when p does not divide the binomial coefficient.
theorem body · 9 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not Stable