Check lean: targets, non-root axioms and a kernel replay in the CI audit

[Deicyde]

Stacked on #115: the base is open-statements-revision, so the diff is this PR's commit only. Retarget to main once #115 lands.

This fixes three gaps from the #115 contract audit that already exist on main: H1, the first half of H4, and the first half of H6. They are kept out of #115 so it stops growing.

What was wrong

• H1. Strict CI never checked that an article's lean: name was compiled. A sorry'd theorem in a file no target imports, after #exit, or inside a string passed the lexical autoform check --lean-root and showed as fully proved. Open statements and a revision contract for shared Lean declarations #115's open-statement probe checks this; the strict path did not.
• H4, first half. A lean: name outside the root package, as a Mathlib article's is, got only a sorry check (open policy) or no check (strict).
• H6, first half. collectAxioms trusts whatever the environment holds, and a root run_cmd can add a declaration with kernel checking off.

Changes

• autoform-verify.yml writes the autoform work assumptions contract under both policies. The strict branch passes it to .github/autoform_audit.py with the new --targets form.
• The strict loader shares the open loader's validation. It refuses a contract that allows open statements, marks an article open, or lets one assume an open statement.
• The strict probe embeds the targets as one JSON string and reports a missing name with the open probe's text: NAME [ID] is not a declaration of the Lean build; fix the article's lean: name or build the module that declares it. Its new helpers are guarded against imported shadows.
• Both probes apply the unsafe/partial check and the axiom allowlist (propext, Classical.choice, Quot.sound) to a lean: name outside the root package. The open probe keeps its sorry message there.
• Both probes replay the root package's constants through the kernel with Lean.Environment.replay, on top of a fresh importModules of the other imported modules. They fail with kernel replay of the root package failed: ... when it throws.
• The old three-argument form still runs the strict audit, without the target check, so an older workflow keeps working with a newer script.
• The README documents --targets, the AUTOFORM_REF requirement now that the strict path calls work assumptions, and what the replay does not cover.
• The template and the Cabannes example copy of the script and workflow stay identical, apart from the pin lines.

Tests

New in tests/test_lake_artifact_audit.py:

• test_target_contract_lists_each_strict_article_declaration
• test_target_contract_refuses_anything_but_the_strict_policy
• test_strict_probe_embeds_its_targets_and_guards_its_helpers
• test_strict_probe_requires_every_target_and_checks_non_root_ones
• test_strict_probe_refuses_a_helper_name_an_imported_module_declares
• test_open_probe_checks_the_axioms_of_a_target_outside_the_root_package
• test_both_probes_replay_the_root_package_through_the_kernel

Local runs at 8958f94:

• ruff check autoform_cli servers tests: clean.
• Real Lean (AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1), tests/test_lake_artifact_audit.py tests/test_impact.py tests/test_contract.py: 149 passed, 1 skipped. The skip is test_helper_runs_on_python_310, because python3.10 is not installed on this machine. I ran this at 562cd59, which differs from 8958f94 only in a README reflow.
• Full suite without Lean: 1264 passed, 49 skipped, 4 failed. The 4 failures are the tests/test_scaffold.py pin tests. They fail only because my local clone has no origin remote, so plugin_pin() finds no pin. In a clone with origin they pass (63 of 63), and they pass in CI.

Caveats

• This breaks the Cabannes example's strict CI until its pin moves. The strict path now runs autoform work assumptions from AUTOFORM_REF. The example pins c994d83, which predates that command, so a project that takes this workflow at that pin fails at that step. The pin can only move to a main commit that has work assumptions, which means after Open statements and a revision contract for shared Lean declarations #115 lands.
• The replay's memory and time cost on a large project has not been measured; the test fixtures are small.
• The strict failure summary still reads root-package declarations failed the kernel-trust audit when the failure is a missing or non-root lean: name.
• H6's second half stays open. Build-time IO, such as a root module's initializer or a run_cmd during lake build, can rewrite the audit script, the workflow's inputs, or the blueprint before the audit reads them. Closing that needs a separate audit job that runs no project code, plus CODEOWNERS on roadmap/README.md and .github/.
• Whether workers are trusted is still an open decision (D4 in the contract audit), so this PR changes no governance. The README records the gap.

[Deicyde]

Two blockers before this is reviewable:

1. The PR is based on closed, unmerged Open statements and a revision contract for shared Lean declarations #115. Its unique commit genuinely depends on the cleaned open-statement layer, so please replay it onto Add opt-in open statements and conditional proof status #138 rather than retargeting the existing history. Preserve Add opt-in open statements and conditional proof status #138's final status-line/error-suppression documentation when resolving the README conflict.
2. The generated example workflow now calls autoform work assumptions, but its AUTOFORM_REF remains c994d83, which predates that command. The example's strict CI therefore fails by construction. Move the pin only after the required command is present on a landed main commit, and rerun the exact restacked head.

The target/audit/replay direction is otherwise distinct from #138 and worth retaining.

[Deicyde]

Re-review at 348d4561: the new fallback prevents old pins from crashing, but it deliberately runs the legacy three-argument audit and therefore skips this PR's new lean: target guarantee. The example still pins c994d83, and the body still says it breaks.

The larger blocker is unchanged: this remains based on closed #115, not rebuilt #138. Replaying the two unique commits onto #138 conflicts in the README exactly where #138 suppresses clean-looking status for failed/reaching-failed declarations; preserve that wording. Then land/pin the new CLI, remove the legacy gap, refresh the body, and rerun CI on the valid base. The target/non-root/replay implementation itself remains sound.

[Deicyde]

Replaced by #156, which carries this PR's two commits onto main. This PR's base, open-statements-revision, will not merge now that #115 has landed on main in split form (#138, #150). The CODEOWNERS template and the write-up of the remaining audit gap are in #157, stacked on #156.