Small Prime Channel Optimality

Abstract

The first m primes maximize information among m complete equal-cost channels.

Theorem 1.1 (The first m prime channels maximize total information).

$$\begin{array}{c}\forall s\in (1,\infty ),H:(1,\infty )\to \mathrm{Primes}\to \mathbb{R},\\ m\in \mathbb{N},c:\mathrm{OrderEmbedding}(\mathrm{Fin}(m),\mathbb{N}),\\ (\forall p,r\in \mathrm{Primes},p<r\Rightarrow H(s,r)<H(s,p))\wedge (\forall i\in \mathrm{Fin}(m),\mathrm{Prime}(c(i)))\Rightarrow \\ \sum _{i\in \mathrm{Fin}(m)}H(s,c(i))\le \sum _{i\in \mathrm{Fin}(m)}H(s,\mathrm{prime}(i)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ArithmeticTomography/SmallPrimeChannelOptimality.small_prime_channel_optimality (✓ std3). ∎

Source. Repository-derived.

Commentary.

The parameter s is publicly restricted to the open interval above one. The function H assigns expected information to every complete prime channel at each such parameter, and the displayed premise states its strict decrease as the prime grows.

An order embedding c from Fin(m) into the natural numbers represents an increasing choice of exactly m distinct channels. The public primality premise ensures that every selected index is a prime; the shared cardinality is the equal-cost budget constraint.

The canonical increasing enumeration of the prime subtype is pointwise no larger than any such ordered choice. Strict decrease of H turns that comparison around, and summing the pointwise inequalities proves the displayed maximum.

References

• Truth anchor: D5/S3/Observer/ArithmeticTomography/SmallPrimeChannelOptimality.small_prime_channel_optimality