conway-refinement

Summary make the chapter introductions match the exact Lean hypotheses, zero cases, and transfinite-induction route correct the corresponding Lean module documentation and the affected blueprint annotation statement keep the PR confined to mathematical descriptions; no renderer, provenance, build-pipeline, or Mantova-guide changes The one-off Mantova proof-outline PDF is not included. Verification

Palomar brings its own official SubVerso dependency. The main project was also bringing a modified SubVerso fork with the same package name, so Palomar stopped before it could render the challenge. This keeps the modified fork in a small, separate Lake project used only by the proof guide. The main mathematical project no longer exposes SubVerso to Palomar, while the proof guide keeps the semantic proof-state features it needs. Checked locally: the full Lean project builds all repository audits pass the separate proof-state extractor builds the extractor successfully reads a real project module the blueprint consistency check passes The complete proof-guide extraction was left for CI as requested.

Palomar could not find a complete Mathlib cache for our Lean 4.31 RC2 dependency. This moves Lean and Mathlib to the final 4.31 release. It keeps the current CombinatorialGames commit, which still compiles against the final release. Tested locally: the full 3,145-job Lake build all Lean audit executables the isolated SubVerso blueprint extractor all 8,542 Mathlib cache files downloaded with none missing