Binomial valuations · Constructive arithmetic

Kummer’s Carry Theorem

vₚ (a+b choose a) = number of base-p carries in a+b

Inspect the constructive bridge from Legendre valuations to explicitly counted addition carries.

Open the definition-aware map Read the final theorem See campaign milestone G034

Current 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.

Recommended

Defined mathematical notation

Browse 22 linked conservative definitions and 15 theorem bodies without losing their exact first-order expansions.

Browse definitions and theorems →

Focused route

Complete dependency graph

Follow the selected theorem through its constructive prerequisites, linked definitions, and original proof scripts.

Trace prerequisites →

Exact certificate

Fully expanded arithmetic

Inspect 1295 original tactic lines and 68 dependency edges with every definition fully expanded.

Open the exact edition →
Independently verified Alpha v34 checked-use theorem family: 13 displayed closed proofs among 4223 checked release theorems; not Stable: 15 theorem bodies · 22 linked definitions · 33 definition-dependency arrows · 68 proof edges · 1295 tactic lines. dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.