Fix course validation and progress tracking

[SamuelSchlesinger]

Summary

• give exercises stable dir/name identities, reject ambiguous bare names, and migrate legacy progress conservatively
• strengthen intro hidden checks and execute IO exercises against exact expected output
• make verify fail when any exercise is incomplete, narrow analysis claims to the proved theorem boundary, and add regression coverage in CI

Why

The analysis course reused several bare exercise names across worlds. Progress keys and lookups used only those names, so one completion could count twice and later exercises could be silently skipped. Several intro validators also checked only part of their stated tasks, and IO exercises were never executed. Finally, verify always exited successfully and the analysis prose overstated the formalized structure.

Impact

Existing progress remains compatible and is upgraded in memory on load. Unique bare names still work; repeated names now require the qualified names shown by the CLI. Incorrect intro implementations and silent IO programs are rejected, while automation can rely on verify's exit status.

Validation

• lake build (257 jobs)
• lake env lean --run tests/LeanlingsRegression.lean
• all 70 intro reference solutions against hidden checks
• exact output checks for both intro IO solutions
• adversarial regression cases for the formerly permissive validators
• isolated incomplete verify run returned exit status 1
• git diff --check