Bertrand’s postulate with defined notation

Zero is a left identity for addition; unlike PA3, this needs induction.

A successor can move through addition on the left.

Addition is commutative.

Addition is associative.

Zero annihilates multiplication on the left.

A successor can move through multiplication on the left.

Multiplication is commutative.

Multiplication distributes over addition on the right.

Multiplication is associative.

One is a left identity for multiplication.

One is a right identity for multiplication.

Multiplication distributes over addition on the left.

No successor is zero (the reusable PA1 lemma).

Successor is injective (the reusable PA2 lemma).

The defined order is reflexive; zero is its witness.

Order witnesses compose by addition, so the defined order is transitive.

Adding a positive successor cannot leave a natural number fixed.

A fixed-point equation remains fixed after dropping an additive prefix.

Opposing additive witnesses force equality.

The witness-defined order is antisymmetric.

Every pair of natural numbers is comparable in the defined order.

A sum equal to zero has zero as its right addend.

Zero products have a zero factor: the 23-entry core capstone.

Every natural is either zero or the successor of a natural.

Every nonzero natural has a predecessor.

Addition preserves equality in both arguments.

Multiplication preserves equality in both arguments.

A common right addend can be cancelled.

A common left addend can be cancelled.

Zero is below every natural number.

Every natural number is below its successor.

Only zero is less than or equal to zero.

Every nonzero natural is at least one.

A natural at least one is nonzero.

Adding on the left produces an explicit order witness.

Adding on the right produces an explicit order witness.

Adding the same right summand preserves the witness-defined order.

Adding the same left summand preserves the witness-defined order.

Successor preserves the witness-defined order.

Successor order reflects to the underlying naturals.

A weak inequality remains true after raising its upper bound by one.

A witnessed strict inequality entails the corresponding weak inequality.

No natural is strictly below itself, with strict order fully expanded.

A witnessed inequality is either equality or a witnessed strict inequality.

Strict order followed by weak order remains strict.

Weak order followed by strict order remains strict.

Strict order is transitive.

Any two naturals satisfy weak order in one direction or strict order in the other.

Two naturals are equal or strictly ordered in exactly one displayed direction.

A strict inequality excludes the reverse weak inequality.

A weak inequality excludes strict inequality in the reverse direction.

A strict upper bound prevents the lower term from containing that bound as an additive middle block.

Left multiplication preserves the witness-defined order.

Right multiplication preserves the witness-defined order.

Multiplication by a nonzero left factor strictly increases across a successor step.

Every dividend has a quotient and bounded remainder for a successor divisor.

Every positive divisor admits a quotient and a strictly bounded remainder.

A bounded remainder keeps its decomposition below the next divisor block.

A positive gap between quotients makes two bounded-remainder decompositions unequal.

Bounded quotient-remainder decompositions have unique quotients and remainders.

A quotient decomposition with zero remainder supplies a divisibility witness.

Every multiple of a nonzero divisor has a bounded zero-remainder decomposition.

A sum equal to zero has zero as its left addend.

A product is one only when both natural factors are one.

A product of two nonzero naturals is nonzero.

A nonzero common left factor can be cancelled.

Two naturals at least two cannot multiply to two.

Two is prime in the expanded first-order prime predicate.

Zero is a multiple of every natural number.

Every natural number is a multiple of one.

Every natural number is a multiple of itself.

A right multiple of a multiple remains a multiple.

A left multiple of a multiple remains a multiple.

The multiple relation is transitive.

A divisor of a nonzero natural is bounded by that natural.

Every natural divisor of one equals one.

Mutual divisibility is antisymmetric over natural numbers.

A common-factor difference is itself a multiple of that factor.

A common divisor of a dividend and divisor also divides the remainder.

A common divisor of a divisor and remainder divides their Euclidean linear step.

Every natural is the relational gcd of itself and zero.

A relational gcd of divisor and remainder is a gcd of dividend and divisor.

Bounded induction constructs a relational gcd whenever the right input is at most the bound.

Every pair of naturals has a relational greatest common divisor.

Coprimality in its expanded common-divisor form is symmetric.

Every natural is coprime to one in the expanded common-divisor relation.

One is coprime to every natural in the expanded common-divisor relation.

A relational gcd witness one implies expanded coprimality.

Permute the outer entries of two additive pairs.

Transport balanced natural Bezout coefficients across one Euclidean division step.

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

Every pair has a relational gcd together with balanced natural Bezout witnesses.

Scale a balanced natural combination on the right.

Every common divisor of two inputs divides the result of a balanced natural combination.

Coprime inputs admit balanced natural Bezout coefficients with result one.

Cancel a coprime factor from a divisibility witness (Gauss cancellation).

Equality of natural numbers is constructively decidable.

Divisibility by a nonzero natural is constructively decidable.

Divisibility of natural numbers is constructively decidable, including the zero divisor case.

Extend a bounded prime factor-pair property by checking the new boundary.

Constructively decide whether a nonzero natural has a bounded nontrivial factor pair.

Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.

Every prime natural is nonzero.

Primality of every natural number is constructively decidable.

A factor with a nonunit cofactor is strictly smaller than a nonzero product.

Bounded strong induction constructs a prime divisor of every nonzero nonunit natural.

Every nonzero nonunit natural has a prime divisor.

Every divisor of a prime is one or the prime itself.

A prime dividing a product divides at least one factor (Euclid's lemma).

Balanced natural congruence is reflexive.

Balanced natural congruence is transitive.

Balanced natural congruence respects addition.

Balanced congruence is preserved by multiplication on the right.

Balanced congruence is preserved by multiplication on the left.

Two balanced-congruent values below the same modulus are equal.

A bounded balanced residue has a directed quotient/remainder witness.

Every Gödel-beta decoding modulus is nonzero.

A value below a Gödel-beta modulus decodes to itself when used as the code.

Every Gödel-beta position has a bounded decoded residue.

The decoded residue at a Gödel-beta position is unique.

A bounded value congruent to a code is its expanded Gödel-beta value.

A multiple is balanced-congruent to zero.

A balanced Bezout identity selects the right coefficient modulo the left modulus.

A balanced Bezout identity selects the left coefficient modulo the right modulus.

The predecessor of a successor acts as minus one in balanced congruence.

Constructive binary CRT for positive coprime natural moduli using balanced congruence.

Every beta-shaped successor modulus is coprime to its base c.

A common divisor of two ordered beta moduli divides the index gap times c.

Beta moduli at an additive index gap dividing c are coprime.

Extend a nonzero common multiple through the next positive natural.

Every finite initial interval has a nonzero common-multiple surrogate.

Ordered bounded indices have coprime beta moduli when c is a common multiple of the bounded positive gaps.

Distinct indices in a bounded prefix have pairwise coprime beta moduli under a bounded common-multiple invariant.

Coprimality with a fixed right operand is closed under multiplication on the left.

Coprimality with a fixed left operand is closed under multiplication on the right.

Balanced congruence descends from a multiple modulus to every divisor modulus.

One binary CRT extension preserves every old congruence whose modulus divides the accumulated product.

The right factor divides a product.

Every decoded beta value is at most its code.

A beta base is at most every beta modulus over that base.

Scaling by a nonzero natural does not decrease a natural.

A right multiple of a bounded common multiple remains such a common multiple.

An old beta value fits every modulus after a constructive scaled-base rebase.

The appended value fits every modulus after the same constructive scaled-base rebase.

Extend the accumulated target-modulus product for an exclusive prefix.

Add the next source value to a target-base CRT code for an exclusive prefix.

Combine modulus-product and cross-base congruence updates for an exclusive prefix.

Fold an empty-based, exclusive beta prefix into another base with append readiness.

Rebase an arbitrary decoded prefix and append one exact natural value.

Every decoded beta factor prefix admits a beta-coded exact prefix-product trace.

Every finite decoded beta prefix has an exact relational product and a coded trace.

The fully expanded beta-coded Product relation is functional in its terminal product.

The product of an empty decoded prefix is one.

A successor product decomposes into its prefix product and final decoded factor.

Append one decoded factor to an existing fully expanded Product witness.

One-way extensional factor-prefix preservation transports Product without changing its trace.

Every decoded factor inside an exact beta Product divides its terminal product.

Three is prime in the expanded first-order prime predicate.

Every natural has a constructive even-or-odd witness.

Every constant beta prefix of length zero is vacuously Repeat.

Recode a constant prefix and append one more copy of its value.

Every value and length admit a beta-coded constant prefix.

Every decoded entry of a Repeat prefix equals its repeated value.

Repeat prefixes with one value preserve every decoded entry extensionally.

Every base and exponent have a relational finite-product power.

The relational zeroth power is one.

Relational powers have a unique natural value.

A successor relational power is its predecessor power times the base.

Every consecutive beta range of length zero is vacuous.

Recode a consecutive prefix and append its next value.

Every start and length admit a beta-coded consecutive range.

A decoded entry of a Range prefix is its start plus its index.

Two Range codes preserve every decoded entry extensionally.

Every decoded beta prefix admits an exact beta-coded prefix-sum trace.

Every decoded beta prefix has a relational finite sum.

Two exact prefix-sum traces over one decoded prefix have equal endpoints.

The relational finite sum has a unique natural value.

The sum of an empty decoded prefix is zero.

A successor sum decomposes into its prefix sum and final summand.

Dropping the final entry preserves the all-bits invariant.

The final entry of a nonempty all-bits prefix is zero or one.

Every all-bits prefix has a relational count of its ones.

An empty bit prefix contains zero ones.

A successor count is its prefix count plus a final zero-or-one bit.

A zero/one count never exceeds the length of its decoded prefix.

A prime is constructively either coprime to a natural or divides it.

A prime not dividing a natural is coprime to that natural.

Distinct primes are coprime in the expanded common-divisor relation.

Every natural has a beta-coded relational factorial value.

The beta-coded relational factorial has a unique value.

The relational factorial of zero is one.

A successor factorial is its predecessor factorial times the successor.

A successor of a zero exponent gives the relational first power.

The relational first power of a natural is the natural itself.

A successor power paired with its predecessor equals predecessor times base.

Every natural strictly below three is zero, one, or two.

A successor of exponent one gives the relational square.

The relational second power is exactly the square.

Relational powers turn addition of exponents into multiplication.

A value below a successor is the predecessor or lies below it.

Every prime natural is the second successor of a natural.

The product of coprime naturals satisfies the universal relational LCM specification.

A finite product of factors pointwise coprime to m is coprime to m.

Pointwise-equal decoded prefixes preserve an exact relational Sum.

Every exact threshold prefix is an AllBits prefix.

Every decoded bit recovers its exact threshold semantics.

A length-k beta prefix consisting only of ones has BitCount k.

The BitCount of a bounded exact initial segment is its threshold.

A bounded exact initial-segment prefix has native BitCount q.

Pointwise sums of decoded entries induce exact addition of finite sums.

Four additive contributions can be regrouped by swapping the middle pair.

Being prime and strictly above a fixed lower endpoint is decidable.

Bounded search returns a prime witness or an explicit prime-free interval certificate.

Multiplication is monotone in both natural-number arguments.

A factor at least one makes right multiplication extensive.

A factor at least one makes left multiplication extensive.

Relational powers are monotone in the base at every exponent.

Every relational power of a base at least one is at least one.

A relational power of a base at least one cannot be zero.

Divisibility by a relational power is constructively decidable.

The zeroth relational power divides every natural.

Finite search either excludes every power divisor or returns a greatest exponent.

Every explicit exponent bound has a greatest power-divisor exponent.

The value itself supplies a canonical finite bound for power valuation.

Canonical bounded power valuations have a unique exponent.

A valuation exponent has a relational power dividing the value.

Every bounded power-divisor exponent lies below the valuation exponent.

Every prime is at least two in witness-defined order.

Multiplying a nonzero natural by a factor at least two exceeds it.

The exponent of a relational power at a prime base is bounded by its value.

A dividing prime power has exponent at most the nonzero dividend.

A canonical valuation at a prime cannot admit the next power divisor.

Canonical prime valuations have the usual maximal-power characterization.

Four factors may exchange their two middle entries.

Divisibility by a higher relational power entails every lower exponent.

Multiplying power divisors adds their exponents.

Divisibility of a power cofactor by its base raises the exponent by one.

A successor power divisor cancels to a prime divisor of the exact cofactor.

A prime dividing neither factor does not divide their product.

A prime valuation extracts a nonzero cofactor not divisible by its prime.

The product of exact prime-power valuations has no next power divisor.

The valuation of a nonzero product is at least the sum of factor valuations.

The valuation of a nonzero product is at most the sum of factor valuations.

Prime-power valuation is additive on nonzero products.

Left multiplication by two is explicit doubling.

A relational power of a product is the product of the powers.

The relational square of two has the concrete value four.

Ceiling by six commutes with adding an explicit multiple of six.

Every natural has a constructive ceiling quotient by six.

The two witness inequalities determine a unique ceiling quotient.

The six-step square increment is exactly six times 2*s+6.

Ceil((s+6)^2/6) is exactly Ceil(s^2/6)+2*s+6.

The floor-square graph projects its lower square bound.

The floor-square graph projects its strict successor-square bound.

Every square is strictly below the next natural square.

Every natural lies in a constructively selected adjacent-square interval.

Witness order on inputs is transported monotonically to floor roots.

Witness order cancels a common nonzero left multiplier.

Left multiplication by three is twice the input plus the input.

Any six-multiple upper bound also bounds the ceiling quotient.

The equation 2*n=3*q+r constructively yields q+c=n and 2*n<=6*c.

Canonical remainder data yields and preserves the complement budget.

Floor-square and ceiling budgets imply e<=c and q+e<=n.

Raw canonical division data closes both B6 quotient-budget inequalities.

A relational factorial value is never zero.

At a prime base, the bounded valuation of one has exponent zero.

Every factorial has a canonical bounded valuation at every base.

The prime valuation of zero factorial is zero.

A successor factorial valuation is the sum of the predecessor and successor-factor valuations.

Every prime-power quotient prefix has a finite beta code.

Equivalent power-quotient prefixes transport decoded quotients pointwise.

Every prime and natural input have a finite relational Legendre sum.

The finite relational Legendre sum has a unique value.

The finite Legendre sum at zero is zero.

A checked predecessor power composes with one multiplication step.

The first omitted prime-power quotient is canonically zero.

Every dividing prime-power exponent lies below the valuation.

Every exponent below a valuation exponent supplies a power divisor.

Every position has a constructive exact threshold-indicator bit.

Append one exact threshold bit while preserving the old prefix.

Every threshold and finite length has an exact beta-coded indicator.

Successor division has exactly the carry and no-carry quotient cases.

A divisibility bit is exactly the successor quotient increment.

A valuation threshold bit constructively decides the corresponding power divisor.

A decoded quotient-prefix entry exposes its power and canonical division data.

Successor prime-power quotients are the old quotients plus their valuation-threshold bits.

One shared power-totality premise constructs a successor power.

Iterated powers multiply exponents using a supplied totality proof.

Exponent monotonicity reuses one supplied power-totality proof.

One totality premise yields the exact seeds 2^2=4 and 2^7=128.

A successor beta sum with final entry zero is its predecessor sum.

The final entry of a length-(n+1) old quotient prefix is zero.

An old Legendre sum has a successor-length quotient code ending in zero.

Every bounded threshold has a beta prefix whose exact sum is the threshold.

Prime Legendre sums satisfy the exact constructive successor recurrence.

H(s) and J(s) together imply H(s+6).

J(s) implies J(s+6) through the shared 2^12 = 4^6 factor.

The paired H/J invariant advances by six under one PowTotal premise.

Factorial and Legendre successor recurrences preserve predecessor agreement.

At every prime, the factorial valuation exponent equals the finite Legendre sum.

Append the next fixed zero-row value while preserving all earlier cells.

Every finite width has a beta-coded Pascal zero row.

Append one Pascal successor-row value and preserve the prefix.

Every previous beta row has a finite Pascal successor row.

Append one semantic Pascal row to both outer beta prefixes.

Every finite width and height has a nested beta Pascal table.

The recurrence-defined Choose relation has a value for every pair.

Zero-row values agree pointwise across beta encodings and widths.

Pascal successor rows preserve pointwise agreement across encodings.

Corresponding decoded Pascal-table rows agree pointwise.

The recurrence-defined Choose relation is functional.

An out-of-range Choose value is zero.

The zeroth entry of every Pascal row is one.

Every decoded Pascal row has diagonal one and zeros above it.

The recurrence-defined diagonal binomial coefficient is one.

A decoded successor table cell is the sum of predecessor cells.

Interior Choose values satisfy Pascal's successor recurrence.

Relational Choose values satisfy Pascal recurrence everywhere.

A column equal to its row has Choose value one.

Complementary columns have equal relational Choose values.

Every in-range relational Choose value is a successor.

Every row has a relational central-binomial value.

Every relational central-binomial value is a successor.

The zeroth relational central-binomial value is one.

Choose is invariant under equality of its upper index.

A successor central binomial is twice its odd-row middle value.

Adjacent rows satisfy the constructive weighted vertical identity.

Successive central binomials satisfy the weighted recurrence.

Relational factorial transports along equality of its length.

Weighted factorial products combine by reassociation.

Complementary factorials represent each constructive Choose value.

Right multiplication by a nonzero natural preserves strict order.

A weighted central recurrence equation advances the strict four-power lower bound.

A relational fourth power of four is the fourfold product.

The fourth central binomial satisfies the compact weighted value.

The strict central-binomial lower bound holds at index four.

For every index at least four, the fourth power is below the index-weighted central binomial.

Every index has its exact prime-or-one selector factor.

The prime-or-one selector factor at a fixed index is unique.

Append one selector factor while preserving the previous prefix.

Every finite length has a beta-coded selector prefix.

Every natural index has a relational primorial value.

The empty dense selector product is one.

A successor primorial splits into its previous value and selector.

Every relational primorial value is a successor.

Equal indices transport the expanded Primorial relation.

Split a finite Product into an initial prefix and an aligned suffix.

Append one offset selector while preserving the prior interval.

Every offset and length has a beta-coded selector interval.

Align a full Primorial mask with an independent offset interval.

Restrict a selector prefix of length a+l to its first a entries.

Split Primorial(a+l) into its prefix and offset interval product.

Every prime at most n divides the relational factorial n!.

Every prime divisor of n! is at most n.

A prime between both denominator indices and the row divides Choose.

A pairwise-coprime product divides every common multiple of its factors.

Distinct positions in an interval decode coprime selector factors.

A selector interval between both denominator indices divides Choose.

The selector interval (n,2n] divides the central coefficient.

The selector interval (n+1,2n+1] divides the odd middle coefficient.

The even Primorial interval is bounded by the central coefficient.

The odd Primorial interval is bounded by the odd middle coefficient.

The weighted recurrence preserves the strong factor-two bound.

The recurrence and functional double-middle law share support.

Recurrence and totality imply the positive-index strong bound.

The expensive recurrence, middle, and totality laws close once.

Twice a positive-index central binomial is at most four-power.

The odd-row middle coefficient is at most four to the half-row.

The inclusive Primorial at one is exactly one.

An even successor has a nonzero half below its predecessor.

The positive prefix half of an odd successor is smaller.

The strong central bound extends to every nonzero index.

The large interval and coefficient laws close once.

Every bounded Primorial is at most the matching fourth power.

The inclusive Primorial is bounded by four to its index.

Every prime divisor of a central coefficient is at most 2*n.

A no-Bertrand certificate forces central prime divisors below n.

A nonzero valuation exponent exposes the base as a divisor.

Every central prime divisor lies in one of the three live ranges.

A supplied power bound remains true after a common block multiplier.

The concrete seed inequality 3^5 <= 4^4 in the relational graph.

The concrete seed inequality 11^2 <= 2^7 in the relational graph.

The block seed 6^10 <= 4^13 used by the finite H window.

A factorized linear budget lies below a square by an explicit gap.

The factorized RFC-v1 H budget at root 32 lies below its square.

The factorized RFC-v1 H budget at root 33 lies below its square.

The factorized RFC-v1 H budget at root 34 lies below its square.

The factorized RFC-v1 H budget at root 35 lies below its square.

The factorized RFC-v1 H budget at root 36 lies below its square.

The factorized RFC-v1 H budget at root 37 lies below its square.

A scaled lower bound cancels against the lower half of CeilDivSix.

The capacity-safe residual block 6^6 <= 4^8.

The capacity-safe residual block 6^4 <= 4^6.

The seed 3^5 <= 4^4 extends by blocks and one residual factor.

An even power of two is the matching power of four.

An odd power of two is bounded by the next power of four.

The seed 11^2 <= 2^7 extends through a common block count.

An even 11-to-2 block exponent converts exactly to base four.

An odd 11-to-2 block exponent converts to the next base-four power.

The seed 6^10 <= 4^13 extends through a common block count.

A double block of base thirty six is a fourfold block of base six.

The RFC-v1 H envelope at the fixed root 32.

The RFC-v1 H envelope at the fixed root 33.

The RFC-v1 H envelope at the fixed root 34.

The RFC-v1 H envelope at the fixed root 35.

The RFC-v1 H envelope at the fixed root 36.

The RFC-v1 H envelope at the fixed root 37.

The RFC-v1 J envelope uniformly covers roots 32 through 37.

All six roots 32 through 37 satisfy both RFC-v1 H/J base bounds.

A factorization of a transports its square without expanding either factor.

The root-32 square identity carried by the shallow factorization 16*32.

The factorized large-input threshold forces every selected root to be at least 32.

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

The common H/J invariant iterates constructively over every six-step block.

All roots s>=32 satisfy both H and J after discharging power totality once.

The floor-root power product is bounded by the H envelope using one supplied power-totality premise.

Fourth-power factors are bounded by the power at every larger exponent sum.

The factorized threshold and all-root envelope imply the B6 power-product inequality under one supplied power-totality premise.

The factorized B6 inequality discharges relational-power totality exactly once.

The public B6 surface retains n+n and reaches the factorized internal theorem through five checked equality rewrites.

Pointwise bounded decoded prefixes have ordered finite products.

A uniformly bounded finite product is at most the matching power.

Strict inequalities add componentwise.

A common left summand cancels from strict witness order.

A dividend below its divisor has quotient zero.

Doubling a dividend changes its quotient by one binary carry.

Relational powers are monotone in the exponent above base one.

Every exponent-two-or-larger power lies above the square tail.

Power valuation transports along equality of its valued number.

The central valuation is the doubled-column factorial deficit.

Factorial Legendre equality exposes the central carry balance.

A prime-power quotient vanishes once its exponent exceeds the dividend.

Every decoded quotient entry at or beyond the dividend is zero.

Zero quotient tails preserve the finite Legendre sum.

A Legendre sum admits an arbitrarily long zero-extended quotient code.

Each pair of doubled quotients has a constructive carry bit.

A carry prefix extends by one freshly decoded carry bit.

Doubled quotient prefixes admit a beta-coded carry prefix.

Every value in a carry prefix is zero or one.

Dropping the final position preserves a carry prefix.

A positive bit count has a one at an index at least its count.

A division with successor quotient bounds its divisor by the dividend.

The doubled quotient sum is twice the source sum plus its carries.

The valuation exponent is exactly the number of doubled-quotient carries.

Every complete prime-power contribution is bounded by twice n.

A prime square above twice n rules out valuation exponent two.

Above the square tail, a central-binomial valuation is at most one.

Bounds between one and two divisors force quotient one.

Bounds between two and three divisors force quotient two.

The scaled two-thirds range places the prime square above 2*n.

The two-thirds range fixes the first quotients at one and two.

Exact doubled quotients and a square tail force every carry to zero.

An all-zero carry prefix forces the exact central valuation to zero.

Primes in the open two-thirds range contribute zero valuation.

A quotient below p places the dividend strictly below 3*p.

Valuation vanishes above the floor of two-thirds and at most n.

A prime above a floor root has square strictly above the value.

Above the floor root, a central prime valuation is at most one.

Every nonzero central valuation lies in one of two live ranges.

The middle live range has exact valuation exponent one.

A nonzero contribution is small-bounded or one middle prime.

Every central prime contribution has one reviewed factor form.

Every index has its complete prime-power contribution or one.

The complete contribution at a fixed index is unique.

Append one contribution while preserving the old prefix.

Every number and finite length has a contribution prefix.

Every number and finite length has a contribution Product.

A power preserves coprimality with a fixed left operand.

Powers of coprime bases are coprime.

Distinct contribution positions decode pairwise-coprime values.

Every complete contribution factor divides its source number.

Every finite complete-contribution Product divides its source.

A selected prime position exposes its valuation power in the product.

A prime in the remaining cofactor raises a selected power.

A prime divisor of the remaining cofactor contradicts maximality.

A supported contribution cofactor is the multiplicative unit.

A supported complete contribution product is a multiple of its source.

Every supported complete contribution product equals its source.

Every nonzero source has an exact supported contribution product.

A central coefficient is exactly its complete contribution product.

Each central contribution lies in a reviewed factor range.

A natural above two has double at least three plus three.

The floor root of twice a natural above two is at least two.

Every natural at least three dominates three times itself by its square.

Three times the floor root lies below the doubled input.

A scaled lower bound forces the division quotient above its scale index.

The floor root is at most the quotient of the doubled input by three.

The floor-root cut has an exact additive gap to the third quotient.

The quotient by three is bounded by its doubled dividend.

The third quotient has an exact additive gap to the doubled input.

Package the two exact additive gaps used by the three-range split.

Append one contribution choice to an offset interval prefix.

Every number, offset, and length has a contribution prefix.

Align a full contribution prefix with its independent suffix.

Restrict a contribution prefix of length a+l to length a.

Split a contribution Product into prefix and offset interval.

Transport only the length carrier of a contribution Product.

A Product whose decoded factors are all one is exactly one.

Every small-range contribution is bounded by the doubled row.

Middle-range contributions are bounded by dense selector factors.

Every contribution above the third quotient is neutral.

The small contribution Product is bounded by (2n)^s.

The middle contribution interval is bounded by its selector interval.

The middle contribution interval is bounded by four to q.

The high contribution interval is the multiplicative unit.

The complete central contribution Product has only two live ranges.

No Bertrand prime forces the reviewed central-binomial upper bound.

Every n at least 16*32 has a prime in the constructive open-closed Bertrand interval.

A displayed nontrivial factorization refutes primality.

A factor pair below (B+1)^2 has a member at most B.

Every composite below (B+1)^2 has a prime divisor at most B.

Trial division by primes through B certifies numbers below (B+1)^2.

The only primes at most twenty-two are the eight displayed values.

A nonzero proper remainder refutes divisibility.

Scale a quotient-remainder equation and normalize its new tail.

Compose the two bounded scaling steps used by the 521 certificate.

A native checked trial-division certificate for 5.

A native checked trial-division certificate for 7.

A native checked trial-division certificate for 13.

A native checked trial-division certificate for 23.

A native checked trial-division certificate for 43.

A native checked trial-division certificate for 83.

A native checked trial-division certificate for 163.

A native checked trial-division certificate for 317.

A native checked trial-division certificate for 521.

Swap the first two addends under a fixed trailing addend.

Normalize the six addends used by the 163-to-317 cover.

One checked adjacent cover supplies a Bertrand witness.

The checked finite cover inequality from 1 to 2.

The checked finite cover inequality from 2 to 3.

The checked finite cover inequality from 3 to 5.

The checked finite cover inequality from 5 to 7.

The checked finite cover inequality from 7 to 13.

The checked finite cover inequality from 13 to 23.

The checked finite cover inequality from 23 to 43.

The checked finite cover inequality from 43 to 9 * 9 + 2.

The compact checked cover from 83 to 163.

The compact checked cover from 163 to 317.

The compact checked cover from 317 to 521.

The factorized production cutoff lies below the final prime.

Every nonzero input below 16*32 has a closed Bertrand witness.

Every nonzero natural has a prime in its open-closed Bertrand interval.

The closed upper endpoint is composite whenever 1<n.

Every n greater than one has a prime strictly below n+n.