fix(ci): declare the Lean update output the evidence guard reads

[bordumb]

Summary

actionlint .github/workflows/ci.yml reported two expression errors on main. Both are fixed; actionlint is now clean on every workflow.

1. Dead evidence guard. formal evidence skips aggregation when needs.formal-lean-authoritative-run.outputs.update_required is 'true', but formal Lean authoritative never declared that output. An undeclared output reads as empty, so the guard passed on every run. When the Lean job packaged an assurance-manifest update on a pull request it still succeeded and skipped its phase-result upload, and formal evidence then failed with the misleading "Missing same-run lean evidence artifact".
   • The Lean job now declares update_required from its formal-update step.
   • It also fails after preserving the update (new step "Stop qualification until the assurance update is committed"), as formal translation already does, so the job that found the drift is the red one.
2. Dead output on repository preflight. It declared update_required from a formal-update step it does not have, left over from 930a74e. Nothing reads needs.repository-preflight.outputs.update_required, so the output is removed.

Pending assurance update on a PR, before and after

Job	Before	After
formal Lean authoritative	success (update uploaded, no phase result)	failure at the stop step, after the update is uploaded
formal evidence	runs, fails on the missing Lean artifact	skipped (Lean result and the now-live guard)
formal-translation gate	failure	failure (required, evidence skipped)
CI qualified	failure	failure
Formal artifact updater	commits the update	unchanged: it keys off the auths-formal-update-<run>-<attempt> artifact and a successful formal-update preflight, not Lean job status

Validator

validate_ci_workflow_gates in xtask/src/formal_qualification.rs now requires the Lean job's job-level outputs: to bind update_required to its own formal-update step, and requires the stop step gated on that output. Fixture tests cover the output removed, the step id removed (the repository-preflight shape), and the stop step removed. The authoritative Lean job runs this validator against the committed ci.yml.

Generated artifacts

• formal/qualification/aeneas/source-closure.json: regenerated for the formal_qualification.rs change (ci.yml is not in the closure).
• formal/assurance-manifest-v1.toml: the 17 source-closure evidence digests rebound to the new file's SHA-256. Per-claim semantic closures are Lean-only and unchanged.
• release/semantic-freeze-versions.toml and release/semantic-freeze.json: freeze_version, auths.release.evolution-contract, auths.release.public-surface, and the source-closure and assurance-manifest frozen-bytes entries each move one version past main. cargo xtask semantic-freeze --update converged in one pass.
• docs/PROGRAM_BOARD.md: section 4 logs the delegated fail-explicitly decision.

Overlap with #174

#174 also edits ci.yml, formal_qualification.rs, the manifest, the source closure, the freeze files, and the board. The hand-written edits sit in different hunks; the generated files will conflict and must be regenerated on whichever PR lands second.

Verification

Run locally only because the change needed them: actionlint .github/workflows/*.yml (clean), cargo xtask semantic-freeze (passed, 63 entries), and a byte-identical reproduction of the source closure.

The first hosted run failed authoritative implementation on four formal_qualification fixture tests: the fixture's new stop step ended at its condition line, and workflow_job_source drops the newline before the next job, so the exact-condition needle missed. The committed workflow was never affected, because a run: line follows the condition there. The fixture now has that line (e4a32d4), and only that failing check was reproduced locally: the 20 formal_qualification tests pass.

Main (#173, #176) is merged in (abae197); its generated files conflicted, so they take main's versions and are regenerated for this branch. Hosted CI on the new head is the verification.