Deterministic faithfulness screen for one informal↔Lean 4 pair: lints, vacuity/triviality checks, and (when a Lean+mathlib REPL is configured and warm) elaboration. Free — no API calls, no key — and ~0.1s once the REPL is warm, so call it constantly while drafting. Catches statements that do not compile, trivially satisfiable existentials, vacuously-true specs, and claims hidden behind an unused declaration.

This screen may only REJECT: an outcome of 'passed_screening' means no defect was found by this harness — it is NOT a certification of faithfulness (measured against human verdicts, human-rejected pairs still passed the full screen 17.0% of the time for theorems, 35.6% for definitions). Every flag is a candidate for human confirmation, not a verdict.

kind is 'theorem' or 'definition'; omit it to infer from the Lean declaration head.

Full faithfulness screen: everything in check_fast plus two independent LLM judges under strict consensus and an adversarial counterexample probe. Costs roughly 17–27¢ per statement (actual spend is reported in the response as actual_cost_usd) and takes 30–60 seconds — call it deliberately, before something ships. Requires ANTHROPIC_API_KEY.

This screen may only REJECT: an outcome of 'passed_screening' means no defect was found by this harness, NOT a certification of faithfulness (measured against human verdicts, human-rejected pairs still passed 17.0% of the time for theorems, 35.6% for definitions). Every flag — including a probe counterexample — is a candidate requiring human confirmation, not a verdict. The response ranks its evidence: a counterexample outranks a deterministic lint, which outranks two-judge consensus; a single-judge flag is below our own reporting bar.

kind is 'theorem' or 'definition'; omit it to infer from the Lean declaration head.