BT0000 · zero_add
Zero is a left identity for addition; unlike PA3, this needs induction.
layer 0 · 3 lines · Stable · empty-context checkedBT0001 · add_succ_left
A successor can move through addition on the left.
layer 0 · 4 lines · Stable · empty-context checkedBT0002 · add_comm
Addition is commutative.
layer 1 · 4 lines · Stable · empty-context checkedBT0003 · add_assoc
Addition is associative.
layer 0 · 5 lines · Stable · empty-context checkedBT0004 · mul_zero_left
Zero annihilates multiplication on the left.
layer 0 · 3 lines · Stable · empty-context checkedBT0005 · mul_succ_left
A successor can move through multiplication on the left.
layer 2 · 6 lines · Stable · empty-context checkedBT0006 · mul_comm
Multiplication is commutative.
layer 3 · 4 lines · Stable · empty-context checkedBT0007 · mul_add
Multiplication distributes over addition on the right.
layer 1 · 5 lines · Stable · empty-context checkedBT0008 · mul_assoc
Multiplication is associative.
layer 2 · 5 lines · Stable · empty-context checkedBT0009 · one_mul
One is a left identity for multiplication.
layer 0 · 3 lines · Stable · empty-context checkedBT000A · mul_one
One is a right identity for multiplication.
layer 1 · 2 lines · Stable · empty-context checkedBT000B · add_mul
Multiplication distributes over addition on the left.
layer 4 · 4 lines · Stable · empty-context checkedBT000C · succ_ne_zero
No successor is zero (the reusable PA1 lemma).
layer 0 · 1 lines · Stable · empty-context checkedBT000D · succ_injective
Successor is injective (the reusable PA2 lemma).
layer 0 · 1 lines · Stable · empty-context checkedBT000E · le_refl
The defined order is reflexive; zero is its witness.
layer 1 · 3 lines · Stable · empty-context checkedBT000F · le_trans
Order witnesses compose by addition, so the defined order is transitive.
layer 1 · 9 lines · Stable · empty-context checkedBT000G · no_succ_add_fixed
Adding a positive successor cannot leave a natural number fixed.
layer 0 · 11 lines · Stable · empty-context checkedBT000H · drop_add_prefix_from_fixed
A fixed-point equation remains fixed after dropping an additive prefix.
layer 1 · 17 lines · Stable · empty-context checkedBT000I · antisymm_from_witnesses
Opposing additive witnesses force equality.
layer 2 · 19 lines · Stable · empty-context checkedBT000J · le_antisymm
The witness-defined order is antisymmetric.
layer 3 · 9 lines · Stable · empty-context checkedBT000K · le_total
Every pair of natural numbers is comparable in the defined order.
layer 0 · 23 lines · Stable · empty-context checkedBT000L · add_eq_zero_right
A sum equal to zero has zero as its right addend.
layer 0 · 9 lines · Stable · empty-context checkedBT000M · mul_eq_zero
Zero products have a zero factor: the 23-entry core capstone.
layer 1 · 12 lines · Stable · empty-context checkedBT000Q · zero_or_succ
Every natural is either zero or the successor of a natural.
layer 0 · 6 lines · Stable · empty-context checkedBT000R · nonzero_is_succ
Every nonzero natural has a predecessor.
layer 0 · 8 lines · Stable · empty-context checkedBT000S · add_congr
Addition preserves equality in both arguments.
layer 0 · 9 lines · Stable · empty-context checkedBT000T · mul_congr
Multiplication preserves equality in both arguments.
layer 0 · 9 lines · Stable · empty-context checkedBT000U · add_right_cancel
A common right addend can be cancelled.
layer 0 · 13 lines · Stable · empty-context checkedBT000V · add_left_cancel
A common left addend can be cancelled.
layer 2 · 13 lines · Stable · empty-context checkedBT000W · zero_le
Zero is below every natural number.
layer 0 · 4 lines · Stable · empty-context checkedBT000X · le_succ_self
Every natural number is below its successor.
layer 1 · 3 lines · Stable · empty-context checkedBT000Y · le_zero
Only zero is less than or equal to zero.
layer 1 · 5 lines · Stable · empty-context checkedBT0010 · one_le_of_ne_zero
Every nonzero natural is at least one.
layer 0 · 8 lines · Stable · empty-context checkedBT0011 · ne_zero_of_one_le
A natural at least one is nonzero.
layer 0 · 8 lines · Stable · empty-context checkedBT0012 · le_add_left
Adding on the left produces an explicit order witness.
layer 0 · 4 lines · Stable · empty-context checkedBT0013 · le_add_right
Adding on the right produces an explicit order witness.
layer 2 · 4 lines · Stable · empty-context checkedBT0014 · add_le_add_right
Adding the same right summand preserves the witness-defined order.
layer 1 · 12 lines · Stable · empty-context checkedBT0015 · add_le_add_left
Adding the same left summand preserves the witness-defined order.
layer 2 · 18 lines · Stable · empty-context checkedBT0016 · succ_le_succ
Successor preserves the witness-defined order.
layer 0 · 8 lines · Stable · empty-context checkedBT0017 · le_of_succ_le_succ
Successor order reflects to the underlying naturals.
layer 0 · 10 lines · Stable · empty-context checkedBT0018 · le_succ
A weak inequality remains true after raising its upper bound by one.
layer 1 · 9 lines · Stable · empty-context checkedBT0019 · lt_to_le
A witnessed strict inequality entails the corresponding weak inequality.
layer 1 · 11 lines · Stable · empty-context checkedBT001B · lt_irrefl_expanded
No natural is strictly below itself, with strict order fully expanded.
layer 1 · 12 lines · Stable · empty-context checkedBT001C · le_eq_or_lt
A witnessed inequality is either equality or a witnessed strict inequality.
layer 1 · 21 lines · Stable · empty-context checkedBT001D · lt_of_lt_of_le
Strict order followed by weak order remains strict.
layer 2 · 11 lines · Stable · empty-context checkedBT001E · lt_of_le_of_lt
Weak order followed by strict order remains strict.
layer 1 · 13 lines · Stable · empty-context checkedBT001F · lt_trans
Strict order is transitive.
layer 1 · 20 lines · Stable · empty-context checkedBT001G · le_or_lt
Any two naturals satisfy weak order in one direction or strict order in the other.
layer 0 · 26 lines · Stable · empty-context checkedBT001H · lt_trichotomy
Two naturals are equal or strictly ordered in exactly one displayed direction.
layer 0 · 39 lines · Stable · empty-context checkedBT001I · lt_not_le
A strict inequality excludes the reverse weak inequality.
layer 0 · 34 lines · Stable · empty-context checkedBT001J · le_not_lt
A weak inequality excludes strict inequality in the reverse direction.
layer 1 · 9 lines · Stable · empty-context checkedBT001K · lt_not_eq_add_middle
A strict upper bound prevents the lower term from containing that bound as an additive middle block.
layer 1 · 44 lines · Stable · empty-context checkedBT001L · mul_le_mul_left
Left multiplication preserves the witness-defined order.
layer 2 · 12 lines · Stable · empty-context checkedBT001M · mul_le_mul_right
Right multiplication preserves the witness-defined order.
layer 5 · 12 lines · Stable · empty-context checkedBT001N · mul_lt_mul_succ_left_nonzero
Multiplication by a nonzero left factor strictly increases across a successor step.
layer 2 · 19 lines · Stable · empty-context checkedBT001O · division_remainder_succ
Every dividend has a quotient and bounded remainder for a successor divisor.
layer 1 · 38 lines · Stable · empty-context checkedBT001P · division_remainder_exists
Every positive divisor admits a quotient and a strictly bounded remainder.
layer 2 · 14 lines · Stable · empty-context checkedBT001R · division_block_upper
A bounded remainder keeps its decomposition below the next divisor block.
layer 2 · 34 lines · Stable · empty-context checkedBT001S · positive_quotient_gap_impossible
A positive gap between quotients makes two bounded-remainder decompositions unequal.
layer 3 · 34 lines · Stable · empty-context checkedBT001U · division_remainder_unique
Bounded quotient-remainder decompositions have unique quotients and remainders.
layer 4 · 74 lines · Stable · empty-context checkedBT001V · zero_remainder_implies_multiple
A quotient decomposition with zero remainder supplies a divisibility witness.
layer 0 · 7 lines · Stable · empty-context checkedBT001W · multiple_has_zero_remainder
Every multiple of a nonzero divisor has a bounded zero-remainder decomposition.
layer 1 · 21 lines · Stable · empty-context checkedBT001X · add_eq_zero_left
A sum equal to zero has zero as its left addend.
layer 2 · 9 lines · Stable · empty-context checkedBT0020 · mul_eq_one_components
A product is one only when both natural factors are one.
layer 1 · 39 lines · Stable · empty-context checkedBT0021 · mul_ne_zero
A product of two nonzero naturals is nonzero.
layer 2 · 15 lines · Stable · empty-context checkedBT0022 · mul_left_cancel_nonzero
A nonzero common left factor can be cancelled.
layer 3 · 42 lines · Stable · empty-context checkedBT0024 · two_large_factors_impossible
Two naturals at least two cannot multiply to two.
layer 3 · 28 lines · Stable · empty-context checkedBT0025 · prime_two
Two is prime in the expanded first-order prime predicate.
layer 4 · 35 lines · Stable · empty-context checkedBT0026 · multiple_zero
Zero is a multiple of every natural number.
layer 0 · 4 lines · Stable · empty-context checkedBT0027 · one_multiple
Every natural number is a multiple of one.
layer 1 · 4 lines · Stable · empty-context checkedBT0028 · multiple_refl
Every natural number is a multiple of itself.
layer 2 · 4 lines · Stable · empty-context checkedBT002A · multiple_mul_right
A right multiple of a multiple remains a multiple.
layer 3 · 8 lines · Stable · empty-context checkedBT002B · multiple_mul_left
A left multiple of a multiple remains a multiple.
layer 4 · 9 lines · Stable · empty-context checkedBT002C · multiple_trans
The multiple relation is transitive.
layer 3 · 11 lines · Stable · empty-context checkedBT002D · divisor_le_nonzero
A divisor of a nonzero natural is bounded by that natural.
layer 1 · 31 lines · Stable · empty-context checkedBT002E · divisor_one
Every natural divisor of one equals one.
layer 2 · 11 lines · Stable · empty-context checkedBT002F · multiple_antisymm
Mutual divisibility is antisymmetric over natural numbers.
layer 4 · 50 lines · Stable · empty-context checkedBT002G · factor_difference
A common-factor difference is itself a multiple of that factor.
layer 2 · 47 lines · Stable · empty-context checkedBT002H · divides_remainder
A common divisor of a dividend and divisor also divides the remainder.
layer 3 · 24 lines · Stable · empty-context checkedBT002I · divides_linear_step
A common divisor of a divisor and remainder divides their Euclidean linear step.
layer 3 · 17 lines · Stable · empty-context checkedBT002L · is_gcd_zero_right
Every natural is the relational gcd of itself and zero.
layer 3 · 11 lines · Stable · empty-context checkedBT002S · is_gcd_euclid_forward
A relational gcd of divisor and remainder is a gcd of dividend and divisor.
layer 4 · 35 lines · Stable · empty-context checkedBT002U · gcd_exists_up_to
Bounded induction constructs a relational gcd whenever the right input is at most the bound.
layer 5 · 74 lines · Stable · empty-context checkedBT002V · gcd_exists_relational
Every pair of naturals has a relational greatest common divisor.
layer 6 · 11 lines · Stable · empty-context checkedBT002W · coprime_symm
Coprimality in its expanded common-divisor form is symmetric.
layer 0 · 10 lines · Stable · empty-context checkedBT002X · coprime_one_right
Every natural is coprime to one in the expanded common-divisor relation.
layer 3 · 7 lines · Stable · empty-context checkedBT002Y · coprime_one_left
One is coprime to every natural in the expanded common-divisor relation.
layer 3 · 7 lines · Stable · empty-context checkedBT0031 · is_gcd_one_to_coprime
A relational gcd witness one implies expanded coprimality.
layer 3 · 15 lines · Stable · empty-context checkedBT0032 · add_permute_outer
Permute the outer entries of two additive pairs.
layer 2 · 25 lines · Stable · empty-context checkedBT0033 · balanced_bezout_euclid_step
Transport balanced natural Bezout coefficients across one Euclidean division step.
layer 5 · 67 lines · Stable · empty-context checkedBT0034 · gcd_balanced_bezout_exists_up_to
Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.
layer 6 · 80 lines · Stable · empty-context checkedBT0035 · gcd_balanced_bezout_exists
Every pair has a relational gcd together with balanced natural Bezout witnesses.
layer 7 · 11 lines · Stable · empty-context checkedBT0036 · balanced_combination_scale_right
Scale a balanced natural combination on the right.
layer 5 · 56 lines · Stable · empty-context checkedBT0037 · common_divisor_divides_balanced_result
Every common divisor of two inputs divides the result of a balanced natural combination.
layer 3 · 48 lines · Stable · empty-context checkedBT0038 · coprime_balanced_bezout
Coprime inputs admit balanced natural Bezout coefficients with result one.
layer 8 · 24 lines · Stable · empty-context checkedBT0039 · gauss_coprime_cancel
Cancel a coprime factor from a divisibility witness (Gauss cancellation).
layer 9 · 30 lines · Stable · empty-context checkedBT003A · eq_decidable
Equality of natural numbers is constructively decidable.
layer 0 · 27 lines · Stable · empty-context checkedBT003B · multiple_decidable_nonzero
Divisibility by a nonzero natural is constructively decidable.
layer 5 · 40 lines · Stable · empty-context checkedBT003C · multiple_decidable
Divisibility of natural numbers is constructively decidable, including the zero divisor case.
layer 6 · 29 lines · Stable · empty-context checkedBT003D · factor_property_succ
Extend a bounded prime factor-pair property by checking the new boundary.
layer 2 · 27 lines · Stable · empty-context checkedBT003E · factor_search_up_to
Constructively decide whether a nonzero natural has a bounded nontrivial factor pair.
layer 6 · 101 lines · Stable · empty-context checkedBT003F · prime_or_composite
Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.
layer 7 · 38 lines · Stable · empty-context checkedBT003G · prime_nonzero
Every prime natural is nonzero.
layer 1 · 20 lines · Stable · empty-context checkedBT003H · prime_decidable
Primality of every natural number is constructively decidable.
layer 8 · 47 lines · Stable · empty-context checkedBT003J · proper_factor_lt
A factor with a nonunit cofactor is strictly smaller than a nonzero product.
layer 4 · 43 lines · Stable · empty-context checkedBT003K · prime_divisor_exists_up_to
Bounded strong induction constructs a prime divisor of every nonzero nonunit natural.
layer 8 · 71 lines · Stable · empty-context checkedBT003L · prime_divisor_exists
Every nonzero nonunit natural has a prime divisor.
layer 9 · 9 lines · Stable · empty-context checkedBT003M · prime_divisor_eq_one_or_self
Every divisor of a prime is one or the prime itself.
layer 2 · 19 lines · Stable · empty-context checkedBT003N · euclid_prime_dvd_product
A prime dividing a product divides at least one factor (Euclid's lemma).
layer 10 · 36 lines · Stable · empty-context checkedBT003O · mod_eq_refl
Balanced natural congruence is reflexive.
layer 0 · 5 lines · Stable · empty-context checkedBT003Q · mod_eq_trans
Balanced natural congruence is transitive.
layer 2 · 42 lines · Stable · empty-context checkedBT003R · mod_eq_add
Balanced natural congruence respects addition.
layer 3 · 42 lines · Stable · empty-context checkedBT003S · mod_eq_mul_right
Balanced congruence is preserved by multiplication on the right.
layer 5 · 26 lines · Stable · empty-context checkedBT003T · mod_eq_mul_left
Balanced congruence is preserved by multiplication on the left.
layer 6 · 25 lines · Stable · empty-context checkedBT003W · mod_eq_bounded_unique
Two balanced-congruent values below the same modulus are equal.
layer 5 · 28 lines · Stable · empty-context checkedBT003X · mod_eq_to_remainder_decomposition
A bounded balanced residue has a directed quotient/remainder witness.
layer 6 · 51 lines · Stable · empty-context checkedBT003Y · beta_modulus_nonzero
Every Gödel-beta decoding modulus is nonzero.
layer 1 · 4 lines · Stable · empty-context checkedBT0040 · beta_at_self_of_bound
A value below a Gödel-beta modulus decodes to itself when used as the code.
layer 1 · 12 lines · Stable · empty-context checkedBT0041 · beta_at_exists
Every Gödel-beta position has a bounded decoded residue.
layer 4 · 24 lines · Stable · empty-context checkedBT0042 · beta_at_unique
The decoded residue at a Gödel-beta position is unique.
layer 5 · 37 lines · Stable · empty-context checkedBT0045 · beta_at_of_mod_eq_bound
A bounded value congruent to a code is its expanded Gödel-beta value.
layer 7 · 17 lines · Stable · empty-context checkedBT0046 · dvd_to_mod_zero
A multiple is balanced-congruent to zero.
layer 1 · 8 lines · Stable · empty-context checkedBT004C · bezout_mod_left
A balanced Bezout identity selects the right coefficient modulo the left modulus.
layer 2 · 19 lines · Stable · empty-context checkedBT004D · bezout_mod_right
A balanced Bezout identity selects the left coefficient modulo the right modulus.
layer 1 · 13 lines · Stable · empty-context checkedBT004E · mod_eq_predecessor_cancel
The predecessor of a successor acts as minus one in balanced congruence.
layer 3 · 15 lines · Stable · empty-context checkedBT004F · binary_crt
Constructive binary CRT for positive coprime natural moduli using balanced congruence.
layer 9 · 276 lines · Stable · empty-context checkedBT004I · beta_modulus_coprime_base
Every beta-shaped successor modulus is coprime to its base c.
layer 4 · 20 lines · Stable · empty-context checkedBT004J · common_divisor_beta_moduli_divides_gap_times_c
A common divisor of two ordered beta moduli divides the index gap times c.
layer 5 · 27 lines · Stable · empty-context checkedBT004K · beta_moduli_coprime_of_gap_dvd
Beta moduli at an additive index gap dividing c are coprime.
layer 10 · 59 lines · Stable · empty-context checkedBT004M · bounded_common_multiple_step
Extend a nonzero common multiple through the next positive natural.
layer 4 · 52 lines · Stable · empty-context checkedBT004N · bounded_common_multiple_exists
Every finite initial interval has a nonzero common-multiple surrogate.
layer 5 · 29 lines · Stable · empty-context checkedBT004O · beta_moduli_coprime_of_lt_bounded_common_multiple
Ordered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.
layer 11 · 49 lines · Stable · empty-context checkedBT004P · beta_moduli_pairwise_coprime_bounded
Distinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.
layer 12 · 44 lines · Stable · empty-context checkedBT004R · coprime_mul_left
Coprimality with a fixed right operand is closed under multiplication on the left.
layer 10 · 34 lines · Stable · empty-context checkedBT004S · coprime_mul_right
Coprimality with a fixed left operand is closed under multiplication on the right.
layer 11 · 26 lines · Stable · empty-context checkedBT004T · mod_eq_of_mod_eq_multiple
Balanced congruence descends from a multiple modulus to every divisor modulus.
layer 3 · 23 lines · Stable · empty-context checkedBT004U · binary_crt_fold_step
One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.
layer 10 · 40 lines · Stable · empty-context checkedBT004V · right_factor_divides_product
The right factor divides a product.
layer 4 · 4 lines · Stable · empty-context checkedBT0053 · beta_value_le_code
Every decoded beta value is at most its code.
layer 0 · 10 lines · Stable · empty-context checkedBT0054 · base_le_beta_modulus
A beta base is at most every beta modulus over that base.
layer 3 · 13 lines · Stable · empty-context checkedBT0055 · le_scaled_nonzero
Scaling by a nonzero natural does not decrease a natural.
layer 6 · 16 lines · Stable · empty-context checkedBT0056 · scaled_bounded_common_multiple
A right multiple of a bounded common multiple remains such a common multiple.
layer 4 · 15 lines · Stable · empty-context checkedBT0057 · beta_value_lt_scaled_base
An old beta value fits every modulus after a constructive scaled-base rebase.
layer 7 · 54 lines · Stable · empty-context checkedBT0058 · new_value_lt_scaled_base
The appended value fits every modulus after the same constructive scaled-base rebase.
layer 7 · 36 lines · Stable · empty-context checkedBT0059 · beta_exclusive_accumulated_product_step
Extend the accumulated target-modulus product for an exclusive prefix.
layer 13 · 95 lines · Stable · empty-context checkedBT005A · beta_exclusive_recode_congruence_step
Add the next source value to a target-base CRT code for an exclusive prefix.
layer 11 · 92 lines · Stable · empty-context checkedBT005B · beta_exclusive_recode_invariant_step
Combine modulus-product and cross-base congruence updates for an exclusive prefix.
layer 14 · 49 lines · Stable · empty-context checkedBT005C · bounded_beta_exclusive_recode_invariant
Fold an empty-based, exclusive beta prefix into another base with append readiness.
layer 15 · 89 lines · Stable · empty-context checkedBT005D · beta_prefix_extend
Rebase an arbitrary decoded prefix and append one exact natural value.
layer 16 · 105 lines · Stable · empty-context checkedBT005E · beta_prefix_product_trace_exists
Every decoded beta factor prefix admits a beta-coded exact prefix-product trace.
layer 17 · 133 lines · Stable · empty-context checkedBT005F · beta_product_exists
Every finite decoded beta prefix has an exact relational product and a coded trace.
layer 18 · 25 lines · Stable · empty-context checkedBT005G · beta_product_functional
The fully expanded beta-coded Product relation is functional in its terminal product.
layer 6 · 153 lines · Stable · empty-context checkedBT005I · beta_product_zero
The product of an empty decoded prefix is one.
layer 6 · 16 lines · Stable · empty-context checkedBT005J · beta_product_succ_decompose
A successor product decomposes into its prefix product and final decoded factor.
layer 6 · 51 lines · Stable · empty-context checkedBT005K · beta_product_succ_append
Append one decoded factor to an existing fully expanded Product witness.
layer 17 · 101 lines · Stable · empty-context checkedBT005L · beta_product_transport_prefix
One-way extensional factor-prefix preservation transports Product without changing its trace.
layer 0 · 44 lines · Stable · empty-context checkedBT0069 · beta_factor_divides_product
Every decoded factor inside an exact beta Product divides its terminal product.
layer 7 · 82 lines · Stable · empty-context checkedBT006N · prime_three
Three is prime in the expanded first-order prime predicate.
layer 3 · 94 lines · Stable · empty-context checkedBT0072 · parity_cases
Every natural has a constructive even-or-odd witness.
layer 0 · 14 lines · Stable · empty-context checkedBT007U · beta_repeat_empty
Every constant beta prefix of length zero is vacuously Repeat.
layer 1 · 18 lines · Stable · empty-context checkedBT007V · beta_repeat_succ_extend
Recode a constant prefix and append one more copy of its value.
layer 17 · 40 lines · Stable · empty-context checkedBT007W · beta_repeat_exists
Every value and length admit a beta-coded constant prefix.
layer 18 · 20 lines · Stable · empty-context checkedBT007X · beta_repeat_entry_eq
Every decoded entry of a Repeat prefix equals its repeated value.
layer 6 · 21 lines · Stable · empty-context checkedBT007Y · beta_repeat_transport_entry
Repeat prefixes with one value preserve every decoded entry extensionally.
layer 7 · 28 lines · Stable · empty-context checkedBT0080 · pow_exists
Every base and exponent have a relational finite-product power.
layer 19 · 22 lines · Stable · empty-context checkedBT0081 · pow_zero
The relational zeroth power is one.
layer 7 · 17 lines · Stable · empty-context checkedBT0082 · pow_functional
Relational powers have a unique natural value.
layer 8 · 56 lines · Stable · empty-context checkedBT0083 · pow_successor_decompose
A successor relational power is its predecessor power times the base.
layer 7 · 54 lines · Stable · empty-context checkedBT0084 · beta_range_empty
Every consecutive beta range of length zero is vacuous.
layer 1 · 18 lines · Stable · empty-context checkedBT0085 · beta_range_succ_extend
Recode a consecutive prefix and append its next value.
layer 17 · 42 lines · Stable · empty-context checkedBT0086 · beta_range_exists
Every start and length admit a beta-coded consecutive range.
layer 18 · 20 lines · Stable · empty-context checkedBT0087 · beta_range_entry_eq
A decoded entry of a Range prefix is its start plus its index.
layer 6 · 21 lines · Stable · empty-context checkedBT0088 · beta_range_transport_entry
Two Range codes preserve every decoded entry extensionally.
layer 7 · 28 lines · Stable · empty-context checkedBT0089 · beta_prefix_sum_trace_exists
Every decoded beta prefix admits an exact beta-coded prefix-sum trace.
layer 17 · 136 lines · Stable · empty-context checkedBT008A · beta_sum_exists
Every decoded beta prefix has a relational finite sum.
layer 18 · 25 lines · Stable · empty-context checkedBT008B · beta_sum_trace_functional
Two exact prefix-sum traces over one decoded prefix have equal endpoints.
layer 6 · 153 lines · Stable · empty-context checkedBT008C · beta_sum_functional
The relational finite sum has a unique natural value.
layer 7 · 23 lines · Stable · empty-context checkedBT008E · beta_sum_zero
The sum of an empty decoded prefix is zero.
layer 6 · 16 lines · Stable · empty-context checkedBT008F · beta_sum_succ_decompose
A successor sum decomposes into its prefix sum and final summand.
layer 6 · 51 lines · Stable · empty-context checkedBT008J · all_bits_prefix_succ
Dropping the final entry preserves the all-bits invariant.
layer 2 · 15 lines · Stable · empty-context checkedBT008K · all_bits_last_succ
The final entry of a nonempty all-bits prefix is zero or one.
layer 2 · 11 lines · Stable · empty-context checkedBT008L · bit_count_exists
Every all-bits prefix has a relational count of its ones.
layer 19 · 12 lines · Stable · empty-context checkedBT008N · bit_count_zero
An empty bit prefix contains zero ones.
layer 7 · 15 lines · Stable · empty-context checkedBT008O · bit_count_succ_decompose
A successor count is its prefix count plus a final zero-or-one bit.
layer 7 · 63 lines · Stable · empty-context checkedBT008P · bit_count_bounded
A zero/one count never exceeds the length of its decoded prefix.
layer 8 · 58 lines · Stable · empty-context checkedBT008Q · prime_coprime_or_divides
A prime is constructively either coprime to a natural or divides it.
layer 7 · 30 lines · Stable · empty-context checkedBT008R · prime_not_divides_coprime
A prime not dividing a natural is coprime to that natural.
layer 8 · 14 lines · Stable · empty-context checkedBT008S · distinct_primes_coprime
Distinct primes are coprime in the expanded common-divisor relation.
layer 9 · 25 lines · Stable · empty-context checkedBT008Y · factorial_exists
Every natural has a beta-coded relational factorial value.
layer 19 · 21 lines · Stable · empty-context checkedBT0090 · factorial_functional
The beta-coded relational factorial has a unique value.
layer 8 · 55 lines · Stable · empty-context checkedBT0091 · factorial_zero
The relational factorial of zero is one.
layer 7 · 16 lines · Stable · empty-context checkedBT0092 · factorial_succ_decompose
A successor factorial is its predecessor factorial times the successor.
layer 7 · 60 lines · Stable · empty-context checkedBT0093 · pow_one_from_zero_successor
A successor of a zero exponent gives the relational first power.
layer 8 · 29 lines · Stable · empty-context checkedBT0094 · pow_one
The relational first power of a natural is the natural itself.
layer 9 · 13 lines · Stable · empty-context checkedBT0095 · pow_successor_pair_mul
A successor power paired with its predecessor equals predecessor times base.
layer 9 · 30 lines · Stable · empty-context checkedBT0097 · lt_three_cases
Every natural strictly below three is zero, one, or two.
layer 2 · 38 lines · Stable · empty-context checkedBT009V · pow_two_from_one_successor
A successor of exponent one gives the relational square.
layer 10 · 28 lines · Stable · empty-context checkedBT009W · pow_two
The relational second power is exactly the square.
layer 11 · 13 lines · Stable · empty-context checkedBT009X · pow_add
Relational powers turn addition of exponents into multiplication.
layer 9 · 90 lines · Stable · empty-context checkedBT00AA · finite_lt_succ_eq_or_lt
A value below a successor is the predecessor or lies below it.
layer 2 · 12 lines · Stable · empty-context checkedBT00AW · prime_is_succ_succ
Every prime natural is the second successor of a natural.
layer 2 · 29 lines · Stable · empty-context checkedBT00BG · coprime_product_is_lcm
The product of coprime naturals satisfies the universal relational LCM specification.
layer 10 · 40 lines · Stable · empty-context checkedBT00DH · beta_product_pointwise_coprime
A finite product of factors pointwise coprime to m is coprime to m.
layer 11 · 62 lines · Alpha body-checked · checked-use disabledBT00I9 · beta_sum_transport_prefix
Pointwise-equal decoded prefixes preserve an exact relational Sum.
layer 0 · 44 lines · Alpha body-checked · checked-use disabledBT00JA · eisenstein_initial_segment_prefix_all_bits
Every exact threshold prefix is an AllBits prefix.
layer 0 · 23 lines · Alpha body-checked · checked-use disabledBT00JB · eisenstein_initial_segment_decoded_choice
Every decoded bit recovers its exact threshold semantics.
layer 6 · 27 lines · Alpha body-checked · checked-use disabledBT00JC · beta_all_one_bit_count_exact
A length-k beta prefix consisting only of ones has BitCount k.
layer 8 · 62 lines · Alpha body-checked · checked-use disabledBT00JD · eisenstein_initial_segment_bit_count_functional
The BitCount of a bounded exact initial segment is its threshold.
layer 9 · 129 lines · Alpha body-checked · checked-use disabledBT00JE · eisenstein_initial_segment_bit_count_exact
A bounded exact initial-segment prefix has native BitCount q.
layer 20 · 33 lines · Alpha body-checked · checked-use disabledBT00K5 · beta_sum_pointwise_add
Pointwise sums of decoded entries induce exact addition of finite sums.
layer 7 · 127 lines · Alpha body-checked · checked-use disabledBT00MY · add_shuffle_middle
Four additive contributions can be regrouped by swapping the middle pair.
layer 3 · 13 lines · Alpha checked-use · empty-context checkedBT00PR · prime_strictly_above_decidable
Being prime and strictly above a fixed lower endpoint is decidable.
layer 9 · 38 lines · Alpha body-checked · checked-use disabledBT00PS · bounded_prime_interval_search
Bounded search returns a prime witness or an explicit prime-free interval certificate.
layer 10 · 68 lines · Alpha body-checked · checked-use disabledBT00PV · mul_le_mul
Multiplication is monotone in both natural-number arguments.
layer 6 · 24 lines · Alpha body-checked · checked-use disabledBT00PW · le_mul_of_one_le_right
A factor at least one makes right multiplication extensive.
layer 3 · 12 lines · Alpha body-checked · checked-use disabledBT00PX · le_mul_of_one_le_left
A factor at least one makes left multiplication extensive.
layer 6 · 12 lines · Alpha body-checked · checked-use disabledBT00PY · pow_base_monotone
Relational powers are monotone in the base at every exponent.
layer 8 · 68 lines · Alpha body-checked · checked-use disabledBT00Q0 · one_le_pow
Every relational power of a base at least one is at least one.
layer 8 · 46 lines · Alpha body-checked · checked-use disabledBT00Q1 · pow_nonzero_of_one_le
A relational power of a base at least one cannot be zero.
layer 9 · 17 lines · Alpha body-checked · checked-use disabledBT00Q3 · power_divides_decidable
Divisibility by a relational power is constructively decidable.
layer 20 · 33 lines · Alpha body-checked · checked-use disabledBT00Q4 · power_divides_zero
The zeroth relational power divides every natural.
layer 20 · 22 lines · Alpha body-checked · checked-use disabledBT00Q5 · bounded_power_valuation_search
Finite search either excludes every power divisor or returns a greatest exponent.
layer 21 · 122 lines · Alpha body-checked · checked-use disabledBT00Q6 · bounded_power_valuation_exists
Every explicit exponent bound has a greatest power-divisor exponent.
layer 22 · 24 lines · Alpha body-checked · checked-use disabledBT00Q7 · power_valuation_exists
The value itself supplies a canonical finite bound for power valuation.
layer 23 · 6 lines · Alpha body-checked · checked-use disabledBT00Q8 · power_valuation_functional
Canonical bounded power valuations have a unique exponent.
layer 4 · 25 lines · Alpha body-checked · checked-use disabledBT00Q9 · power_valuation_power_divides
A valuation exponent has a relational power dividing the value.
layer 0 · 7 lines · Alpha body-checked · checked-use disabledBT00QA · power_valuation_dominates
Every bounded power-divisor exponent lies below the valuation exponent.
layer 0 · 12 lines · Alpha body-checked · checked-use disabledBT00QD · prime_two_le
Every prime is at least two in witness-defined order.
layer 3 · 15 lines · Alpha body-checked · checked-use disabledBT00QE · succ_le_mul_of_two_le_right
Multiplying a nonzero natural by a factor at least two exceeds it.
layer 3 · 23 lines · Alpha body-checked · checked-use disabledBT00QF · prime_power_exponent_le
The exponent of a relational power at a prime base is bounded by its value.
layer 10 · 67 lines · Alpha body-checked · checked-use disabledBT00QG · prime_power_divides_exponent_le_value
A dividing prime power has exponent at most the nonzero dividend.
layer 11 · 27 lines · Alpha body-checked · checked-use disabledBT00QH · power_valuation_successor_not_divides
A canonical valuation at a prime cannot admit the next power divisor.
layer 12 · 30 lines · Alpha body-checked · checked-use disabledBT00QI · power_valuation_selected_and_successor_not_divides
Canonical prime valuations have the usual maximal-power characterization.
layer 13 · 21 lines · Alpha body-checked · checked-use disabledBT00QJ · mul_shuffle_four
Four factors may exchange their two middle entries.
layer 4 · 23 lines · Alpha body-checked · checked-use disabledBT00QK · power_divides_exponent_antitone
Divisibility by a higher relational power entails every lower exponent.
layer 20 · 51 lines · Alpha body-checked · checked-use disabledBT00QL · power_divides_add_mul
Multiplying power divisors adds their exponents.
layer 20 · 47 lines · Alpha body-checked · checked-use disabledBT00QM · power_divides_successor_of_cofactor
Divisibility of a power cofactor by its base raises the exponent by one.
layer 20 · 38 lines · Alpha body-checked · checked-use disabledBT00QN · prime_power_successor_cancel_cofactor
A successor power divisor cancels to a prime divisor of the exact cofactor.
layer 10 · 59 lines · Alpha body-checked · checked-use disabledBT00QO · prime_nondivisor_mul
A prime dividing neither factor does not divide their product.
layer 11 · 19 lines · Alpha body-checked · checked-use disabledBT00QP · power_valuation_exact_cofactor
A prime valuation extracts a nonzero cofactor not divisible by its prime.
layer 21 · 42 lines · Alpha body-checked · checked-use disabledBT00QQ · power_valuation_mul_successor_not_divides
The product of exact prime-power valuations has no next power divisor.
layer 22 · 87 lines · Alpha body-checked · checked-use disabledBT00QR · power_valuation_mul_lower
The valuation of a nonzero product is at least the sum of factor valuations.
layer 21 · 59 lines · Alpha body-checked · checked-use disabledBT00QS · power_valuation_mul_upper
The valuation of a nonzero product is at most the sum of factor valuations.
layer 23 · 45 lines · Alpha body-checked · checked-use disabledBT00QT · prime_power_valuation_mul
Prime-power valuation is additive on nonzero products.
layer 24 · 45 lines · Alpha body-checked · checked-use disabledBT00QU · two_mul_eq_add_self
Left multiplication by two is explicit doubling.
layer 4 · 7 lines · Alpha body-checked · checked-use disabledBT00QV · pow_mul_base
A relational power of a product is the product of the powers.
layer 8 · 110 lines · Alpha body-checked · checked-use disabledBT00QW · pow_two_base_two_value_four
The relational square of two has the concrete value four.
layer 12 · 12 lines · Alpha body-checked · checked-use disabledBT00R0 · ceil_div_six_shift
Ceiling by six commutes with adding an explicit multiple of six.
layer 2 · 39 lines · Alpha body-checked · checked-use disabledBT00R1 · ceil_div_six_total
Every natural has a constructive ceiling quotient by six.
layer 3 · 56 lines · Alpha body-checked · checked-use disabledBT00R2 · ceil_div_six_functional
The two witness inequalities determine a unique ceiling quotient.
layer 3 · 72 lines · Alpha body-checked · checked-use disabledBT00R4 · square_six_shift_identity
The six-step square increment is exactly six times 2*s+6.
layer 5 · 39 lines · Alpha body-checked · checked-use disabledBT00R5 · ceil_div_six_square_six_step
Ceil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.
layer 6 · 24 lines · Alpha body-checked · checked-use disabledBT00R6 · floor_sqrt_lower_bound
The floor-square graph projects its lower square bound.
layer 0 · 5 lines · Alpha body-checked · checked-use disabledBT00R7 · floor_sqrt_strict_upper_bound
The floor-square graph projects its strict successor-square bound.
layer 0 · 5 lines · Alpha body-checked · checked-use disabledBT00R9 · square_lt_successor_square
Every square is strictly below the next natural square.
layer 6 · 16 lines · Alpha body-checked · checked-use disabledBT00RA · floor_sqrt_total
Every natural lies in a constructively selected adjacent-square interval.
layer 7 · 32 lines · Alpha body-checked · checked-use disabledBT00RC · floor_sqrt_monotone
Witness order on inputs is transported monotonically to floor roots.
layer 6 · 46 lines · Alpha body-checked · checked-use disabledBT00RD · mul_le_cancel_left_nonzero
Witness order cancels a common nonzero left multiplier.
layer 4 · 29 lines · Alpha body-checked · checked-use disabledBT00RE · three_mul_eq_two_mul_add_self
Left multiplication by three is twice the input plus the input.
layer 4 · 7 lines · Alpha body-checked · checked-use disabledBT00RF · ceil_div_six_le_of_upper
Any six-multiple upper bound also bounds the ceiling quotient.
layer 3 · 40 lines · Alpha body-checked · checked-use disabledBT00RG · double_triple_remainder_complement_budget
The equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.
layer 6 · 94 lines · Alpha body-checked · checked-use disabledBT00RH · canonical_double_triple_remainder_complement_budget
Canonical remainder data yields and preserves the complement budget.
layer 7 · 16 lines · Alpha body-checked · checked-use disabledBT00RI · floor_ceil_complement_budget
Floor-square and ceiling budgets imply e<=c and q+e<=n.
layer 4 · 34 lines · Alpha body-checked · checked-use disabledBT00RJ · floor_ceil_division_budget
Raw canonical division data closes both B6 quotient-budget inequalities.
layer 8 · 34 lines · Alpha body-checked · checked-use disabledBT00RK · factorial_nonzero
A relational factorial value is never zero.
layer 8 · 47 lines · Alpha body-checked · checked-use disabledBT00RL · prime_power_valuation_one_zero
At a prime base, the bounded valuation of one has exponent zero.
layer 8 · 56 lines · Alpha body-checked · checked-use disabledBT00RM · factorial_valuation_exists
Every factorial has a canonical bounded valuation at every base.
layer 24 · 16 lines · Alpha body-checked · checked-use disabledBT00RO · prime_factorial_valuation_zero
The prime valuation of zero factorial is zero.
layer 9 · 21 lines · Alpha body-checked · checked-use disabledBT00RP · prime_factorial_valuation_succ
A successor factorial valuation is the sum of the predecessor and successor-factor valuations.
layer 25 · 70 lines · Alpha body-checked · checked-use disabledBT00S0 · prime_power_quotient_prefix_exists
Every prime-power quotient prefix has a finite beta code.
layer 20 · 109 lines · Alpha body-checked · checked-use disabledBT00S1 · power_quotient_prefix_transport
Equivalent power-quotient prefixes transport decoded quotients pointwise.
layer 9 · 72 lines · Alpha body-checked · checked-use disabledBT00S2 · prime_legendre_sum_exists
Every prime and natural input have a finite relational Legendre sum.
layer 21 · 23 lines · Alpha body-checked · checked-use disabledBT00S3 · legendre_sum_functional
The finite relational Legendre sum has a unique value.
layer 10 · 49 lines · Alpha body-checked · checked-use disabledBT00S4 · legendre_sum_zero
The finite Legendre sum at zero is zero.
layer 7 · 16 lines · Alpha body-checked · checked-use disabledBT00S5 · pow_successor_compose
A checked predecessor power composes with one multiplication step.
layer 20 · 29 lines · Alpha body-checked · checked-use disabledBT00SA · prime_power_quotient_tail_zero
The first omitted prime-power quotient is canonically zero.
layer 11 · 18 lines · Alpha body-checked · checked-use disabledBT00SB · prime_power_divides_exponent_le_valuation
Every dividing prime-power exponent lies below the valuation.
layer 12 · 24 lines · Alpha body-checked · checked-use disabledBT00SC · power_divides_of_exponent_le_valuation
Every exponent below a valuation exponent supplies a power divisor.
layer 21 · 19 lines · Alpha body-checked · checked-use disabledBT00SD · eisenstein_initial_segment_indicator_choice
Every position has a constructive exact threshold-indicator bit.
layer 1 · 15 lines · Alpha body-checked · checked-use disabledBT00SE · eisenstein_initial_segment_prefix_extend
Append one exact threshold bit while preserving the old prefix.
layer 17 · 46 lines · Alpha body-checked · checked-use disabledBT00SF · eisenstein_initial_segment_prefix_exists
Every threshold and finite length has an exact beta-coded indicator.
layer 18 · 33 lines · Alpha body-checked · checked-use disabledBT00SG · division_remainder_successor_cases
Successor division has exactly the carry and no-carry quotient cases.
layer 5 · 70 lines · Alpha body-checked · checked-use disabledBT00SH · division_successor_quotient_by_bit
A divisibility bit is exactly the successor quotient increment.
layer 6 · 99 lines · Alpha body-checked · checked-use disabledBT00SI · valuation_threshold_bit_decides_power_divides
A valuation threshold bit constructively decides the corresponding power divisor.
layer 22 · 41 lines · Alpha body-checked · checked-use disabledBT00SJ · power_quotient_prefix_decoded_divrem
A decoded quotient-prefix entry exposes its power and canonical division data.
layer 6 · 34 lines · Alpha body-checked · checked-use disabledBT00SK · power_quotient_successor_pointwise_add
Successor prime-power quotients are the old quotients plus their valuation-threshold bits.
layer 23 · 127 lines · Alpha body-checked · checked-use disabledBT00SL · pow_successor_compose_from_total
One shared power-totality premise constructs a successor power.
layer 10 · 30 lines · Alpha body-checked · checked-use disabledBT00SM · pow_mul_exp_from_total
Iterated powers multiply exponents using a supplied totality proof.
layer 10 · 95 lines · Alpha body-checked · checked-use disabledBT00SN · pow_exponent_monotone_from_total
Exponent monotonicity reuses one supplied power-totality proof.
layer 10 · 48 lines · Alpha body-checked · checked-use disabledBT00SO · pow_two_seed_bundle_from_total
One totality premise yields the exact seeds 2^2=4 and 2^7=128.
layer 13 · 266 lines · Alpha body-checked · checked-use disabledBT00SR · beta_sum_succ_last_zero
A successor beta sum with final entry zero is its predecessor sum.
layer 7 · 34 lines · Alpha body-checked · checked-use disabledBT00SS · prime_power_quotient_prefix_last_zero
The final entry of a length-(n+1) old quotient prefix is zero.
layer 12 · 42 lines · Alpha body-checked · checked-use disabledBT00ST · legendre_sum_zero_extended_prefix
An old Legendre sum has a successor-length quotient code ending in zero.
layer 21 · 65 lines · Alpha body-checked · checked-use disabledBT00SU · initial_segment_prefix_sum_exists
Every bounded threshold has a beta prefix whose exact sum is the threshold.
layer 21 · 23 lines · Alpha body-checked · checked-use disabledBT00SV · prime_legendre_sum_succ
Prime Legendre sums satisfy the exact constructive successor recurrence.
layer 24 · 66 lines · Alpha body-checked · checked-use disabledBT00SW · bertrand_h_six_step_transport_from_total
H(s) and J(s) together imply H(s+6).
layer 14 · 201 lines · Alpha body-checked · checked-use disabledBT00SX · bertrand_j_six_step_transport_from_total
J(s) implies J(s+6) through the shared 2^12 = 4^6 factor.
layer 14 · 113 lines · Alpha body-checked · checked-use disabledBT00SY · bertrand_hj_six_step_from_total
The paired H/J invariant advances by six under one PowTotal premise.
layer 15 · 64 lines · Alpha body-checked · checked-use disabledBT00T0 · factorial_legendre_successor_agreement
Factorial and Legendre successor recurrences preserve predecessor agreement.
layer 26 · 45 lines · Alpha body-checked · checked-use disabledBT00T1 · prime_factorial_valuation_eq_legendre_sum
At every prime, the factorial valuation exponent equals the finite Legendre sum.
layer 27 · 69 lines · Alpha body-checked · checked-use disabledBT00T2 · beta_pascal_zero_row_extend
Append the next fixed zero-row value while preserving all earlier cells.
layer 17 · 92 lines · Alpha body-checked · checked-use disabledBT00T3 · beta_pascal_zero_row_exists
Every finite width has a beta-coded Pascal zero row.
layer 18 · 26 lines · Alpha body-checked · checked-use disabledBT00T4 · beta_pascal_row_step_extend
Append one Pascal successor-row value and preserve the prefix.
layer 17 · 112 lines · Alpha body-checked · checked-use disabledBT00T5 · beta_pascal_row_step_exists
Every previous beta row has a finite Pascal successor row.
layer 18 · 30 lines · Alpha body-checked · checked-use disabledBT00T6 · beta_pascal_table_prefix_extend
Append one semantic Pascal row to both outer beta prefixes.
layer 19 · 261 lines · Alpha body-checked · checked-use disabledBT00T7 · beta_pascal_table_prefix_exists
Every finite width and height has a nested beta Pascal table.
layer 20 · 34 lines · Alpha body-checked · checked-use disabledBT00T8 · choose_exists
The recurrence-defined Choose relation has a value for every pair.
layer 21 · 53 lines · Alpha body-checked · checked-use disabledBT00T9 · beta_pascal_zero_row_pointwise_functional
Zero-row values agree pointwise across beta encodings and widths.
layer 6 · 93 lines · Alpha body-checked · checked-use disabledBT00TA · beta_pascal_row_step_pointwise_functional
Pascal successor rows preserve pointwise agreement across encodings.
layer 6 · 164 lines · Alpha body-checked · checked-use disabledBT00TB · beta_pascal_table_row_pointwise_functional
Corresponding decoded Pascal-table rows agree pointwise.
layer 7 · 313 lines · Alpha body-checked · checked-use disabledBT00TC · choose_functional
The recurrence-defined Choose relation is functional.
layer 8 · 92 lines · Alpha body-checked · checked-use disabledBT00TD · choose_out_of_range_zero
An out-of-range Choose value is zero.
layer 1 · 15 lines · Alpha body-checked · checked-use disabledBT00TE · choose_zero
The zeroth entry of every Pascal row is one.
layer 6 · 130 lines · Alpha body-checked · checked-use disabledBT00TF · beta_pascal_table_diagonal_boundary
Every decoded Pascal row has diagonal one and zeros above it.
layer 6 · 369 lines · Alpha body-checked · checked-use disabledBT00TG · choose_self
The recurrence-defined diagonal binomial coefficient is one.
layer 7 · 48 lines · Alpha body-checked · checked-use disabledBT00TH · beta_pascal_table_successor_cell_recurrence
A decoded successor table cell is the sum of predecessor cells.
layer 6 · 128 lines · Alpha body-checked · checked-use disabledBT00TI · choose_succ_succ_of_lt
Interior Choose values satisfy Pascal's successor recurrence.
layer 8 · 206 lines · Alpha body-checked · checked-use disabledBT00TJ · choose_succ_succ
Relational Choose values satisfy Pascal recurrence everywhere.
layer 9 · 94 lines · Alpha body-checked · checked-use disabledBT00TK · choose_self_of_eq
A column equal to its row has Choose value one.
layer 8 · 44 lines · Alpha body-checked · checked-use disabledBT00TL · choose_symmetry
Complementary columns have equal relational Choose values.
layer 22 · 178 lines · Alpha body-checked · checked-use disabledBT00TM · choose_positive
Every in-range relational Choose value is a successor.
layer 22 · 69 lines · Alpha body-checked · checked-use disabledBT00TN · central_binom_exists
Every row has a relational central-binomial value.
layer 22 · 4 lines · Alpha body-checked · checked-use disabledBT00TP · central_binom_positive
Every relational central-binomial value is a successor.
layer 23 · 10 lines · Alpha body-checked · checked-use disabledBT00TQ · central_binom_zero
The zeroth relational central-binomial value is one.
layer 7 · 6 lines · Alpha body-checked · checked-use disabledBT00TR · choose_upper_eq_transport
Choose is invariant under equality of its upper index.
layer 0 · 16 lines · Alpha body-checked · checked-use disabledBT00TS · central_binom_succ_double_middle
A successor central binomial is twice its odd-row middle value.
layer 23 · 55 lines · Alpha body-checked · checked-use disabledBT00TT · choose_weighted_vertical
Adjacent rows satisfy the constructive weighted vertical identity.
layer 22 · 285 lines · Alpha body-checked · checked-use disabledBT00TU · central_binom_succ_recurrence
Successive central binomials satisfy the weighted recurrence.
layer 24 · 36 lines · Alpha body-checked · checked-use disabledBT00TV · factorial_length_eq_transport
Relational factorial transports along equality of its length.
layer 0 · 10 lines · Alpha body-checked · checked-use disabledBT00TW · factorial_weighted_product_combine
Weighted factorial products combine by reassociation.
layer 4 · 29 lines · Alpha body-checked · checked-use disabledBT00TX · choose_factorial_bridge
Complementary factorials represent each constructive Choose value.
layer 23 · 182 lines · Alpha body-checked · checked-use disabledBT00TY · mul_lt_mul_right_nonzero
Right multiplication by a nonzero natural preserves strict order.
layer 6 · 34 lines · Alpha body-checked · checked-use disabledBT00U0 · four_power_central_recurrence_step
A weighted central recurrence equation advances the strict four-power lower bound.
layer 7 · 75 lines · Alpha body-checked · checked-use disabledBT00U1 · pow_four_four_exact
A relational fourth power of four is the fourfold product.
layer 12 · 22 lines · Alpha body-checked · checked-use disabledBT00U2 · central_binom_four_weighted_of_recurrence
The fourth central binomial satisfies the compact weighted value.
layer 8 · 67 lines · Alpha body-checked · checked-use disabledBT00U3 · four_pow_central_seed_package
The strict central-binomial lower bound holds at index four.
layer 23 · 35 lines · Alpha body-checked · checked-use disabledBT00U4 · four_pow_lt_mul_central_binom
For every index at least four, the fourth power is below the index-weighted central binomial.
layer 25 · 105 lines · Alpha body-checked · checked-use disabledBT00U5 · primorial_factor_choice_exists
Every index has its exact prime-or-one selector factor.
layer 9 · 13 lines · Alpha body-checked · checked-use disabledBT00U6 · primorial_factor_choice_functional
The prime-or-one selector factor at a fixed index is unique.
layer 0 · 28 lines · Alpha body-checked · checked-use disabledBT00U7 · primorial_factor_prefix_extend
Append one selector factor while preserving the previous prefix.
layer 17 · 42 lines · Alpha body-checked · checked-use disabledBT00U8 · primorial_factor_prefix_exists
Every finite length has a beta-coded selector prefix.
layer 18 · 20 lines · Alpha body-checked · checked-use disabledBT00UA · primorial_exists
Every natural index has a relational primorial value.
layer 19 · 14 lines · Alpha body-checked · checked-use disabledBT00UC · primorial_zero
The empty dense selector product is one.
layer 7 · 7 lines · Alpha body-checked · checked-use disabledBT00UD · primorial_succ_decompose
A successor primorial splits into its previous value and selector.
layer 7 · 40 lines · Alpha body-checked · checked-use disabledBT00UE · primorial_positive
Every relational primorial value is a successor.
layer 8 · 42 lines · Alpha body-checked · checked-use disabledBT00UF · primorial_index_eq_transport
Equal indices transport the expanded Primorial relation.
layer 0 · 10 lines · Alpha body-checked · checked-use disabledBT00UQ · beta_product_prefix_suffix_split
Split a finite Product into an initial prefix and an aligned suffix.
layer 19 · 107 lines · Alpha body-checked · checked-use disabledBT00UR · primorial_interval_factor_prefix_extend
Append one offset selector while preserving the prior interval.
layer 17 · 43 lines · Alpha body-checked · checked-use disabledBT00US · primorial_interval_factor_prefix_exists
Every offset and length has a beta-coded selector interval.
layer 18 · 21 lines · Alpha body-checked · checked-use disabledBT00UW · primorial_interval_factor_prefix_shift
Align a full Primorial mask with an independent offset interval.
layer 6 · 48 lines · Alpha body-checked · checked-use disabledBT00UX · primorial_factor_prefix_restrict_add
Restrict a selector prefix of length a+l to its first a entries.
layer 3 · 16 lines · Alpha body-checked · checked-use disabledBT00UY · primorial_prefix_interval_split
Split Primorial(a+l) into its prefix and offset interval product.
layer 20 · 54 lines · Alpha body-checked · checked-use disabledBT00VA · factorial_prime_divides_of_le
Every prime at most n divides the relational factorial n!.
layer 8 · 44 lines · Alpha body-checked · checked-use disabledBT00VB · factorial_prime_le_of_divides
Every prime divisor of n! is at most n.
layer 11 · 64 lines · Alpha body-checked · checked-use disabledBT00VC · choose_prime_divides_between
A prime between both denominator indices and the row divides Choose.
layer 24 · 88 lines · Alpha body-checked · checked-use disabledBT00VD · beta_pairwise_coprime_product_divides_common_multiple
A pairwise-coprime product divides every common multiple of its factors.
layer 12 · 130 lines · Alpha body-checked · checked-use disabledBT00VE · primorial_interval_pairwise_coprime
Distinct positions in an interval decode coprime selector factors.
layer 10 · 114 lines · Alpha body-checked · checked-use disabledBT00VF · primorial_interval_divides_choose_between
A selector interval between both denominator indices divides Choose.
layer 25 · 88 lines · Alpha body-checked · checked-use disabledBT00VG · primorial_even_interval_divides_central
The selector interval (n,2n] divides the central coefficient.
layer 26 · 40 lines · Alpha body-checked · checked-use disabledBT00VH · primorial_odd_interval_divides_middle
The selector interval (n+1,2n+1] divides the odd middle coefficient.
layer 26 · 53 lines · Alpha body-checked · checked-use disabledBT00VI · primorial_even_interval_le_central
The even Primorial interval is bounded by the central coefficient.
layer 27 · 24 lines · Alpha body-checked · checked-use disabledBT00VJ · primorial_odd_interval_le_middle
The odd Primorial interval is bounded by the odd middle coefficient.
layer 27 · 29 lines · Alpha body-checked · checked-use disabledBT00VK · central_binom_strong_upper_step
The weighted recurrence preserves the strong factor-two bound.
layer 6 · 94 lines · Alpha body-checked · checked-use disabledBT00VL · central_binom_recurrence_double_bundle
The recurrence and functional double-middle law share support.
layer 24 · 62 lines · Alpha body-checked · checked-use disabledBT00VM · central_binom_strong_upper_of_laws
Recurrence and totality imply the positive-index strong bound.
layer 8 · 89 lines · Alpha body-checked · checked-use disabledBT00VN · central_binom_upper_support_package
The expensive recurrence, middle, and totality laws close once.
layer 25 · 3 lines · Alpha body-checked · checked-use disabledBT00VO · central_binom_strong_upper
Twice a positive-index central binomial is at most four-power.
layer 26 · 7 lines · Alpha body-checked · checked-use disabledBT00VP · central_binom_odd_middle_le_four_pow
The odd-row middle coefficient is at most four to the half-row.
layer 26 · 62 lines · Alpha body-checked · checked-use disabledBT00VQ · primorial_one
The inclusive Primorial at one is exactly one.
layer 8 · 27 lines · Alpha body-checked · checked-use disabledBT00VR · double_half_predecessor_data
An even successor has a nonzero half below its predecessor.
layer 5 · 19 lines · Alpha body-checked · checked-use disabledBT00VS · odd_positive_prefix_predecessor_bound
The positive prefix half of an odd successor is smaller.
layer 5 · 17 lines · Alpha body-checked · checked-use disabledBT00VT · central_binom_nonzero_strong_upper
The strong central bound extends to every nonzero index.
layer 27 · 20 lines · Alpha body-checked · checked-use disabledBT00VU · primorial_four_power_support_package
The large interval and coefficient laws close once.
layer 28 · 11 lines · Alpha body-checked · checked-use disabledBT00VV · primorial_le_four_pow_bounded
Every bounded Primorial is at most the matching fourth power.
layer 28 · 303 lines · Alpha body-checked · checked-use disabledBT00VW · primorial_le_four_pow
The inclusive Primorial is bounded by four to its index.
layer 29 · 17 lines · Alpha body-checked · checked-use disabledBT00VX · central_binom_prime_divisor_le_double
Every prime divisor of a central coefficient is at most 2*n.
layer 24 · 47 lines · Alpha body-checked · checked-use disabledBT00VY · no_bertrand_central_prime_divisor_le
A no-Bertrand certificate forces central prime divisors below n.
layer 25 · 35 lines · Alpha body-checked · checked-use disabledBT00W0 · power_valuation_nonzero_exponent_divides_base
A nonzero valuation exponent exposes the base as a divisor.
layer 21 · 34 lines · Alpha body-checked · checked-use disabledBT00W2 · no_bertrand_central_prime_divisor_ranges
Every central prime divisor lies in one of the three live ranges.
layer 26 · 63 lines · Alpha body-checked · checked-use disabledBT00W3 · pow_block_bound_from_total
A supplied power bound remains true after a common block multiplier.
layer 11 · 66 lines · Alpha body-checked · checked-use disabledBT00W4 · pow_three_five_le_pow_four_four_from_total
The concrete seed inequality 3^5 <= 4^4 in the relational graph.
layer 11 · 171 lines · Alpha body-checked · checked-use disabledBT00W5 · pow_eleven_two_le_pow_two_seven_from_total
The concrete seed inequality 11^2 <= 2^7 in the relational graph.
layer 14 · 121 lines · Alpha body-checked · checked-use disabledBT00W6 · pow_six_ten_le_pow_four_thirteen_from_total
The block seed 6^10 <= 4^13 used by the finite H window.
layer 14 · 136 lines · Alpha body-checked · checked-use disabledBT00W7 · linear_square_budget
A factorized linear budget lies below a square by an explicit gap.
layer 5 · 61 lines · Alpha body-checked · checked-use disabledBT00W8 · bertrand_scaled_budget_root_32
The factorized RFC-v1 H budget at root 32 lies below its square.
layer 6 · 60 lines · Alpha body-checked · checked-use disabledBT00W9 · bertrand_scaled_budget_root_33
The factorized RFC-v1 H budget at root 33 lies below its square.
layer 6 · 54 lines · Alpha body-checked · checked-use disabledBT00WA · bertrand_scaled_budget_root_34
The factorized RFC-v1 H budget at root 34 lies below its square.
layer 6 · 54 lines · Alpha body-checked · checked-use disabledBT00WB · bertrand_scaled_budget_root_35
The factorized RFC-v1 H budget at root 35 lies below its square.
layer 6 · 86 lines · Alpha body-checked · checked-use disabledBT00WC · bertrand_scaled_budget_root_36
The factorized RFC-v1 H budget at root 36 lies below its square.
layer 6 · 99 lines · Alpha body-checked · checked-use disabledBT00WD · bertrand_scaled_budget_root_37
The factorized RFC-v1 H budget at root 37 lies below its square.
layer 6 · 167 lines · Alpha body-checked · checked-use disabledBT00WE · ceil_div_six_budget_of_scaled_le
A scaled lower bound cancels against the lower half of CeilDivSix.
layer 5 · 20 lines · Alpha body-checked · checked-use disabledBT00WF · pow_six_six_le_pow_four_eight_from_total
The capacity-safe residual block 6^6 <= 4^8.
layer 14 · 164 lines · Alpha body-checked · checked-use disabledBT00WG · pow_six_four_le_pow_four_six_from_total
The capacity-safe residual block 6^4 <= 4^6.
layer 14 · 101 lines · Alpha body-checked · checked-use disabledBT00WH · pow_three_five_block_plus_one_le_pow_four_four_block_plus_one_from_total
The seed 3^5 <= 4^4 extends by blocks and one residual factor.
layer 12 · 110 lines · Alpha body-checked · checked-use disabledBT00WI · pow_two_double_eq_pow_four_from_total
An even power of two is the matching power of four.
layer 14 · 26 lines · Alpha body-checked · checked-use disabledBT00WJ · pow_two_successor_double_le_pow_four_successor_from_total
An odd power of two is bounded by the next power of four.
layer 15 · 88 lines · Alpha body-checked · checked-use disabledBT00WK · pow_eleven_double_block_le_pow_two_seven_block_from_total
The seed 11^2 <= 2^7 extends through a common block count.
layer 15 · 41 lines · Alpha body-checked · checked-use disabledBT00WL · pow_eleven_double_block_le_pow_four_even_from_total
An even 11-to-2 block exponent converts exactly to base four.
layer 16 · 37 lines · Alpha body-checked · checked-use disabledBT00WM · pow_eleven_double_block_le_pow_four_odd_from_total
An odd 11-to-2 block exponent converts to the next base-four power.
layer 16 · 41 lines · Alpha body-checked · checked-use disabledBT00WN · pow_six_ten_block_le_pow_four_thirteen_block_from_total
The seed 6^10 <= 4^13 extends through a common block count.
layer 15 · 41 lines · Alpha body-checked · checked-use disabledBT00WO · pow_thirty_six_double_block_eq_pow_six_four_block_from_total
A double block of base thirty six is a fourfold block of base six.
layer 12 · 47 lines · Alpha body-checked · checked-use disabledBT00WP · bertrand_h_root_32_from_total
The RFC-v1 H envelope at the fixed root 32.
layer 17 · 204 lines · Alpha body-checked · checked-use disabledBT00WQ · bertrand_h_root_33_from_total
The RFC-v1 H envelope at the fixed root 33.
layer 16 · 206 lines · Alpha body-checked · checked-use disabledBT00WR · bertrand_h_root_34_from_total
The RFC-v1 H envelope at the fixed root 34.
layer 16 · 148 lines · Alpha body-checked · checked-use disabledBT00WS · bertrand_h_root_35_from_total
The RFC-v1 H envelope at the fixed root 35.
layer 16 · 201 lines · Alpha body-checked · checked-use disabledBT00WT · bertrand_h_root_36_from_total
The RFC-v1 H envelope at the fixed root 36.
layer 17 · 244 lines · Alpha body-checked · checked-use disabledBT00WU · bertrand_h_root_37_from_total
The RFC-v1 H envelope at the fixed root 37.
layer 17 · 167 lines · Alpha body-checked · checked-use disabledBT00WV · bertrand_j_base_thirty_two_window_from_total
The RFC-v1 J envelope uniformly covers roots 32 through 37.
layer 17 · 166 lines · Alpha body-checked · checked-use disabledBT00WW · bertrand_hj_base_window_thirty_two_from_total
All six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.
layer 18 · 241 lines · Alpha body-checked · checked-use disabledBT00WX · scaled_factor_square_identity
A factorization of a transports its square without expanding either factor.
layer 3 · 6 lines · Alpha body-checked · checked-use disabledBT00WY · thirty_two_square_eq_twice_sixteen_times_thirty_two
The root-32 square identity carried by the shallow factorization 16*32.
layer 4 · 7 lines · Alpha body-checked · checked-use disabledBT00X0 · floor_sqrt_factorized_threshold_thirty_two
The factorized large-input threshold forces every selected root to be at least 32.
layer 7 · 27 lines · Alpha body-checked · checked-use disabledBT00X1 · six_block_window_decomposition_above_thirty_two
Every s>=32 is a six-step iterate of one base root in the exact window 32..37.
layer 3 · 57 lines · Alpha body-checked · checked-use disabledBT00X2 · bertrand_hj_six_block_iterate_from_total
The common H/J invariant iterates constructively over every six-step block.
layer 19 · 177 lines · Alpha body-checked · checked-use disabledBT00X3 · bertrand_hj_envelope_thirty_two
All roots s>=32 satisfy both H and J after discharging power totality once.
layer 20 · 68 lines · Alpha body-checked · checked-use disabledBT00X4 · bertrand_floor_power_product_le_h_from_total
The floor-root power product is bounded by the H envelope using one supplied power-totality premise.
layer 12 · 121 lines · Alpha body-checked · checked-use disabledBT00X5 · bertrand_four_power_product_le_of_sum_from_total
Fourth-power factors are bounded by the power at every larger exponent sum.
layer 11 · 51 lines · Alpha body-checked · checked-use disabledBT00X6 · bertrand_main_inequality_factorized_from_total
The factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.
layer 21 · 115 lines · Alpha body-checked · checked-use disabledBT00X7 · bertrand_main_inequality_factorized
The factorized B6 inequality discharges relational-power totality exactly once.
layer 22 · 34 lines · Alpha body-checked · checked-use disabledBT00X8 · bertrand_main_inequality_nat
The public B6 surface retains n+n and reaches the factorized internal theorem through five checked equality rewrites.
layer 23 · 35 lines · Alpha body-checked · checked-use disabledBT00X9 · beta_product_pointwise_le
Pointwise bounded decoded prefixes have ordered finite products.
layer 7 · 97 lines · Alpha body-checked · checked-use disabledBT00XA · beta_product_uniform_le_pow
A uniformly bounded finite product is at most the matching power.
layer 8 · 45 lines · Alpha body-checked · checked-use disabledBT00XB · add_lt_add
Strict inequalities add componentwise.
layer 4 · 37 lines · Alpha body-checked · checked-use disabledBT00XC · add_lt_cancel_left
A common left summand cancels from strict witness order.
layer 3 · 30 lines · Alpha body-checked · checked-use disabledBT00XF · division_zero_quotient_of_lt
A dividend below its divisor has quotient zero.
layer 5 · 26 lines · Alpha body-checked · checked-use disabledBT00XG · division_double_quotient_bit
Doubling a dividend changes its quotient by one binary carry.
layer 5 · 133 lines · Alpha body-checked · checked-use disabledBT00XJ · pow_le_pow_of_exponent_le
Relational powers are monotone in the exponent above base one.
layer 20 · 47 lines · Alpha body-checked · checked-use disabledBT00XK · pow_tail_strict_of_square
Every exponent-two-or-larger power lies above the square tail.
layer 21 · 27 lines · Alpha body-checked · checked-use disabledBT00XL · power_valuation_value_eq_transport
Power valuation transports along equality of its valued number.
layer 0 · 11 lines · Alpha body-checked · checked-use disabledBT00XM · central_binom_factorial_valuation_balance
The central valuation is the doubled-column factorial deficit.
layer 25 · 109 lines · Alpha body-checked · checked-use disabledBT00XN · central_binom_legendre_valuation_balance
Factorial Legendre equality exposes the central carry balance.
layer 28 · 60 lines · Alpha body-checked · checked-use disabledBT00XO · prime_power_quotient_zero_of_exponent_gt
A prime-power quotient vanishes once its exponent exceeds the dividend.
layer 11 · 31 lines · Alpha body-checked · checked-use disabledBT00XP · power_quotient_prefix_tail_entry_zero
Every decoded quotient entry at or beyond the dividend is zero.
layer 12 · 40 lines · Alpha body-checked · checked-use disabledBT00XQ · power_quotient_prefix_sum_extend_zero
Zero quotient tails preserve the finite Legendre sum.
layer 13 · 86 lines · Alpha body-checked · checked-use disabledBT00XR · legendre_sum_extended_prefix_exists
A Legendre sum admits an arbitrarily long zero-extended quotient code.
layer 21 · 40 lines · Alpha body-checked · checked-use disabledBT00XV · double_quotient_carry_choice
Each pair of doubled quotients has a constructive carry bit.
layer 9 · 72 lines · Alpha body-checked · checked-use disabledBT00XW · double_quotient_carry_prefix_extend
A carry prefix extends by one freshly decoded carry bit.
layer 17 · 71 lines · Alpha body-checked · checked-use disabledBT00XX · double_quotient_carry_prefix_exists
Doubled quotient prefixes admit a beta-coded carry prefix.
layer 18 · 73 lines · Alpha body-checked · checked-use disabledBT00XY · double_quotient_carry_prefix_all_bits
Every value in a carry prefix is zero or one.
layer 0 · 30 lines · Alpha body-checked · checked-use disabledBT00Y0 · double_quotient_carry_prefix_restrict
Dropping the final position preserves a carry prefix.
layer 2 · 16 lines · Alpha body-checked · checked-use disabledBT00Y1 · bit_count_positive_last_one
A positive bit count has a one at an index at least its count.
layer 9 · 69 lines · Alpha body-checked · checked-use disabledBT00Y2 · division_successor_quotient_divisor_le
A division with successor quotient bounds its divisor by the dividend.
layer 2 · 21 lines · Alpha body-checked · checked-use disabledBT00Y3 · beta_sum_double_carry_exact
The doubled quotient sum is twice the source sum plus its carries.
layer 8 · 174 lines · Alpha body-checked · checked-use disabledBT00Y4 · central_binom_carry_bit_count
The valuation exponent is exactly the number of doubled-quotient carries.
layer 29 · 116 lines · Alpha body-checked · checked-use disabledBT00Y5 · central_binom_prime_power_contribution_le_double
Every complete prime-power contribution is bounded by twice n.
layer 30 · 149 lines · Alpha body-checked · checked-use disabledBT00Y6 · central_binom_prime_square_tail_exponent_not_two_le
A prime square above twice n rules out valuation exponent two.
layer 31 · 56 lines · Alpha body-checked · checked-use disabledBT00Y7 · central_binom_prime_square_tail_valuation_le_one
Above the square tail, a central-binomial valuation is at most one.
layer 32 · 31 lines · Alpha body-checked · checked-use disabledBT00Y8 · division_quotient_one_of_bounds
Bounds between one and two divisors force quotient one.
layer 4 · 25 lines · Alpha body-checked · checked-use disabledBT00Y9 · division_quotient_two_of_bounds
Bounds between two and three divisors force quotient two.
layer 4 · 28 lines · Alpha body-checked · checked-use disabledBT00YA · prime_square_tail_of_two_three_range
The scaled two-thirds range places the prime square above 2*n.
layer 12 · 85 lines · Alpha body-checked · checked-use disabledBT00YB · division_first_two_of_two_three_range
The two-thirds range fixes the first quotients at one and two.
layer 5 · 67 lines · Alpha body-checked · checked-use disabledBT00YC · double_quotient_carry_prefix_entries_zero
Exact doubled quotients and a square tail force every carry to zero.
layer 22 · 189 lines · Alpha body-checked · checked-use disabledBT00YD · central_binom_prime_valuation_zero_of_exact_double_quotients
An all-zero carry prefix forces the exact central valuation to zero.
layer 30 · 89 lines · Alpha body-checked · checked-use disabledBT00YE · central_binom_prime_valuation_zero_two_thirds_range
Primes in the open two-thirds range contribute zero valuation.
layer 31 · 65 lines · Alpha body-checked · checked-use disabledBT00YF · division_three_scaled_upper_of_quotient_lt
A quotient below p places the dividend strictly below 3*p.
layer 3 · 46 lines · Alpha body-checked · checked-use disabledBT00YG · central_binom_prime_valuation_zero_above_third_quotient
Valuation vanishes above the floor of two-thirds and at most n.
layer 32 · 32 lines · Alpha body-checked · checked-use disabledBT00YH · floor_sqrt_above_root_power_two_strict
A prime above a floor root has square strictly above the value.
layer 12 · 43 lines · Alpha body-checked · checked-use disabledBT00YI · central_binom_prime_above_floor_sqrt_valuation_le_one
Above the floor root, a central prime valuation is at most one.
layer 33 · 52 lines · Alpha body-checked · checked-use disabledBT00YJ · no_bertrand_central_nonzero_valuation_live_ranges
Every nonzero central valuation lies in one of two live ranges.
layer 33 · 55 lines · Alpha body-checked · checked-use disabledBT00YK · no_bertrand_central_nonzero_valuation_factor_ranges
The middle live range has exact valuation exponent one.
layer 34 · 62 lines · Alpha body-checked · checked-use disabledBT00YL · no_bertrand_central_nonzero_contribution_factor_ranges
A nonzero contribution is small-bounded or one middle prime.
layer 35 · 74 lines · Alpha body-checked · checked-use disabledBT00YM · no_bertrand_central_prime_contribution_ranges
Every central prime contribution has one reviewed factor form.
layer 36 · 47 lines · Alpha body-checked · checked-use disabledBT00YN · prime_contribution_choice_exists
Every index has its complete prime-power contribution or one.
layer 24 · 27 lines · Alpha body-checked · checked-use disabledBT00YO · prime_contribution_choice_functional
The complete contribution at a fixed index is unique.
layer 9 · 48 lines · Alpha body-checked · checked-use disabledBT00YP · prime_contribution_prefix_extend
Append one contribution while preserving the old prefix.
layer 25 · 48 lines · Alpha body-checked · checked-use disabledBT00YQ · prime_contribution_prefix_exists
Every number and finite length has a contribution prefix.
layer 26 · 21 lines · Alpha body-checked · checked-use disabledBT00YS · prime_contribution_product_exists
Every number and finite length has a contribution Product.
layer 27 · 15 lines · Alpha body-checked · checked-use disabledBT00YU · coprime_power_right
A power preserves coprimality with a fixed left operand.
layer 12 · 38 lines · Alpha body-checked · checked-use disabledBT00YV · coprime_powers
Powers of coprime bases are coprime.
layer 13 · 55 lines · Alpha body-checked · checked-use disabledBT00YW · prime_contribution_prefix_pairwise_coprime
Distinct contribution positions decode pairwise-coprime values.
layer 14 · 79 lines · Alpha body-checked · checked-use disabledBT00YX · prime_contribution_factor_divides
Every complete contribution factor divides its source number.
layer 9 · 31 lines · Alpha body-checked · checked-use disabledBT00YY · prime_contribution_product_divides
Every finite complete-contribution Product divides its source.
layer 15 · 40 lines · Alpha body-checked · checked-use disabledBT0100 · prime_contribution_selected_entry
A selected prime position exposes its valuation power in the product.
layer 8 · 41 lines · Alpha body-checked · checked-use disabledBT0101 · prime_contribution_selected_successor_divides
A prime in the remaining cofactor raises a selected power.
layer 21 · 31 lines · Alpha body-checked · checked-use disabledBT0102 · prime_contribution_cofactor_prime_contradiction
A prime divisor of the remaining cofactor contradicts maximality.
layer 22 · 70 lines · Alpha body-checked · checked-use disabledBT0103 · prime_contribution_cofactor_eq_one
A supported contribution cofactor is the multiplicative unit.
layer 23 · 41 lines · Alpha body-checked · checked-use disabledBT0104 · prime_contribution_reverse_divides
A supported complete contribution product is a multiple of its source.
layer 24 · 31 lines · Alpha body-checked · checked-use disabledBT0105 · prime_contribution_product_eq
Every supported complete contribution product equals its source.
layer 25 · 19 lines · Alpha body-checked · checked-use disabledBT0106 · prime_contribution_complete_exists
Every nonzero source has an exact supported contribution product.
layer 28 · 21 lines · Alpha body-checked · checked-use disabledBT0107 · central_binom_prime_contribution_product_exists
A central coefficient is exactly its complete contribution product.
layer 29 · 32 lines · Alpha body-checked · checked-use disabledBT0108 · no_bertrand_central_contribution_choice_ranges
Each central contribution lies in a reviewed factor range.
layer 37 · 37 lines · Alpha body-checked · checked-use disabledBT010A · two_lt_double_lower_six
A natural above two has double at least three plus three.
layer 3 · 20 lines · Alpha body-checked · checked-use disabledBT010B · floor_sqrt_two_le_of_two_lt
The floor root of twice a natural above two is at least two.
layer 4 · 79 lines · Alpha body-checked · checked-use disabledBT010C · three_mul_le_square_of_three_le
Every natural at least three dominates three times itself by its square.
layer 6 · 7 lines · Alpha body-checked · checked-use disabledBT010D · floor_sqrt_three_mul_le_double
Three times the floor root lies below the doubled input.
layer 7 · 42 lines · Alpha body-checked · checked-use disabledBT010E · division_quotient_lower_of_scaled_le
A scaled lower bound forces the division quotient above its scale index.
layer 3 · 42 lines · Alpha body-checked · checked-use disabledBT010F · floor_sqrt_le_third_quotient
The floor root is at most the quotient of the doubled input by three.
layer 8 · 21 lines · Alpha body-checked · checked-use disabledBT010G · floor_sqrt_third_quotient_gap_exists
The floor-root cut has an exact additive gap to the third quotient.
layer 9 · 22 lines · Alpha body-checked · checked-use disabledBT010H · division_quotient_le_dividend
The quotient by three is bounded by its doubled dividend.
layer 7 · 26 lines · Alpha body-checked · checked-use disabledBT010I · third_quotient_double_gap_exists
The third quotient has an exact additive gap to the doubled input.
layer 8 · 16 lines · Alpha body-checked · checked-use disabledBT010J · floor_third_double_gap_package
Package the two exact additive gaps used by the three-range split.
layer 10 · 29 lines · Alpha body-checked · checked-use disabledBT010K · prime_contribution_interval_prefix_extend
Append one contribution choice to an offset interval prefix.
layer 25 · 51 lines · Alpha body-checked · checked-use disabledBT010L · prime_contribution_interval_prefix_exists
Every number, offset, and length has a contribution prefix.
layer 26 · 22 lines · Alpha body-checked · checked-use disabledBT010P · prime_contribution_interval_prefix_shift
Align a full contribution prefix with its independent suffix.
layer 10 · 53 lines · Alpha body-checked · checked-use disabledBT010Q · prime_contribution_prefix_restrict_add
Restrict a contribution prefix of length a+l to length a.
layer 3 · 17 lines · Alpha body-checked · checked-use disabledBT010R · prime_contribution_prefix_interval_split
Split a contribution Product into prefix and offset interval.
layer 27 · 56 lines · Alpha body-checked · checked-use disabledBT010S · prime_contribution_product_length_eq_transport
Transport only the length carrier of a contribution Product.
layer 0 · 11 lines · Alpha body-checked · checked-use disabledBT010U · beta_product_all_one_exact
A Product whose decoded factors are all one is exactly one.
layer 7 · 55 lines · Alpha body-checked · checked-use disabledBT010V · no_bertrand_small_contribution_choice_le_double
Every small-range contribution is bounded by the doubled row.
layer 38 · 67 lines · Alpha body-checked · checked-use disabledBT010W · no_bertrand_middle_contribution_choice_le_selector
Middle-range contributions are bounded by dense selector factors.
layer 38 · 64 lines · Alpha body-checked · checked-use disabledBT010X · no_bertrand_high_contribution_choice_eq_one
Every contribution above the third quotient is neutral.
layer 38 · 63 lines · Alpha body-checked · checked-use disabledBT010Y · no_bertrand_small_contribution_product_le_power
The small contribution Product is bounded by (2n)^s.
layer 39 · 64 lines · Alpha body-checked · checked-use disabledBT0110 · no_bertrand_middle_contribution_interval_le_primorial_interval
The middle contribution interval is bounded by its selector interval.
layer 39 · 110 lines · Alpha body-checked · checked-use disabledBT0111 · no_bertrand_middle_contribution_interval_le_four_pow
The middle contribution interval is bounded by four to q.
layer 40 · 96 lines · Alpha body-checked · checked-use disabledBT0112 · no_bertrand_high_contribution_interval_eq_one
The high contribution interval is the multiplicative unit.
layer 39 · 68 lines · Alpha body-checked · checked-use disabledBT0113 · central_binom_factorization_small
The complete central contribution Product has only two live ranges.
layer 40 · 87 lines · Alpha body-checked · checked-use disabledBT0114 · central_binom_le_of_no_bertrand_prime
No Bertrand prime forces the reviewed central-binomial upper bound.
layer 41 · 100 lines · Alpha body-checked · checked-use disabledBT0115 · bertrand_eventually_closed_upper
Every n at least 16*32 has a prime in the constructive open-closed Bertrand interval.
layer 42 · 139 lines · Alpha body-checked · checked-use disabledBT0116 · fixed_nontrivial_factor_not_prime
A displayed nontrivial factorization refutes primality.
layer 0 · 18 lines · Alpha body-checked · checked-use disabledBT0117 · factor_pair_has_small_member_below_square
A factor pair below (B+1)^2 has a member at most B.
layer 6 · 91 lines · Alpha body-checked · checked-use disabledBT0118 · nonprime_has_small_prime_divisor_below_square
Every composite below (B+1)^2 has a prime divisor at most B.
layer 10 · 106 lines · Alpha body-checked · checked-use disabledBT0119 · prime_of_no_small_prime_divisor_below_square
Trial division by primes through B certifies numbers below (B+1)^2.
layer 11 · 26 lines · Alpha body-checked · checked-use disabledBT011A · prime_le_twenty_two_cases
The only primes at most twenty-two are the eight displayed values.
layer 3 · 473 lines · Alpha body-checked · checked-use disabledBT011B · nonzero_remainder_not_multiple
A nonzero proper remainder refutes divisibility.
layer 4 · 32 lines · Alpha body-checked · checked-use disabledBT011C · scaled_remainder_lift
Scale a quotient-remainder equation and normalize its new tail.
layer 4 · 39 lines · Alpha body-checked · checked-use disabledBT011E · double_scaled_remainder_lift
Compose the two bounded scaling steps used by the 521 certificate.
layer 5 · 38 lines · Alpha body-checked · checked-use disabledBT011F · prime_five
A native checked trial-division certificate for 5.
layer 12 · 120 lines · Alpha body-checked · checked-use disabledBT011G · prime_seven
A native checked trial-division certificate for 7.
layer 12 · 120 lines · Alpha body-checked · checked-use disabledBT011H · prime_thirteen
A native checked trial-division certificate for 13.
layer 12 · 124 lines · Alpha body-checked · checked-use disabledBT011I · prime_twenty_three
A native checked trial-division certificate for 23.
layer 12 · 124 lines · Alpha body-checked · checked-use disabledBT011J · prime_forty_three
A native checked trial-division certificate for 43.
layer 12 · 128 lines · Alpha body-checked · checked-use disabledBT011K · prime_eighty_three
A native checked trial-division certificate for 83.
layer 12 · 215 lines · Alpha body-checked · checked-use disabledBT011L · prime_one_hundred_sixty_three
A native checked trial-division certificate for 163.
layer 12 · 224 lines · Alpha body-checked · checked-use disabledBT011M · prime_three_hundred_seventeen
A native checked trial-division certificate for 317.
layer 12 · 256 lines · Alpha body-checked · checked-use disabledBT011N · prime_five_hundred_twenty_one
A native checked trial-division certificate for 521.
layer 12 · 287 lines · Alpha body-checked · checked-use disabledBT011O · bertrand_add_swap_nested
Swap the first two addends under a fixed trailing addend.
layer 2 · 11 lines · Alpha body-checked · checked-use disabledBT011P · bertrand_add_six_permute
Normalize the six addends used by the 163-to-317 cover.
layer 3 · 49 lines · Alpha body-checked · checked-use disabledBT011Q · bertrand_covering_interval
One checked adjacent cover supplies a Bertrand witness.
layer 3 · 39 lines · Alpha body-checked · checked-use disabledBT011R · bertrand_cover_one_two
The checked finite cover inequality from 1 to 2.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011S · bertrand_cover_two_three
The checked finite cover inequality from 2 to 3.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011T · bertrand_cover_three_five
The checked finite cover inequality from 3 to 5.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011U · bertrand_cover_five_seven
The checked finite cover inequality from 5 to 7.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011V · bertrand_cover_seven_thirteen
The checked finite cover inequality from 7 to 13.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011W · bertrand_cover_thirteen_twenty_three
The checked finite cover inequality from 13 to 23.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011X · bertrand_cover_twenty_three_forty_three
The checked finite cover inequality from 23 to 43.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT011Y · bertrand_cover_forty_three_eighty_three
The checked finite cover inequality from 43 to 9 * 9 + 2.
layer 0 · 2 lines · Alpha body-checked · checked-use disabledBT0120 · bertrand_cover_eighty_three_one_hundred_sixty_three
The compact checked cover from 83 to 163.
layer 5 · 40 lines · Alpha body-checked · checked-use disabledBT0121 · bertrand_cover_one_hundred_sixty_three_three_hundred_seventeen
The compact checked cover from 163 to 317.
layer 5 · 67 lines · Alpha body-checked · checked-use disabledBT0122 · bertrand_cover_three_hundred_seventeen_five_hundred_twenty_one
The compact checked cover from 317 to 521.
layer 5 · 162 lines · Alpha body-checked · checked-use disabledBT0123 · bertrand_cutoff_lt_final_prime
The factorized production cutoff lies below the final prime.
layer 5 · 103 lines · Alpha body-checked · checked-use disabledBT0124 · bertrand_small_closed_upper
Every nonzero input below 16*32 has a closed Bertrand witness.
layer 13 · 179 lines · Alpha body-checked · checked-use disabledBT0125 · bertrand_closed_upper
Every nonzero natural has a prime in its open-closed Bertrand interval.
layer 43 · 12 lines · Alpha body-checked · checked-use disabledBT0126 · bertrand_upper_endpoint_factorization
The closed upper endpoint is composite whenever 1<n.
layer 5 · 33 lines · Alpha body-checked · checked-use disabledBT0127 · bertrand_strict
Every n greater than one has a prime strictly below n+n.
layer 44 · 39 lines · Alpha body-checked · checked-use disabled