Cook--Levin circuitization

This facade exports the normalized verifier witness, polynomial execution envelopes, proof-carrying whole-tableau assembly, and the closed verifier circuit. Its principal contracts are well-formedness, exact satisfiability semantics, fixed-verifier polynomial gate and input bounds, and a polynomial bound for the complete circuit encoding. The exported cookLevinMap packages that circuit as an explicit finite-string map with exact membership semantics and a polynomial output-length bound. The generator-clock layer supplies concrete exact unary clocks for every primary verifier-circuit dimension without adding a source-alphabet finiteness premise to the universal construction. The generator-header layer derives the exact tableau arity polynomial, emits the canonical circuit header and initial input-gate family, combines them in one concrete input-preserving run, and proves that the result is a literal prefix of the complete semantic verifier-circuit encoding. The generator-validity layer identifies the literal serialized suffix for all canonical row-validity gates and proves that the resulting stream advances that prefix through the complete validity phase. Its concrete construction now executes every raw one-hot group, halted/none-label equality, all stack canonicality blocks, and the final conjunction in one fixed whole-row controller. The exact output theorem agrees byte-for-byte with validityRowGateStreamAt, and the runtime is explicitly quadratic in the delimiter-bearing row frame. A fixed raw-input source compiler now generates the actual halted-start, halted-left, and halted-right operand triple for every public tableau row in polynomial time. A second fixed source compiler emits the row-major (height, gateStart, rowBase) seeds whose arithmetic expansion is exactly the full semantic row-frame family. The continuous one-hot seed expander is polynomial-time and produces the canonical four-field operands. The transition source is closed byte-for-byte: one fixed polynomial-time TM2 now constructs the unrestricted recursive dispatch, transition boundary, and complete narrowing/equality/final-conjunction tail for every canonical seed. A delimiter-safe quoted-row construction and a verified continuous decoder produce the exact unary input of the established transition-family controller, and composition yields the complete semantic transition gate stream directly from the raw verifier word. The raw-input compiler now also crosses the complete optional accepting boundary. In the representable branch it emits and semantically aligns every halted output-row equality; in the static negative branch it emits the exact absent-operand marker. The final conjunction and selected output wire are compiled as well; a reusable finite-alphabet same-input concatenator joins the header/input/pool prefix to this complete body and emits the canonical circuit encoding directly from the original verifier input.