[SamuelSchlesinger]

Moves thresholdClass_subset_lowerSetClass out of PACLearning/Compression/Order.lean and into a new small module, PACLearning/Compression/Thresholds.lean. Order.lean public-imported OnlineLearning/MistakeBound/Thresholds (and through it SOA and the VC-dimension modules) only for this one lemma. Now the order schemes no longer depend on the online development, and only clients that want the bridge import it. This was review-a's placement nit on #4947.

The new module also states isPACLearnable_thresholdClass: the thresholds x < θ on ℕ have infinite Littlestone dimension, yet they are PAC learnable through the size-1 scheme. The online threshold module's docstring already claimed this; it now names the theorem. The test file, the Operator's Manual paragraph and CslibFrontier.lean are updated. No statement changes, and no other clients exist.

Progress type: refactoring (module placement), plus one PAC corollary for an existing class.

Validation

lake build --wfail --iofail of Compression.Thresholds, Compression.Order and Compression.MistakeBound; CslibFrontierTests/SampleCompression.lean with warnings as errors; lake exe mk_all --check; lake lint on the three changed modules; scripts/check_hygiene.py --check-simp; the encoding readability and projection-chain ratchets; scripts/check_operator_manual.py. Full validation: CI.

Manual impact

• Operator's Manual: the compression paragraph in Distribution-free realizable PAC learning now links the new module and names isPACLearnable_thresholdClass.
• Agent Operator's Manual: no change, because no workflow or procedure changes.

Follow-up to #4947; part of #4914.

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 b9591e7: APPROVE

This resolves my placement nit from #4947. Compression/Order.lean no longer imports OnlineLearning/MistakeBound/Thresholds, which also pulled in SOA and the VC-dimension modules. After this change Order uses nothing from the online development. The bridge's name stays Cslib.MachineLearning.PACLearning.thresholdClass_subset_lowerSetClass, with the same namespace and statement, so the only clients, the test and CslibFrontier.lean, need nothing beyond the new import.

isPACLearnable_thresholdClass is a one-line application of the existing ofSubset/isPACLearnable/measurableReconstruction_of_countable API. The online threshold module's docstring previously claimed this result without naming it; it now names it. A second route exists through vcDim_thresholdClass and the finite-VC upper bound, but no library theorem states this yet. The tests have only examples, so this is not a duplicate. The new module is small, imported only by the clients that need the bridge, and has the usual header, -- upstream: candidate and a docstring with Main results.

Manuals: the Operator's Manual compression paragraph now links Compression/Thresholds and names both declarations. The Agent Operator's Manual needs no edit, because no workflow changed.

Queueing waits for ci-checks and its notices.