IV.R246 — The Lean criterion

Scope labels are enforced by the dual-track system: a claim is tau-effective if and only if it has a corresponding Lean 4 theorem in TauLib with zero sorry terms; a claim is conjectural if no such theorem exists. This binary criterion eliminates all ambiguity.