Rational Response Error Cleanup

Abstract

Arbitrary response-error stacks reach the exact clean one-zero terminal state.

Theorem 1.1 (Arbitrary scratch contents and linear physical erasure).

$$\forall st\in PostControl,\forall input\in \mathrm{List}\left(ResponseSymbol\right),\forall quotient\in \mathrm{List}\left(ResponseSymbol\right),\forall shifts\in \mathrm{List}\left(ResponseSymbol\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(postMachine\right),\mathrm{postCfg}\left(badInput,st,input,quotient,shifts,nil\right),\mathrm{some}\left(\mathrm{haltList}\left(postMachine,\mathrm{singleton}\left(zero\right)\right)\right),\mathrm{length}\left(input\right)+\mathrm{length}\left(quotient\right)+\mathrm{length}\left(shifts\right)+3\right)\right)$$

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

Source. Repository-derived.

Commentary.

At badInput, the finite control and the input, quotient and shift stacks may contain arbitrary ternary words. The output stack is initially empty. Three actual draining passes erase all remaining symbols, write one zero, reset the control and halt with all scratch empty. The bound is the three initial lengths plus three.

This theorem starts at error entry. The whole-word refinement establishes which parser branches reach that entry. No physical oracle or SAT count occurs in this cleanup statement.

References

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