pv bindings and proof-status: ghost bindings and unearned proof credit #5333

Scope

pv bindings and proof-status defects: bindings that point at functions that no longer exist, and proof levels claimed without evidence.

Why it matters

A ghost binding or an unearned proof level overstates what is verified.

Done when

pv reports zero ghost bindings on main, and every claimed proof level has its evidence file.

Parent epic: #3269.

Rows

• proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems #4351 — proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems (branch: 91/4351-on-r5a)
• 213 restored binding.yaml rows name symbols that do not resolve (bindings-gate ghosts, #4369 follow-up) #4379 — 213 restored binding.yaml rows name symbols that do not resolve (bindings-gate ghosts, Migrate the 12 hand-rolled producer build.rs key builders onto build_helper::env_key (#2699 remainder) #4369 follow-up) (branch: e6/4379-ghost-bindings)
• bindings resolver: bin-only modules and OUT_DIR-generated items are invisible to the ONT-3a walk (5 allowlisted rows) #4420 — bindings resolver: bin-only modules and OUT_DIR-generated items are invisible to the ONT-3a walk (5 allowlisted rows) (branch: e6/4420-resolver-bin-outdir)
• pv extract:code: binding function: Type::method never resolves; bare method names are ambiguous across impls #4521 — pv extract:code: binding function: Type::method never resolves; bare method names are ambiguous across impls
• binding-allowlist: 173 ghost bindings (debt ledger, goal empty) #4530 — binding-allowlist: 173 ghost bindings (debt ledger, goal empty)
• pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings #4531 — pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings
• pv bindings resolver: follow OUT_DIR includes mapped to a checked-in file (arch_requirements fallback) #5008 — pv bindings resolver: follow OUT_DIR includes mapped to a checked-in file (arch_requirements fallback)

Each row was a separate ticket, folded here under the 100-open-ticket cap (TRIAGE-100, 2026-10-14) and closed as not planned. Reopen a row's ticket when its work starts; an open PR for it reopens it.

Agent: aprender-clerk