> How can we justify not steelmanning a ternary approach to halting?
I'm not certain I understand what you mean here. In actual practice, the usual approach to undecidable problems--which come up all the time in compilers and formal methods, mind you--is to build a trichotomy of "yes", "no", and "don't know" (sometimes expressed "timeout"). What undecidability says is we can't squeeze the "don't know" category down to nothing, but in many circumstances, that's just fine.
> Can someone show me one proof which doesn’t rely on “muh do the opposite” (how do we know the halts program can’t detect this and crash with Err(ParadoxError)?) or the circular logic appeal to Rice’s theorem which itself depends on halts being undecidable?
Depending on how you define "muh do the opposite", this may be impossible. The essential crux of the theorem is that once your system reaches a certain level of power, it admits the possibilities of quines, which enables a level of self-reference that leads to paradoxes.
The best attempt I can give, that only indirectly reaches into self-reference is this:
Let f(x) be a program that returns the size of the smallest size program needed to output x (this is called Kolmogrov complexity). Let h(p) be a program that returns whether or not the input program p will halt. If h(p) exists, then f(x) necessarily exists:
for p = 1 to infinity:
if h(p) is true:
if p computes x: return sizeof(p)
If f(x) exists, we can write g(y) (informally, output the smallest integer that has at least a given Kolmogrov complexity) as follows: for x = 1 to infinity:
if f(x) > y:
return x
However, we have a paradox now. If g exists, it has a size, which of course bounds the maximum complexity of its output. But we've just asserted that the output has to have a minimum complexity--and if we choose the bounds right, there's no possible overlap. Consequently, something in the construction must be wrong. Yet I've given the code for every program but the halting program... which means the halting program itself can't exist.