Enforce project entry imports in LeanPool root

[Vilin97]

Summary

• require every LeanPool/projects.yml entry_module to be a direct import of LeanPool.lean
• add a regression test proving transitive reachability is insufficient
• document the new repository quality gate

Why

The generated root already directly imports all 145 registered projects, but that invariant was only implied by the all-files generator plus the generic reachability check. A registry-specific check gives future project PRs a precise failure and the exact remediation command.

Impact

There are no Lean content changes and no current name clashes. The existing aggregate lake build LeanPool remains the whole-pool collision gate.

Validation

• cd python && uv run --group test pytest -q — 328 passed
• cd python && uv run ruff check
• cd python && uv run ruff format --check
• lake exe mk_all --check — no update necessary
• current base's Lean Action CI successfully built the aggregate LeanPool root

[github-actions]

LLM review skipped: PR touches no .lean files. Push a Lean change or comment /review after one lands to re-trigger.

[greptile-apps]

Greptile Summary

The PR adds a repository quality check requiring each registered project entry module to be imported directly by LeanPool.lean, along with regression coverage and documentation.

• Adds _check_project_entry_imports to project metadata validation.
• Tests that transitive reachability does not satisfy the direct-import requirement.
• Documents the new repository quality gate.

Confidence Score: 4/5

The missing-root path should be fixed before merging because the new quality gate can silently accept a repository without LeanPool.lean.

The direct-import check correctly handles present aggregate roots, but its missing-file early return leaves the stated invariant unenforced in a concrete repository state.

Files Needing Attention: python/lean_pool/quality.py

Important Files Changed

Filename	Overview
python/lean_pool/quality.py	Adds the direct-entry import check, but silently skips enforcement when LeanPool.lean is missing.
python/tests/test_quality.py	Adds focused regression coverage for transitively reachable project entries, but does not cover a missing aggregate root.
.github/CODE_QUALITY.md	Accurately documents the intended direct-import invariant.

_{Reviews (1): Last reviewed commit: "Enforce project entry imports in LeanPoo..." | Re-trigger Greptile}

[greptile-apps]

Missing root bypasses import gate

When LeanPool/projects.yml registers projects but LeanPool.lean is absent, this branch returns no errors, causing the quality run to accept an aggregate root that imports none of the registered entry modules.

Suggested change

	if not index_path.exists():
	return []
	if not index_path.exists():
	return [
	_QualityError(
	index_path,
	1,
	"LeanPool.lean is missing; run `lake exe mk_all`",
	)
	]