Mirror PAC-Bayes Bernstein prior-moment and finite-grid wrappers

[Robby955]

This PR mirrors the PAC-Bayes Bernstein work that landed on
Robby955/lean-statistical-learning:release-candidate in PR #77 and PR #78
into the public Robby955/FormalSLT repository.

What changed

• Adds FormalSLT/PACBayesMargin.lean, which specializes the Bernstein
  supplied-proxy layer to thresholded classifier-margin losses.
• Extends FormalSLT/PACBayesBernstein.lean with finite-grid and optimized
  finite-grid bad-event wrappers for finitely many lambda choices.
• Updates the PAC-Bayes examples:
  • examples/CheckPACBayesBernstein.lean
  • examples/CheckPACBayesMargin.lean
• Refreshes the public README, theorem map, roadmap, theorem-chain SVG, and
  proof-frontier manifest for the new public theorem surface.
• Adds scripts/repo-stats.sh and .stats.json so README/SVG size figures
  are regenerated from the checked Lean tree instead of edited by hand.

Main checked endpoints

• finitePACBayesBernsteinGrid_badEventMass_le_sum_delta
• finitePACBayesBernsteinGrid_badEventMass_le_delta
• finitePACBayesBernsteinGridOptimized_badEventMass_le_sum_delta
• finitePACBayesBernsteinGridOptimized_badEventMass_le_delta
• finitePACBayesClassifierMarginBernstein_iid_badEventMass_le_delta
• finitePACBayesClassifierMarginBernstein_iid_gridOptimized_badEventMass_le_sum_delta
• finitePACBayesClassifierMarginBernstein_iid_gridOptimized_badEventMass_le_delta

Scope

This is still a finite theorem surface. It does not claim continuous posterior
spaces, infinite hypothesis classes, exact all-real lambda optimization, or
general measurable-space classifier-margin bounds.

Verification

Run in a fresh public clone on branch
feature/mirror-pac-bayes-bernstein-77-78-2026-06-05:

lake build FormalSLT
lake env lean examples/CheckPACBayesBernstein.lean
lake env lean examples/CheckPACBayesMargin.lean
for f in examples/*.lean; do lake env lean "$f"; done
python3 scripts/generate_proof_frontier_manifest.py --check
./scripts/repo-stats.sh --check
git diff --check origin/main..HEAD
python3 /Users/robsneiderman/Desktop/AI4MATH/scripts/audit_public_writing.py \
  README.md CONTRIBUTING.md CITATION.cff \
  docs/assumptions-and-nonclaims.md docs/diagrams.md docs/roadmap.md \
  docs/theorem-map.md docs/SharpMcDiarmid.md

The focused PAC-Bayes checkers report the standard axiom profile:
[propext, Classical.choice, Quot.sound].

No public-only files from Robby955/FormalSLT:main were deleted in this mirror
branch.

[coderabbitai]

Important

Review skipped

Draft detected.

Please check the settings in the CodeRabbit UI or the .coderabbit.yaml file in this repository. To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro Plus

Run ID: 175bcb28-cf56-480e-a8ea-f964849104b0

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

✨ Finishing Touches

🧪 Generate unit tests (beta)

• Create PR with unit tests
• Commit unit tests in branch feature/mirror-pac-bayes-bernstein-77-78-2026-06-05

---

_{Comment @coderabbitai help to get the list of available commands and usage tips.}