Add permanent module-surface regression gates

[jagg-ix]

Scope

Completes the next ten zil-lean-only targets from zil-engine-modularization-plan.md as permanent regression gates rather than one-off commands.

1. build Zil.Engine.Query
2. build Zil.Engine.Provenance
3. build Zil.Impact
4. build Zil.ProofObligation
5. build Zil.TheoremAudit
6. build Zil.QueryGovernance
7. compile a module-system consumer importing all six surfaces
8. compile a legacy non-module consumer importing the same module files
9. recompute and audit the real import closure, public-import visibility, and module-to-module direction
10. build the complete package

Files

• .github/workflows/module-surface.yml
• scripts/check_module_closure.py
• scripts/probes/ModuleSurface.lean
• scripts/probes/LegacyModuleConsumer.lean

Closure audit

The audit starts from the live engine and governance seeds, follows actual Zil.* imports, and fails on:

• a missing source file;
• a reachable file that does not begin with module;
• a module-to-non-module dependency;
• a ZIL dependency lacking public import visibility;
• omission of any file from the original 16-file engine closure; or
• omission of any of the four Phase-2 governance modules.

It prints the recomputed module count, ZIL import-edge count, LOC, and sorted closure so future drift is visible.

Validation

The new Module surface regression workflow passed all ten steps on this PR:

• six individual engine/governance builds;
• module-system consumer probe;
• legacy non-module consumer probe;
• dynamic module-closure audit; and
• complete lake build.

This converts the modularization plan's manual definition-of-done commands into standing repository regression gates.