[heathsanchez]

Scope (draft — not an Arena submission)

Compose six individually qualified upstream-motivated soundness fixes against the exact published Flash source commit 78c7502bac8a5ba000057b3f083bc0595ac65750.

Existing false ACCEPT	Underlying issue	Isolated qualification
nested recursor fields	ammkrn/nanoda_lib#63	run #41741166812
inductive universe scope	ammkrn/nanoda_lib#79	run #41742165125
nested temporary-name capture	ammkrn/nanoda_lib#74	run #41742547106
closure universe substitution / Pi closure context	intgrah/sokonanoda#8, #9	run #41743040598
nullary recursor rule	intgrah/sokonanoda#7	run #41743377323

Each individual patch flipped its target forged export(s) from false ACCEPT (exit 0) to REJECT (exit 1), while preserving the other 178 or 177 official small-test verdicts. This does not imply combined qualification.

This PR's independent gates

1. Build published baseline and stacked candidate with identical release flags.
2. Pin the official Arena corpus SHA-256 and require six specified false-ACCEPT corrections, preserving 173 other small-test verdicts.
3. Retrieve separately archived, SHA-pinned full Mathlib NDJSON (109,790,519 records); run matched published-vs-stacked A/B/B/A with exit codes, wall, peak RSS and source/binary hashes. Preserve negative and UNKNOWN results.

Boundaries

• Do not merge or publish this as a soundness release until CI finishes and its evidence is reviewed.
• No precomputed acceptance, no bypass, no change of axioms or source semantics.
• Changes derived from/upstream-motivated by the linked authors; no independent-origin claim.
• Other known false REJECT and independent Nucleus completeness remain separate residuals.
• No private collaboration notes in this public PR.