We present an algebraic semantics for governed execution in which governance is axiomatized, compositional, and coterminous with expressibility. The framework, mechanized in 32 Rocq modules (~12,000 lines, 454 theorems, 0 admitted), is built on interaction trees and parameterized coinduction. A three-axiom GovernanceAlgebra record (safety, transparency, properness) induces a symmetric monoidal category with verified pentagon, triangle, and hexagon coherence, where every tensor composition preserves governance. An algebraic effect system constrains the handler algebra so that only governance-preserving handlers can be constructed in the safe fragment; programs in the empty capability set provably emit only observability directives. Capability-indexed composition bundles programs with machine-checked capability bounds, and a dual guarantee theorem establishes that within_caps and gov_safe hold simultaneously under all composition operators. The capstone result is the coterminous boundary: within our formal model, every program expressible via the four primitive morphism constructors is governed under interpretation, and every governed program is the image of such a program. Turing completeness is preserved inside governance; unmediated I/O is excluded from the governed fragment. Governance denial is modeled as safe coinductive divergence. The governance algebra is parametric: any system instantiating the three axioms inherits all derived properties, including convergence, compositional closure, and goal preservation. Extracted OCaml runs as a NIF in the BEAM runtime, with property-based testing (70,000+ random inputs, zero disagreements) confirming behavioral equivalence between the specification and the runtime interpreter.

翻译：我们提出了一种有界执行的代数语义，其中治理被公理化、组合化，并与表达能力同界。该框架在32个Rocq模块中实现（约12,000行代码、454个定理、0个未证明定理），基于交互树和参数化余归纳。一个包含三条公理（安全性、透明性、适定性）的治理代数记录（GovernanceAlgebra）诱导出一个对称幺半范畴，其五边形、三角形和六边形相干性已通过验证，且每个张量组合都保持治理。代数效应系统约束了处理器代数，使得在安全片段中只能构造保持治理的处理器；空能力集上的程序可证明仅发出可观测性指令。基于能力索引的组合将程序与机器验证的能力边界整合在一起，一个对偶保证定理确立了在全部组合算子下within_caps和gov_safe同时成立。顶点结果是同界边界：在我们的形式模型中，通过四种原始态射构造子可表达的每个程序在解释下都是有界的，而每个有界程序都是此类程序的像。图灵完备性在治理内部得以保持；无中介的输入/输出被排除在有界片段之外。治理拒绝被建模为安全的余归纳发散。治理代数是参数化的：任何实例化三条公理的系统都继承所有派生性质，包括收敛性、组合封闭性和目标保持性。提取的OCaml代码在BEAM运行时中以本机接口函数（NIF）运行，通过基于属性的测试（70,000+随机输入，零不一致）确认了规约与运行时解释器之间的行为等价性。