Countable-allocation and log-log guardrails

This file isolates the elementary obstruction behind confidence allocation over a countable sequence of geometric epochs. If nonnegative weights have total mass at most one, then every integer block [N, 2N] contains an atom with weight at most 1 / (N + 1). For positive weights, the corresponding logarithmic selection cost is at least log (N + 1).

When epoch k is associated with geometric scale 4^(k+1), the same statement forces a log log-sized atom cost along an unbounded subsequence, up to an explicit additive constant. This is a method-specific obstruction for countable confidence allocation or union-bound stitching. It is not a minimax lower bound for confidence sequences and does not assert a universal law-of-the-iterated-logarithm lower bound.

The final section gives a concrete receipt: telescoping polynomial weights 1 / ((k+1)(k+2)) sum to one, while geometric epoch scales turn their exact selection cost into an explicit iterated-log expression.

Mathematical sources: the pigeonhole principle, summability of nonnegative series, and the standard weighted Bonferroni/Kraft allocation principle.

Blockwise obstruction for arbitrary countable allocations

theorem FormalSLT.AnytimeValid.AllocationLogLog.exists_small_weight_on_dyadicBlock (weight : ℕ → ℝ) (hweight_nonneg : ∀ (k : ℕ), 0 ≤ weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) (N : ℕ) : ∃ k ∈ Finset.Icc N (2 * N), weight k ≤ 1 / (↑N + 1)

Every block [N, 2N] of a nonnegative countable allocation contains an atom no larger than the reciprocal block cardinality. The interval is inclusive and has exactly N + 1 elements.

theorem FormalSLT.AnytimeValid.AllocationLogLog.exists_logCost_ge_log_blockCard (weight : ℕ → ℝ) (hweight_pos : ∀ (k : ℕ), 0 < weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) (N : ℕ) : ∃ k ∈ Finset.Icc N (2 * N), Real.log (↑N + 1) ≤ Real.log (1 / weight k)

Positive countable allocations must pay at least log (N+1) somewhere in every inclusive block [N, 2N].

theorem FormalSLT.AnytimeValid.AllocationLogLog.exists_logCost_ge_indexLog_sub_log_two (weight : ℕ → ℝ) (hweight_pos : ∀ (k : ℕ), 0 < weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) (N : ℕ) : ∃ k ∈ Finset.Icc N (2 * N), Real.log (↑k + 1) - Real.log 2 ≤ Real.log (1 / weight k)

A block witness can be expressed directly in terms of its selected index: the log cost is at least log (k+1) - log 2.

theorem FormalSLT.AnytimeValid.AllocationLogLog.frequently_logCost_ge_indexLog_sub_log_two (weight : ℕ → ℝ) (hweight_pos : ∀ (k : ℕ), 0 < weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) : ∃ᶠ (k : ℕ) in Filter.atTop, Real.log (↑k + 1) - Real.log 2 ≤ Real.log (1 / weight k)

The index-scale lower bound occurs frequently at infinity. This is the filter-level form of the unbounded-subsequence statement.

Translation to geometric epochs

def FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochTime (k : ℕ) : ℕ

Integer sample-size scale associated with geometric epoch k.

Equations

• FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochTime k = 4 ^ (k + 1)

def FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochScale (k : ℕ) : ℝ

Real coercion of the geometric epoch time, used inside logarithms.

Equations

• FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochScale k = ↑(FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochTime k)

noncomputable def FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochIteratedLog (k : ℕ) : ℝ

Iterated natural logarithm of the geometric epoch scale.

Equations

• FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochIteratedLog k = Real.log (Real.log (FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochScale k))

theorem FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochTime_natLog (k : ℕ) : Nat.log 4 (geometricEpochTime k) = k + 1

The base-four logarithm recovers the epoch index exactly.

theorem FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochScale_log (k : ℕ) : Real.log (geometricEpochScale k) = (↑k + 1) * Real.log 4

theorem FormalSLT.AnytimeValid.AllocationLogLog.geometricEpochIteratedLog_eq (k : ℕ) : geometricEpochIteratedLog k = Real.log (↑k + 1) + Real.log (Real.log 4)

Exact conversion from geometric epoch index to iterated logarithm.

theorem FormalSLT.AnytimeValid.AllocationLogLog.exists_geometricEpoch_loglogCost (weight : ℕ → ℝ) (hweight_pos : ∀ (k : ℕ), 0 < weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) (N : ℕ) : ∃ k ∈ Finset.Icc N (2 * N), geometricEpochIteratedLog k - (Real.log 2 + Real.log (Real.log 4)) ≤ Real.log (1 / weight k)

Allocation-based log-log obstruction. For every block of geometric epochs, one selected atom pays at least the iterated logarithm of its epoch scale, up to the displayed universal additive constant.

theorem FormalSLT.AnytimeValid.AllocationLogLog.frequently_geometricEpoch_loglogCost (weight : ℕ → ℝ) (hweight_pos : ∀ (k : ℕ), 0 < weight k) (hweight_summable : Summable weight) (hweight_total : ∑' (k : ℕ), weight k ≤ 1) : ∃ᶠ (k : ℕ) in Filter.atTop, geometricEpochIteratedLog k - (Real.log 2 + Real.log (Real.log 4)) ≤ Real.log (1 / weight k)

The geometric-epoch log-log obstruction holds along an unbounded subsequence.

Polynomial weights on geometric epochs

noncomputable def FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight (k : ℕ) : ℝ

Telescoping polynomial confidence allocation.

Equations

• FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight k = 1 / ((↑k + 1) * (↑k + 2))

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_pos (k : ℕ) : 0 < polynomialEpochWeight k

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_eq_sub (k : ℕ) : polynomialEpochWeight k = 1 / (↑k + 1) - 1 / (↑k + 2)

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_sum_range (K : ℕ) : ∑ k ∈ Finset.range K, polynomialEpochWeight k = 1 - 1 / (↑K + 1)

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_hasSum : HasSum polynomialEpochWeight 1

The polynomial confidence allocation has total mass exactly one.

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_summable : Summable polynomialEpochWeight

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_tsum : ∑' (k : ℕ), polynomialEpochWeight k = 1

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialEpochWeight_log_cost (k : ℕ) : Real.log (1 / polynomialEpochWeight k) = Real.log (↑k + 1) + Real.log (↑k + 2)

Exact log selection price of the polynomial allocation.

theorem FormalSLT.AnytimeValid.AllocationLogLog.polynomialGeometricEpoch_log_cost (k : ℕ) : Real.log (1 / polynomialEpochWeight k) = geometricEpochIteratedLog k - Real.log (Real.log 4) + Real.log (↑k + 2)

Exact polynomial-weight/geometric-epoch receipt.