Fix quoted Lean module path resolution

[kim-em]

Summary

• parse rendered Lean names component-by-component so dots inside guillemet-quoted identifiers remain data
• use the same semantic components for manifest names, source paths, ilean paths, declaration suffixes, and generated helper namespace prefixes
• cover the real Formal Conjectures shape FormalConjectures.Arxiv.«0912.2382».CurlingNumberConjecture
• mirror the path rule in the byte-golden harness and exercise the generator schema version 1 JSON context lookup

This fixes the quoted-module-path issue reported while integrating the FC100 importer in google-deepmind/formal-conjectures#4951. It does not change the frozen generator schema version 1 request/response contract.

Verification

• lake build
• lake build test_module_paths
• lake env .lake/build/bin/test_module_paths
• python3 tests/scripts/contract.py
• python3 tests/scripts/golden.py /home/kim/worktrees/lean-eval-overhaul/kernel-shadow-benchmark
  • two_plus_two: 10 files byte-for-byte
  • noncomputable_hole_example: 10 files byte-for-byte
• python3 -m py_compile tests/scripts/*.py
• actionlint .github/workflows/ci.yml
• git diff --check

Contract note

The scanner consumes module/declaration names that Lean has already accepted; it intentionally does not claim to be a replacement Lean identifier parser. Quoted components may contain dots and an inner opening guillemet, while the closing guillemet terminates the component quote as specified by Lean's module/name syntax.

[kim-em]

Integration check: I applied #1 and then this PR to a fresh a726789 worktree. Both cherry-picks applied without conflict. The combined tree passes the full build, the active-option regression invoked by the JSON contract, the quoted-name executable, strict contract tests, both 10-file byte-golden fixtures, Python bytecode, actionlint, and diff checks. So #1 can merge first without a semantic integration problem; I will rebase this branch onto the resulting main commit if GitHub requires it.

[kim-em]

The combined #1 + #2 generator has now passed the complete FC100 gate at formal-conjectures#4951 head 54abfe5: 100/100 import/verify/generate and 98/100 target compilation, with only the two pre-existing cross-pin drift cases. Both real quoted Arxiv modules compile. Report digests and full details are recorded in the linked FC PR and lean-eval tracker.

[kim-em]

Pre-review cleanup a114d8a clears all Ruff findings in this PR’s touched Python harnesses (stale shebang/executable mismatches, import ordering, and the explicit stdout/stderr pipe form). The quoted-name implementation is unchanged. lake build, dedicated module-path executable, strict JSON contract test, Python bytecode, Ruff, actionlint, and diff checks pass; #1 plus #2 plus the new inline-scoped-command regression also compose and pass locally at combined commit 28f767a.

[kim-em]

Fresh post-cleanup golden parity also passed against clean LeanEval 21c6c02178e14cccc54b6e90e4836d1ca0e9c7e6: two_plus_two 10/10 files and noncomputable_hole_example 10/10 files match byte-for-byte. The disposable verification worktree was then removed.