BanditRLProof.OFULScheduledPowerOfTwoForcedIndexCount

A horizon-independent forcing predicate for successor indices one below powers of two. The `Nat.log2` equality makes the predicate decidable without a classical search over exponents.

def isPowerOfTwoForcedIndex (n : Nat) : Prop

The computable predicate has the intended existential power-of-two semantics.

theorem isPowerOfTwoForcedIndex_iff {n : Nat} : isPowerOfTwoForcedIndex n <-> exists k, n + 1 = 2 ^ k

Power-of-two forced successor indices strictly below `horizon`.

def powerOfTwoForcedIndexSet (horizon : Nat) : Finset Nat

Membership combines the prefix bound with the intended power-of-two equation.

theorem mem_powerOfTwoForcedIndexSet_iff {horizon n : Nat} : n ∈ powerOfTwoForcedIndexSet horizon <-> n < horizon ∧ exists k, n + 1 = 2 ^ k

No declaration docstring is present; use the chapter context and exact statement below.

theorem powerOfTwoForcedIndexSet_zero : powerOfTwoForcedIndexSet 0 = ∅

Index zero is forced exactly in nonempty horizon prefixes.

theorem zero_mem_powerOfTwoForcedIndexSet_iff {horizon : Nat} : 0 ∈ powerOfTwoForcedIndexSet horizon <-> 0 < horizon

There are at most `Nat.log2 horizon + 1` power-of-two forced indices below a horizon. Each member embeds into the image of the admissible exponent range.

theorem card_powerOfTwoForcedIndexSet_le_log2_add_one (horizon : Nat) : (powerOfTwoForcedIndexSet horizon).card <= Nat.log2 horizon + 1