Haoyang Li
A formal explanation certifies a prediction with a subset-minimal sufficient reason. Under incremental disclosure, however, evidence arrives field by field, and a normally sufficient reason can be overturned by later information. We study the smallest reason core that remains sufficient under all admissible later disclosures; its size is the robustness radius. We compile a defeasible classifier into an explicit boundary atlas of entry anchors and exit defeaters, and chart the complexity of auditing it (all statements are in the atlas size). Prediction and standing anchors are read by polynomial-time scans of the atlas, without iterative fixpoint computation; a reason's defeater frontier is obtained by scanning and subset-minimizing the defeaters above it. But verifying that a reason core is robust is coNP-complete, and deciding whether a robust core of size at most theta exists is $Σ_2^p$-complete -- a four-cell P / coNP-complete / NP-complete / $Σ_2^p$-complete landscape, with the accepted (A(t)=1) case reaching the second level of the polynomial hierarchy. The decision version of minimal certified disclosure is NP-complete; its optimization version is fixed-parameter tractable in the number of excluded worlds without defeaters, with the general-defeater case open. On exact audits of depth-limited decision trees over standard tabular datasets under a deliberately small Boolean abstraction, the governing parameters fall in a small-parameter regime (robust cores in the low single digits), so exact robust auditing is tractable in these audited cubes; on adversarial instances built from our reductions the hardness bites, with robust cores of size Theta(n). To our knowledge this is the first $Σ_2^p$-complete audit query for disclosure-robust formal explanations.