Make the proof suite say what it actually ran

The suite had fifteen checks that could not lose. The visual HashHop arena
painted a cyan line and a white ring on the answer slot, then asked the model
to find the answer by looking; the collector re-rolled puzzles until the
running rate crossed its target; the cache check passed if any layer had ever
recorded an entry; the repository check passed on a call graph built in memory
without touching the store; the research-module check asserted non-empty lists
of SHA256-derived placeholder vectors and so could not fail.

Each check now answers for one claim and reports a verdict the reader can act
on: passed, failed, deferred, or removed. A deferred row names what is missing
and the command that would settle it; a removed row says why the old claim was
withdrawn. The suite verdict is failed > deferred > passed, so a claim that
never ran holds the whole report back from saying "proven".

- evals.py (2427 lines) becomes the proofs/ package; largest module 445 lines.
- proofs/__main__.py deleted: it duplicated PRDProofSuite.latest() with a
  different glob. proofs/table.py renders; latest-proof-suite is the one face
  and exits 1 on a failed verdict.
- The arena paints nothing. The puzzle id is printed on its tile instead,
  because removing the ink without it removes the question.
- HashHop runs a fixed 8 puzzles per depth instead of re-rolling to target.
- The contradiction corpus moves from code to contradiction_scenarios.json;
  the check stays deferred while the corpus is the one this repo authored.
- The cache check compiles a nonce question over a real atom twice and reads
  the miss to hit movement; an empty store fails instead of agreeing by luck.
- The repository check requires rows in the store; the research-module check is
  removed.

Two product bugs surfaced on the way:
- text_index.fts_query joined Latin terms with a space, which FTS5 reads as
  AND, so a question longer than its answer retrieved nothing. Terms are ORed
  and bm25 rank orders the candidates.
- profiles.windows_path_to_wsl prefixed /mnt/ onto an already-POSIX path with
  an empty drive, producing /mnt//home/... and failing every launcher probe.

Verification: 168 passed (pytest backend/tests bench/tests); ruff clean on the
proofs package, cli.py, text_index.py, profiles.py, and both test files; mypy
clean on 16 files with a fresh cache; pyright reports 0 errors on proofs/ and
the test file. Ruff debt elsewhere is unchanged: 19 errors in seven files this
commit does not touch, measured against the same files at HEAD.

backend/src/ely_eye/text_index.py

@@ -38,11 +38,19 @@ def fts_query(query: str) -> str:
     A CJK run becomes a quoted phrase so its characters stay adjacent: unphrased, a query for
     钥匙 would match text that mentions 钥 and 匙 worlds apart. Latin tokens get a prefix match,
     which is what lets `atom` reach `atoms`.
+
+    Latin tokens are OR-ed, not AND-ed. A question is longer than the sentence that answers it —
+    "Which PRD requirements prove long context memory, HashHop, and adapters?" shares only some of
+    its words with any single atom — and an AND over every word answers such a question with
+    nothing. bm25 then ranks the candidates by how many of those words each one carries, so the
+    broadened query does not mean a diluted answer.
     """
     terms = _bare(query).split()
     if not terms:
         raise ValueError(f"search needs at least one searchable word, got {query!r}")
-    return " ".join(_cjk_phrase(term) if _is_cjk(term) else f"{_quote(term)}*" for term in terms)
+    if len(terms) == 1:
+        return _cjk_phrase(terms[0]) if _is_cjk(terms[0]) else f"{_quote(terms[0])}*"
+    return " OR ".join(_cjk_phrase(term) if _is_cjk(term) else f"{_quote(term)}*" for term in terms)
 
 
 def _bare(text: str) -> str: