Bounding What Lean Gets to See: Candidate Exposure in Proof-Action Ranking

Tactic rankers determine which proof actions Lean gets to check. Trace matching measures recovery of one recorded action; candidate exposure measures whether the submitted list contains any action Lean accepts. We derive exposure guarantees for similarity retrieval with tactic-family priors. A soft prior of weight λ preserves within-family order and can reverse only comparisons within a similarity gap of λ. Counting these rivals gives a sufficient top-k retention condition under any family prediction; accounting for their shared probabilities gives the exact worst-case rank. Hard routing instead places entire families ahead of a candidate, regardless of similarity. Experiments use 3,723 proof steps from 1,702 theorems in a curated mathlib4 subset. Hard routing moves the first trace-family candidate from mean rank 41 to 531, while soft and unguided ranking have nearly identical trace exact@5 (0.170 and 0.169). Reanalysis of fixed top-five lists with corrected, target-excluding Lean outcomes on 497 matched states gives Accept@5 of 0.412 for unguided retrieval, 0.408 for the soft prior, and 0.342 for hard routing. The hard-minus-unguided difference is -7.04 percentage points (95% theorem-cluster interval [-11.80,-2.59]); the soft difference is -0.40 points ([-1.70,0.84]). Hard routing leads at the first candidate but falls behind by the third. For unguided retrieval, 139 of 205 accepted lists (67.8%) contain no trace hit. The checking cutoff is therefore part of the ranking objective: family predictions should preserve accepted alternatives at the list length the prover actually uses.