Under AD and DC every real set is Lebesgue measurable

Fix $E\subseteq \mathcal{C}$. If its closed inner and open outer bounds differed, their bounds in [0,1] give by F5 a rational $v$ strictly between them, with $0<v\le 1$. Each rational measure game has the explicit natural-number coding in F1's game convention, so A1 determines it. If I won, F1 under A2 would give ${\nu }_{\mathrm{i}\mathrm{n}}(E)\ge v$, a contradiction; if II won it would give ${\nu }_{\mathrm{o}\mathrm{u}\mathrm{t}}(E)\le v$, also a contradiction. Thus the two envelope values agree. The dyadic interface F4 applies under the same A2 and gives $b^{-1}[E]$ Lebesgue measurable.

For any $A\subseteq [0,1)$ take E=b[A]. By F4 the dyadic $b$ is injective, so $b^{-1}[E]=A$: forward membership gives b(x)=b(a) for some a in A and therefore x=a, and reverse membership is immediate. Step 1.1 thus makes every such A measurable.

For arbitrary $A\subseteq \mathbb{R}$, set $A_m=(A\cap [m,m+1))-m$ for each integer m. These are subsets of [0,1), hence measurable by step 2.1. F2 makes each translate $A_m+m$ measurable. Enumerate the integers $0,1,-1,2,-2,\dots$; by F3 their corresponding pieces have union A. The Lebesgue sigma-algebra under A2 (countable choice is derived from DC in F4's proof) is closed under this sequence of unions. Hence A is measurable. No choices of pieces are involved: each is defined by A and m. QED.