Lucas’s Multidigit Binomial Theorem — Exact Proof Explorer

For two genuine base-p digits, an addition carry forces p to divide their relational binomial coefficient.

Every interior coefficient in prime Pascal row p is divisible by p.

Every prime divisor of a relational binomial coefficient is at most its Pascal-row index.

For two base-p digits, carrying is equivalent to prime divisibility of their binomial coefficient.

For two base-p digits, a carry-free sum is equivalent to constructive nondivisibility of their binomial coefficient.

Every natural value has an actual quotient and strictly bounded base-p digit for every nonzero base.

Every prime base constructively provides a quotient and canonical least-significant digit for every natural.

Both the quotient and the bounded base-p digit are constructively functional.

A value strictly below its base has quotient zero and itself as its unique canonical digit.

The canonical least-significant base-p digit is zero exactly when its value is divisible by p.

Every finite beta-coded natural prefix has actual beta-coded quotient and least-significant digit prefixes for each nonzero base.

Every prime base constructively digitizes an entire finite beta-coded source prefix.

At every source beta index, the quotient and digit beta prefixes expose the unique actual quotient/digit witnesses of that source value.

Every nonzero base constructively extracts two genuinely successive digits: the second source is exactly the first quotient.

Every prime base constructively provides two coherent successive digits and their remaining quotient.

Two coherent bounded base-p digits reconstruct the exact natural n = p²*q1 + p*d1 + d0 without introducing exponentiation.

The initial coefficient of every relational Pascal row is exactly one.

The terminal coefficient of every relational Pascal row is exactly one.

Every prime Pascal row has exact boundary coefficients one and every interior coefficient divisible by its prime modulus.

A positive lower base quotient makes its full index strictly greater than every bounded upper digit.

A binomial row consisting of one upper digit vanishes at every index with positive lower base quotient.

The zero-upper-quotient boundary of the Lucas prime block is constructively zero in every positive lower-quotient column.

The complete prime-base Lucas one-digit block congruence holds for arbitrary upper and lower quotients and both bounded digits.

Every actual prime-base division of the upper and lower indices satisfies the complete Lucas quotient-times-digit binomial congruence.

Relational binomial coefficients transport constructively along equality of their lower indices.

Every relational binomial coefficient with a witnessed zero lower index is exactly one.

A positive lower index forces the zeroth Pascal-row coefficient to vanish.

An explicit divisibility witness gives a balanced natural congruence to zero.

Every nonzero digit strictly below its prime base has a complementary digit strictly below that base.

Every nonboundary coefficient of the prime Pascal row is constructively congruent to zero.

Exact Pascal recurrence transports two balanced coefficient congruences to their successor-row sum.

The predecessor of a nonzero digit strictly below the base remains strictly below the base.

Every below-base coefficient of row p+a is congruent modulo prime p to the corresponding coefficient of row a, by constructive Pascal induction.

Adding a natural index to a nonzero prime never produces zero.

Adding a witnessed positive natural strictly increases a natural value.

For every unrestricted upper offset and column index, shifting a Pascal row by a prime adds exactly the original coefficient and its prime-shifted predecessor modulo that prime.

The zero prime-block quotient leaves its additive tail unchanged.

A successor prime-block quotient is exactly one prime shift of its predecessor.

Every below-base binomial column is invariant modulo a prime under an arbitrary number of prime-row shifts.

The exact Lucas congruence holds for every natural upper quotient and every lower index consisting of one base-prime digit.

The full quotient-times-digit Lucas product formula is kernel-checked whenever the lower quotient is zero, for unrestricted upper quotient.

Every natural is the zeroth decoded entry of an actual beta-coded quotient stream.

A decoded initial quotient constructively supplies the empty coherent digit chain.

An actual initial quotient code and arbitrary empty digit code exist for every natural.

One constructive quotient division and two beta-prefix extensions append the next genuinely successive digit without disturbing any earlier step.

Every nonzero base and natural input possess a coherent successive quotient/digit chain of every finite requested length.

Every prime modulus admits arbitrarily long coherent constructive beta-coded base-p digit streams.

The zeroth quotient of every coherent beta-coded digit trace is exactly its original natural input.

Every position below an arbitrary finite chain length exposes its actual consecutive quotients and bounded base-p digit.

Any beta-coded chain of pointwise backward modular recurrences folds into the exact terminal value times the entire beta-coded finite product.

Any pair of beta-coded source streams has a constructively empty relational-Choose coefficient prefix.

Beta-prefix extension and relational binomial totality append the exact coefficient for the next two decoded source entries.

Every pair of beta-coded natural source streams has an actual beta-coded relational-binomial coefficient stream of every finite length.

Every independently supplied decoded upper index, lower index, and coefficient satisfies the exact relational binomial theorem at that prefix position.

A universal one-step Lucas prime-block law implies the full arbitrary-length beta-coded digit product congruence with its exact terminal binomial factor.

For genuinely terminating quotient chains the full multidigit Lucas congruence is exactly the product of their beta-coded digit binomial coefficients, conditional solely on its explicit one-step law.

For a prime base every nonzero successive digit quotient is strictly below its predecessor natural.

Any nonzero quotient at chain position i obeys the constructive global bound q+i<=n.

Every prime-base digit trace longer than its original natural has an actual terminal quotient equal to zero.

For every prime base and every length strictly above n, a genuinely coherent beta-coded digit chain exists and provably terminates with quotient zero.

Unconditional full multidigit Lucas congruence: every actual beta-coded coherent digit pair has coefficient congruent to its terminal binomial times the complete digit-binomial product.

Unconditional constructive Lucas theorem for any two genuinely terminating beta-coded prime-base digit streams: Choose(n,k) is congruent to the entire digitwise binomial product modulo p.

For every prime p, every n,k, and every common length exceeding both, there exist actual terminating coherent digit streams, digit-binomial beta coefficients, their finite product, and the exact Lucas congruence.

Full constructive Lucas theorem: for every prime p and every relational Choose(n,k,C), explicit terminating beta-coded base-p digit streams and their complete digit-binomial product exist and satisfy C congruent to that product modulo p.