Gate literature_search by worker web-search capability

[idrassi]

Closes #4.

Summary

This PR fixes a mixed-backend correctness issue in literature_search.

Previously, --no-isolation was effectively gated by the planner model, but the actual search is executed by the worker backend. That meant configurations such as:

openprover --planner-model opus --worker-model minimax-m2.5 --no-isolation

could expose literature_search to the planner even though the worker could not actually perform web search.

What changed

• gate web-search availability by the worker model, not the planner model
• fail fast for explicit --no-isolation requests when the worker backend cannot perform web search
• add a runtime guard so literature_search cannot silently proceed with a non-search-capable worker
• centralize web-search capability checks in shared model capability helpers
• add focused tests for capability helpers and the CLI validation path
• update docs to clarify that --no-isolation requires a web-search-capable worker model

Validation

Tested with:

python3 -m py_compile openprover/model_caps.py openprover/cli.py openprover/prover.py openprover/llm/claude.py openprover/llm/hf.py tests/test_model_caps.py tests/test_cli_validation.py

python3 -m pytest tests/test_model_caps.py tests/test_cli_validation.py

Also verified that the previously broken mixed-backend case now fails fast with a clear error:

python3 -m openprover --theorem examples/cauchy_schwarz.md --planner-model opus --worker-model minimax-m2.5 --no-isolation --headless --max-time 1s