feat: expose the public PFunctor module surface

[dtumad]

Summary

• add a public, reusable PFunctor.Handler instrumentation API for lifting handler targets and inserting pre/post effects
• provide writer-based tracing operations together with public application and factorization laws
• expose the interaction sampler, fairness, observation, and open-process laws needed by downstream clients without implementation imports

Motivation

Lean's module system gives private and unexposed declarations stronger API-boundary meaning. This change makes the intended downstream surface explicit in PolyFun so clients can depend on public laws instead of using import all or relying on implementation details.

Validation

• lake build
• git diff --check

Downstream

This is the PolyFun side of a paired change. Verified-zkEVM/VCVio#511 pins this commit and exercises the new generic PFunctor surface; that draft is stacked on Verified-zkEVM/VCVio#510.