Effective Chebyshev prime-count bounds — Exact Proof Explorer

Construct the zero/one primality indicator at each dense index.

The empty primality bit prefix is valid.

A primality mask restricts to its preceding prefix.

Every decoded mask entry has the exact primality indicator, independently of beta-code choice.

Append a genuinely decided prime bit while preserving the entire existing prefix.

HA induction constructs the complete finite primality mask at every natural bound.

A primality mask consists of actual zero/one entries.

Construct the exact prime count for every bound, including zero and one.

The exact prime count is at most the ambient finite interval length.

Every actual nonnegative summand is at most its actual finite sum.

The actual prime two makes every prime count at bound at least two positive.

An actual bit-weighted finite product has the corresponding upper bound by a power of its actual bit sum.

An actual bit-weighted finite product has the corresponding lower bound by a power of its actual bit sum.

Construct each exact cutoff entry by decidable order and beta decoding.

The empty cutoff prefix is valid for every source and threshold.

Restrict an actual cutoff table to its preceding prefix.

Every decoded cutoff entry obeys its actual below/above-threshold choice.

Append an actual cutoff choice, preserving every previously coded entry.

Construct the complete finite cutoff table by actual length induction.

The full bit count is at most the cutoff index plus the actual count above that index.

Actual powers of two dominate the successor of their exponent, by HA induction.

Weak order between actual powers of two reflects weak order of the exponents.

Strict order between actual powers of two reflects strict exponent order.

The actual fourth power-base value is the square of the actual binary power value.

For n at least four, the central binomial coefficient dominates the actual 2^n value.

Every actually decoded dense primorial factor has its exact prime-or-one choice.

Every dense primorial factor is at least one, including nonprime positions.

Every decoded prime contribution has its actual valuation and power witness, or is one at a nonprime index.

The actual central-binomial contribution product is bounded factorwise by 2n exactly at prime-mask positions.

Every prime strictly beyond the cutoff contributes at least the cutoff to the actual primorial product.

The actual central binomial coefficient is at most (2n)^pi(N) whenever 2n is at most N; all factors and prime counts are constructed.

The cutoff raised to the actual number of primes beyond it is bounded by the actual primorial.

A lower bound on a doubled input reflects to its actual binary quotient, including either remainder bit.

The successor of a binary-split exponent is at most twice the successor of its half.

For h at least two, twice its successor is at most three times h.

The established binary-length convention always has positive length, including zero input.

Expose the actual lower and upper binary powers for a nonzero input without changing the BitLen definition.

The power-of-two threshold at half the lower exponent has square at most N, while ell is at most both 2U and 3h.

Actual 4^n equals actual 2^(n+n), using only constructed powers and their checked product laws.

At a genuine binary-power cutoff U=2^h, h times the actual upper prime count is at most 2N.

The exact small-prime 2N and large-prime 6N budgets combine to the required 8N bound.

The exact effective Chebyshev upper bound pi(N)*BitLen(N) <= 8N, including every N at least two.

An actual binary-split integer is at most twice its half plus one.

For positive A, twice A plus one is at most three times A.

An actual binary split whose half is bounded by a positive A is bounded by 8A.

Central-binomial growth and actual prime contributions force floor(N/2) <= BitLen(N)*pi(N) whenever the half is at least four.

The required lower prime-count bound for all N at least eight, using the actual binary half and central coefficient.

The exact effective Chebyshev lower bound N <= 8*pi(N)*BitLen(N), including every N at least two.

Exact G027: for every N at least two and its actual prime count and binary length, N <= 8*pi(N)*BitLen(N) and pi(N)*BitLen(N) <= 8N.

The primality indicator is uniquely zero or one, without a classical principle.

Primality masks with different beta codes have equal entries at every actual shared index.

The exact prime count is independent of every mask and sum-trace encoding choice.

The exact prime count at zero is zero.

One contributes no prime: the exact prime count at one is zero.

Every bound has a genuinely constructed, uniquely determined exact prime count.