Indeed, very very nice, a great addition to our library of constructive results in commutative algebra!

Great and quite general answer! Can we improve from "$F$ not empty" to "the unique morphism $F \to 1$ is open and surjective"?

I'm unfortunately not familiar with the universal hypercomputer. For ITTMs, the realizability topos is indeed quite interesting. LEM fails, but Markov's principle and indeed LPO (for the natural numbers) hold. DC holds and hence Cauchy and Dedekind reals agree. There is an injection from $\mathbb{N}^\mathbb{N}$ and from $\mathbb{R}$ to $\mathbb{N}$ (however there is no surjection $\mathbb{N} \twoheadrightarrow \mathbb{R}$). We also used this setting as a countermodel for differentiating between certain Noetherian conditions.

Yes indeed, there is a well-defined pullback operation, but this does NOT proceed by applying the inverse image functor $f^*$ to the frame object. (Applying $f^*$ to a poset will yield a poset again, but even if it was complete before after applying $f^*$ it usually won't be.) Instead, locales need to be pulled back as follows: Pick a generating system for its frame, pull back that generating system using $f^*$, and then complete this generating system into a full-fledged frame again. Details are on page 25 of Steve's paper

If you allow yourself a bit of topos logic, here is how you can do it: Start with the classifying topos of the theory of local rings. This topos has its site the category of finitely presented rings. Then, pass to the slice over $R$. Thereby you obtain the big Zariski topos of $R$. Then use the construction from Section 16.2 of my thesis to cut down to the little Zariski topos of $R$.

Here is a thing you could do, in lieu the geometric morphisms which likely don't exist/are trivial: Internally to the effective topos, you could construct a (suitable version of) the topological topos. That would basically amount to rereading the account of TT, but now not in a metatheory such as ZFC or IZF, but using Russian-style constructivism as the metatheory (with its formal Church–Turing thesis, every function $\mathbb{N} \to \mathbb{N}$ is Turing-computable). You could also do it the other way round.

Dear @JoelDavidHamkins, non-classical logic mathematics is just one further part of the multiverse :-) With the interesting phenomenon that forcing no longer needs to preserve and reflect the truth of bounded first-order statements, if the base universe is nonclassical.

@Gro-Tsen Yes, indeed, on all points you raised in your two comments. :-) (That the altered definition doesn't prove the disjunction and the existence property is not a big issue to me. We need a variant of the standard Kleene definition anyway. All versions of realizability are beautiful)

At the expense of one top-level implication, we can also get the "sloppy" definition to work in weak metatheories: PRA proves that for every formula $\varphi$, if HA proves $\varphi$ then there is a number $n$ such that HA proves $\overline{n} \mathop{\mathbf{r}}\, (\top \Rightarrow \varphi)$.

Yes; perhaps I should stress that in a strong metatheory like IZF or ZFC or even HA + "Turing machines which HA-provably terminate actually terminate", we do have the strong form of the soundness theorem with the external existential quantification even for the "sloppy" definition. The difference is visible only in weak metatheories like PRA, HA or PA. I think most works set in the context of an arbitrary untyped PCA get it right, as there the only pairing function $S \times S \to S$ which comes to mind is the appropriate version of Church pairs.

(fyi, the lower bound of 8000 was lowered by bachelor student Johannes Riebel to 745 (from an earlier bound of 748).)

Intuitively, from a HA-proof of an existential statement we should not be able to extract a witnessing number, just an algorithm for computing a witnessing number.

Just a comment: For the clauses regarding disjunction and existential quantification, it's quite important that the pairing function is not some standard primitive-recursive bijection. Instead, we should pair two numbers $x_1,x_2$ by the index of some canonical Turing machine which on input $i$ terminates with $x_i$. Else the soundness theorem "if HA proves a formula $\varphi$, there is a number $n \in \mathbb{N}$ such that HA proves $n \mathop{\mathbf{r}}\varphi$" is not provable in PRA (nor in HA or PA), such that we need to resort to the weaker statement (2) with the internal $\exists$.