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个模块、约12000行Rocq代码及454条定理。我们建立了七个性质：(P1) 受治理的图灵完备性，(P2) 受治理的预言机表达能力，(P3) 一个可判定性边界：在此边界内，治理谓词是完备的且在布尔组合下封闭，而语义程序性质仍保持非平凡且不可被治理判定，(P4) 许可执行的目标保持性，(P5) 原始能力（计算、内存、推理、外部调用、可观测性）的表达最小性，(P6) 包容不对称性：结构治理严格包容内容级过滤，(P7) 语义透明性：在所有被治理许可的执行中，受治理的解释（排除纯治理事件）与无治理的解释在观测上等价。这些结果共同表明：治理与计算表达能力是正交维度——治理约束程序的效果边界，同时对内部计算保持语义透明。