Don't render a prior-art hedge as a confirmed duplicate

.github/CHALLENGE_REVIEW_RULES.md

@@ -126,7 +126,7 @@ Return a single JSON object:
     "difficulty": "exercise" | "substantial" | "research" | "open_problem",
     "estimated_lines": <int: lines of Lean a solution would take>,
     "estimate_basis": "<one sentence: what the estimate rests on>",
-    "already_formalized": "<Mathlib or pool declaration that already proves this, or empty>",
+    "already_formalized": "<the Mathlib or pool declaration that already proves this — a bare declaration name and nothing else. Leave EMPTY if you found none or could not check; do not write a sentence here, and never use it to say the question is unverifiable>",
     "assessment_one_sentence": "<one sentence: the bottom line for the maintainer>"
   },
   "verdict": "approve" | "request_changes" | "needs_discussion",

.github/REVIEW_RULES.md

@@ -122,7 +122,7 @@ Return a single JSON object:
     "proves_the_claim": "proves_it" | "weaker_than_claimed" | "mismatch" | "unverifiable",
     "claim_note": "<one sentence: what the main theorem actually says, especially where it is narrower than the card's prose>",
     "assumed_inputs": "<what the headline takes as hypothesis rather than proving, and whether the card discloses it; empty if it assumes nothing>",
-    "already_formalized": "<Mathlib or pool declaration that already proves this, or empty>",
+    "already_formalized": "<the Mathlib or pool declaration that already proves this — a bare declaration name and nothing else. Leave EMPTY if you found none or could not check; do not write a sentence here, and never use it to say the question is unverifiable>",
     "source_match": "matches" | "mismatch" | "unverifiable" | "not_a_known_result",
     "code_quality": <int 1-5 where 1 = clear AI slop, 3 = competent, 5 = mathlib-merge-ready; anything other than 3 needs a finding or the note below to point at what earned it>,
     "significance_one_sentence": "<one sentence: what would a mathematician say the contribution is, or why it isn't one>"

python/lean_pool/review.py

@@ -1179,7 +1179,7 @@ def render_project_assessment(payload: dict) -> str:
     ]
     already = (a.get("already_formalized") or "").strip()
     if already:
-        rows.append(("Already formalized", f"🛑 `{already}`"))
+        rows.append(("Already formalized", _prior_art_cell(already)))
     assumed = (a.get("assumed_inputs") or "").strip()
     if assumed:
         rows.append(("Assumed, not proved", assumed))
@@ -1266,7 +1266,7 @@ def render_challenge_assessment(payload: dict) -> str:
     ]
     already = (a.get("already_formalized") or "").strip()
     if already:
-        rows.append(("Already formalized", f"🛑 `{already}`"))
+        rows.append(("Already formalized", _prior_art_cell(already)))
 
     table = "| Aspect | Value |\n|---|---|\n"
     for key, value in rows:
@@ -1288,6 +1288,21 @@ def _icon_cell(icons: dict[str, str], value: str) -> str:
     return f"{icons.get(value, '•')} `{value}`"
 
 
+def _prior_art_cell(value: str) -> str:
+    """Render an ``already_formalized`` value at its actual confidence.
+
+    The field is specified as a declaration name or nothing, but the
+    model sometimes answers the question in prose instead — the first
+    production run under the new rules returned "unverifiable from the
+    supplied diff". Stamping 🛑 on that reads as "this is a duplicate" on
+    a PR the same review approved, which is the opposite of what it said.
+    Treat a multi-word answer as the hedge it is.
+    """
+    if " " in value:
+        return f"🟡 {value}"
+    return f"🛑 `{value}`"
+
+
 def render_solution_assessment(payload: dict) -> str:
     """Render a solution assessment block as a Markdown table."""
     a = payload.get("assessment") or {}

python/tests/test_review.py

@@ -949,6 +949,27 @@ def test_project_assessment_leads_with_the_ungated_checks() -> None:
     assert "Obscure problem" not in table
 
 
+def test_prior_art_hedge_is_not_rendered_as_a_duplicate() -> None:
+    """A prose non-answer must not wear the stop icon a real hit earns.
+
+    The first production run under these rules answered
+    `already_formalized` with "unverifiable from the supplied diff" on a
+    PR it approved; rendering that with 🛑 said the opposite.
+    """
+    from lean_pool.review import render_project_assessment
+
+    hedged = render_project_assessment(
+        {"assessment": {"already_formalized": "unverifiable from the supplied diff"}}
+    )
+    hit = render_project_assessment(
+        {"assessment": {"already_formalized": "SimpleGraph.nonempty_hom"}}
+    )
+
+    assert "🛑" not in hedged
+    assert "🟡 unverifiable from the supplied diff" in hedged
+    assert "🛑 `SimpleGraph.nonempty_hom`" in hit
+
+
 def test_project_assessment_omits_empty_optional_rows() -> None:
     """A clean project shows no prior-art or assumption row at all."""
     from lean_pool.review import render_project_assessment