Upgrade benchmark to Lean 4.24 for lean-lsp-mcp

[Th0rgal]

Summary

• upgrade the benchmark workspace and all 36 case manifests to Lean 4.24.0
• pin final Verity Lean 4.24 commit e271e1248eba4939d09ae92b5eb161d3efed9cc7 and refresh the Lake dependency graph
• regenerate the canonical inventory/report/evaluated-surface metadata
• make the MCP preflight short-circuit test explicitly inject a compatibility failure now that the real benchmark toolchain is compatible
• validate the pinned lean-lsp-mcp==0.28.0 integration against the final Verity revision
• empirically validate JSON-text tool fallback when a provider does not support native tool_calls, instead of assuming fallback support
• support provider-default sampling contracts by omitting temperature, top_p, and reasoning_effort for builtin and metered shell harnesses
• bound JSON-text protocol negotiation to three accounted attempts so stochastic malformed turns do not randomly invalidate otherwise compatible providers

Dependencies

This PR is intentionally stacked and must land after, in order:

1. Upgrade Lean toolchain to 4.24 EVMYulLean#2 (stacked on EVMYulLean Make benchmark ops agent-friendly #1)
2. Upgrade Lean toolchain to 4.24 verity#2193
3. Harness: reusable public dependency prewarm with visible setup #135 (this PR base; provides the builtin lean-lsp-mcp 0.28.0 harness)

Exact dependency pins:

• Verity: e271e1248eba4939d09ae92b5eb161d3efed9cc7
• EVMYulLean (transitive through Verity): 38d53df8b4488d5322894619ea8385fcbb2e6f5d

Validation

• lake update verity: resolved the exact final Verity SHA
• lake build: 2489 jobs passed under Lean 4.24.0
• PATH=/opt/homebrew/bin:$PATH ./scripts/check.sh: 279 tests, all 35 group workspaces, verifier/reference/axiom/pin/manifest checks passed
• PATH=/opt/homebrew/bin:$PATH python3 scripts/check.py all: all 9 checks passed; validated 35 family, 36 implementation, 36 case, and 204 task manifests; Verity pin 0 commits behind
• PATH=/opt/homebrew/bin:$PATH python3 scripts/smoke_builtin_lean_lsp_mcp.py: passed with lean-lsp-mcp==0.28.0, workspace Lean 4.24.0, one initialization, and one successful lean_local_search returning Benchmark.Cases.Ethereum.DepositContractMinimal.deposit_increments_deposit_count_spec
• Leanstral protocol regression: malformed native sentinel output is rejected, while an exact JSON-text preflight_echo response is accepted and selects json_text_fallback
• git diff --check

The host system /usr/bin/python3 is 3.9 and cannot import tomllib; the final complete Python suites used Homebrew Python 3.14.3. This is an environment requirement already reflected by the manifest checker, not a benchmark failure.

Current benchmark head: 5240b4be2c26ba82c68578e3414e818fac732efa.

This remains a draft until the stacked EVMYulLean, Verity, and harness dependencies land. Do not merge out of order.

[Th0rgal]

Superseded by #137. #135 was squash-merged and its head branch deleted, which permanently closed this stacked PR; #137 contains the same five benchmark-specific commits rebased onto the merged main.