proofs.yml lean-build is red on main: lean-action's nanoda step cannot build lean4export under the v4.16.0 toolchain #104

Observed on PR #102 and already red on main (same failure on PR #101's head: https://github.com/hyperpolymath/trope-checker/actions/runs/40391430747).

What happens (run https://github.com/hyperpolymath/trope-checker/actions/runs/40472568287, jobs "Lean grade-boundary" and "Lean grade-factorisation"):

1. lake build succeeds for both packages — "Build completed successfully" — and prints the axiom line for every audited theorem.
2. leanprover/lean-action@v1.6.2 then runs the optional nanoda external checker (nanoda: true, nanoda-allow-sorry: false in the job). Its bundled lean4export is compiled with the project toolchain leanprover/lean4:v4.16.0 and does not compile there: Std.HashMap.emptyWithCapacity, Lean.NameMap.alter/get?, Array.toJson, String.ofList are unknown — APIs newer than v4.16.0. nanoda check failed → job red.
3. Because of (2) the action's own axiom-audit step is skipped, so the sorry-free environment check the job is named for never runs (the per-source lean-source-honesty regex job still does, and is green).

Why it matters: the Formal-proofs gate is red for a tooling reason, so a real Lean regression would be invisible; and the axiom audit, which is the job's point, is skipped.

Also surfaced by the same log: three theorems depend on Classical.choice in addition to propext/Quot.sound — Trope.nine_families (EffectAtoms.lean), FateA.Q_add_left_cancel and FateA.atten_cancel_on_normalForms (GradeRatified.lean). The status surfaces that said "propext/Quot.sound only" are corrected in #102 to "no sorryAx, no user axiom". Classical.choice is a standard Lean axiom, not a hole; the point is that the surfaces now match the audit.

Options (owner's call; not changed in #102, which only reports):

• (a) Pin the toolchain and nanoda to compatible versions (nanoda/lean4export at a tag that builds under v4.16.0, if one exists), or bump lean-toolchain + Mathlib rev together so lean4export compiles — the latter is a real proof-maintenance step.
• (b) Set nanoda: false and rely on axiom-audit plus the regex gate — weaker (one checker fewer) but honest, and it makes the job's red mean something again.
• (c) Make the nanoda step continue-on-error so axiom-audit runs — hides the tooling break; least preferred.