feat: add milestone challenges and a reader-facing audited catalog

[PerAlexandersson]

User-requested high-level challenge and public-progress surface, stacked on CI-first PR #603 (retarget to main after that PR is integrated).

Adds three focused challenge facades: ordinary stable homogenization, general totally nonnegative principal interlacing including singular matrices, and the proved PF-multiplier exponential-generating-function/real-zero branch of Pólya–Schur. These are direct wrappers of existing checked library theorems, not new mathematical proofs. Includes ten curated entries in milestones.json and generated MILESTONES.md with explicit scope and conditional/open labels. Braun–Jal retains its external model-input boundary; the full analytic Pólya–Schur classification is still open.

CI checks catalog consistency, then after the ordinary full build checks all 17 witnesses are theorem declarations and audits their transitive axioms. Only propext, Classical.choice and Quot.sound are allowed. Missing/duplicate results and non-theorem definitions fail. A revision-stamped milestone-audit JSON artifact is suitable for a future web page. This does not add independent Comparator coverage or deploy a new site.

Locally verified without Lean: 12 Python tests, catalog regeneration/check, root/Production registration, exact import-closure budgets (+3), proof-status guard, generated tactic coverage and git diff --check. No local Lean/Lake/AXLE/Aristotle run; awaiting remote compilation and axiom audit. Source metadata alone is not a fresh proof audit. No default-branch push or merge.

[PerAlexandersson]

Review checkpoint: latest head f8a611e hardens metadata object shapes, matches declaration namespaces to their challenge entry points, and handles apostrophes in axiom output. All 17 source-only tests and the 10-entry catalog check pass. A separate Luna review checked all 17 current witness declarations against their listed source files. This remains a curated catalog: English scope and physical source provenance require review, and independent Comparator coverage is not inferred.

Remote full build and the configured three-theorem Comparator re-check passed at ddc159e (run 34640145493). Latest-revision CI and the separate 17-witness transitive-axiom audit remain pending; that earlier success is not claimed for f8a611e. No local Lean/Lake/prover/compiler was run. This PR remains stacked on #603; retarget and recheck after the CI base is accepted.