feat(realizability): add cslib-backed P/poly certificates

[quangvdao]

Summary

Adds the optional PolyFunCslib adapter for boundary-pinned, non-uniform P/poly realizability, stacked on #178.

• keeps the generic PolyFun umbrella backend-neutral; the adapter is a separate Lake library
• supplies a cslib-backed quantitative step class whose representations are bit encodings and whose certified work charge is the cslib time-polynomial envelope
• pins input, output, position, and flattened-index encodings
• translates the family-indexed boundary and realization into PolyFun's generic Boundary, QuantitativeRealization, execution traces, and execution costs
• certifies initialization, combined return-or-query observation, and partial enabled transitions with ToCslib machine families
• records polynomial interaction, state-length, running-time, and description-size bounds, including a theorem bounding the sum of all three concrete machine descriptions
• requires syntactic progress at every reachable query, excluding vacuous certificates for empty answer types
• proves an additive whole-run certified-work bound
• provides closure under input precomposition, result mapping, and pointwise program equality
• bridges pure Boolean certificates to the finite-machine RealizableLE class
• proves a counting-based non-triviality theorem: not every BitVec n → Bool family is in the pinned P/poly class

Files

• PolyFunCslib/Backend.lean: cslib-backed qualitative and quantitative PolyFun step classes plus the generic trace-work lemma.
• PolyFunCslib/PPoly.lean: family boundaries, generic-boundary translation, realizations, progress, witnesses, and closure.
• PolyFunCslib/Nontriviality.lean: canonical coin boundary, counting bridge, and diagonal theorem.
• PolyFunCslib.lean: optional umbrella.
• PolyFunTest/Realizability/CslibPPoly.lean: producer canaries covering a real query, both answer branches, mismatched indices, trace accounting, precomposition, result mapping, and rejection of an empty-answer stuck program.
• Lake/CI/docs files: register, build, lint, axiom-sweep, and explain the separate optional library.

Validation

• ./scripts/validate.sh --lint --test --axioms
• git diff --check

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