The Autonomy Trilemma: A Formal Lower-Bound Thesis for Governed Autonomous Systems

Authors: Mindburn Labs
Version: 2.0
Date: 2026-03-18
Status: Foundational thesis — external review invited
Related: UCS v1.2 §0.6, HUDF §2.4

Abstract

We formalize the Autonomy Trilemma: a lower-bound thesis for governed autonomous systems. We argue that no sound system can simultaneously achieve extensible action spaces, self-contained deterministic replay, and bounded proof surface. We define these properties in a computational model, prove the lower bound via an information-theoretic argument over the total replay burden, show the three feasible trade-off regions, and present HELM's Universal Deployment Framework (HUDF) as a risk-indexed resolution strategy. The result provides the theoretical foundation for HELM's architectural stance that enforcement semantics must never be forked, and that the correct lever for navigating the trilemma is varying what is proved per risk class.

1. Computational Model

1.1 Governed Autonomous System (GAS)

A Governed Autonomous System is a tuple S = (A, Π, E, V) where:

• A is the action space: the set of all possible side-effectful actions the system can execute. We parameterize by |A| = n.
• Π is the policy space: a set of policy functions π: A → {ALLOW, DENY} that partition A into permitted and forbidden actions.
• E: A × Π → {0,1}* is the execution function that, given an action a ∈ A and active policy π ∈ Π, produces a cryptographic receipt.
• V: {0,1}* × A × Π → {ACCEPT, REJECT} is the verifier that checks whether a receipt is valid for a given action under a given policy.

1.2 Operational Semantics

At each time step, the system:

1. Receives an intent i (natural language or structured request).
2. The planner selects an action a ∈ A (stochastic — may involve LLM reasoning).
3. The enforcer evaluates π(a) and, if ALLOW, produces a receipt r = E(a, π).
4. A third-party verifier can later check V(r, a, π) = ACCEPT using only (r, a, π) — no access to the original execution environment.

1.3 Soundness Requirement

The system is sound if and only if:

∀ a ∈ A, ∀ π ∈ Π: If V(r, a, π) = ACCEPT, then π(a) = ALLOW.

That is: no receipt is accepted for a forbidden action. This is the fail-closed invariant.

2. The Three Properties

2.1 Extensible Action Space (F)

Intuition: The system supports dynamically-extensible, non-pre-enumerated action spaces. New tools, connectors, and capabilities can be added at runtime without recompiling the system or regenerating the policy space.

Formal definition: A system satisfies F(n) if the action space |A| ≥ n and the system does not require a priori enumeration of A at deployment time. Specifically:

• Actions may be added to A at runtime (dynamic tool integration, connector discovery).
• The planner may select actions from A that did not exist at genesis time.
• No compile-time bound on |A| is required for the system to operate correctly.

A system achieves unbounded extensibility F(∞) if it satisfies F(n) for all n ∈ ℕ.

What this captures: Open-ended reasoning, dynamic tool integration, novel connector discovery. The system doesn't need to know all possible actions at compile time.

2.2 Self-Contained Deterministic Replay (D)

Intuition: Every execution produces a self-contained proof artifact that a third party can use to deterministically re-derive the enforcement verdict, without access to any external oracle, the original execution environment, or any stochastic process.

Formal definition: A system satisfies D if for every execution (a, π, r):

• The receipt r, together with a and π, is sufficient for a third party to deterministically verify V(r, a, π) = ACCEPT.
• No external oracle, runtime state, or wall-clock dependency is required for verification.
• The receipt is non-repudiable: given (r, a, π), no party can produce an alternative receipt r' for the same (a, π) with a different verdict.

What this captures: Audit, legal non-repudiation, deterministic dispute resolution.

2.3 Bounded Proof Surface (O)

Intuition: The total independent replay burden — everything a third-party verifier needs beyond (a, π) to reproduce the verdict — is bounded.

Formal definition. The proof surface of an execution has two components:

Primary (information content): The total replay material that must be committed:

• |r| — receipt size (bits)
• |π_r| — retained policy state: the subset of π that the verifier must inspect
• |w| — auxiliary witness: any committed supplementary data needed for replay (solver traces, CPI evaluation logs, signature chains)

Secondary (operational cost): The work the verifier must perform:

• T(V) — verifier runtime: time(V(r, a, π))

The theorem (§3) establishes a formal lower bound on the primary component. The secondary component is bounded from below under any reasonable computational model (a verifier that reads Ω(log n) bits of input must spend at least Ω(log n) time), but we state this as an operational consequence rather than a separate formal claim.

A system satisfies O(c) for constant c if the primary proof surface is bounded:

|r| + |π_r| + |w| ≤ c

for all executions, independent of |A|.

What this captures: Unit economics of governance. A constant proof surface means governance cost does not scale with system capability.

3. The Autonomy Trilemma

3.1 Theorem Statement (Lower Bound)

Theorem (Autonomy Trilemma). For any sound Governed Autonomous System S = (A, Π, E, V) with self-contained deterministic replay, if the action space is extensible, then the proof surface grows with the action space.

Formally: If S is sound ∧ F(∞) ∧ D, then ¬O(c) for any fixed c.

3.2 Proof

Assume for contradiction that there exists a sound system S satisfying F(∞) ∧ D ∧ O(c).

Step 1: The verifier's discrimination task.

Because S is sound, the verifier V must affirm that the specific action a is permitted by π. Consider a verifier that receives (r, a, π) for an action a ∈ A under policy π. The verifier's task is to confirm that π(a) = ALLOW.

Now consider two distinct actions a₁, a₂ ∈ A where π(a₁) = ALLOW and π(a₂) = DENY, but a₁ and a₂ are otherwise structurally similar (e.g., they differ only in a target endpoint or parameter value). The receipt r₁ for a₁ must contain information that discriminates a₁ from a₂ in the context of π — otherwise, a malicious party could present r₁ as evidence for a₂, violating soundness.

Step 2: Proof surfaces must be replay-distinguishable.

The total proof surface — receipt r, retained policy state π_r, and auxiliary witness w — must collectively carry enough information to let the verifier distinguish valid from invalid replay claims.

Consider an adversarial policy class: for each action aₖ ∈ A, define πₖ such that πₖ(aₖ) = ALLOW and πₖ(aⱼ) = DENY for all j ≠ k. These are singleton-allow policies.

Note that the verifier receives (r, a, π) — it already knows the action and the policy. However, the receipt r (together with any auxiliary witness w and retained policy state π_r) must provide a verification path that the verifier can check. The key constraint is: the proof surface for (aₖ, πₖ) must be replay-distinguishable from that of (aⱼ, πₖ) for any denied action aⱼ. That is, a valid proof surface for aₖ under πₖ must not also validate for some aⱼ ≠ aₖ under πₖ — otherwise, a malicious party could replay r as evidence for a different action, violating soundness.

Formally, for singleton-allow policies, the mapping from aₖ to its valid proof surface must be injective: distinct allowed actions require distinguishable proof artifacts. If two distinct actions aₖ, aⱼ could share the same (r, π_r, w), the verifier could not distinguish V(r, aₖ, πₖ) from V(r, aⱼ, πₖ), yet one must ACCEPT and the other REJECT.

Step 3: Information-content lower bound.

There are n = |A| distinct singleton-allow policies, each requiring a replay-distinguishable proof surface. By the injectivity requirement, the total information content of the proof surface must support at least n distinct values. By standard counting:

|r| + |π_r| + |w| ≥ log₂(n) bits

This is a pure information-content bound: the proof surface must carry at least log₂(n) bits of discriminating information, independent of the computational model of the verifier.

Step 4: Contradiction.

By F(∞), n is unbounded — |A| can grow without limit. Therefore:

P ≥ Ω(log n) → ∞ as n → ∞

This contradicts O(c), which requires P ≤ c for fixed c. ∎

3.3 Proof Variant: Policy Complexity

The log₂(n) bound is for the simplest policies (singleton allow). For structured policies — those with complex predicates over action attributes (budget conditions, connector constraints, temporal windows) — the bound can be tighter.

Lemma (Policy Complexity Bound). For a policy π with description length |π| bits, the retained policy state must satisfy:

|π_r| ≥ Ω(|π|)

in the worst case, because the verifier must inspect the policy to confirm the verdict. For systems with rich, composable policies (like HELM's P0/P1/P2 stack), this further increases the proof surface.

3.4 Anticipated Objections

Objection 1: "The policy is compressible. Real policies are small rule sets, not arbitrary subsets."

Correct. The singleton-allow policy class is adversarial — real policies are highly structured. However, the log₂(n) bound on the receipt and witness (|r| + |w|) holds regardless of policy structure. Compressing the policy to |π_r| < |π| reduces one component of the proof surface but does not eliminate the need for the receipt itself to discriminate which action was taken. In practice, this means compressible policies reduce the policy retention component but leave the receipt size component intact.

Put differently: policy compression buys you a smaller π_r, but the receipt still must distinguish 1-of-n actions under that compressed policy. The bound shifts from one budget line to another; it does not vanish.

Objection 2: "What if verification is interactive? A challenge-response protocol could reduce the proof surface."

The theorem as stated (§3.1) applies to self-contained, non-interactive replay — property D requires that a third party can verify from (r, a, π) alone, without contacting the original execution environment. Interactive protocols violate this property by definition: they require a live counterparty.

This is an explicit scope constraint (§4.2), not a gap. Interactive verification trades self-containment (a component of D) for proof surface reduction (a component of O). This trade-off is itself an instance of the trilemma: you are relaxing D to improve O.

That said, interactive protocols are a genuine research direction (§9.3). Single-round challenges against committed execution traces could reduce the proof surface for specific policy classes without fully abandoning self-containment. This is an open question, not an objection to the current result.

Objection 3: "The action space is dynamic. If n grows at runtime, isn't the per-instant proof surface bounded?"

Yes, at any given instant when |A| = n, the proof surface is Ω(log n) — which is finite. The unboundedness manifests over the system's lifetime as new actions are added. For a system that adds actions monotonically, the proof surface must grow without bound over time.

This actually strengthens the thesis: dynamic action spaces make the trilemma harder to navigate, not easier. A system that achieves O(c) at genesis, when |A| is small, will eventually violate that bound as the action space grows — unless it either caps extensibility (sacrificing F) or relaxes replay completeness (sacrificing D) for new actions. HUDF handles this by routing new, uncharacterized actions through higher risk tiers (larger proof surface) until they are classified.

4. Scope of the Result

4.1 What the Theorem Covers

• Any sound system with self-contained replay. The lower bound applies regardless of implementation strategy — pure RBAC, capability tokens, formal verification, or hybrid approaches.
• The proof surface as a whole, not just receipt size. The bound applies to the combined burden of receipts, retained policy, and auxiliary witnesses.
• Adversarial policies. The lower bound holds for the worst-case policy class. In practice, policies are structured, and amortized bounds may be better (see §8).

4.2 What the Theorem Does Not Cover

• Non-adversarial average case. Many real-world policies are highly structured (small allow-lists, attribute-based predicates). The Ω(log n) bound is worst-case; typical deployments may achieve sub-logarithmic amortized proof surfaces for common policies.
• Interactive verification. The bound assumes the verifier is non-interactive (receives (r, a, π) in one shot). Interactive verification protocols (challenge-response, probabilistic checks) may achieve different trade-offs.
• Probabilistic soundness. Systems that tolerate a small probability of false verification (e.g., sampling-based audit) can relax the bound. The theorem applies to perfect soundness.
• Policy compression. If the policy is compressible (e.g., described as a small set of rules rather than an explicit enumeration), the retained policy state may be small even for large action spaces. The Ω(log n) bound on receipt + witness still holds.
• Time-bounded action spaces. If the action space is bounded at any given instant but grows over time, the per-instant proof surface is bounded. The unbounded growth manifests only over the system's lifetime.

4.3 Relationship to Practice

The theorem does not say that governed autonomous systems are infeasible. It says that governance has a cost, and that cost grows with system capability. The engineering question is not "how to avoid the trilemma" but "how to navigate it optimally."

5. Feasible Trade-Off Regions

The trilemma does not preclude useful systems — only the simultaneous maximization of all three properties. Three feasible regions exist:

5.1 Region FD: Full Extensibility + Full Replay (Accept Growing Proof Surface)

• The system supports arbitrary action spaces and produces complete, self-contained proof artifacts.
• Cost: Proof surface grows with Ω(log n) or worse. Storage and verification cost increase as the system scales.
• Example: A high-assurance enterprise deployment with full EvidencePacks and formal verification traces.
• When useful: Regulated industries, high-stakes autonomous decisions, legal defensibility requirements.

5.2 Region DO: Full Replay + Bounded Proof Surface (Accept Bounded Extensibility)

• The system produces bounded-size proofs with bounded verification cost.
• Cost: Action space must be bounded. New tools and connectors cannot be dynamically added without re-bounding.
• Example: A fixed-function verifier with a pre-compiled policy table. Essentially a smart contract.
• When useful: Embedded systems, safety-critical controllers, constrained environments.

5.3 Region FO: Full Extensibility + Bounded Overhead (Accept Incomplete Replay)

• The system supports arbitrary action spaces with bounded proof cost.
• Cost: Not every execution is deterministically replayable from the proof artifact alone. Some actions rely on statistical audit, sampling, or condensed evidence.
• Example: Traditional RBAC/ABAC systems with audit logging but no cryptographic replay capability.
• When useful: Low-risk environments, development, internal tools.

6. HUDF: HELM's Risk-Indexed Resolution

The HELM Universal Deployment Framework (HUDF) navigates the trilemma by varying the proof surface investment per risk class rather than making a single global trade-off.

6.1 Design Corollary: Risk-Indexed Proof Surface

Architectural Claim. The HUDF risk-indexed strategy achieves an effective frontier by allocating proof surface proportionally to risk: high-risk executions receive large proof surfaces (Region FD), low-risk executions receive minimal proof surfaces (Region FO), and enforcement semantics remain invariant across all tiers.

This is a design claim supported by the lower bound, not a formal optimality theorem. Its strength is pragmatic: the alternative — forking enforcement semantics per market segment — provably sacrifices more than necessary.

6.2 The "Never Fork Enforcement" Corollary

Corollary. A system that forks enforcement semantics by market segment (e.g., "skip CPI for SMB") sacrifices soundness to reduce proof surface. HUDF achieves the same proof surface reduction without sacrificing soundness, by relaxing proof completeness per risk class while preserving the fail-closed invariant universally.

This is HELM's central architectural law: the Kernel, PEP, and CPI are never forked. Only the evidence routing policy and capability scope change between deployment profiles. The lower bound justifies this: since the proof surface must grow with capability, the correct lever is limiting what is proved, not weakening how enforcement works.

7. Worked Example: T0 vs. T2 vs. T3

To ground the thesis concretely, consider a system with 1,000,000 registered connector actions.

T0: Send a routine notification (Low Risk)

Third-party replay: not possible from receipt alone. Requires rehydrating batch from cold storage. Soundness maintained for disputes via deterministic replay protocol (§12.2 UCS).

T2: Update a customer CRM record (Medium Risk)

Third-party replay: fully reproducible from (r, a, π). Verifier can independently confirm the action was permitted without any external oracle.

T3: Execute a wire transfer (High Risk)

Third-party replay: fully reproducible. Verifier can re-run the formal verification and confirm not just that the action was permitted, but that the plan satisfies the policy under the budget constraints.

Key Observation

The proof surface grows from 32 bytes (T0) to ~30KB (T3) — a ~1000x increase. This is the trilemma in action: all three tiers support the same million-action space (same fluidity) and the same enforcement semantics (same kernel), but the proof investment grows with risk. The T0/T3 proof surface ratio directly reflects the cost of determinism when fluidity is held constant.

8. Comparison with Prior Impossibility Results

8.1 Key Differences

CAP constrains data systems during network partitions. It is binary (choose CP or AP) and applies only under failure conditions.

The Autonomy Trilemma constrains execution governance at every action. It applies in the common case, not just under failure. It is continuous (a trade-off surface, not a binary choice).

The Blockchain Trilemma was stated informally and has never been formally proved. It remains a conjecture. The Autonomy Trilemma has a formal lower-bound argument against a precisely defined system model, though tighter bounds and extensions to dynamic action spaces remain open (see §8).

9. Open Questions

1. Tighter bounds. The Ω(log n) bound is for worst-case singleton policies. For structured policies (attribute predicates, compact representations), amortized bounds may be sub-logarithmic. What is the tight bound for HELM's P0/P1/P2 policy stack?
2. Dynamic action spaces. The current proof assumes a static |A| = n. For dynamically-extensible spaces where n grows at runtime, the lower bound strengthens — the proof surface must grow unboundedly over the system's lifetime, even if bounded at any instant.
3. Interactive verification. Challenge-response protocols may reshape the proof surface trade-off. Can a single-round challenge reduce the proof surface from Ω(log n) to O(1) for specific policy classes?
4. Quantum implications. ZK-SNARKs already compress proofs; post-quantum ZK may reshape the overhead axis. Does the fundamental log-n barrier persist under quantum verification?
5. Empirical validation. Measured proof surface data from production HELM deployments would ground the theoretical trade-off curves. What is the actual T0/T3 ratio in practice?

Appendix A: Notation Summary

Appendix B: Trade-Off Region Summary

This document is a foundational thesis. The lower bound is formal within the scope defined in §4. The HUDF resolution (§6) is an architectural corollary — a design strategy justified by the lower bound, not a formal optimality claim. Both are open to refinement as the theory matures.