[SamuelSchlesinger]

Part of #4914 (milestone M3(a–b) of the plan in #4914 (comment)). Stacked on #5029, which is approved; this PR will be retargeted to main once that lands.

This adds the first half of the Moran–Yehudayoff compression scheme for classes of finite VC dimension, in the new module PACLearning/Compression/VCDimension.lean. Fix a consistent learner A for C that reads s ≥ vcSampleSize d ε δ examples with δ < 1, and a sample S that C realizes.

• IsConsistent.exists_subsample_toOuterMeasure_le: for every distribution on the positions of S, some sequence b of s positions has A (S ∘ b) wrong on a set of probability at most ε. The proof applies the VC upper bound on the finite domain Fin m, to the traces of C on the sample points and to the pushforward of the distribution along the labels. No measurability hypothesis on C or A is needed.
• IsConsistent.exists_pmf_subsample_toOuterMeasure_le (for 0 < m): minimax (Probability/Minimax.lean) turns this into a single distribution on subsamples that is wrong at each example with probability at most ε.

This is mathematical progress toward #4914 but not the scheme itself. The remaining milestone (M3(c–d)) samples a few subsamples whose majority vote is right everywhere. That needs ε-approximations for the dual class (M2, after #4945) and Assouad's bound (#5029).

Validation: lake build --wfail --iofail of the new module, the new test CslibFrontierTests/VCCompression.lean with warnings as errors, lake exe mk_all --check, lake lint on the module, hygiene --check-simp, the encoding and projection-chain ratchets and the manual checker all pass locally. CI covers the rest.

Manuals: the Operator's Manual gets one paragraph in learning-and-testing.md. The Agent Operator's Manual needs no change because there is no workflow or tooling change.

Implemented by a Jetski AI agent as worker compression under coordinator session 5f40c2da.

[SamuelSchlesinger]

Reviewer review-a (Jetski swarm, coordinator session 5f40c2da; non-author agent review, not human review) at a6edeb9 (delta over #5029's f5b8120): APPROVE, with one locator check to fold into the retarget push

What is proved. Fix a consistent learner A for C reading s ≥ vcSampleSize d ε δ examples, with δ < 1. For every sample S that C realizes and every q : PMF (Fin m), some b : Fin s → Fin m has q{i | A (S ∘ b) wrong at i} ≤ ε. For 0 < m, some μ : PMF (Fin s → Fin m) is wrong at each example with probability at most ε. This is a milestone toward the Moran–Yehudayoff scheme, not the scheme itself; the PR body and the manual both say so.

Proof. I checked the first theorem.

• The traces C' = {c ∘ x} on Fin m inherit the shattering bound through #5029's card_le_of_comp.
• A' composes A with the sample points, and it is consistent for C'.
• D = (q.map fun i => (i, y i)).toMeasure is realized by c₀ ∘ x.
• On the a.e. set where every drawn example carries S's label, A' T = A (S ∘ T.1) ∘ x. So if every b failed, the bad set would have full measure, 1 ≤ ofReal δ, which contradicts δ < 1.

Fin m is discrete, so no measurability hypothesis is needed. The second theorem applies the existing Yao/minimax lemma PMF.exists_forall_toOuterMeasure_le with I = Fin s → Fin m, nonempty because 0 < m, and finite J = Fin m, and converts between ofReal and toReal correctly. Both theorems reuse existing APIs: the VC upper bound, minimax, and toOuterMeasure_ne_top. Nothing is re-proved. The test is non-vacuous: thresholds, a concrete two-point sample, and the explicit sample size.

Please check before merge. The docstrings cite "[MoranYehudayoff2016, proof of Theorem 1.3]". In the paper, Theorem 1.3 (size exp(O(d))) follows from Theorem 1.4 (size O(d* d log(d* d)) in terms of the dual VC dimension) together with Claim 1.5. As far as I can tell the weak-learning and minimax steps are in the proof of Theorem 1.4. I only confirmed this from a secondary summary, so please check it against arXiv v2. If it is Theorem 1.4, fix it in the push that retargets this PR to main after #5029 lands; I will review that delta anyway.

Non-blocking:

1. card_le_one_of_setShatters_thresholdClass is now copied in two test files (DualVCDimension and VCCompression). It is the hC form every finite-VC client of the thresholds needs. A public lemma next to not_setShatters_thresholdClass in OnlineLearning/MistakeBound/Thresholds.lean would let both tests use it.
2. The statements use only Mathlib's PMF/toOuterMeasure. If public import CslibFrontier.Probability.PMF exists only for proof-time lemmas, a plain import keeps the PMF hub out of this module's public interface.

Manuals: the Operator's Manual paragraph describes the actual API and states the remaining step. The Agent Operator's Manual needs no edit.

The PR is stacked on #5029, so queueing waits for #5029 to land, the retarget and merge of main, and ci-checks at that head.