Correctness of the pure Tseitin input validator

This proof-only module identifies the finite-state validity scan used by the CNF-to-3CNF reduction machine with the existing executable CNF decoder. The argument first characterizes accepted token prefixes as canonical CNF.tokens streams, then transports that characterization across the concrete two-bit tokenization.

theorem Complexity.SAT.ThreeSAT.Machine.validEncoding_eq_decode?_isSome_internal (z : List Bool) : validEncoding z = (CNF.decode? z).isSome

The pure finite-state validator accepts exactly the inputs on which the existing executable CNF decoder succeeds.