Add exact Lemma 2.1 monotonicity audit

Add expanded five-claim execution and proof audit

At-scale PAC reproduction of linear-contract sample complexity (Thm 1.1/Cor 1.2, Lemmas 2.1/2.2) — 5 claims

Reproduce linear-contract sample complexity: uniform conv O(1/sqrt s) slope -0.488, EUM eps-optimal, action-independent, reward monotone, O(1/nu^2) cover