Total Rational Response Refinement

Abstract

Every raw ternary response executes to a canonical binary word in linear time.

Theorem 1.1 (Whole-word execution, arithmetic recovery and exact fault output).

$$\forall w\in \mathrm{List}\left(ResponseSymbol\right),\mathrm{Nonempty}\left(TM2OutputsInTime\left(postMachine,w,\mathrm{some}\left(\mathrm{binaryWord}\left(\mathrm{totalPostOutput}\left(w\right)\right)\right),3\cdot \mathrm{length}\left(w\right)+10\right)\right)\wedge \left(\left(\forall xs\in \mathrm{List}\left(Bool\right),\forall e\in Nat,w=\mathrm{responseWord}\left(xs,e\right)\Rightarrow \left(3\mid \mathrm{msbValue}\left(\mathrm{cons}\left(true,xs\right)\right)\Rightarrow \left(\left(0<e\Rightarrow \mathrm{Odd}\left(\mathrm{msbValue}\left(\mathrm{cons}\left(true,xs\right)\right)\right)\right)\Rightarrow \begin{array}{r}e=0\Rightarrow \mathrm{msbValue}\left(\mathrm{totalPostOutput}\left(w\right)\right)=2\cdot \lfloor \frac{\mathrm{msbValue}\left(\mathrm{cons}\left(true,xs\right)\right)}{3}\rfloor \\ 0<e\Rightarrow \mathrm{msbValue}\left(\mathrm{totalPostOutput}\left(w\right)\right)=\lfloor \frac{\lfloor \frac{\mathrm{msbValue}\left(\mathrm{cons}\left(true,xs\right)\right)}{3}\rfloor }{2^{e-1}}\rfloor \end{array}\right)\right)\right)\wedge \left(\left(\left(\neg \mathrm{suitableResponse}\left(w\right)\right)\Rightarrow \mathrm{totalPostOutput}\left(w\right)=\mathrm{singleton}\left(false\right)\right)\wedge \left(\mathrm{totalPostOutput}\left(w\right)=\mathrm{singleton}\left(false\right)\vee \left(\exists bs\in \mathrm{List}\left(Bool\right),\mathrm{totalPostOutput}\left(w\right)=\mathrm{cons}\left(true,bs\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S0/Computability/RationalResponseRefinement.post_word_run (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every word over zero, one and slash, the fixed four-stack, eleven-label machine reaches the exact clean haltList output in at most three times the input length plus ten actual transitions. All scratch is empty and the finite control is restored.

Arithmetic suitability means a positive binary numerator, exactly one slash and a denominator one followed by e zeros. The numerator is divisible by three and is odd when e is positive. Suitable words yield twice p divided by three when e is zero, and otherwise the integer quotient of p divided by three and then by two to the power e minus one. Every unsuitable word produces exactly one zero. Every output is one zero or begins with one.

Suitability is an arithmetic condition, independent of the physical trace. The word 11/1 is suitable and yields two; the physical dummy response 11/100 yields zero. Count correctness requires the separate physical response relation. Zero output does not characterize rejection.

References

• Truth anchor: D5/S0/Computability/RationalResponseRefinement.post_word_run
• Dependency: D5/S0/Computability/RationalMalformedCleanup
• Dependency: D5/S0/Computability/RationalPostprocessor