PD0004 · Primep is nonunit and every factorization of p has a unit factor.
conservative definition · not a theoremCurrent 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.
dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.
PD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremPD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0013 · BetaAtx is the bounded beta-decoded value at index i.
conservative definition · not a theoremPD0041 · Choosez is the recurrence-defined binomial coefficient of row n and column k.
conservative definition · not a theoremPD0014 · Productz is the product of a beta-coded prefix of length l.
conservative definition · not a theoremPD0018 · RangeThe decoded prefix is a,a+1,...,a+l-1.
conservative definition · not a theoremPD0023 · Factorialz is the relational factorial of n.
conservative definition · not a theoremPD0003 · DvdThe natural number d divides n.
conservative definition · not a theoremPD0008 · ModEqBalanced-natural congruence modulo m.
conservative definition · not a theoremPD0015 · Sumz is the sum of a beta-coded prefix of length l.
conservative definition · not a theoremPD0019 · RepeatThe decoded prefix repeats a for l positions.
conservative definition · not a theoremPD0020 · Powz is the relational e-th power of a.
conservative definition · not a theoremPD0044 · PowerDividesThe relational power p to exponent e divides n.
conservative definition · not a theoremPD0045 · BoundedPowerValuatione is the greatest exponent at most b for which p to that exponent divides n.
conservative definition · not a theoremPD0046 · PowerValuatione is the canonical bounded p-adic power valuation of n.
conservative definition · not a theoremCF0005 · CarryThe sum of two natural digits is at least the base p.
conservative definition · not a theoremCF0010 · DigitA base-p digit d and quotient q satisfy n = p·q+d with the witnessed strict bound d<p.
conservative definition · not a theoremPD0007 · DivRemq and r are a quotient and a strict remainder for n by d.
conservative definition · not a theoremPD0040 · DivisionPrefixBeta prefixes encode pointwise quotients and strict remainders.
conservative definition · not a theoremLU0000 · lucas_digit_carry_implies_prime_dividesFor two genuine base-p digits, an addition carry forces p to divide their relational binomial coefficient.
theorem body · 5 linked definitions · unenrolled candidate · no checked-use authorityLU0001 · lucas_prime_row_interior_divisibleEvery interior coefficient in prime Pascal row p is divisible by p.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0002 · lucas_choose_prime_divisor_boundEvery prime divisor of a relational binomial coefficient is at most its Pascal-row index.
theorem body · 5 linked definitions · unenrolled candidate · no checked-use authorityLU0003 · lucas_digit_carry_iff_prime_dividesFor two base-p digits, carrying is equivalent to prime divisibility of their binomial coefficient.
theorem body · 5 linked definitions · unenrolled candidate · no checked-use authorityLU0004 · lucas_digit_no_carry_iff_not_dividesFor two base-p digits, a carry-free sum is equivalent to constructive nondivisibility of their binomial coefficient.
theorem body · 5 linked definitions · unenrolled candidate · no checked-use authorityLU0005 · lucas_base_p_digit_totalEvery natural value has an actual quotient and strictly bounded base-p digit for every nonzero base.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU0006 · lucas_prime_base_digit_totalEvery prime base constructively provides a quotient and canonical least-significant digit for every natural.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityLU0007 · lucas_base_p_digit_functionalBoth the quotient and the bounded base-p digit are constructively functional.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU0008 · lucas_base_p_digit_of_small_valueA value strictly below its base has quotient zero and itself as its unique canonical digit.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityLU0009 · lucas_base_p_zero_digit_iff_dividesThe canonical least-significant base-p digit is zero exactly when its value is divisible by p.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityLU000A · lucas_base_p_digit_prefix_existsEvery finite beta-coded natural prefix has actual beta-coded quotient and least-significant digit prefixes for each nonzero base.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU000B · lucas_prime_base_digit_prefix_existsEvery prime base constructively digitizes an entire finite beta-coded source prefix.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityLU000C · lucas_base_p_digit_prefix_pointAt every source beta index, the quotient and digit beta prefixes expose the unique actual quotient/digit witnesses of that source value.
theorem body · 4 linked definitions · unenrolled candidate · no checked-use authorityLU000D · lucas_base_p_two_digit_totalEvery nonzero base constructively extracts two genuinely successive digits: the second source is exactly the first quotient.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU000E · lucas_prime_base_two_digit_totalEvery prime base constructively provides two coherent successive digits and their remaining quotient.
theorem body · 2 linked definitions · unenrolled candidate · no checked-use authorityLU000F · lucas_base_p_two_digit_reconstructionTwo coherent bounded base-p digits reconstruct the exact natural n = p²*q1 + p*d1 + d0 without introducing exponentiation.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU000G · lucas_prime_row_initial_coefficient_oneThe initial coefficient of every relational Pascal row is exactly one.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU000H · lucas_prime_row_terminal_coefficient_oneThe terminal coefficient of every relational Pascal row is exactly one.
theorem body · 1 linked definitions · unenrolled candidate · no checked-use authorityLU000I · lucas_prime_row_sparse_completeEvery prime Pascal row has exact boundary coefficients one and every interior coefficient divisible by its prime modulus.
theorem body · 4 linked definitions · unenrolled candidate · no checked-use authorityLU000J · lucas_positive_lower_quotient_exceeds_upper_digitA positive lower base quotient makes its full index strictly greater than every bounded upper digit.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000K · lucas_positive_lower_quotient_digit_coefficient_zeroA binomial row consisting of one upper digit vanishes at every index with positive lower base quotient.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000L · lucas_zero_upper_quotient_high_column_vanishesThe zero-upper-quotient boundary of the Lucas prime block is constructively zero in every positive lower-quotient column.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000M · lucas_prime_block_digit_congruenceThe complete prime-base Lucas one-digit block congruence holds for arbitrary upper and lower quotients and both bounded digits.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000N · lucas_one_step_division_congruenceEvery actual prime-base division of the upper and lower indices satisfies the complete Lucas quotient-times-digit binomial congruence.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000O · lucas_choose_lower_eq_transportRelational binomial coefficients transport constructively along equality of their lower indices.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000P · lucas_choose_zero_index_is_oneEvery relational binomial coefficient with a witnessed zero lower index is exactly one.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000Q · lucas_choose_zero_upper_positive_is_zeroA positive lower index forces the zeroth Pascal-row coefficient to vanish.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000R · lucas_divisible_implies_zero_modAn explicit divisibility witness gives a balanced natural congruence to zero.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000S · lucas_positive_digit_has_bounded_complementEvery nonzero digit strictly below its prime base has a complementary digit strictly below that base.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000T · lucas_prime_row_interior_zero_modEvery nonboundary coefficient of the prime Pascal row is constructively congruent to zero.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000U · lucas_pascal_congruence_stepExact Pascal recurrence transports two balanced coefficient congruences to their successor-row sum.
theorem body · 2 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000V · lucas_predecessor_digit_below_baseThe predecessor of a nonzero digit strictly below the base remains strictly below the base.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000W · lucas_prime_shift_below_baseEvery below-base coefficient of row p+a is congruent modulo prime p to the corresponding coefficient of row a, by constructive Pascal induction.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000X · lucas_prime_plus_index_nonzeroAdding a natural index to a nonzero prime never produces zero.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000Y · lucas_add_positive_index_strictAdding a witnessed positive natural strictly increases a natural value.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU000Z · lucas_prime_shift_high_columnFor 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.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0010 · lucas_prime_block_zero_reassociationThe zero prime-block quotient leaves its additive tail unchanged.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0011 · lucas_prime_block_successor_reassociationA successor prime-block quotient is exactly one prime shift of its predecessor.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0012 · lucas_repeated_prime_shift_below_baseEvery below-base binomial column is invariant modulo a prime under an arbitrary number of prime-row shifts.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0013 · lucas_low_digit_congruenceThe exact Lucas congruence holds for every natural upper quotient and every lower index consisting of one base-prime digit.
theorem body · 0 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0014 · lucas_low_digit_product_congruenceThe full quotient-times-digit Lucas product formula is kernel-checked whenever the lower quotient is zero, for unrestricted upper quotient.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0015 · lucas_digit_chain_initial_code_existsEvery natural is the zeroth decoded entry of an actual beta-coded quotient stream.
theorem body · 1 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0016 · lucas_digit_chain_emptyA decoded initial quotient constructively supplies the empty coherent digit chain.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0017 · lucas_digit_chain_empty_existsAn actual initial quotient code and arbitrary empty digit code exist for every natural.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0018 · lucas_digit_chain_extendOne constructive quotient division and two beta-prefix extensions append the next genuinely successive digit without disturbing any earlier step.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU0019 · lucas_digit_chain_existsEvery nonzero base and natural input possess a coherent successive quotient/digit chain of every finite requested length.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001A · lucas_prime_digit_chain_existsEvery prime modulus admits arbitrarily long coherent constructive beta-coded base-p digit streams.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001B · lucas_digit_chain_initial_valueThe zeroth quotient of every coherent beta-coded digit trace is exactly its original natural input.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001C · lucas_digit_chain_step_existsEvery position below an arbitrary finite chain length exposes its actual consecutive quotients and bounded base-p digit.
theorem body · 3 linked definitions · unenrolled candidate · no checked-use authorityLU001D · lucas_modular_backward_product_foldAny beta-coded chain of pointwise backward modular recurrences folds into the exact terminal value times the entire beta-coded finite product.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001E · lucas_choose_prefix_emptyAny pair of beta-coded source streams has a constructively empty relational-Choose coefficient prefix.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001F · lucas_choose_prefix_extendBeta-prefix extension and relational binomial totality append the exact coefficient for the next two decoded source entries.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001G · lucas_choose_prefix_existsEvery pair of beta-coded natural source streams has an actual beta-coded relational-binomial coefficient stream of every finite length.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001H · lucas_choose_prefix_pointEvery independently supplied decoded upper index, lower index, and coefficient satisfies the exact relational binomial theorem at that prefix position.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001I · lucas_multidigit_congruence_from_one_stepA universal one-step Lucas prime-block law implies the full arbitrary-length beta-coded digit product congruence with its exact terminal binomial factor.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001J · lucas_terminating_multidigit_theorem_from_one_stepFor 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.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001K · lucas_prime_digit_nonzero_quotient_strictFor a prime base every nonzero successive digit quotient is strictly below its predecessor natural.
theorem body · 3 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001L · lucas_prime_digit_chain_nonzero_index_boundAny nonzero quotient at chain position i obeys the constructive global bound q+i<=n.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001M · lucas_prime_digit_chain_terminal_zeroEvery prime-base digit trace longer than its original natural has an actual terminal quotient equal to zero.
theorem body · 5 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001N · lucas_terminating_prime_digit_chain_existsFor every prime base and every length strictly above n, a genuinely coherent beta-coded digit chain exists and provably terminates with quotient zero.
theorem body · 4 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001O · lucas_multidigit_congruenceUnconditional full multidigit Lucas congruence: every actual beta-coded coherent digit pair has coefficient congruent to its terminal binomial times the complete digit-binomial product.
theorem body · 7 linked definitions · unenrolled candidate · no checked-use authorityLU001P · lucas_terminating_multidigit_theoremUnconditional 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.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001Q · lucas_theorem_for_lengthFor 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.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not StableLU001R · lucas_theoremFull 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.
theorem body · 7 linked definitions · Alpha v30 alpha_closed · checked-use authorized; not Stable