Clause Machine Error Cleanup

Abstract

Error cleanup returns the zero-variable, one-empty-clause query descriptor.

Theorem 1.1 (All stack contents, exact clean halt and linear cleanup time).

$$\forall st\in PreControl,\forall input\in \mathrm{List}\left(Bool\right),\forall header\in \mathrm{List}\left(Bool\right),\forall scratch\in \mathrm{List}\left(Bool\right),\forall query\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(preMachine\right),\mathrm{preCfg}\left(badInput,st,input,header,scratch,query,nil\right),\mathrm{some}\left(\mathrm{haltList}\left(preMachine,dummyQuery\right)\right),\mathrm{length}\left(input\right)+\mathrm{length}\left(header\right)+\mathrm{length}\left(scratch\right)+\mathrm{length}\left(query\right)+5\right)\right)$$

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

Source. Repository-derived.

Commentary.

From error entry, every finite control state and all arbitrary Boolean input, header, scratch and partial-query words are included, with the output stack initially empty. The actual fixed machine drains those four stacks, writes the dummy query, resets its control to the initial state and reaches the exact haltList configuration.

The transition bound is the sum of the four initial stack lengths plus five. Each pop removes one real symbol. Four empty-stack transitions select the next cleanup phase, and the final fixed statement writes the complete dummy word.

The dummy word describes zero hidden variables and one empty raw clause. This result proves cleanup from error entry. The separate parser-to-error-entry run and its complete polynomial bound are required for universal malformed-source correctness.

References

• Truth anchor: D5/S0/Computability/ClauseMalformedCleanup.pre_error_cleanup
• Dependency: D5/S0/Computability/ClauseQueryPreprocessor