面向AI工作流架构的效果透明治理：语义保持、表达极小性与可判定性边界

我们提出了对结构化治理的AI工作流架构的机器验证形式化，并证明可以在不降低内部计算表达能力的情况下施加效果层面的治理。我们使用Rocq 8.19中的Interaction Trees（交互树）定义了一个治理算子G，它中介所有带效果的指令，包括内存访问、外部调用和oracle（LLM）查询。我们的开发以0个被承认引理通过编译，由36个模块、约12,000行Rocq代码和454个定理组成。我们建立了七条性质：(P1) 受治理的图灵完备性；(P2) 受治理的oracle表达能力；(P3) 一条可判定性边界——治理谓词是全函数且在布尔组合下封闭，而语义程序性质仍然非平凡且无法由治理判定；(P4) 对被允许执行的目标保持性；(P5) 原始能力（计算、内存、推理、外部调用、可观测性）的表达极小性；(P6) 包含不对称性，表明结构化治理严格包含内容级过滤；(P7) 语义透明性：在治理允许的所有执行上，受治理解释在以仅治理事件为模的意义下与无治理解释观测等价。综合起来，这些结果表明治理与计算表达能力是正交的维度：治理约束程序的效果边界，同时对内部计算保持语义透明。