Mark landed contribution directions; replace v4.34.0 deprecations in the corpus

[carlok]

Two maintenance commits. Since #216, editing existing modules is maintenance-only, and a maintenance/ PR doesn't go through the receiver. So the second commit's correctness evidence is spelled out below.

1. docs/CONTRIBUTION-DIRECTIONS.md: statuses

• A, B, D and E have landed. Each now names its module and entrypoint.
• C is partly covered: D's specialization proves the trace form, and the general charpoly identity for companion-matrix powers has landed, so C may now be a short corollary.
• H's infrastructure has landed: both path enumerations and the Stern–Brocot interval invariants. The bridge that relates the two path conventions is still open.

Status lines name modules and entrypoints rather than PRs, as the document asks.

@qazW12345: this also covers your #197, #207, #195, #208–#211. One rule change to know about since #186 closed: #216 makes ordinary submissions add-only. Extend an accepted module by importing it from a new one. It also rejects code that runs at build or import time (initialize, run_cmd, simprocs, extern/implemented_by, …). None of your submissions did either.

2. Corpus deprecations under Mathlib v4.34.0

There were 11 deprecation warnings in 8 modules. A later Mathlib will make them errors, and the next upgrade's audit would then fail.

deprecated	replacement	modules
import Mathlib.Data.Real.Basic	Mathlib.Basic.Real.Basic	Nesbitt, SlopeMinorant
import Mathlib.Data.Complex.Basic	Mathlib.Basic.Complex.Basic	InversiveGeometry
if_pos / if_neg	ite_eq_left / ite_eq_right (identical signatures, Init/Core.lean:1179, :1188)	LogisticMap, CircularDominoTilings, SternDiatomic, ThueMorse
Set.mem_setOf_eq	Set.mem_ofPred_eq	Furstenberg

Furstenberg's five haveILetI lints are fixed too (letI → let in proofs of propositions), so that module now builds with no warnings. Those warnings had flooded the receiver report that #193 fixed.

Evidence that only proofs changed: checked locally on v4.34.0, not by CI.

• lake build: success. Deprecation warnings go from 11 to 0, and all warnings from 27 to 11 (all style lints, left alone).
• lake exe frontier-audit -- LeanFrontier before and after: the same 477 declarations, with identical canonical types, kinds and axioms. No accepted statement changed.
• lake env leanchecker passes on all 8 edited modules.

🤖 Generated with Claude Code

[carlok]

Updated after #223, #225–#228 merged: brought up to date with main, marked dossier targets G and H landed, and fixed two more deprecations (if_true/if_false in #227's SternBrocot/NodeInterval.lean). Re-verified on the new corpus: lake build with 0 deprecation warnings; frontier-audit -- LeanFrontier before/after reports the same 486 declarations with identical canonical types, kinds and axioms; leanchecker passes on all 9 edited modules.