FormalSLT PR #82 adds finite PAC-Bayes wrappers for a randomized-prior presentation, plus a compact NN-generalization example that shows how a monotone complexity penalty can improve a bound when the supplied certificate decreases.
The module gives stable names to PAC-Bayes Bernstein and randomized-prior adapters that are already finite and certificate-driven. The example keeps the neural-network story finite: a two-hypothesis class, a monotone penalty, and a checked inequality showing that lowering the supplied complexity proxy lowers the displayed penalty.