Deploy Pages only after autoform verify passes, and refuse a lean: name defined twice

[Deicyde]

Status: obsolete-base draft; do not merge or mechanically retarget. #115 closed unmerged, and this head still has source-selection and workflow-trigger/concurrency blockers. Rebuild Pages gating (#169) and duplicate-source validation (#170) as separate current-main PRs after #165, then close #140 as superseded.

Historical note: this was drafted as two commits on #115. That base closed unmerged; preserve the design record here and rebuild the unique work as described above.

This fixes two gaps from the #115 contract audit that already exist on main: H3, and the second half of H4.

What was wrong

• H3. blueprint-pages.yml deployed on every matching push to main without waiting for autoform verify. The public site could therefore show a theorem as fully proved for a commit whose build or audit failed.
• H4, second half. The Lean source index kept the first lexical definition of each name. When an unbuilt draft file repeated a built declaration's full name, the site linked the draft, CI built and audited the other declaration, and check passed.

Changes

• Pages now runs on workflow_run of autoform verify. It builds and deploys only when that run succeeded for a push to main from this repository. A fork's pull request can carry head_branch: main, so the event and the head repository are checked too.
• It checks out the verified commit and passes it to render --ref. Under workflow_run, GITHUB_SHA is main's current head, so without this the permalinks would point at a different commit.
• Pull requests still build without deploying, and workflow_dispatch now does the same. A maintainer redeploys by re-running the latest verify run on main.
• The source index also records every definition of a name that resolves to more than one declaration. check --lean-root fails, listing each path:line, when an article names such a name. The Pages workflow runs that check before rendering, so the deploy stops too.
• A private declaration counts by the name its source writes, as work impact resolves it. Two private ones with no public one are ambiguous. A public one and private ones in other files are distinct in Lean, so they are not.
• Which declaration find returns is unchanged, and render, audit, doctor and skeleton keep using it.
• The README, the Setup skill, and the example copy of the workflow are updated. The template and the example stay identical apart from the pin lines.

Tests

New:

• tests/test_graph.py::test_check_cli_refuses_a_lean_name_defined_more_than_once
• tests/test_lean_sources.py::test_a_name_defined_in_two_files_keeps_the_first_and_records_both
• tests/test_lean_sources.py::test_the_same_short_name_in_two_namespaces_is_not_a_duplicate
• tests/test_lean_sources.py::test_private_names_collide_only_when_no_public_one_wins

tests/test_skill_examples.py checks the new Pages triggers and conditions in both workflow copies.

Local runs at a5fec94:

• 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: 136 passed, 1 skipped. The skip is test_helper_runs_on_python_310, because python3.10 is not installed on this machine.
• Full suite without Lean: 1259 passed, 45 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

• The workflow_run trigger and its conditions have not run on GitHub. They cannot be exercised locally, so the first verified push to main in a project that takes this workflow is the first real test.
• workflow_run has no paths filter and verify runs on every push to main, so every verified push redeploys, even one that changes nothing the site shows.
• A project that takes this workflow stops deploying from commits whose verify run fails, which is the point. A project with a red main therefore keeps its last verified site until main is green again.

[Deicyde]

This needs changes before review:

1. It is based on closed, unmerged Open statements and a revision contract for shared Lean declarations #115. The two unique commits apply cleanly to current main, so rebuild them there; consider separating Pages gating from source-index duplicate validation because they have independent risk and rollback surfaces.
2. The duplicate resolver can select the wrong declaration. When an earlier file contains private helper and a later file contains public helper, _ambiguous treats the name as valid but the index still stores same[0]; check passes while render/linking points at the private declaration. Make the public declaration win and assert the selected path/name, not only duplicates == {}.
3. The bundled example remains pinned to c994d83, so it silently executes the old check without this duplicate validation. Update the pin only once the feature exists on landed main, then exercise the generated workflow.

[Deicyde]

Re-review confirms the prior blockers remain at a5fec947: obsolete #115 base, earlier-private/later-public selection still returns the private declaration, and the pinned example never executes the new duplicate check.

The Pages privilege split is otherwise sound, but the rebuild also needs two changes: gate workflow_run by the exact workflow path, not only the display name (a second same-name workflow can satisfy the current guards), and separate deploy concurrency from PR/manual/failed-run builds so those events cannot replace a pending verified-main deployment. Please split/rebuild Pages gating and duplicate validation on current main, then refresh the immutable example pin after the validation code lands.