Restored Dense Word Execution

Abstract

Actual dictionary construction and lookup produce a clean dense word.

Theorem 1.1 (Restored Dense Word Execution).

$$\forall w\in \mathrm{List}\left(Bool\right),\mathrm{Nonempty}\left(\mathrm{EvalsToInTime}\left(\mathrm{step}\left(denseMachine\right),\mathrm{initList}\left(denseMachine,w\right),\mathrm{some}\left(\mathrm{haltList}\left(denseMachine,\mathrm{denseConverted}\left(w\right)\right)\right),\mathrm{denseRunClock}\left(w\right)\right)\right)\wedge \left(\forall F\in ConventionalFormula,\mathrm{readWord}\left(w\right)=\mathrm{some}\left(F\right)\Rightarrow \left(w=\mathrm{formulaWord}\left(F\right)\wedge \left(\forall c\in Clause,c\in F\Rightarrow \mathrm{length}\left(c\right)\le 3\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The actual parser phase is followed by rightmost dictionary deduplication, dimension writing, restored first-index lookups, literal copying, dictionary draining and output reversal. Every raw word reaches the exact clean haltList containing denseConverted within the phase-by-phase denseRunClock. Malformed input takes the actual drain and zero-variable empty-clause source branch. Accepted input has its full original spelling and clause width; the semantic refinement then supplies the quadratic clock and count transport.

References

• Truth anchor: D5/S0/Computability/DenseClauseExecution.denseExecution
• Dependency: D5/S0/Computability/DenseClauseMachine