I'm sure this is just my google-fu failing me, but: what are sufficient, non-overkill large cardinal axioms which guarantee "Every (boldface) $\Pi^1_n$ set of (real codes for) countable ordinals contains or is disjoint from a club subset of $\omega_1$"? (I asked this question on math.stackexchange a couple weeks ago http://math.stackexchange.com/questions/1539202/clubbiness-of-pi1-n-setshttps://math.stackexchange.com/questions/1539202/clubbiness-of-pi1-n-sets, and received some attention but no answer.)
To clarify, I'm asking about the strength over ZFC.
Here's a very silly upper bound: suppose $L(\mathbb{R})$ is a model of AD, and moreover every $\Pi^1_n$-sentence with real parameters is absolute between $L(\mathbb{R})$ and $V$ (actually, I think this is already a consequence of "$L(\mathbb{R})\models AD$," but I'm not sure). Then let $A\in V$ be a $\Pi^1_n$-set of countable ordinals, via the formula (with real parameters) $\varphi$. By the absoluteness assumption, $\varphi^{L(\mathbb{R})}=A$, so $A\in L(\mathbb{R})$. And since $L(\mathbb{R})\models AD$, $L(\mathbb{R})$ thinks $A$ contains or is disjoint from a club. But inner models compute club-ness correctly, so we're done.
This seems massively overkill to me, though - what is the right bound?
