Model Collapse Despite Ground-Truth Verification

Exact verifier labels do not stop a sampled source from losing target support. A proof system can certify every retained artifact while leaving target modes that never reach the verifier untested. Lean answers one local question: did this artifact check in the declared environment? It checks survivors; it cannot restore target support that generation or filtering removed. We formalize this support-loss form of collapse for proof-supervised LLMs. Lean acceptance is exact for a sampled formal artifact; it is not a claim that the artifact distribution equals the target population. A target-risk claim concerns tasks $x\sim P$ in a different space $\mathcal{X}$. We therefore separate artifact checks from target-task risk. A target-risk report must declare an adapter and audit it over target modes. Our first result shows the cost of missing support: if a target mode has positive mass but zero anchored source mass, two systems can have the same verifier statistics while their target risks differ by that mode's mass. The verifier has not failed; the denominator has changed. Our fixed-model bound charges residual mass, unsupported target mass, and, on supported modes, verified source loss, loss-class discrepancy, formalization error, and holdout uncertainty. For hypothesis testing, a verified aggregate becomes evidence about $P$ only after the report declares the tested population $P$, $H_0$, $H_1$, the test level $\eta$, and the upper-bound statistic $T_{\mathrm{audit}}$. The rejection rule is then explicit, for example $T_{\mathrm{audit}}\le\epsilon$.