How is this HA unprovable formula recursive realizable? In Realizability: A Historical Essay [Jaap van Oosten, 2002], it is said that recursive realizability and HA provability do not concur, because although every HA provable closed formula is realizable, not every realizable closed formula is HA provable. Van Oosten points out that Propositional calculus and realizability [G.F. Rose] first proved this, but his example is a bit unwieldy and the old syntax a bit terse. Van Oosten also notes, in a footnote, the following simple formula due to G.S. Tseitin, which would be realizable but not HA provable:
$$ \big[\neg (A \land B) \land (\neg A \to (C \lor D)) \land (\neg B \to (C \lor D))\big] \to \big[(\neg A \to C)\lor(\neg B \to C)\lor(\neg A \to D)\lor(\neg B \to D)\big] $$
I get how this formula is not HA provable, because it's essentially just De Morgan. But I don't see how this would be recursive realizable? Somehow De Morgen is intertwined twice, but I don't see how this would cleverly sitestep the otherwise unrealizable $\neg (A\land B) \to (\neg A \lor \neg B)$.
 A: Let us first have a look at the core obstace for $$\neg (A \wedge B) \rightarrow (\neg A \vee \neg B)$$
Negated formulas do not have computational content, so $\neg (A \wedge B)$ is only a promise that either $A$ or $B$ is false, but does not provide any useful information. But we need to explicit compute a bit telling us whether $\neg A$ or $\neg B$ is going to be realized, and we have no input to compute this from.
Now in the given formula, we have three premises: As before, $\neg (A \wedge B)$ is merely a promise, but contains no information. $\neg A \rightarrow (C \vee D)$ is realized by a Turing machine $M_1$ that if $\neg A$ holds, will terminate, and tell us either that $C$ holds (and provide a realizer), or that $D$ holds (and provide a realizer). Likewise, $\neg B \rightarrow (C \vee D)$ gives a Turing machine $M_2$, working analogously.
The promise that $\neg (A \wedge B)$ guarantees that at least one of $M_1$ and $M_2$ halts. Markov's principle lets us compute the index of one that does. For example, assume that $M_1$ halts and claims that $C$ holds (and gives a claimed realizer of $C$). Classically, this means one of two things: Either $\neg A$ holds, in which case $M_1$ is required to be correct, or $\neg A$ does not hold. In either case, we can now claim that $\neg A \rightarrow C$ (on the righthand side of the big implication), and give the claimed realizer of $C$ as the output here. Any other combination of what machine $M_1$, $M_2$ halts, and what they are claiming then, also gives us one of the cases on the right.
