KU0000 · division_add_quotient_bitAdding arbitrary dividends changes the sum of their quotients by at most one carry.
layer 0 · 138 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.
KU0001 · division_add_quotient_lowerThe quotient of a sum is at least the sum of its two quotients.
layer 1 · 36 lines · Dependency-curried candidate body; not Alpha-enrolled; no checked-use authorityKU0002 · division_add_quotient_upperThe quotient of a sum is at most one above the sum of its quotients.
layer 1 · 36 lines · Dependency-curried candidate body; not Alpha-enrolled; no checked-use authorityKU0003 · choose_factorial_valuation_balanceAn arbitrary binomial valuation is the deficit between three factorial valuations.
layer 0 · 123 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU0004 · choose_legendre_valuation_balanceThe valuation of any in-range binomial coefficient is its exact Legendre-sum deficit.
layer 1 · 84 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU0005 · binomial_legendre_valuation_balanceFor C(a+b,a), the prime valuation equals the three-summand Legendre deficit.
layer 2 · 31 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU0006 · add_quotient_carry_choiceThree arbitrary power-quotient prefixes admit a constructive pointwise carry bit.
layer 1 · 105 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU0007 · add_quotient_carry_prefix_extendA three-prefix additive carry code extends by one selected terminal bit.
layer 0 · 85 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU0008 · add_quotient_carry_prefix_existsThree arbitrary power-quotient prefixes admit a beta-coded additive carry prefix.
layer 2 · 94 lines · Alpha v34 independently verified · 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.
layer 0 · 34 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableKU000A · add_quotient_carry_prefix_restrictDropping the terminal position preserves a three-prefix additive carry code.
layer 0 · 18 lines · Alpha v34 independently verified · 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.
layer 1 · 228 lines · Alpha v34 independently verified · 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.
layer 3 · 157 lines · Alpha v34 independently verified · 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.
layer 0 · 31 lines · Alpha v34 independently verified · 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.
layer 4 · 95 lines · Alpha v34 independently verified · alpha_closed; checked-use authorized; not StableExactly 13 displayed theorems have independently verified Alpha checked-use authority; none is admitted to Stable. Body-only enrollment never grants checked theorem use.