Strict Growth of the Optimal Real-law Slope

Abstract

The minimum ratio of dyadic sampling cost to least atom mass grows strictly with the label count.

Simplex(m,p) means that p is a real vector indexed by Fin m with sum one; PositiveLaw adds strict positivity of every coordinate. PositiveSimplex(m) is the set of vectors satisfying PositiveLaw(m,p). LeastIndex(p,k) means p(k) is at most every coordinate. R(p,d) is 2^d minus the sum of the integer floors of 2^d p(i), and L(p) is the sum of R(p,d)/2^d over all natural depths. These definitions include terminating binary coordinates and all real probability laws.

Definition 1.1 (The full real-law slope).

$$\forall m:\mathbb{N},\mathrm{alpha}\left(m\right)=\mathrm{sInf}\left(\left\{y\in \mathbb{R}\mid \exists p:(\mathrm{Fin}\left(m\right)\to \mathbb{R}),\exists k:\mathrm{Fin}\left(m\right),\mathrm{PositiveLaw}\left(m,p\right)\wedge \mathrm{LeastIndex}\left(p,k\right)\wedge y=\frac{L\left(p\right)}{p\left(k\right)}\right\}\right)$$

Formalization. D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha (✓ std3).

Source. Repository-derived.

Commentary.

For m >= 2, alpha(m) is the infimum of L(p)/p(k) over every strictly positive real law p on Fin m whose coordinates sum to one, with k an index of a smallest coordinate. No rationality, computability, or finite-depth restriction is imposed. The same definition applies to the single-label endpoint.

Theorem 1.2 (Normalized floor tails).

$$\forall m,p,\mathrm{Simplex}\left(m,p\right)\to ((\forall d,0\le R\left(p,d\right)\le m)\wedge \mathrm{Summable}\left(d\mapsto \frac{R\left(p,d\right)}{2^d}\right)\wedge 0\le L\left(p\right))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.law_data (✓ std3). ∎

Source. Repository-derived.

Commentary.

The floor inequalities bound each residual between zero and the number of coordinates. Geometric domination makes the tail series summable and its sum nonnegative.

Theorem 1.3 (The first charged bit).

$$\forall m,p,(2\le m\wedge \mathrm{PositiveLaw}\left(m,p\right))\to 1\le L\left(p\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.cost_ge_one (✓ std3). ∎

Source. Repository-derived.

Commentary.

With at least two positive coordinates, every coordinate is below one. All depth-zero floors vanish, so the depth-zero contribution is one.

Theorem 1.4 (Every law bounds the infimum).

$$\forall m,p,k,(\mathrm{PositiveLaw}\left(m,p\right)\wedge \mathrm{LeastIndex}\left(p,k\right))\to \mathrm{alpha}\left(m\right)\le \frac{L\left(p\right)}{p\left(k\right)}$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha_le (✓ std3). ∎

Source. Repository-derived.

Commentary.

All admissible ratios are nonnegative. The infimum is therefore at most the ratio of any particular positive normalized law.

Theorem 1.5 (A lower bound from the least mass).

$$\forall m,(2\le m)\to m\le \mathrm{alpha}\left(m\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha_ge_labels (✓ std3). ∎

Source. Repository-derived.

Commentary.

The least coordinate is at most 1/m and the cost is at least one. Every admissible ratio, and hence its infimum, is at least m.

Theorem 1.6 (Lower semicontinuity on the positive simplex).

$$\forall m,k,\mathrm{LowerSemicontinuousOn}\left(p\mapsto \frac{L\left(p\right)}{p\left(k\right)},\mathrm{PositiveSimplex}\left(m\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.ratio_lower_semicontinuous (✓ std3). ∎

Source. Repository-derived.

Commentary.

At a fixed law, finitely many floors cannot increase in a sufficiently small neighborhood. Every finite tail prefix supplies a local lower bound. Convergence of the nonnegative series and continuity of the positive denominator pass this bound to the full ratio.

Theorem 1.7 (Attainment in the full real domain).

$$\forall m,(2\le m)\to \exists p,k,\mathrm{PositiveLaw}\left(m,p\right)\wedge \mathrm{LeastIndex}\left(p,k\right)\wedge \frac{L\left(p\right)}{p\left(k\right)}=\mathrm{alpha}\left(m\right)$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.attained (✓ std3). ∎

Source. Repository-derived.

Commentary.

The uniform law supplies a finite comparison ratio. Since every multi-label law costs at least one, any smaller ratio has its least coordinate bounded away from zero. After relabeling this coordinate to a fixed index, optimization takes place on a nonempty compact subset of the real simplex. Lower semicontinuity supplies a minimum there, and laws outside it have larger ratio.

Theorem 1.8 (Strict growth with the number of labels).

$$\mathrm{alpha}\left(1\right)=0\wedge \mathrm{alpha}\left(2\right)=2\wedge (\forall m:\mathbb{N},(3\le m)\to \mathrm{alpha}\left((m-1)\right)<\mathrm{alpha}\left(m\right))$$

Proof. Machine-checked in Lean as D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Jeremie Lumbroso (2013). Optimal Discrete Uniform Generation from Coin Flips, and Applications. URL: https://arxiv.org/abs/1304.1916v1.

Commentary.

For a strictly positive normalized real law p on m labels, the dyadic cost is the sum over depths d of the unassigned floor remainder divided by 2^d. The function alpha is the infimum of this cost divided by the smallest mass. The domain contains all such real laws, without a rationality or finite-depth restriction.

The endpoint values and the nonincrease of cost under merging are standard consequences of the classical Knuth-Yao DDG cost expression recalled by Lumbroso, Section 2.1. A single label has zero cost. For two labels, the cost is at least one and the smallest mass is at most one half. The uniform two-label law has cost one and attains ratio two. Merging two atoms never increases any floor remainder, by the superadditivity of the integer floor.

For strict growth, take an attaining law with at least three labels. If the smallest atom is unique, merging it with another atom strictly raises the new minimum mass. If two atoms have the same smallest mass, their first positive binary digit produces a strict carry one depth earlier, so merging them strictly reduces the convergent cost sum. In each case the new law has a strictly smaller ratio, proving the strict inequality for consecutive label counts.

References

• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha_ge_labels
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.alpha_le
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.attained
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.cost_ge_one
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.law_data
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.ratio_lower_semicontinuous
• Truth anchor: D5/S3/Arith/FibonacciAtomic/OptimalLawStrictSlope.result
• Dependency: D5/S3/Arith/FibonacciAtomic/DyadicSupportLines