[kim-em]

Generated challenges explicitly imported Lake.Toml, Lake.Util.Message, and Lean because EvalTools.Markers exposed those implementation dependencies. This broke consumers that reuse challenges, including Comparator's finite graph Ramsey preset.

Source modules still receive these implementation dependencies transitively through the marker implementation; the standalone generated headers now omit them.

Keep the compatibility marker module limited to LeanEvalGenerator.Core.Markers, which the generator already omits, and regenerate all 312 workspaces. This removes the accidental imports from 499 files across 307 workspaces. Add regression checks for marker-only modules and the narrow Ramsey import header. Rename an implicitly used commuting-probability binder to clear an existing linter warning in its generated solution wrapper.

Validation:

• All 137 generator unit tests pass.
• All 307 affected workspaces compile with warnings treated as errors, excluding intentional sorry holes; the commuting-probability wrapper also passes after the binder fix.
• Full source compilation and declaration inventory validation pass.
• For the two Init-only workspaces, source/generated statements, 172 declaration types, and 68 definition values are definitionally equal.
• All regenerated Lean files match the compiled snapshot; generated catalog validation and git diff --check pass.