To make this more easily readable, I'll start with the question and then give the explanation/motivation.

**Question**. Is the following principle *(or its weakening, with "for every real $r$" replaced with "for every real $r$ on a cone")* consistent with ZFC?

$(*)\quad$ "For every normal functional $F$ of type $n>2$, there is some normal $G$ of type $2$ such that

for every real $r$we have ${}_1sc(F,r)={}_1sc(G,r)$."

(Admittedly I don't know that the *negation* of $(*)$ is consistent, but $(*)$ seems so strong that an outright proof would seriously surprise me and so it seems better to ask for mere consistency.)

Above, "$\le$" denotes reducibility in the sense of Kleene's finite-type recursion (or its many equivalent formulations). For $k\le n$ and $F$ a type-$n$ functional, we let $_ksc(F)=\{g\in tp(k): g\le F\}$; this is the *$k$-section of $F$*. A type-$n$ functional $F$ is *normal* if it computes the type-$n$ "equality functional" $^nE$ (which determines whether a type-$(n-1)$ functional is identically zero or not); intuitively, $^2E$ is the usual Turing jump operator, and normality in type-$2$ is just "effective discontinuity".

The motivation for considering $(*)$ as even remotely plausible comes from (the $k=1$ case of) Sacks' Plus-One Theorem, which states that the result holds if we remove the real parameter. (Further motivation at least for the *interestingness* of $(*)$ comes from the *extended* plus-one hypothesis, but this does not seem to be directly related.)

My personal suspicion is that even the weak version of $(*)$ is inconsistent with ZFC, but I don't see how to prove that. Possibly a line of attack would come from examining the proof that the extended plus-one hypothesis fails in ZF+AD. However, as said above I don't see any direct connection here.

In the other direction, one approach to proving that $(*)$ *is* consistent would be to analyze a "boldface" version of the forcing Sacks used to prove the Plus-One Theorem. Roughly speaking, given a normal type-$n$ functional $F$ ($n>2$) Sacks forces with countable partial maps $p:\omega^\omega\rightarrow\omega$ satisfying two properties: $(i)$ that a certain hierarchy $Trees(p)$ of objects recursive in $p$ has a certain technical property, and $(ii)$ $p\in{}_1sc(F)$. (The generic object $H$ is then a functional defined on $_1sc(F)$, and the $G$ we want $H\cup\{(f,0): f\not\in{}_1sc(F)\}$.) The boldface version of this would probably consist of those $p$ such that *for every real $r$* (possibly on a cone):

$(i)$ The hierarchy $Trees(p\upharpoonright {}_1sc(F,r), r)$ has the technical property.

$(ii)$ The restriction $p\upharpoonright{}_1sc(F,r)$ is an element of $_1sc(F,r)$.

However, it's not at all clear to me that this modified forcing behaves the way we would want.

$k$-envelope; an analogous question can be formulated for envelopes with $1$ replaced by $2$ - see page $36$ of Longley's survey - and I would be equally interested in that, but for now I'm sticking with sections if only for simplicity. $\endgroup$