Canonical Quotient-State Realization of Bounded-Width Dynamic Programming in Layered Tseytin 3-CNF

This paper studies canonical quotient-state compression in a deterministic residual decision model, on a bounded-width layered 3-CNF family that arises from standard Tseytin encodings of bounded-fanin layered Boolean circuits. An admitted target family is defined, and the fixed gate-by-gate translation from the source family is shown to land inside it.

On that family the paper proves that every reachable residual admits an active/future cut with bounded boundary; that the unresolved suffix affects continuation only through a Boolean suffix summary on that boundary; that the suffix summary at a fixed cut index is determined by the fixed input and the cut position; that the suffix-summary sequence is computable in deterministic polynomial time by backward dynamic programming on the layered suffix; that the branch-labelled successor on canonical residual states is well defined; and that for fixed width and fanin bound, the reachable canonical quotient-state space is linearly bounded in the clause count.

Where the statement stops. This is a structural realisation for the admitted bounded-width family, with every state-counting and running-time bound parameterised by the two fixed constants. It expresses standard bounded-interface dynamic-programming semantics as a quotient-state construction inside a forward residual model. It says nothing about formula families outside that admitted regime.