A Bounded, Machine-Checkable Governance Kernel for Trust-Gated Agent Execution

We present a bounded, machine-checkable governance kernel for agent systems, formalized in the Lean 4 theorem prover. The kernel couples three execution-boundary properties: (1) a liveness detection theorem for a discrete Beta-style trust model proving that sustained failure forces threshold crossing in finite steps from any finite starting state, (2) a safety governed-execution theorem proving that when the circuit is open, a spend-bearing action is blocked before budget mutation, and when execution succeeds, the resulting spend state remains within the configured budget limit, and (3) a risk-calibrated admissibility theorem proving that higher-risk actions can execute only when a stricter trust threshold is satisfied. A hardened capped-prior variant yields a uniform responsiveness bound independent of arbitrarily long benign history. These proofs are explicitly separated from the deployed runtime, which extends the trust model with float weights and bidirectional decay that are implemented but not formally verified here. The supplementary Lean 4 proof artifact builds as a standalone package with zero sorry markers across the core theorem surface.