feat(EvalTools): fail validation on problem modules no manifest reaches

[kim-em]

This PR makes validate-manifest fail on any problem module the manifest cannot reach. It parses the header of every .lean file under LeanEval/ and rejects the ones that are neither named by some manifest module field nor imported, directly or transitively, by a module that is. manifests/problems/*.toml is CI's only entry point into the problem sources, so an unreached module is never compiled and never validated: a new problem can be added with a broken statement and CI stays green. The check parses imports rather than building anything, so it costs no build time and runs before the inventory cross-check.

Two smaller guards come with it. loadManifest now rejects non-.toml files in manifests/problems/ instead of skipping them silently, which is what let #513 land a manifest named direct_summand.lean and take its module out of the build with it; dotfiles are still ignored so a stray .DS_Store cannot wedge CI. And a manifest entry whose module names no file under LeanEval/ is now reported as a typo rather than surfacing later as an unrelated-looking unreachable-module error.

main passes the new check as-is: 245 manifest entries name 229 of the 237 modules under LeanEval/, and the other 8 are imported by modules that are.

Fixes #519.

🤖 Prepared with Claude Code

[kim-em]

Second-opinion review (Codex) turned up three real gaps, all now fixed in 28332a0:

• Module identity was concatenated text. LeanEval/Foo/Bar.lean and LeanEval/Foo.Bar.lean both flattened to LeanEval.Foo.Bar, so a manifest entry for the nested file vouched for a sibling Lake never builds — the exact false negative this PR exists to close. In the other direction, import LeanEval.«Foo-Bar» failed to match LeanEval/Foo-Bar.lean and reported a false orphan. Coverage is now keyed on Lean.Name, built from path components, with manifest module fields read through a shared parseModuleName that eval_inventory also uses, so the check and the inventory cannot disagree about which file a module field names.
• Skipping dotfiles reopened the hole. The @[eval_problem] elaborator reads every *.toml in manifests/problems/ independently of loadManifest, so a hidden .foo.toml could satisfy the attribute for a declaration that never reached the catalog. The exemption is now .DS_Store alone.
• The walk followed directory symlinks. A link duplicates a subtree under a second module prefix, or points at an ancestor and recurses forever. Symlinks under LeanEval/ are now rejected with a clear error.

Tests grew to 13, covering each case. main still passes the check unchanged (245 manifest entries, 237 modules), and both negative cases still fail as expected — including LeanEval/EasyProblems.Extra.lean, now correctly reported as LeanEval.«EasyProblems.Extra».