feat(tocslib): add polynomial-time single-tape toolkit

[quangvdao]

Summary

Adds a separate ToCslib Lake library for reusable extensions of the pinned cslib single-tape machine API. This is the low-level first slice extracted from VCVio #500.

• encoded polynomial-time witnesses with explicit machine-description size;
• fixed-width and variable-width binary encoding families, with independent source/target universes;
• concrete constant and finite-table machines;
• canonical finite machine tables and the counting/diagonalization toolkit;
• direct producer canaries for bit order, finite-table semantics, bit overwrite, and function-space cardinality.

Ownership

ToCslib imports only cslib and Mathlib. It does not import PolyFun realizability, oracle semantics, probability, or cryptography. The later PolyFun backend adapter will import it explicitly; the generated PolyFun umbrella does not.

Validation

• lake build ToCslib
• lake build PolyFunTest.ToCslib.Basic
• lake build PolyFun
• lake lint (now covers both PolyFun and ToCslib)
• ./scripts/validate.sh --lint --test --axioms
• git diff --check

All pass locally on Lean 4.33.1, with zero sorry/axiom debt under PolyFun and ToCslib.