Require complete project-root indexes in module-system packages

[Vilin97]

Now that #559 migrated every project, make the project-root layout mandatory for module-system packages. The quality gate and local mk_all must reject a flat LeanPool.lean even if every Imports.lean is deleted, and regenerate exactly one complete public aggregate per project. Keep independent legacy non-module fixtures supported; fix the rebase fast-path fixture to use valid TOML.

Validation: 561 Python tests passed (2 unrelated optional skips), including deletion of all aggregates, complete public export compilation, stale/missing/duplicate/private/cross-project imports, collision safety and mechanical rebase conflicts. Ruff, formatting and lake exe mk_all --module --check passed. The complete content migration passed whole-tree static quality checks before merge. No formalization sources, thresholds or branch protection settings change.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk] Enforces stricter module indexing rules in the build system.

The PR appears safe to merge; no actionable regression was identified.

Summary

This PR makes project-root aggregates mandatory for module-system packages while preserving flat indexes for non-module fixtures.

• Enables the Python index gate to recognize requiresModuleSystem = true even when every project aggregate has been deleted.
• Gives the rebase fast-path fixture valid TOML so the new configuration check can read it.

_{Reviews (1) · Last reviewed commit: "Require complete project-root indexes in..."}