Exact greatest-integer semantics of $f(n)$

For every natural number $n$, including $n=0$, set $I_n=\{m\in\mathbb N:n<m<2n\}$ and $J_n=\{m\in\mathbb N:2n<m<4n\}$. For a natural number $k$, let $G_n(k)$ mean that for every finite set $B\subseteq J_n$, there exists a finite set $C\subseteq I_n$ such that $c+c'\notin B$ for every two distinct elements $c,c'\in C$, and $k\le |B|+|C|$. The integer $f(n)$ is the integer coercion of the bounded-search value that returns the greatest natural number $k\le |J_n|+|I_n|$ satisfying $G_n(k)$, with value $0$ if no such $k$ exists. The theorem asserts both that, for every finite $B\subseteq J_n$, there is a finite $C\subseteq I_n$ with no sum of two distinct members of $C$ belonging to $B$ and with $f(n)\le |B|+|C|$ after the cardinality is regarded as an integer, and that every integer $t$—including negative integers—with this same universal property satisfies $t\le f(n)$. Thus the asserted maximality is among all integer thresholds, although $f(n)$ itself is nonnegative by definition. In the included case $n=0$, both intervals are empty, so the only possible $B$ and admissible $C$ are empty and the guarantee reduces to $t\le 0$.