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 covers every raw one-hot group, the following halted/none-label equality, every stack's suffix-OR active mask, and every fixed stack-cell XNOR block with exact contextual runs and closed wire indices. The leading blank-bit negations now close each complete semantic six-gate cell block. Finite-family decomposition also identifies the exact ordered 6H cell suffix and complete mask-plus-cells stream of each fixed stack. The fixed stack enumeration then closes the complete semantic stack-family byte stream. A uniform executable family iterator remains an execution gap; the exact post-stack boundary is now fixed, so the final conjunction is the only remaining semantic tail.