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，用于中介所有效果指令，包括内存访问、外部调用和预言机（LLM）查询。我们的开发编译通过，未引入任何待证引理，包含36个模块、约12,000行Rocq代码和454个定理。我们确立了七个性质：(P1) 受治理的图灵完备性；(P2) 受治理的预言机表达能力；(P3) 可判定性边界——治理谓词是全的且在布尔组合下封闭，而语义程序性质对治理而言保持非平凡且不可判定；(P4) 允许执行的目标保持性；(P5) 原始能力（计算、内存、推理、外部调用、可观察性）的表达简约性；(P6) 包含不对称性——表明结构治理严格包含内容级过滤；(P7) 语义透明性：在所有治理允许的执行中，受治理的解释与未受治理的解释（除治理专属事件外）在观察上等价。这些结果共同表明，治理与计算表达能力是正交维度：治理约束程序的效果边界，同时对内部计算保持语义透明。