PD0001 · LeWitness-defined non-strict order on natural numbers.
conservative definition · not a theoremPD0002 · LtWitness-defined strict order on natural numbers.
conservative definition · not a theoremPD0003 · DvdThe natural number d divides n.
conservative definition · not a theoremPD0004 · Primep is nonunit and every factorization of p has a unit factor.
conservative definition · not a theoremPD0005 · CoprimeEvery common divisor of a and b is one.
conservative definition · not a theoremPD0006 · IsGCDg is a common divisor divisible by every common divisor.
conservative definition · not a theoremPD0007 · DivRemq and r are a quotient and a strict remainder for n by d.
conservative definition · not a theoremPD0008 · ModEqBalanced-natural congruence modulo m.
conservative definition · not a theoremPD0013 · BetaAtx is the bounded beta-decoded value at index i.
conservative definition · not a theoremPD0014 · Productz is the product of a beta-coded prefix of length l.
conservative definition · not a theoremPD0015 · Sumz is the sum of a beta-coded prefix of length l.
conservative definition · not a theoremPD0016 · AllBitsEvery decoded entry below l is zero or one.
conservative definition · not a theoremPD0017 · BitCountz is the sum of a beta-coded all-bit prefix.
conservative definition · not a theoremPD0018 · RangeThe decoded prefix is a,a+1,...,a+l-1.
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 theoremPD0023 · Factorialz is the relational factorial of n.
conservative definition · not a theoremPD0041 · Choosez is the recurrence-defined binomial coefficient of row n and column k.
conservative definition · not a theoremPD0042 · CentralBinomz is the central binomial coefficient Choose(2n,n).
conservative definition · not a theoremPD0043 · Primorialz is the finite product of the primes at most n.
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 theoremPD0048 · FactorialValuatione is the bounded p-adic valuation of the factorial n!.
conservative definition · not a theoremPD0049 · PowerQuotPrefixThe beta-coded prefix stores the quotients of n by the first l positive powers of p.
conservative definition · not a theoremPD0050 · LegendreSume is the finite Legendre sum of the quotients of n by positive powers of p.
conservative definition · not a theoremPD0051 · FloorSqrts is the integer floor square root: s² ≤ n < (s+1)².
conservative definition · not a theoremPD0052 · CeilDivSixq is the ceiling of n divided by six.
conservative definition · not a theoremBT0000 · zero_addZero is a left identity for addition; unlike PA3, this needs induction.
theorem · proof layer 0 · 0 definitionsBT0001 · add_succ_leftA successor can move through addition on the left.
theorem · proof layer 0 · 0 definitionsBT0002 · add_commAddition is commutative.
theorem · proof layer 1 · 0 definitionsBT0003 · add_assocAddition is associative.
theorem · proof layer 0 · 0 definitionsBT0004 · mul_zero_leftZero annihilates multiplication on the left.
theorem · proof layer 0 · 0 definitionsBT0005 · mul_succ_leftA successor can move through multiplication on the left.
theorem · proof layer 2 · 0 definitionsBT0006 · mul_commMultiplication is commutative.
theorem · proof layer 3 · 0 definitionsBT0007 · mul_addMultiplication distributes over addition on the right.
theorem · proof layer 1 · 0 definitionsBT0008 · mul_assocMultiplication is associative.
theorem · proof layer 2 · 0 definitionsBT0009 · one_mulOne is a left identity for multiplication.
theorem · proof layer 0 · 0 definitionsBT000A · mul_oneOne is a right identity for multiplication.
theorem · proof layer 1 · 0 definitionsBT000B · add_mulMultiplication distributes over addition on the left.
theorem · proof layer 4 · 0 definitionsBT000C · succ_ne_zeroNo successor is zero (the reusable PA1 lemma).
theorem · proof layer 0 · 0 definitionsBT000D · succ_injectiveSuccessor is injective (the reusable PA2 lemma).
theorem · proof layer 0 · 0 definitionsBT000E · le_reflThe defined order is reflexive; zero is its witness.
theorem · proof layer 1 · 1 definitionsBT000F · le_transOrder witnesses compose by addition, so the defined order is transitive.
theorem · proof layer 1 · 1 definitionsBT000G · no_succ_add_fixedAdding a positive successor cannot leave a natural number fixed.
theorem · proof layer 0 · 0 definitionsBT000H · drop_add_prefix_from_fixedA fixed-point equation remains fixed after dropping an additive prefix.
theorem · proof layer 1 · 0 definitionsBT000I · antisymm_from_witnessesOpposing additive witnesses force equality.
theorem · proof layer 2 · 0 definitionsBT000J · le_antisymmThe witness-defined order is antisymmetric.
theorem · proof layer 3 · 1 definitionsBT000K · le_totalEvery pair of natural numbers is comparable in the defined order.
theorem · proof layer 0 · 1 definitionsBT000L · add_eq_zero_rightA sum equal to zero has zero as its right addend.
theorem · proof layer 0 · 0 definitionsBT000M · mul_eq_zeroZero products have a zero factor: the 23-entry core capstone.
theorem · proof layer 1 · 0 definitionsBT000Q · zero_or_succEvery natural is either zero or the successor of a natural.
theorem · proof layer 0 · 0 definitionsBT000R · nonzero_is_succEvery nonzero natural has a predecessor.
theorem · proof layer 0 · 0 definitionsBT000S · add_congrAddition preserves equality in both arguments.
theorem · proof layer 0 · 0 definitionsBT000T · mul_congrMultiplication preserves equality in both arguments.
theorem · proof layer 0 · 0 definitionsBT000U · add_right_cancelA common right addend can be cancelled.
theorem · proof layer 0 · 0 definitionsBT000V · add_left_cancelA common left addend can be cancelled.
theorem · proof layer 2 · 0 definitionsBT000W · zero_leZero is below every natural number.
theorem · proof layer 0 · 1 definitionsBT000X · le_succ_selfEvery natural number is below its successor.
theorem · proof layer 1 · 1 definitionsBT000Y · le_zeroOnly zero is less than or equal to zero.
theorem · proof layer 1 · 1 definitionsBT0010 · one_le_of_ne_zeroEvery nonzero natural is at least one.
theorem · proof layer 0 · 1 definitionsBT0011 · ne_zero_of_one_leA natural at least one is nonzero.
theorem · proof layer 0 · 1 definitionsBT0012 · le_add_leftAdding on the left produces an explicit order witness.
theorem · proof layer 0 · 1 definitionsBT0013 · le_add_rightAdding on the right produces an explicit order witness.
theorem · proof layer 2 · 1 definitionsBT0014 · add_le_add_rightAdding the same right summand preserves the witness-defined order.
theorem · proof layer 1 · 1 definitionsBT0015 · add_le_add_leftAdding the same left summand preserves the witness-defined order.
theorem · proof layer 2 · 1 definitionsBT0016 · succ_le_succSuccessor preserves the witness-defined order.
theorem · proof layer 0 · 2 definitionsBT0017 · le_of_succ_le_succSuccessor order reflects to the underlying naturals.
theorem · proof layer 0 · 2 definitionsBT0018 · le_succA weak inequality remains true after raising its upper bound by one.
theorem · proof layer 1 · 1 definitionsBT0019 · lt_to_leA witnessed strict inequality entails the corresponding weak inequality.
theorem · proof layer 1 · 2 definitionsBT001B · lt_irrefl_expandedNo natural is strictly below itself, with strict order fully expanded.
theorem · proof layer 1 · 1 definitionsBT001C · le_eq_or_ltA witnessed inequality is either equality or a witnessed strict inequality.
theorem · proof layer 1 · 2 definitionsBT001D · lt_of_lt_of_leStrict order followed by weak order remains strict.
theorem · proof layer 2 · 2 definitionsBT001E · lt_of_le_of_ltWeak order followed by strict order remains strict.
theorem · proof layer 1 · 2 definitionsBT001F · lt_transStrict order is transitive.
theorem · proof layer 1 · 1 definitionsBT001G · le_or_ltAny two naturals satisfy weak order in one direction or strict order in the other.
theorem · proof layer 0 · 2 definitionsBT001H · lt_trichotomyTwo naturals are equal or strictly ordered in exactly one displayed direction.
theorem · proof layer 0 · 1 definitionsBT001I · lt_not_leA strict inequality excludes the reverse weak inequality.
theorem · proof layer 0 · 2 definitionsBT001J · le_not_ltA weak inequality excludes strict inequality in the reverse direction.
theorem · proof layer 1 · 2 definitionsBT001K · lt_not_eq_add_middleA strict upper bound prevents the lower term from containing that bound as an additive middle block.
theorem · proof layer 1 · 1 definitionsBT001L · mul_le_mul_leftLeft multiplication preserves the witness-defined order.
theorem · proof layer 2 · 1 definitionsBT001M · mul_le_mul_rightRight multiplication preserves the witness-defined order.
theorem · proof layer 5 · 1 definitionsBT001N · mul_lt_mul_succ_left_nonzeroMultiplication by a nonzero left factor strictly increases across a successor step.
theorem · proof layer 2 · 1 definitionsBT001O · division_remainder_succEvery dividend has a quotient and bounded remainder for a successor divisor.
theorem · proof layer 1 · 1 definitionsBT001P · division_remainder_existsEvery positive divisor admits a quotient and a strictly bounded remainder.
theorem · proof layer 2 · 1 definitionsBT001R · division_block_upperA bounded remainder keeps its decomposition below the next divisor block.
theorem · proof layer 2 · 1 definitionsBT001S · positive_quotient_gap_impossibleA positive gap between quotients makes two bounded-remainder decompositions unequal.
theorem · proof layer 3 · 1 definitionsBT001U · division_remainder_uniqueBounded quotient-remainder decompositions have unique quotients and remainders.
theorem · proof layer 4 · 1 definitionsBT001V · zero_remainder_implies_multipleA quotient decomposition with zero remainder supplies a divisibility witness.
theorem · proof layer 0 · 1 definitionsBT001W · multiple_has_zero_remainderEvery multiple of a nonzero divisor has a bounded zero-remainder decomposition.
theorem · proof layer 1 · 2 definitionsBT001X · add_eq_zero_leftA sum equal to zero has zero as its left addend.
theorem · proof layer 2 · 0 definitionsBT0020 · mul_eq_one_componentsA product is one only when both natural factors are one.
theorem · proof layer 1 · 0 definitionsBT0021 · mul_ne_zeroA product of two nonzero naturals is nonzero.
theorem · proof layer 2 · 0 definitionsBT0022 · mul_left_cancel_nonzeroA nonzero common left factor can be cancelled.
theorem · proof layer 3 · 0 definitionsBT0024 · two_large_factors_impossibleTwo naturals at least two cannot multiply to two.
theorem · proof layer 3 · 0 definitionsBT0025 · prime_twoTwo is prime in the expanded first-order prime predicate.
theorem · proof layer 4 · 1 definitionsBT0026 · multiple_zeroZero is a multiple of every natural number.
theorem · proof layer 0 · 1 definitionsBT0027 · one_multipleEvery natural number is a multiple of one.
theorem · proof layer 1 · 1 definitionsBT0028 · multiple_reflEvery natural number is a multiple of itself.
theorem · proof layer 2 · 1 definitionsBT002A · multiple_mul_rightA right multiple of a multiple remains a multiple.
theorem · proof layer 3 · 1 definitionsBT002B · multiple_mul_leftA left multiple of a multiple remains a multiple.
theorem · proof layer 4 · 1 definitionsBT002C · multiple_transThe multiple relation is transitive.
theorem · proof layer 3 · 1 definitionsBT002D · divisor_le_nonzeroA divisor of a nonzero natural is bounded by that natural.
theorem · proof layer 1 · 3 definitionsBT002E · divisor_oneEvery natural divisor of one equals one.
theorem · proof layer 2 · 1 definitionsBT002F · multiple_antisymmMutual divisibility is antisymmetric over natural numbers.
theorem · proof layer 4 · 1 definitionsBT002G · factor_differenceA common-factor difference is itself a multiple of that factor.
theorem · proof layer 2 · 1 definitionsBT002H · divides_remainderA common divisor of a dividend and divisor also divides the remainder.
theorem · proof layer 3 · 1 definitionsBT002I · divides_linear_stepA common divisor of a divisor and remainder divides their Euclidean linear step.
theorem · proof layer 3 · 1 definitionsBT002L · is_gcd_zero_rightEvery natural is the relational gcd of itself and zero.
theorem · proof layer 3 · 1 definitionsBT002S · is_gcd_euclid_forwardA relational gcd of divisor and remainder is a gcd of dividend and divisor.
theorem · proof layer 4 · 1 definitionsBT002U · gcd_exists_up_toBounded induction constructs a relational gcd whenever the right input is at most the bound.
theorem · proof layer 5 · 4 definitionsBT002V · gcd_exists_relationalEvery pair of naturals has a relational greatest common divisor.
theorem · proof layer 6 · 2 definitionsBT002W · coprime_symmCoprimality in its expanded common-divisor form is symmetric.
theorem · proof layer 0 · 1 definitionsBT002X · coprime_one_rightEvery natural is coprime to one in the expanded common-divisor relation.
theorem · proof layer 3 · 1 definitionsBT002Y · coprime_one_leftOne is coprime to every natural in the expanded common-divisor relation.
theorem · proof layer 3 · 1 definitionsBT0031 · is_gcd_one_to_coprimeA relational gcd witness one implies expanded coprimality.
theorem · proof layer 3 · 3 definitionsBT0032 · add_permute_outerPermute the outer entries of two additive pairs.
theorem · proof layer 2 · 0 definitionsBT0033 · balanced_bezout_euclid_stepTransport balanced natural Bezout coefficients across one Euclidean division step.
theorem · proof layer 5 · 0 definitionsBT0034 · gcd_balanced_bezout_exists_up_toBounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.
theorem · proof layer 6 · 4 definitionsBT0035 · gcd_balanced_bezout_existsEvery pair has a relational gcd together with balanced natural Bezout witnesses.
theorem · proof layer 7 · 2 definitionsBT0036 · balanced_combination_scale_rightScale a balanced natural combination on the right.
theorem · proof layer 5 · 0 definitionsBT0037 · common_divisor_divides_balanced_resultEvery common divisor of two inputs divides the result of a balanced natural combination.
theorem · proof layer 3 · 1 definitionsBT0038 · coprime_balanced_bezoutCoprime inputs admit balanced natural Bezout coefficients with result one.
theorem · proof layer 8 · 2 definitionsBT0039 · gauss_coprime_cancelCancel a coprime factor from a divisibility witness (Gauss cancellation).
theorem · proof layer 9 · 2 definitionsBT003A · eq_decidableEquality of natural numbers is constructively decidable.
theorem · proof layer 0 · 0 definitionsBT003B · multiple_decidable_nonzeroDivisibility by a nonzero natural is constructively decidable.
theorem · proof layer 5 · 3 definitionsBT003C · multiple_decidableDivisibility of natural numbers is constructively decidable, including the zero divisor case.
theorem · proof layer 6 · 1 definitionsBT003D · factor_property_succExtend a bounded prime factor-pair property by checking the new boundary.
theorem · proof layer 2 · 2 definitionsBT003E · factor_search_up_toConstructively decide whether a nonzero natural has a bounded nontrivial factor pair.
theorem · proof layer 6 · 2 definitionsBT003F · prime_or_compositeEvery nonzero nonunit natural is constructively prime or has a nontrivial factor pair.
theorem · proof layer 7 · 2 definitionsBT003G · prime_nonzeroEvery prime natural is nonzero.
theorem · proof layer 1 · 1 definitionsBT003H · prime_decidablePrimality of every natural number is constructively decidable.
theorem · proof layer 8 · 1 definitionsBT003J · proper_factor_ltA factor with a nonunit cofactor is strictly smaller than a nonzero product.
theorem · proof layer 4 · 2 definitionsBT003K · prime_divisor_exists_up_toBounded strong induction constructs a prime divisor of every nonzero nonunit natural.
theorem · proof layer 8 · 4 definitionsBT003L · prime_divisor_existsEvery nonzero nonunit natural has a prime divisor.
theorem · proof layer 9 · 2 definitionsBT003M · prime_divisor_eq_one_or_selfEvery divisor of a prime is one or the prime itself.
theorem · proof layer 2 · 2 definitionsBT003N · euclid_prime_dvd_productA prime dividing a product divides at least one factor (Euclid's lemma).
theorem · proof layer 10 · 4 definitionsBT003O · mod_eq_reflBalanced natural congruence is reflexive.
theorem · proof layer 0 · 1 definitionsBT003Q · mod_eq_transBalanced natural congruence is transitive.
theorem · proof layer 2 · 1 definitionsBT003R · mod_eq_addBalanced natural congruence respects addition.
theorem · proof layer 3 · 1 definitionsBT003S · mod_eq_mul_rightBalanced congruence is preserved by multiplication on the right.
theorem · proof layer 5 · 1 definitionsBT003T · mod_eq_mul_leftBalanced congruence is preserved by multiplication on the left.
theorem · proof layer 6 · 1 definitionsBT003W · mod_eq_bounded_uniqueTwo balanced-congruent values below the same modulus are equal.
theorem · proof layer 5 · 2 definitionsBT003X · mod_eq_to_remainder_decompositionA bounded balanced residue has a directed quotient/remainder witness.
theorem · proof layer 6 · 3 definitionsBT003Y · beta_modulus_nonzeroEvery Gödel-beta decoding modulus is nonzero.
theorem · proof layer 1 · 0 definitionsBT0040 · beta_at_self_of_boundA value below a Gödel-beta modulus decodes to itself when used as the code.
theorem · proof layer 1 · 2 definitionsBT0041 · beta_at_existsEvery Gödel-beta position has a bounded decoded residue.
theorem · proof layer 4 · 2 definitionsBT0042 · beta_at_uniqueThe decoded residue at a Gödel-beta position is unique.
theorem · proof layer 5 · 1 definitionsBT0045 · beta_at_of_mod_eq_boundA bounded value congruent to a code is its expanded Gödel-beta value.
theorem · proof layer 7 · 3 definitionsBT0046 · dvd_to_mod_zeroA multiple is balanced-congruent to zero.
theorem · proof layer 1 · 2 definitionsBT004C · bezout_mod_leftA balanced Bezout identity selects the right coefficient modulo the left modulus.
theorem · proof layer 2 · 1 definitionsBT004D · bezout_mod_rightA balanced Bezout identity selects the left coefficient modulo the right modulus.
theorem · proof layer 1 · 1 definitionsBT004E · mod_eq_predecessor_cancelThe predecessor of a successor acts as minus one in balanced congruence.
theorem · proof layer 3 · 1 definitionsBT004F · binary_crtConstructive binary CRT for positive coprime natural moduli using balanced congruence.
theorem · proof layer 9 · 2 definitionsBT004I · beta_modulus_coprime_baseEvery beta-shaped successor modulus is coprime to its base c.
theorem · proof layer 4 · 2 definitionsBT004J · common_divisor_beta_moduli_divides_gap_times_cA common divisor of two ordered beta moduli divides the index gap times c.
theorem · proof layer 5 · 1 definitionsBT004K · beta_moduli_coprime_of_gap_dvdBeta moduli at an additive index gap dividing c are coprime.
theorem · proof layer 10 · 2 definitionsBT004M · bounded_common_multiple_stepExtend a nonzero common multiple through the next positive natural.
theorem · proof layer 4 · 1 definitionsBT004N · bounded_common_multiple_existsEvery finite initial interval has a nonzero common-multiple surrogate.
theorem · proof layer 5 · 1 definitionsBT004O · beta_moduli_coprime_of_lt_bounded_common_multipleOrdered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.
theorem · proof layer 11 · 4 definitionsBT004P · beta_moduli_pairwise_coprime_boundedDistinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.
theorem · proof layer 12 · 3 definitionsBT004R · coprime_mul_leftCoprimality with a fixed right operand is closed under multiplication on the left.
theorem · proof layer 10 · 2 definitionsBT004S · coprime_mul_rightCoprimality with a fixed left operand is closed under multiplication on the right.
theorem · proof layer 11 · 1 definitionsBT004T · mod_eq_of_mod_eq_multipleBalanced congruence descends from a multiple modulus to every divisor modulus.
theorem · proof layer 3 · 2 definitionsBT004U · binary_crt_fold_stepOne binary CRT extension preserves every old congruence whose modulus divides the accumulated product.
theorem · proof layer 10 · 3 definitionsBT004V · right_factor_divides_productThe right factor divides a product.
theorem · proof layer 4 · 1 definitionsBT0053 · beta_value_le_codeEvery decoded beta value is at most its code.
theorem · proof layer 0 · 2 definitionsBT0054 · base_le_beta_modulusA beta base is at most every beta modulus over that base.
theorem · proof layer 3 · 1 definitionsBT0055 · le_scaled_nonzeroScaling by a nonzero natural does not decrease a natural.
theorem · proof layer 6 · 2 definitionsBT0056 · scaled_bounded_common_multipleA right multiple of a bounded common multiple remains such a common multiple.
theorem · proof layer 4 · 1 definitionsBT0057 · beta_value_lt_scaled_baseAn old beta value fits every modulus after a constructive scaled-base rebase.
theorem · proof layer 7 · 3 definitionsBT0058 · new_value_lt_scaled_baseThe appended value fits every modulus after the same constructive scaled-base rebase.
theorem · proof layer 7 · 2 definitionsBT0059 · beta_exclusive_accumulated_product_stepExtend the accumulated target-modulus product for an exclusive prefix.
theorem · proof layer 13 · 4 definitionsBT005A · beta_exclusive_recode_congruence_stepAdd the next source value to a target-base CRT code for an exclusive prefix.
theorem · proof layer 11 · 6 definitionsBT005B · beta_exclusive_recode_invariant_stepCombine modulus-product and cross-base congruence updates for an exclusive prefix.
theorem · proof layer 14 · 6 definitionsBT005C · bounded_beta_exclusive_recode_invariantFold an empty-based, exclusive beta prefix into another base with append readiness.
theorem · proof layer 15 · 6 definitionsBT005D · beta_prefix_extendRebase an arbitrary decoded prefix and append one exact natural value.
theorem · proof layer 16 · 6 definitionsBT005E · beta_prefix_product_trace_existsEvery decoded beta factor prefix admits a beta-coded exact prefix-product trace.
theorem · proof layer 17 · 3 definitionsBT005F · beta_product_existsEvery finite decoded beta prefix has an exact relational product and a coded trace.
theorem · proof layer 18 · 3 definitionsBT005G · beta_product_functionalThe fully expanded beta-coded Product relation is functional in its terminal product.
theorem · proof layer 6 · 2 definitionsBT005I · beta_product_zeroThe product of an empty decoded prefix is one.
theorem · proof layer 6 · 1 definitionsBT005J · beta_product_succ_decomposeA successor product decomposes into its prefix product and final decoded factor.
theorem · proof layer 6 · 2 definitionsBT005K · beta_product_succ_appendAppend one decoded factor to an existing fully expanded Product witness.
theorem · proof layer 17 · 4 definitionsBT005L · beta_product_transport_prefixOne-way extensional factor-prefix preservation transports Product without changing its trace.
theorem · proof layer 0 · 3 definitionsBT0069 · beta_factor_divides_productEvery decoded factor inside an exact beta Product divides its terminal product.
theorem · proof layer 7 · 5 definitionsBT006N · prime_threeThree is prime in the expanded first-order prime predicate.
theorem · proof layer 3 · 1 definitionsBT0072 · parity_casesEvery natural has a constructive even-or-odd witness.
theorem · proof layer 0 · 0 definitionsBT007U · beta_repeat_emptyEvery constant beta prefix of length zero is vacuously Repeat.
theorem · proof layer 1 · 1 definitionsBT007V · beta_repeat_succ_extendRecode a constant prefix and append one more copy of its value.
theorem · proof layer 17 · 3 definitionsBT007W · beta_repeat_existsEvery value and length admit a beta-coded constant prefix.
theorem · proof layer 18 · 1 definitionsBT007X · beta_repeat_entry_eqEvery decoded entry of a Repeat prefix equals its repeated value.
theorem · proof layer 6 · 3 definitionsBT007Y · beta_repeat_transport_entryRepeat prefixes with one value preserve every decoded entry extensionally.
theorem · proof layer 7 · 3 definitionsBT0080 · pow_existsEvery base and exponent have a relational finite-product power.
theorem · proof layer 19 · 2 definitionsBT0081 · pow_zeroThe relational zeroth power is one.
theorem · proof layer 7 · 1 definitionsBT0082 · pow_functionalRelational powers have a unique natural value.
theorem · proof layer 8 · 4 definitionsBT0083 · pow_successor_decomposeA successor relational power is its predecessor power times the base.
theorem · proof layer 7 · 3 definitionsBT0084 · beta_range_emptyEvery consecutive beta range of length zero is vacuous.
theorem · proof layer 1 · 1 definitionsBT0085 · beta_range_succ_extendRecode a consecutive prefix and append its next value.
theorem · proof layer 17 · 3 definitionsBT0086 · beta_range_existsEvery start and length admit a beta-coded consecutive range.
theorem · proof layer 18 · 1 definitionsBT0087 · beta_range_entry_eqA decoded entry of a Range prefix is its start plus its index.
theorem · proof layer 6 · 3 definitionsBT0088 · beta_range_transport_entryTwo Range codes preserve every decoded entry extensionally.
theorem · proof layer 7 · 3 definitionsBT0089 · beta_prefix_sum_trace_existsEvery decoded beta prefix admits an exact beta-coded prefix-sum trace.
theorem · proof layer 17 · 3 definitionsBT008A · beta_sum_existsEvery decoded beta prefix has a relational finite sum.
theorem · proof layer 18 · 3 definitionsBT008B · beta_sum_trace_functionalTwo exact prefix-sum traces over one decoded prefix have equal endpoints.
theorem · proof layer 6 · 2 definitionsBT008C · beta_sum_functionalThe relational finite sum has a unique natural value.
theorem · proof layer 7 · 1 definitionsBT008E · beta_sum_zeroThe sum of an empty decoded prefix is zero.
theorem · proof layer 6 · 1 definitionsBT008F · beta_sum_succ_decomposeA successor sum decomposes into its prefix sum and final summand.
theorem · proof layer 6 · 2 definitionsBT008J · all_bits_prefix_succDropping the final entry preserves the all-bits invariant.
theorem · proof layer 2 · 1 definitionsBT008K · all_bits_last_succThe final entry of a nonempty all-bits prefix is zero or one.
theorem · proof layer 2 · 2 definitionsBT008L · bit_count_existsEvery all-bits prefix has a relational count of its ones.
theorem · proof layer 19 · 2 definitionsBT008N · bit_count_zeroAn empty bit prefix contains zero ones.
theorem · proof layer 7 · 1 definitionsBT008O · bit_count_succ_decomposeA successor count is its prefix count plus a final zero-or-one bit.
theorem · proof layer 7 · 4 definitionsBT008P · bit_count_boundedA zero/one count never exceeds the length of its decoded prefix.
theorem · proof layer 8 · 3 definitionsBT008Q · prime_coprime_or_dividesA prime is constructively either coprime to a natural or divides it.
theorem · proof layer 7 · 4 definitionsBT008R · prime_not_divides_coprimeA prime not dividing a natural is coprime to that natural.
theorem · proof layer 8 · 3 definitionsBT008S · distinct_primes_coprimeDistinct primes are coprime in the expanded common-divisor relation.
theorem · proof layer 9 · 3 definitionsBT008Y · factorial_existsEvery natural has a beta-coded relational factorial value.
theorem · proof layer 19 · 2 definitionsBT0090 · factorial_functionalThe beta-coded relational factorial has a unique value.
theorem · proof layer 8 · 4 definitionsBT0091 · factorial_zeroThe relational factorial of zero is one.
theorem · proof layer 7 · 1 definitionsBT0092 · factorial_succ_decomposeA successor factorial is its predecessor factorial times the successor.
theorem · proof layer 7 · 3 definitionsBT0093 · pow_one_from_zero_successorA successor of a zero exponent gives the relational first power.
theorem · proof layer 8 · 1 definitionsBT0094 · pow_oneThe relational first power of a natural is the natural itself.
theorem · proof layer 9 · 1 definitionsBT0095 · pow_successor_pair_mulA successor power paired with its predecessor equals predecessor times base.
theorem · proof layer 9 · 1 definitionsBT0097 · lt_three_casesEvery natural strictly below three is zero, one, or two.
theorem · proof layer 2 · 2 definitionsBT009V · pow_two_from_one_successorA successor of exponent one gives the relational square.
theorem · proof layer 10 · 1 definitionsBT009W · pow_twoThe relational second power is exactly the square.
theorem · proof layer 11 · 1 definitionsBT009X · pow_addRelational powers turn addition of exponents into multiplication.
theorem · proof layer 9 · 1 definitionsBT00AA · finite_lt_succ_eq_or_ltA value below a successor is the predecessor or lies below it.
theorem · proof layer 2 · 2 definitionsBT00AW · prime_is_succ_succEvery prime natural is the second successor of a natural.
theorem · proof layer 2 · 1 definitionsBT00BG · coprime_product_is_lcmThe product of coprime naturals satisfies the universal relational LCM specification.
theorem · proof layer 10 · 2 definitionsBT00DH · beta_product_pointwise_coprimeA finite product of factors pointwise coprime to m is coprime to m.
theorem · proof layer 11 · 4 definitionsBT00I9 · beta_sum_transport_prefixPointwise-equal decoded prefixes preserve an exact relational Sum.
theorem · proof layer 0 · 3 definitionsBT00JA · eisenstein_initial_segment_prefix_all_bitsEvery exact threshold prefix is an AllBits prefix.
theorem · proof layer 0 · 3 definitionsBT00JB · eisenstein_initial_segment_decoded_choiceEvery decoded bit recovers its exact threshold semantics.
theorem · proof layer 6 · 2 definitionsBT00JC · beta_all_one_bit_count_exactA length-k beta prefix consisting only of ones has BitCount k.
theorem · proof layer 8 · 3 definitionsBT00JD · eisenstein_initial_segment_bit_count_functionalThe BitCount of a bounded exact initial segment is its threshold.
theorem · proof layer 9 · 5 definitionsBT00JE · eisenstein_initial_segment_bit_count_exactA bounded exact initial-segment prefix has native BitCount q.
theorem · proof layer 20 · 5 definitionsBT00K5 · beta_sum_pointwise_addPointwise sums of decoded entries induce exact addition of finite sums.
theorem · proof layer 7 · 3 definitionsBT00MY · add_shuffle_middleFour additive contributions can be regrouped by swapping the middle pair.
theorem · proof layer 3 · 0 definitionsBT00PR · prime_strictly_above_decidableBeing prime and strictly above a fixed lower endpoint is decidable.
theorem · proof layer 9 · 2 definitionsBT00PS · bounded_prime_interval_searchBounded search returns a prime witness or an explicit prime-free interval certificate.
theorem · proof layer 10 · 3 definitionsBT00PV · mul_le_mulMultiplication is monotone in both natural-number arguments.
theorem · proof layer 6 · 1 definitionsBT00PW · le_mul_of_one_le_rightA factor at least one makes right multiplication extensive.
theorem · proof layer 3 · 2 definitionsBT00PX · le_mul_of_one_le_leftA factor at least one makes left multiplication extensive.
theorem · proof layer 6 · 2 definitionsBT00PY · pow_base_monotoneRelational powers are monotone in the base at every exponent.
theorem · proof layer 8 · 2 definitionsBT00Q0 · one_le_powEvery relational power of a base at least one is at least one.
theorem · proof layer 8 · 3 definitionsBT00Q1 · pow_nonzero_of_one_leA relational power of a base at least one cannot be zero.
theorem · proof layer 9 · 2 definitionsBT00Q3 · power_divides_decidableDivisibility by a relational power is constructively decidable.
theorem · proof layer 20 · 3 definitionsBT00Q4 · power_divides_zeroThe zeroth relational power divides every natural.
theorem · proof layer 20 · 2 definitionsBT00Q5 · bounded_power_valuation_searchFinite search either excludes every power divisor or returns a greatest exponent.
theorem · proof layer 21 · 4 definitionsBT00Q6 · bounded_power_valuation_existsEvery explicit exponent bound has a greatest power-divisor exponent.
theorem · proof layer 22 · 3 definitionsBT00Q7 · power_valuation_existsThe value itself supplies a canonical finite bound for power valuation.
theorem · proof layer 23 · 1 definitionsBT00Q8 · power_valuation_functionalCanonical bounded power valuations have a unique exponent.
theorem · proof layer 4 · 2 definitionsBT00Q9 · power_valuation_power_dividesA valuation exponent has a relational power dividing the value.
theorem · proof layer 0 · 2 definitionsBT00QA · power_valuation_dominatesEvery bounded power-divisor exponent lies below the valuation exponent.
theorem · proof layer 0 · 3 definitionsBT00QD · prime_two_leEvery prime is at least two in witness-defined order.
theorem · proof layer 3 · 2 definitionsBT00QE · succ_le_mul_of_two_le_rightMultiplying a nonzero natural by a factor at least two exceeds it.
theorem · proof layer 3 · 2 definitionsBT00QF · prime_power_exponent_leThe exponent of a relational power at a prime base is bounded by its value.
theorem · proof layer 10 · 4 definitionsBT00QG · prime_power_divides_exponent_le_valueA dividing prime power has exponent at most the nonzero dividend.
theorem · proof layer 11 · 3 definitionsBT00QH · power_valuation_successor_not_dividesA canonical valuation at a prime cannot admit the next power divisor.
theorem · proof layer 12 · 4 definitionsBT00QI · power_valuation_selected_and_successor_not_dividesCanonical prime valuations have the usual maximal-power characterization.
theorem · proof layer 13 · 3 definitionsBT00QJ · mul_shuffle_fourFour factors may exchange their two middle entries.
theorem · proof layer 4 · 0 definitionsBT00QK · power_divides_exponent_antitoneDivisibility by a higher relational power entails every lower exponent.
theorem · proof layer 20 · 3 definitionsBT00QL · power_divides_add_mulMultiplying power divisors adds their exponents.
theorem · proof layer 20 · 2 definitionsBT00QM · power_divides_successor_of_cofactorDivisibility of a power cofactor by its base raises the exponent by one.
theorem · proof layer 20 · 3 definitionsBT00QN · prime_power_successor_cancel_cofactorA successor power divisor cancels to a prime divisor of the exact cofactor.
theorem · proof layer 10 · 5 definitionsBT00QO · prime_nondivisor_mulA prime dividing neither factor does not divide their product.
theorem · proof layer 11 · 2 definitionsBT00QP · power_valuation_exact_cofactorA prime valuation extracts a nonzero cofactor not divisible by its prime.
theorem · proof layer 21 · 5 definitionsBT00QQ · power_valuation_mul_successor_not_dividesThe product of exact prime-power valuations has no next power divisor.
theorem · proof layer 22 · 5 definitionsBT00QR · power_valuation_mul_lowerThe valuation of a nonzero product is at least the sum of factor valuations.
theorem · proof layer 21 · 4 definitionsBT00QS · power_valuation_mul_upperThe valuation of a nonzero product is at most the sum of factor valuations.
theorem · proof layer 23 · 5 definitionsBT00QT · prime_power_valuation_mulPrime-power valuation is additive on nonzero products.
theorem · proof layer 24 · 3 definitionsBT00QU · two_mul_eq_add_selfLeft multiplication by two is explicit doubling.
theorem · proof layer 4 · 0 definitionsBT00QV · pow_mul_baseA relational power of a product is the product of the powers.
theorem · proof layer 8 · 1 definitionsBT00QW · pow_two_base_two_value_fourThe relational square of two has the concrete value four.
theorem · proof layer 12 · 1 definitionsBT00R0 · ceil_div_six_shiftCeiling by six commutes with adding an explicit multiple of six.
theorem · proof layer 2 · 1 definitionsBT00R1 · ceil_div_six_totalEvery natural has a constructive ceiling quotient by six.
theorem · proof layer 3 · 3 definitionsBT00R2 · ceil_div_six_functionalThe two witness inequalities determine a unique ceiling quotient.
theorem · proof layer 3 · 3 definitionsBT00R4 · square_six_shift_identityThe six-step square increment is exactly six times 2*s+6.
theorem · proof layer 5 · 0 definitionsBT00R5 · ceil_div_six_square_six_stepCeil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.
theorem · proof layer 6 · 1 definitionsBT00R6 · floor_sqrt_lower_boundThe floor-square graph projects its lower square bound.
theorem · proof layer 0 · 2 definitionsBT00R7 · floor_sqrt_strict_upper_boundThe floor-square graph projects its strict successor-square bound.
theorem · proof layer 0 · 2 definitionsBT00R9 · square_lt_successor_squareEvery square is strictly below the next natural square.
theorem · proof layer 6 · 2 definitionsBT00RA · floor_sqrt_totalEvery natural lies in a constructively selected adjacent-square interval.
theorem · proof layer 7 · 2 definitionsBT00RC · floor_sqrt_monotoneWitness order on inputs is transported monotonically to floor roots.
theorem · proof layer 6 · 3 definitionsBT00RD · mul_le_cancel_left_nonzeroWitness order cancels a common nonzero left multiplier.
theorem · proof layer 4 · 2 definitionsBT00RE · three_mul_eq_two_mul_add_selfLeft multiplication by three is twice the input plus the input.
theorem · proof layer 4 · 0 definitionsBT00RF · ceil_div_six_le_of_upperAny six-multiple upper bound also bounds the ceiling quotient.
theorem · proof layer 3 · 3 definitionsBT00RG · double_triple_remainder_complement_budgetThe equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.
theorem · proof layer 6 · 2 definitionsBT00RH · canonical_double_triple_remainder_complement_budgetCanonical remainder data yields and preserves the complement budget.
theorem · proof layer 7 · 3 definitionsBT00RI · floor_ceil_complement_budgetFloor-square and ceiling budgets imply e<=c and q+e<=n.
theorem · proof layer 4 · 3 definitionsBT00RJ · floor_ceil_division_budgetRaw canonical division data closes both B6 quotient-budget inequalities.
theorem · proof layer 8 · 5 definitionsBT00RK · factorial_nonzeroA relational factorial value is never zero.
theorem · proof layer 8 · 1 definitionsBT00RL · prime_power_valuation_one_zeroAt a prime base, the bounded valuation of one has exponent zero.
theorem · proof layer 8 · 4 definitionsBT00RM · factorial_valuation_existsEvery factorial has a canonical bounded valuation at every base.
theorem · proof layer 24 · 3 definitionsBT00RO · prime_factorial_valuation_zeroThe prime valuation of zero factorial is zero.
theorem · proof layer 9 · 2 definitionsBT00RP · prime_factorial_valuation_succA successor factorial valuation is the sum of the predecessor and successor-factor valuations.
theorem · proof layer 25 · 4 definitionsBT00S0 · prime_power_quotient_prefix_existsEvery prime-power quotient prefix has a finite beta code.
theorem · proof layer 20 · 6 definitionsBT00S1 · power_quotient_prefix_transportEquivalent power-quotient prefixes transport decoded quotients pointwise.
theorem · proof layer 9 · 5 definitionsBT00S2 · prime_legendre_sum_existsEvery prime and natural input have a finite relational Legendre sum.
theorem · proof layer 21 · 4 definitionsBT00S3 · legendre_sum_functionalThe finite relational Legendre sum has a unique value.
theorem · proof layer 10 · 4 definitionsBT00S4 · legendre_sum_zeroThe finite Legendre sum at zero is zero.
theorem · proof layer 7 · 1 definitionsBT00S5 · pow_successor_composeA checked predecessor power composes with one multiplication step.
theorem · proof layer 20 · 1 definitionsBT00SA · prime_power_quotient_tail_zeroThe first omitted prime-power quotient is canonically zero.
theorem · proof layer 11 · 3 definitionsBT00SB · prime_power_divides_exponent_le_valuationEvery dividing prime-power exponent lies below the valuation.
theorem · proof layer 12 · 4 definitionsBT00SC · power_divides_of_exponent_le_valuationEvery exponent below a valuation exponent supplies a power divisor.
theorem · proof layer 21 · 3 definitionsBT00SD · eisenstein_initial_segment_indicator_choiceEvery position has a constructive exact threshold-indicator bit.
theorem · proof layer 1 · 1 definitionsBT00SE · eisenstein_initial_segment_prefix_extendAppend one exact threshold bit while preserving the old prefix.
theorem · proof layer 17 · 2 definitionsBT00SF · eisenstein_initial_segment_prefix_existsEvery threshold and finite length has an exact beta-coded indicator.
theorem · proof layer 18 · 2 definitionsBT00SG · division_remainder_successor_casesSuccessor division has exactly the carry and no-carry quotient cases.
theorem · proof layer 5 · 2 definitionsBT00SH · division_successor_quotient_by_bitA divisibility bit is exactly the successor quotient increment.
theorem · proof layer 6 · 3 definitionsBT00SI · valuation_threshold_bit_decides_power_dividesA valuation threshold bit constructively decides the corresponding power divisor.
theorem · proof layer 22 · 4 definitionsBT00SJ · power_quotient_prefix_decoded_divremA decoded quotient-prefix entry exposes its power and canonical division data.
theorem · proof layer 6 · 5 definitionsBT00SK · power_quotient_successor_pointwise_addSuccessor prime-power quotients are the old quotients plus their valuation-threshold bits.
theorem · proof layer 23 · 9 definitionsBT00SL · pow_successor_compose_from_totalOne shared power-totality premise constructs a successor power.
theorem · proof layer 10 · 1 definitionsBT00SM · pow_mul_exp_from_totalIterated powers multiply exponents using a supplied totality proof.
theorem · proof layer 10 · 1 definitionsBT00SN · pow_exponent_monotone_from_totalExponent monotonicity reuses one supplied power-totality proof.
theorem · proof layer 10 · 3 definitionsBT00SO · pow_two_seed_bundle_from_totalOne totality premise yields the exact seeds 2^2=4 and 2^7=128.
theorem · proof layer 13 · 1 definitionsBT00SR · beta_sum_succ_last_zeroA successor beta sum with final entry zero is its predecessor sum.
theorem · proof layer 7 · 2 definitionsBT00SS · prime_power_quotient_prefix_last_zeroThe final entry of a length-(n+1) old quotient prefix is zero.
theorem · proof layer 12 · 5 definitionsBT00ST · legendre_sum_zero_extended_prefixAn old Legendre sum has a successor-length quotient code ending in zero.
theorem · proof layer 21 · 5 definitionsBT00SU · initial_segment_prefix_sum_existsEvery bounded threshold has a beta prefix whose exact sum is the threshold.
theorem · proof layer 21 · 5 definitionsBT00SV · prime_legendre_sum_succPrime Legendre sums satisfy the exact constructive successor recurrence.
theorem · proof layer 24 · 7 definitionsBT00SW · bertrand_h_six_step_transport_from_totalH(s) and J(s) together imply H(s+6).
theorem · proof layer 14 · 4 definitionsBT00SX · bertrand_j_six_step_transport_from_totalJ(s) implies J(s+6) through the shared 2^12 = 4^6 factor.
theorem · proof layer 14 · 2 definitionsBT00SY · bertrand_hj_six_step_from_totalThe paired H/J invariant advances by six under one PowTotal premise.
theorem · proof layer 15 · 4 definitionsBT00T0 · factorial_legendre_successor_agreementFactorial and Legendre successor recurrences preserve predecessor agreement.
theorem · proof layer 26 · 4 definitionsBT00T1 · prime_factorial_valuation_eq_legendre_sumAt every prime, the factorial valuation exponent equals the finite Legendre sum.
theorem · proof layer 27 · 4 definitionsBT00T2 · beta_pascal_zero_row_extendAppend the next fixed zero-row value while preserving all earlier cells.
theorem · proof layer 17 · 2 definitionsBT00T3 · beta_pascal_zero_row_existsEvery finite width has a beta-coded Pascal zero row.
theorem · proof layer 18 · 2 definitionsBT00T4 · beta_pascal_row_step_extendAppend one Pascal successor-row value and preserve the prefix.
theorem · proof layer 17 · 2 definitionsBT00T5 · beta_pascal_row_step_existsEvery previous beta row has a finite Pascal successor row.
theorem · proof layer 18 · 2 definitionsBT00T6 · beta_pascal_table_prefix_extendAppend one semantic Pascal row to both outer beta prefixes.
theorem · proof layer 19 · 3 definitionsBT00T7 · beta_pascal_table_prefix_existsEvery finite width and height has a nested beta Pascal table.
theorem · proof layer 20 · 2 definitionsBT00T8 · choose_existsThe recurrence-defined Choose relation has a value for every pair.
theorem · proof layer 21 · 3 definitionsBT00T9 · beta_pascal_zero_row_pointwise_functionalZero-row values agree pointwise across beta encodings and widths.
theorem · proof layer 6 · 2 definitionsBT00TA · beta_pascal_row_step_pointwise_functionalPascal successor rows preserve pointwise agreement across encodings.
theorem · proof layer 6 · 2 definitionsBT00TB · beta_pascal_table_row_pointwise_functionalCorresponding decoded Pascal-table rows agree pointwise.
theorem · proof layer 7 · 2 definitionsBT00TC · choose_functionalThe recurrence-defined Choose relation is functional.
theorem · proof layer 8 · 3 definitionsBT00TD · choose_out_of_range_zeroAn out-of-range Choose value is zero.
theorem · proof layer 1 · 2 definitionsBT00TE · choose_zeroThe zeroth entry of every Pascal row is one.
theorem · proof layer 6 · 3 definitionsBT00TF · beta_pascal_table_diagonal_boundaryEvery decoded Pascal row has diagonal one and zeros above it.
theorem · proof layer 6 · 2 definitionsBT00TG · choose_selfThe recurrence-defined diagonal binomial coefficient is one.
theorem · proof layer 7 · 3 definitionsBT00TH · beta_pascal_table_successor_cell_recurrenceA decoded successor table cell is the sum of predecessor cells.
theorem · proof layer 6 · 2 definitionsBT00TI · choose_succ_succ_of_ltInterior Choose values satisfy Pascal's successor recurrence.
theorem · proof layer 8 · 4 definitionsBT00TJ · choose_succ_succRelational Choose values satisfy Pascal recurrence everywhere.
theorem · proof layer 9 · 2 definitionsBT00TK · choose_self_of_eqA column equal to its row has Choose value one.
theorem · proof layer 8 · 1 definitionsBT00TL · choose_symmetryComplementary columns have equal relational Choose values.
theorem · proof layer 22 · 1 definitionsBT00TM · choose_positiveEvery in-range relational Choose value is a successor.
theorem · proof layer 22 · 2 definitionsBT00TN · central_binom_existsEvery row has a relational central-binomial value.
theorem · proof layer 22 · 1 definitionsBT00TP · central_binom_positiveEvery relational central-binomial value is a successor.
theorem · proof layer 23 · 1 definitionsBT00TQ · central_binom_zeroThe zeroth relational central-binomial value is one.
theorem · proof layer 7 · 1 definitionsBT00TR · choose_upper_eq_transportChoose is invariant under equality of its upper index.
theorem · proof layer 0 · 1 definitionsBT00TS · central_binom_succ_double_middleA successor central binomial is twice its odd-row middle value.
theorem · proof layer 23 · 2 definitionsBT00TT · choose_weighted_verticalAdjacent rows satisfy the constructive weighted vertical identity.
theorem · proof layer 22 · 1 definitionsBT00TU · central_binom_succ_recurrenceSuccessive central binomials satisfy the weighted recurrence.
theorem · proof layer 24 · 2 definitionsBT00TV · factorial_length_eq_transportRelational factorial transports along equality of its length.
theorem · proof layer 0 · 1 definitionsBT00TW · factorial_weighted_product_combineWeighted factorial products combine by reassociation.
theorem · proof layer 4 · 0 definitionsBT00TX · choose_factorial_bridgeComplementary factorials represent each constructive Choose value.
theorem · proof layer 23 · 2 definitionsBT00TY · mul_lt_mul_right_nonzeroRight multiplication by a nonzero natural preserves strict order.
theorem · proof layer 6 · 2 definitionsBT00U0 · four_power_central_recurrence_stepA weighted central recurrence equation advances the strict four-power lower bound.
theorem · proof layer 7 · 1 definitionsBT00U1 · pow_four_four_exactA relational fourth power of four is the fourfold product.
theorem · proof layer 12 · 1 definitionsBT00U2 · central_binom_four_weighted_of_recurrenceThe fourth central binomial satisfies the compact weighted value.
theorem · proof layer 8 · 1 definitionsBT00U3 · four_pow_central_seed_packageThe strict central-binomial lower bound holds at index four.
theorem · proof layer 23 · 3 definitionsBT00U4 · four_pow_lt_mul_central_binomFor every index at least four, the fourth power is below the index-weighted central binomial.
theorem · proof layer 25 · 3 definitionsBT00U5 · primorial_factor_choice_existsEvery index has its exact prime-or-one selector factor.
theorem · proof layer 9 · 1 definitionsBT00U6 · primorial_factor_choice_functionalThe prime-or-one selector factor at a fixed index is unique.
theorem · proof layer 0 · 1 definitionsBT00U7 · primorial_factor_prefix_extendAppend one selector factor while preserving the previous prefix.
theorem · proof layer 17 · 3 definitionsBT00U8 · primorial_factor_prefix_existsEvery finite length has a beta-coded selector prefix.
theorem · proof layer 18 · 3 definitionsBT00UA · primorial_existsEvery natural index has a relational primorial value.
theorem · proof layer 19 · 5 definitionsBT00UC · primorial_zeroThe empty dense selector product is one.
theorem · proof layer 7 · 1 definitionsBT00UD · primorial_succ_decomposeA successor primorial splits into its previous value and selector.
theorem · proof layer 7 · 4 definitionsBT00UE · primorial_positiveEvery relational primorial value is a successor.
theorem · proof layer 8 · 2 definitionsBT00UF · primorial_index_eq_transportEqual indices transport the expanded Primorial relation.
theorem · proof layer 0 · 1 definitionsBT00UQ · beta_product_prefix_suffix_splitSplit a finite Product into an initial prefix and an aligned suffix.
theorem · proof layer 19 · 3 definitionsBT00UR · primorial_interval_factor_prefix_extendAppend one offset selector while preserving the prior interval.
theorem · proof layer 17 · 3 definitionsBT00US · primorial_interval_factor_prefix_existsEvery offset and length has a beta-coded selector interval.
theorem · proof layer 18 · 3 definitionsBT00UW · primorial_interval_factor_prefix_shiftAlign a full Primorial mask with an independent offset interval.
theorem · proof layer 6 · 4 definitionsBT00UX · primorial_factor_prefix_restrict_addRestrict a selector prefix of length a+l to its first a entries.
theorem · proof layer 3 · 3 definitionsBT00UY · primorial_prefix_interval_splitSplit Primorial(a+l) into its prefix and offset interval product.
theorem · proof layer 20 · 5 definitionsBT00VA · factorial_prime_divides_of_leEvery prime at most n divides the relational factorial n!.
theorem · proof layer 8 · 5 definitionsBT00VB · factorial_prime_le_of_dividesEvery prime divisor of n! is at most n.
theorem · proof layer 11 · 4 definitionsBT00VC · choose_prime_divides_betweenA prime between both denominator indices and the row divides Choose.
theorem · proof layer 24 · 6 definitionsBT00VD · beta_pairwise_coprime_product_divides_common_multipleA pairwise-coprime product divides every common multiple of its factors.
theorem · proof layer 12 · 5 definitionsBT00VE · primorial_interval_pairwise_coprimeDistinct positions in an interval decode coprime selector factors.
theorem · proof layer 10 · 4 definitionsBT00VF · primorial_interval_divides_choose_betweenA selector interval between both denominator indices divides Choose.
theorem · proof layer 25 · 7 definitionsBT00VG · primorial_even_interval_divides_centralThe selector interval (n,2n] divides the central coefficient.
theorem · proof layer 26 · 7 definitionsBT00VH · primorial_odd_interval_divides_middleThe selector interval (n+1,2n+1] divides the odd middle coefficient.
theorem · proof layer 26 · 7 definitionsBT00VI · primorial_even_interval_le_centralThe even Primorial interval is bounded by the central coefficient.
theorem · proof layer 27 · 7 definitionsBT00VJ · primorial_odd_interval_le_middleThe odd Primorial interval is bounded by the odd middle coefficient.
theorem · proof layer 27 · 7 definitionsBT00VK · central_binom_strong_upper_stepThe weighted recurrence preserves the strong factor-two bound.
theorem · proof layer 6 · 1 definitionsBT00VL · central_binom_recurrence_double_bundleThe recurrence and functional double-middle law share support.
theorem · proof layer 24 · 2 definitionsBT00VM · central_binom_strong_upper_of_lawsRecurrence and totality imply the positive-index strong bound.
theorem · proof layer 8 · 3 definitionsBT00VN · central_binom_upper_support_packageThe expensive recurrence, middle, and totality laws close once.
theorem · proof layer 25 · 2 definitionsBT00VO · central_binom_strong_upperTwice a positive-index central binomial is at most four-power.
theorem · proof layer 26 · 4 definitionsBT00VP · central_binom_odd_middle_le_four_powThe odd-row middle coefficient is at most four to the half-row.
theorem · proof layer 26 · 4 definitionsBT00VQ · primorial_oneThe inclusive Primorial at one is exactly one.
theorem · proof layer 8 · 2 definitionsBT00VR · double_half_predecessor_dataAn even successor has a nonzero half below its predecessor.
theorem · proof layer 5 · 1 definitionsBT00VS · odd_positive_prefix_predecessor_boundThe positive prefix half of an odd successor is smaller.
theorem · proof layer 5 · 1 definitionsBT00VT · central_binom_nonzero_strong_upperThe strong central bound extends to every nonzero index.
theorem · proof layer 27 · 3 definitionsBT00VU · primorial_four_power_support_packageThe large interval and coefficient laws close once.
theorem · proof layer 28 · 9 definitionsBT00VV · primorial_le_four_pow_boundedEvery bounded Primorial is at most the matching fourth power.
theorem · proof layer 28 · 9 definitionsBT00VW · primorial_le_four_powThe inclusive Primorial is bounded by four to its index.
theorem · proof layer 29 · 3 definitionsBT00VX · central_binom_prime_divisor_le_doubleEvery prime divisor of a central coefficient is at most 2*n.
theorem · proof layer 24 · 5 definitionsBT00VY · no_bertrand_central_prime_divisor_leA no-Bertrand certificate forces central prime divisors below n.
theorem · proof layer 25 · 5 definitionsBT00W0 · power_valuation_nonzero_exponent_divides_baseA nonzero valuation exponent exposes the base as a divisor.
theorem · proof layer 21 · 4 definitionsBT00W2 · no_bertrand_central_prime_divisor_rangesEvery central prime divisor lies in one of the three live ranges.
theorem · proof layer 26 · 5 definitionsBT00W3 · pow_block_bound_from_totalA supplied power bound remains true after a common block multiplier.
theorem · proof layer 11 · 2 definitionsBT00W4 · pow_three_five_le_pow_four_four_from_totalThe concrete seed inequality 3^5 <= 4^4 in the relational graph.
theorem · proof layer 11 · 2 definitionsBT00W5 · pow_eleven_two_le_pow_two_seven_from_totalThe concrete seed inequality 11^2 <= 2^7 in the relational graph.
theorem · proof layer 14 · 2 definitionsBT00W6 · pow_six_ten_le_pow_four_thirteen_from_totalThe block seed 6^10 <= 4^13 used by the finite H window.
theorem · proof layer 14 · 2 definitionsBT00W7 · linear_square_budgetA factorized linear budget lies below a square by an explicit gap.
theorem · proof layer 5 · 1 definitionsBT00W8 · bertrand_scaled_budget_root_32The factorized RFC-v1 H budget at root 32 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00W9 · bertrand_scaled_budget_root_33The factorized RFC-v1 H budget at root 33 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00WA · bertrand_scaled_budget_root_34The factorized RFC-v1 H budget at root 34 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00WB · bertrand_scaled_budget_root_35The factorized RFC-v1 H budget at root 35 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00WC · bertrand_scaled_budget_root_36The factorized RFC-v1 H budget at root 36 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00WD · bertrand_scaled_budget_root_37The factorized RFC-v1 H budget at root 37 lies below its square.
theorem · proof layer 6 · 1 definitionsBT00WE · ceil_div_six_budget_of_scaled_leA scaled lower bound cancels against the lower half of CeilDivSix.
theorem · proof layer 5 · 2 definitionsBT00WF · pow_six_six_le_pow_four_eight_from_totalThe capacity-safe residual block 6^6 <= 4^8.
theorem · proof layer 14 · 3 definitionsBT00WG · pow_six_four_le_pow_four_six_from_totalThe capacity-safe residual block 6^4 <= 4^6.
theorem · proof layer 14 · 3 definitionsBT00WH · pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_totalThe seed 3^5 <= 4^4 extends by blocks and one residual factor.
theorem · proof layer 12 · 3 definitionsBT00WI · pow_two_double_eq_pow_four_from_totalAn even power of two is the matching power of four.
theorem · proof layer 14 · 1 definitionsBT00WJ · pow_two_successor_double_le_pow_four_successor_from_totalAn odd power of two is bounded by the next power of four.
theorem · proof layer 15 · 3 definitionsBT00WK · pow_eleven_double_block_le_pow_two_seven_block_from_totalThe seed 11^2 <= 2^7 extends through a common block count.
theorem · proof layer 15 · 2 definitionsBT00WL · pow_eleven_double_block_le_pow_four_even_from_totalAn even 11-to-2 block exponent converts exactly to base four.
theorem · proof layer 16 · 2 definitionsBT00WM · pow_eleven_double_block_le_pow_four_odd_from_totalAn odd 11-to-2 block exponent converts to the next base-four power.
theorem · proof layer 16 · 2 definitionsBT00WN · pow_six_ten_block_le_pow_four_thirteen_block_from_totalThe seed 6^10 <= 4^13 extends through a common block count.
theorem · proof layer 15 · 2 definitionsBT00WO · pow_thirty_six_double_block_eq_pow_six_four_block_from_totalA double block of base thirty six is a fourfold block of base six.
theorem · proof layer 12 · 1 definitionsBT00WP · bertrand_h_root_32_from_totalThe RFC-v1 H envelope at the fixed root 32.
theorem · proof layer 17 · 3 definitionsBT00WQ · bertrand_h_root_33_from_totalThe RFC-v1 H envelope at the fixed root 33.
theorem · proof layer 16 · 4 definitionsBT00WR · bertrand_h_root_34_from_totalThe RFC-v1 H envelope at the fixed root 34.
theorem · proof layer 16 · 4 definitionsBT00WS · bertrand_h_root_35_from_totalThe RFC-v1 H envelope at the fixed root 35.
theorem · proof layer 16 · 4 definitionsBT00WT · bertrand_h_root_36_from_totalThe RFC-v1 H envelope at the fixed root 36.
theorem · proof layer 17 · 4 definitionsBT00WU · bertrand_h_root_37_from_totalThe RFC-v1 H envelope at the fixed root 37.
theorem · proof layer 17 · 4 definitionsBT00WV · bertrand_j_base_thirty_two_window_from_totalThe RFC-v1 J envelope uniformly covers roots 32 through 37.
theorem · proof layer 17 · 3 definitionsBT00WW · bertrand_hj_base_window_thirty_two_from_totalAll six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.
theorem · proof layer 18 · 4 definitionsBT00WX · scaled_factor_square_identityA factorization of a transports its square without expanding either factor.
theorem · proof layer 3 · 0 definitionsBT00WY · thirty_two_square_eq_twice_sixteen_times_thirty_twoThe root-32 square identity carried by the shallow factorization 16*32.
theorem · proof layer 4 · 0 definitionsBT00X0 · floor_sqrt_factorized_threshold_thirty_twoThe factorized large-input threshold forces every selected root to be at least 32.
theorem · proof layer 7 · 3 definitionsBT00X1 · six_block_window_decomposition_above_thirty_twoEvery s>=32 is a six-step iterate of one base root in the exact window 32..37.
theorem · proof layer 3 · 3 definitionsBT00X2 · bertrand_hj_six_block_iterate_from_totalThe common H/J invariant iterates constructively over every six-step block.
theorem · proof layer 19 · 4 definitionsBT00X3 · bertrand_hj_envelope_thirty_twoAll roots s>=32 satisfy both H and J after discharging power totality once.
theorem · proof layer 20 · 4 definitionsBT00X4 · bertrand_floor_power_product_le_h_from_totalThe floor-root power product is bounded by the H envelope using one supplied power-totality premise.
theorem · proof layer 12 · 4 definitionsBT00X5 · bertrand_four_power_product_le_of_sum_from_totalFourth-power factors are bounded by the power at every larger exponent sum.
theorem · proof layer 11 · 3 definitionsBT00X6 · bertrand_main_inequality_factorized_from_totalThe factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.
theorem · proof layer 21 · 6 definitionsBT00X7 · bertrand_main_inequality_factorizedThe factorized B6 inequality discharges relational-power totality exactly once.
theorem · proof layer 22 · 4 definitionsBT00X8 · bertrand_main_inequality_natThe public B6 surface retains n+n and reaches the factorized internal theorem through five checked equality rewrites.
theorem · proof layer 23 · 4 definitionsBT00X9 · beta_product_pointwise_lePointwise bounded decoded prefixes have ordered finite products.
theorem · proof layer 7 · 4 definitionsBT00XA · beta_product_uniform_le_powA uniformly bounded finite product is at most the matching power.
theorem · proof layer 8 · 5 definitionsBT00XB · add_lt_addStrict inequalities add componentwise.
theorem · proof layer 4 · 1 definitionsBT00XC · add_lt_cancel_leftA common left summand cancels from strict witness order.
theorem · proof layer 3 · 1 definitionsBT00XF · division_zero_quotient_of_ltA dividend below its divisor has quotient zero.
theorem · proof layer 5 · 2 definitionsBT00XG · division_double_quotient_bitDoubling a dividend changes its quotient by one binary carry.
theorem · proof layer 5 · 2 definitionsBT00XJ · pow_le_pow_of_exponent_leRelational powers are monotone in the exponent above base one.
theorem · proof layer 20 · 3 definitionsBT00XK · pow_tail_strict_of_squareEvery exponent-two-or-larger power lies above the square tail.
theorem · proof layer 21 · 3 definitionsBT00XL · power_valuation_value_eq_transportPower valuation transports along equality of its valued number.
theorem · proof layer 0 · 1 definitionsBT00XM · central_binom_factorial_valuation_balanceThe central valuation is the doubled-column factorial deficit.
theorem · proof layer 25 · 4 definitionsBT00XN · central_binom_legendre_valuation_balanceFactorial Legendre equality exposes the central carry balance.
theorem · proof layer 28 · 5 definitionsBT00XO · prime_power_quotient_zero_of_exponent_gtA prime-power quotient vanishes once its exponent exceeds the dividend.
theorem · proof layer 11 · 5 definitionsBT00XP · power_quotient_prefix_tail_entry_zeroEvery decoded quotient entry at or beyond the dividend is zero.
theorem · proof layer 12 · 7 definitionsBT00XQ · power_quotient_prefix_sum_extend_zeroZero quotient tails preserve the finite Legendre sum.
theorem · proof layer 13 · 7 definitionsBT00XR · legendre_sum_extended_prefix_existsA Legendre sum admits an arbitrarily long zero-extended quotient code.
theorem · proof layer 21 · 4 definitionsBT00XV · double_quotient_carry_choiceEach pair of doubled quotients has a constructive carry bit.
theorem · proof layer 9 · 5 definitionsBT00XW · double_quotient_carry_prefix_extendA carry prefix extends by one freshly decoded carry bit.
theorem · proof layer 17 · 2 definitionsBT00XX · double_quotient_carry_prefix_existsDoubled quotient prefixes admit a beta-coded carry prefix.
theorem · proof layer 18 · 3 definitionsBT00XY · double_quotient_carry_prefix_all_bitsEvery value in a carry prefix is zero or one.
theorem · proof layer 0 · 3 definitionsBT00Y0 · double_quotient_carry_prefix_restrictDropping the final position preserves a carry prefix.
theorem · proof layer 2 · 2 definitionsBT00Y1 · bit_count_positive_last_oneA positive bit count has a one at an index at least its count.
theorem · proof layer 9 · 3 definitionsBT00Y2 · division_successor_quotient_divisor_leA division with successor quotient bounds its divisor by the dividend.
theorem · proof layer 2 · 2 definitionsBT00Y3 · beta_sum_double_carry_exactThe doubled quotient sum is twice the source sum plus its carries.
theorem · proof layer 8 · 4 definitionsBT00Y4 · central_binom_carry_bit_countThe valuation exponent is exactly the number of doubled-quotient carries.
theorem · proof layer 29 · 10 definitionsBT00Y5 · central_binom_prime_power_contribution_le_doubleEvery complete prime-power contribution is bounded by twice n.
theorem · proof layer 30 · 10 definitionsBT00Y6 · central_binom_prime_square_tail_exponent_not_two_leA prime square above twice n rules out valuation exponent two.
theorem · proof layer 31 · 6 definitionsBT00Y7 · central_binom_prime_square_tail_valuation_le_oneAbove the square tail, a central-binomial valuation is at most one.
theorem · proof layer 32 · 6 definitionsBT00Y8 · division_quotient_one_of_boundsBounds between one and two divisors force quotient one.
theorem · proof layer 4 · 3 definitionsBT00Y9 · division_quotient_two_of_boundsBounds between two and three divisors force quotient two.
theorem · proof layer 4 · 3 definitionsBT00YA · prime_square_tail_of_two_three_rangeThe scaled two-thirds range places the prime square above 2*n.
theorem · proof layer 12 · 4 definitionsBT00YB · division_first_two_of_two_three_rangeThe two-thirds range fixes the first quotients at one and two.
theorem · proof layer 5 · 3 definitionsBT00YC · double_quotient_carry_prefix_entries_zeroExact doubled quotients and a square tail force every carry to zero.
theorem · proof layer 22 · 6 definitionsBT00YD · central_binom_prime_valuation_zero_of_exact_double_quotientsAn all-zero carry prefix forces the exact central valuation to zero.
theorem · proof layer 30 · 10 definitionsBT00YE · central_binom_prime_valuation_zero_two_thirds_rangePrimes in the open two-thirds range contribute zero valuation.
theorem · proof layer 31 · 7 definitionsBT00YF · division_three_scaled_upper_of_quotient_ltA quotient below p places the dividend strictly below 3*p.
theorem · proof layer 3 · 3 definitionsBT00YG · central_binom_prime_valuation_zero_above_third_quotientValuation vanishes above the floor of two-thirds and at most n.
theorem · proof layer 32 · 6 definitionsBT00YH · floor_sqrt_above_root_power_two_strictA prime above a floor root has square strictly above the value.
theorem · proof layer 12 · 4 definitionsBT00YI · central_binom_prime_above_floor_sqrt_valuation_le_oneAbove the floor root, a central prime valuation is at most one.
theorem · proof layer 33 · 7 definitionsBT00YJ · no_bertrand_central_nonzero_valuation_live_rangesEvery nonzero central valuation lies in one of two live ranges.
theorem · proof layer 33 · 7 definitionsBT00YK · no_bertrand_central_nonzero_valuation_factor_rangesThe middle live range has exact valuation exponent one.
theorem · proof layer 34 · 7 definitionsBT00YL · no_bertrand_central_nonzero_contribution_factor_rangesA nonzero contribution is small-bounded or one middle prime.
theorem · proof layer 35 · 8 definitionsBT00YM · no_bertrand_central_prime_contribution_rangesEvery central prime contribution has one reviewed factor form.
theorem · proof layer 36 · 8 definitionsBT00YN · prime_contribution_choice_existsEvery index has its complete prime-power contribution or one.
theorem · proof layer 24 · 3 definitionsBT00YO · prime_contribution_choice_functionalThe complete contribution at a fixed index is unique.
theorem · proof layer 9 · 3 definitionsBT00YP · prime_contribution_prefix_extendAppend one contribution while preserving the old prefix.
theorem · proof layer 25 · 5 definitionsBT00YQ · prime_contribution_prefix_existsEvery number and finite length has a contribution prefix.
theorem · proof layer 26 · 5 definitionsBT00YS · prime_contribution_product_existsEvery number and finite length has a contribution Product.
theorem · proof layer 27 · 6 definitionsBT00YU · coprime_power_rightA power preserves coprimality with a fixed left operand.
theorem · proof layer 12 · 2 definitionsBT00YV · coprime_powersPowers of coprime bases are coprime.
theorem · proof layer 13 · 2 definitionsBT00YW · prime_contribution_prefix_pairwise_coprimeDistinct contribution positions decode pairwise-coprime values.
theorem · proof layer 14 · 6 definitionsBT00YX · prime_contribution_factor_dividesEvery complete contribution factor divides its source number.
theorem · proof layer 9 · 5 definitionsBT00YY · prime_contribution_product_dividesEvery finite complete-contribution Product divides its source.
theorem · proof layer 15 · 8 definitionsBT0100 · prime_contribution_selected_entryA selected prime position exposes its valuation power in the product.
theorem · proof layer 8 · 7 definitionsBT0101 · prime_contribution_selected_successor_dividesA prime in the remaining cofactor raises a selected power.
theorem · proof layer 21 · 3 definitionsBT0102 · prime_contribution_cofactor_prime_contradictionA prime divisor of the remaining cofactor contradicts maximality.
theorem · proof layer 22 · 9 definitionsBT0103 · prime_contribution_cofactor_eq_oneA supported contribution cofactor is the multiplicative unit.
theorem · proof layer 23 · 8 definitionsBT0104 · prime_contribution_reverse_dividesA supported complete contribution product is a multiple of its source.
theorem · proof layer 24 · 8 definitionsBT0105 · prime_contribution_product_eqEvery supported complete contribution product equals its source.
theorem · proof layer 25 · 8 definitionsBT0106 · prime_contribution_complete_existsEvery nonzero source has an exact supported contribution product.
theorem · proof layer 28 · 8 definitionsBT0107 · central_binom_prime_contribution_product_existsA central coefficient is exactly its complete contribution product.
theorem · proof layer 29 · 9 definitionsBT0108 · no_bertrand_central_contribution_choice_rangesEach central contribution lies in a reviewed factor range.
theorem · proof layer 37 · 8 definitionsBT010A · two_lt_double_lower_sixA natural above two has double at least three plus three.
theorem · proof layer 3 · 2 definitionsBT010B · floor_sqrt_two_le_of_two_ltThe floor root of twice a natural above two is at least two.
theorem · proof layer 4 · 3 definitionsBT010C · three_mul_le_square_of_three_leEvery natural at least three dominates three times itself by its square.
theorem · proof layer 6 · 2 definitionsBT010D · floor_sqrt_three_mul_le_doubleThree times the floor root lies below the doubled input.
theorem · proof layer 7 · 3 definitionsBT010E · division_quotient_lower_of_scaled_leA scaled lower bound forces the division quotient above its scale index.
theorem · proof layer 3 · 3 definitionsBT010F · floor_sqrt_le_third_quotientThe floor root is at most the quotient of the doubled input by three.
theorem · proof layer 8 · 4 definitionsBT010G · floor_sqrt_third_quotient_gap_existsThe floor-root cut has an exact additive gap to the third quotient.
theorem · proof layer 9 · 4 definitionsBT010H · division_quotient_le_dividendThe quotient by three is bounded by its doubled dividend.
theorem · proof layer 7 · 3 definitionsBT010I · third_quotient_double_gap_existsThe third quotient has an exact additive gap to the doubled input.
theorem · proof layer 8 · 2 definitionsBT010J · floor_third_double_gap_packagePackage the two exact additive gaps used by the three-range split.
theorem · proof layer 10 · 3 definitionsBT010K · prime_contribution_interval_prefix_extendAppend one contribution choice to an offset interval prefix.
theorem · proof layer 25 · 5 definitionsBT010L · prime_contribution_interval_prefix_existsEvery number, offset, and length has a contribution prefix.
theorem · proof layer 26 · 5 definitionsBT010P · prime_contribution_interval_prefix_shiftAlign a full contribution prefix with its independent suffix.
theorem · proof layer 10 · 6 definitionsBT010Q · prime_contribution_prefix_restrict_addRestrict a contribution prefix of length a+l to length a.
theorem · proof layer 3 · 5 definitionsBT010R · prime_contribution_prefix_interval_splitSplit a contribution Product into prefix and offset interval.
theorem · proof layer 27 · 6 definitionsBT010S · prime_contribution_product_length_eq_transportTransport only the length carrier of a contribution Product.
theorem · proof layer 0 · 6 definitionsBT010U · beta_product_all_one_exactA Product whose decoded factors are all one is exactly one.
theorem · proof layer 7 · 3 definitionsBT010V · no_bertrand_small_contribution_choice_le_doubleEvery small-range contribution is bounded by the doubled row.
theorem · proof layer 38 · 8 definitionsBT010W · no_bertrand_middle_contribution_choice_le_selectorMiddle-range contributions are bounded by dense selector factors.
theorem · proof layer 38 · 8 definitionsBT010X · no_bertrand_high_contribution_choice_eq_oneEvery contribution above the third quotient is neutral.
theorem · proof layer 38 · 8 definitionsBT010Y · no_bertrand_small_contribution_product_le_powerThe small contribution Product is bounded by (2n)^s.
theorem · proof layer 39 · 10 definitionsBT0110 · no_bertrand_middle_contribution_interval_le_primorial_intervalThe middle contribution interval is bounded by its selector interval.
theorem · proof layer 39 · 10 definitionsBT0111 · no_bertrand_middle_contribution_interval_le_four_powThe middle contribution interval is bounded by four to q.
theorem · proof layer 40 · 11 definitionsBT0112 · no_bertrand_high_contribution_interval_eq_oneThe high contribution interval is the multiplicative unit.
theorem · proof layer 39 · 10 definitionsBT0113 · central_binom_factorization_smallThe complete central contribution Product has only two live ranges.
theorem · proof layer 40 · 10 definitionsBT0114 · central_binom_le_of_no_bertrand_primeNo Bertrand prime forces the reviewed central-binomial upper bound.
theorem · proof layer 41 · 10 definitionsBT0115 · bertrand_eventually_closed_upperEvery n at least 16*32 has a prime in the constructive open-closed Bertrand interval.
theorem · proof layer 42 · 7 definitionsBT0116 · fixed_nontrivial_factor_not_primeA displayed nontrivial factorization refutes primality.
theorem · proof layer 0 · 1 definitionsBT0117 · factor_pair_has_small_member_below_squareA factor pair below (B+1)^2 has a member at most B.
theorem · proof layer 6 · 2 definitionsBT0118 · nonprime_has_small_prime_divisor_below_squareEvery composite below (B+1)^2 has a prime divisor at most B.
theorem · proof layer 10 · 4 definitionsBT0119 · prime_of_no_small_prime_divisor_below_squareTrial division by primes through B certifies numbers below (B+1)^2.
theorem · proof layer 11 · 4 definitionsBT011A · prime_le_twenty_two_casesThe only primes at most twenty-two are the eight displayed values.
theorem · proof layer 3 · 3 definitionsBT011B · nonzero_remainder_not_multipleA nonzero proper remainder refutes divisibility.
theorem · proof layer 4 · 3 definitionsBT011C · scaled_remainder_liftScale a quotient-remainder equation and normalize its new tail.
theorem · proof layer 4 · 0 definitionsBT011E · double_scaled_remainder_liftCompose the two bounded scaling steps used by the 521 certificate.
theorem · proof layer 5 · 0 definitionsBT011F · prime_fiveA native checked trial-division certificate for 5.
theorem · proof layer 12 · 3 definitionsBT011G · prime_sevenA native checked trial-division certificate for 7.
theorem · proof layer 12 · 3 definitionsBT011H · prime_thirteenA native checked trial-division certificate for 13.
theorem · proof layer 12 · 3 definitionsBT011I · prime_twenty_threeA native checked trial-division certificate for 23.
theorem · proof layer 12 · 3 definitionsBT011J · prime_forty_threeA native checked trial-division certificate for 43.
theorem · proof layer 12 · 3 definitionsBT011K · prime_eighty_threeA native checked trial-division certificate for 83.
theorem · proof layer 12 · 3 definitionsBT011L · prime_one_hundred_sixty_threeA native checked trial-division certificate for 163.
theorem · proof layer 12 · 3 definitionsBT011M · prime_three_hundred_seventeenA native checked trial-division certificate for 317.
theorem · proof layer 12 · 3 definitionsBT011N · prime_five_hundred_twenty_oneA native checked trial-division certificate for 521.
theorem · proof layer 12 · 3 definitionsBT011O · bertrand_add_swap_nestedSwap the first two addends under a fixed trailing addend.
theorem · proof layer 2 · 0 definitionsBT011P · bertrand_add_six_permuteNormalize the six addends used by the 163-to-317 cover.
theorem · proof layer 3 · 0 definitionsBT011Q · bertrand_covering_intervalOne checked adjacent cover supplies a Bertrand witness.
theorem · proof layer 3 · 3 definitionsBT011R · bertrand_cover_one_twoThe checked finite cover inequality from 1 to 2.
theorem · proof layer 0 · 1 definitionsBT011S · bertrand_cover_two_threeThe checked finite cover inequality from 2 to 3.
theorem · proof layer 0 · 1 definitionsBT011T · bertrand_cover_three_fiveThe checked finite cover inequality from 3 to 5.
theorem · proof layer 0 · 1 definitionsBT011U · bertrand_cover_five_sevenThe checked finite cover inequality from 5 to 7.
theorem · proof layer 0 · 1 definitionsBT011V · bertrand_cover_seven_thirteenThe checked finite cover inequality from 7 to 13.
theorem · proof layer 0 · 1 definitionsBT011W · bertrand_cover_thirteen_twenty_threeThe checked finite cover inequality from 13 to 23.
theorem · proof layer 0 · 1 definitionsBT011X · bertrand_cover_twenty_three_forty_threeThe checked finite cover inequality from 23 to 43.
theorem · proof layer 0 · 1 definitionsBT011Y · bertrand_cover_forty_three_eighty_threeThe checked finite cover inequality from 43 to 9 * 9 + 2.
theorem · proof layer 0 · 1 definitionsBT0120 · bertrand_cover_eighty_three_one_hundred_sixty_threeThe compact checked cover from 83 to 163.
theorem · proof layer 5 · 1 definitionsBT0121 · bertrand_cover_one_hundred_sixty_three_three_hundred_seventeenThe compact checked cover from 163 to 317.
theorem · proof layer 5 · 1 definitionsBT0122 · bertrand_cover_three_hundred_seventeen_five_hundred_twenty_oneThe compact checked cover from 317 to 521.
theorem · proof layer 5 · 1 definitionsBT0123 · bertrand_cutoff_lt_final_primeThe factorized production cutoff lies below the final prime.
theorem · proof layer 5 · 1 definitionsBT0124 · bertrand_small_closed_upperEvery nonzero input below 16*32 has a closed Bertrand witness.
theorem · proof layer 13 · 3 definitionsBT0125 · bertrand_closed_upperEvery nonzero natural has a prime in its open-closed Bertrand interval.
theorem · proof layer 43 · 3 definitionsBT0126 · bertrand_upper_endpoint_factorizationThe closed upper endpoint is composite whenever 1<n.
theorem · proof layer 5 · 2 definitionsBT0127 · bertrand_strictEvery n greater than one has a prime strictly below n+n.
theorem · proof layer 44 · 3 definitions