A Lean formalization of Bayesian bandit value interpolation

This technical note and reproducible Lean packet formalize Bayesian bandit value interpolation from Seungki Min, Costis Maglaras and Ciamac C. Moallemi, Thompson Sampling with Information Relaxation Penalties, arXiv:1902.04251v2, Appendix D.3.2. In the exact independent-arm Bayesian model with measurable conjugate updates and integrable predictive rewards, the values Ukn decrease at every observation step, and the WFH/WVZ endpoints and adjacent-arm identities hold, including horizon zero. The finite-history posterior under the actual product outcome law is proved, not assumed. The contribution is a complete formalization of established mathematics. It includes a posterior-kernel induction, conditioning on other arms, conditional-mean and integrability arguments, finite-allocation Jensen bounds and endpoint identities. The formalized cumulative quantity S sums posterior predictive means, not observed rewards. Other information-relaxation mission milestones are outside the scope of this exact theorem. The archive preserves the exact accepted proof, public platform definition, independently repeated complete-type audit, pinned Lean 4.33.1 and Mathlib 0df444a360eaa60ab8c11dca51a86af692955474, fresh source reproduction and a false-conclusion control rejected as expected. The only axioms are propext, Classical.choice and Quot.sound. Pinned dependency caches remain trusted inputs; this is not a bootstrap verification. Original mathematics belongs to Min, Maglaras and Moallemi. mikedeng1 supplied the platform model and prior indexing clarification; Shuze Chen reviewed the statement. Prior accepted queelius Jensen proofs and Mathlib contributors are specifically credited, including Rémy Degenne, Etienne Marion and Lorenzo Luccioli. Alexander Richard Towell directed the work. Substantial OpenAI Codex assistance in formalization, verification and publication preparation is disclosed. No mathematical novelty, source-author endorsement or independent human peer review is claimed. The proof and curated source were publicly disclosed on 20 October 2026; their exact timestamps and URLs are preserved separately from this archive publication. The owning research repository remains private. This deposit covers one coherent contribution, not the entire Prove2Me campaign.