基于前提消除的数据缓存中的导出惩罚：容量、强逆近似与色散二分法

我们引入一个信息论框架，用于在独立前提消除（premise erasure）条件下，对推理引擎中的缓存进行建模。我们比较两种解码器模型：一种是使用任意 bit-string 缓存配合通用解码器的编码方案，另一种是受导出约束的方案，其中缓存由逻辑事实组成，解码器必须生成有效证明。我们建立了四个编码定理。第一个证明，每一步导出都携带由基本大小决定的普遍每步信息内容。第二个揭示了线性链架构与平衡-合并 Datalog 架构在相同深度下的指数容量分离。第三个识别了一个关键访问频率，将其划分为缓存和按需导出最优的 regimes。第四个确定了在消除条件下的最小受导出约束缓存，将查询信息分解为可靠缓存与噪声信道容量。核心结果是导出惩罚：受导出约束缓存与编码缓存之比在所有查询数量、重叠结构和可靠性目标下，都收敛于消除率的倒数。这一惩罚源于一个结构性缓存刚性定理：只有位于目标查询导出有向无环图（derivation DAG）内的缓存事实才对韧性作出贡献，阻止了跨坐标误差纠正。除容量外，我们还证明了在 KL 散度率下的强逆近似，带有 Bahadur--Rao 前缀因子；一个色散二分法（positive coded dispersion 相对于 zero derivation-constrained dispersion）；以及一个完整的八 regime 相位图。架构相关的深度-依赖映射导致合并架构的指数级更尖锐的相位转变。所有结果在同义表示之间都可迁移。