We present a machine-checked formalization of structurally governed AI workflow architectures and prove that effect-level governance can be imposed without reducing internal computational expressivity. Using Interaction Trees in Rocq 8.19, we define a governance operator G that mediates all effectful directives, including memory access, external calls, and oracle (LLM) queries. Our development compiles with 0 admitted lemmas and consists of 36 modules, ~12,000 lines of Rocq, and 454 theorems. We establishseven properties: (P1) governed Turing completeness, (P2) governed oracle expressivity, (P3) a decidability boundary in which governance predicates are total and closed under Boolean composition while semantic program properties remain non-trivial and undecidable by governance, (P4) goal preservation for permitted executions, (P5) expressive minimality of primitive capabilities (compute, memory, reasoning, external call, observability), (P6) subsumption asymmetry showing structural governance strictly subsumes content-level filtering, and (P7) semantic transparency: on all executions where governance permits, the governed interpretation is observationally equivalent (modulo governance-only events) to the ungoverned interpretation. Together, these results show that governance and computational expressivity are orthogonal dimensions: governance constrains the effect boundary of programs while remaining semantically transparent to internal computation.

翻译：我们提出了一种机器检验的结构化治理AI工作流架构的形式化方法，并证明可以在不降低内部计算表达能力的前提下施加效果级治理。通过在Rocq 8.19中使用交互树，我们定义了一个治理算子G，该算子中介所有具有效果性的指令，包括内存访问、外部调用和预言机（大语言模型）查询。我们的开发工作零假设引理，包含36个模块、约12,000行Rocq代码和454个定理。我们建立了七项性质：（P1）受治理的图灵完备性；（P2）受治理的预言机表达能力；（P3）一个可判定性边界：在此边界内治理谓词是全的且在布尔复合下封闭，而语义程序属性对治理而言是非平凡且不可判定的；（P4）允许执行的目标保持性；（P5）原始能力（计算、内存、推理、外部调用、可观测性）的表达极简性；（P6）包含非对称性：表明结构化治理严格包含内容级过滤；（P7）语义透明性：在所有治理允许的执行中，受治理的解释与未受治理的解释在观测上（除治理专有事件外）等价。这些结果共同表明：治理与计算表达能力是正交维度——治理约束程序的效果边界，同时保持对内部计算的语义透明性。