Complete constructive base-p digitwise congruence · Constructive arithmetic

Lucas’s Multidigit Binomial Theorem

n = Σ nᵢpⁱ · k = Σ kᵢpⁱ · (n choose k) ≡ ∏ (nᵢ choose kᵢ) (mod p)

Explore the complete unconditional constructive multidigit Lucas congruence, genuinely terminating beta-coded digit chains, exact prime-block Pascal identities, coefficient streams, and witnessed digitwise products.

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

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 20 linked conservative definitions and 64 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 3113 original tactic lines and 217 dependency edges with every definition fully expanded.

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