The finite next-bit prediction experiment

This module proves the exact finite identity behind Yao's next-bit argument. If replacing an independent candidate bit by its target raises test acceptance by gap, then the predictor that trusts the candidate exactly on accepting tests recovers the target with probability 1/2 + gap.

The theorem is stated over an arbitrary nonempty finite background space, so it can be instantiated with NW seeds and all random coordinates other than the predicted bit without committing to a particular coordinate codec.

theorem Complexity.NextBitPrediction.successProbability_eq_half_add_gap {background : Type u_1} [Fintype background] [Nonempty background] (target : background → Bool) (testAt : background → Bool → Bool) : successProbability target testAt = 1 / 2 + targetAcceptanceProbability target testAt - candidateAcceptanceProbability testAt

Exact Yao prediction identity: success is one half plus the acceptance gain from replacing the independent candidate by the target bit.