Complete engine and governance modularization

[jagg-ix]

What changed

Completed the remaining Phase 1 engine closure and the next governance targets from the modularization plan.

New module conversions

1. Zil/Core/Declaration.lean
2. Zil/Core/DeclarationSet.lean
3. Zil/Core/Program.lean
4. Zil/Engine/Provenance.lean
5. Zil/Impact.lean
6. Zil/Parser/Tuple.lean — required by the live ProofObligation import graph
7. Zil/ProofObligation.lean
8. Zil/TheoremAudit.lean
9. Zil/QueryGovernance.lean

The tenth completed target is the combined module-import probe over the engine and governance surface.

Each newly converted file now begins with module, uses public import for its dependencies, and exposes the current API through @[expose] public section.

Required correction to earlier conversions

Compilation exposed a flaw in the original mechanical recipe: an exposed declaration cannot depend on a private helper. The first concrete failure was RelExpr.variables depending on private pushName.

This PR therefore promotes helper declarations across the converted closure during the blanket-exposure phase. It also renames the canonical codec's former private nameFromString helper to canonicalNameFromString, avoiding a namespace collision with the attribute codec after exposure.

These changes preserve evaluation, parsing, codec, provenance, and governance behavior. Interface tightening can follow after the module migration is complete.

Validation

The following all passed on Lean v4.31.0:

• individual builds for all nine new module targets
• combined module probe importing:
  • Zil.Engine.Provenance
  • Zil.Impact
  • Zil.ProofObligation
  • Zil.TheoremAudit
  • Zil.QueryGovernance
• complete lake build

The temporary validation workflow was removed after publishing the validated source commit. The final PR diff contains source files only.