Forward-port to Lean/mathlib v4.31.0

[gotrevor]

Forward-ports Foundation to Lean/mathlib v4.31.0 (from v4.29.0).

What changed

• lean-toolchain: v4.29.0 → v4.31.0
• mathlib require → v4.31.0; doc-gen4 require → v4.31.0 tag (upstream tracked main — flip back if preferred)
• Source migration across 133 Foundation/*.lean files for the v4.29 → v4.31 API changes
• ~29 instance declarations demoted to def/lemma (e.g. the Sound/Complete instances, buildAxioms.instHasJ*, instRooted, isTree, set_nonempty, set_countable). These were non-synthesizable (explicit non-class hypotheses like (hV : C ⊧* Ax), (ha : a ≠ M.root)) or non-class heads (Set.Nonempty/Set.Countable are Props, not classes), which v4.31's stricter instance check now rejects. None were firing in typeclass resolution, so the demotion is behavior-preserving — flagged here so instance→def in a mechanical port isn't surprising.

Faithfulness

• sorry/admit baseline unchanged at 27, all pre-existing upstream (the heaviest files — ProvabilityLogic/Classification/Result.lean (9) and Modal/Maximal/Makinson.lean (6) — match upstream master exactly). Zero new holes introduced by the port.

Known follow-up — mathlib v4.31 deprecations

The build is green, but emits deprecation warnings (no sorry, no errors — pure hygiene). The port leans on still-working-but-deprecated mathlib API in a few spots. These are deliberately left for a focused follow-up PR to keep this bump minimal and reviewable. Inventory: 122 warning lines → 22 distinct symbols.

• ~19 drop-in renames, dominated by mathlib's relation-predicate refactor: Reflexive/Irreflexive/Symmetric/AntiSymmetric → Std.Refl/Std.Irrefl/Std.Symm/Std.Antisymm; IsRefl/IsIrrefl/IsAsymm/IsAntisymm/IsTotal/IsTrichotomous → Std.*; plus Set.diff_subset→Set.sdiff_subset, Set.Infinite.diff→Set.Infinite.sdiff, Set.insert_diff_singleton→Set.insert_sdiff_singleton, List.max?_eq_some_iff'→List.max?_eq_some_iff, WellFounded.isIrrefl→WellFounded.irrefl, _root_.not_imp→Classical.not_imp, and 3 deprecated module-imports (Mathlib.Data.Finite.Card, Mathlib.Data.Nat.Lattice, Mathlib.Logic.IsEmpty).
• 3 need per-site care: Transitive→IsTrans _ (add the type placeholder), Nat.lt_succ→Nat.lt_succ_iff (confirm same statement), Std.Irrefl.swap→inferInstance (structural, not a rename).

Provenance ⚠️

This is a mechanical port produced with Claude Code, not yet human-reviewed. The tactic-level substitutions (using!, grind→simp, etc.) are written up here: https://github.com/gotrevor/mathlib-bump-cookbook/blob/main/v4.29.1-to-v4.31.0.md — treat it as a starting point, not vetted work.

This PR targets the fork's own master purely so CI can verify the build; it carries only the Lean + lockfile changes (the migration handoff notes live separately on the mathlib-v4.31 branch).