The Raisonnier family is a Sigma-one-three filter

Upward closure: if $a\in F(x)$ is witnessed by a cover $⟨F_n⟩$ and $a\subseteq b$, the same cover witnesses $b\in F(x)$.

For later use, here is the choice-free relativized coding fact in [F3]. A real $p$ can code a well-founded extensional relation on $\omega$ whose collapse is a correct countable level $L_{\beta }[x]$ containing a specified real $z$. Well-foundedness is ${\mathrm{\Pi }}_1^1$, and the definition recursion, satisfaction relation and distinguished element checks are arithmetic. Every $z\in L[x]\cap {\omega }^{\omega }$ has such a certificate: take the canonical Skolem hull of $\omega \cup \{x,z\}$ in a sufficiently large level and collapse it; least Skolem witnesses canonically enumerate the hull, so no choice is used. Conversely collapse and induction through the hierarchy make every certificate correct. Thus $z\in L[x]$ is ${\mathrm{\Sigma }}_2^1(x)$.

Closure under intersections: if $a,b\in F(x)$ are witnessed by covers $⟨F_n^a:n<\omega ⟩$, $⟨F_m^b:m<\omega ⟩$, fix a bijection $\pi :\omega \to \omega \times \omega$ and, for $\pi (k)=(n,m)$, put $F_k:=F_n^a\cap F_m^b$. These pairwise intersections cover $L[x]\cap 2^{\omega }$: for any $z$ in that set, choose $n$ and $m$ with $z\in F_n^a$ and $z\in F_m^b$, and then $z\in F_k$ for the unique $k$ with $\pi (k)=(n,m)$. Moreover $H(F_k)\subseteq H(F_n^a)\cap H(F_m^b)$, because a first difference of two points lying in the intersection is a first difference of points of each factor. Hence ${\bigcup }_{k}H(F_k)\subseteq a\cap b$ and $a\cap b\in F(x)$.

By [F1] and [F5] replace each cover member by a closed body $[T_n]$ of a binary tree $T_n\subseteq 2^{<\omega }$ and code the sequence by one real $y$. Membership $a\in F(x)$ is equivalent to the existence of $y$ such that (i) every binary constructible real lies in some $[T_n]$, that is, $\mathrm{\forall }z\in 2^{\omega }(z\in L[x]⟶z\in {\bigcup }_n[T_n])$, and (ii) every first difference of two points of one $[T_n]$ lies in $a$. Using the certificate form from step 1.2, clause (i) is ${\mathrm{\Pi }}_2^1(x)$: universally quantify a binary real and a proposed certificate, and require either failure of its ${\mathrm{\Pi }}_1^1$ certificate or membership in one tree body. Clause (ii) is ${\mathrm{\Pi }}_1^1$, not arithmetic: universally quantify two binary proposed branches and then check the arithmetic first-difference implication. It is therefore also ${\mathrm{\Pi }}_2^1$. Their conjunction preceded by the existential tree-sequence code $y$ is ${\mathrm{\Sigma }}_3^1(x)$ in the sense of [F6].

For every $\alpha <{\omega }_1^{L[x]}$, $L[x]$ contains a real coding a well-order of a subset of $\omega$ of type $\alpha$: use the domain $\alpha$ for finite $\alpha$ (including the empty domain for $0$), and a bijective enumeration by $\omega$ for infinite $\alpha$. Encode both the domain and the relation by binary coordinates using the fixed pairing. Choose the ${<}_{L[x]}$-least such code; uniqueness gives an injection $\alpha \mapsto c_{\alpha }$ from ${\omega }_1^{L[x]}$ into $L[x]\cap 2^{\omega }$ without any simultaneous choice. Hence the Given equality makes $L[x]\cap 2^{\omega }$ uncountable in the ambient universe. If $\mathrm{\varnothing }\in F(x)$, a witnessing cover would have $H(F_n)=\mathrm{\varnothing }$ for every $n$, so every $F_n$ would have at most one point; Countable Choice would make their union countable, contradicting that uncountability. Thus $F(x)$ is proper.

The Fréchet filter is contained in $F(x)$: fix $n$ and let the cover consist of the $2^n$ cylinders $[s]$, $s\in 2^n$, padded by empty sets. Two distinct reals in one cylinder agree on the first $n$ coordinates, so their first differing coordinate is at least $n$ and their prefix length $h$ is at least $n+1$. In particular ${\bigcup }_{s}H([s])\subseteq \{k:k\ge n\}=\omega \setminus n$, so the cofinite set $\omega \setminus n$ belongs to $F(x)$. Together with the steps above this makes $F(x)$ a proper filter extending the Fréchet filter.

The steps above establish that $F(x)$ is a proper filter extending the Fréchet filter, and step 2.2 that membership is ${\mathrm{\Sigma }}_3^1(x)$; this is the Statement.