MK0001 beta_valuation_prefix_emptyEvery empty decoded list has an empty bounded-valuation table.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; 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.
MK0002 beta_valuation_prefix_drop_lastA finite valuation table restricts to its predecessor prefix.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0003 beta_valuation_prefix_lastEach actual last table entry has the exact canonical valuation of its actual decoded factor.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0004 beta_valuation_prefix_extendAppend an actual valuation and recode the complete finite table with all prior entries preserved.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0005 beta_valuation_prefix_existsEvery finite decoded list has a genuinely constructed finite table of bounded power valuations.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0006 beta_prime_product_valuation_eq_sumFor a prime and any nonzero finite factor list, the exact product valuation equals the finite sum of its actual factor valuations.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0007 beta_prime_product_valuation_from_sumA real finite sum of factor valuations constructs the exact valuation of their nonzero product.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0008 multinomial_binomial_prefix_emptyThe empty multinomial factor prefix requires no binomial entries.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0009 multinomial_binomial_prefix_drop_lastA complete binomial factor table restricts to the predecessor prefix.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000A multinomial_binomial_prefix_extendAppend one actual binomial factor while preserving every previously coded factor.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000B multinomial_binomial_prefix_existsConstruct all actual binomial factors for any finite decoded part and partial-sum tables.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000C multinomial_binomial_prefix_nonzeroEvery actual multinomial binomial factor is strictly nonzero, including zero-valued input parts.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000D multinomial_exists_of_sumAn actual finite sum of parts has an actual iterated-binomial multinomial coefficient.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000E multinomial_existsEvery finite natural part list, including the empty list, has a witnessed total and multinomial coefficient.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK000F multinomial_nonzeroAn actual multinomial coefficient is always nonzero; no undefined zero valuation is used in Kummer's theorem.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0010 multinomial_valuations_give_carry_prefixApply the actual checked binary Kummer proof to every decoded addition row; the resulting certificate contains real quotient columns and carry bits.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0011 multinomial_kummer_carry_valuationFor every prime and every finite natural part list, an actual multinomial coefficient has a constructed exact valuation equal to all witnessed column carries; the empty list and zero parts are included.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0012 multinomial_empty_valuesThe empty multinomial has exactly total zero and coefficient one.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StableMK0013 multinomial_empty_carry_countAn actual empty finite addition has exactly zero column carries, with no prime-base assumption needed.
Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not StablePD0013 BetaAt(b,c,i,x)x is the bounded beta-decoded value at index i.
Conservative definition · notation layer 0PD0002 Lt(a,b)Witness-defined strict order on natural numbers.
Conservative definition · notation layer 0ND0075 BetaSumTrace(b,c,l,n,sb,sc)Actual running-sum beta trace: zero initially, each decoded input is added once, and the terminal value is n.
Conservative definition · notation layer 1PD0001 Le(a,b)Witness-defined non-strict order on natural numbers.
Conservative definition · notation layer 0PD0003 Dvd(d,n)The natural number d divides n.
Conservative definition · notation layer 0PD0014 Product(b,c,l,z)z is the product of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0019 Repeat(b,c,a,l)The decoded prefix repeats a for l positions.
Conservative definition · notation layer 1PD0020 Pow(a,e,z)z is the relational e-th power of a.
Conservative definition · notation layer 2PD0044 PowerDivides(p,e,n)The relational power p to exponent e divides n.
Conservative definition · notation layer 3PD0045 BoundedPowerValuation(p,n,b,e)e is the greatest exponent at most b for which p to that exponent divides n.
Conservative definition · notation layer 4PD0046 PowerValuation(p,n,e)e is the canonical bounded p-adic power valuation of n.
Conservative definition · notation layer 5ND0087 BetaValuationPrefix(p,b,c,vb,vc,l)A beta table of the exact inherited bounded power valuations of the actual decoded factors; product additivity separately requires nonzero factors.
Conservative definition · notation layer 6PD0041 Choose(n,k,z)z is the recurrence-defined binomial coefficient of row n and column k.
Conservative definition · notation layer 1ND0088 MultinomialBinomialPrefix(b,c,sb,sc,cb,cc,l)The actual factor at each position is Choose(previous total + next part, previous total).
Conservative definition · notation layer 2ND0089 Multinomial(b,c,l,n,z)An actual list of parts with total n, a running sum, and the finite product of its iterated binomial factors; the empty product is one.
Conservative definition · notation layer 3ND0090 BinaryAddCarryPrefix(lb,lc,rb,rc,tb,tc,cb,cc,l)Actual zero/one carry rows relate the decoded left, right, and total quotient columns.
Conservative definition · notation layer 1PD0007 DivRem(n,d,q,r)q and r are a quotient and a strict remainder for n by d.
Conservative definition · notation layer 1PD0049 PowerQuotPrefix(p,n,b,c,l)The beta-coded prefix stores the quotients of n by the first l positive powers of p.
Conservative definition · notation layer 3PD0015 Sum(b,c,l,z)z is the sum of a beta-coded prefix of length l.
Conservative definition · notation layer 1PD0016 AllBits(b,c,l)Every decoded entry below l is zero or one.
Conservative definition · notation layer 1PD0017 BitCount(b,c,l,z)z is the sum of a beta-coded all-bit prefix.
Conservative definition · notation layer 2ND0091 BinaryColumnCarryCount(p,a,b,e)Actual base-p quotient columns, their binary addition carry bits, and the witnessed total number e of those bits.
Conservative definition · notation layer 4ND0092 MultinomialCarryPrefix(p,b,c,sb,sc,vb,vc,l)An actual binary column-carry count for each successive addition of a part to its previous running total.
Conservative definition · notation layer 5ND0093 CarryCountMany(p,b,c,l,e)The sum of all actual column-carry counts in sequential addition of a finite list; this definition contains no coefficient or valuation.
Conservative definition · notation layer 6PD0004 Prime(p)p is nonunit and every factorization of p has a unit factor.
Conservative definition · notation layer 0PD0047 PrimePowerValuation(p,n,e)p is prime, n is nonzero, and e is the bounded p-adic valuation of n.
Conservative definition · notation layer 6Only proof arrows are theorem dependencies. Definition arrows are hygienic abbreviations of exact first-order formulas and introduce no axiom or kernel symbol.