归因不可行性：在共线性条件下，没有特征排序方法同时满足忠实性、稳定性与完整性

当特征存在共线性时，不存在任何特征排序方法能够同时满足忠实性、稳定性与完整性。对于共线特征对，排序过程等价于硬币抛掷。我们证明了这一不可行性，并对四类模型进行量化分析，通过集成平均方法（DASH）进行解决方案，并借助305个Lean 4定理进行机械验证。我们刻画了完整的归因设计空间：恰好存在两类方法——忠实性-完整性方法（不稳定，排序在50%的时间内会翻转）与像DASH这样的集成方法（稳定，对称特征报告平局），而不存在其他方法落在这一二元对立之外。该不可行性具有量化意义：对于梯度提升树，归因比例随1/(1-rho^2)发散；对于Lasso，归因比例无穷大；而对随机森林则收敛。DASH（Diversified Aggregation of SHAP）在无偏聚合方法中实现了Cramer-Rao方差界，并给出紧密的集成规模公式。在77个公开数据集的调查中，68%的数据集表现出归因不稳定性。当特征具有相等的因果效应时，切换到条件SHAP也无法逃避这一不可行性。该框架包含实用诊断工具——Z检验工作流程和单模型筛选工具——并直接影响公平性审计：在共线性条件下，基于SHAP的代理性别歧视审计必然不可靠。该设计空间定理、诊断工具以及不可行性在Lean 4中进行机械验证（305个定理，16个公理，0个sorry）——据我们所知，这是解释性人工智能领域首个被形式化验证的不可行性结果。